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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ (W.map f).Δ' = (Units.map ↑f) W.Δ'

Tactic:
ext

Goal state after:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
A : Type v
inst✝ : CommRing A
f : R →+* A
⊢ ↑(W.map f).Δ' = ↑((Units.map ↑f) W.Δ')
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y W'.negPolynomial = W'.negY x y

Tactic:
rw [negY, sub_sub, negPolynomial]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Affine R
x y : R
⊢ evalEval x y (-Y - C (C W'.a₁ * X + C W'.a₃)) = -y - (W'.a₁ * x + W'.a₃)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ x✝¹ = x✝

Tactic:
ext

Goal state after:
case u
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ ↑x✝¹.u = ↑x✝.u

case r
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ x✝¹.r = x✝.r

case s
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ x✝¹.s = x✝.s

case t
R : Type u
inst✝¹ : CommRing R
A : Type v
inst✝ : CommRing A
φ : R →+* A
hφ : Function.Injective ⇑φ
x✝¹ x✝ : VariableChange R
h✝ : (fun C ↦ C.map φ) x✝¹ = (fun C ↦ C.map φ) x✝
left✝¹ : φ x✝¹.r = φ x✝.r
left✝ : φ x✝¹.s = φ x✝.s
right✝ : φ x✝¹.t = φ x✝.t
h : ↑φ ↑x✝¹.u = ↑φ ↑x✝.u
⊢ x✝¹.t = x✝.t
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 } = { u := 1, r := 0, s := 0, t := 0 }

Tactic:
ext

Goal state after:
case u
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ ↑{ u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.u = ↑{ u := 1, r := 0, s := 0, t := 0 }.u

case r
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.r = { u := 1, r := 0, s := 0, t := 0 }.r

case s
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.s = { u := 1, r := 0, s := 0, t := 0 }.s

case t
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ { u := (Units.map ↑φ) 1, r := φ 0, s := φ 0, t := φ 0 }.t = { u := 1, r := 0, s := 0, t := 0 }.t
Module: Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
      t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) } =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
      s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
      t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }

Tactic:
ext

Goal state after:
case u
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ ↑{ u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
          t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.u =
    ↑{ u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
          s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
          t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.u

case r
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
        t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.r =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
        s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
        t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.r

case s
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
        t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.s =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
        s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
        t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.s

case t
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
C✝ : VariableChange R
A : Type v
inst✝ : CommRing A
φ : R →+* A
C C' : VariableChange R
⊢ { u := (Units.map ↑φ) (C.u * C'.u), r := φ (C.r * ↑C'.u ^ 2 + C'.r), s := φ (↑C'.u * C.s + C'.s),
        t := φ (C.t * ↑C'.u ^ 3 + C.r * C'.s * ↑C'.u ^ 2 + C'.t) }.t =
    { u := (Units.map ↑φ) C.u * (Units.map ↑φ) C'.u, r := φ C.r * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.r,
        s := ↑((Units.map ↑φ) C'.u) * φ C.s + φ C'.s,
        t := φ C.t * ↑((Units.map ↑φ) C'.u) ^ 3 + φ C.r * φ C'.s * ↑((Units.map ↑φ) C'.u) ^ 2 + φ C'.t }.t
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Affine R
⊢ (CoordinateRing.basis W') 1 = (mk W') Y

Tactic:
simpa only [basis_apply] using! pow_one _

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

Goal state before:
pp: case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
⊢ { a := 1, b := -W.slope x₁ x₂ y₁ y₂ ^ 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c := 2 * x₁ * W.slope x₁ x₂ y₁ y₂ ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ + (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * W.slope x₁ x₂ y₁ y₂ ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }

Tactic:
slope_of_X_ne hx

Goal state after:
case neg
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
⊢ { a := 1, b := -((y₁ - y₂) / (x₁ - x₂)) ^ 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂,
      c :=
        2 * x₁ * ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((y₁ - y₂) / (x₁ - x₂)) +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * ((y₁ - y₂) / (x₁ - x₂)) -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)) + x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)),
      d := -(x₁ * x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))) }
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula

Goal state before:
pp: case neg
F : Type u
K : Type v
inst✝³ : Field F
inst✝² : Field K
W : Affine F
inst✝¹ : DecidableEq F
inst✝ : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : ¬x₁ = x₂
⊢ (f y₁ - f y₂) / (f x₁ - f x₂) = f (W.slope x₁ x₂ y₁ y₂)

Tactic:
slope_of_X_ne hx

Goal state after:
case neg
F : Type u
K : Type v
inst✝³ : Field F
inst✝² : Field K
W : Affine F
inst✝¹ : DecidableEq F
inst✝ : DecidableEq K
f : F →+* K
x₁ x₂ y₁ y₂ : F
hx : ¬x₁ = x₂
⊢ (f y₁ - f y₂) / (f x₁ - f x₂) = f ((y₁ - y₂) / (x₁ - x₂))
Module: Mathlib.NumberTheory.EllipticDivisibilitySequence

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
W : ℤ → R
odd : Function.Odd W
a b c : ℤ
⊢ atomRel W a b c a = W a * W 0 * atom W b c

Tactic:
by
  simp_rw [atomRel, atom_mul_atom odd a b, mul_comm <| atom W b a, sub_self, zero_add, atom_same]

Goal state after:
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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
⊢ ∃ i, (D.obj i).IsQuasiAffine

Tactic:
have (x : c.pt) : ∃ (i : I) (f : Γ(D.obj i, ⊤)),
      IsAffineOpen (Scheme.basicOpen _ f) ∧ c.π.app i x ∈ (Scheme.basicOpen _ f) := by
    obtain ⟨i⟩ := IsCofiltered.nonempty (C := I)
    obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ := (D.obj i).isBasis_affineOpens.exists_subset_of_mem_open
      (Set.mem_univ (c.π.app i x)) isOpen_univ
    obtain ⟨_, ⟨_, ⟨r, hr, rfl⟩, rfl⟩, hxr, hrU⟩ :=
      (IsQuasiAffine.isBasis_basicOpen c.pt).exists_subset_of_mem_open hxU (c.π.app i ⁻¹ᵁ U).isOpen
    obtain ⟨j, r, rfl⟩ := exists_appTop_π_eq_of_isLimit D c hc r
    obtain ⟨k, fki, fkj, -⟩ := IsCofilteredOrEmpty.cone_objs i j
    obtain ⟨l, flk, hl⟩ := exists_map_preimage_le_map_preimage D c hc (isCompact_basicOpen _
      isCompact_univ ((D.map fkj).appTop r)) (V := D.map fki ⁻¹ᵁ U) (by
        rwa [← preimage_basicOpen_top, ← Hom.comp_preimage, ← Hom.comp_preimage,
          c.w, c.w, preimage_basicOpen_top])
    refine ⟨l, (D.map (flk ≫ fkj)).appTop r, ?_, ?_⟩
    · convert!
      (hU.preimage (D.map (flk ≫ fki))).basicOpen
        ((D.obj _).presheaf.map (homOfLE le_top).op ((D.map (flk ≫ fkj)).appTop r)) using 1
      rwa [Scheme.basicOpen_res, eq_comm, inf_eq_right, Functor.map_comp,
        elementwise_of% Scheme.Hom.comp_appTop, ← Scheme.preimage_basicOpen_top, Functor.map_comp,
        Scheme.Hom.comp_preimage]
    · change x ∈ c.π.app l ⁻¹ᵁ (D.obj l).basicOpen _
      rwa [Scheme.preimage_basicOpen_top, ← elementwise_of% Scheme.Hom.comp_appTop, Cone.w]

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
inst✝² : ∀ (i : I), CompactSpace ↥(D.obj i)
inst✝¹ : ∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)
inst✝ : c.pt.IsQuasiAffine
this : ∀ (x : ↥c.pt), ∃ i f, IsAffineOpen ((D.obj i).basicOpen f) ∧ (c.π.app i) x ∈ (D.obj i).basicOpen f
⊢ ∃ i, (D.obj i).IsQuasiAffine
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✝¹ : Nontrivial R
inst✝ : WeierstrassCurve.IsElliptic W'
p : W'.Point → Prop
p0 : p Point.zero
⊢ (fun xy ↦ ∃ (h : W'.Nonsingular xy.1 xy.2), p (Point.some xy.1 xy.2 h)) = fun xy ↦
    ∃ (h : W'.Equation xy.1 xy.2), p (Point.mk h)

Tactic:
ext

Goal state after:
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✝¹ : Nontrivial R
inst✝ : WeierstrassCurve.IsElliptic W'
p : W'.Point → Prop
p0 : p Point.zero
x✝ : R × R
⊢ (∃ (h : W'.Nonsingular x✝.1 x✝.2), p (Point.some x✝.1 x✝.2 h)) ↔ ∃ (h : W'.Equation x✝.1 x✝.2), p (Point.mk h)
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:
constructor

Goal state after:
case some.some.mp
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₂

case some.some.mpr
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₂
⊢ x₁ = x₂ ∧ y₁ = W.negY x₂ y₂ → some x₁ y₁ h✝¹ + some x₂ y₂ h✝ = 0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point

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

Tactic:
constructor

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

case mpr
F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
P : W.Point
⊢ P = 0 → toClass P = 0
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
inst✝⁴ : IsCofiltered I
R : CommRingCat
inst✝³ : IsAffine (Spec R)
S : CommRingCat
inst✝² : IsAffine (Spec S)
φ : R ⟶ S
inst✝¹ : LocallyOfFinitePresentation (Spec.map φ)
D : I ⥤ CommRingCatᵒᵖ
inst✝ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
e : ((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec ≅ (Functor.const I).obj (Spec R) :=
  NatIso.ofComponents (fun x ↦ Iso.refl ((((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).obj x)) ⋯
t : (Functor.const Iᵒᵖ).obj R ⟶ D.leftOp
c' : Cocone D.leftOp
ψ : S ⟶ Opposite.unop (coneOfCoconeLeftOp c').pt
ha :
  (Scheme.Spec.mapCone (coneOfCoconeLeftOp c')).π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom =
    (Functor.const I).map (Spec.map ψ ≫ Spec.map φ)
hc : IsColimit c'
i : Iᵒᵖ
g : S ⟶ D.leftOp.obj i
hg : φ ≫ g = t.app i
hg' : ψ = g ≫ c'.ι.app i
⊢ Spec.map g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app (Opposite.unop i)

Tactic:
simpa using! congr(Spec.map $hg)

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : IsReduced R
x : Fin 3 → R
hx : (fun i ↦ (eval x) (W.addSubMap i)) = 0
i : Fin 3
⊢ x i = 0 i

Tactic:
simpa [congrFun hx] using (addSubMapCoeff_condition W x i).symm

Goal state after:
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
⊢ (W.toCharNeTwoNF • W).IsCharNeTwoNF

Tactic:
constructor

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: 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).IsShortNF

Tactic:
constructor

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.IsomOfJ

Goal state before:
pp: case h
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 = E'

Tactic:
ext

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
⊢ ({ u := 1, r := 0, s := s, t := 0 } • E).a₁ = E'.a₁

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₂

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₃

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₄

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₆
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree

Goal state before:
pp: 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)) ∧
    ((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:
constructor

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
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)

Tactic:
constructor

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

Goal state before:
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:
constructor

Goal state after:
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.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,
      a₄_of_isCharTwoJNeZeroNF]
    ring1

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

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

Tactic:
constructor

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

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