mathlib-initiative/mathlib-tactics huggingface dataset:
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
r✝ : R
x✝ : T
⊢ (have I := inst✝;
    r✝ • x✝) =
    r✝ • x✝

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
r✝ : R
x✝ : T
⊢ (have I := inst✝;
    r✝ • x✝) =
    r✝ • x✝
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
r✝ : R
x✝ : T
⊢ (algebraMap R T) r✝ * x✝ = r✝ • x✝

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
r✝ : R
x✝ : T
⊢ (algebraMap R T) r✝ * x✝ = r✝ • x✝
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)
⊢ (algebraMap S (S ⊗[R] T)).toAlgebra = Algebra.TensorProduct.leftAlgebra

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)
⊢ (algebraMap S (S ⊗[R] T)).toAlgebra = Algebra.TensorProduct.leftAlgebra
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)
r✝ : S
x✝ : S ⊗[R] T
⊢ (have I := (algebraMap S (S ⊗[R] T)).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝

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)
r✝ : S
x✝ : S ⊗[R] T
⊢ (have I := (algebraMap S (S ⊗[R] T)).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝
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)
r✝ : S
x✝ : S ⊗[R] T
⊢ r✝ • x✝ = (algebraMap S (S ⊗[R] T)) r✝ * x✝

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)
r✝ : S
x✝ : S ⊗[R] T
⊢ r✝ • x✝ = (algebraMap S (S ⊗[R] T)) r✝ * 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:
;

Goal state after:
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
Module: Mathlib.RingTheory.Extension.Cotangent.Basis

Goal state before:
pp: case inr
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
⊢ ⊤ ≤
    Submodule.comap (Submodule.subtype P.ker) (Submodule.span P.Ring (⇑(Submodule.subtype P.ker) '' Set.range v)) ⊔
      P.ker • ⊤

Tactic:
← Submodule.map_span,

Goal state after:
case inr
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
⊢ ⊤ ≤
    Submodule.comap (Submodule.subtype P.ker)
        (Submodule.map (Submodule.subtype P.ker) (Submodule.span P.Ring (Set.range v))) ⊔
      P.ker • ⊤
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
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.Smooth R S
s : Set S
hs : Ideal.span s = ⊤
h : ∀ x ∈ s, Algebra.IsStandardSmooth R (Localization.Away x)
t : S
ht : t ∈ s
⊢ Algebra.IsStandardSmooth R (Localization.Away t)

Tactic:
exact h t ht

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 (X.homOfLE e ≫ f ∣_ V)

Tactic:
;

Goal state after:
n m : ℕ
X Y : Scheme
f✝ f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : Smooth f
⊢ Smooth (X.homOfLE e ≫ f ∣_ V)
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 : ι
⊢ (AlgHom.restrictScalars k (Polynomial.aeval (a i))).comp
      ((Polynomial.mapAlgHom (aeval fun j ↦ ⟨a ↑j, ⋯⟩)).comp
        ((↑(optionEquivLeft k { b // b ≠ i })).comp ↑(renameEquiv k (Equiv.optionSubtypeNe i).symm))) =
    aeval a

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
hFa : (aeval a) F = 0
i : ι
⊢ (AlgHom.restrictScalars k (Polynomial.aeval (a i))).comp
      ((Polynomial.mapAlgHom (aeval fun j ↦ ⟨a ↑j, ⋯⟩)).comp
        ((↑(optionEquivLeft k { b // b ≠ i })).comp ↑(renameEquiv k (Equiv.optionSubtypeNe i).symm))) =
    aeval a
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 i✝ : ι
⊢ ((AlgHom.restrictScalars k (Polynomial.aeval (a i))).comp
        ((Polynomial.mapAlgHom (aeval fun j ↦ ⟨a ↑j, ⋯⟩)).comp
          ((↑(optionEquivLeft k { b // b ≠ i })).comp ↑(renameEquiv k (Equiv.optionSubtypeNe i).symm))))
      (X i✝) =
    (aeval a) (X i✝)

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
hFa : (aeval a) F = 0
i i✝ : ι
⊢ ((AlgHom.restrictScalars k (Polynomial.aeval (a i))).comp
        ((Polynomial.mapAlgHom (aeval fun j ↦ ⟨a ↑j, ⋯⟩)).comp
          ((↑(optionEquivLeft k { b // b ≠ i })).comp ↑(renameEquiv k (Equiv.optionSubtypeNe i).symm))))
      (X i✝) =
    (aeval a) (X i✝)
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:
;

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 : Irreducible F
i : ι
H : AlgebraicIndependent k fun x ↦ a ↑x
x✝ : K
⊢ x✝ ∈ a '' {i}ᶜ ↔ x✝ ∈ Set.range fun x ↦ a ↑x
Module: Mathlib.AlgebraicGeometry.Morphisms.Proper

Goal state before:
pp: this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom

Tactic:
inf_comm,

Goal state after:
this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @IsFinite = @IsAffineHom ⊓ @IsProper
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
⊢ (aeval a).comp (rename Subtype.val) = (Algebra.adjoin k (a '' {i}ᶜ)).val.comp (aeval fun j ↦ ⟨a ↑j, ⋯⟩)

Tactic:
;

Goal state after:
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
⊢ (aeval a).comp (rename Subtype.val) = (Algebra.adjoin k (a '' {i}ᶜ)).val.comp (aeval fun j ↦ ⟨a ↑j, ⋯⟩)
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:
;

Goal state after:
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✝)
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 : U.ι (genericPoint ↥↑U) ∈ smoothLocus f
⊢ x ∈ irreducibleComponent x

Tactic:
;

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
⊢ x ∈ irreducibleComponent x
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 := ⋯
hF''0 : F'' ≠ 0
v : ↥F.support
⊢ (((aeval a).toLinearMap ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv k).symm ∘ₗ Finsupp.lmapDomain k k fun s ↦ σ' ↑s) ∘ₗ
        Finsupp.lsingle v)
      1 =
    ((Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) ∘ₗ Finsupp.lsingle v) 1

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
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 := ⋯
hF''0 : F'' ≠ 0
v : ↥F.support
⊢ (((aeval a).toLinearMap ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv k).symm ∘ₗ Finsupp.lmapDomain k k fun s ↦ σ' ↑s) ∘ₗ
        Finsupp.lsingle v)
      1 =
    ((Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)) ∘ₗ Finsupp.lsingle v) 1
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X Y : Scheme
f✝ f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : Etale f
⊢ Etale (X.homOfLE e ≫ f ∣_ V)

Tactic:
;

Goal state after:
X Y : Scheme
f✝ f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst✝ : Etale f
⊢ Etale (X.homOfLE e ≫ f ∣_ V)
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝⁴ : Type ?u.17
x✝³ : Type ?u.16
x✝² : CommRing x✝⁴
x✝¹ : CommRing x✝³
x✝ : x✝⁴ →+* x✝³
⊢ x✝.Etale ↔ RingHom.IsStandardSmoothOfRelativeDimension 0 x✝

Tactic:
;

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x✝⁴ : Type ?u.17
x✝³ : Type ?u.16
x✝² : CommRing x✝⁴
x✝¹ : CommRing x✝³
x✝ : x✝⁴ →+* x✝³
⊢ x✝.Etale ↔ RingHom.IsStandardSmoothOfRelativeDimension 0 x✝
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')
hF''0 : F'' ≠ 0
this :
  ((aeval a).toLinearMap ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv k).symm ∘ₗ Finsupp.lmapDomain k k fun s ↦ σ' ↑s) =
    Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)
⊢ (aeval a) (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')) =
    ((aeval a).toLinearMap ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv k).symm ∘ₗ Finsupp.lmapDomain k k fun s ↦ σ' ↑s) F'

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
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')
hF''0 : F'' ≠ 0
this :
  ((aeval a).toLinearMap ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv k).symm ∘ₗ Finsupp.lmapDomain k k fun s ↦ σ' ↑s) =
    Finsupp.linearCombination k fun s ↦ (aeval a) ((monomial (σ' ↑s)) 1)
⊢ (aeval a) (AddMonoidAlgebra.ofCoeff (Finsupp.mapDomain (fun s ↦ σ' ↑s) F')) =
    ((aeval a).toLinearMap ∘ₗ ↑(AddMonoidAlgebra.coeffLinearEquiv k).symm ∘ₗ Finsupp.lmapDomain k k fun s ↦ σ' ↑s) F'
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X✝ X : Scheme
Z Y : X.Etale
f : Z ⟶ Y
⊢ Etale (Over.hom Z.toComma)

Tactic:
;

Goal state after:
X✝ X : Scheme
Z Y : X.Etale
f : Z ⟶ Y
⊢ Etale (Over.hom Z.toComma)
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
⊢ FormallyUnramified (Spec.map φ)

Tactic:
HasRingHomProperty.Spec_iff (P := @FormallyUnramified)

Goal state after:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : IsOpenImmersion (pullback.diagonal (Spec.map φ))
⊢ (CommRingCat.Hom.hom φ).FormallyUnramified
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula

Goal state before:
pp: case a
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'.negAddY P Q - W'.a₁ * 0 - W'.a₃ * 0) * (P z * Q z) ^ 3 +
        -(P z * Q z) * ((P y * Q z - Q y * P z) ^ 3 * (P z * Q z)) -
      (-(P y * Q z - Q y * P z) ^ 3 * (P z * Q z) ^ 2 + -(P z * Q z) * (W'.negAddY P Q * (P z * Q z) ^ 2)) =
    0

Tactic:
;

Goal state after:
case a
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'.negAddY P Q - W'.a₁ * 0 - W'.a₃ * 0) * (P z * Q z) ^ 3 +
        -(P z * Q z) * ((P y * Q z - Q y * P z) ^ 3 * (P z * Q z)) -
      (-(P y * Q z - Q y * P z) ^ 3 * (P z * Q z) ^ 2 + -(P z * Q z) * (W'.negAddY P Q * (P z * Q z) ^ 2)) =
    0
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: case e'_5
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
x✝ : ↥X
algInst✝ : Algebra ↑(Y.presheaf.stalk (f x✝)) ↑(X.presheaf.stalk x✝) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x✝)).toAlgebra
this : IsLocalHom (algebraMap ↑(Y.presheaf.stalk (f x✝)) ↑(X.presheaf.stalk x✝))
h :
  Algebra.IsSeparable (IsLocalRing.ResidueField ↑(Y.presheaf.stalk (f x✝)))
    (IsLocalRing.ResidueField ↑(X.presheaf.stalk x✝))
e_1✝ : ↑(Y.residueField (f x✝)) = IsLocalRing.ResidueField ↑(Y.presheaf.stalk (f x✝))
e_2✝ : ↑(X.residueField x✝) = IsLocalRing.ResidueField ↑(X.presheaf.stalk x✝)
e_3✝ : CommRingCat.instCommRingObjForgetRingHomCarrier ≍ IsLocalRing.instCommRingResidueField ↑(Y.presheaf.stalk (f x✝))
e_4✝ :
  (X.instFieldCarrierResidueField x✝).toDivisionRing.toRing ≍
    (IsLocalRing.ResidueField.field ↑(X.presheaf.stalk x✝)).toDivisionRing.toRing
x : ↑(Y.residueField (f x✝))
⊢ (algebraMap ↑(Y.residueField (f x✝)) ↑(X.residueField x✝)) x =
    (algebraMap ↑(Y.residueField (f x✝)) ↑(X.residueField x✝)) x

Tactic:
obtain ⟨x, rfl⟩ := IsLocalRing.residue_surjective x

Goal state after:
case e'_5
X Y : Scheme
f : X ⟶ Y
inst✝¹ : FormallyUnramified f
inst✝ : LocallyOfFiniteType f
x✝ : ↥X
algInst✝ : Algebra ↑(Y.presheaf.stalk (f x✝)) ↑(X.presheaf.stalk x✝) :=
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x✝)).toAlgebra
this : IsLocalHom (algebraMap ↑(Y.presheaf.stalk (f x✝)) ↑(X.presheaf.stalk x✝))
h :
  Algebra.IsSeparable (IsLocalRing.ResidueField ↑(Y.presheaf.stalk (f x✝)))
    (IsLocalRing.ResidueField ↑(X.presheaf.stalk x✝))
e_1✝ : ↑(Y.residueField (f x✝)) = IsLocalRing.ResidueField ↑(Y.presheaf.stalk (f x✝))
e_2✝ : ↑(X.residueField x✝) = IsLocalRing.ResidueField ↑(X.presheaf.stalk x✝)
e_3✝ : CommRingCat.instCommRingObjForgetRingHomCarrier ≍ IsLocalRing.instCommRingResidueField ↑(Y.presheaf.stalk (f x✝))
e_4✝ :
  (X.instFieldCarrierResidueField x✝).toDivisionRing.toRing ≍
    (IsLocalRing.ResidueField.field ↑(X.presheaf.stalk x✝)).toDivisionRing.toRing
x : ↑(Y.presheaf.stalk (f x✝))
⊢ (algebraMap ↑(Y.residueField (f x✝)) ↑(X.residueField x✝)) ((IsLocalRing.residue ↑(Y.presheaf.stalk (f x✝))) x) =
    (algebraMap ↑(Y.residueField (f x✝)) ↑(X.residueField x✝)) ((IsLocalRing.residue ↑(Y.presheaf.stalk (f x✝))) x)
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this : IsDominant i
x✝ : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x✝) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x✝ ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
x : ↥Z
⊢ g₁ x = g₂ x

Tactic:
;

Goal state after:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this : IsDominant i
x✝ : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x✝) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x✝ ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
x : ↥Z
⊢ g₁ x = g₂ x
Module: Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified

Goal state before:
pp: X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this : IsDominant i
x✝ : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x✝) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x✝ ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
x : ↥Z'
⊢ g₁ (i x) = g₂ (i x)

Tactic:
;

Goal state after:
X Y Z' Z : Scheme
i : Z' ⟶ Z
hi : IsNilpotent (Scheme.Hom.ker i)
inst✝¹ : IsClosedImmersion i
f : X ⟶ Y
inst✝ : FormallyUnramified f
g₁ g₂ : Z ⟶ X
hig : i ≫ g₁ = i ≫ g₂
hgf : g₁ ≫ f = g₂ ≫ f
this : IsDominant i
x✝ : ↥Z
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f (g₁ x✝) ∈ ↑U
V : Opens ↥X
hV : V ∈ X.affineOpens
hxV : g₁ x✝ ∈ ↑V
hVU : V ≤ f ⁻¹ᵁ U
x : ↥Z'
⊢ g₁ (i x) = g₂ (i x)