mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 4 ≠ 0
⊢ 4 = 4

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈).natDegree ≤ 4

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈).natDegree ≤ 4
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈).coeff 4 = 3

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈).coeff 4 = 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 3 ≠ 0
⊢ 3 ≠ 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 3 ≠ 0
⊢ 3 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 3 ≠ 0
⊢ 3 = 3

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 +
          C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X +
        C (W.b₄ * W.b₈ - W.b₆ ^ 2)).natDegree ≤
    6

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 +
          C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X +
        C (W.b₄ * W.b₈ - W.b₆ ^ 2)).natDegree ≤
    6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 +
            C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X +
          C (W.b₄ * W.b₈ - W.b₆ ^ 2)).coeff
      6 =
    2

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (2 * X ^ 6 + C W.b₂ * X ^ 5 + 5 * C W.b₄ * X ^ 4 + 10 * C W.b₆ * X ^ 3 + 10 * C W.b₈ * X ^ 2 +
            C (W.b₂ * W.b₈ - W.b₄ * W.b₆) * X +
          C (W.b₄ * W.b₈ - W.b₆ ^ 2)).coeff
      6 =
    2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 2 ≠ 0
⊢ 2 ≠ 0

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 2 ≠ 0
⊢ 2 ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
h : 2 ≠ 0
⊢ 2 = 2

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (2 * ↑(expDegree (m + 2))) + 2 * ↑(expDegree (m + 3)) + 2 * ↑(expDegree (m + 5)) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + 2 * ↑(expDegree (m + 3)) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (2 * ↑(expDegree (m + 2))) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (2 * ↑(expDegree (m + 3))) + 2 * if Even m then 0 else 6

Tactic:
]

Goal state after:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (2 * ↑(expDegree (m + 2))) + 2 * ↑(expDegree (m + 3)) + 2 * ↑(expDegree (m + 5)) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + 2 * ↑(expDegree (m + 3)) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (2 * ↑(expDegree (m + 2))) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (2 * ↑(expDegree (m + 3))) + 2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 + 4 * W.a₂ = 4 * W.a₂

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 + 4 * W.a₂ = 4 * W.a₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 2 * W.a₄ + W.a₁ * 0 = 2 * W.a₄

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 2 * W.a₄ + W.a₁ * 0 = 2 * W.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 + 4 * W.a₆ = 4 * W.a₆

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 + 4 * W.a₆ = 4 * W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).Ψ n = (mapRingHom (mapRingHom f)) (W.Ψ n)

Tactic:
]

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).Ψ n = (mapRingHom (mapRingHom f)) (W.Ψ n)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * ↑(expDegree (m + 3)) + 2 * ↑(expDegree (m + 5)) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + 2 * ↑(expDegree (m + 3)) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (2 * ↑(expDegree (m + 3))) + 2 * if Even m then 0 else 6

Tactic:
]

Goal state after:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * ↑(expDegree (m + 3)) + 2 * ↑(expDegree (m + 5)) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + 2 * ↑(expDegree (m + 3)) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (2 * ↑(expDegree (m + 3))) + 2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - 0 * 0 * W.a₄ + W.a₂ * 0 ^ 2 - W.a₄ ^ 2 = 4 * W.a₂ * W.a₆ - W.a₄ ^ 2

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - 0 * 0 * W.a₄ + W.a₂ * 0 ^ 2 - W.a₄ ^ 2 = 4 * W.a₂ * W.a₆ - W.a₄ ^ 2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).Φ n = (mapRingHom f) (W.Φ n)

Tactic:
]

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).Φ n = (mapRingHom f) (W.Φ n)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).ψ n = (mapRingHom (mapRingHom f)) (W.ψ n)

Tactic:
]

Goal state after:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W : WeierstrassCurve R
f : R →+* S
n : ℤ
⊢ (W.map f).ψ n = (mapRingHom (mapRingHom f)) (W.ψ n)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ (4 * W.a₂) ^ 2 - 24 * (2 * W.a₄) = 16 * W.a₂ ^ 2 - 48 * W.a₄

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ (4 * W.a₂) ^ 2 - 24 * (2 * W.a₄) = 16 * W.a₂ ^ 2 - 48 * W.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W⁄B).ψ₂ = (W⁄B).ψ₂

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W⁄B).Ψ₂Sq = (W⁄B).Ψ₂Sq

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
j : ↥s
⊢ c.π.app i ⁻¹ᵁ 𝒱 j ≤ ((Functor.const I).map (a ≫ f)).app i ⁻¹ᵁ ↑(↑(↑↑j).2).2

Tactic:
]

Goal state after:
I : Type u
inst✝⁵ : Category.{u, u} I
S X : Scheme
D : I ⥤ Scheme
t : D ⟶ (Functor.const I).obj S
f : X ⟶ S
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : LocallyOfFinitePresentation f
inst✝² : ∀ {i j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝¹ : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
a : c.pt ⟶ X
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
𝒰 : IsOpenCover fun V ↦ (↑V).1
i : I
s : Finset { x // x.1 ∈ c.pt.affineOpens ∧ x.1 ≤ (Opens.comap (TopCat.Hom.hom a.base)) (↑x.2).1 }
𝒱 : ↥s → (D.obj i).Opens
h𝒱 : IsOpenCover 𝒱
h𝒱𝒰 : ∀ (j : ↥s), IsAffineOpen (𝒱 j) ∧ (↑↑j).1 = c.π.app i ⁻¹ᵁ 𝒱 j
j : ↥s
⊢ c.π.app i ⁻¹ᵁ 𝒱 j ≤ ((Functor.const I).map (a ≫ f)).app i ⁻¹ᵁ ↑(↑(↑↑j).2).2
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W⁄B).Ψ₃ = (W⁄B).Ψ₃

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ -(4 * W.a₂) ^ 3 + 36 * (4 * W.a₂) * (2 * W.a₄) - 216 * (4 * W.a₆) = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ -(4 * W.a₂) ^ 3 + 36 * (4 * W.a₂) * (2 * W.a₄) - 216 * (4 * W.a₆) = -64 * W.a₂ ^ 3 + 288 * W.a₂ * W.a₄ - 864 * W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * ↑(expDegree (m + 5)) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * if Even m then 0 else 6

Tactic:
]

Goal state after:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          2 * ↑(expDegree (m + 5)) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
⊢ (W⁄B).preΨ₄ = (W⁄B).preΨ₄

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ -(4 * W.a₂) ^ 2 * (4 * W.a₂ * W.a₆ - W.a₄ ^ 2) - 8 * (2 * W.a₄) ^ 3 - 27 * (4 * W.a₆) ^ 2 +
      9 * (4 * W.a₂) * (2 * W.a₄) * (4 * W.a₆) =
    -64 * W.a₂ ^ 3 * W.a₆ + 16 * W.a₂ ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * W.a₂ * W.a₄ * W.a₆

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ -(4 * W.a₂) ^ 2 * (4 * W.a₂ * W.a₆ - W.a₄ ^ 2) - 8 * (2 * W.a₄) ^ 3 - 27 * (4 * W.a₆) ^ 2 +
      9 * (4 * W.a₂) * (2 * W.a₄) * (4 * W.a₆) =
    -64 * W.a₂ ^ 3 * W.a₆ + 16 * W.a₂ ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * W.a₂ * W.a₄ * W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℕ
⊢ (W⁄B).preΨ' n = (W⁄B).preΨ' n

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W⁄B).preΨ n = (W⁄B).preΨ n

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ -64 * 0 ^ 3 * W.a₆ + 16 * 0 ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * 0 * W.a₄ * W.a₆ =
    -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ -64 * 0 ^ 3 * W.a₆ + 16 * 0 ^ 2 * W.a₄ ^ 2 - 64 * W.a₄ ^ 3 - 432 * W.a₆ ^ 2 + 288 * 0 * W.a₄ * W.a₆ =
    -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W⁄B).ΨSq n = (W⁄B).ΨSq n

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ 2 * W.a₄ = -W.a₄

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ 2 * W.a₄ = -W.a₄
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ 4 * W.a₆ = W.a₆

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ 4 * W.a₆ = W.a₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ W.b₆ = W.a₆

Tactic:
rw [b₆_of_isShortNF]
  linear_combination W.a₆ * CharP.cast_eq_zero R 3

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -48 * W.a₄ = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -48 * W.a₄ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -864 * W.a₆ = 0

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -864 * W.a₆ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * if Even m then 0 else 6

Tactic:
]

Goal state after:
m : ℕ
⊢ ((↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) +
          (↑(m + 5) ^ 2 - if Even (m + 5) then 4 else 1) ∧
      (↑(2 * m + 6) ^ 2 - if Even (2 * m + 6) then 4 else 1) =
        2 * ↑(expDegree (m + 1)) + (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * (2 * ↑(expDegree (m + 4)))) ∧
    (2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 4)) + 3 * (↑(m + 2) ^ 2 - if Even (m + 2) then 4 else 1) + 2 * if Even m then 6 else 0) ∧
      2 * ↑(expDegree (2 * m + 4 + 1)) =
        2 * ↑(expDegree (m + 1)) + 3 * (↑(m + 3) ^ 2 - if Even (m + 3) then 4 else 1) + 2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) = -W.a₄ ^ 3

Tactic:
]

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) = -W.a₄ ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ W.Δ = -W.a₄ ^ 3

Tactic:
rw [Δ_of_isShortNF]

Goal state after:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) = -W.a₄ ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W⁄B).Ψ n = (W⁄B).Ψ n

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsShortNF
h : -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) ≠ 0
⊢ W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)

Tactic:
]

Goal state after:
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve F
inst✝¹ : W.IsElliptic
inst✝ : W.IsShortNF
h : -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) ≠ 0
⊢ W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
S : Type s
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
W : WeierstrassCurve R
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
n : ℤ
⊢ (W⁄B).Φ n = (W⁄B).Φ n

Tactic:
]

Goal state after: