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

Goal state before:
pp: case inr.inr
R : Type u_1
K : Type u_2
inst✝ : DivisionRing K
⊢ Submodule.IsPrincipal ⊤

Tactic:
· exact top_isPrincipal

Goal state after:
Module: Mathlib.RingTheory.TotallySplit

Goal state before:
pp: n✝ : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n✝ →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n✝ + 1)
h✝ : Nontrivial R
this✝⁴ : Nontrivial S
U : Type u
w✝⁶ : CommRing U
w✝⁵ : Algebra S U
e✝ : S ⊗[R] S ≃ₐ[S] S × U
algInst✝¹ : Algebra (S × U) U := ⋯
this✝³ : IsScalarTower S (S × U) U
this✝² : Etale S U
this✝¹ : Module.Finite S U
this✝ : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n✝ + 1
this : Module.rankAtStalk U = ↑n✝
V : Type u
w✝⁴ : CommRing V
w✝³ : Algebra S V
w✝² : Module.FaithfullyFlat S V
w✝¹ : Module.Finite S V
w✝ : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst✝ : Algebra R V := ⋯
scalarTowerInst✝ : IsScalarTower R S V := ⋯
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V := ⋯
⊢ Function.Surjective (PrimeSpectrum.comap (algebraMap R S))

Tactic:
← PrimeSpectrum.rankAtStalk_pos_iff_comap_surjective

Goal state after:
n✝ : ℕ
ih :
  ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Etale R S] [Module.Finite R S],
    Module.rankAtStalk S = ↑n✝ →
      ∃ T x x_1, ∃ (_ : Module.FaithfullyFlat R T) (_ : Module.Finite R T) (_ : Etale R T), IsFiniteSplit T (T ⊗[R] S)
R S : Type u
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Etale R S
inst✝ : Module.Finite R S
hn : Module.rankAtStalk S = ↑(n✝ + 1)
h✝ : Nontrivial R
this✝⁴ : Nontrivial S
U : Type u
w✝⁶ : CommRing U
w✝⁵ : Algebra S U
e✝ : S ⊗[R] S ≃ₐ[S] S × U
algInst✝¹ : Algebra (S × U) U := (RingHom.snd S U).toAlgebra
this✝³ : IsScalarTower S (S × U) U
this✝² : Etale S U
this✝¹ : Module.Finite S U
this✝ : ∀ (p : PrimeSpectrum S), 1 + Module.rankAtStalk U p = n✝ + 1
this : Module.rankAtStalk U = ↑n✝
V : Type u
w✝⁴ : CommRing V
w✝³ : Algebra S V
w✝² : Module.FaithfullyFlat S V
w✝¹ : Module.Finite S V
w✝ : Etale S V
hV : IsFiniteSplit V (V ⊗[S] U)
n : ℕ
f : V ⊗[S] U ≃ₐ[V] Fin n → V
algInst✝ : Algebra R V := ((algebraMap S V).comp (algebraMap R S)).toAlgebra
scalarTowerInst✝ : IsScalarTower R S V := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R V))
e : V ⊗[R] S ≃ₐ[V] Unit ⊕ Fin n → V :=
  (TensorProduct.cancelBaseChange R S V V S).symm.trans
    ((TensorProduct.congr AlgEquiv.refl e✝).trans
      ((TensorProduct.prodRight S V V S U).trans
        (((TensorProduct.rid S V V).prodCongr f).trans
          (((AlgEquiv.funUnique V Unit V).symm.prodCongr AlgEquiv.refl).trans
            (AlgEquiv.sumArrowEquivProdArrow Unit (Fin n) V V).symm))))
⊢ ∀ (p : PrimeSpectrum R), 0 < Module.rankAtStalk S p
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set A
hS : S ⊆ ↑I
⊢ (SubDPIdeal.span hI S).carrier = span {y | ∃ n, ∃ (_ : n ≠ 0), ∃ x, ∃ (_ : x ∈ S), y = hI.dpow n x}

Tactic:
by
  set J : SubDPIdeal hI := {
    carrier := span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x }
    isSubideal := hI.dpow_span_isSubideal hS
    dpow_mem _ hk _ hz := dpow_mem_span_of_mem_span hI hS hk hz }
  simp only [SubDPIdeal.span, sInf_carrier_def]
  apply le_antisymm
  · have h : J ∈ insert ⊤ {J : hI.SubDPIdeal | S ⊆ ↑J.carrier} :=
      Set.mem_insert_of_mem _
        (fun x hx ↦ subset_span ⟨1, one_ne_zero, x, hx, by rw [hI.dpow_one (hS hx)]⟩)
    refine sInf_le_of_le ⟨J, ?_⟩ (le_refl _)
    simp only [h, ciInf_pos, J]
  · rw [le_iInf₂_iff]
    intro K hK
    have : S ≤ K := by
      simp only [Set.mem_insert_iff, Set.mem_ofPred_eq] at hK
      rcases hK with rfl | hKS
      exacts [hS, hKS]
    rw [span_le]
    rintro y ⟨n, hn, x, hx, rfl⟩
    exact K.dpow_mem n hn x (this hx)

Goal state after:
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a x : A
hx : x ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
n : ℕ
⊢ a ^ n * hI.dpow n x = hI'.dpow n (a * x)

Tactic:
hI'.dpow_mul hx.1,

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a x : A
hx : x ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
n : ℕ
⊢ a ^ n * hI.dpow n x = a ^ n * hI'.dpow n x
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
⊢ IsNilpotent (constantCoeff (![f₀, f₁, f₂] ((fun i ↦ i) ⟨0, ⋯⟩)))

Tactic:
simpa

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

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
⊢ IsNilpotent (constantCoeff (![f₀, f₁, f₂] ((fun i ↦ i) ⟨1, ⋯⟩)))

Tactic:
simpa

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

Goal state before:
pp: case «2»
R : Type u_1
inst✝ : CommRing R
σ : Type u_3
F : FormalGroup R
f₀ f₁ f₂ : MvPowerSeries σ R
h₀ : PowerSeries.HasSubst f₀
h₁ : PowerSeries.HasSubst f₁
h₂ : PowerSeries.HasSubst f₂
aux₁ : HasSubst ![subst ![Y₀, Y₁] F.toPowerSeries, Y₂]
aux₂ : HasSubst ![Y₀, subst ![Y₁, Y₂] F.toPowerSeries]
⊢ IsNilpotent (constantCoeff (![f₀, f₁, f₂] ((fun i ↦ i) ⟨2, ⋯⟩)))

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
⊢ ↑(invOneSubPow S 1) = invUnitsSub 1

Tactic:
simp [invOneSubPow, invUnitsSub]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
d e : ℕ
⊢ invOneSubPow S (d + e) = invOneSubPow S d * invOneSubPow S e

Tactic:
invOneSubPow_eq_inv_one_sub_pow,

Goal state after:
S : Type u_1
inst✝ : CommRing S
d e : ℕ
⊢ (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ (d + e) =
    (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ d * (Units.mkOfMulEqOne (1 - X) (mk 1) ⋯)⁻¹ ^ e
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: Γ : Type u_1
R : Type u_3
V : Type u_4
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : LinearOrder Γ
inst✝³ : IsOrderedCancelAddMonoid Γ
inst✝² : CommRing R
inst✝¹ : CommRing V
inst✝ : Algebra R V
x : V⟦Γ⟧
a b : PowerSeries R
g : Γ
h : 0 < x.orderTop
n : ℕ
hn : ((powerSeriesFamily x (a * b)) n).coeff g ≠ 0
⊢ ∑ x_1 ∈ HasAntidiagonal.antidiagonal n,
      (PowerSeries.coeff x_1.1) a • (PowerSeries.coeff x_1.2) b • ((powers x) n).coeff g ≠
    0

Tactic:
simpa [PowerSeries.coeff_mul, sum_smul, mul_smul, h] using hn

Goal state after:
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: case inr.right
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h✝ : Nontrivial A
this : ((binomialFamily x r) 0).coeff 0 = 1
⊢ (binomialFamily x r).hsum.leadingCoeff = 1

Tactic:
← this

Goal state after:
case inr.right
Γ : Type u_1
R : Type u_2
A : Type u_3
inst✝⁶ : LinearOrder Γ
inst✝⁵ : AddCommMonoid Γ
inst✝⁴ : IsOrderedCancelAddMonoid Γ
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : A⟦Γ⟧
hx : 0 < (x - 1).orderTop
r : R
h✝ : Nontrivial A
this : ((binomialFamily x r) 0).coeff 0 = 1
⊢ (binomialFamily x r).hsum.leadingCoeff = ((binomialFamily x r) 0).coeff 0
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝² : PartialOrder Γ
inst✝¹ : AddCommMonoid R
M : Type ?u.14
inst✝ : SMulZeroClass M R
r : M
t : SummableFamily Γ R β
g : Γ
⊢ {a | ((r • ⇑t) a).coeff g ≠ 0} ⊆ Function.support fun a ↦ (t a).coeff g

Tactic:
intro i hi

Goal state after:
Γ : Type u_1
Γ' : Type u_2
R : Type u_3
V : Type u_4
α : Type u_5
β : Type u_6
inst✝² : PartialOrder Γ
inst✝¹ : AddCommMonoid R
M : Type ?u.14
inst✝ : SMulZeroClass M R
r : M
t : SummableFamily Γ R β
g : Γ
i : β
hi : i ∈ {a | ((r • ⇑t) a).coeff g ≠ 0}
⊢ i ∈ Function.support fun a ↦ (t a).coeff g
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ᶠ (i : α × β), ∑ x ∈ VAddAntidiagonal g ⋯, (s i.1).coeff x.1 • (t i.2).coeff x.2 =
    ∑ x ∈ VAddAntidiagonal g ⋯,
      ∑ x_1 ∈ (t.coeff x.2).support, (∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1) • (t x_1).coeff x.2

Tactic:
Finset.sum_smul

Goal state after:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
β : Type u_6
inst✝⁶ : PartialOrder Γ
inst✝⁵ : PartialOrder Γ'
inst✝⁴ : VAdd Γ Γ'
inst✝³ : IsOrderedCancelVAdd Γ Γ'
R : Type u_7
V : Type u_8
inst✝² : Semiring R
inst✝¹ : AddCommMonoid V
inst✝ : Module R V
s : SummableFamily Γ R α
t : SummableFamily Γ' V β
g : Γ'
⊢ ∑ᶠ (i : α × β), ∑ x ∈ VAddAntidiagonal g ⋯, (s i.1).coeff x.1 • (t i.2).coeff x.2 =
    ∑ x ∈ VAddAntidiagonal g ⋯,
      ∑ x_1 ∈ (t.coeff x.2).support, ∑ i ∈ (s.coeff x.1).support, (s i).coeff x.1 • (t x_1).coeff x.2
Module: Mathlib.RingTheory.Ideal.MonicSpan

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
p : Ideal R[X]
ism : (comap C p).IsMaximal
ne : p ≠ Ideal.map C (comap C p)
q : Ideal R := comap C p
this : Field (R ⧸ q) := Quotient.field q
ne' : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p ≠ ⊥
y : (R ⧸ q)[X]
mony : y.Monic
hy : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p = span {y}
⊢ ∃ f, f.Monic ∧ p = Ideal.map C (comap C p) ⊔ span {f}

Tactic:
have : y ∈ lifts (Ideal.Quotient.mk q) := map_surjective _ Ideal.Quotient.mk_surjective _

Goal state after:
R : Type u_1
inst✝ : CommRing R
p : Ideal R[X]
ism : (comap C p).IsMaximal
ne : p ≠ Ideal.map C (comap C p)
q : Ideal R := comap C p
this✝ : Field (R ⧸ q) := Quotient.field q
ne' : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p ≠ ⊥
y : (R ⧸ q)[X]
mony : y.Monic
hy : Ideal.map (mapRingHom (Ideal.Quotient.mk q)) p = span {y}
this : y ∈ lifts (Ideal.Quotient.mk q)
⊢ ∃ f, f.Monic ∧ p = Ideal.map C (comap C p) ⊔ span {f}
Module: Mathlib.RingTheory.IdealFilter.Topology

Goal state before:
pp: A : Type u_1
inst✝ : Ring A
F : IdealFilter A
x✝ : ∃ B, B.sets = {x | ∃ I ∈ F, ↑I = x}
B : RingFilterBasis A
hB : B.sets = {x | ∃ I ∈ F, ↑I = x}
I : Ideal A
hI : I ∈ F
a : A
⊢ ↑I ∈ {x | ∃ I ∈ F, ↑I = x}

Tactic:
simpa

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

Goal state before:
pp: case directed
A : Type u_1
inst✝ : Ring A
F G : IdealFilter A
⊢ DirectedOn (fun x1 x2 ↦ x1 ≥ x2) {L | ∃ K ∈ G, F.IsTorsionQuot L K}

Tactic:
rintro I ⟨K, hK, hIK⟩ J ⟨L, hL, hJL⟩
    refine ⟨I ⊓ J, ?_, inf_le_left, inf_le_right⟩
    exact ⟨K ⊓ L, G.inf_mem hK hL,
      (hIK.anti_right inf_le_left).inf (hJL.anti_right inf_le_right)⟩

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes
⊢ (IsLocalRing.maximalIdeal R).height ≤ 1

Tactic:
refine Ideal.height_le_iff.mpr fun q h₁ h₂ ↦ ?_
  suffices q.height = 0 by rw [this]; exact zero_lt_one
  rw [← WithBot.coe_inj,
    ← IsLocalization.AtPrime.ringKrullDim_eq_height q (Localization.AtPrime q),
    WithBot.coe_zero, ← ringKrullDimZero_iff_ringKrullDim_eq_zero,
    ← isArtinianRing_iff_krullDimLE_zero, isArtinianRing_iff_isNilpotent_maximalIdeal,
    ← Localization.AtPrime.map_eq_maximalIdeal]
  have : IsArtinianRing (R ⧸ I) :=
    IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRing I hp
  let f := algebraMap R (Localization.AtPrime q)
  let qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
    { toFun n := ((q.map f ^ n).comap f).map (Ideal.Quotient.mk I)
      monotone' i j e := Ideal.map_mono (Ideal.comap_mono (Ideal.pow_le_pow_right e)) }
  obtain ⟨n, hn⟩ := IsArtinian.monotone_stabilizes qs
  refine ⟨n, ?_⟩
  apply Submodule.eq_bot_of_le_smul_of_le_jacobson_bot (q.map f) _ (IsNoetherian.noetherian _)
  rotate_left
  · rw [IsLocalRing.jacobson_eq_maximalIdeal, Localization.AtPrime.map_eq_maximalIdeal]
    exact bot_ne_top
  rw [smul_eq_mul, ← pow_succ',
    ← (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)).map_rel_iff]
  refine Submodule.le_of_le_smul_of_le_jacobson_bot (I := I) (IsNoetherian.noetherian _) ?_ ?_
  · rw [IsLocalRing.jacobson_eq_maximalIdeal]
    exacts [hp.le, bot_ne_top]
  · replace hn := congr(Ideal.comap (Ideal.Quotient.mk I) $(hn _ n.le_succ))
    simp only [qs, OrderHom.coe_mk, ← RingHom.ker_eq_comap_bot, Ideal.mk_ker,
      Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective] at hn
    intro x hx
    obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp (hn.le (Ideal.mem_sup_left hx))
    refine Submodule.add_mem_sup hy ?_
    obtain ⟨z, rfl⟩ := (Submodule.IsPrincipal.mem_iff_eq_smul_generator I).mp hz
    rw [smul_eq_mul, smul_eq_mul, mul_comm]
    refine Ideal.mul_mem_mul ?_ (Submodule.IsPrincipal.generator_mem _)
    dsimp [IsLocalization.orderEmbedding] at hx
    rwa [Ideal.mem_comap, f.map_add, f.map_mul, Ideal.add_mem_iff_right _
      (Ideal.pow_le_pow_right n.le_succ hy), mul_comm, Ideal.unit_mul_mem_iff_mem] at hx
    refine IsLocalization.map_units (M := q.primeCompl) _ ⟨_, ?_⟩
    change Submodule.IsPrincipal.generator I ∉ (↑q : Set R)
    rw [← Set.singleton_subset_iff, ← Ideal.span_le, Ideal.span_singleton_generator]
    exact fun e ↦ h₂.not_ge (hp.2 ⟨h₁, e⟩ h₂.le)

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
hx' : ¬IsUnit x
⊢ span {x} ≠ ⊤

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
x : PrimeSpectrum A
m : M
hm : ∀ (r : A), r • m = 0 → r ∈ x.asIdeal
r : R
e : r • m = 0
⊢ (algebraMap R A) r • m = 0

Tactic:
simpa

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits

Goal state before:
pp: P : ProfiniteGrp.{u}
x : ↑P.toProfinite.toTop
h : x ∈ (Hom.hom P.toLimit).ker
xne1 : ¬x = 1
H : OpenNormalSubgroup ↑P.toProfinite.toTop
hH : ↑H ⊆ {x}ᶜ
⊢ False

Tactic:
exact hH ((QuotientGroup.eq_one_iff x).mp (congrFun (Subtype.val_inj.mpr h) H)) rfl

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Set R
hs : s.Finite
hI : p ∈ (span s).minimalPrimes
⊢ p ∈ (span ↑hs.toFinset).minimalPrimes

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
hI : I ≠ ⊤
⊢ I.height ≤ Cardinal.toENat (Submodule.spanRank I)

Tactic:
by
  obtain ⟨J, hJ⟩ := nonempty_minimalPrimes hI
  rw [I.height_eq_inf_minimalPrimes]
  exact (iInf₂_le J hJ).trans (I.height_le_spanRank_toENat_of_mem_minimalPrimes J hJ)

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
r : R
p : Ideal R
inst✝ : p.IsPrime
hrm : r ∈ p
⊢ {r} ⊆ ↑p

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
r : R
p : Ideal R
inst✝ : p.IsPrime
hrp : r ∈ p
⊢ {r} ⊆ ↑?m.31

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: case h
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
q : LTSeries ↑(support R M)
m : Ideal R
hmm : m.IsMaximal
hm : (↑(RelSeries.last q)).asIdeal ≤ m
hlt : (↑(RelSeries.last q)).asIdeal < m
⊢ q.length ≤ (RelSeries.snoc q ⟨{ asIdeal := m, isPrime := ⋯ }, ⋯⟩ hlt).length ∧
    (↑(RelSeries.snoc q ⟨{ asIdeal := m, isPrime := ⋯ }, ⋯⟩ hlt).last).asIdeal.IsMaximal

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommRing R
inst✝⁶ : IsNoetherianRing R
S : Type u_2
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
inst✝³ : IsNoetherianRing S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
⊢ P.height ≤ p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height

Tactic:
obtain ⟨s, hp, heq⟩ := p.exists_finset_card_eq_height_of_isNoetherianRing
  let P' := P.map (Ideal.Quotient.mk <| p.map (algebraMap R S))
  obtain ⟨s', hP', heq'⟩ := P'.exists_finset_card_eq_height_of_isNoetherianRing
  have hsP'sub : (s' : Set <| S ⧸ (Ideal.map (algebraMap R S) p)) ⊆ (P' : Set <| S ⧸ _) :=
    fun x hx ↦ hP'.le (Ideal.subset_span hx)
  have : Set.SurjOn (Ideal.Quotient.mk (p.map (algebraMap R S))) P s' := by
    refine Set.SurjOn.mono subset_rfl hsP'sub fun x hx ↦ ?_
    obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective x
    rw [SetLike.mem_coe, Ideal.mem_quotient_iff_mem] at hx
    · use y, hx
    · rw [Ideal.map_le_iff_le_comap, Ideal.LiesOver.over (p := p) (P := P)]
  obtain ⟨o, ho, hinj, himgo⟩ := s'.exists_subset_injOn_image_eq_of_surjOn (P : Set S) this
  let t : Finset S := Finset.image (algebraMap R S) s ∪ o
  suffices h : P.height ≤ t.card by
    rw [← heq, ← heq']
    apply le_trans h
    norm_cast
    refine le_trans (Finset.card_union_le _ _) (add_le_add Finset.card_image_le ?_)
    rw [← himgo, Finset.card_image_of_injOn hinj]
  refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_
  have : Ideal.span t = Ideal.map (algebraMap R S) (.span s) ⊔ .span o := by
    simp [t, Ideal.map_span]
  refine this ▸ map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes hp (span_le.mpr ho) ?_
  convert! hP'
  simp [Ideal.map_span, ← himgo]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.LTSeries

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
x : R
n : ℕ
hn :
  ∀ (p : LTSeries (PrimeSpectrum R)),
    x ∈ (RelSeries.last p).asIdeal →
      p.length = n →
        ∃ q,
          x ∈ (q.toFun 1).asIdeal ∧
            n = q.length ∧ RelSeries.head p = RelSeries.head q ∧ RelSeries.last p = RelSeries.last q
p : LTSeries (PrimeSpectrum R)
hx✝ : x ∈ (RelSeries.last p).asIdeal
hp : p.length = n + 1
h0 : ¬n = 0
q : PrimeSpectrum R
hxq : x ∈ q.asIdeal
h2 : p.toFun ⟨p.length - 2, ⋯⟩ < q
hq : q < RelSeries.last p
Q : LTSeries (PrimeSpectrum R)
hx : x ∈ (Q.toFun 1).asIdeal
hQ : n = Q.length
hh : ((RelSeries.eraseLast p).eraseLast.snoc q h2).head = RelSeries.head Q
hl : ((RelSeries.eraseLast p).eraseLast.snoc q h2).last = RelSeries.last Q
h1 : 1 < Q.length + 1
h : 1 = Fin.castSucc 1
⊢ n + 1 = (RelSeries.snoc Q (RelSeries.last p) ⋯).length

Tactic:
simpa

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
x : M
hp : ({x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical).IsPrime
⊢ ({x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical) ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t

Tactic:
obtain ⟨q, hq1, hq2⟩ := eq_inf_of_isPrime_inf hp

Goal state after:
case mpr
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
h : ∀ (x : M), (N.colon {x}).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
x : M
hp : ({x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical).IsPrime
q : Submodule R M
hq1 : q ∈ {x_1 ∈ t | x ∉ x_1}
hq2 : (q.colon Set.univ).radical = {x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical
⊢ ({x_1 ∈ t | x ∉ x_1}.inf fun q ↦ (q.colon Set.univ).radical) ∈ (fun J ↦ (J.colon Set.univ).radical) '' ↑t
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h : Ideal.span (Set.range f) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
⊢ ∃ i, f i ∉ q

Tactic:
rw [← PrimeSpectrum.iSup_basicOpen_eq_top_iff] at h

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
f : ι → S
h : ⨆ i, PrimeSpectrum.basicOpen (f i) = ⊤
T : ι → Type u_4
inst✝⁵ : (i : ι) → CommSemiring (T i)
inst✝⁴ : (i : ι) → Algebra R (T i)
inst✝³ : (i : ι) → Algebra S (T i)
inst✝² : ∀ (i : ι), IsScalarTower R S (T i)
inst✝¹ : ∀ (i : ι), IsLocalization.Away (f i) (T i)
inst✝ : ∀ (i : ι), IsLocalIso R (T i)
q : Ideal S
hq : q.IsPrime
⊢ ∃ i, f i ∉ q
Module: Mathlib.RingTheory.LocalIso

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Set S
h✝ : Ideal.span s = ⊤
h : ∀ x ∈ s, IsLocalIso R (Localization.Away x)
⊢ Ideal.span (Set.range fun i ↦ ↑i) = ⊤

Tactic:
simpa

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

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
⊢ (ResidueField R)[(residue S) β] = ⊤ → R[β] = ⊤

Tactic:
intro hβ

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝⁷ : CommRing R
inst✝⁶ : CommRing S
inst✝⁵ : Algebra R S
inst✝⁴ : IsLocalRing S
inst✝³ : IsLocalRing R
inst✝² : Module.Finite R S
inst✝¹ : FaithfulSMul R S
inst✝ : FormallyUnramified R S
β : S
hβ : (ResidueField R)[(residue S) β] = ⊤
⊢ R[β] = ⊤