-- 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 : ℕ
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)
succ :
  ∀ (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)),
    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))
⊢ 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)

Tactic:
induction k with
  | zero => rfl
  | succ k ih => ?_