-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
simp_rw :
  HPow.hPow (α := 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)
      2 =
    (mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) (W.ΨSq n))
simp_rw₁ :
  HPow.hPow (α := 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)
      2 =
    (mk W : (a : R[X][Y]) → CoordinateRing W)
      ((C : (a : R[X]) → R[X][Y]) (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ n) 2 * if Even n then W.Ψ₂Sq else 1))
simp_rw₂ :
  HPow.hPow (β := ℕ)
      (HMul.hMul (α := CoordinateRing W) (β := CoordinateRing 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)))
      2 =
    HMul.hMul (α := CoordinateRing W) (β := CoordinateRing W)
      ((mk W : (a : R[X][Y]) → CoordinateRing W)
          ((C : (a : R[X]) → R[X][Y]) (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ n) 2)) :
        CoordinateRing W)
      ((mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) (if Even n then W.Ψ₂Sq else 1)) :
        CoordinateRing W)
simp_rw₃ :
  HPow.hPow (β := ℕ)
      (HMul.hMul (α := CoordinateRing W) (β := CoordinateRing 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)))
      2 =
    HMul.hMul (α := CoordinateRing W) (β := CoordinateRing W)
      ((mk W : (a : R[X][Y]) → CoordinateRing W)
          ((C : (a : R[X]) → R[X][Y]) (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ n) 2)) :
        CoordinateRing W)
      ((mk W : (a : R[X][Y]) → CoordinateRing W)
          (if Even n then (C : (a : R[X]) → R[X][Y]) W.Ψ₂Sq else (C : (a : R[X]) → R[X][Y]) 1) :
        CoordinateRing W)
⊢ HPow.hPow (α := CoordinateRing W) (β := ℕ) ((mk W : (a : R[X][Y]) → CoordinateRing W) (W.Ψ n)) 2 =
    (mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) (W.ΨSq n))
have simp_rw₄ : HPow.hPow (β := ℕ)
    (HMul.hMul (α := CoordinateRing W) (β := CoordinateRing W)
      ((mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) (W.preΨ n)) : CoordinateRing W)
      (if Even n then (mk W : (a : R[X][Y]) → CoordinateRing W) W.ψ₂ else (mk W : (a : R[X][Y]) → CoordinateRing W) 1))
    2 =
  HMul.hMul (α := CoordinateRing W) (β := CoordinateRing W)
    ((mk W : (a : R[X][Y]) → CoordinateRing W)
        ((C : (a : R[X]) → R[X][Y]) (HPow.hPow (α := R[X]) (β := ℕ) (W.preΨ n) 2)) :
      CoordinateRing W)
    (if Even n then (mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) W.Ψ₂Sq)
      else (mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) 1) :
      CoordinateRing W)
Tactic: simp_rw [Ψ, ΨSq, map_mul, apply_ite C, apply_ite <| mk W, mul_pow, ite_pow, mk_ψ₂_sq, map_one,
    one_pow, map_pow]