awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ 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 : 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))
Tactic: simp_rw [ψ, normEDS, Ψ, preΨ, map_mul, map_preNormEDS, map_pow, ← mk_ψ₂_sq, ← pow_mul]
-- 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))
⊢ 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₁ : 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)
Tactic: simp_rw [ψ, normEDS, Ψ, preΨ, map_mul, map_preNormEDS, map_pow, ← mk_ψ₂_sq, ← pow_mul]
-- 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)
⊢ 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₂ : 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)
Tactic: simp_rw [ψ, normEDS, Ψ, preΨ, map_mul, map_preNormEDS, map_pow, ← mk_ψ₂_sq, ← pow_mul]
-- 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)
⊢ 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₃ : 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)
Tactic: simp_rw [ψ, normEDS, Ψ, preΨ, map_mul, map_preNormEDS, map_pow, ← mk_ψ₂_sq, ← pow_mul]
-- 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)
⊢ 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)
    ((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))
Tactic: simp_rw [ψ, normEDS, Ψ, preΨ, map_mul, map_preNormEDS, map_pow, ← mk_ψ₂_sq, ← pow_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
⊢ W.φ 4 =
    HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y]) 2) *
          HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2 -
        HMul.hMul (β := R[X][Y])
          (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y])
            (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 4))
          ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) +
      HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) 4
have rw : HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
      (HPow.hPow (β := ℕ) (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y]) W.ψ₂)
        2) -
    HMul.hMul (β := R[X][Y])
      (HMul.hMul (α := R[X][Y]) (β := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y]) W.ψ₂ *
          HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 3 -
        1 * HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) 3)
      ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) =
  HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y]) 2) *
        HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 2 -
      HMul.hMul (β := R[X][Y])
        (HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) W.preΨ₄ : R[X][Y])
          (HPow.hPow (α := R[X][Y]) (β := ℕ) W.ψ₂ 4))
        ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) +
    HPow.hPow (α := R[X][Y]) (β := ℕ) ((C : (a : R[X]) → R[X][Y]) W.Ψ₃ : R[X][Y]) 4
Tactic: rw [φ, ψ_four, show (4 + 1 : ℤ) = 2 * 2 + 1 by rfl, ψ_odd, two_add_two_eq_four, ψ_four,
    show (2 - 1 : ℤ) = 1 by rfl, ψ_two, ψ_one, two_add_one_eq_three, show (4 - 1 : ℤ) = 3 by rfl,
    ψ_three]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
inst : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ Eq (α := R[X][Y]) (W.φ (-n)) (W.φ n)
have simp_rw : HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) (HPow.hPow (α := R[X][Y]) (β := ℕ) (-W.ψ n) 2) -
    HMul.hMul (α := R[X][Y]) (W.ψ (-n + 1)) (W.ψ (-n - 1)) =
  HMul.hMul (α := R[X][Y]) ((C : (a : R[X]) → R[X][Y]) X : R[X][Y]) (HPow.hPow (α := R[X][Y]) (β := ℕ) (W.ψ n) 2) -
    HMul.hMul (α := R[X][Y]) (W.ψ (n + 1)) (W.ψ (n - 1))
Tactic: simp_rw [φ, ψ_neg, neg_sq, ← sub_neg_eq_add, ← neg_sub', sub_neg_eq_add, ← neg_add', ψ_neg,
    neg_mul_neg, mul_comm <| W.ψ <| n - 1]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ Eq (α := B[X][Y]) (W⁄B).ψ₂ (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W⁄A).ψ₂)
have rw : Eq (α := B[X][Y]) (W⁄B).ψ₂ ((W⁄A).map (↑f : A →+* B)).ψ₂
Tactic: rw [← map_ψ₂, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := B[X][Y]) (W⁄B).ψ₂ ((W⁄A).map (↑f : A →+* B)).ψ₂
⊢ Eq (α := B[X][Y]) (W⁄B).ψ₂ (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) (W⁄A).ψ₂)
have rw₁ : Eq (α := B[X][Y]) (W⁄B).ψ₂ (W⁄B).ψ₂
Tactic: rw [← map_ψ₂, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ Eq (α := B[X]) (W⁄B).Ψ₂Sq (Polynomial.map (↑f : A →+* B) (W⁄A).Ψ₂Sq)
have rw : Eq (α := B[X]) (W⁄B).Ψ₂Sq ((W⁄A).map (↑f : A →+* B)).Ψ₂Sq
Tactic: rw [← map_Ψ₂Sq, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := B[X]) (W⁄B).Ψ₂Sq ((W⁄A).map (↑f : A →+* B)).Ψ₂Sq
⊢ Eq (α := B[X]) (W⁄B).Ψ₂Sq (Polynomial.map (↑f : A →+* B) (W⁄A).Ψ₂Sq)
have rw₁ : Eq (α := B[X]) (W⁄B).Ψ₂Sq (W⁄B).Ψ₂Sq
Tactic: rw [← map_Ψ₂Sq, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ Eq (α := B[X]) (W⁄B).Ψ₃ (Polynomial.map (↑f : A →+* B) (W⁄A).Ψ₃)
have rw : Eq (α := B[X]) (W⁄B).Ψ₃ ((W⁄A).map (↑f : A →+* B)).Ψ₃
Tactic: rw [← map_Ψ₃, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := B[X]) (W⁄B).Ψ₃ ((W⁄A).map (↑f : A →+* B)).Ψ₃
⊢ Eq (α := B[X]) (W⁄B).Ψ₃ (Polynomial.map (↑f : A →+* B) (W⁄A).Ψ₃)
have rw₁ : Eq (α := B[X]) (W⁄B).Ψ₃ (W⁄B).Ψ₃
Tactic: rw [← map_Ψ₃, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
⊢ Eq (α := B[X]) (W⁄B).preΨ₄ (Polynomial.map (↑f : A →+* B) (W⁄A).preΨ₄)
have rw : Eq (α := B[X]) (W⁄B).preΨ₄ ((W⁄A).map (↑f : A →+* B)).preΨ₄
Tactic: rw [← map_preΨ₄, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
rw : Eq (α := B[X]) (W⁄B).preΨ₄ ((W⁄A).map (↑f : A →+* B)).preΨ₄
⊢ Eq (α := B[X]) (W⁄B).preΨ₄ (Polynomial.map (↑f : A →+* B) (W⁄A).preΨ₄)
have rw₁ : Eq (α := B[X]) (W⁄B).preΨ₄ (W⁄B).preΨ₄
Tactic: rw [← map_preΨ₄, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℕ
⊢ Eq (α := B[X]) ((W⁄B).preΨ' n) (Polynomial.map (↑f : A →+* B) ((W⁄A).preΨ' n))
have rw : Eq (α := B[X]) ((W⁄B).preΨ' n) (((W⁄A).map (↑f : A →+* B)).preΨ' n)
Tactic: rw [← map_preΨ', map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℕ
rw : Eq (α := B[X]) ((W⁄B).preΨ' n) (((W⁄A).map (↑f : A →+* B)).preΨ' n)
⊢ Eq (α := B[X]) ((W⁄B).preΨ' n) (Polynomial.map (↑f : A →+* B) ((W⁄A).preΨ' n))
have rw₁ : Eq (α := B[X]) ((W⁄B).preΨ' n) ((W⁄B).preΨ' n)
Tactic: rw [← map_preΨ', map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ Eq (α := B[X]) ((W⁄B).preΨ n) (Polynomial.map (↑f : A →+* B) ((W⁄A).preΨ n))
have rw : Eq (α := B[X]) ((W⁄B).preΨ n) (((W⁄A).map (↑f : A →+* B)).preΨ n)
Tactic: rw [← map_preΨ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
rw : Eq (α := B[X]) ((W⁄B).preΨ n) (((W⁄A).map (↑f : A →+* B)).preΨ n)
⊢ Eq (α := B[X]) ((W⁄B).preΨ n) (Polynomial.map (↑f : A →+* B) ((W⁄A).preΨ n))
have rw₁ : Eq (α := B[X]) ((W⁄B).preΨ n) ((W⁄B).preΨ n)
Tactic: rw [← map_preΨ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ Eq (α := B[X]) ((W⁄B).ΨSq n) (Polynomial.map (↑f : A →+* B) ((W⁄A).ΨSq n))
have rw : Eq (α := B[X]) ((W⁄B).ΨSq n) (((W⁄A).map (↑f : A →+* B)).ΨSq n)
Tactic: rw [← map_ΨSq, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
rw : Eq (α := B[X]) ((W⁄B).ΨSq n) (((W⁄A).map (↑f : A →+* B)).ΨSq n)
⊢ Eq (α := B[X]) ((W⁄B).ΨSq n) (Polynomial.map (↑f : A →+* B) ((W⁄A).ΨSq n))
have rw₁ : Eq (α := B[X]) ((W⁄B).ΨSq n) ((W⁄B).ΨSq n)
Tactic: rw [← map_ΨSq, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ Eq (α := B[X][Y]) ((W⁄B).Ψ n) (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) ((W⁄A).Ψ n))
have rw : Eq (α := B[X][Y]) ((W⁄B).Ψ n) (((W⁄A).map (↑f : A →+* B)).Ψ n)
Tactic: rw [← map_Ψ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
rw : Eq (α := B[X][Y]) ((W⁄B).Ψ n) (((W⁄A).map (↑f : A →+* B)).Ψ n)
⊢ Eq (α := B[X][Y]) ((W⁄B).Ψ n) (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) ((W⁄A).Ψ n))
have rw₁ : Eq (α := B[X][Y]) ((W⁄B).Ψ n) ((W⁄B).Ψ n)
Tactic: rw [← map_Ψ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ Eq (α := B[X]) ((W⁄B).Φ n) (Polynomial.map (↑f : A →+* B) ((W⁄A).Φ n))
have rw : Eq (α := B[X]) ((W⁄B).Φ n) (((W⁄A).map (↑f : A →+* B)).Φ n)
Tactic: rw [← map_Φ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
rw : Eq (α := B[X]) ((W⁄B).Φ n) (((W⁄A).map (↑f : A →+* B)).Φ n)
⊢ Eq (α := B[X]) ((W⁄B).Φ n) (Polynomial.map (↑f : A →+* B) ((W⁄A).Φ n))
have rw₁ : Eq (α := B[X]) ((W⁄B).Φ n) ((W⁄B).Φ n)
Tactic: rw [← map_Φ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ Eq (α := B[X][Y]) ((W⁄B).ψ n) (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) ((W⁄A).ψ n))
have rw : Eq (α := B[X][Y]) ((W⁄B).ψ n) (((W⁄A).map (↑f : A →+* B)).ψ n)
Tactic: rw [← map_ψ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
rw : Eq (α := B[X][Y]) ((W⁄B).ψ n) (((W⁄A).map (↑f : A →+* B)).ψ n)
⊢ Eq (α := B[X][Y]) ((W⁄B).ψ n) (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) ((W⁄A).ψ n))
have rw₁ : Eq (α := B[X][Y]) ((W⁄B).ψ n) ((W⁄B).ψ n)
Tactic: rw [← map_ψ, map_baseChange]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic (goal)
Goal:
R : Type r
S : Type s
inst : CommRing R
inst_1 : CommRing S
W : WeierstrassCurve R
inst_2 : Algebra R S
A : Type u
inst_3 : CommRing A
inst_4 : Algebra R A
inst_5 : Algebra S A
inst_6 : IsScalarTower R S A
B : Type v
inst_7 : CommRing B
inst_8 : Algebra R B
inst_9 : Algebra S B
inst_10 : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ Eq (α := B[X][Y]) ((W⁄B).φ n) (Polynomial.map (R := A[X]) (mapRingHom (↑f : A →+* B)) ((W⁄A).φ n))
have rw : Eq (α := B[X][Y]) ((W⁄B).φ n) (((W⁄A).map (↑f : A →+* B)).φ n)
Tactic: rw [← map_φ, map_baseChange]