-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
simp_rw :
  Eq (α := CoordinateRing W)
    ((mk W : (a : R[X][Y]) → CoordinateRing W)
      (normEDS W.ψ₂ ((C : (a : R[X]) → R[X][Y]) W.Ψ₃) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄) n))
    ((mk W : (a : R[X][Y]) → CoordinateRing W) (W.Ψ n))
simp_rw₁ :
  Eq (α := CoordinateRing W)
    ((mk W : (a : R[X][Y]) → CoordinateRing W)
        (preNormEDS (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 4) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃)
            ((C : (a : R[X]) → R[X][Y]) W.preΨ₄) n *
          if Even n then W.ψ₂ else 1) :
      CoordinateRing W)
    ((mk W : (a : R[X][Y]) → CoordinateRing W) (W.Ψ n) : CoordinateRing W)
simp_rw₂ :
  Eq (α := CoordinateRing W)
    ((mk W : (a : R[X][Y]) → CoordinateRing W)
        (preNormEDS (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 4) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃)
            ((C : (a : R[X]) → R[X][Y]) W.preΨ₄) n *
          if Even n then W.ψ₂ else 1) :
      CoordinateRing W)
    ((mk W : (a : R[X][Y]) → CoordinateRing W)
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) (W.preΨ n) : R[X][Y])
          (if Even n then W.ψ₂ else 1)) :
      CoordinateRing W)
simp_rw₃ :
  Eq (α := CoordinateRing W)
    ((mk W : (a : R[X][Y]) → CoordinateRing W)
        (preNormEDS (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 4) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃)
            ((C : (a : R[X]) → R[X][Y]) W.preΨ₄) n *
          if Even n then W.ψ₂ else 1) :
      CoordinateRing W)
    ((mk W : (a : R[X][Y]) → CoordinateRing W)
        (HMul.hMul (α := R[X][Y]) (β := R[X][Y])
          ((C : (a : R[X]) → R[X][Y]) (preNormEDS (HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2) W.Ψ₃ W.preΨ₄ n) : R[X][Y])
          (if Even n then W.ψ₂ else 1)) :
      CoordinateRing W)
simp_rw₄ :
  HMul.hMul (α := CoordinateRing W) (β := CoordinateRing W)
      ((mk W : (a : R[X][Y]) → CoordinateRing W)
          (preNormEDS (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 4) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃)
            ((C : (a : R[X]) → R[X][Y]) W.preΨ₄) n) :
        CoordinateRing W)
      ((mk W : (a : R[X][Y]) → CoordinateRing W) (if Even n then W.ψ₂ else 1) : CoordinateRing W) =
    HMul.hMul (α := CoordinateRing W) (β := CoordinateRing W)
      ((mk W : (a : R[X][Y]) → CoordinateRing W)
          ((C : (a : R[X]) → R[X][Y]) (preNormEDS (HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2) W.Ψ₃ W.preΨ₄ n)) :
        CoordinateRing W)
      ((mk W : (a : R[X][Y]) → CoordinateRing W) (if Even n then W.ψ₂ else 1))
⊢ Eq (α := CoordinateRing W) ((mk W : (a : R[X][Y]) → CoordinateRing W) (W.ψ n))
    ((mk W : (a : R[X][Y]) → CoordinateRing W) (W.Ψ n))
have simp_rw₅ : HMul.hMul (α := CoordinateRing W) (β := CoordinateRing W)
    (preNormEDS ((mk W : (a : R[X][Y]) → CoordinateRing W) (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 4))
        ((mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃))
        ((mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄)) n :
      CoordinateRing W)
    ((mk W : (a : R[X][Y]) → CoordinateRing W) (if Even n then W.ψ₂ else 1) : CoordinateRing W) =
  HMul.hMul (α := CoordinateRing W) (β := CoordinateRing W)
    (preNormEDS
        ((mk W : (a : R[X][Y]) → CoordinateRing W)
          ((C : (a : R[X]) → R[X][Y]) (HPow.hPow (α := R[X]) (β := ℕ) W.Ψ₂Sq 2)))
        ((mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃))
        ((mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄)) n :
      CoordinateRing W)
    ((mk W : (a : R[X][Y]) → CoordinateRing W) (if Even n then W.ψ₂ else 1))
Tactic: simp_rw [ψ, normEDS, Ψ, preΨ, map_mul, map_preNormEDS, map_pow, ← mk_ψ₂_sq, ← pow_mul]