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

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : IsAffine X
inst✝² : ∀ (i : I), IsAffine (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
f : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : IsAffine (Spec R)
ha : c.π ≫ t = (Functor.const I).map (a ≫ f)
this :
  ∀ {X : Scheme} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    c.π ≫ t = (Functor.const I).map (a ≫ f) → (∃ S, X = Spec S) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hX : ¬∃ S, X = Spec S
⊢ c.π ≫ t = (Functor.const I).map ((a ≫ X.isoSpec.hom) ≫ X.isoSpec.inv ≫ f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineTransitionLimit

Goal state before:
pp: I : Type u
inst✝⁵ : Category.{u, u} I
X : Scheme
D : I ⥤ Scheme
c : Cone D
hc : IsLimit c
inst✝⁴ : IsCofiltered I
inst✝³ : IsAffine X
inst✝² : ∀ (i : I), IsAffine (D.obj i)
a : c.pt ⟶ X
R : CommRingCat
t : D ⟶ (Functor.const I).obj (Spec R)
f✝ : X ⟶ Spec R
inst✝¹ : LocallyOfFinitePresentation f✝
inst✝ : IsAffine (Spec R)
ha : c.π ≫ t = (Functor.const I).map (a ≫ f✝)
this :
  ∀ {X : Scheme} [IsAffine X] (a : c.pt ⟶ X) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    c.π ≫ t = (Functor.const I).map (a ≫ f) → (∃ S, X = Spec S) → ∃ i g, c.π.app i ≫ g = a ∧ g ≫ f = t.app i
hX : ¬∃ S, X = Spec S
i : I
f : D.obj i ⟶ Spec Γ(X, ⊤)
hf : c.π.app i ≫ f = a ≫ X.isoSpec.hom ∧ f ≫ X.isoSpec.inv ≫ f✝ = t.app i
⊢ c.π.app i ≫ f ≫ X.isoSpec.inv = a ∧ (f ≫ X.isoSpec.inv) ≫ f✝ = t.app i

Tactic:
by

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
⊢ ∀ (x y : W.Point),
    (match x + y with
      | zero => 0
      | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) =
      (match x with
        | zero => 0
        | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)) +
        match y with
        | zero => 0
        | some x y h => (ClassGroup.mk W.FunctionField) (CoordinateRing.XYIdeal' h)

Tactic:
by

Goal state after:
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.Nonsingular x₁ y₁
x₂ y₂ : F
h✝ : W.Nonsingular x₂ y₂
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
⊢ ¬some x₁ y₁ h✝¹ + some x₂ y₂ h✝ = 0

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (W.Ψ n) ^ 2 = (mk W) (C (W.ΨSq n))

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ ↑(CoordinateRing.XYIdeal' ⋯) = ↑?m.48

Tactic:
by

Goal state after:
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:
by

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 : 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
i : I
⊢ IsIso (e.app i)

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
⊢ Function.Injective ⇑toClass

Tactic:
rintro (_ | ⟨_, _, h⟩) _ hP

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₂✝
⊢ zero = a₂✝

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₂✝
⊢ some x✝ y✝ h = a₂✝
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
⊢ W.Φ (↑n + 1) =
    (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:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 0 = 1

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.Φ 1 = X

Tactic:
by

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

Goal state before:
pp: F : Type u
inst✝¹ : Field F
W : Affine F
inst✝ : DecidableEq F
⊢ Function.Injective ⇑toClass

Tactic:
by

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
x✝² x✝¹ x✝ : W.Point
⊢ toClass (x✝² + x✝¹ + x✝) = toClass (x✝² + (x✝¹ + x✝))

Tactic:
by

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
x✝¹ x✝ : W.Point
⊢ toClass (x✝¹ + x✝) = toClass (x✝ + x✝¹)

Tactic:
by

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 : 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
i : I
⊢ IsAffine ((D ⋙ Γ.rightOp ⋙ Scheme.Spec).obj i)

Tactic:
by

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
x✝ : W.Point
⊢ -x✝ + x✝ = 0

Tactic:
by

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 : 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)
⊢ ((Cone.postcompose (asIso e).hom).obj c).π ≫ inv e ≫ t = (Functor.const I).map (a ≫ Spec.map φ)

Tactic:
by

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

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

Tactic:
by

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 : 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:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ Even 2

Tactic:
by

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 : 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
⊢ (e.app i ≫ g) ≫ Spec.map φ = t.app i

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ ¬Even 3

Tactic:
by

Goal state after:
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ᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
t : D ⋙ Scheme.Spec ⟶ (Functor.const I).obj (Spec R)
a : c.pt ⟶ Spec S
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
⊢ ∀ {X Y : I} (f : X ⟶ Y),
    (((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).map f ≫
        (Iso.refl ((((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).obj Y)).hom =
      (Iso.refl ((((Functor.const Iᵒᵖ).obj R).rightOp ⋙ Scheme.Spec).obj X)).hom ≫
        ((Functor.const I).obj (Spec R)).map f

Tactic:
by

Goal state after:
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ᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
t : D ⋙ Scheme.Spec ⟶ (Functor.const I).obj (Spec R)
a : c.pt ⟶ Spec S
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
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)) ⋯
x✝¹ x✝ : Iᵒᵖ
f : x✝¹ ⟶ x✝
⊢ Spec.map (((Functor.const Iᵒᵖ).obj R).map f ≫ Spec.preimage (t.app (Opposite.unop x✝))) =
    Spec.map (Spec.preimage (t.app (Opposite.unop x✝¹)) ≫ D.leftOp.map f)

Tactic:
by

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 y₁ = (W'⁄K).negY (f x₂) (f y₂)

Tactic:
by

Goal state after:
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ᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
t : D ⋙ Scheme.Spec ⟶ (Functor.const I).obj (Spec R)
a : c.pt ⟶ Spec S
ha : c.π ≫ t = (Functor.const I).map (a ≫ Spec.map φ)
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.whiskerRight { app := fun i ↦ Spec.preimage (t.app (Opposite.unop i)), naturality := ⋯ }.rightOp
        Scheme.Spec ≫
      e.hom

Tactic:
by

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

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

Tactic:
by

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 : (W'⁄F).Point),
    (match x + y with
      | zero => 0
      | some x y h => some (f x) (f y) ⋯) =
      (match x with
        | zero => 0
        | some x y h => some (f x) (f y) ⋯) +
        match y with
        | zero => 0
        | some x y h => some (f x) (f y) ⋯

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ W.Φ (-n) = W.Φ n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (preNormEDS (W.ψ₂ ^ 4) (C W.Ψ₃) (C W.preΨ₄) n) * (mk W) (if Even n then W.ψ₂ else 1) =
    (mk W) (C (preNormEDS (W.Ψ₂Sq ^ 2) W.Ψ₃ W.preΨ₄ n)) * (mk W) (if Even n then W.ψ₂ else 1)

Tactic:
map_preNormEDS,

Goal state after:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ preNormEDS ((mk W) (W.ψ₂ ^ 4)) ((mk W) (C W.Ψ₃)) ((mk W) (C W.preΨ₄)) n * (mk W) (if Even n then W.ψ₂ else 1) =
    preNormEDS ((mk W) (C (W.Ψ₂Sq ^ 2))) ((mk W) (C W.Ψ₃)) ((mk W) (C W.preΨ₄)) n * (mk W) (if Even n then W.ψ₂ else 1)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
⊢ (mk W) (W.ψ n) = (mk W) (W.Ψ n)

Tactic:
by

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

Goal state before:
pp: 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
P : (W'⁄F).Point
⊢ (map g) ((map f) P) = (map (g.comp f)) P

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.φ 0 = 1

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.φ 1 = C X

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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ᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
a : c.pt ⟶ Spec S
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
ha : c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom = (Functor.const I).map (a ≫ Spec.map φ)
this :
  ∀ (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c) (a : c.pt ⟶ Spec S),
    c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ c', c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')) →
        ∃ i g,
          c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
hc' : ¬∃ c', c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')
inst : IsAffine c.pt
e' : (D ⋙ Scheme.Spec).op ⋙ Γ ≅ D.leftOp := D.leftOp.isoWhiskerLeft SpecΓIdentity
c' : Cone D := coneOfCoconeLeftOp ((Cocone.precompose e'.inv).obj (Γ.mapCocone c.op))
⊢ ∀ (i : Iᵒᵖ), IsAffine (Opposite.unop ((D ⋙ Scheme.Spec).op.obj i))

Tactic:
by

Goal state after:
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ᵒᵖ
c : Cone (D ⋙ Scheme.Spec)
hc : IsLimit c
inst✝¹ : ∀ (i : I), IsAffine ((D ⋙ Scheme.Spec).obj i)
a : c.pt ⟶ Spec S
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
ha : c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom = (Functor.const I).map (a ≫ Spec.map φ)
this :
  ∀ (c : Cone (D ⋙ Scheme.Spec)) (hc : IsLimit c) (a : c.pt ⟶ Spec S),
    c.π ≫ Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom = (Functor.const I).map (a ≫ Spec.map φ) →
      (∃ c', c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')) →
        ∃ i g,
          c.π.app i ≫ g = a ∧ g ≫ Spec.map φ = (Functor.whiskerRight (NatTrans.rightOp t) Scheme.Spec ≫ e.hom).app i
hc' : ¬∃ c', c = Scheme.Spec.mapCone (coneOfCoconeLeftOp c')
inst✝ : IsAffine c.pt
e' : (D ⋙ Scheme.Spec).op ⋙ Γ ≅ D.leftOp := D.leftOp.isoWhiskerLeft SpecΓIdentity
c' : Cone D := coneOfCoconeLeftOp ((Cocone.precompose e'.inv).obj (Γ.mapCocone c.op))
inst : ∀ (i : Iᵒᵖ), IsAffine (Opposite.unop ((D ⋙ Scheme.Spec).op.obj i))
i : I
⊢ c.π.app i ≫ Spec.map (t.app (Opposite.op i)) = a ≫ Spec.map φ

Tactic:
by

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

Goal state before:
pp: R : Type r
S : Type s
F : Type u
K : Type v
inst✝¹² : CommRing R
inst✝¹¹ : CommRing S
inst✝¹⁰ : Field F
inst✝⁹ : Field K
W' : Affine R
inst✝⁸ : DecidableEq F
inst✝⁷ : DecidableEq K
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
f : F →ₐ[S] K
⊢ Function.Injective ⇑(map f)

Tactic:
by

Goal state after: