mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
m✝ : ℕ
ih : ∀ k_1 < 2 * (m✝ + 1) + 1, f (complEDS' b c d k k_1) = complEDS' (f b) (f c) (f d) k k_1
⊢ complEDS' (f b) (f c) (f d) k (m✝ + 1) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k - 1) -
      f (complEDS' b c d k (m✝ + 2)) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k - 1) =
    complEDS' (f b) (f c) (f d) k (m✝ + 1) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k - 1) -
      complEDS' (f b) (f c) (f d) k (m✝ + 2) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k - 1)

Tactic:
]

Goal state after:
case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
m✝ : ℕ
ih : ∀ k_1 < 2 * (m✝ + 1) + 1, f (complEDS' b c d k k_1) = complEDS' (f b) (f c) (f d) k k_1
⊢ complEDS' (f b) (f c) (f d) k (m✝ + 1) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k - 1) -
      f (complEDS' b c d k (m✝ + 2)) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k - 1) =
    complEDS' (f b) (f c) (f d) k (m✝ + 1) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k - 1) -
      complEDS' (f b) (f c) (f d) k (m✝ + 2) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k - 1)
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: case odd
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
b c d : R
k : ℤ
m✝ : ℕ
ih : ∀ k_1 < 2 * (m✝ + 1) + 1, f (complEDS' b c d k k_1) = complEDS' (f b) (f c) (f d) k k_1
⊢ complEDS' (f b) (f c) (f d) k (m✝ + 1) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k - 1) -
      complEDS' (f b) (f c) (f d) k (m✝ + 2) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k - 1) =
    complEDS' (f b) (f c) (f d) k (m✝ + 1) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 2) * k - 1) -
      complEDS' (f b) (f c) (f d) k (m✝ + 2) ^ 2 * normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k + 1) *
        normEDS (f b) (f c) (f d) ((↑m✝ + 1) * k - 1)

Tactic:
]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C (C 4 * X ^ 3 + C (W.a₁ ^ 2 + 4 * W.a₂) * X ^ 2 + C (2 * (2 * W.a₄ + W.a₁ * W.a₃)) * X + C (W.a₃ ^ 2 + 4 * W.a₆)) =
    (C (C 2) * Y + C (C W.toAffine.a₁ * X + C W.toAffine.a₃)) ^ 2 -
      4 *
        (Y ^ 2 + C (C W.toAffine.a₁ * X + C W.toAffine.a₃) * Y -
          C (X ^ 3 + C W.toAffine.a₂ * X ^ 2 + C W.toAffine.a₄ * X + C W.toAffine.a₆))

Tactic:
]

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C (C 4 * X ^ 3 + C (W.a₁ ^ 2 + 4 * W.a₂) * X ^ 2 + C (2 * (2 * W.a₄ + W.a₁ * W.a₃)) * X + C (W.a₃ ^ 2 + 4 * W.a₆)) =
    (C (C 2) * Y + C (C W.toAffine.a₁ * X + C W.toAffine.a₃)) ^ 2 -
      4 *
        (Y ^ 2 + C (C W.toAffine.a₁ * X + C W.toAffine.a₃) * Y -
          C (X ^ 3 + C W.toAffine.a₂ * X ^ 2 + C W.toAffine.a₄ * X + C W.toAffine.a₆))
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 * W.Ψ₂Sq =
    (W.preΨ (m - 1) ^ 2 * W.preΨ m * W.preΨ (m + 2) - W.preΨ (m - 2) * W.preΨ m * W.preΨ (m + 1) ^ 2) ^ 2 * W.Ψ₂Sq

Tactic:
]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℤ
⊢ ((W.preΨ (m + 2) * W.preΨ m ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
        W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) ^
      2 =
    ((W.preΨ (m + 2) * W.preΨ m ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
        W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) ^
      2

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg.some.some.inr
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ (p ^ 2 - (p * q * (C W'.a₁ * X + C W'.a₃) + q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆))).degree =
    max (2 • some dp) (2 • some dq + 3)

Tactic:
]

Goal state after:
case neg.some.some.inr
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ (p ^ 2 - (p * q * (C W'.a₁ * X + C W'.a₃) + q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆))).degree =
    max (2 • some dp) (2 • some dq + 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case e'_3.e'_3
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ 2 • some dp = 2 • some dp

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg.some.some.inr.convert_2
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ some dp + some dq + 1 < 2 • some dp

Tactic:
]

Goal state after:
case neg.some.some.inr.convert_2
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ some dp + some dq + 1 < 2 • some dp
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg.some.some.inr.convert_3
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ 2 • some dq + 3 < 2 • some dp

Tactic:
]

Goal state after:
case neg.some.some.inr.convert_3
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ 2 • some dq + 3 < 2 • some dp
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case neg.some.some.inr.convert_5
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ 2 • some dq + 3 < 2 • some dp

Tactic:
]

Goal state after:
case neg.some.some.inr.convert_5
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
hp : ¬p.degree = ⊥
hq : ¬q.degree = ⊥
dp : ℕ
hdp : (p ^ 2).degree = 2 • some dp
hp' : p.degree = some dp
dq : ℕ
hdq : (q ^ 2 * (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)).degree = 2 • some dq + 3
hdpq : (p * q * (C W'.a₁ * X + C W'.a₃)).degree ≤ some dp + some dq + 1
hq' : q.degree = some dq
hpq : dq + 1 < dp
⊢ 2 • some dq + 3 < 2 • some dp
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: case refine_3.refine_2
I : Type u
inst✝⁶ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁵ : IsCofiltered I
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)
𝒰 : c.pt.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : Finite 𝒰.I₀
i : I
V : 𝒰.I₀ → (D.obj i).Opens
hV : TopologicalSpace.IsOpenCover V
hV' : ∀ (j : 𝒰.I₀), IsAffineOpen (V j) ∧ Hom.opensRange (𝒰.f j) = c.π.app i ⁻¹ᵁ V j
hV'' : ∀ (k : 𝒰.I₀), Set.range ⇑(𝒰.f k) = ⇑(c.π.app i) ⁻¹' ↑(V k)
k : 𝒰.I₀
s : PullbackCone ⋯.fromSpec (c.π.app i)
y : ↥s.pt
⊢ (s.fst ≫ ⋯.fromSpec) y ∈ V k

Tactic:
]

Goal state after:
case refine_3.refine_2
I : Type u
inst✝⁶ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁵ : IsCofiltered I
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)
𝒰 : c.pt.OpenCover
inst✝¹ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
inst✝ : Finite 𝒰.I₀
i : I
V : 𝒰.I₀ → (D.obj i).Opens
hV : TopologicalSpace.IsOpenCover V
hV' : ∀ (j : 𝒰.I₀), IsAffineOpen (V j) ∧ Hom.opensRange (𝒰.f j) = c.π.app i ⁻¹ᵁ V j
hV'' : ∀ (k : 𝒰.I₀), Set.range ⇑(𝒰.f k) = ⇑(c.π.app i) ⁻¹' ↑(V k)
k : 𝒰.I₀
s : PullbackCone ⋯.fromSpec (c.π.app i)
y : ↥s.pt
⊢ (s.fst ≫ ⋯.fromSpec) y ∈ V k
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • p.degree) (2 • q.degree + 3) ≠ 1

Tactic:
]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Affine R
inst✝ : IsDomain R
p q : R[X]
⊢ max (2 • p.degree) (2 • q.degree + 3) ≠ 1
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)

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)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
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 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.some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some x₂ y₂ h✝ = 0 ↔ some x₂ y₂ h✝ = 0

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case some.some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some x₁ y₁ h✝¹ + some x₂ y₂ h✝ = 0 ↔ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂

Tactic:
]

Goal state after:
case some.some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ y₁ : F
h✝¹ : W.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
⊢ some x₁ y₁ h✝¹ + some x₂ y₂ h✝ = 0 ↔ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case mp
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
P : W.Point
⊢ toClass P = 0 → P = 0

Tactic:
intro hP

Goal state after:
case mp
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
P : W.Point
hP : toClass P = 0
⊢ P = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (X * W.ΨSq (↑n + 1) - W.preΨ (↑n + 1 + 1) * W.preΨ ↑n * if Even (↑n + 1) then 1 else W.Ψ₂Sq) =
    (X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) -
      W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1

Tactic:
]

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ (X * W.ΨSq (↑n + 1) - W.preΨ (↑n + 1 + 1) * W.preΨ ↑n * if Even (↑n + 1) then 1 else W.Ψ₂Sq) =
    (X * W.preΨ' (n + 1) ^ 2 * if Even n then 1 else W.Ψ₂Sq) -
      W.preΨ' (n + 2) * W.preΨ' n * if Even n then W.Ψ₂Sq else 1
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x✝ y✝ : F
h : W.Equation x✝ y✝
right✝ : evalEval x✝ y✝ W.polynomialX ≠ 0 ∨ evalEval x✝ y✝ W.polynomialY ≠ 0
hP : toClass (some x✝ y✝ ⋯) = 0
p : W.CoordinateRing
h0 : p ≠ 0
hp : CoordinateRing.XYIdeal W x✝ (C y✝) = span {p}
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case zero
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
a₂✝ : W.Point
hP : toClass zero = toClass a₂✝
⊢ toClass (-zero) + toClass zero = 0

Tactic:
]

Goal state after:
case zero
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
a₂✝ : W.Point
hP : toClass zero = toClass a₂✝
⊢ toClass (-zero) + toClass zero = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x✝ y✝ : F
h : W.Nonsingular x✝ y✝
a₂✝ : W.Point
hP : toClass (some x✝ y✝ h) = toClass a₂✝
⊢ toClass (-some x✝ y✝ h) + toClass (some x✝ y✝ h) = 0

Tactic:
]

Goal state after:
case some
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x✝ y✝ : F
h : W.Nonsingular x✝ y✝
a₂✝ : W.Point
hP : toClass (some x✝ y✝ h) = toClass a₂✝
⊢ toClass (-some x✝ y✝ h) + toClass (some x✝ y✝ h) = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: 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✝ : W.Point
⊢ -x✝ = -x✝

Tactic:
]

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

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

Tactic:
]

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * 1 ^ 2 * (C 4 * X ^ 3 + C W.b₂ * X ^ 2 + C (2 * W.b₄) * X + C W.b₆) -
      (3 * X ^ 4 + C W.b₂ * X ^ 3 + 3 * C W.b₄ * X ^ 2 + 3 * C W.b₆ * X + C W.b₈) * 1 * 1 =
    X ^ 4 - C W.b₄ * X ^ 2 - C (2 * W.b₆) * X - C W.b₈
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : IsCofiltered I
inst✝⁵ : ∀ (i : I), IsAffine (D.obj i)
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝⁴ : IsAffine (Spec R)
S : CommRingCat
inst✝³ : IsAffine (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst✝² : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine (D.obj i)]
    (t : D ⟶ (Functor.const I).obj (Spec R)) (a : c.pt ⟶ Spec S),
    c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ D', D = D' ⋙ Scheme.Spec) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst✝¹ : ∀ (i : I), IsIso (e.app i)
inst✝ : IsIso e
inst : ∀ (i : I), IsAffine ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
i : I
g : (D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i ⟶ Spec S
hg : ((Cone.postcompose (asIso e).hom).obj c).π.app i ≫ g = a
hg' : g ≫ Spec.map φ = (inv e ≫ t).app i
⊢ (c.π.app i ≫ e.app i) ≫ g = a

Tactic:
]

Goal state after:
I : Type u
inst✝⁷ : Category.{u, u} I
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁶ : IsCofiltered I
inst✝⁵ : ∀ (i : I), IsAffine (D.obj i)
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
inst✝⁴ : IsAffine (Spec R)
S : CommRingCat
inst✝³ : IsAffine (Spec S)
a : c.pt ⟶ Spec S
φ : R ⟶ S
inst✝² : LocallyOfFinitePresentation (Spec.map φ)
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
this :
  ∀ (D : I ⥤ Scheme) (c : Cone D) (hc : IsLimit c) [∀ (i : I), IsAffine (D.obj i)]
    (t : D ⟶ (Functor.const I).obj (Spec R)) (a : c.pt ⟶ Spec S),
    c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ D', D = D' ⋙ Scheme.Spec) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = t.app i
hD : ¬∃ D', D = D' ⋙ Scheme.Spec
e : D ⟶ D ⋙ Γ.rightOp ⋙ Scheme.Spec := D.whiskerLeft ΓSpec.adjunction.unit
inst✝¹ : ∀ (i : I), IsIso (e.app i)
inst✝ : IsIso e
inst : ∀ (i : I), IsAffine ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)
i : I
g : (D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i ⟶ Spec S
hg : ((Cone.postcompose (asIso e).hom).obj c).π.app i ≫ g = a
hg' : g ≫ Spec.map φ = (inv e ≫ t).app i
⊢ (c.π.app i ≫ e.app i) ≫ g = a
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq = X * W.Ψ₃ ^ 2 - W.preΨ₄ * W.Ψ₂Sq

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: 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
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₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
⊢ f ((W'⁄F).negY x₂ y₂) = f ((W'⁄F).negY x₂ y₂)

Tactic:
]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - (W.preΨ₄ * 1 ^ 3 * W.Ψ₂Sq ^ 2 - 1 * W.Ψ₃ ^ 3 * 1) * W.Ψ₃ * 1 =
    X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)

Tactic:
]

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - (W.preΨ₄ * 1 ^ 3 * W.Ψ₂Sq ^ 2 - 1 * W.Ψ₃ ^ 3 * 1) * W.Ψ₃ * 1 =
    X * W.preΨ₄ ^ 2 * W.Ψ₂Sq - W.Ψ₃ * (W.preΨ₄ * W.Ψ₂Sq ^ 2 - W.Ψ₃ ^ 3)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: case pos
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
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₁
x₂ y₂ : F
h₂ : (W'⁄F).Nonsingular x₂ y₂
hxy : x₁ = x₂ ∧ y₁ = (W'⁄F).negY x₂ y₂
⊢ (match 0 with
    | zero => 0
    | some x y h => some (f x) (f y) ⋯) =
    0

Tactic:
]

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C X * (C W.preΨ₄ * W.ψ₂) ^ 2 - (C W.preΨ₄ * W.ψ₂ * W.ψ₂ ^ 3 - 1 * C W.Ψ₃ ^ 3) * C W.Ψ₃ =
    C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4

Tactic:
]

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ C X * (C W.preΨ₄ * W.ψ₂) ^ 2 - (C W.preΨ₄ * W.ψ₂ * W.ψ₂ ^ 3 - 1 * C W.Ψ₃ ^ 3) * C W.Ψ₃ =
    C X * C W.preΨ₄ ^ 2 * W.ψ₂ ^ 2 - C W.preΨ₄ * W.ψ₂ ^ 4 * C W.Ψ₃ + C W.Ψ₃ ^ 4
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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