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

Goal state before:
pp: case hdp
A : Type u_3
B : Type u_4
C : Type u_5
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
n : ℕ
a : A
ha : a ∈ ↑I
⊢ g (hJ.dpow n (f a)) = (g.comp f) (hI.dpow n a)

Tactic:
RingHom.comp_apply,

Goal state after:
case hdp
A : Type u_3
B : Type u_4
C : Type u_5
inst✝² : CommSemiring A
inst✝¹ : CommSemiring B
inst✝ : CommSemiring C
I : Ideal A
J : Ideal B
K : Ideal C
hI : DividedPowers I
hJ : DividedPowers J
hK : DividedPowers K
f : A →+* B
g : B →+* C
heq : J = map f I
hf : hI.IsDPMorphism hJ f
hh : hI.IsDPMorphism hK (g.comp f)
n : ℕ
a : A
ha : a ∈ ↑I
⊢ g (hJ.dpow n (f a)) = g (f (hI.dpow n a))
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A : Type u_3
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
S : Set A
hS : I = span S
hdp : ∀ {n : ℕ}, ∀ a ∈ S, hI.dpow n a = hI'.dpow n a
⊢ hI' = hI

Tactic:
ext n a
  by_cases ha : a ∈ I
  · refine hI.dpow_comp_from_gens hI' (f := RingHom.id A) hS ?_ ?_ a ha
    · intro s hs
      simp only [RingHom.id_apply, hS]
      exact subset_span hs
    · intro m b hb
      simpa only [RingHom.id_apply] using (hdp b hb)
  · rw [hI.dpow_null ha, hI'.dpow_null ha]

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ ⋯.choose = ⟨dpow' p n ↑x, ⋯⟩

Tactic:
have hinj : Injective (PadicInt.Coe.ringHom (p := p)) :=
      (Set.injective_codRestrict Subtype.property).mp fun ⦃a₁ a₂⦄ a ↦ a
    have heq : Coe.ringHom ⟨dpow' p n x, dpow'_int p n hx⟩ =
        inverse (n ! : ℚ_[p]) * Coe.ringHom x ^ n := by
      simp [dpow', inverse_eq_inv', Coe.ringHom_apply]
    simpa only [← hinj.eq_iff, (Exists.choose_spec (_ : ∃ a, ∃ _, Coe.ringHom a = _)).2,
      RatAlgebra.dpow_apply, Submodule.mem_top] using! heq.symm

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

Goal state before:
pp: case pos
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∈ Ideal.span {↑p}
⊢ ⋯.choose = ⟨dpow' p n ↑x, ⋯⟩

pp: case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∉ Ideal.span {↑p}
⊢ 0 = 0

Tactic:
· have hinj : Injective (PadicInt.Coe.ringHom (p := p)) :=
      (Set.injective_codRestrict Subtype.property).mp fun ⦃a₁ a₂⦄ a ↦ a
    have heq : Coe.ringHom ⟨dpow' p n x, dpow'_int p n hx⟩ =
        inverse (n ! : ℚ_[p]) * Coe.ringHom x ^ n := by
      simp [dpow', inverse_eq_inv', Coe.ringHom_apply]
    simpa only [← hinj.eq_iff, (Exists.choose_spec (_ : ∃ a, ∃ _, Coe.ringHom a = _)).2,
      RatAlgebra.dpow_apply, Submodule.mem_top] using! heq.symm

Goal state after:
case neg
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
x : ℤ_[p]
hx : x ∉ Ideal.span {↑p}
⊢ 0 = 0
Module: Mathlib.RingTheory.GradedAlgebra.Homogeneous.Subsemiring

Goal state before:
pp: case inr
ι : 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 : ∀ x ∈ s, IsHomogeneousElem 𝒜 x
i : ι
x : A
hx✝ : x ∈ insert 0 s
hx : x ∈ s
⊢ ↑(((decompose 𝒜) x) i) ∈ insert 0 s

Tactic:
obtain ⟨j, hj⟩ := h x hx
    obtain rfl | h := eq_or_ne i j <;> simp [decompose_of_mem _ hj, of_eq_of_ne, *]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
u : Rˣ
⊢ constantCoeff (invUnitsSub u) = 1 /ₚ u

Tactic:
← coeff_zero_eq_constantCoeff_apply,

Goal state after:
R : Type u_1
inst✝ : Ring R
u : Rˣ
⊢ (coeff 0) (invUnitsSub u) = 1 /ₚ u
Module: Mathlib.RingTheory.PowerSeries.WellKnown

Goal state before:
pp: S : Type u_1
inst✝ : CommRing S
⊢ (invOneSubPow S 0).inv = 1

Tactic:
by
  delta invOneSubPow
  simp only [Units.inv_eq_val_inv, inv_one, Units.val_one]

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

Goal state before:
pp: Γ : Type u_1
Γ' : Type u_2
α : Type u_5
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
x : R⟦Γ⟧
s : SummableFamily Γ' V α
⊢ (of R).symm ((const Unit x) default • (of R) s.hsum) = (of R).symm (x • (of R) s.hsum)

Tactic:
const_toFun

Goal state after:
Γ : Type u_1
Γ' : Type u_2
α : Type u_5
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
x : R⟦Γ⟧
s : SummableFamily Γ' V α
⊢ (of R).symm (x • (of R) s.hsum) = (of R).symm (x • (of R) s.hsum)
Module: Mathlib.RingTheory.HahnSeries.Summable

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
a : α
⊢ (s.embDomain f) (f a) = s a

Tactic:
rw [embDomain_apply, dif_pos (Set.mem_range_self a)]
  exact congr rfl (f.injective (Classical.choose_spec (Set.mem_range_self a)))

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

Goal state before:
pp: Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
⊢ (s.embDomain f).hsum.coeff g = s.hsum.coeff g

Tactic:
simp only [coeff_hsum, embDomain_apply, apply_dite HahnSeries.coeff, dite_apply, coeff_zero]

Goal state after:
Γ : Type u_1
R : Type u_3
α : Type u_5
β : Type u_6
inst✝¹ : PartialOrder Γ
inst✝ : AddCommMonoid R
s : SummableFamily Γ R α
f : α ↪ β
g : Γ
⊢ (∑ᶠ (i : β), if h : i ∈ Set.range ⇑f then (s (Classical.choose ⋯)).coeff g else 0) = ∑ᶠ (i : α), (s i).coeff g
Module: Mathlib.RingTheory.HahnSeries.Valuation

Goal state before:
pp: case neg
Γ : Type u_1
R : Type u_2
inst✝⁴ : AddCancelCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
⊢ ↑(x * y).order = ↑(x.order + y.order)

Tactic:
WithTop.coe_eq_coe,

Goal state after:
case neg
Γ : Type u_1
R : Type u_2
inst✝⁴ : AddCancelCommMonoid Γ
inst✝³ : LinearOrder Γ
inst✝² : IsOrderedCancelAddMonoid Γ
inst✝¹ : Ring R
inst✝ : IsDomain R
x y : R⟦Γ⟧
hx : ¬x = 0
hy : ¬y = 0
⊢ (x * y).order = x.order + y.order
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)
h1 : IsUnit a ∧ IsUnit y
⊢ IsUnit a

Tactic:
exact h1.1

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)
m k : ℕ
⊢ c m ≡ c (m + k) [SMOD I ^ m]

Tactic:
induction k with
        | zero => rw [add_zero]
        | succ k ih => ?_

Goal state after:
case succ
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)
m k : ℕ
ih : c m ≡ c (m + k) [SMOD I ^ m]
⊢ c m ≡ c (m + (k + 1)) [SMOD I ^ m]
Module: Mathlib.RingTheory.Henselian

Goal state before:
pp: case refine_1
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
n : ℕ
ha : c n ≡ a [SMOD I ^ n]
⊢ Polynomial.eval (c n) f ∈ I ^ n

Tactic:
exact Ideal.pow_le_pow_right le_self_add (hfcI _)

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J
J : Ideal R
hJ : J.FG
⊢ I ⊓ J = I * J

Tactic:
exact H hJ

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
⊢ zeroLocus ↑I = zeroLocus ↑J ↔ I = J

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ h ▸ rfl⟩
  rw [← I.ker_piRingHom_atPrime_eq_of_pure, ← J.ker_piRingHom_atPrime_eq_of_pure]
  generalize hs : zeroLocus (I : Set R) = s
  generalize ht : zeroLocus (J : Set R) = t
  obtain rfl : s = t := by rw [← hs, ← ht, h]
  rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : _root_.Ideal R
⊢ supportDim R (R ⧸ I) = ringKrullDim (R ⧸ I)

Tactic:
rw [supportDim_eq_ringKrullDim_quotient_annihilator, Ideal.annihilator_quotient]

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

Goal state before:
pp: case a
R : Type u_1
inst✝³ : CommRing R
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsLocalRing R
dim : Module.supportDim R N = 0
x✝ : Nontrivial N :=
  of_eq_true
    (Eq.trans
      ((fun M [AddCommGroup M] [Module R M] ↦ Eq.symm (propext (Module.supportDim_ne_bot_iff_nontrivial R M))) N)
      (Eq.trans (congrFun' (congrArg Ne dim) ⊥)
        (Eq.trans (congrArg Not WithBot.zero_ne_bot._simp_1) not_false_eq_true)))
p : PrimeSpectrum R
hp : p ∈ Module.support R N
nmem : ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }
⊢ False

Tactic:
have : p < ⟨maximalIdeal R, IsMaximal.isPrime' (maximalIdeal R)⟩ :=
      lt_of_le_of_ne (IsLocalRing.le_maximalIdeal IsPrime.ne_top') nmem

Goal state after:
case a
R : Type u_1
inst✝³ : CommRing R
N : Type u_3
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsLocalRing R
dim : Module.supportDim R N = 0
x✝ : Nontrivial N :=
  of_eq_true
    (Eq.trans
      ((fun M [AddCommGroup M] [Module R M] ↦ Eq.symm (propext (Module.supportDim_ne_bot_iff_nontrivial R M))) N)
      (Eq.trans (congrFun' (congrArg Ne dim) ⊥)
        (Eq.trans (congrArg Not WithBot.zero_ne_bot._simp_1) not_false_eq_true)))
p : PrimeSpectrum R
hp : p ∈ Module.support R N
nmem : ¬p = { asIdeal := maximalIdeal R, isPrime := ⋯ }
this : p < { asIdeal := maximalIdeal R, isPrime := ⋯ }
⊢ False
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
h : p.height ≤ ↑t.card
⊢ t.card ≤ s.card + Submodule.spanFinrank I

Tactic:
have : (Submodule.FG.finite_generators hI).toFinset.card = I.spanFinrank := by
      rw [← Set.ncard_eq_toFinset_card (hs := Submodule.FG.finite_generators hI)]
      exact Submodule.FG.generators_ncard hI

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
h : p.height ≤ ↑t.card
this : ⋯.toFinset.card = Submodule.spanFinrank I
⊢ t.card ≤ s.card + Submodule.spanFinrank I
Module: Mathlib.RingTheory.KrullDimension.Polynomial

Goal state before:
pp: case h_option
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
ι : Type u_2
inst✝¹ : Finite ι
α✝ : Type u_2
inst✝ : Fintype α✝
IH : ringKrullDim (MvPolynomial α✝ R) = ringKrullDim R + ↑(Nat.card α✝)
⊢ ringKrullDim (MvPolynomial (Option α✝) R) = ringKrullDim R + ↑(Nat.card (Option α✝))

Tactic:
simp only [Nat.card_eq_fintype_card, Fintype.card_option, Nat.cast_add, Nat.cast_one,
      ← add_assoc] at IH ⊢
    rw [ringKrullDim_eq_of_ringEquiv (MvPolynomial.optionEquivLeft _ _).toRingEquiv,
      Polynomial.ringKrullDim_of_isNoetherianRing, IH]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
h : (e ⟨q, ⋯⟩).asIdeal.height ≤ 1
⊢ False

Tactic:
show q = closedPoint R from PrimeSpectrum.ext hqm

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
p₁ p₀ : PrimeSpectrum R
h₀ : p₀ < p₁
h₁ : p₁ < closedPoint R
x : R
hx : x ∈ 𝔪
hn : x ∉ p₀.asIdeal
e : ↑(zeroLocus ↑p₀.asIdeal) ≃o PrimeSpectrum (R ⧸ p₀.asIdeal) := p₀.asIdeal.primeSpectrumQuotientOrderIsoZeroLocus.symm
q✝ : Ideal R
hq : q✝ ∈ (p₀.asIdeal + span {x}).minimalPrimes
q : PrimeSpectrum R := { asIdeal := q✝, isPrime := ⋯ }
this : q.asIdeal.IsPrime
hxq : x ∈ q.asIdeal
hqm : q.asIdeal = 𝔪
h : (e ⟨closedPoint R, ⋯⟩).asIdeal.height ≤ 1
⊢ False
Module: Mathlib.RingTheory.KrullDimension.Regular

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
x : R
hn : ∀ p ∈ (annihilator R M).minimalPrimes, x ∉ p
a✝¹ : Nontrivial M
a✝ : Nontrivial (QuotSMulTop x M)
this✝ : Nonempty ↑(support R M)
this : Nonempty ↑(support R (QuotSMulTop x M))
p : LTSeries ↑(support R (QuotSMulTop x M))
hp : ↑(RelSeries.head p) ∈ support R M ∧ x ∈ ↑(↑(RelSeries.head p)).asIdeal
le : support R (QuotSMulTop x M) ⊆ support R M
q : LTSeries ↑(support R M) := p.map (Set.MapsTo.restrict id (support R (QuotSMulTop x M)) (support R M) le) ⋯
r✝ : Ideal R
hrm : r✝ ∈ (annihilator R M).minimalPrimes
hr : r✝ ≤ (↑(RelSeries.head q)).asIdeal
r : ↑(support R M) := ⟨{ asIdeal := r✝, isPrime := ⋯ }, ⋯⟩
h : r = RelSeries.head q
⊢ (↑(RelSeries.head q)).asIdeal ∈ (annihilator R M).minimalPrimes

Tactic:
by rwa [← h]

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case refine_1
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
x✝ : M
⊢ x✝ ∈
      (Finset.image (fun t ↦ t.inf id)
            (Finset.image (fun J ↦ {I ∈ s | (I.colon Set.univ).radical = (J.colon Set.univ).radical}) s)).inf
        id ↔
    x✝ ∈ N

Tactic:
grind [Finset.inf_image, Submodule.mem_finsetInf]

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
t : Finset (Submodule R M)
ht : N.IsMinimalPrimaryDecomposition t
⊢ (fun J ↦ (J.colon Set.univ).radical) '' ↑t = N.associatedPrimes

Tactic:
by
  classical
  replace h x : radical (N.colon {x}) = (t.filter (x ∉ ·)).inf fun q ↦ radical (q.colon .univ) := by
    simp_rw [← ht.inf_eq, colon_finsetInf, ← radicalInfTopHom_apply, map_finset_inf,
      Function.comp_def, radicalInfTopHom_apply, id_eq]
    rw [Finset.inf_congr rfl (fun q hq ↦ (ht.primary hq).radical_colon_singleton_eq_ite x),
      Finset.inf_ite, Finset.inf_top, top_inf_eq]
  ext p
  constructor
  · rintro ⟨q, hqt, rfl⟩
    obtain ⟨x, hxt, hxq⟩ := SetLike.not_le_iff_exists.mp (ht.minimal hqt)
    use (ht.primary hqt).isPrime_radical_colon, x
    rw [h, ← Finset.insert_erase (Finset.mem_filter.mpr ⟨hqt, hxq⟩), Finset.inf_insert,
      eq_comm, inf_eq_left, Finset.le_inf_iff]
    simp only [mem_finsetInf, Finset.mem_erase] at hxt
    grind
  · rintro ⟨hp, x, rfl⟩
    rw [h] at hp ⊢
    obtain ⟨q, hq1, hq2⟩ := eq_inf_of_isPrime_inf hp
    exact ⟨q, Finset.mem_of_mem_filter q hq1, hq2⟩

Goal state after:
Module: Mathlib.RingTheory.Lasker

Goal state before:
pp: case neg
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∉ ⋃ r ∈ s₀, ↑↑r
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = ⊤

Tactic:
replace hy2 : y ∈ S := by
      simp only [Submonoid.mem_iInf, Ideal.mem_primeCompl_iff, Subtype.forall, S]
      intro r hrI hrs
      contrapose hy2
      exact Set.mem_biUnion hrs hy2

Goal state after:
case neg
R : Type u_3
M : Type u_4
inst✝² : CommRing R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N : Submodule R M
s₀ : Finset ↑N.associatedPrimes
hs₀ : IsLowerSet ↑s₀
q : Submodule R M
hqp : q.IsPrimary
p : ↑N.associatedPrimes
S : Submonoid R := ⨅ q ∈ s₀, (↑q).primeCompl
f : M →ₗ[R] LocalizedModule S M := mkLinearMap S M
hp : p ∉ s₀
hq : ¬↑(q.colon Set.univ) ⊆ ⋃ r ∈ s₀, ↑↑r
y : R
hy1 : y ∈ ↑(q.colon Set.univ)
hy2 : y ∈ S
⊢ comap (mkLinearMap S M) (localized₀ S (mkLinearMap S M) q) = ⊤
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u
inst✝¹⁰ : Group G
inst✝⁹ : MulSemiringAction G B
inst✝⁸ : SMulCommClass G A B
inst✝⁷ : TopologicalSpace G
inst✝⁶ : CompactSpace G
inst✝⁵ : TotallyDisconnectedSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : TopologicalSpace B
inst✝² : DiscreteTopology B
inst✝¹ : ContinuousSMul G B
inst✝ : IsInvariant A B G
x : B
⊢ IsIntegral A x

Tactic:
obtain ⟨N, hN⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
    (stabilizer_isOpen G x) (one_mem _)

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹³ : CommRing A
inst✝¹² : CommRing B
inst✝¹¹ : Algebra A B
G : Type u
inst✝¹⁰ : Group G
inst✝⁹ : MulSemiringAction G B
inst✝⁸ : SMulCommClass G A B
inst✝⁷ : TopologicalSpace G
inst✝⁶ : CompactSpace G
inst✝⁵ : TotallyDisconnectedSpace G
inst✝⁴ : IsTopologicalGroup G
inst✝³ : TopologicalSpace B
inst✝² : DiscreteTopology B
inst✝¹ : ContinuousSMul G B
inst✝ : IsInvariant A B G
x : B
N : OpenNormalSubgroup G
hN : ↑N ⊆ ↑(MulAction.stabilizer G x)
⊢ IsIntegral A x
Module: Mathlib.RingTheory.LocalProperties.InjectiveDimension

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : Small.{v, u} R
inst✝ : IsNoetherianRing R
S : Submonoid R
M : ModuleCat R
⊢ injectiveDimension (M.localizedModule S) ≤ injectiveDimension M

Tactic:
have aux (n : ℕ) : injectiveDimension M ≤ n → injectiveDimension (M.localizedModule S) ≤ n := by
    simp only [injectiveDimension_le_iff]
    intro h
    exact M.localizedModule_hasInjectiveDimensionLE n S

Goal state after:
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
⊢ injectiveDimension (M.localizedModule S) ≤ injectiveDimension M
Module: Mathlib.RingTheory.Invariant.Profinite

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
inst✝² : IsInvariant A B G
P Q : Ideal B
inst✝¹ : P.IsPrime
inst✝ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
F : OpenNormalSubgroup G ⥤ Type u :=
  { obj := fun N ↦ { g // Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) Q = g • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P },
    map := fun {N N'} f ↦
      ↾fun x ↦ ⟨(QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑x, ⋯⟩,
    map_id := ⋯, map_comp := ⋯ }
this✝ : ∀ (N : OpenNormalSubgroup G), Nonempty (F.obj N)
s : (j : OpenNormalSubgroup G) → F.obj j
hs : s ∈ F.sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑(s N), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑(s N)
x : B
⊢ x ∈ Q ↔ x ∈ a • P

Tactic:
obtain ⟨N, hN⟩ := ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
    (stabilizer_isOpen G x) (one_mem _)

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹⁵ : CommRing A
inst✝¹⁴ : CommRing B
inst✝¹³ : Algebra A B
G : Type u
inst✝¹² : Group G
inst✝¹¹ : MulSemiringAction G B
inst✝¹⁰ : SMulCommClass G A B
inst✝⁹ : TopologicalSpace G
inst✝⁸ : CompactSpace G
inst✝⁷ : TotallyDisconnectedSpace G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : TopologicalSpace B
inst✝⁴ : DiscreteTopology B
inst✝³ : ContinuousSMul G B
inst✝² : IsInvariant A B G
P Q : Ideal B
inst✝¹ : P.IsPrime
inst✝ : Q.IsPrime
hPQ : Ideal.under A P = Ideal.under A Q
B' : (G : Type u) → [inst : Monoid G] → [inst_1 : MulSemiringAction G B] → [SMulCommClass G A B] → Subalgebra A B :=
  FixedPoints.subalgebra A B
F : OpenNormalSubgroup G ⥤ Type u :=
  { obj := fun N ↦ { g // Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) Q = g • Ideal.under (↥(B' ↥↑N.toOpenSubgroup)) P },
    map := fun {N N'} f ↦
      ↾fun x ↦ ⟨(QuotientGroup.map (↑N.toOpenSubgroup) N'.toOpenSubgroup.1 (MonoidHom.id G) ⋯) ↑x, ⋯⟩,
    map_id := ⋯, map_comp := ⋯ }
this✝ : ∀ (N : OpenNormalSubgroup G), Nonempty (F.obj N)
s : (j : OpenNormalSubgroup G) → F.obj j
hs : s ∈ F.sections
a : ↑(ProfiniteGrp.of G).toProfinite.toTop :=
  (ProfiniteGrp.Hom.hom (ProfiniteGrp.of G).isoLimittoFiniteQuotientFunctor.inv) ⟨fun N ↦ ↑(s N), ⋯⟩
this : ∀ (N : OpenNormalSubgroup G), ↑a = ↑(s N)
x : B
N : OpenNormalSubgroup G
hN : ↑N ⊆ ↑(MulAction.stabilizer G x)
⊢ x ∈ Q ↔ x ∈ a • P