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

Goal state before:
pp: case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * (W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial) ^ 2 -
        C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * 1) *
      1 =
    C (W.preΨ (m + 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) ^ 3 - C (W.preΨ (m - 1)) * 1 * (C (W.preΨ (m + 1)) * 1) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3)

pp: case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * 1 -
        C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * (W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial) ^ 2) *
      1 =
    C (W.preΨ (m + 2)) * 1 * (C (W.preΨ m) * 1) ^ 3 - C (W.preΨ (m - 1)) * W.ψ₂ * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
        (-C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3)

Tactic:
<;>

Goal state after:
case pos
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * (W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial) ^ 2 -
        C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * 1) *
      1 =
    C (W.preΨ (m + 2)) * W.ψ₂ * (C (W.preΨ m) * W.ψ₂) ^ 3 - C (W.preΨ (m - 1)) * 1 * (C (W.preΨ (m + 1)) * 1) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) * (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3)

case neg
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
h✝ : ¬Even m
⊢ (C (W.preΨ (m + 2)) * C (W.preΨ m) ^ 3 * 1 -
        C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3 * (W.ψ₂ ^ 2 - 4 * W.toAffine.polynomial) ^ 2) *
      1 =
    C (W.preΨ (m + 2)) * 1 * (C (W.preΨ m) * 1) ^ 3 - C (W.preΨ (m - 1)) * W.ψ₂ * (C (W.preΨ (m + 1)) * W.ψ₂) ^ 3 +
      W.toAffine.polynomial * (16 * W.toAffine.polynomial - 8 * W.ψ₂ ^ 2) *
        (-C (W.preΨ (m - 1)) * C (W.preΨ (m + 1)) ^ 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
⊢ 0 + zero = zero

pp: case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x✝ y✝ : F
h✝ : W.Nonsingular x✝ y✝
⊢ 0 + some x✝ y✝ h✝ = some x✝ y✝ h✝

Tactic:
<;>

Goal state after:
case zero
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
⊢ 0 + zero = zero

case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x✝ y✝ : F
h✝ : W.Nonsingular x✝ y✝
⊢ 0 + some x✝ y✝ h✝ = some x✝ y✝ h✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
⊢ zero + 0 = zero

pp: case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x✝ y✝ : F
h✝ : W.Nonsingular x✝ y✝
⊢ some x✝ y✝ h✝ + 0 = some x✝ y✝ h✝

Tactic:
<;>

Goal state after:
case zero
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
⊢ zero + 0 = zero

case some
R : Type r
S : Type s
A F : Type u
B K : Type v
L : Type w
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
W' : Affine R
W : Affine F
inst✝² : DecidableEq F
inst✝¹ : DecidableEq K
inst✝ : DecidableEq L
x✝ y✝ : F
h✝ : W.Nonsingular x✝ y✝
⊢ some x✝ y✝ h✝ + 0 = some x✝ y✝ h✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero
R : Type r
F : Type u
inst✝³ : CommRing R
inst✝² : Field F
W' : Affine R
inst✝¹ : DecidableEq F
inst✝ : Algebra R F
⊢ (map (Algebra.ofId F F)) zero = zero

pp: case some
R : Type r
F : Type u
inst✝³ : CommRing R
inst✝² : Field F
W' : Affine R
inst✝¹ : DecidableEq F
inst✝ : Algebra R F
x✝ y✝ : F
h✝ : (W'⁄F).Nonsingular x✝ y✝
⊢ (map (Algebra.ofId F F)) (some x✝ y✝ h✝) = some x✝ y✝ h✝

Tactic:
<;>

Goal state after:
case zero
R : Type r
F : Type u
inst✝³ : CommRing R
inst✝² : Field F
W' : Affine R
inst✝¹ : DecidableEq F
inst✝ : Algebra R F
⊢ (map (Algebra.ofId F F)) zero = zero

case some
R : Type r
F : Type u
inst✝³ : CommRing R
inst✝² : Field F
W' : Affine R
inst✝¹ : DecidableEq F
inst✝ : Algebra R F
x✝ y✝ : F
h✝ : (W'⁄F).Nonsingular x✝ y✝
⊢ (map (Algebra.ofId F F)) (some x✝ y✝ h✝) = some x✝ y✝ h✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero
R : Type r
S : Type s
F : Type u
K : Type v
L : Type w
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K
inst✝¹³ : Field L
W' : Affine R
inst✝¹² : DecidableEq F
inst✝¹¹ : DecidableEq K
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
⊢ (map g) ((map f) zero) = (map (g.comp f)) zero

pp: case some
R : Type r
S : Type s
F : Type u
K : Type v
L : Type w
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K
inst✝¹³ : Field L
W' : Affine R
inst✝¹² : DecidableEq F
inst✝¹¹ : DecidableEq K
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x✝ y✝ : F
h✝ : (W'⁄F).Nonsingular x✝ y✝
⊢ (map g) ((map f) (some x✝ y✝ h✝)) = (map (g.comp f)) (some x✝ y✝ h✝)

Tactic:
<;>

Goal state after:
case zero
R : Type r
S : Type s
F : Type u
K : Type v
L : Type w
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K
inst✝¹³ : Field L
W' : Affine R
inst✝¹² : DecidableEq F
inst✝¹¹ : DecidableEq K
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
⊢ (map g) ((map f) zero) = (map (g.comp f)) zero

case some
R : Type r
S : Type s
F : Type u
K : Type v
L : Type w
inst✝¹⁷ : CommRing R
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Field F
inst✝¹⁴ : Field K
inst✝¹³ : Field L
W' : Affine R
inst✝¹² : DecidableEq F
inst✝¹¹ : DecidableEq K
inst✝¹⁰ : DecidableEq L
inst✝⁹ : Algebra R S
inst✝⁸ : Algebra R F
inst✝⁷ : Algebra S F
inst✝⁶ : IsScalarTower R S F
inst✝⁵ : Algebra R K
inst✝⁴ : Algebra S K
inst✝³ : IsScalarTower R S K
inst✝² : Algebra R L
inst✝¹ : Algebra S L
inst✝ : IsScalarTower R S L
f : F →ₐ[S] K
g : K →ₐ[S] L
x✝ y✝ : F
h✝ : (W'⁄F).Nonsingular x✝ y✝
⊢ (map g) ((map f) (some x✝ y✝ h✝)) = (map (g.comp f)) (some x✝ y✝ h✝)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ zero.xRep ≠ 0

pp: case some
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).xRep ≠ 0

Tactic:
<;>

Goal state after:
case zero
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ zero.xRep ≠ 0

case some
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).xRep ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ (-zero).xRep = zero.xRep

pp: case some
R : Type r
inst✝ : CommRing R
W' : Affine R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (-some x✝ y✝ h✝).xRep = (some x✝ y✝ h✝).xRep

Tactic:
<;>

Goal state after:
case zero
R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ (-zero).xRep = zero.xRep

case some
R : Type r
inst✝ : CommRing R
W' : Affine R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (-some x✝ y✝ h✝).xRep = (some x✝ y✝ h✝).xRep
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case inl
F : Type u
inst✝ : Field F
W : Affine F
P : W.Point
⊢ P.xRep = P.xRep

pp: case inr
F : Type u
inst✝ : Field F
W : Affine F
Q : W.Point
⊢ (-Q).xRep = Q.xRep

Tactic:
<;>

Goal state after:
case inl
F : Type u
inst✝ : Field F
W : Affine F
P : W.Point
⊢ P.xRep = P.xRep

case inr
F : Type u
inst✝ : Field F
W : Affine F
Q : W.Point
⊢ (-Q).xRep = Q.xRep
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case zero
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
Q : W'.Point
⊢ zero.sym2x Q ≠ 0

pp: case some
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
Q : W'.Point
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x Q ≠ 0

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
Q : W'.Point
⊢ zero.sym2x Q ≠ 0

case some
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
Q : W'.Point
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x Q ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case zero.zero
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ zero.sym2x zero ≠ 0

pp: case zero.some
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ zero.sym2x (some x✝ y✝ h✝) ≠ 0

pp: case some.zero
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x zero ≠ 0

pp: case some.some
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝¹ y✝¹ : R
h✝¹ : W'.Nonsingular x✝¹ y✝¹
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝¹ y✝¹ h✝¹).sym2x (some x✝ y✝ h✝) ≠ 0

Tactic:
<;>

Goal state after:
case zero.zero
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
⊢ zero.sym2x zero ≠ 0

case zero.some
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ zero.sym2x (some x✝ y✝ h✝) ≠ 0

case some.zero
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x zero ≠ 0

case some.some
R : Type u_1
inst✝¹ : CommRing R
W' : Affine R
inst✝ : Nontrivial R
x✝¹ y✝¹ : R
h✝¹ : W'.Nonsingular x✝¹ y✝¹
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝¹ y✝¹ h✝¹).sym2x (some x✝ y✝ h✝) ≠ 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case zero
R : Type u_1
inst✝ : CommRing R
W' : Affine R
Q : W'.Point
⊢ zero.sym2x Q = Q.sym2x zero

pp: case some
R : Type u_1
inst✝ : CommRing R
W' : Affine R
Q : W'.Point
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x Q = Q.sym2x (some x✝ y✝ h✝)

Tactic:
<;>

Goal state after:
case zero
R : Type u_1
inst✝ : CommRing R
W' : Affine R
Q : W'.Point
⊢ zero.sym2x Q = Q.sym2x zero

case some
R : Type u_1
inst✝ : CommRing R
W' : Affine R
Q : W'.Point
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x Q = Q.sym2x (some x✝ y✝ h✝)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap

Goal state before:
pp: case zero.zero
R : Type u_1
inst✝ : CommRing R
W' : Affine R
⊢ zero.sym2x zero = zero.sym2x zero

pp: case zero.some
R : Type u_1
inst✝ : CommRing R
W' : Affine R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ zero.sym2x (some x✝ y✝ h✝) = (some x✝ y✝ h✝).sym2x zero

pp: case some.zero
R : Type u_1
inst✝ : CommRing R
W' : Affine R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x zero = zero.sym2x (some x✝ y✝ h✝)

pp: case some.some
R : Type u_1
inst✝ : CommRing R
W' : Affine R
x✝¹ y✝¹ : R
h✝¹ : W'.Nonsingular x✝¹ y✝¹
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝¹ y✝¹ h✝¹).sym2x (some x✝ y✝ h✝) = (some x✝ y✝ h✝).sym2x (some x✝¹ y✝¹ h✝¹)

Tactic:
<;>

Goal state after:
case zero.zero
R : Type u_1
inst✝ : CommRing R
W' : Affine R
⊢ zero.sym2x zero = zero.sym2x zero

case zero.some
R : Type u_1
inst✝ : CommRing R
W' : Affine R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ zero.sym2x (some x✝ y✝ h✝) = (some x✝ y✝ h✝).sym2x zero

case some.zero
R : Type u_1
inst✝ : CommRing R
W' : Affine R
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝ y✝ h✝).sym2x zero = zero.sym2x (some x✝ y✝ h✝)

case some.some
R : Type u_1
inst✝ : CommRing R
W' : Affine R
x✝¹ y✝¹ : R
h✝¹ : W'.Nonsingular x✝¹ y✝¹
x✝ y✝ : R
h✝ : W'.Nonsingular x✝ y✝
⊢ (some x✝¹ y✝¹ h✝¹).sym2x (some x✝ y✝ h✝) = (some x✝ y✝ h✝).sym2x (some x✝¹ y✝¹ h✝¹)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: case a₁
R : Type u_1
inst✝² : CommRing R
F : Type u_2
inst✝¹ : Field F
W : WeierstrassCurve R
inst✝ : Invertible 2
⊢ (W.toCharNeTwoNF • W).a₁ = 0

pp: case a₃
R : Type u_1
inst✝² : CommRing R
F : Type u_2
inst✝¹ : Field F
W : WeierstrassCurve R
inst✝ : Invertible 2
⊢ (W.toCharNeTwoNF • W).a₃ = 0

Tactic:
<;>

Goal state after:
case a₁
R : Type u_1
inst✝² : CommRing R
F : Type u_2
inst✝¹ : Field F
W : WeierstrassCurve R
inst✝ : Invertible 2
⊢ (W.toCharNeTwoNF • W).a₁ = 0

case a₃
R : Type u_1
inst✝² : CommRing R
F : Type u_2
inst✝¹ : Field F
W : WeierstrassCurve R
inst✝ : Invertible 2
⊢ (W.toCharNeTwoNF • W).a₃ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: case a₁
R : Type u_1
inst✝³ : CommRing R
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve R
inst✝¹ : Invertible 2
inst✝ : Invertible 3
⊢ ({ u := 1, r := ⅟3 * -(W.toCharNeTwoNF • W).a₂, s := 0, t := 0 } • W.toCharNeTwoNF • W).a₁ = 0

pp: case a₂
R : Type u_1
inst✝³ : CommRing R
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve R
inst✝¹ : Invertible 2
inst✝ : Invertible 3
⊢ ({ u := 1, r := ⅟3 * -(W.toCharNeTwoNF • W).a₂, s := 0, t := 0 } • W.toCharNeTwoNF • W).a₂ = 0

pp: case a₃
R : Type u_1
inst✝³ : CommRing R
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve R
inst✝¹ : Invertible 2
inst✝ : Invertible 3
⊢ ({ u := 1, r := ⅟3 * -(W.toCharNeTwoNF • W).a₂, s := 0, t := 0 } • W.toCharNeTwoNF • W).a₃ = 0

Tactic:
<;>

Goal state after:
case a₁
R : Type u_1
inst✝³ : CommRing R
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve R
inst✝¹ : Invertible 2
inst✝ : Invertible 3
⊢ ({ u := 1, r := ⅟3 * -(W.toCharNeTwoNF • W).a₂, s := 0, t := 0 } • W.toCharNeTwoNF • W).a₁ = 0

case a₂
R : Type u_1
inst✝³ : CommRing R
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve R
inst✝¹ : Invertible 2
inst✝ : Invertible 3
⊢ ({ u := 1, r := ⅟3 * -(W.toCharNeTwoNF • W).a₂, s := 0, t := 0 } • W.toCharNeTwoNF • W).a₂ = 0

case a₃
R : Type u_1
inst✝³ : CommRing R
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve R
inst✝¹ : Invertible 2
inst✝ : Invertible 3
⊢ ({ u := 1, r := ⅟3 * -(W.toCharNeTwoNF • W).a₂, s := 0, t := 0 } • W.toCharNeTwoNF • W).a₃ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
F : Type u_2
inst✝² : Field F
W : WeierstrassCurve R
inst✝¹ : Invertible 2
inst✝ : Invertible 3
⊢ (W.toShortNF • W).IsShortNF

Tactic:
by
  rw [toShortNF, mul_smul]
  constructor <;> simp [variableChange_a₁, variableChange_a₂, variableChange_a₃]

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

Goal state before:
pp: case h.a₃
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ ({ u := 1, r := 0, s := s, t := 0 } • E).a₃ = E'.a₃

Tactic:
simp_rw [variableChange_a₃, inv_one, Units.val_one, a₃_of_isCharTwoJNeZeroNF]

Goal state after:
case h.a₃
F : Type u_1
inst✝⁴ : Field F
inst✝³ : IsSepClosed F
E E' : WeierstrassCurve F
inst✝² : CharP F 2
inst✝¹ : E.IsCharTwoJNeZeroNF
inst✝ : E'.IsCharTwoJNeZeroNF
heq : E.a₆ = E'.a₆
s : F
hs : 1 * s ^ 2 + 1 * s + (E.a₂ + E'.a₂) = 0
⊢ 1 ^ 3 * (0 + 0 * E.a₁ + 2 * 0) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

pp: case right
m : ℕ
⊢ ((2 * ↑m + 4 + 1) ^ 2 - 1 =
      ((↑m + 4) ^ 2 - if Even m then 4 else 1) + 3 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) +
        2 * if Even m then 6 else 0) ∧
    (2 * ↑m + 4 + 1) ^ 2 - 1 =
      ((↑m + 1) ^ 2 - if Even m then 1 else 4) + 3 * ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
        2 * if Even m then 0 else 6

Tactic:
<;>

Goal state after:
case left
m : ℕ
⊢ (2 * ↑m + 6) ^ 2 - 4 =
      2 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
        ((↑m + 5) ^ 2 - if Even m then 1 else 4) ∧
    (2 * ↑m + 6) ^ 2 - 4 =
      ((↑m + 1) ^ 2 - if Even m then 1 else 4) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
        2 * ((↑m + 4) ^ 2 - if Even m then 4 else 1)

case right
m : ℕ
⊢ ((2 * ↑m + 4 + 1) ^ 2 - 1 =
      ((↑m + 4) ^ 2 - if Even m then 4 else 1) + 3 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) +
        2 * if Even m then 6 else 0) ∧
    (2 * ↑m + 4 + 1) ^ 2 - 1 =
      ((↑m + 1) ^ 2 - if Even m then 1 else 4) + 3 * ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
        2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

pp: case left.right
m : ℕ
⊢ (2 * ↑m + 6) ^ 2 - 4 =
    ((↑m + 1) ^ 2 - if Even m then 1 else 4) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
      2 * ((↑m + 4) ^ 2 - if Even m then 4 else 1)

pp: case right.left
m : ℕ
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 =
    ((↑m + 4) ^ 2 - if Even m then 4 else 1) + 3 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) +
      2 * if Even m then 6 else 0

pp: case right.right
m : ℕ
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 =
    ((↑m + 1) ^ 2 - if Even m then 1 else 4) + 3 * ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
      2 * if Even m then 0 else 6

Tactic:
<;>

Goal state after:
case left.left
m : ℕ
⊢ (2 * ↑m + 6) ^ 2 - 4 =
    2 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
      ((↑m + 5) ^ 2 - if Even m then 1 else 4)

case left.right
m : ℕ
⊢ (2 * ↑m + 6) ^ 2 - 4 =
    ((↑m + 1) ^ 2 - if Even m then 1 else 4) + ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
      2 * ((↑m + 4) ^ 2 - if Even m then 4 else 1)

case right.left
m : ℕ
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 =
    ((↑m + 4) ^ 2 - if Even m then 4 else 1) + 3 * ((↑m + 2) ^ 2 - if Even m then 4 else 1) +
      2 * if Even m then 6 else 0

case right.right
m : ℕ
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 =
    ((↑m + 1) ^ 2 - if Even m then 1 else 4) + 3 * ((↑m + 3) ^ 2 - if Even m then 1 else 4) +
      2 * if Even m then 0 else 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms

Goal state before:
pp: case of_j_ne_zero
R : Type u_1
inst✝² : CommRing R
F : Type u_2
inst✝¹ : Field F
W : WeierstrassCurve R
inst✝ : W.IsCharThreeJNeZeroNF
⊢ W.IsCharNeTwoNF

pp: case of_j_eq_zero
R : Type u_1
inst✝² : CommRing R
F : Type u_2
inst✝¹ : Field F
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ W.IsCharNeTwoNF

Tactic:
<;>

Goal state after:
case of_j_ne_zero
R : Type u_1
inst✝² : CommRing R
F : Type u_2
inst✝¹ : Field F
W : WeierstrassCurve R
inst✝ : W.IsCharThreeJNeZeroNF
⊢ W.IsCharNeTwoNF

case of_j_eq_zero
R : Type u_1
inst✝² : CommRing R
F : Type u_2
inst✝¹ : Field F
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ W.IsCharNeTwoNF
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case pos
m : ℕ
h✝ : Even m
⊢ (2 * ↑m + 6) ^ 2 - 4 = 2 * ((↑m + 2) ^ 2 - 4) + ((↑m + 3) ^ 2 - 1) + ((↑m + 5) ^ 2 - 1)

pp: case neg
m : ℕ
h✝ : ¬Even m
⊢ (2 * ↑m + 6) ^ 2 - 4 = 2 * ((↑m + 2) ^ 2 - 1) + ((↑m + 3) ^ 2 - 4) + ((↑m + 5) ^ 2 - 4)

pp: case pos
m : ℕ
h✝ : Even m
⊢ (2 * ↑m + 6) ^ 2 - 4 = (↑m + 1) ^ 2 - 1 + ((↑m + 3) ^ 2 - 1) + 2 * ((↑m + 4) ^ 2 - 4)

pp: case neg
m : ℕ
h✝ : ¬Even m
⊢ (2 * ↑m + 6) ^ 2 - 4 = (↑m + 1) ^ 2 - 4 + ((↑m + 3) ^ 2 - 4) + 2 * ((↑m + 4) ^ 2 - 1)

pp: case pos
m : ℕ
h✝ : Even m
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 = (↑m + 4) ^ 2 - 4 + 3 * ((↑m + 2) ^ 2 - 4) + 2 * 6

pp: case neg
m : ℕ
h✝ : ¬Even m
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 = (↑m + 4) ^ 2 - 1 + 3 * ((↑m + 2) ^ 2 - 1) + 2 * 0

pp: case pos
m : ℕ
h✝ : Even m
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 = (↑m + 1) ^ 2 - 1 + 3 * ((↑m + 3) ^ 2 - 1) + 2 * 0

pp: case neg
m : ℕ
h✝ : ¬Even m
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 = (↑m + 1) ^ 2 - 4 + 3 * ((↑m + 3) ^ 2 - 4) + 2 * 6

Tactic:
<;>

Goal state after:
case pos
m : ℕ
h✝ : Even m
⊢ (2 * ↑m + 6) ^ 2 - 4 = 2 * ((↑m + 2) ^ 2 - 4) + ((↑m + 3) ^ 2 - 1) + ((↑m + 5) ^ 2 - 1)

case neg
m : ℕ
h✝ : ¬Even m
⊢ (2 * ↑m + 6) ^ 2 - 4 = 2 * ((↑m + 2) ^ 2 - 1) + ((↑m + 3) ^ 2 - 4) + ((↑m + 5) ^ 2 - 4)

case pos
m : ℕ
h✝ : Even m
⊢ (2 * ↑m + 6) ^ 2 - 4 = (↑m + 1) ^ 2 - 1 + ((↑m + 3) ^ 2 - 1) + 2 * ((↑m + 4) ^ 2 - 4)

case neg
m : ℕ
h✝ : ¬Even m
⊢ (2 * ↑m + 6) ^ 2 - 4 = (↑m + 1) ^ 2 - 4 + ((↑m + 3) ^ 2 - 4) + 2 * ((↑m + 4) ^ 2 - 1)

case pos
m : ℕ
h✝ : Even m
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 = (↑m + 4) ^ 2 - 4 + 3 * ((↑m + 2) ^ 2 - 4) + 2 * 6

case neg
m : ℕ
h✝ : ¬Even m
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 = (↑m + 4) ^ 2 - 1 + 3 * ((↑m + 2) ^ 2 - 1) + 2 * 0

case pos
m : ℕ
h✝ : Even m
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 = (↑m + 1) ^ 2 - 1 + 3 * ((↑m + 3) ^ 2 - 1) + 2 * 0

case neg
m : ℕ
h✝ : ¬Even m
⊢ (2 * ↑m + 4 + 1) ^ 2 - 1 = (↑m + 1) ^ 2 - 4 + 3 * ((↑m + 3) ^ 2 - 4) + 2 * 6
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: case inl
n : ℕ
⊢ ↑(expCoeff (2 * n)) = if Even (2 * n) then ↑(2 * n) / 2 else ↑(2 * n)

pp: case inr
n : ℕ
⊢ ↑(expCoeff (2 * n + 1)) = if Even (2 * n + 1) then ↑(2 * n + 1) / 2 else ↑(2 * n + 1)

Tactic:
<;>

Goal state after:
case inl
n : ℕ
⊢ ↑(expCoeff (2 * n)) = if Even (2 * n) then ↑(2 * n) / 2 else ↑(2 * n)

case inr
n : ℕ
⊢ ↑(expCoeff (2 * n + 1)) = if Even (2 * n + 1) then ↑(2 * n + 1) / 2 else ↑(2 * n + 1)