mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Real.Embedding

Goal state before:
pp: M : Type u_1
inst✝⁶ : AddCommGroup M
inst✝⁵ : LinearOrder M
inst✝⁴ : IsOrderedAddMonoid M
inst✝³ : One M
inst✝² : ZeroLEOneClass M
inst✝¹ : NeZero 1
inst✝ : Archimedean M
x y : M
h : x < y
hyz : 0 < y - x
hy : y = y - x + x
n : ℕ
hn : 1 ≤ n • (y - x)
⊢ ↑{ num := 1, den := n + 1, den_nz := ⋯, reduced := ⋯ } ∈ ratLt' (y - x)

Tactic:
simpa using hn.trans_lt <| nsmul_lt_nsmul_left hyz (show n < n + 1 by simp)

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff d) φ = 0
h' : φ.lexOrder < w
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : φ.lexOrder = ↑(toLex d)
⊢ ↑(toLex d) < w

Tactic:
← hd

Goal state after:
case mpr
σ : Type u_1
R : Type u_2
inst✝² : Semiring R
inst✝¹ : LinearOrder σ
inst✝ : WellFoundedGT σ
φ : MvPowerSeries σ R
w : WithTop (Lex (σ →₀ ℕ))
h : ∀ (d : σ →₀ ℕ), ↑(toLex d) < w → (coeff d) φ = 0
h' : φ.lexOrder < w
hφ : φ ≠ 0
d : σ →₀ ℕ
hd : φ.lexOrder = ↑(toLex d)
⊢ φ.lexOrder < w
Module: Mathlib.Analysis.Normed.Group.Ultra

Goal state before:
pp: case cons.inr
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ ‖f a‖₊ ≠ ‖∏ x ∈ s, f x‖₊

Tactic:
rw [hj']

Goal state after:
case cons.inr
M : Type u_1
ι : Type u_2
inst✝¹ : SeminormedCommGroup M
inst✝ : IsUltrametricDist M
f : ι → M
a : ι
s : Finset ι
ha : a ∉ s
IH : ‖∏ i ∈ s, f i‖₊ = s.sup fun i ↦ ‖f i‖₊
hs : (↑(Finset.cons a s ha)).Pairwise fun i j ↦ ‖f i‖₊ ≠ ‖f j‖₊
hs' : s.Nonempty
j : ι
hj : j ∈ s
hj' : ‖∏ i ∈ s, f i‖₊ = ‖f j‖₊
⊢ ‖f a‖₊ ≠ ‖f j‖₊
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
x y : L
⊢ ↑((RankOne.hom v) (v.restrict (x - y))) = ↑((RankOne.hom v) (v.restrict (y - x)))

Tactic:
rw [← neg_sub, Valuation.map_neg]

Goal state after:
Module: Mathlib.RingTheory.MvPowerSeries.LexOrder

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝³ : Semiring R
inst✝² : LinearOrder σ
inst✝¹ : WellFoundedGT σ
inst✝ : NoZeroDivisors R
φ ψ : MvPowerSeries σ R
⊢ (φ * ψ).lexOrder = φ.lexOrder + ψ.lexOrder

Tactic:
obtain rfl | hφ := eq_or_ne φ 0
  · simp
  obtain rfl | hψ := eq_or_ne ψ 0
  · simp
  rcases exists_finsupp_eq_lexOrder_of_ne_zero hφ with ⟨p, hp⟩
  rcases exists_finsupp_eq_lexOrder_of_ne_zero hψ with ⟨q, hq⟩
  apply le_antisymm _ (lexOrder_mul_ge φ ψ)
  rw [hp, hq]
  apply lexOrder_le_of_coeff_ne_zero (d := p + q)
  rw [coeff_mul_of_add_lexOrder hp hq, mul_ne_zero_iff]
  exact ⟨coeff_ne_zero_of_lexOrder hp.symm, coeff_ne_zero_of_lexOrder hq.symm⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.NormedValued

Goal state before:
pp: case refine_2
L : Type u_1
inst✝¹ : Field L
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
val : Valued L Γ₀
hv : v.RankOne
this : Nonempty { ε // ε > 0 }
U : Set (L × L)
x✝ : ∃ a, 0 < a ∧ {p | v.norm (p.1 - p.2) < a} ⊆ U
r : ℝ
hr_pos : 0 < r
hr : {p | v.norm (p.1 - p.2) < r} ⊆ U
⊢ ∃ i, {p | v.restrict (p.2 - p.1) < ↑i} ⊆ U

Tactic:
· have : Nontrivial Γ₀ˣ := (nontrivial_iff_exists_ne (1 : Γ₀ˣ)).mpr
            ⟨RankOne.unit val.v, RankOne.unit_ne_one val.v⟩
          obtain ⟨u, hu⟩ := Real.exists_lt_of_strictMono hv.strictMono hr_pos
          use u
          apply subset_trans _ hr
          intro x hx
          simp only [Valuation.norm, mem_ofPred_eq]
          apply lt_trans _ hu
          rw [NNReal.coe_lt_coe, ← neg_sub, Valuation.map_neg]
          exact (RankOne.strictMono Valued.v).lt_iff_lt.mpr hx

Goal state after:
Module: Mathlib.CategoryTheory.Sites.CoproductSheafCondition

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this : (E.sigmaOfIsColimit hc).HasPullbacks
⊢ IsSheafFor F (singleton (Cofan.IsColimit.desc hc f)) ↔ IsSheafFor F (ofArrows X f)

Tactic:
have (i : E.I₀) : HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit) := by
    dsimp [sigmaOfIsColimit_f]; infer_instance

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
S : C
ι : Type u_3
X : ι → C
f : (i : ι) → X i ⟶ S
inst✝⁴ : (ofArrows X f).HasPairwisePullbacks
c : Cofan X
hc : IsColimit c
hc' : IsUniversalColimit c
inst✝³ : HasPullback (Cofan.IsColimit.desc hc f) (Cofan.IsColimit.desc hc f)
inst✝² : ∀ (i : ι), HasPullback (f i) (Cofan.IsColimit.desc hc f)
F : Cᵒᵖ ⥤ Type u_4
inst✝¹ : PreservesLimit (Discrete.functor fun i ↦ op (X i)) F
inst✝ : PreservesLimit (Discrete.functor fun ij ↦ op (Limits.pullback (f ij.1) (f ij.2))) F
E : PreZeroHypercover S := { I₀ := ι, X := X, f := f }
this✝ : (E.sigmaOfIsColimit hc).HasPullbacks
this : ∀ (i : E.I₀), HasPullback (E.f i) ((E.sigmaOfIsColimit hc).f PUnit.unit)
⊢ IsSheafFor F (singleton (Cofan.IsColimit.desc hc f)) ↔ IsSheafFor F (ofArrows X f)
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsSeparable K L
inst✝ : EssFiniteType K L
this✝ : FormallyUnramified K L
this : Module.Finite K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
pb : PowerBasis K L := Field.powerBasisOfFiniteOfSeparable K L
x : B
hx : (Ideal.Quotient.mk I) x = f pb.gen
helper : ∀ (x : B), (IsScalarTower.toAlgHom K B (B ⧸ I)) x = (Ideal.Quotient.mk I) x
⊢ (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0

Tactic:
rw [← helper, ← aeval_algHom_apply, helper, hx, aeval_algHom_apply, minpoly.aeval, map_zero]

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

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
x y : L
this✝ : FiniteDimensional K ↥K⟮x, y⟯
this : Algebra.IsSeparable K ↥K⟮x, y⟯
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯

Tactic:
obtain ⟨⟨α, hα⟩, e⟩ := Field.exists_primitive_element K K⟮x, y⟯

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : Algebra.IsSeparable K L
B : Type (max u_1 u_2)
x✝¹ : CommRing B
x✝ : Algebra K B
I : Ideal B
h : I ^ 2 = ⊥
f : L →ₐ[K] B ⧸ I
g : (k : L) → ↥K⟮k⟯ →ₐ[K] B
hg₁ : ∀ (k : L), (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) (g k)
hg₂ :
  ∀ (k : L) (y : ↥K⟮k⟯ →ₐ[K] B),
    (fun g ↦ (Ideal.Quotient.mkₐ K I).comp g = f.comp (IsScalarTower.toAlgHom K (↥K⟮k⟯) L)) y → y = g k
hg₃ : ∀ (x y : L) (h : x ∈ K⟮y⟯), (g y) ⟨x, h⟩ = (g x) (IntermediateField.AdjoinSimple.gen K x)
x y : L
this✝ : FiniteDimensional K ↥K⟮x, y⟯
this : Algebra.IsSeparable K ↥K⟮x, y⟯
α : L
hα : α ∈ K⟮x, y⟯
e : K⟮⟨α, hα⟩⟯ = ⊤
⊢ ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
Module: Mathlib.RingTheory.Etale.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
f : A
⊢ FormallyEtale R (Localization.Away f) ↔ Etale R (Localization.Away f)

Tactic:
refine ⟨fun H ↦ ⟨H, inferInstance⟩, fun _ ↦ inferInstance⟩

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
inst✝ : FinitePresentation R A
⊢ FormallyEtale R A ↔ Etale R A

Tactic:
refine ⟨fun H ↦ ⟨H, inferInstance⟩, fun _ ↦ inferInstance⟩

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: R : Type u
inst✝⁶ : CommRing R
I : Ideal R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCompletion I M
a : AdicCauchySequence I M
hx : (map I f) ((mk I M) a) = 0
⊢ (mk I M) a = 0

Tactic:
refine AdicCompletion.mk_zero_of _ _ _ ⟨42, fun n _ ↦ ⟨n + k, by lia, n, by lia, ?_⟩⟩

Goal state after:
R : Type u
inst✝⁶ : CommRing R
I : Ideal R
M : Type u
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
hf : Function.Injective ⇑f
k : ℕ
hk : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCompletion I M
a : AdicCauchySequence I M
hx : (map I f) ((mk I M) a) = 0
n : ℕ
x✝ : n ≥ 42
⊢ ↑a (n + k) ∈ I ^ n • ⊤
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
n : ℕ
y : N ⧸ I ^ n • ⊤
y' : N ⧸ I ^ (n + 1) • ⊤
hyy' : (factor ⋯) y' = y
hxy : (I ^ n • ⊤).mkQ (f x) = y
y0 : N
hy0 : (I ^ (n + 1) • ⊤).mkQ y0 = y'
⊢ ∃ x', x ≡ x' [SMOD I ^ n • ⊤] ∧ (I ^ (n + 1) • ⊤).mkQ (f x') = y'

Tactic:
have : f x ≡ y0 [SMOD (I ^ n • ⊤ : Submodule R N)] := by
    rw [SModEq, ← mkQ_apply, ← mkQ_apply, ← factor_mk (pow_smul_top_le I N n.le_succ) y0,
        hy0, hyy', hxy]

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
x : M
n : ℕ
y : N ⧸ I ^ n • ⊤
y' : N ⧸ I ^ (n + 1) • ⊤
hyy' : (factor ⋯) y' = y
hxy : (I ^ n • ⊤).mkQ (f x) = y
y0 : N
hy0 : (I ^ (n + 1) • ⊤).mkQ y0 = y'
this : f x ≡ y0 [SMOD I ^ n • ⊤]
⊢ ∃ x', x ≡ x' [SMOD I ^ n • ⊤] ∧ (I ^ (n + 1) • ⊤).mkQ (f x') = y'
Module: Mathlib.RingTheory.AdicCompletion.Functoriality

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
I : Ideal R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
h✝ : Function.Surjective ⇑((I • ⊤).mkQ ∘ₗ f)
y : AdicCompletion I N
h : ∃ x, ∀ (n : ℕ), x n ≡ x (n + 1) [SMOD I ^ n • ⊤] ∧ Submodule.Quotient.mk (f (x n)) = (eval I N n) y
⊢ ∃ a, (map I f) a = y

Tactic:
by
    obtain ⟨x, hx⟩ := h
    use AdicCompletion.mk I M ⟨x, fun h ↦
        eq_factor_of_eq_factor_succ (fun _ _ ↦ pow_smul_top_le I M) _ (fun n ↦ (hx n).1) h⟩
    ext n
    simp [hx n]

Goal state after:
Module: Mathlib.RingTheory.AdicCompletion.Exactness

Goal state before:
pp: R : Type u
inst✝⁸ : CommRing R
I : Ideal R
M : Type u
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
N : Type u
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
P : Type u
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R N
f : M →ₗ[R] N
g : N →ₗ[R] P
hf : Function.Injective ⇑f
hfg : Function.Exact ⇑f ⇑g
hg : Function.Surjective ⇑g
k : ℕ
hkn : ∀ n ≥ k, I ^ n • ⊤ ⊓ f.range = I ^ (n - k) • (I ^ k • ⊤ ⊓ f.range)
x : AdicCauchySequence I N
hker : ∀ (n : ℕ), g (↑x n) ∈ I ^ n • ⊤
x✝ n : ℕ
⊢ g (↑x (k + n)) ∈ Submodule.map g (I ^ (k + n) • ⊤)

Tactic:
rw [map_smul'', Submodule.map_top, range_eq_top.mpr hg]
    exact hker (k + n)

Goal state after:
Module: Mathlib.RingTheory.Extension.Presentation.Submersive

Goal state before:
pp: R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
this : Fintype σ
⊢ ((LinearMap.toMatrix (Pi.basisFun S σ) (Pi.basisFun S σ)) P.aevalDifferential).det = P.jacobian

Tactic:
rw [LinearMap.toMatrix_eq_toMatrix', jacobian_eq_jacobiMatrix_det,
      aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, P.algebraMap_eq]

Goal state after:
R : Type u
S : Type v
ι : Type w
σ : Type t
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Finite σ
P : SubmersivePresentation R S ι σ
this : Fintype σ
⊢ ((aeval P.val).mapMatrix P.jacobiMatrix).det = ↑(aeval P.val) P.jacobiMatrix.det
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'.addX P Q * (P z * Q z) ^ 2 =
    ((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 - Q x * P z)

Tactic:
linear_combination (norm := (rw [addX]; ring1))
    (2 * Q x * P z * Q z ^ 3 - P x * Q z ^ 4) * (equation_iff _).mp hP
      + (Q x * P z ^ 4 - 2 * P x * P z ^ 3 * Q z) * (equation_iff _).mp hQ

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:
exact D.hgmem

Goal state after:
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)
⊢ (algebraMap S (S ⊗[R] T)).IsStandardSmooth

Tactic:
rw [RingHom.IsStandardSmooth]; convert! this; ext; simp_rw [Algebra.smul_def]; rfl

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 ?u.29) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
⊢ ∃ g, g.Etale

Tactic:
obtain ⟨ι, σ, _, _, P, e⟩ :=
    Algebra.IsStandardSmoothOfRelativeDimension.out (R := R) (S := S) (n := n)

Goal state after:
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 ?u.29) → [_root_.Finite α] → Fintype α := Fintype.ofFinite
ι σ : Type
w✝¹ : _root_.Finite σ
w✝ : _root_.Finite ι
P : Algebra.SubmersivePresentation R S ι σ
e : P.dimension = n
⊢ ∃ g, g.Etale
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
⊢ S ⊗[D.T] D.presLeft.toExtension.Cotangent ≃ₗ[S] P.toExtension.Cotangent

Tactic:
by
  refine LinearEquiv.ofLinearMap D.tensorCotangentHom D.tensorCotangentInv ?_ ?_
  · refine b.ext fun i ↦ ?_
    simpa only [LinearMap.coe_comp, Function.comp_apply, tensorCotangentInv_apply,
      tensorCotangentHom_tmul] using! D.hf (b i)
  · ext : 2
    refine LinearMap.ext_on_range D.span_range_mk_kerGen fun i ↦ ?_
    simp [-toExtension_commRing, -toExtension_Ring, -toExtension_algebra₂, tensorCotangentHom_tmul,
      kerGen, D.hf]

Goal state after:
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)))
⊢ (Presentation.naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯).σ (-1) = -1

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)))
⊢ (Presentation.naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯).σ 0 = 0

Tactic:
· rw [Presentation.naive, Generators.naive_σ];
    simp

Goal state after:
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)))
⊢ (Presentation.naive (fun x ↦ if x = 0 then 0 else if x = -1 then -1 else Function.surjInv ⋯ x) ⋯).σ 0 = 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
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:
simp [A₀]

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:
simp [A₀]

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

Goal state before:
pp: n : ℕ
X Y : Scheme
f : X ⟶ Y
inst✝ : SmoothOfRelativeDimension n f
x : ↥X
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))
⊢ ∃ U,
    ∃ (_ : IsAffineOpen U),
      ∃ V,
        ∃ (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth

Tactic:
exact ⟨U, hU, V, hV, hx, e, hf.isStandardSmooth⟩

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
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := Equiv.subtypeEquivRight ⋯
⊢ Irreducible
    ((Polynomial.mapAlgHom (aeval fun j ↦ ⟨a ↑j, ⋯⟩))
      ((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)))

Tactic:
refine (congrArg Irreducible ?_).mp <|
    hF.map (renameEquiv k ((Equiv.optionSubtypeNe i).symm)) |>.map
      (optionEquivLeft k _) |>.map (Polynomial.mapAlgEquiv <|
        (renameEquiv k d).trans <| H.aevalEquiv.trans
        (Subalgebra.equivOfEq _ _ congr(Algebra.adjoin k $hc.symm)))

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
hc : a '' {i}ᶜ = Set.range fun x ↦ a ↑x
d : { j // j ≠ i } ≃ ↑{j | j ≠ i} := Equiv.subtypeEquivRight ⋯
⊢ (Polynomial.mapAlgEquiv
        ((renameEquiv k d).trans
          (H.aevalEquiv.trans
            ((Algebra.adjoin k (Set.range fun x ↦ a ↑x)).equivOfEq (Algebra.adjoin k (a '' {i}ᶜ)) ⋯))))
      ((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)) =
    (Polynomial.mapAlgHom (aeval fun j ↦ ⟨a ↑j, ⋯⟩))
      ((optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F))
Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth

Goal state before:
pp: X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this✝ : (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).EssFiniteType
algInst✝ : Algebra ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X)))
  ↑(X.presheaf.stalk (genericPoint ↥X)) :=
  (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).toAlgebra
algebraizeInst✝ :
  Algebra.EssFiniteType ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X)))
    ↑(X.presheaf.stalk (genericPoint ↥X))
K' : CommRingCat := (Spec.structureSheaf K).presheaf.stalk (f (genericPoint ↥X))
e : K ≃ₐ[K] ↑K' := IsLocalization.atUnits (↑(CommRingCat.of K)) (f (genericPoint ↥X)).asIdeal.primeCompl ⋯
this : Algebra.IsAlgebraic K ↑K'
⊢ (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).FormallySmooth

Tactic:
let : Field K' := (e.toRingEquiv.symm.isField (Field.toIsField K)).toField

Goal state after:
X : Scheme
K : Type u
inst✝³ : Field K
inst✝² : PerfectField K
inst✝¹ : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFinitePresentation f
this✝¹ : (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).EssFiniteType
algInst✝ : Algebra ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X)))
  ↑(X.presheaf.stalk (genericPoint ↥X)) :=
  (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).toAlgebra
algebraizeInst✝ :
  Algebra.EssFiniteType ↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X)))
    ↑(X.presheaf.stalk (genericPoint ↥X))
K' : CommRingCat := (Spec.structureSheaf K).presheaf.stalk (f (genericPoint ↥X))
e : K ≃ₐ[K] ↑K' := IsLocalization.atUnits (↑(CommRingCat.of K)) (f (genericPoint ↥X)).asIdeal.primeCompl ⋯
this✝ : Algebra.IsAlgebraic K ↑K'
this : Field ↑K' := ⋯.toField
⊢ (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X))).FormallySmooth
Module: Mathlib.AlgebraicGeometry.Morphisms.Etale

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Etale) ↔
    (∀ {U : Y.Opens},
        IsAffineOpen U →
          ∀ {V : X.Opens},
            IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat) ∧
      (∀ {U : Y.Opens},
          IsAffineOpen U →
            ∀ {V : X.Opens},
              IsAffineOpen V →
                ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FormallyUnramified) ∧
        LocallyOfFinitePresentation f

Tactic:
locallyOfFinitePresentation_iff

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Etale) ↔
    (∀ {U : Y.Opens},
        IsAffineOpen U →
          ∀ {V : X.Opens},
            IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Flat) ∧
      (∀ {U : Y.Opens},
          IsAffineOpen U →
            ∀ {V : X.Opens},
              IsAffineOpen V →
                ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FormallyUnramified) ∧
        ∀ {U : Y.Opens},
          IsAffineOpen U →
            ∀ {V : X.Opens},
              IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FinitePresentation