-- Module: Mathlib.RingTheory.Perfection
Goal:
K : Type u₁
inst : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst_1 : CommRing O
inst_2 : Algebra O K
hv : v.Integers O
p : ℕ
inst_3 : Fact (Nat.Prime p)
inst_4 : Fact ¬IsUnit.{u₂} (M := O) (↑p : O)
f : PreTilt O p
h : ∃ (n : ℕ), Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)
k : ℕ
ih :
  ∀
    (hfn :
      Ne (α := ModP O p)
        ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                    Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                  k) :
              (a : PreTilt O p) → ModP O p)
            f :
          ModP O p)
        (0 : ModP O p)),
    ModP.preVal K v O p
          ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h) :
              (a : PreTilt O p) → ModP O p)
            f) ^
        p ^
          Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h =
      ModP.preVal K v O p
          ((coeff
                (Nat.find (p := fun (n : ℕ) ↦
                    Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                  k) :
              (a : PreTilt O p) → ModP O p)
            f) ^
        p ^
          (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k)
hfn :
  Ne (α := ModP O p)
    ((coeff
            (Nat.find (p := fun (n : ℕ) ↦
                Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
              (k + 1)) :
          (a : PreTilt O p) → ModP O p)
        f :
      ModP O p)
    (0 : ModP O p)
x : O
hx :
  Eq (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    ((coeff
            (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                k +
              1) :
          (a : PreTilt O p) → ModP O p)
        f :
      ModP O p)
h1 :
  Ne (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
h2 :
  Ne (α := HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) (x ^ p) :
      HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
    (0 : HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
succ :
  ModP.preVal K v O p
        ((coeff
              (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                k) :
            (a : PreTilt O p) → ModP O p)
          f) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          k) =
    ModP.preVal K v O p
        ((coeff
              (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                (k + 1)) :
            (a : PreTilt O p) → ModP O p)
          f) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          (k + 1))
succ₁ :
  ModP.preVal K v O p
        ((coeff
              (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                k) :
            (a : PreTilt O p) → ModP O p)
          f) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          k) =
    ModP.preVal K v O p
        ((coeff
              (Nat.find (p := fun (n : ℕ) ↦
                    Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                  k +
                1) :
            (a : PreTilt O p) → ModP O p)
          f) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k +
          1)
succ₂ :
  ModP.preVal K v O p
        ((coeff
              (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                k) :
            (a : PreTilt O p) → ModP O p)
          f) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          k) =
    ModP.preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k +
          1)
succ₃ :
  ModP.preVal K v O p
        (HPow.hPow (α := ModP O p)
          ((coeff
                  (Nat.find (p := fun (n : ℕ) ↦
                        Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                      k +
                    1) :
                (a : PreTilt O p) → ModP O p)
              f :
            ModP O p)
          p) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          k) =
    ModP.preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k +
          1)
succ₄ :
  ModP.preVal K v O p
        (HPow.hPow (α := ModP O p)
          ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x :
            HasQuotient.Quotient O (B := Ideal O) (Ideal.span {(↑p : O)}))
          p) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          k) =
    ModP.preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k +
          1)
succ₅ :
  ModP.preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → ModP O p) (x ^ p)) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          k) =
    ModP.preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → O ⧸ Ideal.span {(↑p : O)}) x) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k +
          1)
succ₆ :
  ModP.preVal K v O p ((Ideal.Quotient.mk (Ideal.span {(↑p : O)}) : (a : O) → ModP O p) (x ^ p)) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          k) =
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0)
      (p ^
        (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k +
          1))
succ₇ :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) (x ^ p)) : ℝ≥0)
      (p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          k)) =
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0)
      (p ^
        (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k +
          1))
succ₈ :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) (HPow.hPow (α := K) ((algebraMap O K : (a : O) → K) x : K) p) : ℝ≥0)
      (p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          k)) =
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0)
      (p ^
        (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k +
          1))
succ₉ :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0) p ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          k) =
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0)
      (p ^
        (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k +
          1))
succ₁₀ :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0)
      (p *
        p ^
          (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k)) =
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0)
      (p ^
        (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k +
          1))
succ₁₁ succ₁₂ :
  HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0)
      (p *
        p ^
          (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k)) =
    HPow.hPow (α := ℝ≥0) ((v : (a : K) → ℝ≥0) ((algebraMap O K : (a : O) → K) x) : ℝ≥0)
      (p *
        p ^
          (Nat.find (p := fun (n : ℕ) ↦
              Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
            k))
⊢ ModP.preVal K v O p
        ((coeff
              (Nat.find (p := fun (n : ℕ) ↦
                Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h) :
            (a : PreTilt O p) → ModP O p)
          f) ^
      p ^
        Nat.find (p := fun (n : ℕ) ↦
          Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h =
    ModP.preVal K v O p
        ((coeff
              (Nat.find (p := fun (n : ℕ) ↦
                  Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
                (k + 1)) :
            (a : PreTilt O p) → ModP O p)
          f) ^
      p ^
        (Nat.find (p := fun (n : ℕ) ↦
            Ne (α := ModP O p) ((coeff n : (a : PreTilt O p) → ModP O p) f : ModP O p) (0 : ModP O p)) h +
          (k + 1))

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

Premises used: PreTilt.coeff_pow_p, add_assoc, map_pow, ModP.preVal_mk, pow_mul, Valuation.map_pow, PreTilt.coeff_nat_find_add_ne_zero, pow_succ'