mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k G
B : Rep k H
f : G →* H
φ : A ⟶ res f B
n : ℕ
⊢ chainsMap₂ f φ ≫ (shortComplexH2 B).g = (shortComplexH2 A).g ≫ chainsMap₁ f φ

Tactic:
by
    simp only [shortComplexH2]
    ext : 3
    simpa [d₂₁, map_add, map_sub, ← map_inv]
      using congr(Finsupp.single _ $((hom_comm_apply φ _ _).symm))

Goal state after:
Module: Mathlib.RingTheory.Ideal.AssociatedPrime.Localization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
⊢ Ideal.comap (algebraMap R R') p ≤ (⊥.colon {↑(∏ a, g a) • m}).radical

pp: case refine_2
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
r : R
hr : r ∈ (⊥.colon {↑(∏ a, g a) • m}).radical
⊢ r ∈ Ideal.comap (algebraMap R R') p

Tactic:
· rw [← hT, Ideal.span_le]
    intro a ha
    simp only [SetLike.mem_coe, Ideal.mem_radical_iff, mem_bot, mem_colon_singleton]
    obtain ⟨u, hu⟩ : g ⟨a, ha⟩ ∣ (∏ a, g a) := by
      apply Finset.dvd_prod_of_mem g (Finset.mem_univ ⟨a, ha⟩)
    use e ⟨a, ha⟩
    rw [hu, Submonoid.coe_mul, smul_smul, ← mul_assoc, mul_comm, ← smul_smul, mul_comm, ← smul_smul]
    exact smul_eq_zero_of_right u.1 (hg ⟨a, ha⟩)

Goal state after:
case refine_2
R : Type u_1
inst✝⁹ : CommRing R
S : Submonoid R
R' : Type u_2
inst✝⁸ : CommRing R'
inst✝⁷ : Algebra R R'
hSR' : IsLocalization S R'
M : Type u_3
M' : Type u_4
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R M'
f : M →ₗ[R] M'
inst✝² : IsLocalizedModule S f
inst✝¹ : Module R' M'
inst✝ : IsScalarTower R R' M'
p : Ideal R'
hp : p.IsPrime
T : Finset R
hT : Ideal.span ↑T = Ideal.comap (algebraMap R R') p
m : M
s : ↥S
hx : p = (⊥.colon {IsLocalizedModule.mk' f m s}).radical
e : ↥T → ℕ
g : ↥T → ↥S
hg : ∀ (a : ↥T), g a • ↑a ^ e a • m = 0
r : R
hr : r ∈ (⊥.colon {↑(∏ a, g a) • m}).radical
⊢ r ∈ Ideal.comap (algebraMap R R') p
Module: Mathlib.RingTheory.DividedPowers.Basic

Goal state before:
pp: case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
hn : ¬n = 0
⊢ (if n = 0 then if m = 0 then 1 else 0 else 0) = if m = 0 ∧ n = 0 then ↑((m + n).choose m) else 0

Tactic:
if_neg hn,

Goal state after:
case neg
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
m n : ℕ
x : A
hx : x ∈ ⊥
hn : ¬n = 0
⊢ 0 = if m = 0 ∧ n = 0 then ↑((m + n).choose m) else 0
Module: Mathlib.RingTheory.DividedPowers.DPMorphism

Goal state before:
pp: A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx : x ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}
n : ℕ
⊢ f r ^ n * f (hI.dpow n x) = hJ.dpow n (f r * f x)

Tactic:
hJ.dpow_mul (hf (mem_map_of_mem f hx.1)),

Goal state after:
A✝ : Type u_1
B✝ : Type u_2
inst✝³ : CommSemiring A✝
inst✝² : CommSemiring B✝
I✝ : Ideal A✝
J✝ : Ideal B✝
hI✝ : DividedPowers I✝
hJ✝ : DividedPowers J✝
A : Type u_3
B : Type u_4
inst✝¹ : CommSemiring A
inst✝ : CommSemiring B
I : Ideal A
J : Ideal B
hI : DividedPowers I
hJ : DividedPowers J
f : A →+* B
hf : map f I ≤ J
r x : A
hx : x ∈ {x | x ∈ I ∧ ∀ (n : ℕ), f (hI.dpow n x) = hJ.dpow n (f x)}
n : ℕ
⊢ f r ^ n * f (hI.dpow n x) = f r ^ n * hJ.dpow n (f x)
Module: Mathlib.RingTheory.DividedPowers.RatAlgebra

Goal state before:
pp: case pos
A : Type u_1
inst✝¹ : CommSemiring A
I : Ideal A
inst✝ : DecidablePred fun x ↦ x ∈ I
n : ℕ
hn_fac : IsUnit ↑(n - 1)!
hnI : I ^ n = 0
m : ℕ
x : A
hx : x ∈ I
y : A
hy : y ∈ I
hmn : m < n
⊢ dpow I m (x + y) = ∑ k ∈ Finset.antidiagonal m, dpow I k.1 x * dpow I k.2 y

Tactic:
exact dpow_add_of_lt hn_fac hmn hx hy

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ IsSMulRegular M b ∧ IsSMulRegular (M ⧸ a • ⊤) b

Tactic:
and_iff_left hb

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
a b : R
h2 : IsSMulRegular M b
ha : IsSMulRegular M a
hb : IsSMulRegular (QuotSMulTop a M) b
⊢ IsSMulRegular M b
Module: Mathlib.RingTheory.Regular.RegularSequence

Goal state before:
pp: case cons
R : Type u_1
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
rs : List R
h✝ : IsWeaklyRegular M rs
rs' : List R
h'' : rs ~ rs'
h' :
  ∀ (a b : R) (rs' : List R),
    a :: b :: rs' <+~ rs →
      let K := torsionBy R (M ⧸ Ideal.ofList rs' • ⊤) b;
      K = a • K → K = ⊥
rs₁ rs₂ : List R
r : R
l₁✝ l₂✝ : List R
a✝ : l₁✝ ~ l₂✝
ih :
  ∀ (rs₀ : List R),
    rs₀ ++ l₁✝ <+~ rs →
      rs₀ ++ l₂✝ <+~ rs →
        IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₁✝ → IsWeaklyRegular (M ⧸ Ideal.ofList rs₀ • ⊤) l₂✝
rs₀ : List R
H₁ : rs₀ ++ r :: l₁✝ <+~ rs
H₃ : rs₀ ++ r :: l₂✝ <+~ rs
h : IsSMulRegular (M ⧸ Ideal.ofList rs₀ • ⊤) r ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₀) • ⊤) l₁✝
e : (M ⧸ Ideal.ofList (r :: rs₀) • ⊤) ≃ₗ[R] QuotSMulTop r (M ⧸ Ideal.ofList rs₀ • ⊤) :=
  quotOfListConsSMulTopEquivQuotSMulTopOuter M r rs₀
⊢ IsSMulRegular (M ⧸ Ideal.ofList rs₀ • ⊤) r ∧ IsWeaklyRegular (M ⧸ Ideal.ofList (r :: rs₀) • ⊤) l₂✝

Tactic:
refine h.imp_right (ih (r :: rs₀) ?_ ?_) <;>
      exact List.perm_middle.subperm_right.mp ‹_›

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

Goal state before:
pp: case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∈ S
⊢ ⊤.carrier ⊓ J.carrier = I ⊓ ↑(⨅ (_ : J ∈ S), ⟨J.carrier, ⋯⟩)

Tactic:
ciInf_pos hJ

Goal state after:
case pos
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI : DividedPowers I
S : Set hI.SubDPIdeal
J : hI.SubDPIdeal
hJ : J ∈ S
⊢ ⊤.carrier ⊓ J.carrier = I ⊓ ↑⟨J.carrier, ⋯⟩
Module: Mathlib.RingTheory.DividedPowers.SubDPIdeal

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

Tactic:
apply And.intro (I.add_mem ha.1 hb.1) (fun n ↦ ?_)

Goal state after:
A : Type u_1
inst✝ : CommSemiring A
I : Ideal A
hI hI' : DividedPowers I
a b : A
ha : a ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
hb : b ∈ {a | a ∈ I ∧ ∀ (n : ℕ), hI.dpow n a = hI'.dpow n a}
n : ℕ
⊢ hI.dpow n (a + b) = hI'.dpow n (a + b)
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
f : A →+* B
J : Ideal B
hf : Function.Surjective ⇑f
hIJ : J = Ideal.map f I
hIf : hI.IsSubDPIdeal (RingHom.ker f ⊓ I)
m✝ n✝ : ℕ
x✝ : B
hx : x✝ ∈ J
⊢ dpow hI f m✝ x✝ * dpow hI f n✝ x✝ = ↑((m✝ + n✝).choose m✝) * dpow hI f (m✝ + n✝) x✝

Tactic:
by
    obtain ⟨a, ha, rfl⟩ := (mem_map_iff_of_surjective f hf).mp (hIJ ▸ hx)
    simp only [dpow_apply' hI hIf ha]
    rw [← _root_.map_mul, hI.mul_dpow ha, _root_.map_mul, map_natCast]

Goal state after:
Module: Mathlib.RingTheory.GradedAlgebra.TensorProduct

Goal state before:
pp: ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
i j : ι
⊢ ∀ {gi gj : S ⊗[R] A},
    gi ∈ Submodule.baseChange S (𝒜 i) → gj ∈ Submodule.baseChange S (𝒜 j) → gi * gj ∈ Submodule.baseChange S (𝒜 (i + j))

Tactic:
suffices h : ((𝒜 i).baseChange S).map₂ (Algebra.lmul S (S ⊗[R] A)) ((𝒜 j).baseChange S) ≤
      (𝒜 (i + j)).baseChange S from fun xi xj ↦ (h <| apply_mem_map₂ _ · ·)

Goal state after:
ι : Type u_1
R : Type u_2
A : Type u_3
S : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : Algebra R S
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : Semiring A
inst✝¹ : Algebra R A
𝒜 : ι → Submodule R A
inst✝ : GradedAlgebra 𝒜
i j : ι
⊢ Submodule.map₂ (↑(Algebra.lmul S (S ⊗[R] A))) (Submodule.baseChange S (𝒜 i)) (Submodule.baseChange S (𝒜 j)) ≤
    Submodule.baseChange S (𝒜 (i + j))
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⟦Γ⟧
hx : ¬0 < x.orderTop
f : PowerSeries R
⊢ powerSeriesFamily x f = powerSeriesFamily 0 f

Tactic:
ext n g

Goal state after:
Γ : 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⟦Γ⟧
hx : ¬0 < x.orderTop
f : PowerSeries R
n : ℕ
g : Γ
⊢ ((powerSeriesFamily x f) n).coeff g = ((powerSeriesFamily 0 f) n).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✝ : AddCommMonoid R
e : α ≃ β
s : SummableFamily Γ R α
⊢ (⋃ a, (s (e.symm a)).support).IsPWO

Tactic:
by
    refine Set.IsPWO.mono s.isPWO_iUnion_support fun g => ?_
    simp only [Set.mem_iUnion, mem_support, ne_eq, forall_exists_index]
    exact fun b hg => Exists.intro (e.symm b) hg

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

Tactic:
by_cases hd₁ : d 1 = 0

Goal state after:
case pos
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : d 1 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0

case neg
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
d : Fin (Nat.succ 0).succ →₀ ℕ
hd : d ≠ single 0 1
hd₁ : ¬d 1 = 0
⊢ (coeff d) F.toPowerSeries • (coeff (single () 1)) (d.prod fun s e ↦ ![PowerSeries.X, 0] s ^ e) = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ constantCoeff (subst ![PowerSeries.X, 0] F.toPowerSeries) = 0

Tactic:
PowerSeries.X,

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ constantCoeff (subst ![X (), 0] F.toPowerSeries) = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «1»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![PowerSeries.X, 0] F.toPowerSeries)
⊢ subst (fun x ↦ subst ![PowerSeries.X, 0] F.toPowerSeries) (![PowerSeries.X, 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![subst ![PowerSeries.X, 0] F.toPowerSeries, 0] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
· simp [← PowerSeries.subst_def, ← PowerSeries.coe_substAlgHom this]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ constantCoeff (subst ![0, PowerSeries.X] F.toPowerSeries) = 0

Tactic:
PowerSeries.X,

Goal state after:
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
⊢ constantCoeff (subst ![0, X ()] F.toPowerSeries) = 0
Module: Mathlib.RingTheory.FormalGroup.Basic

Goal state before:
pp: case «0»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ subst (fun x ↦ subst ![0, PowerSeries.X] F.toPowerSeries) (![0, PowerSeries.X] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ![0, subst ![0, PowerSeries.X] F.toPowerSeries] ((fun i ↦ i) ⟨0, ⋯⟩)

pp: case «1»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ subst (fun x ↦ subst ![0, PowerSeries.X] F.toPowerSeries) (![0, PowerSeries.X] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![0, subst ![0, PowerSeries.X] F.toPowerSeries] ((fun i ↦ i) ⟨1, ⋯⟩)

Tactic:
· simp [← PowerSeries.subst_def, ← PowerSeries.coe_substAlgHom this]

Goal state after:
case «1»
R : Type u_1
inst✝ : CommRing R
F : FormalGroup R
this : PowerSeries.HasSubst (subst ![0, PowerSeries.X] F.toPowerSeries)
⊢ subst (fun x ↦ subst ![0, PowerSeries.X] F.toPowerSeries) (![0, PowerSeries.X] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![0, subst ![0, PowerSeries.X] F.toPowerSeries] ((fun i ↦ i) ⟨1, ⋯⟩)
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
q : Ideal R
h₁ : q.IsPrime
h₂ : q < IsLocalRing.maximalIdeal R
this : IsArtinianRing (R ⧸ I)
⊢ IsNilpotent (map (algebraMap R (Localization.AtPrime q)) q)

Tactic:
let f := algebraMap R (Localization.AtPrime q)

Goal state after:
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)
⊢ IsNilpotent (map (algebraMap R (Localization.AtPrime q)) q)
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot (L ⊓ K) K
k : A
hk : k ∈ K
I : Ideal A
hI : I ∈ F
hI_le : I ≤ Submodule.colon (L ⊓ K) {k}
⊢ ∃ I ∈ F, I ≤ Submodule.colon L {k}

Tactic:
have hcol : (L ⊓ K).colon {k} = Submodule.colon L {k} :=
      Submodule.colon_inf_eq_left_of_subset (Set.singleton_subset_iff.mpr hk)

Goal state after:
case mp
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot (L ⊓ K) K
k : A
hk : k ∈ K
I : Ideal A
hI : I ∈ F
hI_le : I ≤ Submodule.colon (L ⊓ K) {k}
hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
⊢ ∃ I ∈ F, I ≤ Submodule.colon L {k}
Module: Mathlib.RingTheory.IdealFilter.Basic

Goal state before:
pp: case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot L K
k : A
hk : k ∈ K
I : Ideal A
hI : I ∈ F
hI_le : I ≤ Submodule.colon L {k}
⊢ ∃ I ∈ F, I ≤ Submodule.colon (L ⊓ K) {k}

Tactic:
have hcol : (L ⊓ K).colon {k} = Submodule.colon L {k} :=
      Submodule.colon_inf_eq_left_of_subset (Set.singleton_subset_iff.mpr hk)

Goal state after:
case mpr
A : Type u_1
inst✝ : Ring A
F : IdealFilter A
L K : Ideal A
h : F.IsTorsionQuot L K
k : A
hk : k ∈ K
I : Ideal A
hI : I ∈ F
hI_le : I ≤ Submodule.colon L {k}
hcol : Submodule.colon (L ⊓ K) {k} = Submodule.colon L {k}
⊢ ∃ I ∈ F, I ≤ Submodule.colon (L ⊓ K) {k}
Module: Mathlib.Topology.Algebra.ClopenNhdofOne

Goal state before:
pp: case a
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
⊢ False

Tactic:
have einU : 1 ∈ U := by
      refine Set.mem_compl (fun ⟨l, hl, (hgl : g * l = 1)⟩ ↦ ?_)
      rw [← inv_eq_iff_mul_eq_one] at hgl
      exact hg_not <| inv_mem_iff.mp (hgl ▸ hl)

Goal state after:
case a
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
einU : 1 ∈ U
⊢ False
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
I : Ideal R
h : I ≤ Ring.jacobson R
⊢ ringKrullDim R ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)

Tactic:
by
  nontriviality R
  rw [ringKrullDim_le_iff_isMaximal_height_le]
  intro m hm
  exact height_le_ringKrullDim_quotient_add_spanFinrank <|
    le_trans h <| Ring.jacobson_le_of_isMaximal m

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, x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪

Tactic:
let q : PrimeSpectrum R := ⟨q, hq.1.1⟩

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 := ⋯ }
⊢ ∃ q, x ∈ q.asIdeal ∧ p₀ < q ∧ q.asIdeal < 𝔪
Module: Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsNoetherianRing R
s : Set R
hs : s ⊆ ↑(Ring.jacobson R)
⊢ ringKrullDim R ≤ ringKrullDim (R ⧸ Ideal.span s) + ↑s.encard

Tactic:
refine le_trans (ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank (Ideal.span s) ?_) ?_
  · simpa [Ideal.span_le]
  · gcongr; norm_cast; exact Submodule.spanFinrank_span_le_encard _

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
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := lq.map (PrimeSpectrum.comap (Quotient.mk (map (algebraMap R S) p))) ⋯
this✝ : (RelSeries.head l').asIdeal.LiesOver (RelSeries.last lp).asIdeal
lp' : LTSeries (PrimeSpectrum S)
hlp'len : lp'.length = lp.length
hlp' : RelSeries.last lp' = { asIdeal := (RelSeries.head l').asIdeal, isPrime := ⋯ }
right✝ : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList lp') = RelSeries.toList lp
this : (RelSeries.smash lp' l' hlp').length = lp.length + lq.length
⊢ ↑(RelSeries.smash lp' l' hlp').length ≤ Order.height { asIdeal := P, isPrime := inst✝¹ }

Tactic:
apply Order.length_le_height

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
inst✝³ : Algebra.HasGoingDown R S
p : Ideal R
inst✝² : p.IsPrime
P : Ideal S
inst✝¹ : P.IsPrime
inst✝ : P.LiesOver p
lp : LTSeries (PrimeSpectrum R)
hlp : RelSeries.last lp = { asIdeal := p, isPrime := ⋯ }
hlenp : ↑lp.length = p.height
lq : LTSeries (PrimeSpectrum (S ⧸ map (algebraMap R S) p))
hlq : RelSeries.last lq = { asIdeal := map (Quotient.mk (map (algebraMap R S) p)) P, isPrime := ⋯ }
hlenq : ↑lq.length = (map (Quotient.mk (map (algebraMap R S) p)) P).height
l' : LTSeries (PrimeSpectrum S) := ⋯
this✝ : (RelSeries.head l').asIdeal.LiesOver (RelSeries.last lp).asIdeal
lp' : LTSeries (PrimeSpectrum S)
hlp'len : lp'.length = lp.length
hlp' : RelSeries.last lp' = { asIdeal := (RelSeries.head l').asIdeal, isPrime := ⋯ }
right✝ : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList lp') = RelSeries.toList lp
this : (RelSeries.smash lp' l' hlp').length = lp.length + lq.length
⊢ (RelSeries.smash lp' l' hlp').last ≤ { asIdeal := P, isPrime := inst✝¹ }
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) ⋯
⊢ ↑p.length + 1 ≤ ⨆ p, ↑p.length

Tactic:
obtain ⟨r, hrm, hr⟩ := exists_minimalPrimes_le (mem_support_iff_of_finite.mp q.head.2)

Goal state after:
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
⊢ ↑p.length + 1 ≤ ⨆ p, ↑p.length
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
⊢ J' ∈ {I ∈ s | (I.colon Set.univ).radical = (J'.colon Set.univ).radical}

Tactic:
by simp [hJ']

Goal state after:
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 ↔ ⨆ m, injectiveDimension (M.localizedModule m.asIdeal.primeCompl) ≤ ↑n
⊢ injectiveDimension M ≤ ⊥ ↔ ⨆ p, injectiveDimension (M.localizedModule p.asIdeal.primeCompl) ≤ ⊥

Tactic:
simp only [le_bot_iff, injectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton,
      iSup_eq_bot, ModuleCat.localizedModule, ← Equiv.subsingleton_congr (equivShrink _)]
    refine ⟨fun h p ↦ LocalizedModule.instSubsingleton _, fun h ↦ ?_⟩
    apply Module.subsingleton_of_localization_maximal (R := R)
      (fun p ↦ LocalizedModule p.primeCompl M) (fun p ↦ LocalizedModule.mkLinearMap p.primeCompl M)
    intro p hp
    exact h ⟨p, hp⟩

Goal state after: