-- Mathlib/RingTheory/Perfection.lean
theorem valAux_eq {f : PreTilt O p} {n : ℕ} (hfn : coeff _ _ n f ≠ 0) :
    valAux K v O p f = ModP.preVal K v O p (coeff _ _ n f) ^ p ^ n

Proof state:
case intro.succ.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff (ModP O p) p n) f ≠ 0
k : ℕ
ih :
  (coeff (ModP O p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (ModP O p) p (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (ModP O p) p (Nat.find h + k + 1)) f
h1 : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
⊢ ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))

Tactic:
have h2 : (Ideal.Quotient.mk _ (x ^ p) : ModP O p) ≠ 0 := by
  erw [RingHom.map_pow, hx, ← RingHom.map_pow, coeff_pow_p]
  exact coeff_nat_find_add_ne_zero k

Result:
case intro.succ.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff (ModP O p) p n) f ≠ 0
k : ℕ
ih :
  (coeff (ModP O p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (ModP O p) p (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (ModP O p) p (Nat.find h + k + 1)) f
h1 : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
h2 : (Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p) ≠ 0
⊢ ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))

Proof state:
case intro.succ.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff (ModP O p) p n) f ≠ 0
k : ℕ
ih :
  (coeff (ModP O p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (ModP O p) p (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (ModP O p) p (Nat.find h + k + 1)) f
h1 : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
h2 : (Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p) ≠ 0
⊢ ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))

Tactic:
erw [ih (coeff_nat_find_add_ne_zero k), ← hx, ← coeff_pow_p, RingHom.map_pow, ← hx,
  ← RingHom.map_pow, ModP.preVal_mk hv h1, ModP.preVal_mk hv h2, RingHom.map_pow, v.map_pow,
  ← pow_mul, pow_succ']

Result:
case intro.succ.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff (ModP O p) p n) f ≠ 0
k : ℕ
ih :
  (coeff (ModP O p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (ModP O p) p (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (ModP O p) p (Nat.find h + k + 1)) f
h1 : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
h2 : (Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p) ≠ 0
⊢ v ((algebraMap O K) x) ^ (p * p ^ (Nat.find h + k)) = v ((algebraMap O K) x) ^ (p * p ^ (Nat.find h).add k)

Proof state:
case intro.succ
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff (ModP O p) p n) f ≠ 0
k : ℕ
ih :
  (coeff (ModP O p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (ModP O p) p (Nat.find h + (k + 1))) f ≠ 0
⊢ ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))

Tactic:
obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective (coeff (ModP O p) p (Nat.find h + k + 1) f)

Result:
case intro.succ.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff (ModP O p) p n) f ≠ 0
k : ℕ
ih :
  (coeff (ModP O p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (ModP O p) p (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (ModP O p) p (Nat.find h + k + 1)) f
⊢ ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))

Proof state:
case intro.succ.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff (ModP O p) p n) f ≠ 0
k : ℕ
ih :
  (coeff (ModP O p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (ModP O p) p (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (ModP O p) p (Nat.find h + k + 1)) f
⊢ ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))

Tactic:
have h1 : (Ideal.Quotient.mk _ x : ModP O p) ≠ 0 := hx.symm ▸ hfn

Result:
case intro.succ.intro
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff (ModP O p) p n) f ≠ 0
k : ℕ
ih :
  (coeff (ModP O p) p (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (ModP O p) p (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (ModP O p) p (Nat.find h + k + 1)) f
h1 : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
⊢ ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h)) f) ^ p ^ Nat.find h =
    ModP.preVal K v O p ((coeff (ModP O p) p (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))