mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : P.σ g ^ n * ↑x ∈ P.ker ^ 2
⊢ ⟨g ^ n, ⋯⟩ • Extension.Cotangent.mk x = 0

Tactic:
]

Goal state after:
case h
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : P.σ g ^ n * ↑x ∈ P.ker ^ 2
⊢ ⟨g ^ n, ⋯⟩ • Extension.Cotangent.mk x = 0
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 * 0 + 3 * P x * 0 ^ 2 * P z + P y ^ 2 * 0 ^ 2 - Q y ^ 2 * P z ^ 2 + W'.a₁ * P x * P y * 0 ^ 2 -
                  W'.a₁ * 0 * Q y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * 0 ^ 2 +
              W'.a₂ * 0 ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * 0 ^ 2 -
          W'.a₃ * Q y * P z ^ 2 * 0 -
        W'.a₄ * P x * P z * 0 ^ 2 +
      W'.a₄ * 0 * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * 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 * 0 + 3 * P x * 0 ^ 2 * P z + P y ^ 2 * 0 ^ 2 - Q y ^ 2 * P z ^ 2 + W'.a₁ * P x * P y * 0 ^ 2 -
                  W'.a₁ * 0 * Q y * P z ^ 2 -
                W'.a₂ * P x ^ 2 * 0 ^ 2 +
              W'.a₂ * 0 ^ 2 * P z ^ 2 +
            W'.a₃ * P y * P z * 0 ^ 2 -
          W'.a₃ * Q y * P z ^ 2 * 0 -
        W'.a₄ * P x * P z * 0 ^ 2 +
      W'.a₄ * 0 * P z ^ 2 * 0 =
    -(Q y ^ 2 * P z) * P z
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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ W'.addZ P Q * (P z * Q z) = 0

Tactic:
addZ_eq' hP hQ,

Goal state after:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
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
⊢ (P x * Q z - Q x * P z) ^ 3 = 0
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
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
⊢ 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
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ ¬P x * Q z = Q x * P z

Tactic:
]

Goal state after:
F : Type u
inst✝¹ : Field F
W : Projective F
inst✝ : DecidableEq F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ ¬P x * Q z = Q x * P z
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: case h
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : P.σ g ^ n * ↑x ∈ P.ker ^ 2
⊢ ↑(P.σ g ^ n • x) ∈ P.toExtension.ker ^ 2

Tactic:
]

Goal state after:
case h
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
n : ℕ
hm : P.σ g ^ n * ↑x ∈ P.ker ^ 2
⊢ ↑(P.σ g ^ n • x) ∈ P.toExtension.ker ^ 2
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
⊢ (compLocalizationAwayAlgHom T g P) (((localizationAway T g).toComp P).toAlgHom ↑x) = 0

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
Q : Generators S T Unit := localizationAway T g
algInst✝ : Algebra P.Ring ((localizationAway T g).comp P).Ring := ((localizationAway T g).toComp P).toAlgHom.toAlgebra
f : P.Ring ⧸ P.ker ^ 2 := (Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)
π : ((localizationAway T g).comp P).Ring →ₐ[R] Localization.Away ((Ideal.Quotient.mk (P.ker ^ 2)) (P.σ g)) :=
  compLocalizationAwayAlgHom T g P
x : ↥P.toExtension.ker
hx :
  (lift
        (↑S
          (↑(LinearMap.ringLmapEquivSelf T T (P.toExtension.Cotangent →ₗ[S] (Q.comp P).toExtension.Cotangent)).symm
            (Extension.Cotangent.map (Q.toComp P).toExtensionHom))))
      (((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x)) =
    0
⊢ (compLocalizationAwayAlgHom T g P) (((localizationAway T g).toComp P).toAlgHom ↑x) = 0
Module: Mathlib.RingTheory.Extension.Cotangent.LocalizationAway

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
ι : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
g : S
inst✝ : IsLocalization.Away g T
P : Generators R S ι
x : ((localizationAway T g).comp P).toExtension.Cotangent
⊢ x = x

Tactic:
]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Algebra.Etale R S ↔ Algebra.Etale R S

Tactic:
]

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

Goal state before:
pp: x✝⁴ : Type u_6
x✝³ : Type u_5
x✝² : CommRing x✝⁴
x✝¹ : CommRing x✝³
x✝ : x✝⁴ →+* x✝³
⊢ x✝.FormallyUnramified ∧ x✝.Smooth ↔ x✝.FormallyUnramified ∧ x✝.Smooth

Tactic:
]

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

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FormallyUnramified ∧ f.Smooth
⊢ f.FormallyUnramified

Tactic:
]

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : f.FormallyUnramified ∧ f.Smooth
⊢ f.FormallyUnramified
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ f.FormallyUnramified ∧ f.Smooth

Tactic:
]

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ f.FormallyUnramified ∧ f.Smooth
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: ⊢ IsStableUnderBaseChange fun {R S} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun R S x x_1 f ↦ f.FormallyUnramified ∧ f.Smooth) R S inst inst_1

Tactic:
]

Goal state after:
⊢ IsStableUnderBaseChange fun {R S} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun R S x x_1 f ↦ f.FormallyUnramified ∧ f.Smooth) R S inst inst_1
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: ⊢ PropertyIsLocal fun {R S} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun R S x x_1 f ↦ f.FormallyUnramified ∧ f.Smooth) R S inst inst_1

Tactic:
]

Goal state after:
⊢ PropertyIsLocal fun {R S} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun R S x x_1 f ↦ f.FormallyUnramified ∧ f.Smooth) R S inst inst_1
Module: Mathlib.RingTheory.RingHom.Etale

Goal state before:
pp: ⊢ StableUnderComposition fun {R S} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun R S x x_1 f ↦ f.FormallyUnramified ∧ f.Smooth) R S inst inst_1

Tactic:
]

Goal state after:
⊢ StableUnderComposition fun {R S} [inst : CommRing R] [inst_1 : CommRing S] ↦
    (fun R S x x_1 f ↦ f.FormallyUnramified ∧ f.Smooth) R S inst inst_1
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
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
i : σ
⊢ (Subtype.val ∘ D.f ∘ ⇑b) i ∈ ↑(RingHom.ker (aeval P.val))

Tactic:
simpa only [Generators.toExtension_Ring, Generators.toExtension_commRing, Function.comp_apply,
    SetLike.mem_coe, RingHom.mem_ker, ← P.algebraMap_apply] using (D.f _).property

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

Goal state before:
pp: case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.g - 1 ∈ RingHom.ker (algebraMap P.Ring S)

Tactic:
]

Goal state after:
case refine_3
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
σ✝ : Type u_3
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
⊢ D.g - 1 ∈ RingHom.ker (algebraMap P.Ring S)
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.addX P Q = W.addX P Q

Tactic:
]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Algebra.IsStandardSmooth R S ↔ Algebra.IsStandardSmooth R S

Tactic:
]

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
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R S ↔ Algebra.IsStandardSmoothOfRelativeDimension n R S

Tactic:
]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
⊢ Algebra.IsStandardSmooth R T

Tactic:
]

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : g.IsStandardSmooth
hf : f.IsStandardSmooth
⊢ Algebra.IsStandardSmooth R T
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n m : ℕ
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
⊢ Algebra.IsStandardSmoothOfRelativeDimension (n + m) R T

Tactic:
]

Goal state after:
n m : ℕ
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
⊢ Algebra.IsStandardSmoothOfRelativeDimension (n + m) R T
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (0 + n) (e.toRingHom.comp f)

Tactic:
]

Goal state after:
n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : R →+* S
e : S ≃+* T
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (0 + n) (e.toRingHom.comp f)
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (n + 0) (f.comp e.toRingHom)

Tactic:
]

Goal state after:
n : ℕ
R S T : Type u_2
x✝² : CommRing R
x✝¹ : CommRing S
x✝ : CommRing T
f : S →+* T
e : R ≃+* S
hf : IsStandardSmoothOfRelativeDimension n f
⊢ IsStandardSmoothOfRelativeDimension (n + 0) (f.comp e.toRingHom)
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
⊢ Algebra.IsStandardSmooth R T

Tactic:
]

Goal state after:
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
⊢ Algebra.IsStandardSmooth R T
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
⊢ Algebra.IsStandardSmooth S (S ⊗[R] T)

Tactic:
]

Goal state after:
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmooth R T
this : Algebra.IsStandardSmooth S (S ⊗[R] T)
⊢ Algebra.IsStandardSmooth S (S ⊗[R] T)
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R T

Tactic:
]

Goal state after:
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
⊢ Algebra.IsStandardSmoothOfRelativeDimension n R T
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)

Tactic:
]

Goal state after:
n : ℕ
R S T : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Algebra.IsStandardSmoothOfRelativeDimension n R T
this : Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
⊢ Algebra.IsStandardSmoothOfRelativeDimension n S (S ⊗[R] T)
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
D : DescentAux A B
⊢ D.P.coeffs ⊆ ↑(subalgebra R D)

Tactic:
]

Goal state after:
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
D : DescentAux A B
⊢ D.P.coeffs ⊆ ↑(subalgebra R D)
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
r✝ : R
x✝ : Rᵣ
⊢ (have I := (algebraMap R Rᵣ).toAlgebra;
    r✝ • x✝) =
    (algebraMap R Rᵣ) r✝ * x✝

Tactic:
]

Goal state after:
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
r✝ : R
x✝ : Rᵣ
⊢ (have I := (algebraMap R Rᵣ).toAlgebra;
    r✝ • x✝) =
    (algebraMap R Rᵣ) r✝ * x✝
Module: Mathlib.RingTheory.RingHom.StandardSmooth

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
this : (algebraMap R Rᵣ).toAlgebra = inst✝¹
⊢ Algebra.IsStandardSmoothOfRelativeDimension 0 R Rᵣ

Tactic:
]

Goal state after:
R : Type u
inst✝³ : CommRing R
Rᵣ : Type u_2
inst✝² : CommRing Rᵣ
inst✝¹ : Algebra R Rᵣ
r : R
inst✝ : IsLocalization.Away r Rᵣ
this : (algebraMap R Rᵣ).toAlgebra = inst✝¹
⊢ Algebra.IsStandardSmoothOfRelativeDimension 0 R Rᵣ
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
D : DescentAux A B
i : D.vars
this : ↑(D.h i).coeffs ⊆ ⋃ i, ↑(D.h i).coeffs
⊢ ↑(D.h i).coeffs ⊆ ↑(subalgebra R D)

Tactic:
]

Goal state after:
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
D : DescentAux A B
i : D.vars
this : ↑(D.h i).coeffs ⊆ ⋃ i, ↑(D.h i).coeffs
⊢ ↑(D.h i).coeffs ⊆ ↑(subalgebra R D)
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
⊢ Nat.card ι - Nat.card σ = Nat.card ι - Nat.card σ

Tactic:
]

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
D : DescentAux A B
i : D.rels
p : MvPolynomial D.vars A
hp : p ∈ ↑(D.p i).coeffs
this : ↑p.coeffs ⊆ ⋃ i, ⋃ x ∈ (D.p i).coeffs, ↑x.coeffs
⊢ ↑p.coeffs ⊆ ↑(subalgebra R D)

Tactic:
]

Goal state after:
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
D : DescentAux A B
i : D.rels
p : MvPolynomial D.vars A
hp : p ∈ ↑(D.p i).coeffs
this : ↑p.coeffs ⊆ ⋃ i, ⋃ x ∈ (D.p i).coeffs, ↑x.coeffs
⊢ ↑p.coeffs ⊆ ↑(subalgebra R D)
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

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

Tactic:
]

Goal state after:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ -P x * P y ^ 2 * P z + P x * P y ^ 2 * P z - 2 * P x * P y * P y * P z + 2 * P x * P y * P y * P z -
                            W'.a₁ * P x ^ 2 * P y * P z +
                          W'.a₁ * P x ^ 2 * P y * P z +
                        W'.a₂ * P x ^ 2 * P x * P z -
                      W'.a₂ * P x * P x ^ 2 * P z -
                    W'.a₃ * P x * P y * 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 ^ 2 * P z ^ 2 -
          W'.a₄ * P x ^ 2 * P z ^ 2 +
        3 * W'.a₆ * P x * P z * P z ^ 2 -
      3 * W'.a₆ * P x * P z ^ 2 * P z =
    0
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
D : DescentAux A B
i : D.vars
q : MvPolynomial D.vars A
hq : q ∈ ↑(D.q i).coeffs
this : ↑q.coeffs ⊆ ⋃ i, ⋃ x ∈ (D.q i).coeffs, ↑(coeffs x)
⊢ ↑q.coeffs ⊆ ↑(subalgebra R D)

Tactic:
]

Goal state after:
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
D : DescentAux A B
i : D.vars
q : MvPolynomial D.vars A
hq : q ∈ ↑(D.q i).coeffs
this : ↑q.coeffs ⊆ ⋃ i, ⋃ x ∈ (D.q i).coeffs, ↑(coeffs x)
⊢ ↑q.coeffs ⊆ ↑(subalgebra R D)