-- Lean 4 proof step from Mathlib.NumberTheory.Padics.Hensel (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
R : Type u_1
inst_1 : CommSemiring R
inst_2 : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm :
  norm (E := ℤ_[p]) (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F : ℤ_[p]) <
    HPow.hPow (β := ℕ)
      (norm (E := ℤ_[p])
        (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]))
      2
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen.{u_1} (R := R) (F := F) (a := a) n z
h1 :
  ‖HDiv.hDiv (α := ℚ_[p]) (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
          ℚ_[p])‖ ≤
    1
hzeq :
  z1 =
    Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
      (HDiv.hDiv (α := ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
        (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
          ℚ_[p]))
      h1
hdzne :
  Ne (α := ℤ_[p])
    (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
      ℤ_[p])
    (0 : ℤ_[p])
hdzne' :
  Ne (α := ℚ_[p])
    (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
      ℚ_[p])
    0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) (Polynomial.map (algebraMap R ℤ_[p]) F) =
    Polynomial.eval z (Polynomial.map (algebraMap R ℤ_[p]) F) +
        Polynomial.eval z
            ((Polynomial.derivative : (a : Polynomial ℤ_[p]) → Polynomial ℤ_[p])
              (Polynomial.map (algebraMap R ℤ_[p]) F)) *
          -z1 +
      q * HPow.hPow (β := ℕ) (-z1) 2
this :
  ‖(↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
          ℚ_[p]) *
        HDiv.hDiv (α := ℚ_[p])
          (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
          (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
            ℚ_[p])‖ ≤
    1
⊢ HMul.hMul (α := ℤ_[p])
      (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
      (-z1) =
    -((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F
have z₁ : HMul.hMul (α := ℤ_[p])
    (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
      ℤ_[p])
    (-z1) =
  HMul.hMul (α := ℤ_[p]) (β := ℤ_[p])
    (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
        ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
      ℤ_[p])
    (-Subtype.mk (p := fun (x : ℚ_[p]) ↦ ‖x‖ ≤ 1)
        (HDiv.hDiv (α := ℚ_[p])
          (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p]) F) : ℚ_[p])
          (↑(((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
                ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F)) :
            ℚ_[p]))
        h1)
Tactic: calc
      F.derivative.aeval z * -z1 =
          F.derivative.aeval z * -⟨↑(F.aeval z) / ↑(F.derivative.aeval z), h1⟩ := by rw [hzeq]
      _ = -(F.derivative.aeval z * ⟨↑(F.aeval z) / ↑(F.derivative.aeval z), h1⟩) := mul_neg _ _
      _ = -⟨F.derivative.aeval z * (F.aeval z / (F.derivative.aeval z : ℤ_[p]) : ℚ_[p]), this⟩ :=
        (Subtype.ext <| by simp only [PadicInt.coe_neg, PadicInt.coe_mul])
      _ = -F.aeval z := by simp only [mul_div_cancel₀ _ hdzne', Subtype.coe_eta]