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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ ↑P.cotangentExtendScalarsEquiv ∘ₗ
      h1Cotangentι ∘ₗ
        H1Cotangent.map (defaultHom P.Ring S P.extendScalars) ∘ₗ
          H1Cotangent.map ((Generators.self R S).defaultHom (Generators.self P.Ring S)).toExtensionHom =
    h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P)

Tactic:
← (H1Cotangent.map P.extendScalars.defaultHom).restrictScalars_self,

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ ↑P.cotangentExtendScalarsEquiv ∘ₗ
      h1Cotangentι ∘ₗ
        ↑S (H1Cotangent.map (defaultHom P.Ring S P.extendScalars)) ∘ₗ
          H1Cotangent.map ((Generators.self R S).defaultHom (Generators.self P.Ring S)).toExtensionHom =
    h1Cotangentι ∘ₗ H1Cotangent.map (defaultHom R S P)
Module: Mathlib.RingTheory.Extension.ExtendScalars

Goal state before:
pp: case e_f
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ H1Cotangent.δ R P.Ring S = P.cotangentComplex ∘ₗ ↑P.h1CotangentEquivCotangent

Tactic:
P.cotangentComplex_comp_h1CotangentEquivCotangent

Goal state after:
case e_f
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : Extension R S
⊢ H1Cotangent.δ R P.Ring S = H1Cotangent.δ R P.Ring S
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : hI.DPMorphism hJ
x✝ : ℕ
hn : x✝ ≠ 0
a : A
⊢ f.toRingHom a = 0 → a ∈ I → f.toRingHom (hI.dpow x✝ a) = 0 ∧ hI.dpow x✝ a ∈ I

Tactic:
intro ha

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
I : Ideal A
hI : DividedPowers I
B : Type u_2
inst✝ : CommRing B
J : Ideal B
hJ : DividedPowers J
f : hI.DPMorphism hJ
x✝ : ℕ
hn : x✝ ≠ 0
a : A
ha : f.toRingHom a = 0
⊢ a ∈ I → f.toRingHom (hI.dpow x✝ a) = 0 ∧ hI.dpow x✝ a ∈ I
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case mul
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x✝ x y : A
hx✝ : x ∈ Subsemiring.closure s
hy✝ : y ∈ Subsemiring.closure s
h₁ : ∀ (i : ι), ↑(((decompose 𝒜) x) i) ∈ Subsemiring.closure s
h₂ : ∀ (i : ι), ↑(((decompose 𝒜) y) i) ∈ Subsemiring.closure s
i : ι
⊢ ↑(DFinsupp.sum ((decompose 𝒜) x) fun i₁ b ↦
        (DFinsupp.sum ((decompose 𝒜) y) fun x aj ↦ (of (fun i ↦ ↥(𝒜 i)) (i₁ + x)) (GradedMonoid.GMul.mul b aj)) i) ∈
    Subsemiring.closure s

Tactic:
DFinsupp.sum,

Goal state after:
case mul
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x✝ x y : A
hx✝ : x ∈ Subsemiring.closure s
hy✝ : y ∈ Subsemiring.closure s
h₁ : ∀ (i : ι), ↑(((decompose 𝒜) x) i) ∈ Subsemiring.closure s
h₂ : ∀ (i : ι), ↑(((decompose 𝒜) y) i) ∈ Subsemiring.closure s
i : ι
⊢ ↑(∑ i_1 ∈ DFinsupp.support ((decompose 𝒜) x),
        (DFinsupp.sum ((decompose 𝒜) y) fun x_1 aj ↦
            (of (fun i ↦ ↥(𝒜 i)) (i_1 + x_1)) (GradedMonoid.GMul.mul (((decompose 𝒜) x) i_1) aj))
          i) ∈
    Subsemiring.closure s
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case mul
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x✝¹ x y : A
hx✝ : x ∈ Subsemiring.closure s
hy✝ : y ∈ Subsemiring.closure s
h₁ : ∀ (i : ι), ↑(((decompose 𝒜) x) i) ∈ Subsemiring.closure s
h₂ : ∀ (i : ι), ↑(((decompose 𝒜) y) i) ∈ Subsemiring.closure s
i j : ι
x✝ : j ∈ DFinsupp.support ((decompose 𝒜) x)
⊢ ↑(DFinsupp.sum ((decompose 𝒜) y) fun i₁ b ↦
        ((of (fun i ↦ ↥(𝒜 i)) (j + i₁)) (GradedMonoid.GMul.mul (((decompose 𝒜) x) j) b)) i) ∈
    Subsemiring.closure s

Tactic:
DFinsupp.sum,

Goal state after:
case mul
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : AddMonoid ι
inst✝⁴ : Semiring A
inst✝³ : SetLike σ A
inst✝² : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝¹ : DecidableEq ι
inst✝ : GradedRing 𝒜
s : Set A
h : ∀ (i : ι) ⦃x : A⦄, x ∈ s → ↑(((decompose 𝒜) x) i) ∈ s
x✝¹ x y : A
hx✝ : x ∈ Subsemiring.closure s
hy✝ : y ∈ Subsemiring.closure s
h₁ : ∀ (i : ι), ↑(((decompose 𝒜) x) i) ∈ Subsemiring.closure s
h₂ : ∀ (i : ι), ↑(((decompose 𝒜) y) i) ∈ Subsemiring.closure s
i j : ι
x✝ : j ∈ DFinsupp.support ((decompose 𝒜) x)
⊢ ↑(∑ i_1 ∈ DFinsupp.support ((decompose 𝒜) y),
        ((of (fun i ↦ ↥(𝒜 i)) (j + i_1)) (GradedMonoid.GMul.mul (((decompose 𝒜) x) j) (((decompose 𝒜) y) i_1))) i) ∈
    Subsemiring.closure s
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]
this : HasSubst ![f₀, f₁, f₂]
⊢ ![subst ![f₀, f₁] F.toPowerSeries, f₂] ((fun i ↦ i) ⟨0, ⋯⟩) =
    subst ![f₀, f₁, f₂] (![subst ![Y₀, Y₁] F.toPowerSeries, Y₂] ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
simp only [Nat.succ_eq_add_one, Nat.reduceAdd, Fin.zero_eta, Fin.isValue,
          Matrix.cons_val_zero, subst_comp_subst_apply HasSubst.X_X this]

Goal state after:
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]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![f₀, f₁] F.toPowerSeries = subst (fun s ↦ subst ![f₀, f₁, f₂] (![Y₀, Y₁] s)) F.toPowerSeries
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]
this : HasSubst ![f₀, f₁, f₂]
⊢ ![subst ![f₀, f₁] F.toPowerSeries, f₂] ((fun i ↦ i) ⟨1, ⋯⟩) =
    subst ![f₀, f₁, f₂] (![subst ![Y₀, Y₁] F.toPowerSeries, Y₂] ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
· simp [subst_X this]

Goal state after:
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]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![f₀, f₁, f₂] (![Y₀, subst ![Y₁, Y₂] F.toPowerSeries] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ![f₀, subst ![f₁, f₂] F.toPowerSeries] ((fun i ↦ i) ⟨0, ⋯⟩)

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]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![f₀, f₁, f₂] (![Y₀, subst ![Y₁, Y₂] F.toPowerSeries] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![f₀, subst ![f₁, f₂] F.toPowerSeries] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
· simp [subst_X this]

Goal state after:
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]
this : HasSubst ![f₀, f₁, f₂]
⊢ subst ![f₀, f₁, f₂] (![Y₀, subst ![Y₁, Y₂] F.toPowerSeries] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![f₀, subst ![f₁, f₂] F.toPowerSeries] ((fun i ↦ i) ⟨1, ⋯⟩)
Module: Mathlib.RingTheory.HahnSeries.HEval

Goal state before:
pp: case neg
Γ : 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
⊢ ((powerSeriesFamily x (a * b)).coeff g).support ⊆
    image (fun i ↦ i.1 + i.2) (((powerSeriesFamily x a).mul (powerSeriesFamily x b)).coeff g).support

Tactic:
simp only [coeff_support, Set.Finite.toFinset_subset, support_subset_iff]
    intro n hn
    by_cases hz : n = 0
    · have : g = 0 ∧ (a.constantCoeff * b.constantCoeff) • (1 : V) ≠ 0 := by
        simpa [hz, h] using hn
      simp only [coe_image, Set.mem_image]
      use (0, 0)
      simp [this.2, this.1, h, hz, smul_smul, mul_comm]
    · simp [h, hz] at hn

Goal state after:
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
x y : SummableFamily Γ R α
g : Γ
⊢ {a | ((⇑x + ⇑y) a).coeff g ≠ 0} ⊆ (Function.support fun a ↦ (x a).coeff g) ∪ Function.support fun a ↦ (y a).coeff g

Tactic:
intro a ha

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
x y : SummableFamily Γ R α
g : Γ
a : α
ha : a ∈ {a | ((⇑x + ⇑y) a).coeff g ≠ 0}
⊢ a ∈ (Function.support fun a ↦ (x a).coeff g) ∪ Function.support fun a ↦ (y a).coeff g
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: case inr.refine_1
Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x : R⟦Γ⟧
h : 0 < (x - 1).orderTop
h✝ : Nontrivial R
⊢ IsUnit x.leadingCoeff

Tactic:
rw [(x.orderTop_self_sub_one_pos_iff.mp h).2]
      exact isUnit_one

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

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingUp R S
⊢ SpecializingMap (PrimeSpectrum.comap (algebraMap R S))

Tactic:
P

Goal state after:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : HasGoingUp R S
P : PrimeSpectrum S
⊢ ∀ ⦃b : PrimeSpectrum R⦄,
    flip (fun x1 x2 ↦ x1 ⤳ x2) b (PrimeSpectrum.comap (algebraMap R S) P) →
      ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' P ∧ PrimeSpectrum.comap (algebraMap R S) a' = b
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h✝ : HasGoingUp R S
P : PrimeSpectrum S
q : PrimeSpectrum R
hq : PrimeSpectrum.comap (algebraMap R S) P ≤ q
Q : Ideal S
hle : P.asIdeal ≤ Q
hQ : Q.IsPrime
h : Q.LiesOver q.asIdeal
⊢ ∃ a', flip (fun x1 x2 ↦ x1 ⤳ x2) a' P ∧ PrimeSpectrum.comap (algebraMap R S) a' = q

Tactic:
refine ⟨⟨Q, hQ⟩, (PrimeSpectrum.le_iff_specializes P _).mp hle, ?_⟩

Goal state after:
case refine_1
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h✝ : HasGoingUp R S
P : PrimeSpectrum S
q : PrimeSpectrum R
hq : PrimeSpectrum.comap (algebraMap R S) P ≤ q
Q : Ideal S
hle : P.asIdeal ≤ Q
hQ : Q.IsPrime
h : Q.LiesOver q.asIdeal
⊢ PrimeSpectrum.comap (algebraMap R S) { asIdeal := Q, isPrime := hQ } = q
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : SpecializingMap (PrimeSpectrum.comap (algebraMap R S))
q : Ideal R
hq : q.IsPrime
P : Ideal S
hP : P.IsPrime
hlt : Ideal.under R P < q
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q

Tactic:
have : PrimeSpectrum.comap (algebraMap R S) ⟨P, hP⟩ ⤳ (⟨q, hq⟩ : PrimeSpectrum R) :=
      (PrimeSpectrum.le_iff_specializes _ _).mp hlt.le

Goal state after:
case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : SpecializingMap (PrimeSpectrum.comap (algebraMap R S))
q : Ideal R
hq : q.IsPrime
P : Ideal S
hP : P.IsPrime
hlt : Ideal.under R P < q
this : PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := hP } ⤳ { asIdeal := q, isPrime := hq }
⊢ ∃ Q, P ≤ Q ∧ Q.IsPrime ∧ Q.LiesOver q
Module: Mathlib.RingTheory.Ideal.HasGoingUp

Goal state before:
pp: case refine_2
R : Type u_3
S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
h : SpecializingMap (PrimeSpectrum.comap (algebraMap R S))
q : Ideal R
hq : q.IsPrime
P : Ideal S
hP : P.IsPrime
hlt : Ideal.under R P < q
this : PrimeSpectrum.comap (algebraMap R S) { asIdeal := P, isPrime := hP } ⤳ { asIdeal := q, isPrime := hq }
Q : PrimeSpectrum S
hs : flip (fun x1 x2 ↦ x1 ⤳ x2) Q { asIdeal := P, isPrime := hP }
heq : PrimeSpectrum.comap (algebraMap R S) Q = { asIdeal := q, isPrime := hq }
⊢ q = Ideal.under R Q.asIdeal

Tactic:
simpa [PrimeSpectrum.ext_iff] using heq.symm

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsNoetherianRing R
h : ∀ (p : Ideal R) [p.IsPrime], p.height = 1 → Submodule.IsPrincipal p
⊢ UniqueFactorizationMonoid R

Tactic:
by
  rw [iff_exists_prime_mem_of_isPrime]
  intro I hIn _
  rcases I.ne_bot_iff.mp hIn with ⟨x, hxI, hx0⟩
  rcases Ideal.exists_minimalPrimes_le (I.span_singleton_le_iff_mem.mpr hxI) with ⟨p, hpmin, hpl⟩
  have : p.IsPrime := hpmin.isPrime
  have hpn : p ≠ ⊥ := fun hpb ↦ hx0 <|
    Ideal.span_singleton_eq_bot.mp <| bot_unique (hpmin.le.trans_eq hpb)
  have hpp : p.IsPrincipal := h p <| le_antisymm
    (Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes _ p hpmin)
      (by simpa [Order.one_le_iff_ne_zero])
  exact ⟨hpp.generator p, hpl (hpp.generator_mem p), hpp.prime_generator_of_isPrime p hpn⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : I.Pure
x : R
hx : x ∈ I
h : x ∈ I * span {x}
⊢ ∃ y ∈ I, x = x * y

Tactic:
by
    rw [Ideal.mem_mul_span_singleton] at h
    grind

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

Goal state before:
pp: case h
n : ℕ
H :
  ∀ m < n,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
hn : s.card = n
⊢ p.height ≤ ↑n

Tactic:
replace hn : s.card ≤ n := hn.le

Goal state after:
case h
n : ℕ
H :
  ∀ m < n,
    ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) (s : Finset R),
      p ∈ (span ↑s).minimalPrimes → s.card = m → p.height ≤ ↑m
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p : Ideal R
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
hn : s.card ≤ n
⊢ p.height ≤ ↑n
Module: Mathlib.RingTheory.Spectrum.Prime.Module

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
⊢ IsClosed (support R M)

Tactic:
rw [support_eq_zeroLocus]
  apply PrimeSpectrum.isClosed_zeroLocus

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

Goal state before:
pp: P : ProfiniteGrp.{u}
⊢ IsIso P.toLimit

Tactic:
rw [CategoryTheory.ConcreteCategory.isIso_iff_bijective]
  exact ⟨toLimit_injective P, toLimit_surjective P⟩

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p₁ p₀ p₂ : PrimeSpectrum R
h₀✝ : p₀ < p₁
h₁✝ : p₁ < p₂
x : R
hx : x ∈ p₂.asIdeal
e : PrimeSpectrum (Localization.AtPrime p₂.asIdeal) ≃o ↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) :=
  IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.asIdeal) p₂.asIdeal
hm : closedPoint (Localization.AtPrime p₂.asIdeal) = e.symm ⟨p₂, ⋯⟩
q : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)
hxq : (algebraMap R (Localization.AtPrime p₂.asIdeal)) x ∈ (e.symm (e q)).asIdeal
h₀ : e.symm ⟨p₀, ⋯⟩ < e.symm (e q)
h₁ : (e.symm (e q)).asIdeal < maximalIdeal (Localization.AtPrime p₂.asIdeal)
h : e q < ⟨p₂, ⋯⟩
⊢ ↑(e q) < p₂

Tactic:
Subtype.mk_lt_mk

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
p₁ p₀ p₂ : PrimeSpectrum R
h₀✝ : p₀ < p₁
h₁✝ : p₁ < p₂
x : R
hx : x ∈ p₂.asIdeal
e : PrimeSpectrum (Localization.AtPrime p₂.asIdeal) ≃o ↑(Set.Iic { asIdeal := p₂.asIdeal, isPrime := ⋯ }) :=
  IsLocalization.AtPrime.primeSpectrumOrderIso (Localization.AtPrime p₂.asIdeal) p₂.asIdeal
hm : closedPoint (Localization.AtPrime p₂.asIdeal) = e.symm ⟨p₂, ⋯⟩
q : PrimeSpectrum (Localization.AtPrime p₂.asIdeal)
hxq : (algebraMap R (Localization.AtPrime p₂.asIdeal)) x ∈ (e.symm (e q)).asIdeal
h₀ : e.symm ⟨p₀, ⋯⟩ < e.symm (e q)
h₁ : (e.symm (e q)).asIdeal < maximalIdeal (Localization.AtPrime p₂.asIdeal)
h : ↑(e q) < p₂
⊢ ↑(e q) < p₂
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
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
this : Set.SurjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑P ↑s'
o : Finset S
ho : ↑o ⊆ ↑P
hinj : Set.InjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑o
himgo : Finset.image (⇑(Quotient.mk (map (algebraMap R S) p))) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S)) s ∪ o
h : P.height ≤ ↑t.card
⊢ P.height ≤ p.height + (map (Quotient.mk (map (algebraMap R S) p)) P).height

Tactic:
← heq,

Goal state after:
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
s : Finset R
hp : p ∈ (span ↑s).minimalPrimes
heq : ↑s.card = p.height
P' : Ideal (S ⧸ map (algebraMap R S) p) := map (Quotient.mk (map (algebraMap R S) p)) P
s' : Finset (S ⧸ map (algebraMap R S) p)
hP' : P' ∈ (span ↑s').minimalPrimes
heq' : ↑s'.card = P'.height
hsP'sub : ↑s' ⊆ ↑P'
this : Set.SurjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑P ↑s'
o : Finset S
ho : ↑o ⊆ ↑P
hinj : Set.InjOn ⇑(Quotient.mk (map (algebraMap R S) p)) ↑o
himgo : Finset.image (⇑(Quotient.mk (map (algebraMap R S) p))) o = s'
t : Finset S := Finset.image (⇑(algebraMap R S)) s ∪ o
h : P.height ≤ ↑t.card
⊢ P.height ≤ ↑s.card + (map (Quotient.mk (map (algebraMap R S) p)) P).height
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
x : R
reg : IsSMulRegular R x
hx : x ∈ maximalIdeal R
⊢ x ∈ Ring.jacobson R

Tactic:
by
    simpa [ringJacobson_eq_maximalIdeal R]

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I.colon Set.univ).radical = (J.colon Set.univ).radical
this : (I'.colon Set.univ).radical = (J'.colon Set.univ).radical
⊢ I = J

Tactic:
← hI,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I.colon Set.univ).radical = (J.colon Set.univ).radical
this : (I'.colon Set.univ).radical = (J'.colon Set.univ).radical
⊢ {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = J
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ : (I.colon Set.univ).radical = (J.colon Set.univ).radical
⊢ (I'.colon Set.univ).radical = (J'.colon Set.univ).radical

Tactic:
← hI,

Goal state after:
case refine_3
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s : Finset (Submodule R M)
hs : s.inf id = N
hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary
I J I' : Submodule R M
hI' : I' ∈ s
hI : {I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id = I
J' : Submodule R M
hJ' : J' ∈ s
hJ : {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}.inf id = J
hIJ :
  (({I ∈ s | (I.colon Set.univ).radical = (I'.colon Set.univ).radical}.inf id).colon Set.univ).radical =
    (J.colon Set.univ).radical
⊢ (I'.colon Set.univ).radical = (J'.colon Set.univ).radical
Module: Mathlib.RingTheory.LittleWedderburn

Goal state before:
pp: case intro.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝² : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
⊢ d < n

Tactic:
rw [← Nat.pow_lt_pow_iff_right hq, ← card_D, ← card_Zx]

Goal state after:
case intro.mk
D : Type u_1
inst✝¹ : DivisionRing D
inst✝ : Finite D
hD : InductionHyp D
val✝ : Fintype D
Z : Subring D := Subring.center D
hZ : Z ≠ ⊤
this✝² : Field ↥Z := hD.field ⋯
q : ℕ := card ↥Z
card_Z : q = card ↥Z
hq : 1 < q
n : ℕ := finrank (↥Z) D
card_D : card D = q ^ n
h1qn : 1 ≤ q ^ n
Φₙ : ℤ[X] := cyclotomic n ℤ
key : ↑q - 1 + ↑(∑ x ∈ (ConjClasses.noncenter Dˣ).toFinset, x.carrier.toFinset.card) = ↑q ^ n - 1
i✝ : ConjClasses Dˣ
x : Dˣ
hx : ConjClasses.mk x ∈ ConjClasses.noncenter Dˣ
Zx : Subring D := Subring.centralizer {↑x}
hZx : Zx ≠ ⊤
this✝¹ : Field ↥Zx := hD.field ⋯
this✝ : Algebra ↥Z ↥Zx := (Subring.inclusion ⋯).toAlgebra
d : ℕ := finrank ↥Z ↥Zx
card_Zx : card ↥Zx = q ^ d
h1qd : 1 ≤ q ^ d
this : IsScalarTower (↥Z) (↥Zx) D
aux : ∀ {k : ℕ}, eval (↑q) (X ^ k - 1) = ↑q ^ k - 1
⊢ card ↥Zx < card D