-- 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
n : ℕ
z : ℤ_[p]
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
z1 : ℤ_[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
z' : ℤ_[p] := z - z1
hdist :
  ‖HAdd.hAdd (α := ℤ_[p]) (β := ℤ_[p])
        (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])
        (-((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
              ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])‖ <
    norm (E := ℤ_[p])
      (-((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
this :
  norm (E := ℤ_[p])
      (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p]) =
    norm (E := ℤ_[p])
      (-((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
⊢ norm (E := ℤ_[p])
      (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p]) =
    norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
have rwa : ∀
  (this :
    norm (E := ℤ_[p])
        (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p]) =
      norm (E := ℤ_[p])
        (((Polynomial.aeval z : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
            ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
          ℤ_[p])),
  norm (E := ℤ_[p])
      (((Polynomial.aeval z' : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p]) =
    norm (E := ℤ_[p])
      (((Polynomial.aeval a : Polynomial R →ₐ[R] ℤ_[p]) : (a : Polynomial R) → ℤ_[p])
          ((Polynomial.derivative : (a : Polynomial R) → Polynomial R) F) :
        ℤ_[p])
Tactic: rwa [norm_neg, hz.1] at this
Cleared hypotheses: this