-- Lean 4 proof step from Mathlib.RingTheory.Perfection (goal)
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)
⊢ 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))
have succ : ∀ (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)),
  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: obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective (coeff (Nat.find h + k + 1) f)