-- Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
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))
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))
simp_rw₆ :
  preNormEDS (HPow.hPow (α := CoordinateRing W) (β := ℕ) ((mk W : (a : R[X][Y]) → CoordinateRing W) 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 *
      (mk W : (a : R[X][Y]) → CoordinateRing W) (if Even n then W.ψ₂ else 1) =
    preNormEDS
        (HPow.hPow (α := CoordinateRing W) (β := ℕ)
          ((mk W : (a : R[X][Y]) → CoordinateRing W) ((C : (a : R[X]) → R[X][Y]) W.Ψ₂Sq) : CoordinateRing W) 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 *
      (mk W : (a : R[X][Y]) → CoordinateRing W) (if Even n then W.ψ₂ else 1)
simp_rw₇ :
  preNormEDS (HPow.hPow (α := CoordinateRing W) (β := ℕ) ((mk W : (a : R[X][Y]) → CoordinateRing W) 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 *
      (mk W : (a : R[X][Y]) → CoordinateRing W) (if Even n then W.ψ₂ else 1) =
    preNormEDS
        (HPow.hPow (β := ℕ)
          (HPow.hPow (α := CoordinateRing W) (β := ℕ) ((mk W : (a : R[X][Y]) → CoordinateRing W) W.ψ₂) 2) 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 *
      (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))

Tactic:
simp_rw [ψ, normEDS, Ψ, preΨ, map_mul, map_preNormEDS, map_pow, ← mk_ψ₂_sq, ← pow_mul]

Premises used: WeierstrassCurve.ψ, map_preNormEDS, WeierstrassCurve.Ψ, map_pow, normEDS, pow_mul, map_mul, WeierstrassCurve.Affine.CoordinateRing.mk_ψ₂_sq, WeierstrassCurve.preΨ