mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
P : Presentation A B (Fin (Presentation.ofFinitePresentationVars A B))
  (Fin (Presentation.ofFinitePresentationRels A B)) :=
  Presentation.ofFinitePresentation A B
f : P.Ring →ₐ[A] B := IsScalarTower.toAlgHom A P.Ring B
hkerf : RingHom.ker f = Ideal.span (Set.range P.relation)
σ : B →ₐ[A] MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A ⧸ RingHom.ker f ^ 2
hsig✝ : f.kerSquareLift.comp σ = AlgHom.id A B
h : Fin (Presentation.ofFinitePresentationVars A B) → MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A
hh :
  ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), (Ideal.Quotient.mk (RingHom.ker f ^ 2)) (h i) = σ (P.val i)
hdiag : (Ideal.Quotient.mkₐ A (RingHom.ker f ^ 2)).comp (aeval h) = σ.comp (aeval P.val)
p :
  Fin (Presentation.ofFinitePresentationRels A B) →
    MvPolynomial (Fin (Presentation.ofFinitePresentationRels A B))
      (MvPolynomial (Fin (Presentation.ofFinitePresentationVars A B)) A)
homog : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (p j).IsHomogeneous 2
hp : ∀ (j : Fin (Presentation.ofFinitePresentationRels A B)), (eval P.relation) (p j) = (aeval h) (P.relation j)
hsig : ∀ (i : Fin (Presentation.ofFinitePresentationVars A B)), f (h i) = P.val i
i : Fin (Presentation.ofFinitePresentationVars A B)
⊢ h i - X i ∈ Ideal.span (Set.range P.relation)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
this✝¹ : (α : Type) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e✝ : P.dimension = n
e₀ : σ ⊕ Fin n ≃ ι :=
  ((Equiv.ofInjective P.map ⋯).sumCongr (Finite.equivFinOfCardEq ⋯).symm).trans (Equiv.Set.sumCompl (Set.range P.map))
e : MvPolynomial σ (MvPolynomial (Fin n) R) ≃ₐ[R] P.Ring :=
  (MvPolynomial.sumAlgEquiv R σ (Fin n)).symm.trans (MvPolynomial.renameEquiv R e₀)
φ : MvPolynomial (Fin n) R →ₐ[R] P.Ring :=
  (↑e).comp (IsScalarTower.toAlgHom R (MvPolynomial (Fin n) R) (MvPolynomial σ (MvPolynomial (Fin n) R)))
algInst✝¹ : Algebra (MvPolynomial (Fin n) R) P.Ring := φ.toAlgebra
algInst✝ : Algebra (MvPolynomial (Fin n) R) S := ((algebraMap P.Ring S).comp φ.toRingHom).toAlgebra
scalarTowerInst✝ : IsScalarTower (MvPolynomial (Fin n) R) P.Ring S :=
  IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap (MvPolynomial (Fin n) R) S))
this✝ : IsScalarTower R (MvPolynomial (Fin n) R) P.Ring
this : IsScalarTower R (MvPolynomial (Fin n) R) S
H :
  (MvPolynomial.aeval fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))).toRingHom =
    (algebraMap P.Ring S).comp e.toRingEquiv.toRingHom
P'✝ : Algebra.PreSubmersivePresentation (MvPolynomial (Fin n) R) S σ σ :=
  let __Generators := Algebra.Generators.ofSurjective (fun x ↦ (algebraMap P.Ring S) (e (MvPolynomial.X x))) ⋯;
  { toGenerators := __Generators, relation := ⇑e.symm ∘ P.relation, span_range_relation_eq_ker := ⋯, map := _root_.id,
    map_inj := ⋯ }
P' : Algebra.SubmersivePresentation (MvPolynomial (Fin n) R) S σ σ :=
  let __spread.0 := P'✝;
  { toPreSubmersivePresentation := __spread.0, jacobian_isUnit := ⋯ }
⊢ P'.dimension = 0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsStandardSmoothOfRelativeDimension n R S
⊢ ∃ g, g.Etale

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
n : ℕ
hf : IsStandardSmoothOfRelativeDimension n f
⊢ ∃ g, g.comp MvPolynomial.C = f ∧ g.Etale

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
⊢ ∃ A₀ B₀ x x_1, FiniteType R ↥A₀ ∧ Smooth (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Smooth A B
⊢ ∃ A₀ B₀ x x_1 x_2 x_3 x_4,
    Function.Injective ⇑(algebraMap A₀ A) ∧ FiniteType R A₀ ∧ Smooth A₀ B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[A₀] B₀)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsStandardSmooth
⊢ ∃ n g, g.comp MvPolynomial.C = f ∧ g.Etale

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
n : ℕ
inst✝ : IsStandardSmoothOfRelativeDimension n A B
ι σ : Type
w✝¹ : Finite σ
w✝ : Finite ι
P : SubmersivePresentation A B ι σ
hP : P.dimension = n
A₀ : Subalgebra R A := adjoin R P.coeffs
⊢ P.coeffs ⊆ ↑(algebraMap (↥A₀) A).range

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
n : ℕ
inst✝ : IsStandardSmoothOfRelativeDimension n A B
ι σ : Type
w✝¹ : Finite σ
w✝ : Finite ι
P : SubmersivePresentation A B ι σ
hP : P.dimension = n
A₀ : Subalgebra R A := adjoin R P.coeffs
this : P.HasCoeffs ↥A₀
⊢ adjoin R ↑⋯.toFinset = A₀

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
n : ℕ
inst✝ : IsStandardSmoothOfRelativeDimension n A B
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ IsStandardSmoothOfRelativeDimension n (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.NoetherianDescent

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
A : Type u
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : Etale A B
⊢ ∃ A₀ B₀ x x_1, A₀.FG ∧ Etale (↥A₀) B₀ ∧ Nonempty (B ≃ₐ[A] A ⊗[↥A₀] B₀)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.IsStandardSmooth
⊢ f.Smooth

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.Smooth
⊢ Locally (fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ f.Smooth ↔ Locally (fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth) f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.RingHom.LocallyStandardSmooth

Goal state before:
pp: R S : Type u
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ f.Etale ↔ IsStandardSmoothOfRelativeDimension 0 f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
ι : Type u_3
inst✝² : Field L
inst✝¹ : Field K
inst✝ : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
⊢ FormallySmooth K ↥(IntermediateField.adjoin K (Set.range v))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
ι : Type u_3
inst✝² : Field L
inst✝¹ : Field K
inst✝ : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
hb' : IntermediateField.adjoin K (Set.range v) = ⊤
⊢ FormallySmooth K L

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
ι : Type u_3
inst✝³ : Field L
inst✝² : Field K
inst✝¹ : Algebra K L
v : ι → L
hb : AlgebraicIndependent K v
inst✝ : Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range v))) L
⊢ FormallySmooth K L

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝ : Finite α
σ : Type u_5
b₀ : Module.Basis σ S P.toExtension.Cotangent
⊢ ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
s : Finset L
hs : IsTranscendenceBasis K Subtype.val
H : Algebra.IsSeparable (↥(IntermediateField.adjoin K ↑s)) L
⊢ Algebra.IsSeparable (↥(IntermediateField.adjoin K (Set.range Subtype.val))) L

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Smooth.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
ι : Type u_3
inst✝⁴ : Field L
inst✝³ : Field K
inst✝² : Algebra K L
inst✝¹ : PerfectField K
inst✝ : EssFiniteType K L
⊢ FormallySmooth K L

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝¹ : Finite α
inst✝ : Module.Free S P.toExtension.Cotangent
h✝ : Subsingleton S
⊢ Ideal.span (Set.range fun x ↦ 1) = (ofSurjective (fun i ↦ 0) ⋯).ker

Tactic:
by

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

Goal state before:
pp: n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ @Smooth = affineLocally fun {R S} [CommRing R] [CommRing S] ↦ RingHom.Smooth

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ HasRingHomProperty @Smooth fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmooth

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝¹ : Finite α
inst✝ : Module.Free S P.toExtension.Cotangent
h✝ : Subsingleton S
P' : Presentation R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) :=
  let __Generators := ofSurjective (fun i ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun x ↦ 1, span_range_relation_eq_ker := ⋯ }
this : Subsingleton P'.toExtension.Cotangent
⊢ P'.val ∘ Sum.inr = P.val

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝¹ : Finite α
inst✝ : Module.Free S P.toExtension.Cotangent
h✝ : Subsingleton S
P' : Presentation R S (Unit ⊕ α) (Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)) :=
  let __Generators := ofSurjective (fun i ↦ 0) ⋯;
  { toGenerators := __Generators, relation := fun x ↦ 1, span_range_relation_eq_ker := ⋯ }
this : Subsingleton P'.toExtension.Cotangent
⊢ ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)), default r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ Smooth f ↔
    ∀ (x : ↥X),
      ∃ U,
        ∃ (_ : IsAffineOpen U),
          ∃ V,
            ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
              (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth

Tactic:
by

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

Goal state before:
pp: n : ℕ
X Y : Scheme
f : X ⟶ Y
inst✝ : SmoothOfRelativeDimension n f
⊢ Smooth f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
α : Type u_4
P : Generators R S α
inst✝¹ : Finite α
inst✝ : Module.Free S P.toExtension.Cotangent
⊢ ∃ P' b,
    P'.val ∘ Sum.inr = P.val ∧
      ∀ (r : Unit ⊕ Fin (Module.finrank S P.toExtension.Cotangent)), b r = Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Tactic:
by

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

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
⊢ W'.negAddY P Q * (P z * Q z) ^ 2 +
        ((2 * Q y * P z * Q z ^ 3 - P y * Q z ^ 4) * 0 + (Q y * P z ^ 4 - 2 * P y * P z ^ 3 * Q z) * 0) -
      ((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 * (P x * Q z - Q x * P z) -
                    W'.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
                  P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
                Q x * P z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2) +
          P y * Q z * (P x * Q z - Q x * P z) ^ 3 +
        ((2 * Q y * P z * Q z ^ 3 - P y * Q z ^ 4) *
            (P y ^ 2 * P z + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 2 -
              (P x ^ 3 + W'.a₂ * P x ^ 2 * P z + W'.a₄ * P x * P z ^ 2 + W'.a₆ * P z ^ 3)) +
          (Q y * P z ^ 4 - 2 * P y * P z ^ 3 * Q z) *
            (Q y ^ 2 * Q z + W'.a₁ * Q x * Q y * Q z + W'.a₃ * Q y * Q z ^ 2 -
              (Q x ^ 3 + W'.a₂ * Q x ^ 2 * Q z + W'.a₄ * Q x * Q z ^ 2 + W'.a₆ * Q z ^ 3)))) =
    0

Tactic:
(rw [negAddY]; ring1)

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

Goal state before:
pp: n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ HasRingHomProperty (@SmoothOfRelativeDimension n) fun {R S} [CommRing R] [CommRing S] ↦
    Locally fun {R S} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n

Tactic:
by

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

Goal state before:
pp: n m : ℕ
X Y : Scheme
f✝ f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : Smooth f
⊢ Smooth (Scheme.Hom.resLE f V U e)

Tactic:
by

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

Goal state before:
pp: n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
hf : SmoothOfRelativeDimension n f
hg : SmoothOfRelativeDimension m g
x : ↥X
U₂ : Z.Opens
hU₂ : IsAffineOpen U₂
V₂ : Y.Opens
hV₂ : IsAffineOpen V₂
hfx₂ : f x ∈ V₂
e₂ : V₂ ≤ g ⁻¹ᵁ U₂
hf₂ : IsStandardSmoothOfRelativeDimension m (CommRingCat.Hom.hom (Scheme.Hom.appLE g U₂ V₂ e₂))
U₁' : Y.Opens
hU₁' : IsAffineOpen U₁'
V₁' : X.Opens
hV₁' : IsAffineOpen V₁'
hx₁' : x ∈ V₁'
e₁' : V₁' ≤ f ⁻¹ᵁ U₁'
hf₁' : IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U₁' V₁' e₁'))
r : ↑Γ(Y, ↑⟨V₂, hV₂⟩)
s : ↑Γ(X, ↑⟨V₁', hV₁'⟩)
hx₁ : x ∈ X.basicOpen s
e₁ : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
hf₁ :
  IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁))
e : X.basicOpen s ≤ (f ≫ g) ⁻¹ᵁ U₂
⊢ Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e =
    Scheme.Hom.appLE g U₂ V₂ e₂ ≫
      CommRingCat.ofHom (algebraMap ↑Γ(Y, V₂) ↑Γ(Y, Y.basicOpen r)) ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁

Tactic:
by

Goal state after:
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
⊢ W'.negAddY P Q * (P z * Q z) ^ 2 =
    (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 * (P x * Q z - Q x * P z) -
                W'.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
              P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
            Q x * P z * (P x * Q z - Q x * P z) ^ 2 -
          P x * Q z * (P x * Q z - Q x * P z) ^ 2) +
      P y * Q z * (P x * Q z - Q x * P z) ^ 3

Tactic:
by

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

Goal state before:
pp: n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
hf : SmoothOfRelativeDimension n f
hg : SmoothOfRelativeDimension m g
x : ↥X
⊢ ∃ U,
    ∃ (_ : IsAffineOpen U),
      ∃ V,
        ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (f ≫ g) ⁻¹ᵁ U),
          IsStandardSmoothOfRelativeDimension (n + m) (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) U V e))

Tactic:
by

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

Goal state before:
pp: n m : ℕ
X Y : Scheme
f : X ⟶ Y
hf : Smooth f
⊢ LocallyOfFinitePresentation f

Tactic:
by

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
⊢ W.negAddY P Q =
    ((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 * (P x * Q z - Q x * P z) -
                  W.a₂ * P z * Q z * (P x * Q z - Q x * P z) ^ 2 -
                P x * Q z * (P x * Q z - Q x * P z) ^ 2 -
              Q x * P z * (P x * Q z - Q x * P z) ^ 2 -
            P x * Q z * (P x * Q z - Q x * P z) ^ 2) +
        P y * Q z * (P x * Q z - Q x * P z) ^ 3) /
      (P z * Q z) ^ 2

Tactic:
by

Goal state after:
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
hFa : (aeval a) F = 0
i : ι
⊢ (Polynomial.aeval (a i)) (F.toPolynomialAdjoinImageCompl a i) = 0

Tactic:
by

Goal state after:
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 : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
⊢ a '' {i}ᶜ = Set.range fun x ↦ a ↑x

Tactic:
by

Goal state after:
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 : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
⊢ ∀ (x : ι), x ≠ i ↔ x ∈ {j | j ≠ i}

Tactic:
by

Goal state after:
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 : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
⊢ Irreducible (F.toPolynomialAdjoinImageCompl a i)

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)

Tactic:
by

Goal state after:
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
hF0 : F ≠ 0
hFa : (aeval a) F = 0
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
this : ∀ (q₁ q₂ : MvPolynomial ι k), F = q₁ * q₂ → (aeval a) q₁ = 0 → IsUnit q₁ ∨ IsUnit q₂
h₁ : ¬(aeval a) q₁ = 0
⊢ (aeval a) q₂ = 0

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P Q : Fin 3 → R
u v : R
⊢ W'.negAddY (u • P) (v • Q) = (u * v) ^ 2 * W'.negAddY P Q

Tactic:
by

Goal state after:
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
hF0 : F ≠ 0
hFa : (aeval a) F = 0
⊢ Irreducible F

Tactic:
by

Goal state after:
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 ≤ ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F).totalDegree

Tactic:
by

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

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ W'.negAddY P P = 0

Tactic:
by

Goal state after:
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
⊢ W'.negAddY P Q = P y ^ 2 * Q z * W'.negY Q

Tactic:
by

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

Goal state before:
pp: ⊢ @IsProper = @IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType

Tactic:
by

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.RespectsIso @IsProper

Tactic:
by

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderComposition @IsProper

Tactic:
by

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsMultiplicative @IsProper

Tactic:
by

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ MorphismProperty.IsStableUnderBaseChange @IsProper

Tactic:
by

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

Goal state before:
pp: X Y Z S : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget @IsProper

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
⊢ ∃ U,
    ∃ (_ : IsAffineOpen U),
      ∃ V, ∃ (_ : IsAffineOpen V) (hVU : V ≤ f ⁻¹ᵁ U), x ∈ V ∧ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).Smooth

Tactic:
by

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
⊢ IsOpen {x | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth}

Tactic:
by

Goal state after: