-- Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
theorem solution_spec' {a₁ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (a₂ : 𝕎 k) :
    solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Tactic:
obtain ⟨q, hq⟩ := Nat.exists_eq_succ_of_ne_zero hp.out.ne_zero

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
q : ℕ
hq : p = q.succ
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
q : ℕ
hq : p = q.succ
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Tactic:
have hq' : q = p - 1 := by simp only [hq, tsub_zero, Nat.succ_sub_succ_eq_sub]

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
q : ℕ
hq : p = q.succ
hq' : q = p - 1
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
q : ℕ
hq : p = q.succ
hq' : q = p - 1
⊢ solution p a₁ a₂ * (a₂.coeff 0 / a₁.coeff 0) * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Tactic:
field_simp [ha₁, mul_comm]

Result:
no goals

Proof state:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
q : ℕ
hq : p = q.succ
hq' : q = p - 1
⊢ solution p a₁ a₂ ^ q.succ * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Tactic:
rw [pow_succ', hq', this]

Result:
case intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
q : ℕ
hq : p = q.succ
hq' : q = p - 1
⊢ solution p a₁ a₂ * (a₂.coeff 0 / a₁.coeff 0) * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Tactic:
have := solution_spec p a₁ a₂

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
q : ℕ
hq : p = q.succ
⊢ q = p - 1

Tactic:
simp only [hq, tsub_zero, Nat.succ_sub_succ_eq_sub]

Result:
no goals