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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P y + 3 * P x * P x ^ 2 * P y - P y ^ 2 * P y * P z + P y * P y ^ 2 * P z +
                                W'.a₁ * P x * P y ^ 2 * P z -
                              W'.a₁ * P x * P y ^ 2 * P z -
                            W'.a₂ * P x ^ 2 * P y * P z +
                          W'.a₂ * P x ^ 2 * P y * P z +
                        2 * W'.a₂ * P x * P x * P y * P z -
                      2 * W'.a₂ * P x * P x * P y * P z -
                    W'.a₃ * P y ^ 2 * P z ^ 2 +
                  W'.a₃ * P y ^ 2 * P z ^ 2 +
                W'.a₄ * P x * P y * P z ^ 2 -
              2 * W'.a₄ * P x * P y * P z * P z +
            2 * W'.a₄ * P x * P y * P z * P z -
          W'.a₄ * P x * P y * P z ^ 2 +
        3 * W'.a₆ * P y * P z * P z ^ 2 -
      3 * W'.a₆ * P y * P z ^ 2 * P z =
    0

Tactic:
]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -3 * P x ^ 2 * P x * P y + 3 * P x * P x ^ 2 * P y - P y ^ 2 * P y * P z + P y * P y ^ 2 * P z +
                                W'.a₁ * P x * P y ^ 2 * P z -
                              W'.a₁ * P x * P y ^ 2 * P z -
                            W'.a₂ * P x ^ 2 * P y * P z +
                          W'.a₂ * P x ^ 2 * P y * P z +
                        2 * W'.a₂ * P x * P x * P y * P z -
                      2 * W'.a₂ * P x * P x * P y * P z -
                    W'.a₃ * P y ^ 2 * P z ^ 2 +
                  W'.a₃ * P y ^ 2 * P z ^ 2 +
                W'.a₄ * P x * P y * P z ^ 2 -
              2 * W'.a₄ * P x * P y * P z * P z +
            2 * W'.a₄ * P x * P y * P z * P z -
          W'.a₄ * P x * P y * P z ^ 2 +
        3 * W'.a₆ * P y * P z * P z ^ 2 -
      3 * W'.a₆ * P y * P z ^ 2 * P z =
    0
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F.totalDegree ≤ ((rename Subtype.val) (F₀.coeff (σ i))).totalDegree
⊢ σ i ≤ F.totalDegree

Tactic:
]

Goal state after:
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F.totalDegree ≤ ((rename Subtype.val) (F₀.coeff (σ i))).totalDegree
⊢ σ i ≤ F.totalDegree
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_3
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F.totalDegree ≤ ((rename Subtype.val) (F₀.coeff (σ i))).totalDegree
this : (F₀.coeff (σ i)).totalDegree + σ i ≤ F.totalDegree
⊢ False

Tactic:
]

Goal state after:
case refine_3
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F.totalDegree ≤ ((rename Subtype.val) (F₀.coeff (σ i))).totalDegree
this : (F₀.coeff (σ i)).totalDegree + σ i ≤ F.totalDegree
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : (Scheme.Opens.ι V) ⟨x, hxV⟩ ∈ X.basicOpen r
hr : Algebra.Smooth (↑Γ(Y, U)) (Localization.Away r)
⊢ x ∈ X.basicOpen r

Tactic:
]

Goal state after:
case refine_1
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : (Scheme.Opens.ι V) ⟨x, hxV⟩ ∈ X.basicOpen r
hr : Algebra.Smooth (↑Γ(Y, U)) (Localization.Away r)
⊢ x ∈ X.basicOpen r
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -3 * 0 ^ 2 * Q x * Q y + 3 * 0 * Q x ^ 2 * P y - P y ^ 2 * Q y * Q z + P y * Q y ^ 2 * 0 + W'.a₁ * 0 * Q y ^ 2 * 0 -
                              W'.a₁ * Q x * P y ^ 2 * Q z -
                            W'.a₂ * 0 ^ 2 * Q y * Q z +
                          W'.a₂ * Q x ^ 2 * P y * 0 +
                        2 * W'.a₂ * 0 * Q x * P y * Q z -
                      2 * W'.a₂ * 0 * Q x * Q y * 0 -
                    W'.a₃ * P y ^ 2 * Q z ^ 2 +
                  W'.a₃ * Q y ^ 2 * 0 ^ 2 +
                W'.a₄ * 0 * P y * Q z ^ 2 -
              2 * W'.a₄ * 0 * Q y * 0 * Q z +
            2 * W'.a₄ * Q x * P y * 0 * Q z -
          W'.a₄ * Q x * Q y * 0 ^ 2 +
        3 * W'.a₆ * P y * 0 * Q z ^ 2 -
      3 * W'.a₆ * Q y * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * (-Q y - W'.a₁ * Q x - W'.a₃ * Q z)

Tactic:
]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -3 * 0 ^ 2 * Q x * Q y + 3 * 0 * Q x ^ 2 * P y - P y ^ 2 * Q y * Q z + P y * Q y ^ 2 * 0 + W'.a₁ * 0 * Q y ^ 2 * 0 -
                              W'.a₁ * Q x * P y ^ 2 * Q z -
                            W'.a₂ * 0 ^ 2 * Q y * Q z +
                          W'.a₂ * Q x ^ 2 * P y * 0 +
                        2 * W'.a₂ * 0 * Q x * P y * Q z -
                      2 * W'.a₂ * 0 * Q x * Q y * 0 -
                    W'.a₃ * P y ^ 2 * Q z ^ 2 +
                  W'.a₃ * Q y ^ 2 * 0 ^ 2 +
                W'.a₄ * 0 * P y * Q z ^ 2 -
              2 * W'.a₄ * 0 * Q y * 0 * Q z +
            2 * W'.a₄ * Q x * P y * 0 * Q z -
          W'.a₄ * Q x * Q y * 0 ^ 2 +
        3 * W'.a₆ * P y * 0 * Q z ^ 2 -
      3 * W'.a₆ * Q y * 0 ^ 2 * Q z =
    P y ^ 2 * Q z * (-Q y - W'.a₁ * Q x - W'.a₃ * Q z)
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (IsSeparated f ∧ UniversallyClosed f) ∧ LocallyOfFiniteType f ↔
    (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (IsSeparated f ∧ UniversallyClosed f) ∧ LocallyOfFiniteType f ↔
    (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).RespectsIso

Tactic:
]

Goal state after:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).RespectsIso
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsStableUnderComposition

Tactic:
]

Goal state after:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsStableUnderComposition
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsMultiplicative

Tactic:
]

Goal state after:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsMultiplicative
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝¹ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this✝ : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
hr : (algebraMap (↑Γ(Y, U)) (Localization.Away r)).Smooth
this : IsLocalization.Away r ↑Γ(X, X.basicOpen r)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)).Smooth

Tactic:
]

Goal state after:
case refine_2
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this✝¹ : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.FinitePresentation ↑Γ(Y, U) ↑Γ(X, V)
this✝ : Algebra.IsSmoothAt (↑Γ(Y, U)) (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
r : ↑Γ(X, V)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩).asIdeal
hr : (algebraMap (↑Γ(Y, U)) (Localization.Away r)).Smooth
this : IsLocalization.Away r ↑Γ(X, X.basicOpen r)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)).Smooth
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsStableUnderBaseChange

Tactic:
]

Goal state after:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType).IsStableUnderBaseChange
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType)

Tactic:
]

Goal state after:
X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget (@IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -3 * P x ^ 2 * 0 * Q y + 3 * P x * 0 ^ 2 * P y - P y ^ 2 * Q y * 0 + P y * Q y ^ 2 * P z +
                                W'.a₁ * P x * Q y ^ 2 * P z -
                              W'.a₁ * 0 * P y ^ 2 * 0 -
                            W'.a₂ * P x ^ 2 * Q y * 0 +
                          W'.a₂ * 0 ^ 2 * P y * P z +
                        2 * W'.a₂ * P x * 0 * P y * 0 -
                      2 * W'.a₂ * P x * 0 * Q y * P z -
                    W'.a₃ * P y ^ 2 * 0 ^ 2 +
                  W'.a₃ * Q y ^ 2 * P z ^ 2 +
                W'.a₄ * P x * P y * 0 ^ 2 -
              2 * W'.a₄ * P x * Q y * P z * 0 +
            2 * W'.a₄ * 0 * P y * P z * 0 -
          W'.a₄ * 0 * Q y * P z ^ 2 +
        3 * W'.a₆ * P y * P z * 0 ^ 2 -
      3 * W'.a₆ * Q y * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * (-P y - W'.a₁ * P x - W'.a₃ * P z)

Tactic:
]

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -3 * P x ^ 2 * 0 * Q y + 3 * P x * 0 ^ 2 * P y - P y ^ 2 * Q y * 0 + P y * Q y ^ 2 * P z +
                                W'.a₁ * P x * Q y ^ 2 * P z -
                              W'.a₁ * 0 * P y ^ 2 * 0 -
                            W'.a₂ * P x ^ 2 * Q y * 0 +
                          W'.a₂ * 0 ^ 2 * P y * P z +
                        2 * W'.a₂ * P x * 0 * P y * 0 -
                      2 * W'.a₂ * P x * 0 * Q y * P z -
                    W'.a₃ * P y ^ 2 * 0 ^ 2 +
                  W'.a₃ * Q y ^ 2 * P z ^ 2 +
                W'.a₄ * P x * P y * 0 ^ 2 -
              2 * W'.a₄ * P x * Q y * P z * 0 +
            2 * W'.a₄ * 0 * P y * P z * 0 -
          W'.a₄ * 0 * Q y * P z ^ 2 +
        3 * W'.a₆ * P y * P z * 0 ^ 2 -
      3 * W'.a₆ * Q y * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * (-P y - W'.a₁ * P x - W'.a₃ * P z)
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType) =
    @IsAffineHom ⊓ (@UniversallyClosed ⊓ @LocallyOfFiniteType)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : Smooth f
⊢ ⊤ ≤ smoothLocus f

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : Smooth f
⊢ ⊤ ≤ smoothLocus f
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (@IsProper ⊓ @IsAffineHom) f ↔ IsProper f ∧ IsAffineHom f

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (@IsProper ⊓ @IsAffineHom) f ↔ IsProper f ∧ IsAffineHom f
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this : CompactSpace ↥X
⊢ UniversallyClosed f

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this : CompactSpace ↥X
⊢ UniversallyClosed f
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_1
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F₀.coeff (σ i) = 0
e : ι ≃ Option { b // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this : σ ∉ F.support
⊢ False

Tactic:
]

Goal state after:
case refine_1
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F₀.coeff (σ i) = 0
e : ι ≃ Option { b // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this : σ ∉ F.support
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↥X
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ UniversallyClosed (Spec.map (Scheme.Hom.appTop f)) ∧ IsAffineHom (Spec.map (Scheme.Hom.appTop f))

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↥X
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ UniversallyClosed (Spec.map (Scheme.Hom.appTop f)) ∧ IsAffineHom (Spec.map (Scheme.Hom.appTop f))
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : Smooth f
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.Smooth ↑Γ(Y, U) ↑Γ(X, V)
⊢ IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : Smooth f
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ ⇑f ⁻¹' U.carrier
this : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth
algInst✝ : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algebraizeInst✝ : Algebra.Smooth ↑Γ(Y, U) ↑Γ(X, V)
⊢ IsAffineOpen.primeIdealOf hV ⟨x, hxV⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
H✝ : smoothLocus f = ⊤
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V
H : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ (CommRingCat.Hom.hom (appTop (resLE f U V hVU))).Smooth

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
H✝ : smoothLocus f = ⊤
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V
H : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth
this✝ : IsAffine ↑U
this : IsAffine ↑V
⊢ (CommRingCat.Hom.hom (appTop (resLE f U V hVU))).Smooth
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X Y U : Scheme
f : U ⟶ X
g : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : LocallyOfFinitePresentation g
x : ↥U
⊢ (CommRingCat.Hom.hom (stalkMap (f ≫ g) x)).FormallySmooth ↔ x ∈ ↑(smoothLocus (f ≫ g))

Tactic:
]

Goal state after:
X Y U : Scheme
f : U ⟶ X
g : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : LocallyOfFinitePresentation g
x : ↥U
⊢ (CommRingCat.Hom.hom (stalkMap (f ≫ g) x)).FormallySmooth ↔ x ∈ ↑(smoothLocus (f ≫ g))
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this : (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).EssFiniteType
⊢ (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).FormallySmooth

Tactic:
]

Goal state after:
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this : (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).EssFiniteType
⊢ (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).FormallySmooth
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z = Q x * P z
⊢ (P y * Q z - Q y * P z) *
        ((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                  W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (Q x * P z - Q x * P z) -
                W'.a₂ * P z * Q z * (Q x * P z - Q x * P z) ^ 2 -
              Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
            Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
          Q x * P z * (Q x * P z - Q x * P z) ^ 2) +
      P y * Q z * (Q x * P z - Q x * P z) ^ 3 =
    (P y * Q z - Q y * P z) ^ 3 * (P z * Q z)

Tactic:
]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z = Q x * P z
⊢ (P y * Q z - Q y * P z) *
        ((P y * Q z - Q y * P z) ^ 2 * P z * Q z +
                  W'.a₁ * (P y * Q z - Q y * P z) * P z * Q z * (Q x * P z - Q x * P z) -
                W'.a₂ * P z * Q z * (Q x * P z - Q x * P z) ^ 2 -
              Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
            Q x * P z * (Q x * P z - Q x * P z) ^ 2 -
          Q x * P z * (Q x * P z - Q x * P z) ^ 2) +
      P y * Q z * (Q x * P z - Q x * P z) ^ 3 =
    (P y * Q z - Q y * P z) ^ 3 * (P z * Q z)
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
hFa : (aeval a) F = 0
i : ι
hi : i ∈ F.vars
σ : ι →₀ ℕ
hσ : σ ∈ F.support
hσi : i ∈ σ.support
h : F.toPolynomialAdjoinImageCompl a i = 0
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W.negAddY P Q = W.negAddY P Q

Tactic:
]

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

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ n / d *
        ((n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                  Q x * P z * d ^ 2) *
                d /
              (P z * Q z) ^ 2 /
            (d ^ 3 / (P z * Q z)) -
          P x / P z) +
      P y / P z =
    (n *
            (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                Q x * P z * d ^ 2 -
              P x * Q z * d ^ 2) +
          P y * Q z * d ^ 3) /
        (P z * Q z) ^ 2 /
      (d ^ 3 / (P z * Q z))

Tactic:
]

Goal state after:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ n / d *
        ((n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                  Q x * P z * d ^ 2) *
                d /
              (P z * Q z) ^ 2 /
            (d ^ 3 / (P z * Q z)) -
          P x / P z) +
      P y / P z =
    (n *
            (n ^ 2 * P z * Q z + W.a₁ * n * P z * Q z * d - W.a₂ * P z * Q z * d ^ 2 - P x * Q z * d ^ 2 -
                Q x * P z * d ^ 2 -
              P x * Q z * d ^ 2) +
          P y * Q z * d ^ 3) /
        (P z * Q z) ^ 2 /
      (d ^ 3 / (P z * Q z))