mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ degBound k D (n + 1) = numBound k D (n + 1) ^ numBound k D (n + 1) * degBound k D n

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 3
⊢ W.j = ↑W.Δ'⁻¹ * W.b₂ ^ 6

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound k D (n + 1) = numBound k D n * degBound k D n * D n

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
⊢ degBound k₀ (fun t ↦ Nat.casesOn t k D) (0 + 1) = (k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 3
⊢ W.j = 0 ↔ W.b₂ ^ 6 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 3
h : W.b₂ = 0
⊢ W.j = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
W : WeierstrassCurve R
inst✝² : W.IsElliptic
inst✝¹ : CharP R 3
inst✝ : IsReduced R
⊢ W.j = 0 ↔ W.b₂ = 0

Tactic:
by

Goal state after:
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).IsElliptic

Tactic:
by

Goal state after:
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).Δ' = f ↑W.Δ'

Tactic:
by

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

Goal state after:
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).Δ'⁻¹ = f ↑W.Δ'⁻¹

Tactic:
by

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

Goal state after:
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).j = f W.j

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
x : ↥(D.obj i)
⊢ ∃ U, ∃ (_ : IsAffineOpen U) (_ : x ∈ U), ∃ j f, (ConcreteCategory.hom (Scheme.Hom.app (D.map f) U)) ((s |_ U) ⋯) = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ degBound k₀ (fun t ↦ Nat.casesOn t k D) (n + 1 + 1) =
    (k₀ * k) ^ (k₀ * k) * degBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
⊢ numBound k₀ (fun x ↦ Nat.casesOn x k D) (0 + 1) = numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) 0

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ W.polynomial =
    { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly,
        d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
⊢ W.polynomial ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₀ k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ numBound k₀ (fun x ↦ Nat.casesOn x k D) (n + 1 + 1) = numBound (k₀ * k) ((k₀ * k) ^ (k₀ * k) • D) (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
hD : ∀ i < 0, D₁ i ≤ D₂ i
⊢ degBound k₁ D₁ 0 ≤ degBound k₂ D₂ 0

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
⊢ W.polynomial.degree = 2

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ degBound k₁ D₁ (n + 1) ≤ degBound k₂ D₂ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
hD : ∀ i < 0, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ 0 ≤ numBound k₂ D₂ 0

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : Nontrivial R
⊢ W.polynomial.natDegree = 2

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ W.polynomial.Monic

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k₁ k₂ : ℕ
D₁ D₂ : ℕ → ℕ
hk : k₁ ≤ k₂
n : ℕ
hD : ∀ i < n + 1, D₁ i ≤ D₂ i
⊢ numBound k₁ D₁ (n + 1) ≤ numBound k₂ D₂ (n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k : ℕ
D : ℕ → ℕ
⊢ 0 < degBound k D 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity

Goal state before:
pp: k : ℕ
D : ℕ → ℕ
n : ℕ
⊢ 0 < degBound k D (n + 1)

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
t : Finset ↥(D.obj i)
ht : ⋃ x ∈ t, ↑(U x) = ⊤
x : ↥t
⊢ i ∈ insert i (Finset.image j t)

Tactic:
by

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C✝ C' C : VariableChange R
⊢ C⁻¹ * C = 1

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
t : Finset ↥(D.obj i)
ht : ⋃ x ∈ t, ↑(U x) = ⊤
⊢ Finset
    ((X : I) ×' (Y : I) ×' (_ : X ∈ insert i (Finset.image j t)) ×' (_ : Y ∈ insert i (Finset.image j t)) ×' (X ⟶ Y))

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
t : Finset ↥(D.obj i)
ht : ⋃ x ∈ t, ↑(U x) = ⊤
k : I
fk : {X : I} → X ∈ insert i (Finset.image j t) → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ insert i (Finset.image j t)) (mY : Y ∈ insert i (Finset.image j t)) {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ Finset.image (fun x ↦ ⟨j ↑x, ⟨i, ⟨⋯, ⟨⋯, f ↑x⟩⟩⟩⟩) t.attach → fk mX ≫ f_1 = fk mY
⊢ i ∈ insert i (Finset.image j t)

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
t : Finset ↥(D.obj i)
ht : ⋃ x ∈ t, ↑(U x) = ⊤
k : I
fk : {X : I} → X ∈ insert i (Finset.image j t) → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ insert i (Finset.image j t)) (mY : Y ∈ insert i (Finset.image j t)) {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ Finset.image (fun x ↦ ⟨j ↑x, ⟨i, ⟨⋯, ⟨⋯, f ↑x⟩⟩⟩⟩) t.attach → fk mX ≫ f_1 = fk mY
x : ↥(D.obj k)
⊢ i ∈ insert i (Finset.image j t)

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
t : Finset ↥(D.obj i)
ht : ⋃ x ∈ t, ↑(U x) = ⊤
k : I
fk : {X : I} → X ∈ insert i (Finset.image j t) → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ insert i (Finset.image j t)) (mY : Y ∈ insert i (Finset.image j t)) {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ Finset.image (fun x ↦ ⟨j ↑x, ⟨i, ⟨⋯, ⟨⋯, f ↑x⟩⟩⟩⟩) t.attach → fk mX ≫ f_1 = fk mY
x : ↥(D.obj k)
l : ↥(D.obj i)
hl : l ∈ t
hlU : (D.map (fk ⋯)) x ∈ ↑(U l)
⊢ i ∈ insert i (Finset.image j t)

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
t : Finset ↥(D.obj i)
ht : ⋃ x ∈ t, ↑(U x) = ⊤
k : I
fk : {X : I} → X ∈ insert i (Finset.image j t) → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ insert i (Finset.image j t)) (mY : Y ∈ insert i (Finset.image j t)) {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ Finset.image (fun x ↦ ⟨j ↑x, ⟨i, ⟨⋯, ⟨⋯, f ↑x⟩⟩⟩⟩) t.attach → fk mX ≫ f_1 = fk mY
x : ↥(D.obj k)
l : ↥(D.obj i)
hl : l ∈ t
hlU : (D.map (fk ⋯)) x ∈ ↑(U l)
⊢ ⟨l, hl⟩ ∈ t.attach

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
inst✝ : IsDomain R
⊢ Irreducible W.polynomial

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
t : Finset ↥(D.obj i)
ht : ⋃ x ∈ t, ↑(U x) = ⊤
k : I
fk : {X : I} → X ∈ insert i (Finset.image j t) → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ insert i (Finset.image j t)) (mY : Y ∈ insert i (Finset.image j t)) {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ Finset.image (fun x ↦ ⟨j ↑x, ⟨i, ⟨⋯, ⟨⋯, f ↑x⟩⟩⟩⟩) t.attach → fk mX ≫ f_1 = fk mY
x : ↥(D.obj k)
l : ↥(D.obj i)
hl : l ∈ t
hlU : (D.map (fk ⋯)) x ∈ ↑(U l)
⊢ ⟨j ↑⟨l, hl⟩, ⟨i, ⟨⋯, ⟨⋯, f ↑⟨l, hl⟩⟩⟩⟩⟩ = ⟨j l, ⟨i, ⟨⋯, ⟨⋯, f l⟩⟩⟩⟩

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ evalEval x y W.polynomial = y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ evalEval 0 0 W.polynomial = -W.a₆

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y = x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ W.Equation 0 0 ↔ W.a₆ = 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
U : ↥(D.obj i) → (D.obj i).Opens
hU : ∀ (x : ↥(D.obj i)), IsAffineOpen (U x)
hxU : ∀ (x : ↥(D.obj i)), x ∈ U x
j : ↥(D.obj i) → I
f : (x : ↥(D.obj i)) → j x ⟶ i
H : ∀ (x : ↥(D.obj i)), (ConcreteCategory.hom (Scheme.Hom.app (D.map (f x)) (U x))) ((s |_ U x) ⋯) = 0
t : Finset ↥(D.obj i)
ht : ⋃ x ∈ t, ↑(U x) = ⊤
k : I
fk : {X : I} → X ∈ insert i (Finset.image j t) → (k ⟶ X)
hk :
  ∀ {X Y : I} (mX : X ∈ insert i (Finset.image j t)) (mY : Y ∈ insert i (Finset.image j t)) {f_1 : X ⟶ Y},
    ⟨X, ⟨Y, ⟨mX, ⟨mY, f_1⟩⟩⟩⟩ ∈ Finset.image (fun x ↦ ⟨j ↑x, ⟨i, ⟨⋯, ⟨⋯, f ↑x⟩⟩⟩⟩) t.attach → fk mX ≫ f_1 = fk mY
x : ↥(D.obj k)
l : ↥(D.obj i)
hl : l ∈ t
hlU : (D.map (fk ⋯)) x ∈ ↑(U l)
h₁ : fk ⋯ = fk ⋯ ≫ f l
⊢ D.map (fk ⋯) ⁻¹ᵁ U l ≤ D.map (fk ⋯) ⁻¹ᵁ D.map (f l) ⁻¹ᵁ U l

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ↔ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Equation 0 0

Tactic:
rw [equation_iff', ← neg_eq_zero, equation_zero, variableChange_a₆, inv_one, Units.val_one]

Goal state after:
R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ -(y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆)) = 0 ↔
    1 ^ 6 *
        (W.a₆ + { u := 1, r := x, s := 0, t := y }.r * W.a₄ + { u := 1, r := x, s := 0, t := y }.r ^ 2 * W.a₂ +
                { u := 1, r := x, s := 0, t := y }.r ^ 3 -
              { u := 1, r := x, s := 0, t := y }.t * W.a₃ -
            { u := 1, r := x, s := 0, t := y }.t ^ 2 -
          { u := 1, r := x, s := 0, t := y }.r * { u := 1, r := x, s := 0, t := y }.t * W.a₁) =
      0
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ↔ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Equation 0 0

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Equation x y ↔ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Equation 0 0

Tactic:
by
  rw [equation_iff', ← neg_eq_zero, equation_zero, variableChange_a₆, inv_one, Units.val_one]
  congr! 1
  ring1

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ evalEval x y W.polynomialX = W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄)

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ evalEval 0 0 W.polynomialX = -W.a₄

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ evalEval x y W.polynomialY = 2 * y + W.a₁ * x + W.a₃

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ evalEval 0 0 W.polynomialY = W.a₃

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Nonsingular x y ↔ W.Equation x y ∧ (W.a₁ * y - (3 * x ^ 2 + 2 * W.a₂ * x + W.a₄) ≠ 0 ∨ 2 * y + W.a₁ * x + W.a₃ ≠ 0)

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Nonsingular x y ↔ W.Equation x y ∧ (W.a₁ * y ≠ 3 * x ^ 2 + 2 * W.a₂ * x + W.a₄ ∨ y ≠ -y - W.a₁ * x - W.a₃)

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
⊢ W.Nonsingular 0 0 ↔ W.a₆ = 0 ∧ (W.a₃ ≠ 0 ∨ W.a₄ ≠ 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
inst✝ : CompactSpace ↥(D.obj i)
s : ↑Γ(D.obj i, ⊤)
hs : (ConcreteCategory.hom (Scheme.Hom.appTop (c.π.app i))) s = 0
⊢ ∃ j f, (ConcreteCategory.hom (Scheme.Hom.appTop (D.map f))) s = 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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
⊢ IsCompact ↑(D.map (Over.mk (𝟙 i)).hom ⁻¹ᵁ U)

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
this : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
⊢ (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
⊢ W.Nonsingular x y ↔ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)).Nonsingular 0 0

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
hΔ : Δ W ≠ 0
⊢ W.Equation 0 0 ↔ W.Nonsingular 0 0

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
hΔ : Δ W ≠ 0
⊢ Δ (toAffine ({ u := 1, r := x, s := 0, t := y } • W)) ≠ 0

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W : Affine R
x y : R
hΔ : Δ W ≠ 0
⊢ W.Equation x y ↔ W.Nonsingular x y

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W.map f).polynomial = Polynomial.map (mapRingHom f) W.polynomial

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
x y : R
h : W.Equation x y
⊢ (W.map f).Equation (f x) (f y)

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ⇑f
x y : R
⊢ (W.map f).Equation (f x) (f y) ↔ W.Equation x y

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W.map f).polynomialX = Polynomial.map (mapRingHom f) W.polynomialX

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 j : I} (f : i ⟶ j), IsAffineHom (D.map f)
i : I
U : (D.obj i).Opens
hU : IsCompact ↑U
s : ↑Γ(D.obj i, U)
hs : (ConcreteCategory.hom (Scheme.Hom.app (c.π.app i) U)) s = 0
this : CompactSpace ↥((opensDiagram D i U).obj (Over.mk (𝟙 i)))
H : (D.map (𝟙 i) ⁻¹ᵁ U).ι ''ᵁ ⊤ ≤ U
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop ((opensCone D c i U).π.app (Over.mk (𝟙 i)))))
      ((ConcreteCategory.hom ((D.obj i).presheaf.map (homOfLE ⋯).op)) s) =
    0

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
⊢ (W.map f).polynomialY = Polynomial.map (mapRingHom f) W.polynomialY

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W : Affine R
S : Type s
inst✝ : CommRing S
f : R →+* S
hf : Function.Injective ⇑f
x y : R
⊢ (W.map f).Nonsingular (f x) (f y) ↔ W.Nonsingular x y

Tactic:
by

Goal state after: