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

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_5
P : Generators R S ι
v : κ → ι
h : LinearIndependent S fun k ↦ (D R S) (P.val (v k))
hx : (Finsupp.sum 0 fun a b ↦ b • (D R S) (P.val (v a))) = 0
⊢ (Finsupp.sum 0 fun i a ↦ a • P.cotangentSpaceBasis (v i)) = 0

Tactic:
simp

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

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
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth R (Localization.Away g)
⊢ (Ideal.map (algebraMap S (Localization.Away g)) p).IsPrime

Tactic:
apply IsLocalization.isPrime_of_isPrime_disjoint (.powers g) _ _ ‹_›

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : FinitePresentation R S
p : Ideal S
inst✝¹ : p.IsPrime
inst✝ : IsSmoothAt R p
this :
  ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
    [FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [IsSmoothAt R p],
    Smooth R S → ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
h : ¬Smooth R S
g : S
hg : g ∉ p
hsm : Smooth R (Localization.Away g)
⊢ Disjoint ↑(Submonoid.powers g) ↑p
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
h : (algebraMap P.Ring (Localization.Away f)) ↑x = 0
⊢ ((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk x) = 0

Tactic:
rw [IsScalarTower.algebraMap_apply _ (P.Ring ⧸ P.ker ^ 2) _,
      IsLocalization.map_eq_zero_iff (Submonoid.powers f) (Localization.Away f)] at h

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
h : ∃ m, ↑m * (algebraMap P.Ring (P.Ring ⧸ P.ker ^ 2)) ↑x = 0
⊢ ((TensorProduct.mk S T P.toExtension.Cotangent) 1) (Extension.Cotangent.mk 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 ι
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 = (algebraMap P.Ring S) (P.σ g)

Tactic:
simp

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
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : ↥D.presLeft.toExtension.ker
⊢ Extension.Cotangent.mk ⟨D.fhom.toExtensionHom.toRingHom ↑x, ⋯⟩ = Extension.Cotangent.mk ⟨↑x, ⋯⟩

Tactic:
Hom.toExtensionHom_toRingHom,

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
x : ↥D.presLeft.toExtension.ker
⊢ Extension.Cotangent.mk ⟨D.fhom.toAlgHom.toRingHom ↑x, ⋯⟩ = Extension.Cotangent.mk ⟨↑x, ⋯⟩
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case e_6.h1
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ (if -1 = 0 then 0 else if -1 = -1 then -1 else Function.surjInv ⋯ (-1)) = -1

Tactic:
simp

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

Goal state before:
pp: case e_6.h0
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
ι : Type u_4
P : Generators R S ι
σ : Type u_5
b : Module.Basis σ S P.toExtension.Cotangent
D : Aux P b
inst✝ : Nontrivial S
this : Nontrivial (MvPolynomial ι R ⧸ Ideal.span (Set.range (Subtype.val ∘ D.f ∘ ⇑b)))
⊢ (if 0 = 0 then 0 else if 0 = -1 then -1 else Function.surjInv ⋯ 0) = 0

Tactic:
simp

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
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
h : ∃ p', p'.IsHomogeneous 1 ∧ (eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) p' = p i - X i
⊢ (((Ideal.Quotient.mkₐ (↥(subalgebra R D))
                  (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))).kerSquareLift.comp
            (Ideal.Quotient.liftₐ (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))
              ((Ideal.Quotient.mkₐ (↥(subalgebra R D))
                    (RingHom.ker
                        (Ideal.Quotient.mkₐ (↥(subalgebra R D))
                          (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))) ^
                      2)).comp
                (aeval p))
              ⋯)).comp
        (Ideal.Quotient.mkₐ (↥(subalgebra R D))
          (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))))
      (X i) =
    ((AlgHom.id (↥(subalgebra R D)) (Presentation.ModelOfHasCoeffs ↥(subalgebra R D))).comp
        (Ideal.Quotient.mkₐ (↥(subalgebra R D))
          (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D))))))
      (X i)

Tactic:
apply (Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mpr

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
p : D.vars → MvPolynomial D.vars ↥(subalgebra R D)
hp : ∀ (i : D.vars), (MvPolynomial.map (algebraMap (↥(subalgebra R D)) A)) (p i) = D.h i
hf₀ :
  Function.Surjective
    ⇑(Ideal.Quotient.mkₐ (↥(subalgebra R D))
        (Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))))
i : D.vars
h : ∃ p', p'.IsHomogeneous 1 ∧ (eval (Presentation.relationOfHasCoeffs ↥(subalgebra R D))) p' = p i - X i
⊢ ↑(aeval p) (X i) - X i ∈ Ideal.span (Set.range (Presentation.relationOfHasCoeffs ↥(subalgebra R D)))
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)
j : Fin (Presentation.ofFinitePresentationRels A B)
⊢ σ ((aeval P.val) (P.relation j)) = 0

Tactic:
simp

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
h✝ : Nontrivial S
f : P.toExtension.Cotangent → ↥P.toExtension.ker
hf : ∀ (b : P.toExtension.Cotangent), Extension.Cotangent.mk (f b) = b
v : σ → ↥P.ker := fun i ↦ f (b₀ i)
J : Ideal P.Ring := Ideal.span (Set.range (Subtype.val ∘ v))
hJfg : P.ker.FG
hJ : J ≤ P.ker
⊢ P.ker ≤ (Submodule.subtype P.ker).range

Tactic:
simp

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

Goal state before:
pp: case e'_1
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
x✝ : L
⊢ Set.range Subtype.val = ↑s

Tactic:
simp

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

Goal state before:
pp: case e'_3.e'_2
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
e_1✝ : ↥(IntermediateField.adjoin K (Set.range Subtype.val)) = ↥(IntermediateField.adjoin K ↑s)
⊢ Set.range Subtype.val = ↑s

Tactic:
simp

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

Goal state before:
pp: case e'_5
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
e_1✝ : ↥(IntermediateField.adjoin K (Set.range Subtype.val)) = ↥(IntermediateField.adjoin K ↑s)
e_3✝ :
  (IntermediateField.adjoin K (Set.range Subtype.val)).toField.toCommRing ≍
    (IntermediateField.adjoin K ↑s).toField.toCommRing
⊢ Set.range Subtype.val = ↑s

Tactic:
simp

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
x✝ : K
⊢ x✝ ∈ a '' {i}ᶜ ↔ x✝ ∈ Set.range fun x ↦ a ↑x

Tactic:
simp

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

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

Goal state before:
pp: X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↥X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this✝ : Field ↑Γ(Spec (CommRingCat.of K), ⊤) := ⋯.toField
this : Field ↑Γ(X, ⊤) := ⋯.toField
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

Tactic:
have : Nonempty U := ⟨⟨x, hxU⟩⟩

Goal state after:
X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↥X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this✝¹ : Field ↑Γ(Spec (CommRingCat.of K), ⊤) := ⋯.toField
this✝ : Field ↑Γ(X, ⊤) := ⋯.toField
this : Nonempty ↥↑U
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: X : Scheme
K : Type u
inst✝³ : Field K
f : X ⟶ Spec (CommRingCat.of K)
inst✝² : IsIntegral X
inst✝¹ : UniversallyClosed f
inst✝ : LocallyOfFiniteType f
x : ↥X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
this✝¹ : Field ↑Γ(Spec (CommRingCat.of K), ⊤) := ⋯.toField
this✝ : Field ↑Γ(X, ⊤) := ⋯.toField
this : Nonempty ↥↑U
⊢ U ≤ f ⁻¹ᵁ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_2
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
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H :
  (Algebra.adjoin k (a '' {i}ᶜ)).val
      ((aeval fun j ↦ ⟨a ↑j, ⋯⟩)
        (((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)).coeff (σ i))) =
    0
i✝ : { b // b ≠ i }
⊢ ((aeval a).comp (rename Subtype.val)) (X i✝) =
    ((Algebra.adjoin k (a '' {i}ᶜ)).val.comp (aeval fun j ↦ ⟨a ↑j, ⋯⟩)) (X i✝)

Tactic:
simp

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

Goal state before:
pp: case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
⊢ Dense ↑(smoothLocus f)

Tactic:
rw [dense_iff_closure_eq, Set.eq_univ_iff_forall]

Goal state after:
case inr
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst : LocallyOfFinitePresentation f],
    CompactSpace ↥X → Dense ↑(smoothLocus f)
H : ¬CompactSpace ↥X
⊢ ∀ (x : ↥X), x ∈ closure ↑(smoothLocus f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this : IsNoetherian X
⊢ Dense ↑(smoothLocus f)

Tactic:
rw [dense_iff_closure_eq, Set.eq_univ_iff_forall]

Goal state after:
X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this : IsNoetherian X
⊢ ∀ (x : ↥X), x ∈ closure ↑(smoothLocus f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this✝¹ : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure ↑U = irreducibleComponent x
this✝ : IsIntegral ↑U
this : genericPoint ↥↑U ∈ U.ι ⁻¹ᵁ smoothLocus f
⊢ U.ι (genericPoint ↥↑U) ∈ smoothLocus f

Tactic:
Scheme.Hom.mem_preimage

Goal state after:
X✝ : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
X : Scheme
inst✝¹ : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
H : CompactSpace ↥X
this✝¹ : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure ↑U = irreducibleComponent x
this✝ : IsIntegral ↑U
this : U.ι (genericPoint ↥↑U) ∈ smoothLocus f
⊢ U.ι (genericPoint ↥↑U) ∈ smoothLocus f
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
p : ℕ
hp : Nat.Prime p
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
this : ∀ (i : ι), ∀ σ ∈ F.support, p ∣ σ i
σ' : (ι →₀ ℕ) → ι →₀ ℕ
hσ' : ∀ σ ∈ F.support, σ = p • σ' σ
hσ'' : ∀ (σ : ↥F.support), ↑σ = p • σ' ↑σ
H : ∀ (ι : Type u_3) (x : Fintype ι) (v : ι → K), LinearIndependent k v → LinearIndependent k fun x ↦ v x ^ p
F' : ↥F.support →₀ k
hF' : (Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) F' = 0
hF'0 : ¬F' = 0
F'' : MvPolynomial ι k := AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')
⊢ 0 = 0

Tactic:
simp

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hft : LocallyOfFiniteType f
hfu : FormallyUnramified f
⊢ diagonal (@Etale) f

Tactic:
exact inferInstanceAs <| Etale (pullback.diagonal f)

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ Etale f → (@LocallyOfFiniteType ⊓ @FormallyUnramified) f

Tactic:
hf

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
hf : Etale f
⊢ (@LocallyOfFiniteType ⊓ @FormallyUnramified) f
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : FormallyUnramified R S
inst✝ : EssFiniteType R S
x : ↑(CommRingCat.of S)
⊢ (CommRingCat.Hom.hom (CommRingCat.ofHom (TensorProduct.lmul' R).toRingHom)) (1 ⊗ₜ[R] x) = x

Tactic:
simp

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion (pullback.diagonal f)
⊢ FormallyUnramified f

Tactic:
wlog hY : ∃ R, Y = Spec R

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion (pullback.diagonal f)
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion (pullback.diagonal f)], (∃ R, Y = Spec R) → FormallyUnramified f
hY : ¬∃ R, Y = Spec R
⊢ FormallyUnramified f

X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion (pullback.diagonal f)
hY : ∃ R, Y = Spec R
⊢ FormallyUnramified f
Module: Mathlib.AlgebraicGeometry.Morphisms.LocalIso

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
⊢ IsLocalIso f ≤ P f

Tactic:
hf

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : P.ContainsIdentities
inst✝ : IsZariskiLocalAtSource P
X Y : Scheme
f : X ⟶ Y
hf : IsLocalIso f
⊢ P f
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
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
n : ι
inst✝ : ExpChar k p
ha' : IsTranscendenceBasis k fun i ↦ a ↑i
S : Set (MvPolynomial ι k) := {F | F ≠ 0 ∧ (aeval a) F = 0}
h : AlgebraicIndependent k a
⊢ n ∉ {n}ᶜ

Tactic:
simp

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

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ n + 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
n : ℕ
hn : Scheme.Hom.ker i ^ n = 0
⊢ ↑(0 * Scheme.Hom.ker i).support = Set.univ

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Descent

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P✝ Q✝ W : MorphismProperty C
A X✝ Y✝ Z✝ : C
fst : A ⟶ X✝
snd : A ⟶ Y✝
f✝ : X✝ ⟶ Z✝
g✝ : Y✝ ⟶ Z✝
inst✝⁴ : HasPullbacks C
P Q : MorphismProperty C
inst✝³ : P.DescendsAlong Q
inst✝² : P.RespectsIso
inst✝¹ : Q.IsStableUnderBaseChange
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : HasPullback f g
hf : Q f
hfst : P.diagonal (pullback.fst f g)
⊢ pullback.diagonal g ≫ pullback.snd g g ≫ g = g

Tactic:
simp

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
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
inst✝ : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis k fun i ↦ a ↑i
hn : n ∉ s
j : ↑(insert n s)
⊢ n ∈ insert n s

Tactic:
simp

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
p : ℕ
hp : Nat.Prime p
H : ∀ (s : Finset K), LinearIndepOn k id ↑s → LinearIndepOn k (fun x ↦ x ^ p) ↑s
a : ι → K
inst✝ : ExpChar k p
s : Set ι
n : ι
ha : IsTranscendenceBasis k fun i ↦ a ↑i
hn : n ∉ s
e₁ : { j // j ≠ ⟨n, ⋯⟩ } ≃ ↑s :=
  { toFun := fun x ↦ ⟨↑↑x, ⋯⟩, invFun := fun x ↦ ⟨⟨↑x, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ n ∈ insert n s

Tactic:
simp

Goal state after: