[GOAL]
A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n
x✝ : A
⊢ (fun a n => if x : n = 0 then 1 else Exists.choose (_ : ∃ a_1, (fun a => a ^ n) a_1 = a)) x✝ 0 = 1
[PROOFSTEP]
classical exact dif_pos rfl
[GOAL]
A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n
x✝ : A
⊢ (fun a n => if x : n = 0 then 1 else Exists.choose (_ : ∃ a_1, (fun a => a ^ n) a_1 = a)) x✝ 0 = 1
[PROOFSTEP]
exact dif_pos rfl
[GOAL]
A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n
n✝ : α
a : A
hn : n✝ ≠ 0
⊢ (fun a n => if x : n = 0 then 1 else Exists.choose (_ : ∃ a_1, (fun a => a ^ n) a_1 = a)) a n✝ ^ n✝ = a
[PROOFSTEP]
dsimp only
[GOAL]
A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n
n✝ : α
a : A
hn : n✝ ≠ 0
⊢ (if x : n✝ = 0 then 1 else Exists.choose (_ : ∃ a_1, (fun a => a ^ n✝) a_1 = a)) ^ n✝ = a
[PROOFSTEP]
rw [dif_neg hn]
[GOAL]
A : Type u_1
α : Type u_2
inst✝² : Monoid A
inst✝¹ : Pow A α
inst✝ : Zero α
H : ∀ {n : α}, n ≠ 0 → Function.Surjective fun a => a ^ n
n✝ : α
a : A
hn : n✝ ≠ 0
⊢ Exists.choose (_ : ∃ a_1, (fun a => a ^ n✝) a_1 = a) ^ n✝ = a
[PROOFSTEP]
exact (H hn a).choose_spec
[GOAL]
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ a ∈ n • ⊤
[PROOFSTEP]
rw [H hn]
[GOAL]
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
a : A
n : ℤ
hn : ¬n = 0
⊢ a ∈ ⊤
[PROOFSTEP]
trivial
[GOAL]
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
n✝ : ℤ
a : A
hn : n✝ ≠ 0
⊢ n✝ • (fun a n => if hn : n = 0 then 0 else Exists.choose (_ : a ∈ n • ⊤)) a n✝ = a
[PROOFSTEP]
simp_rw [dif_neg hn]
[GOAL]
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
n✝ : ℤ
a : A
hn : n✝ ≠ 0
⊢ n✝ • Exists.choose (_ : a ∈ n✝ • ⊤) = a
[PROOFSTEP]
generalize_proofs h1
[GOAL]
A : Type u_1
inst✝ : AddCommGroup A
H : ∀ {n : ℤ}, n ≠ 0 → n • ⊤ = ⊤
n✝ : ℤ
a : A
hn : n✝ ≠ 0
h1 : a ∈ n✝ • ⊤
⊢ n✝ • Exists.choose h1 = a
[PROOFSTEP]
exact h1.choose_spec.2
[GOAL]
𝕜 : Type ?u.71834
inst✝¹ : DivisionRing 𝕜
inst✝ : CharZero 𝕜
q : 𝕜
⊢ (fun q n => q / ↑n) q 0 = 0
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type ?u.71834
inst✝¹ : DivisionRing 𝕜
inst✝ : CharZero 𝕜
n : ℤ
q : 𝕜
hn : n ≠ 0
⊢ n • (fun q n => q / ↑n) q n = q
[PROOFSTEP]
rw [zsmul_eq_mul, (Int.cast_commute n _).eq, div_mul_cancel q (Int.cast_ne_zero.mpr hn)]
[GOAL]
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
n : ℤ
a : A
hn : n ≠ 0
⊢ (fun a z =>
          match z with
          | ofNat n => RootableBy.root a n
          | -[n+1] => (RootableBy.root a (n + 1))⁻¹)
        a n ^
      n =
    a
[PROOFSTEP]
induction n
[GOAL]
case ofNat
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : ofNat a✝ ≠ 0
⊢ (fun a z =>
          match z with
          | ofNat n => RootableBy.root a n
          | -[n+1] => (RootableBy.root a (n + 1))⁻¹)
        a (ofNat a✝) ^
      ofNat a✝ =
    a
[PROOFSTEP]
change RootableBy.root a _ ^ _ = a
[GOAL]
case ofNat
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : ofNat a✝ ≠ 0
⊢ RootableBy.root a a✝ ^ ofNat a✝ = a
[PROOFSTEP]
norm_num
[GOAL]
case ofNat
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : ofNat a✝ ≠ 0
⊢ RootableBy.root a a✝ ^ a✝ = a
[PROOFSTEP]
rw [RootableBy.root_cancel]
[GOAL]
case ofNat.a
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : ofNat a✝ ≠ 0
⊢ a✝ ≠ 0
[PROOFSTEP]
rw [Int.ofNat_eq_coe] at hn 
[GOAL]
case ofNat.a
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : ↑a✝ ≠ 0
⊢ a✝ ≠ 0
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
case negSucc
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : -[a✝+1] ≠ 0
⊢ (fun a z =>
          match z with
          | ofNat n => RootableBy.root a n
          | -[n+1] => (RootableBy.root a (n + 1))⁻¹)
        a -[a✝+1] ^
      -[a✝+1] =
    a
[PROOFSTEP]
change (RootableBy.root a _)⁻¹ ^ _ = a
[GOAL]
case negSucc
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : -[a✝+1] ≠ 0
⊢ (RootableBy.root a (a✝ + 1))⁻¹ ^ -[a✝+1] = a
[PROOFSTEP]
norm_num
[GOAL]
case negSucc
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : -[a✝+1] ≠ 0
⊢ RootableBy.root a (a✝ + 1) ^ (a✝ + 1) = a
[PROOFSTEP]
rw [RootableBy.root_cancel]
[GOAL]
case negSucc.a
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℕ
a : A
a✝ : ℕ
hn : -[a✝+1] ≠ 0
⊢ a✝ + 1 ≠ 0
[PROOFSTEP]
norm_num
[GOAL]
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℤ
n : ℕ
a : A
hn : n ≠ 0
⊢ (fun a n => RootableBy.root a ↑n) a n ^ n = a
[PROOFSTEP]
simpa only [zpow_coe_nat] using RootableBy.root_cancel a (show (n : ℤ) ≠ 0 by exact_mod_cast hn)
[GOAL]
A : Type u_1
inst✝¹ : Group A
inst✝ : RootableBy A ℤ
n : ℕ
a : A
hn : n ≠ 0
⊢ ↑n ≠ 0
[PROOFSTEP]
exact_mod_cast hn
[GOAL]
A : Type u_1
B : Type u_2
α : Type u_3
inst✝⁵ : Zero α
inst✝⁴ : Monoid A
inst✝³ : Monoid B
inst✝² : Pow A α
inst✝¹ : Pow B α
inst✝ : RootableBy A α
f : A → B
hf : Surjective f
hpow : ∀ (a : A) (n : α), f (a ^ n) = f a ^ n
n : α
hn : n ≠ 0
x : B
y : A
hy : f y = x
⊢ f (RootableBy.root y n) ^ n = x
[PROOFSTEP]
rw [← hpow (RootableBy.root y n) n, RootableBy.root_cancel _ hn, hy]
