-- 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:
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
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p) ≠ 0

Tactic:
erw [RingHom.map_pow, hx, ← RingHom.map_pow, coeff_pow_p]

Result:
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
⊢ (coeff (ModP O p) p (Nat.find h + k)) f ≠ 0

Proof state:
case intro.zero
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
hfn : (coeff (ModP O p) p (Nat.find h + 0)) 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 + 0)) f) ^ p ^ (Nat.find h + 0)

Tactic:
rfl

Result:
no goals

Proof state:
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
n : ℕ
hfn : (coeff (ModP O p) p n) f ≠ 0
⊢ valAux K v O p f = ModP.preVal K v O p ((coeff (ModP O p) p n) f) ^ p ^ n

Tactic:
have h : ∃ n, coeff _ _ n f ≠ 0 := ⟨n, hfn⟩

Result:
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
n : ℕ
hfn : (coeff (ModP O p) p n) f ≠ 0
h : ∃ n, (coeff (ModP O p) p n) f ≠ 0
⊢ valAux K v O p f = ModP.preVal K v O p ((coeff (ModP O p) p n) f) ^ p ^ n

Proof state:
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
n : ℕ
hfn : (coeff (ModP O p) p n) f ≠ 0
h : ∃ n, (coeff (ModP O p) p n) f ≠ 0
⊢ valAux K v O p f = ModP.preVal K v O p ((coeff (ModP O p) p n) f) ^ p ^ n

Tactic:
rw [valAux, dif_pos h]

Result:
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
n : ℕ
hfn : (coeff (ModP O p) p n) f ≠ 0
h : ∃ n, (coeff (ModP O p) p n) 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 n) f) ^ p ^ n

Proof state:
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
n : ℕ
hfn : (coeff (ModP O p) p n) f ≠ 0
h : ∃ n, (coeff (ModP O p) p n) 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 n) f) ^ p ^ n

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le (Nat.find_min' h hfn)

Result:
case 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 : ℕ
hfn : (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)

Proof state:
case 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 : ℕ
hfn : (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)

Tactic:
induction' k with k ih

Result:
case intro.zero
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
hfn : (coeff (ModP O p) p (Nat.find h + 0)) 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 + 0)) f) ^ p ^ (Nat.find h + 0)

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))

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
⊢ v ((algebraMap O K) x) ^ (p * p ^ (Nat.find h + k)) = v ((algebraMap O K) x) ^ (p * p ^ (Nat.find h).add k)

Tactic:
rfl

Result:
no goals