mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: case w.hy
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
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (u * (aeval x) (minpoly K pb.gen)) ^ 2 ∈ ⊥

Tactic:
← h

Goal state after:
case w.hy
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
hx' : (Ideal.Quotient.mk I) ((aeval x) (minpoly K pb.gen)) = 0
u : B
hu : (aeval x) (derivative (minpoly K pb.gen)) * u + 1 ∈ I
⊢ (u * (aeval x) (minpoly K pb.gen)) ^ 2 ∈ I ^ 2
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)
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f

Tactic:
have H : ∀ x y : L, ∃ α : L, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯ := by
    intro x y
    have : FiniteDimensional K K⟮x, y⟯ := by
      apply IntermediateField.finiteDimensional_adjoin
      intro x _; exact (Algebra.IsSeparable.isSeparable K x).isIntegral
    have := IsSeparable.of_algHom _ _ (IsScalarTower.toAlgHom K (K⟮x, y⟯) L)
    obtain ⟨⟨α, hα⟩, e⟩ := Field.exists_primitive_element K K⟮x, y⟯
    apply_fun (IntermediateField.map (IntermediateField.val _)) at e
    rw [IntermediateField.adjoin_map, ← AlgHom.fieldRange_eq_map] at e
    simp only [IntermediateField.coe_val, Set.image_singleton,
      IntermediateField.fieldRange_val] at e
    have hx : x ∈ K⟮α⟯ := e ▸ IntermediateField.subset_adjoin K {x, y} (by simp)
    have hy : y ∈ K⟮α⟯ := e ▸ IntermediateField.subset_adjoin K {x, y} (by simp)
    exact ⟨α, hx, hy⟩

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)
H : ∀ (x y : L), ∃ α, x ∈ K⟮α⟯ ∧ y ∈ K⟮α⟯
⊢ ∃ a, (Ideal.Quotient.mkₐ K I).comp a = f
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
A : Type u
inst✝⁴ : Field K
inst✝³ : CommRing A
inst✝² : Algebra K A
inst✝¹ : EssFiniteType K A
inst✝ : FormallyUnramified K A
⊢ FormallyEtale K A

Tactic:
have := FormallyUnramified.isReduced_of_field K A
  have : IsArtinianRing A := .of_finite K A
  have (I : MaximalSpectrum A) : FormallyEtale K (A ⧸ I.asIdeal) := by
    rw [FormallyEtale.iff_isSeparable, ← FormallyUnramified.iff_isSeparable]
    infer_instance
  exact .of_equiv ((IsArtinianRing.equivPi A).restrictScalars K).symm

Goal state after:
Module: Mathlib.RingTheory.Kaehler.TensorProduct

Goal state before:
pp: case smul
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
inst✝⁷ : CommRing A
inst✝⁶ : CommRing B
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : Algebra S B
inst✝¹ : IsScalarTower R A B
inst✝ : IsScalarTower R S B
h : Algebra.IsPushout R S A B
x : S ⊗[R] Ω[A⁄R]
s : S
b : B
e : (LinearMap.liftBaseChange S (↑R (map R S A B))) (b • x) = b • (LinearMap.liftBaseChange S (↑R (map R S A B))) x
⊢ (LinearMap.liftBaseChange S (↑R (map R S A B))) ((s • b) • x) =
    (s • b) • (LinearMap.liftBaseChange S (↑R (map R S A B))) x

Tactic:
rw [smul_assoc, map_smul, e, smul_assoc]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsLocalRing S
inst✝¹¹ : Algebra R S
P : Type u_3
K : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : Algebra S K
inst✝⁴ : Algebra P K
inst✝³ : IsScalarTower P S K
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
h₃ : maximalIdeal S ≤ RingHom.ker (algebraMap S K)
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this✝¹ : Algebra (ResidueField S) K := f.toAlgebra
this✝ : IsScalarTower S (ResidueField S) K
this : IsScalarTower P (ResidueField S) K
⊢ Function.Injective ⇑(LinearMap.lTensor K (cotangentComplexBaseChange R S P (ResidueField S))) ↔
    Function.Injective ⇑(cotangentComplexBaseChange R S P K)

Tactic:
have : (AlgebraTensorModule.cancelBaseChange _ _ _ _ _).toLinearMap ∘ₗ
      (cotangentComplexBaseChange R S P (ResidueField S)).baseChange K ∘ₗ
      (AlgebraTensorModule.cancelBaseChange _ _ _ _ _).symm.toLinearMap =
      (cotangentComplexBaseChange R S P K) := by
    ext
    #adaptation_note /-- Prior to nightly-2026-04-06, this was just `simp`. -/
    simp_rw [AlgebraTensorModule.curry_apply, LinearMap.restrictScalars_comp, curry_apply,
      LinearMap.coe_comp, LinearMap.coe_restrictScalars, LinearEquiv.coe_coe, Function.comp_apply,
      AlgebraTensorModule.cancelBaseChange_symm_tmul, LinearMap.baseChange_tmul,
      cotangentComplexBaseChange_tmul, kerToTensor_apply, one_smul,
      AlgebraTensorModule.cancelBaseChange_tmul]
    simp

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : IsLocalRing S
inst✝¹¹ : Algebra R S
P : Type u_3
K : Type u_4
inst✝¹⁰ : Field K
inst✝⁹ : CommRing P
inst✝⁸ : Algebra R P
inst✝⁷ : Algebra P S
inst✝⁶ : IsScalarTower R P S
inst✝⁵ : Algebra S K
inst✝⁴ : Algebra P K
inst✝³ : IsScalarTower P S K
inst✝² : FormallySmooth R P
inst✝¹ : Module.Free P Ω[P⁄R]
inst✝ : Module.Finite P Ω[P⁄R]
h₁ : Function.Surjective ⇑(algebraMap P S)
h₂ : (RingHom.ker (algebraMap P S)).FG
h₃ : maximalIdeal S ≤ RingHom.ker (algebraMap S K)
f : ResidueField S →ₐ[S] K := Ideal.Quotient.liftₐ (maximalIdeal S) (ofId S K) h₃
this✝² : Algebra (ResidueField S) K := f.toAlgebra
this✝¹ : IsScalarTower S (ResidueField S) K
this✝ : IsScalarTower P (ResidueField S) K
this :
  ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K Ω[P⁄R]) ∘ₗ
      LinearMap.baseChange K (cotangentComplexBaseChange R S P (ResidueField S)) ∘ₗ
        ↑(AlgebraTensorModule.cancelBaseChange P (ResidueField S) K K ↥(RingHom.ker (algebraMap P S))).symm =
    cotangentComplexBaseChange R S P K
⊢ Function.Injective ⇑(LinearMap.lTensor K (cotangentComplexBaseChange R S P (ResidueField S))) ↔
    Function.Injective ⇑(cotangentComplexBaseChange R S P K)
Module: Mathlib.RingTheory.Etale.Field

Goal state before:
pp: K : Type u_1
A : Type u
inst✝⁹ : Field K
inst✝⁸ : CommRing A
inst✝⁷ : Algebra K A
B : Type u_3
inst✝⁶ : CommRing B
inst✝⁵ : EssFiniteType K A
inst✝⁴ : FormallyEtale K A
inst✝³ : Algebra K B
inst✝² : EssFiniteType K B
inst✝¹ : FormallyEtale K B
inst✝ : IsSepClosed K
f : A →ₐ[K] B
x : A
p : PrimeSpectrum B
⊢ (equivPiOfIsSepClosed K A) x (PrimeSpectrum.comap (↑f) p) = (equivPiOfIsSepClosed K B) (f x) p

Tactic:
dsimp [equivPiOfIsSepClosed]
  simp only [Equiv.piCongrLeft_symm_apply, AlgEquiv.piCongrRight_apply,
    IsArtinianRing.primeSpectrumEquivMaximalSpectrum_apply_asIdeal, PrimeSpectrum.comap_asIdeal,
    IsArtinianRing.equivPi_apply]
  have heq : ofId K (B ⧸ p.asIdeal) = (Ideal.quotientMapₐ p.asIdeal f le_rfl).comp (ofId _ _) := by
    simp
  suffices h : Ideal.quotientMapₐ p.asIdeal f le_rfl x = f x by
    apply FaithfulSMul.algebraMap_injective K (B ⧸ p.asIdeal)
    rw [← ofId_apply, ← ofId_apply]
    nth_rw 1 [heq]
    simp only [AlgHom.coe_comp, Function.comp_apply, AlgEquiv.ofBijective_apply_symm_apply]
    convert h
    apply AlgEquiv.ofBijective_apply_symm_apply
  simp

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r✝ : AdicCompletion I R
x : AdicCompletion I M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
⊢ (transitionMap I M hmn) ((fun n ↦ (eval I R n) ((mk I R) r) • (eval I M n) x) n) =
    (fun n ↦ (eval I R n) ((mk I R) r) • (eval I M n) x) m

Tactic:
apply induction_on I M x (fun x ↦ ?_)

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
I : Ideal R
M : Type u_3
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r✝ : AdicCompletion I R
x✝ : AdicCompletion I M
m n : ℕ
hmn : m ≤ n
r : AdicCauchySequence I R
x : AdicCauchySequence I M
⊢ (transitionMap I M hmn) ((fun n ↦ (eval I R n) ((mk I R) r) • (eval I M n) ((mk I M) x)) n) =
    (fun n ↦ (eval I R n) ((mk I R) r) • (eval I M n) ((mk I M) x)) m
Module: Mathlib.LinearAlgebra.Basis.Exact

Goal state before:
pp: R : Type u_1
M : Type u_2
K : Type u_3
P : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup K
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R K
inst✝ : Module R P
f : K →ₗ[R] M
g : M →ₗ[R] P
hfg : Function.Exact ⇑f ⇑g
p q : Submodule R M
hpq : IsCompl p q
hmap : map g q = ⊤
⊢ Function.Surjective ⇑(p.projectionOnto q hpq ∘ₗ f)

Tactic:
rw [← Set.surjOn_univ, LinearMap.coe_comp, Set.surjOn_comp_iff, Set.image_univ]
  rw [← LinearMap.coe_range, ← Submodule.top_coe (R := R), surjOn_iff_le_map,
    ← hfg.linearMap_ker_eq]
  intro x triv
  obtain ⟨a, haq, ha⟩ : g x.val ∈ q.map g := by rwa [hmap]
  exact ⟨x - a, by simp [← ha], by simpa⟩

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

Goal state before:
pp: R : Type u_1
S : Type u_2
ι : Type u_3
σ : Type u_4
inst✝¹³ : CommRing R
inst✝¹² : CommRing S
inst✝¹¹ : Algebra R S
P : Presentation R S ι σ
R₀ : Type u_5
inst✝¹⁰ : CommRing R₀
inst✝⁹ : Algebra R₀ R
inst✝⁸ : Algebra R₀ S
inst✝⁷ : IsScalarTower R₀ R S
inst✝⁶ : P.HasCoeffs R₀
R₁ : Type u_6
inst✝⁵ : CommRing R₁
inst✝⁴ : Algebra R₀ R₁
inst✝³ : Algebra R₁ R
inst✝² : IsScalarTower R₀ R₁ R
inst✝¹ : Algebra R₁ S
inst✝ : IsScalarTower R₁ R S
⊢ P.HasCoeffs R₁

Tactic:
by
  refine ⟨subset_trans (P.coeffs_subset_range R₀) ?_⟩
  simp [IsScalarTower.algebraMap_eq R₀ R₁ R, RingHom.coe_comp, Set.range_comp]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Nontrivial S
n : ℕ
inst✝ : IsStandardSmoothOfRelativeDimension n R S
⊢ Module.rank S Ω[S⁄R] = ↑n

Tactic:
by
  obtain ⟨_, _, _, _, ⟨P, hP⟩⟩ := ‹IsStandardSmoothOfRelativeDimension n R S›
  rw [P.rank_kaehlerDifferential, hP]

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✝
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
h✝ : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
this✝ : eₚ = ↑b.repr.symm
heₚ : Function.Bijective ⇑eₚ
this : Finite κ
g : S
hg : g ∉ p
h : Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers g)) e)
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)

Tactic:
let l₁ₜ : (κ →₀ S) →ₗ[S] (κ →₀ Localization.Away g) :=
    Finsupp.mapRange.linearMap (Algebra.linearMap S _)

Goal state after:
R✝ : Type u_1
S✝ : Type u_2
inst✝⁸ : CommRing R✝
inst✝⁷ : CommRing S✝
inst✝⁶ : Algebra R✝ S✝
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
h✝ : Smooth R S
κ : Type u_2
a : κ → S
b : Module.Basis κ (Localization.AtPrime p) Ω[Localization.AtPrime p⁄R]
hb : ∀ (i : κ), b i = (⇑(map R R S (Localization.AtPrime p)) ∘ ⇑(D R S)) (a i)
e : (κ →₀ S) →ₗ[S] Ω[S⁄R] := Finsupp.linearCombination S fun i ↦ (D R S) (a i)
l₁ : (κ →₀ S) →ₗ[S] κ →₀ Localization.AtPrime p :=
  Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.AtPrime p))
l₂ : Ω[S⁄R] →ₗ[S] Ω[Localization.AtPrime p⁄R] := map R R S (Localization.AtPrime p)
eₚ : (κ →₀ Localization.AtPrime p) →ₗ[Localization.AtPrime p] Ω[Localization.AtPrime p⁄R] :=
  (IsLocalizedModule.mapExtendScalars p.primeCompl l₁ l₂ (Localization.AtPrime p)) e
this✝ : eₚ = ↑b.repr.symm
heₚ : Function.Bijective ⇑eₚ
this : Finite κ
g : S
hg : g ∉ p
h : Function.Bijective ⇑((LocalizedModule.map (Submonoid.powers g)) e)
l₁ₜ : (κ →₀ S) →ₗ[S] κ →₀ Localization.Away g := Finsupp.mapRange.linearMap (Algebra.linearMap S (Localization.Away g))
⊢ ∃ f ∉ p, IsStandardSmooth R (Localization.Away f)
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
⊢ IsStandardSmoothOfRelativeDimension (n + m) (g.comp f)

Tactic:
rw [IsStandardSmoothOfRelativeDimension]
  algebraize [f, g, (g.comp f)]
  exact Algebra.IsStandardSmoothOfRelativeDimension.trans m n R S T

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
inst✝ : Nontrivial S
⊢ D.basis (Sum.inl ()) = D.cotangentEquivProd.symm (cMulXSubOneCotangent S D.gbar, 0)

Tactic:
simpa [basis] using! Generators.basisCotangentAway_apply _ _

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

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

Tactic:
let p := (hU.primeIdealOf ⟨f x, hVU hx⟩).asIdeal

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this : Algebra ↑Γ(Y, U) ↑Γ(X, V) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal ↑Γ(Y, U) := (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    hV.primeIdealOf ⟨x, hx⟩ ∈ Algebra.smoothLocus ↑Γ(Y, U) ↑Γ(X, V)
Module: Mathlib.FieldTheory.SeparablyGenerated

Goal state before:
pp: case refine_1
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F₀.coeff (σ i) = 0
e : ι ≃ Option { b // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this :
  coeff (Finsupp.equivMapDomain e σ).some
      (((optionEquivLeft k { b // b ≠ i }) ((rename ⇑(Equiv.optionSubtypeNe i).symm) F)).coeff
        ((Finsupp.equivMapDomain e σ) none)) =
    coeff (Finsupp.equivMapDomain e σ) ((rename ⇑(Equiv.optionSubtypeNe i).symm) F)
⊢ False

Tactic:
Finsupp.equivMapDomain_eq_mapDomain,

Goal state after:
case refine_1
k : Type u_1
K : Type u_2
ι : Type u_3
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF : ∀ (F' : MvPolynomial ι k), F' ≠ 0 → (aeval a) F' = 0 → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : σ i ≠ 0
H✝ : (F.toPolynomialAdjoinImageCompl a i).coeff (σ i) = 0
F₀ : Polynomial (MvPolynomial { b // b ≠ i } k) :=
  (optionEquivLeft k { b // b ≠ i }) ((renameEquiv k (Equiv.optionSubtypeNe i).symm) F)
H : F₀.coeff (σ i) = 0
e : ι ≃ Option { b // b ≠ i } := (Equiv.optionSubtypeNe i).symm
this :
  coeff (Finsupp.mapDomain (⇑e) σ).some
      (((optionEquivLeft k { b // b ≠ i }) ((rename ⇑(Equiv.optionSubtypeNe i).symm) F)).coeff
        ((Finsupp.mapDomain (⇑e) σ) none)) =
    coeff (Finsupp.mapDomain (⇑e) σ) ((rename ⇑(Equiv.optionSubtypeNe i).symm) F)
⊢ False
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}
this : ¬AlgebraicIndependent k a
⊢ S.Nonempty

Tactic:
simpa [S, algebraicIndependent_iff, and_comm] using! this

Goal state after:
Module: Mathlib.RingTheory.Algebraic.StronglyTranscendental

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid R
inst✝¹ : IsLocalization M S
inst✝ : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : (aeval x) p * t = 0
a : R
ha₁ : a ∈ M
ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p
H : (aeval x) (IsLocalization.integerNormalization M p) = a • (aeval x) p
this : map (algebraMap R T) (IsLocalization.integerNormalization M p) * C t = 0
⊢ map (algebraMap S T) p * C t = 0

Tactic:
IsScalarTower.algebraMap_eq R S T,

Goal state after:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : CommRing T
inst✝³ : Algebra R T
inst✝² : Algebra S T
M : Submonoid R
inst✝¹ : IsLocalization M S
inst✝ : IsScalarTower R S T
x : T
h : IsStronglyTranscendental R x
t : T
p : S[X]
hp : (aeval x) p * t = 0
a : R
ha₁ : a ∈ M
ha₂ : map (algebraMap R S) (IsLocalization.integerNormalization M p) = a • p
H : (aeval x) (IsLocalization.integerNormalization M p) = a • (aeval x) p
this : map ((algebraMap S T).comp (algebraMap R S)) (IsLocalization.integerNormalization M p) * C t = 0
⊢ map (algebraMap S T) p * C t = 0
Module: Mathlib.RingTheory.IntegralClosure.GoingDown

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Algebra.IsIntegral R S
inst✝² : IsIntegrallyClosed R
this✝ : IsDomain R
p : Ideal R
inst✝¹ : p.IsPrime
Q : Ideal S
inst✝ : Q.IsPrime
hpQ : p < Ideal.under R Q
SQ : Type u_2 := Localization.AtPrime Q
this : Ideal.comap (algebraMap R SQ) (Ideal.map (algebraMap R SQ) p) ≤ p
P : Ideal SQ
hP : P.IsPrime
e : Ideal.comap (algebraMap R SQ) P = p
⊢ p = Ideal.under R (Ideal.under S P)

Tactic:
by rw [Ideal.under_under, ← e]

Goal state after:
Module: Mathlib.RingTheory.LocalRing.ResidueField.Polynomial

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
I : Ideal R
inst✝⁴ : I.IsPrime
J : Ideal R[X]
inst✝³ : J.IsPrime
inst✝² : J.LiesOver I
inst✝¹ : Algebra (Localization.AtPrime I) (Localization.AtPrime J)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra I J
hJ : J = Ideal.map C I
f : J.ResidueField →+* RatFunc I.ResidueField :=
  Ideal.ResidueField.lift J
    ((algebraMap I.ResidueField[X] (RatFunc I.ResidueField)).comp (mapRingHom (algebraMap R I.ResidueField))) ⋯ ⋯
hf : f.comp (algebraMap I.ResidueField J.ResidueField) = algebraMap I.ResidueField (RatFunc I.ResidueField)
x✝ : I.ResidueField[X]
x : I.ResidueField[X]
hx : (aeval ((algebraMap R[X] J.ResidueField) X)) x = 0
r : R[X]
hr : map (Ideal.Quotient.mk I) r = IsLocalization.integerNormalization (R ⧸ I)⁰ x
s : R
hb0 : (Ideal.Quotient.mk I) s ∈ (R ⧸ I)⁰
hb :
  map (algebraMap (R ⧸ I) I.ResidueField) (IsLocalization.integerNormalization (R ⧸ I)⁰ x) = (Ideal.Quotient.mk I) s • x
⊢ s ∉ I

Tactic:
by simpa [Ideal.Quotient.eq_zero_iff_mem] using! hb0

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
P : Ideal R[X]
inst✝ : P.IsPrime
⊢ ¬Algebra.WeaklyQuasiFiniteAt R P

Tactic:
intro H
  wlog hR : IsField R
  · let p := P.under R
    obtain ⟨Q, hQ⟩ := (PrimeSpectrum.preimageEquivFiber R R[X]
        ⟨p, inferInstance⟩).symm.surjective ⟨⟨P, ‹_›⟩, rfl⟩
    have inst : Algebra.WeaklyQuasiFiniteAt p.ResidueField Q.asIdeal :=
      .baseChange P Q.asIdeal congr($(hQ.symm).1.1)
    exact this (Q.asIdeal.comap (polyEquivTensor' R p.ResidueField).toRingHom)
      inferInstance (Field.toIsField _)
  let := hR.toField
  have := Module.Finite.of_injective
    (IsScalarTower.toAlgHom R R[X] (Localization.AtPrime P)).toLinearMap
    (IsLocalization.injective _ P.primeCompl_le_nonZeroDivisors)
  exact transcendental_X R (Algebra.IsIntegral.isIntegral X).isAlgebraic

Goal state after:
Module: Mathlib.RingTheory.QuasiFinite.Weakly

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
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
q : Ideal T
inst✝¹ : q.IsPrime
inst✝ : WeaklyQuasiFiniteAt R q
⊢ WeaklyQuasiFiniteAt S q

Tactic:
have : Algebra.QuasiFiniteAt S (q.map (Ideal.Quotient.mk ((q.under R).map (algebraMap R T)))) :=
    .of_restrictScalars R _ _
  have H : (q.under R).map (algebraMap R T) ≤ (q.under S).map (algebraMap S T) := by
    simpa [Ideal.under, IsScalarTower.algebraMap_eq R S T, ← Ideal.map_map,
      ← Ideal.comap_comap, -Ideal.under_under] using Ideal.map_mono Ideal.map_comap_le
  delta WeaklyQuasiFiniteAt
  refine .of_surjectiveOnStalks (q.map (Ideal.Quotient.mk ((q.under R).map (algebraMap R T))))
    (Ideal.quotientMapₐ _ (.id _ _) (by exact H)) (RingHom.surjectiveOnStalks_of_surjective
      (Ideal.quotientMap_surjective (H := by exact H) Function.surjective_id)) _ ?_
  apply Ideal.comap_injective_of_surjective _ Ideal.Quotient.mk_surjective
  rw [Ideal.comap_comap, Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective]
  refine .trans ?_ (Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective _).symm
  simp [← RingHom.ker_eq_comap_bot, Ideal.map_comap_le]

Goal state after: