mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing T
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra S T
inst✝⁵ : Algebra R T
inst✝⁴ : IsScalarTower R S T
p : Ideal R
P : Ideal S
I : Ideal T
inst✝³ : p.IsMaximal
inst✝² : P.IsMaximal
inst✝¹ : P.LiesOver p
inst✝ : I.LiesOver P
⊢ p.inertiaDeg' I = p.inertiaDeg' P * P.inertiaDeg' I

Tactic:
have h₁ := P.over_def p
  have h₂ := I.over_def P
  have h₃ := (LiesOver.trans I P p).over
  simp only [inertiaDeg', dif_pos h₁.symm, dif_pos h₂.symm, dif_pos h₃.symm]
  let : Algebra (R ⧸ p) (S ⧸ P) := Ideal.Quotient.algebraQuotientOfLEComap h₁.le
  let : Algebra (S ⧸ P) (T ⧸ I) := Ideal.Quotient.algebraQuotientOfLEComap h₂.le
  let : Algebra (R ⧸ p) (T ⧸ I) := Ideal.Quotient.algebraQuotientOfLEComap h₃.le
  let : IsScalarTower (R ⧸ p) (S ⧸ P) (T ⧸ I) := IsScalarTower.of_algebraMap_eq <| by
    rintro ⟨x⟩; exact congr_arg _ (IsScalarTower.algebraMap_apply R S T x)
  exact (finrank_mul_finrank (R ⧸ p) (S ⧸ P) (T ⧸ I)).symm

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ ∀ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    x ∉ (normalizedFactors b).toFinset → id x ^ Multiset.count x (normalizedFactors b) = 1

Tactic:
simp only [Multiset.mem_toFinset]

Goal state after:
case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ ∀ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    x ∉ normalizedFactors b → id x ^ Multiset.count x (normalizedFactors b) = 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicative

Goal state before:
pp: case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ ∀ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    x ∉ (normalizedFactors a).toFinset → id x ^ Multiset.count x (normalizedFactors a) = 1

Tactic:
simp only [Multiset.mem_toFinset]

Goal state after:
case e_a.e_a
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
β : Type u_3
inst✝ : CommMonoidWithZero β
f : α → β
a b : α
h0 : f 0 = 0
h1 : ∀ {x y : α}, IsUnit y → f (x * y) = f x * f y
hpr : ∀ {p : α} (i : ℕ), Prime p → f (p ^ i) = f p ^ i
hcp : ∀ {x y : α}, IsRelPrime x y → f (x * y) = f x * f y
this✝² : DecidableEq α := Classical.decEq α
ha0 : ¬a = 0
hb0 : ¬b = 0
hf1 : ¬f 1 = 0
this✝¹ : Nontrivial α
this✝ : StrongNormalizationMonoid α := UniqueFactorizationMonoid.strongNormalizationMonoid
this :
  f
      (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
        p ^ (Multiset.count p (normalizedFactors a) + Multiset.count p (normalizedFactors b))) =
    f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors a)) *
      f
        (∏ p ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
          p ^ Multiset.count p (normalizedFactors b))
ua : αˣ
a_eq : (normalizedFactors a).prod * ↑ua = a
ub : αˣ
b_eq : (normalizedFactors b).prod * ↑ub = b
⊢ ∀ x ∈ (normalizedFactors a).toFinset ∪ (normalizedFactors b).toFinset,
    x ∉ normalizedFactors a → id x ^ Multiset.count x (normalizedFactors a) = 1
Module: Mathlib.RingTheory.Localization.InvSubmonoid

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : ↥M
⊢ ↑((toInvSubmonoid M S) x) = mk' S 1 x

Tactic:
rw [← (IsLocalization.map_units S x).mul_left_inj]
  simp

Goal state after:
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous[inst✝¹, inst✝] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ {x} = f ⁻¹' f '' {x}

Tactic:
Set.preimage_image_eq _ hf

Goal state after:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Function.Injective f
hf' : Continuous[inst✝¹, inst✝] f
x : X
hx : x ∈ f ⁻¹' closedPoints Y
⊢ {x} = {x}
Module: Mathlib.Topology.JacobsonSpace

Goal state before:
pp: case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst✝] (closure[inst✝] Z \ Z)
e : Z ∩ closedPoints X = ∅
this : Z ⊆ closure[inst✝] Z \ Z
⊢ False

Tactic:
rw [Set.subset_sdiff, disjoint_self, Set.bot_eq_empty] at this

Goal state after:
case mp
X : Type u_1
inst✝ : TopologicalSpace X
H : ∀ {Z : Set X}, IsClosed[inst✝] Z → closure[inst✝] (Z ∩ closedPoints X) = Z
Z : Set X
hZ : Z ≠ ∅
hZ' : IsClosed[inst✝] (closure[inst✝] Z \ Z)
e : Z ∩ closedPoints X = ∅
this : Z ⊆ closure[inst✝] Z ∧ Z = ∅
⊢ False
Module: Mathlib.RingTheory.RamificationInertia.Inertia

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
q : Ideal S
inst✝⁴ : q.IsPrime
inst✝³ : q.LiesOver (under R q)
inst✝² : (under R q).IsPrime
inst✝¹ : Algebra (Localization.AtPrime (under R q)) (Localization.AtPrime q)
inst✝ : Localization.AtPrime.IsLiesOverAlgebra (under R q) q
⊢ q.inertiaDeg R = Module.finrank (under R q).ResidueField q.ResidueField

Tactic:
exact inertiaDeg_def q R

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : IsNoetherianRing S
hpP : map f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H : map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
h₂ : map (algebraMap S (Localization.AtPrime P)) (map f p) ≤ map (algebraMap S (Localization.AtPrime P)) (P ^ 2)
⊢ False

Tactic:
rw [Ideal.map_pow, Localization.AtPrime.map_eq_maximalIdeal, Ideal.map_map,
    ← IsScalarTower.algebraMap_eq, H, pow_two] at h₂

Goal state after:
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : IsNoetherianRing S
hpP : map f p ≤ P
hp : P ≠ ⊥
hp' : P.primeCompl ≤ nonZeroDivisors S
H : map (algebraMap R (Localization.AtPrime P)) p = maximalIdeal (Localization.AtPrime P)
h₂ :
  maximalIdeal (Localization.AtPrime P) ≤
    maximalIdeal (Localization P.primeCompl) * maximalIdeal (Localization P.primeCompl)
⊢ False
Module: Mathlib.RingTheory.Unramified.Basic

Goal state before:
pp: R : Type v
inst✝⁵ : CommRing R
A : Type u
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
B : Type w
inst✝² : CommRing B
inst✝¹ : Algebra R B
I : Ideal B
inst✝ : FormallyUnramified R A
hI : ⨅ i, I ^ i = ⊥
g₁ g₂ : A →ₐ[R] B
H : ∀ (x : A), (Ideal.Quotient.mk I) (g₁ x) = (Ideal.Quotient.mk I) (g₂ x)
⊢ g₁ = g₂

Tactic:
have (i : ℕ) :
      (Ideal.Quotient.mkₐ R (I ^ i)).comp g₁ = (Ideal.Quotient.mkₐ R (I ^ i)).comp g₂ := by
    by_cases hi : i = 0
    · ext x
      have : Subsingleton (B ⧸ I ^ i) := by
        rw [hi, pow_zero, Ideal.one_eq_top]
        infer_instance
      exact Subsingleton.elim _ _
    apply ext (I.map (algebraMap _ _)) ⟨i, by simp [← Ideal.map_pow]⟩
    intro x
    dsimp
    rw [Ideal.Quotient.eq, ← map_sub, ← Ideal.mem_comap, Ideal.comap_map_of_surjective',
      sup_eq_left.mpr, ← Ideal.Quotient.eq]
    · exact H _
    · simpa using Ideal.pow_le_self hi
    · exact Ideal.Quotient.mk_surjective
  ext x
  rw [← sub_eq_zero, ← Ideal.mem_bot, ← hI, Ideal.mem_iInf]
  intro i
  rw [← Ideal.Quotient.eq_zero_iff_mem, map_sub, sub_eq_zero]
  exact DFunLike.congr_fun (this i) x

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Ramification

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing T
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra S T
inst✝⁹ : Algebra R T
inst✝⁸ : IsScalarTower R S T
inst✝⁷ : IsDedekindDomain S
inst✝⁶ : IsDedekindDomain T
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : P.LiesOver p
hp : p ≠ ⊥
this✝ : P.IsPrime
this : IsTorsionFree R T
⊢ p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q

Tactic:
have hP : P ≠ ⊥ := ne_bot_of_liesOver_of_ne_bot hp _

Goal state after:
case inr
R : Type u_1
S : Type u_2
T : Type u_3
inst✝¹⁴ : CommRing R
inst✝¹³ : CommRing S
inst✝¹² : CommRing T
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Algebra S T
inst✝⁹ : Algebra R T
inst✝⁸ : IsScalarTower R S T
inst✝⁷ : IsDedekindDomain S
inst✝⁶ : IsDedekindDomain T
inst✝⁵ : IsDomain R
inst✝⁴ : IsTorsionFree R S
inst✝³ : IsTorsionFree S T
p : Ideal R
P : Ideal S
Q : Ideal T
inst✝² : Q.IsPrime
inst✝¹ : Q.LiesOver P
inst✝ : P.LiesOver p
hp : p ≠ ⊥
this✝ : P.IsPrime
this : IsTorsionFree R T
hP : P ≠ ⊥
⊢ p.ramificationIdx' Q = p.ramificationIdx' P * P.ramificationIdx' Q
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : QuasiFinite R S
inst✝¹ : IsArtinianRing R
inst✝ : IsLocalRing R
e : (maximalIdeal R).Fiber S ≃ₐ[R] S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R) :=
  (TensorProduct.congr
        (AlgEquiv.ofBijective (Ideal.Quotient.liftₐ (maximalIdeal R) (ofId R (maximalIdeal R).ResidueField) ⋯) ⋯).symm
        AlgEquiv.refl).trans
    ((TensorProduct.comm R (R ⧸ maximalIdeal R) S).trans
      (AlgEquiv.restrictScalars R (TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)).symm))
this : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
⊢ (RingHom.ker (Ideal.Quotient.mkₐ R (Ideal.map (algebraMap R S) (maximalIdeal R)))).FG

Tactic:
rw [← RingHom.ker_coe_toRingHom, Ideal.Quotient.mkₐ_ker]

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
inst✝² : QuasiFinite R S
inst✝¹ : IsArtinianRing R
inst✝ : IsLocalRing R
e : (maximalIdeal R).Fiber S ≃ₐ[R] S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R) :=
  (TensorProduct.congr
        (AlgEquiv.ofBijective (Ideal.Quotient.liftₐ (maximalIdeal R) (ofId R (maximalIdeal R).ResidueField) ⋯) ⋯).symm
        AlgEquiv.refl).trans
    ((TensorProduct.comm R (R ⧸ maximalIdeal R) S).trans
      (AlgEquiv.restrictScalars R (TensorProduct.quotIdealMapEquivTensorQuot S (maximalIdeal R)).symm))
this : Module.Finite R (S ⧸ Ideal.map (algebraMap R S) (maximalIdeal R))
⊢ (Ideal.map (algebraMap R S) (maximalIdeal R)).FG
Module: Mathlib.RingTheory.QuasiFinite.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
⊢ QuasiFinite R S ↔ ∀ (I : Ideal R), I.IsPrime → (I.primesOver S).Finite

Tactic:
iff_finite_comap_preimage_singleton,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : FiniteType R S
⊢ (∀ (x : PrimeSpectrum R), (PrimeSpectrum.comap (algebraMap R S) ⁻¹' {x}).Finite) ↔
    ∀ (I : Ideal R), I.IsPrime → (I.primesOver S).Finite
Module: Mathlib.RingTheory.Smooth.Basic

Goal state before:
pp: case h₁
R : Type u
A : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R A
B✝ : Type u_1
inst✝³ : CommRing B✝
inst✝² : FormallySmooth R A
I✝ : Ideal B✝
hI✝ : IsNilpotent I✝
B : Type u_1
inst✝¹ : CommRing B
I : Ideal B
hI : I ^ 2 = ⊥
inst✝ : Algebra R B
⊢ Function.Surjective (Ideal.Quotient.mkₐ R I).comp

Tactic:
exact FormallySmooth.comp_surjective R A I hI

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsArtinianRing R
p : PrimeSpectrum S
inst✝ : FiniteType R S
H✝ : IsClopen {p}
this✝ : IsNoetherianRing S
this : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = ↑(PrimeSpectrum.basicOpen e)
hep : e ∉ p.asIdeal
⊢ QuasiFiniteAt R p.asIdeal

Tactic:
let f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal :=
    IsLocalization.Away.liftAlgHom e (f := Algebra.ofId _ _)
      (IsLocalization.map_units (M := p.asIdeal.primeCompl) _ ⟨e, hep⟩)

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : IsArtinianRing R
p : PrimeSpectrum S
inst✝ : FiniteType R S
H✝ : IsClopen {p}
this✝ : IsNoetherianRing S
this : IsJacobsonRing S
e : S
he : IsIdempotentElem e
H : {p} = ↑(PrimeSpectrum.basicOpen e)
hep : e ∉ p.asIdeal
f : Localization.Away e →ₐ[S] Localization.AtPrime p.asIdeal := IsLocalization.Away.liftAlgHom e ⋯
⊢ QuasiFiniteAt R p.asIdeal
Module: Mathlib.RingTheory.Kaehler.JacobiZariski

Goal state before:
pp: case h2
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
⊢ (Q.comp P).toExtension.Ring ∙ z ≤
    Submodule.comap Extension.Cotangent.mk
      (Submodule.restrictScalars (Q.comp P).Ring
        (Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range))

Tactic:
← Submodule.map_le_map_iff_of_injective
      (f := Submodule.subtype _) Subtype.val_injective,

Goal state after:
case h2
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : (Q.comp P).Ring
hx' : x ∈ (Q.comp P).toExtension.ker
y : (Q.comp P).Ring
hy : y ∈ (Q.comp P).ker * (Q.comp P).ker
e : x - y ∈ Ideal.map (Q.toComp P).toAlgHom P.ker
z : ↥(Q.comp P).ker := ⟨x - y, ⋯⟩
hz : ↑z ∈ Ideal.map (Q.toComp P).toAlgHom.toRingHom P.ker
this : Extension.Cotangent.mk ⟨x, hx'⟩ = Extension.Cotangent.mk z
⊢ Submodule.map (Submodule.subtype (Q.comp P).toExtension.ker) ((Q.comp P).toExtension.Ring ∙ z) ≤
    Submodule.map (Submodule.subtype (Q.comp P).toExtension.ker)
      (Submodule.comap Extension.Cotangent.mk
        (Submodule.restrictScalars (Q.comp P).Ring
          (Submodule.span T ↑(Extension.Cotangent.map (Q.toComp P).toExtensionHom).range)))
Module: Mathlib.RingTheory.Unramified.Locus

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ Module.support A Ω[A⁄R] ⊆ (↑(PrimeSpectrum.basicOpen f))ᶜ ↔ FormallyUnramified R (Localization.Away f)

Tactic:
PrimeSpectrum.basicOpen_eq_zeroLocus_compl,

Goal state after:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
⊢ Module.support A Ω[A⁄R] ⊆ (PrimeSpectrum.zeroLocus {f})ᶜᶜ ↔ FormallyUnramified R (Localization.Away f)
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case refine_1.refine_1
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
x✝ : P
hx✝ : x✝ ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
x : P
hx : x ∈ RingHom.ker (algebraMap P S)
y : P
⊢ y ∈ RingHom.ker (algebraMap P S) → 1 ⊗ₜ[P] (D R P) (x • y) = 0

Tactic:
hy

Goal state after:
case refine_1.refine_1
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
x✝ : P
hx✝ : x✝ ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
x : P
hx : x ∈ RingHom.ker (algebraMap P S)
y : P
hy : y ∈ RingHom.ker (algebraMap P S)
⊢ 1 ⊗ₜ[P] (D R P) (x • y) = 0
Module: Mathlib.RingTheory.Smooth.Kaehler

Goal state before:
pp: case refine_1.refine_2
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
x✝ : P
hx✝ : x✝ ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
x y : P
hx : 1 ⊗ₜ[P] (D R P) x = 0
⊢ 1 ⊗ₜ[P] (D R P) y = 0 → 1 ⊗ₜ[P] (D R P) (x + y) = 0

Tactic:
hy

Goal state after:
case refine_1.refine_2
R : Type u_1
P : Type u_2
S : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hf : Surjective ⇑(algebraMap P S)
this : Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) ≤ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P)).ker →
  P ⧸ Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2) →ₗ[R] S ⊗[P] Ω[P⁄R] :=
  (Submodule.restrictScalars R (RingHom.ker (algebraMap P S) ^ 2)).liftQ (↑R ((mk P S Ω[P⁄R]) 1) ∘ₗ ↑(D R P))
x✝ : P
hx✝ : x✝ ∈ RingHom.ker (algebraMap P S) * RingHom.ker (algebraMap P S)
x y : P
hx : 1 ⊗ₜ[P] (D R P) x = 0
hy : 1 ⊗ₜ[P] (D R P) y = 0
⊢ 1 ⊗ₜ[P] (D R P) (x + y) = 0
Module: Mathlib.RingTheory.Unramified.Field

Goal state before:
pp: K : Type u_1
A : Type u_2
inst✝⁶ : Field K
inst✝⁵ : CommRing A
inst✝⁴ : Algebra K A
inst✝³ : FormallyUnramified K A
inst✝² : EssFiniteType K A
inst✝¹ : IsAlgClosed K
inst✝ : IsLocalRing A
⊢ IsField A

Tactic:
rw [IsLocalRing.isField_iff_maximalIdeal_eq, eq_bot_iff]
  intro x hx
  obtain ⟨x, rfl⟩ := (bijective_of_isAlgClosed_of_isLocalRing K A).surjective x
  change _ = 0
  rw [← (algebraMap K A).map_zero]
  by_contra hx'
  exact hx ((isUnit_iff_ne_zero.mpr
    (fun e ↦ hx' ((algebraMap K A).congr_arg e))).map (algebraMap K A))

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

Goal state before:
pp: R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.toExtension.Cotangent
property✝ : x ∈ P.toExtension.cotangentComplex.ker
⊢ (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom) ⟨x, property✝⟩ ∈
    ↑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker

Tactic:
obtain ⟨⟨(x : P.Ring), x_in⟩, rfl⟩ := Extension.Cotangent.mk_surjective x

Goal state after:
R : Type u₁
S : Type u₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type u₃
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
ι : Type w₁
σ : Type w₂
Q : Generators S T ι
P : Generators R S σ
x : P.Ring
x_in : x ∈ P.toExtension.ker
property✝ : Extension.Cotangent.mk ⟨x, x_in⟩ ∈ P.toExtension.cotangentComplex.ker
⊢ (Extension.H1Cotangent.map (Q.toComp P).toExtensionHom) ⟨Extension.Cotangent.mk ⟨x, x_in⟩, property✝⟩ ∈
    ↑(Extension.H1Cotangent.map (Q.ofComp P).toExtensionHom).ker
Module: Mathlib.RingTheory.Etale.Kaehler

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R S
inst✝³ : Algebra R T
inst✝² : Algebra S T
inst✝¹ : IsScalarTower R S T
M : Submonoid S
inst✝ : IsLocalization M T
P : Extension R S := (Generators.self R S).toExtension
M' : Submonoid P.Ring := Submonoid.comap (algebraMap P.Ring S) M
x✝ : ↥M'
y : P.Ring
hy : y ∈ M'
⊢ IsUnit (((IsScalarTower.toAlgHom R S T).comp (IsScalarTower.toAlgHom R P.Ring S)) ↑⟨y, hy⟩)

Tactic:
simpa using IsLocalization.map_units T ⟨algebraMap P.Ring S y, hy⟩

Goal state after: