mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Maximal.Localization

Goal state before:
pp: ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
i : ι
I : MaximalSpectrum (R i)
hr :
  (toPiLocalization ((i : ι) → R i)) r { asIdeal := Ideal.comap (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ } =
    Function.update 0 { asIdeal := J, isMaximal := max } 1
      { asIdeal := Ideal.comap (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }
⊢ (toPiLocalization (R i)) (r i) I = (toPiLocalization (R i)) (0 i) I

Tactic:
dsimp only [toPiLocalization_apply_apply, Subtype.coe_mk] at hr

Goal state after:
ι : Type u_5
R : ι → Type u_4
inst✝² : (i : ι) → CommSemiring (R i)
inst✝¹ : ∀ (i : ι), Nontrivial (R i)
inst✝ : Infinite ι
surj : Function.Surjective ⇑(toPiLocalization ((i : ι) → R i))
J : Ideal ((i : ι) → R i)
max : J.IsMaximal
notMem : { asIdeal := J, isPrime := ⋯ } ∉ Set.range (PrimeSpectrum.sigmaToPi R)
r : (i : ι) → R i
i : ι
I : MaximalSpectrum (R i)
hr :
  (algebraMap ((i : ι) → R i) (Localization.AtPrime (Ideal.comap (Pi.evalRingHom R i) I.asIdeal))) r =
    Function.update 0 { asIdeal := J, isMaximal := max } 1
      { asIdeal := Ideal.comap (Pi.evalRingHom R i) I.asIdeal, isMaximal := ⋯ }
⊢ (toPiLocalization (R i)) (r i) I = (toPiLocalization (R i)) (0 i) I
Module: Mathlib.Topology.Sets.OpenCover

Goal state before:
pp: case neg
X : Type u_1
ι : Type u_2
inst✝ : TopologicalSpace X
U : ι → Opens X
hn : Pairwise ((fun x1 x2 ↦ ¬Disjoint x1 x2) on U)
h : ∀ (i : ι), IsPreirreducible ↑(U i)
s : Set X
hs : IsOpen[inst✝] s
hsU : s ⊆ ⋃ i, ↑(U i)
x✝ : X
hx : x✝ ∈ s
i : ι
hi : x✝ ∈ ↑(U i)
u : Set X
hu : u ∈ irreducibleComponents X
hUu : (U i).carrier ⊆ u
huniv : ¬s ⊆ u
huo : IsOpen[inst✝] uᶜ
a : X
ha₁ : a ∈ s
ha₂ : a ∉ u
j : ι
haj : a ∈ ↑(U j)
hji : j ≠ i
x : X
hx₁ : x ∈ ↑(U i)
hx₂ : x ∈ uᶜ
⊢ False

Tactic:
exact hx₂ <| hUu hx₁

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: α : Type u_2
inst✝ : TopologicalSpace α
U V : Opens α
⊢ ↑(U ⇨ V) = interior (↑U ⇨ ↑V)

Tactic:
by
  rw [himp_def, coe_interior]

Goal state after:
Module: Mathlib.Topology.LocallyClosed

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s = s ∪ (frontier s)ᶜ

Tactic:
by
  rw [coborder, compl_eq_comm, compl_union, compl_compl, ← sdiff_eq_compl_inter,
    ← union_sdiff_right, union_comm, ← closure_eq_self_union_frontier]

Goal state after:
Module: Mathlib.Topology.Sets.Opens

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
ι : Type u_5
U : ι → Opens X
hU : IsBasis (range U)
W : Opens X
hW : IsCompact W.carrier
κ : Type u
a : κ → ι
heq : W = ⨆ k, U (a k)
⊢ W.carrier ⊆ ⋃ i, (U (a i)).carrier

Tactic:
simp [heq]

Goal state after:
Module: Mathlib.Order.BooleanSubalgebra

Goal state before:
pp: case refine_1
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ (∃ t, a = t.sup fun x ↦ ↑x.1 \ ↑x.2) → a ∈ closure s

pp: case refine_2
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ ∀ x ∈ closure s,
    ∀ y ∈ closure s,
      (∃ t, x = t.sup fun x ↦ ↑x.1 \ ↑x.2) →
        (∃ t, y = t.sup fun x ↦ ↑x.1 \ ↑x.2) → ∃ t, x ⊔ y = t.sup fun x ↦ ↑x.1 \ ↑x.2

pp: case refine_3
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ ∀ x ∈ closure s, (∃ t, x = t.sup fun x ↦ ↑x.1 \ ↑x.2) → ∃ t, xᶜ = t.sup fun x ↦ ↑x.1 \ ↑x.2

Tactic:
· rintro ⟨t, rfl⟩
    exact t.sup_mem _ (subset_closure bot_mem) (fun _ h _ ↦ sup_mem h) _
      fun x hx ↦ sdiff_mem (subset_closure x.1.2) (subset_closure x.2.2)

Goal state after:
case refine_2
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ ∀ x ∈ closure s,
    ∀ y ∈ closure s,
      (∃ t, x = t.sup fun x ↦ ↑x.1 \ ↑x.2) →
        (∃ t, y = t.sup fun x ↦ ↑x.1 \ ↑x.2) → ∃ t, x ⊔ y = t.sup fun x ↦ ↑x.1 \ ↑x.2

case refine_3
α : Type u_2
inst✝ : BooleanAlgebra α
s : Set α
isSublattice : IsSublattice s
bot_mem : ⊥ ∈ s
top_mem : ⊤ ∈ s
a : α
⊢ ∀ x ∈ closure s, (∃ t, x = t.sup fun x ↦ ↑x.1 \ ↑x.2) → ∃ t, xᶜ = t.sup fun x ↦ ↑x.1 \ ↑x.2
Module: Mathlib.Topology.NoetherianSpace

Goal state before:
pp: α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
t : Set α
ht : t ⊆ ⋃ i, f i
⊢ IsCompact t

Tactic:
← Set.inter_eq_left.mpr ht,

Goal state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
ι : Type u_3
f : ι → Set α
inst✝ : Finite ι
hf : ∀ (i : ι), ∀ t ⊆ f i, IsCompact t
t : Set α
ht : t ⊆ ⋃ i, f i
⊢ IsCompact (t ∩ ⋃ i, f i)
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case e'_3
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
H : ∀ (i : ι), IsLocallyConstructible (↑(U i) ↓∩ s)
x✝ : X
i : ι
hi : x✝ ∈ U i
V : Set ↑↑(U i)
hVx : V ∈ 𝓝 ⟨x✝, hi⟩
hV : IsOpen[instTopologicalSpaceSubtype] V
hV' : IsConstructible (V ↓∩ ↑(U i) ↓∩ s)
e : ↑V ≃ₜ ↑(Subtype.val '' V) := (Equiv.Set.image Subtype.val V ⋯).toHomeomorphOfIsInducing ⋯
e_1✝ : ↑(Subtype.val '' V) = ↑(Subtype.val '' V)
x : { x // x ∈ (U i).carrier }
hx : x ∈ V
⊢ ⟨↑x, ⋯⟩ ∈ (Subtype.val '' V) ↓∩ s ↔ ⟨↑x, ⋯⟩ ∈ ⇑e.symm ⁻¹' V ↓∩ ↑(U i) ↓∩ s

Tactic:
simp [e, Equiv.toHomeomorphOfIsInducing]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Descent

Goal state before:
pp: A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
⊢ ComonadicLeftAdjoint (extendScalars f)

Tactic:
have := preservesFiniteLimits_extendScalars_of_flat hf.flat

Goal state after:
A B : Type u
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : f.FaithfullyFlat
this : PreservesFiniteLimits (extendScalars f)
⊢ ComonadicLeftAdjoint (extendScalars f)
Module: Mathlib.RingTheory.RingHom.Flat

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Flat
hg : g.Flat
⊢ (g.comp f).Flat

Tactic:
by
  algebraize [f, g, (g.comp f)]
  exact Module.Flat.trans R S T

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

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (vanishingIdeal s).IsRadical

Tactic:
rw [← vanishingIdeal_closure, ← zeroLocus_vanishingIdeal_eq_closure,
    vanishingIdeal_zeroLocus_eq_radical]

Goal state after:
R : Type u
inst✝ : CommSemiring R
s : Set (PrimeSpectrum R)
⊢ (vanishingIdeal s).radical.IsRadical
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case inr.mp
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
⊢ exponent G ∣ n → ∀ (g : G), g ^ n = 1

pp: case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
⊢ (∀ (g : G), g ^ n = 1) → exponent G ∣ n

Tactic:
· intro h g
    rw [Nat.dvd_iff_mod_eq_zero] at h
    rw [pow_eq_mod_exponent, h, pow_zero]

Goal state after:
case inr.mpr
G : Type u
inst✝ : Monoid G
n : ℕ
hpos : n > 0
⊢ (∀ (g : G), g ^ n = 1) → exponent G ∣ n
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: α : Type u_1
a : α
inst✝² : Group α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ha : ∀ (x : α), x ∈ zpowers a
⊢ image (fun i ↦ a ^ i) (range (Nat.card α)) = univ

Tactic:
← orderOf_eq_card_of_forall_mem_zpowers ha,

Goal state after:
α : Type u_1
a : α
inst✝² : Group α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
ha : ∀ (x : α), x ∈ zpowers a
⊢ image (fun i ↦ a ^ i) (range (orderOf a)) = univ
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : H →* G
hϕ : Function.Injective ⇑ϕ
⊢ IsPGroup p H

Tactic:
by
  simp_rw [IsPGroup, ← hϕ.eq_iff, ϕ.map_pow, ϕ.map_one]
  exact fun h => hG (ϕ h)

Goal state after:
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case H
G : Type u
inst✝ : CommMonoid G
h : ∀ (g : G), 0 < orderOf g
he : ExponentExists G
⊢ ∀ a ∈ Set.range fun g ↦ orderOf g, a ≤ exponent G

Tactic:
simp_rw [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
      exact orderOf_le_exponent he

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
⊢ #{a | orderOf a = m} = φ m

Tactic:
refine IH m hm.2 (hm.1.trans hd) (Finset.card_pos.2 ⟨a ^ (d / m), ?_⟩)

Goal state after:
α : Type u_1
inst✝² : Group α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hn : ∀ (n : ℕ), 0 < n → #{a | a ^ n = 1} ≤ n
d : ℕ
IH : ∀ m < d, m ∣ Fintype.card α → 0 < #{a | orderOf a = m} → #{a | orderOf a = m} = φ m
hd : d ∣ Fintype.card α
hpos : 0 < #{a | orderOf a = d}
hd0 : d ≠ 0
a : α
ha' : a ∈ {a | orderOf a = d}
ha : orderOf a = d
m : ℕ
hm : m ∣ d ∧ m < d
⊢ a ^ (d / m) ∈ {a | orderOf a = m}
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝² : Group G
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p ↥Q
hp : ⊥ < zpowers x
⊢ False

Tactic:
←
    comap_lt_comap_of_surjective (QuotientGroup.mk'_surjective _),

Goal state after:
p : ℕ
G : Type u_1
inst✝² : Group G
P : Sylow p G
inst✝¹ : (↑P).Normal
inst✝ : (↑P).FiniteIndex
h✝ : p ∣ Nat.card (G ⧸ ↑P)
x : G ⧸ ↑P
hx : orderOf x = p
h : IsPGroup p ↥(zpowers x)
Q : Subgroup G := comap (QuotientGroup.mk' ↑P) (zpowers x)
hQ : IsPGroup p ↥Q
hp : comap (QuotientGroup.mk' ↑P) ⊥ < comap (QuotientGroup.mk' ↑P) (zpowers x)
⊢ False
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: G : Type u_1
inst✝ : CommMonoid G
tG : IsMulTorsion G
⊢ torsion G = ⊤

Tactic:
ext; tauto

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
⊢ b ≤ iSup s → ∃ t, b ≤ ⨆ a_2 ∈ t, s a_2

Tactic:
hb

Goal state after:
α : Type u_2
inst✝ : CompleteLattice α
a : α
b : ↑(Iic a)
h : ∀ (ι : Type u_2) (s : ι → α), ↑b ≤ iSup s → ∃ t, ↑b ≤ ⨆ a ∈ t, s a
ι : Type u_2
s : ι → ↑(Iic a)
hb : b ≤ iSup s
⊢ ∃ t, b ≤ ⨆ a_1 ∈ t, s a_1
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝³ : CommGroup M
inst✝² : Group N
f : M →* N
h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)
inst✝¹ : IsCyclic ↥f.ker
inst✝ : IsCyclic ↥f.range
⊢ IsCyclic M

Tactic:
cases (finite_or_infinite f.ker).symm
  · rw [Nat.card_eq_zero_of_infinite, Nat.coprime_zero_left] at h
    rw [← f.range.eq_bot_iff_card, f.range_eq_bot_iff, ← f.ker_eq_top_iff] at h
    rwa [← Subgroup.topEquiv.isCyclic, ← h]
  cases (finite_or_infinite f.range).symm
  · rw [Nat.card_eq_zero_of_infinite (α := f.range), Nat.coprime_zero_right] at h
    rwa [(f.ofInjective (f.ker_eq_bot_iff.mp (f.ker.eq_bot_of_card_eq h))).isCyclic]
  have := f.finite_iff_finite_ker_range.mpr ⟨‹_›, ‹_›⟩
  rw [IsCyclic.iff_exponent_eq_card]
  apply dvd_antisymm Group.exponent_dvd_nat_card
  rw [← f.ker.card_mul_index, Subgroup.index_ker]
  apply h.mul_dvd_of_dvd_of_dvd <;> rw [← IsCyclic.exponent_eq_card]
  · exact Monoid.exponent_dvd_of_monoidHom _ f.ker.subtype_injective
  · exact MonoidHom.exponent_dvd f.rangeRestrict_surjective

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Intervals

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝² : CompleteLattice α
inst✝¹ : IsModularLattice α
inst✝ : IsCompactlyGenerated α
s : Set ι
f : ι → α
h : ∀ i ∈ s, ComplementedLattice ↑(Iic (f i))
h' : ⨆ i ∈ s, f i = ⊤
i : ι
hi : i ∈ s
⊢ ∃ t, f i = sSup t ∧ ∀ a ∈ t, IsAtom a

Tactic:
by
    replace h := complementedLattice_iff_isAtomistic.mp (h i hi)
    obtain ⟨u, hu, hu'⟩ := eq_sSup_atoms (⊤ : Iic (f i))
    refine ⟨(↑) '' u, ?_, ?_⟩
    · replace hu : f i = ↑(sSup u) := Subtype.ext_iff.mp hu
      simp_rw [hu, Iic.coe_sSup]
    · rintro b ⟨⟨a, ha'⟩, ha, rfl⟩
      exact IsAtom.of_isAtom_coe_Iic (hu' _ ha)

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝ : CommSemiring R
I : ι → Ideal R
this✝ : DecidableEq ι
a : ι
t : Finset ι
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, ↑(μ i) = 1) ↔ (↑t).Pairwise fun i j ↦ I i ⊔ I j = ⊤
this : Std.Symm fun x1 x2 ↦ I x1 ⊔ I x2 = ⊤
μ : (i : ι) → ↥(⨅ j ∈ Finset.cons a t hat, ⨅ (_ : j ≠ i), I j)
hμ : ↑(μ a) + ∑ x ∈ t, ↑(μ x) = 1
i : ι
⊢ ↑(μ i) ∈ ⨅ j ∈ t, ⨅ (_ : j ≠ i), I j

Tactic:
have := Submodule.coe_mem (μ i)
      simp only [mem_iInf] at this ⊢
      intro j hj ij
      exact this _ (Finset.subset_cons _ hj) ij

Goal state after:
Module: Mathlib.Order.JordanHolder

Goal state before:
pp: X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ (toList s₁).toFinset = (toList s₂).toFinset

Tactic:
simpa only [Finset.ext_iff, List.mem_toFinset, RelSeries.mem_toList]

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

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : Submodule R M
⊢ IsSimpleModule R ↥m ↔ IsAtom m

Tactic:
rw [← Set.isSimpleOrder_Iic_iff_isAtom, isSimpleModule_iff]
  exact m.mapIic.isSimpleOrder_iff

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

Goal state before:
pp: case inr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Ring S
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m : Submodule R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
this : Nontrivial M
⊢ ∃ a, ⊤ = R ∙ a

Tactic:
have ⟨m, hm⟩ := exists_ne (0 : M)

Goal state after:
case inr
ι : Type u_1
R : Type u_2
S : Type u_3
inst✝⁶ : Ring R
inst✝⁵ : Ring S
M : Type u_4
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
m✝ : Submodule R M
N : Type u_5
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsSimpleModule R M
this : Nontrivial M
m : M
hm : m ≠ 0
⊢ ∃ a, ⊤ = R ∙ a
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: case refine_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsSimpleModule R M
this : Nontrivial M
⊢ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)

Tactic:
have ⟨m, hm⟩ := exists_ne (0 : M)

Goal state after:
case refine_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : IsSimpleModule R M
this : Nontrivial M
m : M
hm : m ≠ 0
⊢ ∃ I, I.IsMaximal ∧ Nonempty (M ≃ₗ[R] R ⧸ I)
Module: Mathlib.RingTheory.SimpleModule.Basic

Goal state before:
pp: R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t ↦ Bool.rec q p t
⊢ IsSemisimpleModule R ↥(p ⊔ q)

Tactic:
rw [show p ⊔ q = ⨆ i ∈ Set.univ, f i by rw [iSup_univ, iSup_bool_eq]]

Goal state after:
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p q : Submodule R M
x✝¹ : IsSemisimpleModule R ↥p
x✝ : IsSemisimpleModule R ↥q
f : Bool → Submodule R M := fun t ↦ Bool.rec q p t
⊢ IsSemisimpleModule R ↥(⨆ i ∈ Set.univ, f i)
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
h : x✝ ∈ torsionBy R M 1
⊢ x✝ ∈ ⊥

Tactic:
rw [mem_torsionBy_iff, one_smul] at h

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
h : x✝ = 0
⊢ x✝ ∈ ⊥
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: case insert.refine_2
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
s✝ : Set M
i : M
s : Set M
a✝ : i ∉ s
hs✝ : s.Finite
ih :
  (∃ r, r - 1 ∈ I ∧ N ≤ comap ((LinearMap.lsmul R M) r) (I • span R s) ∧ s ⊆ ↑N) → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
r : R
hr1 : r - 1 ∈ I
hs : i ∈ ↑N ∧ s ⊆ ↑N
c : R
hc1 : c - 1 ∈ I
hci : c • i ∈ I • span R s
n : M
hn : n ∈ N
z : M
hz : z ∈ I • span R s
d : R
left✝ : d ∈ I
hyz : d • i + z = r • n
⊢ d • c • i + c • z ∈ I • span R s

Tactic:
exact add_mem (smul_mem _ _ hci) (smul_mem _ _ hz)

Goal state after:
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : Quotient.mk (a • x) = 0
⊢ Quotient.mk'' x ∈ ⊥

Tactic:
Quotient.mk_eq_zero

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • x ∈ torsion R M
⊢ Quotient.mk'' x ∈ ⊥
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this✝ : map N.mkQ (I • N') = map N.mkQ N'
this : comap N.mkQ (map N.mkQ N') = comap N.mkQ (map N.mkQ (J • N'))
⊢ N ⊔ N' = N ⊔ J • N'

Tactic:
comap_map_eq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this✝ : map N.mkQ (I • N') = map N.mkQ N'
this : N' ⊔ N.mkQ.ker = comap N.mkQ (map N.mkQ (J • N'))
⊢ N ⊔ N' = N ⊔ J • N'
Module: Mathlib.Algebra.Module.Torsion.Basic

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • x ∈ torsion R M
⊢ Quotient.mk x = 0

Tactic:
Quotient.mk_eq_zero

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
z : M ⧸ torsion R M
x : M
x✝ : Quotient.mk'' x ∈ torsion R (M ⧸ torsion R M)
a : ↥R⁰
hax : a • x ∈ torsion R M
⊢ x ∈ torsion R M
Module: Mathlib.RingTheory.Nakayama

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this✝ : map N.mkQ (I • N') = map N.mkQ N'
this : N' ⊔ N.mkQ.ker = comap N.mkQ (map N.mkQ (J • N'))
⊢ N ⊔ N' = N ⊔ J • N'

Tactic:
comap_map_eq,

Goal state after:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : N'.FG
hIJ : I ≤ J.jacobson
hNN : N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap N.mkQ)
this✝ : map N.mkQ (I • N') = map N.mkQ N'
this : N' ⊔ N.mkQ.ker = J • N' ⊔ N.mkQ.ker
⊢ N ⊔ N' = N ⊔ J • N'
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: case a
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
⊢ F.submodule.toAddSubmonoid ≤ AddSubmonoid.closure (⋃ i, single R i '' ↑(F.N i))

Tactic:
· intro f hf
    rw [← f.ofCoeff_coeff, ← f.coeff.sum_single, ofCoeff_finsuppSum]
    apply AddSubmonoid.sum_mem _ _
    rintro c -
    exact AddSubmonoid.subset_closure (Set.subset_iUnion _ c <| Set.mem_image_of_mem _ (hf c))

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

Goal state before:
pp: case refine_2
R : Type u
S : Type v
S' : Type w
inst✝⁶ : CommRing R
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : CommSemiring S'
inst✝² : Algebra S' R
inst✝¹ : Algebra S S'
inst✝ : IsScalarTower S S' R
I : Ideal R
⊢ Function.Surjective fun c ↦ ⟨I.cotangentToQuotientSquare c, ⋯⟩

Tactic:
· rintro ⟨_, x, hx, rfl⟩
    exact ⟨I.toCotangent ⟨x, hx⟩, Subtype.ext rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F : I.Filtration M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
this : IsNoetherian ↥(reesAlgebra I) ↥F.submodule
⊢ F'.submodule.FG

Tactic:
rw [isNoetherian_submodule] at this

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
I : Ideal R
F : I.Filtration M
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
this : ∀ s ≤ F.submodule, s.FG
⊢ F'.submodule.FG
Module: Mathlib.RingTheory.Ideal.Cotangent

Goal state before:
pp: case a
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsLocalRing R
fg : (maximalIdeal R).FG
s : Set ↥(maximalIdeal R)
hs_card : Cardinal.mk ↑s = ⊤.spanRank
hs_span : Submodule.span R s = ⊤
hs_span' : Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s) = ⊤
⊢ (Submodule.span (ResidueField R) (⇑(maximalIdeal R).toCotangent '' s)).spanRank ≤ Cardinal.mk ↑s

Tactic:
grw [Submodule.spanRank_span_le_card, Cardinal.mk_image_le]

Goal state after:
Module: Mathlib.RingTheory.Filtration

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
I : Ideal R
inst✝¹ : IsNoetherianRing R
inst✝ : IsLocalRing R
h : I ≠ ⊤
⊢ ⨅ i, I ^ i = ⊥

Tactic:
convert! I.iInf_pow_smul_eq_bot_of_isLocalRing (M := R) h
  ext i
  rw [smul_eq_mul, ← Ideal.one_eq_top, mul_one]

Goal state after:
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ (if i = j then X✝ else 0) = X✝

Tactic:
if_pos h

Goal state after:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ X✝ = X✝
Module: Mathlib.Algebra.Homology.Single

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ Y✝ = if i = j then Y✝ else 0

Tactic:
if_pos h

Goal state after:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
X✝ Y✝ : V
f : X✝ ⟶ Y✝
i : ι
h : i = j
⊢ Y✝ = Y✝
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a.refine_1
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
⊢ 0 ∈ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)

Tactic:
exact zero_mem _

Goal state after:
Module: Mathlib.Algebra.Homology.Additive

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁷ : Category.{v, u} V
inst✝⁶ : Preadditive V
W : Type u_2
inst✝⁵ : Category.{v_1, u_2} W
inst✝⁴ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝³ : Category.{v_2, u_3} W₁
inst✝² : Category.{v_3, u_4} W₂
inst✝¹ : HasZeroMorphisms W₁
inst✝ : HasZeroMorphisms W₂
c : ComplexShape ι
C D : HomologicalComplex V c
f✝ : C ⟶ D
i✝ : ι
n : ℕ
f : C ⟶ D
i j : ι
x✝ : c.Rel i j
⊢ (n • f.f i) ≫ D.d i j = C.d i j ≫ (n • f.f j)

Tactic:
simp [Preadditive.nsmul_comp, Preadditive.comp_nsmul]

Goal state after: