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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r s : R
n : ℕ
ab : ℕ × ℕ
hab : ab ∈ antidiagonal n
⊢ (Ring.choose s ab.2 * Ring.choose r ab.1) • 1 = Ring.choose s ab.2 • Ring.choose r ab.1 • 1

Tactic:
mul_smul

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : BinomialRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
r s : R
n : ℕ
ab : ℕ × ℕ
hab : ab ∈ antidiagonal n
⊢ Ring.choose s ab.2 • Ring.choose r ab.1 • 1 = Ring.choose s ab.2 • Ring.choose r ab.1 • 1
Module: Mathlib.RingTheory.PowerSeries.Binomial

Goal state before:
pp: case zero
A : Type u_2
inst✝ : CommRing A
n : ℕ
⊢ ↑(↑n).negOnePow • (coeff n) ↑(invOneSubPow A 0) = Ring.choose (-↑0) n • 1

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
A : Type u_2
inst✝ : CommRing A
n : ℕ
hn : n = 0
⊢ ↑(↑n).negOnePow • (coeff n) ↑(invOneSubPow A 0) = Ring.choose (-↑0) n • 1

case neg
A : Type u_2
inst✝ : CommRing A
n : ℕ
hn : ¬n = 0
⊢ ↑(↑n).negOnePow • (coeff n) ↑(invOneSubPow A 0) = Ring.choose (-↑0) n • 1
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: Γ : 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
n : ℕ
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r)) n = 0 ^ n

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
Γ : 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
n : ℕ
hn : n = 0
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r)) n = 0 ^ n

case neg
Γ : 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
n : ℕ
hn : ¬n = 0
⊢ (powerSeriesFamily 0 (PowerSeries.binomialSeries A r)) n = 0 ^ n
Module: Mathlib.RingTheory.HahnSeries.Binomial

Goal state before:
pp: Γ : 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
n : ℕ
g : Γ
hg : g ∈ ((binomialFamily x r) n).support
⊢ 0 ≤ g

Tactic:
by_cases hn : n = 0

Goal state after:
case pos
Γ : 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
n : ℕ
g : Γ
hg : g ∈ ((binomialFamily x r) n).support
hn : n = 0
⊢ 0 ≤ g

case neg
Γ : 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
n : ℕ
g : Γ
hg : g ∈ ((binomialFamily x r) n).support
hn : ¬n = 0
⊢ 0 ≤ g
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 : α
ha : (x a).coeff g + (y a).coeff g ≠ 0
⊢ a ∈ (Function.support fun a ↦ (x a).coeff g) ∪ Function.support fun a ↦ (y a).coeff g

Tactic:
Set.mem_union,

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 : (x a).coeff g + (y a).coeff g ≠ 0
⊢ (a ∈ Function.support fun a ↦ (x a).coeff g) ∨ a ∈ Function.support fun a ↦ (y a).coeff g
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✝ : AddCommGroup R
s✝ t : SummableFamily Γ R α
a : α
s : SummableFamily Γ R α
⊢ (⋃ a, (s a).support).IsPWO

Tactic:
exact s.isPWO_iUnion_support

Goal state after:
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 : Γ'
gh : Γ × Γ'
x✝ : gh ∈ VAddAntidiagonal g ⋯
ab : α × β
hab : ab ∈ Set.Finite.toFinset ⋯
hsupp : (Function.support fun i ↦ (s i.1).coeff gh.1 • (t i.2).coeff gh.2) ⊆ ↑⋯.toFinset
⊢ ab ∈ (s.coeff gh.1).support ×ˢ (t.coeff gh.2).support

Tactic:
simp_all only [mem_vaddAntidiagonal, Set.mem_iUnion, mem_support, ne_eq, Set.Finite.mem_toFinset,
    Function.mem_support, Set.Finite.coe_toFinset, support_subset_iff, Set.mem_prod,
    Set.mem_ofPred_eq, Prod.forall, coeff_support, mem_product]

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 : Γ'
gh : Γ × Γ'
ab : α × β
x✝ : (∃ i, ¬(s i).coeff gh.1 = 0) ∧ (∃ i, ¬(t i).coeff gh.2 = 0) ∧ gh.1 +ᵥ gh.2 = g
hab : ¬(s ab.1).coeff gh.1 • (t ab.2).coeff gh.2 = 0
hsupp :
  ∀ (a : α) (b : β),
    ¬(s a).coeff gh.1 • (t b).coeff gh.2 = 0 → ¬(s.toFun a).coeff gh.1 = 0 ∧ ¬(t.toFun b).coeff gh.2 = 0
⊢ ¬(s ab.1).coeff gh.1 = 0 ∧ ¬(t ab.2).coeff gh.2 = 0
Module: Mathlib.RingTheory.HahnSeries.HahnEmbedding

Goal state before:
pp: M : Type u_1
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
f₁ : M →+o DivisibleHull M := DivisibleHull.coeOrderAddMonoidHom M
hf₁ : Function.Injective ⇑f₁
hf₁class :
  ∀ (a : M), ArchimedeanClass.mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (ArchimedeanClass.mk (f₁ a))
f₂' : DivisibleHull M →ₗ[ℚ] Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧
hf₂' : StrictMono ⇑f₂'
hf₂class' :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂' a)).orderTop
f₂ : DivisibleHull M →+o Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ :=
  { toAddMonoidHom := f₂'.toAddMonoidHom, monotone' := ⋯ }
hf₂ : Function.Injective ⇑f₂
hf₂class :
  ∀ (a : DivisibleHull M),
    ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂ a)).orderTop
f₃ : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧ →+o Lex ℝ⟦FiniteArchimedeanClass M⟧ :=
  embDomainOrderAddMonoidHom
    (RelIso.toRelEmbedding (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M).symm))
hf₃ : Function.Injective ⇑f₃
hf₃class :
  ∀ (a : Lex ℝ⟦FiniteArchimedeanClass (DivisibleHull M)⟧),
    (ofLex a).orderTop =
      (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)).withTopCongr
        (ofLex (f₃ a)).orderTop
a : M
x✝ : WithTop (FiniteArchimedeanClass M)
⊢ (DivisibleHull.archimedeanClassOrderIso M).symm
      ((FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M))
        ((FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)).withTopCongr x✝)) =
    (FiniteArchimedeanClass.withTopOrderIso M) x✝

Tactic:
cases (ofLex (f₃ (f₂ (f₁ a)))).orderTop with

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h1 : IsUnit ((a * y - 1) * 1 + 1)
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
⊢ IsUnit a

Tactic:
have h1 : IsUnit a ∧ IsUnit y := by simpa using h1

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
h✝ : I ≤ ⊥.jacobson
a : R
h : IsUnit ((Ideal.Quotient.mk I) a)
y : R
h1✝ : IsUnit ((a * y - 1) * 1 + 1)
h2 : ∀ (y_1 : R), IsUnit ((y * a - 1) * y_1 + 1)
h1 : IsUnit a ∧ IsUnit y
⊢ IsUnit a
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
inst✝³ : AddCommMonoid Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedCancelAddMonoid Γ
inst✝ : CommRing R
x y : R⟦Γ⟧
r : R
hr : r * x.leadingCoeff = 1
hxy : x = y + (single x.order) x.leadingCoeff
oinv : Γ
hxo : oinv + x.order = 0
⊢ 1 - (single oinv) r * x = -((single oinv) r * y)

Tactic:
nth_rw 1 [hxy]
  rw [mul_add, single_mul_single, hr, hxo,
    sub_add_eq_sub_sub_swap, sub_eq_neg_self, sub_eq_zero_of_eq single_zero_one.symm]

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✝³ : AddCommGroup Γ
inst✝² : LinearOrder Γ
inst✝¹ : IsOrderedAddMonoid Γ
inst✝ : Field R
x : R⟦Γ⟧
x0 : x ≠ 0
⊢ x * x⁻¹ = 1

Tactic:
by
    have h :=
      SummableFamily.one_sub_self_mul_hsum_powers
        (unit_aux x (inv_mul_cancel₀ (leadingCoeff_ne_zero.mpr x0)) _ (neg_add_cancel x.order))
    rw [sub_sub_cancel] at h
    rw [inv_def, ← mul_assoc, mul_comm x, h]

Goal state after:
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Ideal R
inst✝ : IsAdicComplete I R
f : R[X]
x✝ : f.Monic
a₀ : R
h₁ : Polynomial.eval a₀ f ∈ I
h₂ : IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (derivative f)))
f' : R[X] := derivative f
c : ℕ → R := fun n ↦ Nat.recOn n a₀ fun x b ↦ b - Polynomial.eval b f * (Polynomial.eval b f')⁻¹ʳ
hc : ∀ (n : ℕ), c (n + 1) = c n - Polynomial.eval (c n) f * (Polynomial.eval (c n) f')⁻¹ʳ
hc_mod : ∀ (n : ℕ), c n ≡ a₀ [SMOD I]
hf'c : ∀ (n : ℕ), IsUnit (Polynomial.eval (c n) f')
hfcI : ∀ (n : ℕ), Polynomial.eval (c n) f ∈ I ^ (n + 1)
aux : ∀ (m n : ℕ), m ≤ n → c m ≡ c n [SMOD I ^ m • ⊤]
a : R
ha : ∀ (n : ℕ), c n ≡ a [SMOD I ^ n • ⊤]
this : ∀ (n : ℕ), Polynomial.eval a f ≡ 0 [SMOD I ^ n • ⊤]
⊢ f.IsRoot a

Tactic:
by exact IsHausdorff.haus' _ this

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : UniqueFactorizationMonoid R
p : Ideal R
inst✝ : p.IsPrime
hph : p.height = 1
⊢ Submodule.IsPrincipal p

Tactic:
by
  have hpn : p ≠ ⊥ := p.ne_bot_of_height_eq_one hph
  obtain ⟨x, hxmem, hxp⟩ := Ideal.IsPrime.exists_mem_prime_of_ne_bot ‹_› hpn
  exact ⟨x, p.eq_span_singleton_of_height_eq_one hph hxmem hxp⟩

Goal state after:
Module: Mathlib.Topology.Algebra.ClopenNhdofOne

Goal state before:
pp: G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : CompactSpace G
inst✝ : TotallyDisconnectedSpace G
H : ClosedSubgroup G
g : G
hg : g ∈ sInf {N | IsOpen ↑N ∧ ↑H ≤ N}
hg_not : g ∉ ↑H
U : Set G := (g • ↑H)ᶜ
UOpen : IsOpen U
x✝ : 1 ∈ g • ↑H
l : G
hl : l ∈ ↑H
hgl : g⁻¹ = l
⊢ False

Tactic:
exact hg_not <| inv_mem_iff.mp (hgl ▸ hl)

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

Goal state before:
pp: case hIN.refine_2
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
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
f : R →+* Localization.AtPrime q := algebraMap R (Localization.AtPrime q)
qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ := { toFun := fun n ↦ map (Quotient.mk I) (comap f (map f q ^ n)), monotone' := ⋯ }
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → qs n = qs m
⊢ (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
      (map (algebraMap R (Localization.AtPrime q)) q ^ n) ≤
    (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)) (map f q ^ (n + 1)) ⊔
      I •
        (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q))
          (map (algebraMap R (Localization.AtPrime q)) q ^ n)

Tactic:
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.Pure

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I J : Ideal R
inst✝¹ : I.Pure
inst✝ : J.Pure
h : zeroLocus ↑I = zeroLocus ↑J
s : Set (PrimeSpectrum R)
hs : zeroLocus ↑I = s
t : Set (PrimeSpectrum R)
ht : zeroLocus ↑J = t
⊢ s = t

Tactic:
rw [← hs, ← ht, h]

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (algebraMap R Rₚ) p
⊢ p'.IsMaximal

Tactic:
p'_def,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
p : Ideal R
P : Ideal R[X]
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver p
this : p.IsPrime
Rₚ : Type u_1 := Localization.AtPrime p
p' : Ideal Rₚ := Ideal.map (algebraMap R Rₚ) p
p'_def : p' = Ideal.map (algebraMap R Rₚ) p
⊢ (Ideal.map (algebraMap R Rₚ) p).IsMaximal
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this✝ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset
⊢ p ∈ (span ↑t).minimalPrimes

Tactic:
rw [Finset.coe_union, Set.Finite.coe_toFinset, span_union, sup_comm, span,
    Submodule.span_generators]

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
I p : Ideal R
inst✝ : p.IsPrime
hrp : I ≤ p
p' : Ideal (R ⧸ I) := map (algebraMap R (R ⧸ I)) p
this✝ : p'.IsPrime
s : Finset (R ⧸ I)
hps : p' ∈ (span ↑s).minimalPrimes
hs : ↑s.card = p'.height
hsp' : ↑s ⊆ ↑p'
this : Set.SurjOn ⇑(Quotient.mk I) ↑p ↑s
o : Finset R
hsubset : ↑o ⊆ ↑p
ho : Set.InjOn ⇑(Quotient.mk I) ↑o
himgo : Finset.image (⇑(Quotient.mk I)) o = s
hI : I.FG
t : Finset R := o ∪ ⋯.toFinset
⊢ p ∈ (I ⊔ span ↑o).minimalPrimes
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)
hq : ↑(e q) < p₂
⊢ ∃ q, x ∈ q.asIdeal ∧ p₀ < q ∧ q < p₂

Tactic:
exact Exists.intro (e q).1
    ⟨(p₂.1.under_map_of_isLocalizationAtPrime hq.le).le hxq, e.symm.lt_iff_lt.mp h₀, hq⟩

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
⊢ RelSeries.head p = (RelSeries.snoc Q (RelSeries.last p) ⋯).head

Tactic:
simp [← hh]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
rs : List R
reg : Sequence.IsRegular R rs
⊢ ringKrullDim (R ⧸ ofList rs) + ↑rs.length = ringKrullDim R

Tactic:
by
  have eq : ofList rs = ofList rs • (⊤ : Ideal R) := by simp
  rw [ringKrullDim_eq_of_ringEquiv (quotientEquivAlgOfEq R eq).toRingEquiv,
    ← supportDim_quotient_eq_ringKrullDim, ← supportDim_self_eq_ringKrullDim]
  exact supportDim_add_length_eq_supportDim_of_isRegular rs reg

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h✝ : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
x : M
hx : x ∈ N
y : M
x✝ : x + a ^ n • y ∈ f n ⊓ (N + a ^ n • ⊤)
h1 : x + a ^ n • y ∈ ↑(f n)
h : (a ^ n • y ∈ N) = ((a ^ n * a ^ n) • y ∈ N)
⊢ x + a ^ n • y ∈ N

Tactic:
mul_smul

Goal state after:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
N : Submodule R M
a : R
b : M
hab : a • b ∈ N
f : ℕ → Submodule R M := fun n ↦ { carrier := {x | a ^ n • x ∈ N}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
hf : Monotone f
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → { toFun := f, monotone' := hf } n = { toFun := f, monotone' := hf } m
h✝ : ∀ ⦃b c : Submodule R M⦄, b ⊓ c = N → b = N ∨ c = N
x : M
hx : x ∈ N
y : M
x✝ : x + a ^ n • y ∈ f n ⊓ (N + a ^ n • ⊤)
h1 : x + a ^ n • y ∈ ↑(f n)
h : (a ^ n • y ∈ N) = (a ^ n • a ^ n • y ∈ N)
⊢ x + a ^ n • y ∈ N
Module: Mathlib.RingTheory.LocalProperties.FinitePresentation

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
s : Set R
hs : Ideal.span s = ⊤
Mₚ : ↑s → Type u_3
inst✝⁷ : (g : ↑s) → AddCommGroup (Mₚ g)
inst✝⁶ : (g : ↑s) → Module R (Mₚ g)
Rₚ : ↑s → Type u_4
inst✝⁵ : (g : ↑s) → CommRing (Rₚ g)
inst✝⁴ : (g : ↑s) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↑s), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↑s) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↑s), IsScalarTower R (Rₚ g) (Mₚ g)
ϕ : (g : ↑s) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↑s), IsLocalizedModule (Submonoid.powers ↑g) (ϕ g)
h : ∀ (g : ↑s), FinitePresentation (Rₚ g) (Mₚ g)
this : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
fsurj : Function.Surjective ⇑f
⊢ f.ker.FG

Tactic:
refine f.ker.of_localizationSpan' s hs (Rₚ := Rₚ)
    (fun g ↦ TensorProduct.mk R (Rₚ g) (Fin n → R) 1) (fun g ↦ ?_)

Goal state after:
R : Type u_1
inst✝¹⁰ : CommRing R
M : Type u_2
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
s : Set R
hs : Ideal.span s = ⊤
Mₚ : ↑s → Type u_3
inst✝⁷ : (g : ↑s) → AddCommGroup (Mₚ g)
inst✝⁶ : (g : ↑s) → Module R (Mₚ g)
Rₚ : ↑s → Type u_4
inst✝⁵ : (g : ↑s) → CommRing (Rₚ g)
inst✝⁴ : (g : ↑s) → Algebra R (Rₚ g)
inst✝³ : ∀ (g : ↑s), IsLocalization.Away (↑g) (Rₚ g)
inst✝² : (g : ↑s) → Module (Rₚ g) (Mₚ g)
inst✝¹ : ∀ (g : ↑s), IsScalarTower R (Rₚ g) (Mₚ g)
ϕ : (g : ↑s) → M →ₗ[R] Mₚ g
inst✝ : ∀ (g : ↑s), IsLocalizedModule (Submonoid.powers ↑g) (ϕ g)
h : ∀ (g : ↑s), FinitePresentation (Rₚ g) (Mₚ g)
this : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
fsurj : Function.Surjective ⇑f
g : ↑s
⊢ (Submodule.localized' (Rₚ g) (Submonoid.powers ↑g) ((TensorProduct.mk R (Rₚ g) (Fin n → R)) 1) f.ker).FG
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n → injectiveDimension (M.localizedModule S) ≤ ↑n
N : ℕ∞
⊢ injectiveDimension M ≤ ↑N → injectiveDimension (M.localizedModule S) ≤ ↑N

Tactic:
induction N with
    | top => simp
    | coe n => simpa using aux n

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)
p : Ideal R
hp : p.IsMaximal
this✝ : Small.{v, u} (Localization.AtPrime p) := small_of_surjective Localization.mkHom_surjective
this : Module.Injective (Localization.AtPrime p) ↑(M.localizedModule p.primeCompl)
⊢ Module.Injective (Localization.AtPrime p) (LocalizedModule p.primeCompl ↑M)

Tactic:
rw [← Module.Baer.iff_injective] at this ⊢

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
h : ∀ (m : MaximalSpectrum R), Injective (M.localizedModule m.asIdeal.primeCompl)
p : Ideal R
hp : p.IsMaximal
this✝ : Small.{v, u} (Localization.AtPrime p) := small_of_surjective Localization.mkHom_surjective
this : Module.Baer (Localization.AtPrime p) ↑(M.localizedModule p.primeCompl)
⊢ Module.Baer (Localization.AtPrime p) (LocalizedModule p.primeCompl ↑M)
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case bot
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
h : ∀ (i : PrimeSpectrum R), Subsingleton (LocalizedModule i.asIdeal.primeCompl ↑M)
p : Ideal R
hp : p.IsMaximal
⊢ Subsingleton (LocalizedModule p.primeCompl ↑M)

Tactic:
exact h ⟨p, hp.isPrime⟩

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑n
N : ℕ∞
⊢ injectiveDimension M ≤ ↑N ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑N

Tactic:
induction N with
    | top => simp
    | coe n => simpa using aux n

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: case coe
R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
M : ModuleCat R
aux : ∀ (n : ℕ), injectiveDimension M ≤ ↑n ↔ ⨆ m, injectiveDimension (M.localizedModule m.asIdeal.primeCompl) ≤ ↑n
N : ℕ∞
⊢ injectiveDimension M ≤ ↑N ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ↑N

Tactic:
induction N with
    | top => simp
    | coe n => simpa using aux n

Goal state after: