mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Sets.Closeds

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : β → α
hf : IsInducing f
⊢ Function.Injective (map f ⋯)

Tactic:
intro A B h_images_eq
  apply SetLike.coe_injective
  replace h_images_eq : closure (f '' A) = closure (f '' B) := congr($h_images_eq)
  rw [← A.isClosed.closure_eq, hf.closure_eq_preimage_closure_image, h_images_eq,
    ← hf.closure_eq_preimage_closure_image, B.isClosed.closure_eq]

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s : Set α
H : IsQuasiSeparated s
h : IsEmbedding f
U V : Set β
hU : U ⊆ f '' s
hU' : IsOpen[inst✝] U
hU'' : IsCompact U
hV : V ⊆ f '' s
hV' : IsOpen[inst✝] V
hV'' : IsCompact V
⊢ V ⊆ range f

Tactic:
exact hV.trans (Set.image_subset_range _ _)

Goal state after:
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
h : ¬∀ t ∈ s, IsOpen[inst✝¹] t
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
⊢ IsCompact (⋂₀ s)

Tactic:
have heq : s = a ∪ b := subset_antisymm (by grind) (by grind)

Goal state after:
case inr
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSeparatedSpace α
s : Set (Set α)
hf : s.Finite
hne : s.Nonempty
ho : ∀ t ∈ s, IsOpen[inst✝¹] t ∨ IsClosed[inst✝¹] t
hc : ∀ t ∈ s, IsCompact t
this :
  ∀ {α : Type u_1} [inst : TopologicalSpace α] [QuasiSeparatedSpace α] {s : Set (Set α)},
    s.Finite →
      s.Nonempty → (∀ t ∈ s, IsOpen t ∨ IsClosed t) → (∀ t ∈ s, IsCompact t) → (∀ t ∈ s, IsOpen t) → IsCompact (⋂₀ s)
h : ¬∀ t ∈ s, IsOpen[inst✝¹] t
a : Set (Set α) := {t | t ∈ s ∧ IsOpen[inst✝¹] t}
b : Set (Set α) := {t | t ∈ s ∧ IsClosed[inst✝¹] t}
heq : s = a ∪ b
⊢ IsCompact (⋂₀ s)
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝¹ : LE P
inst✝ : IsCodirectedOrder P
I J : Ideal P
⊢ (↑I ∩ ↑J).Nonempty

Tactic:
obtain ⟨a, ha⟩ := I.nonempty

Goal state after:
P : Type u_1
inst✝¹ : LE P
inst✝ : IsCodirectedOrder P
I J : Ideal P
a : P
ha : a ∈ ↑I
⊢ (↑I ∩ ↑J).Nonempty
Module: Mathlib.Topology.QuasiSeparated

Goal state before:
pp: case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSeparatedSpace α
inst✝ : CompactSpace α
s : Set (Set α)
hf : s.Finite
ho : ∀ t ∈ s, IsOpen[inst✝²] t ∨ IsClosed[inst✝²] t
hc : ∀ t ∈ s, IsCompact t
hne : s.Nonempty
⊢ IsCompact (⋂₀ s)

Tactic:
exact QuasiSeparatedSpace.isCompact_sInter_of_nonempty hf hne ho hc

Goal state after:
Module: Mathlib.Order.Ideal

Goal state before:
pp: P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
⊢ x ∉ I ∨ xᶜ ∉ I

Tactic:
have h : xᶜ ∈ I → x ∉ I := hI.notMem_of_compl_mem
  tauto

Goal state after:
Module: Mathlib.Topology.Constructible

Goal state before:
pp: case a
X : Type u_2
inst✝ : TopologicalSpace X
ι : Type u_4
U : ι → Opens X
hU : IsOpenCover U
h₁ : ∀ (i : ι), IsRetrocompact ↑(U i)
h₂ : ∀ (i : ι), IsQuasiSeparated ↑(U i)
V₁ V₂ : Set X
ho₁ : IsOpen[inst✝] V₁
hc₁ : IsCompact V₁
ho₂ : IsOpen[inst✝] V₂
hc₂ : IsCompact V₂
t : Finset ι
ht : V₁ ⊆ ⋃ i ∈ t, (U i).carrier
⊢ ⋃ i ∈ t, ↑(U i) ∩ V₁ ∩ (↑(U i) ∩ V₂) ⊆ V₁ ∩ V₂

Tactic:
· aesop (add simp Set.subset_def)

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

Goal state before:
pp: case cons
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
this : (RelSeries.head L).asIdeal.LiesOver l.head.asIdeal
Q : Ideal S
Qlt : Q < (RelSeries.head L).asIdeal
hQ : Q.IsPrime
Qlo : Q.LiesOver q.asIdeal
⊢ ∃ L,
    L.length = (l.cons q lt).length ∧
      RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
        List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = (l.cons q lt).toList

Tactic:
use L.cons ⟨Q, hQ⟩ Qlt

Goal state after:
case h
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.HasGoingDown R S
l : RelSeries {(a, b) | a < b}
q : PrimeSpectrum R
lt : (q, l.head) ∈ {(a, b) | a < b}
ih :
  ∀ (P : Ideal S) [inst : P.IsPrime] [lo : P.LiesOver l.last.asIdeal],
    ∃ L,
      L.length = l.length ∧
        RelSeries.last L = { asIdeal := P, isPrime := ⋯ } ∧
          List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
P : Ideal S
inst✝ : P.IsPrime
lo : P.LiesOver l.last.asIdeal
L : LTSeries (PrimeSpectrum S)
len : L.length = l.length
last : RelSeries.last L = { asIdeal := P, isPrime := ⋯ }
spec : List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.toList L) = l.toList
this : (RelSeries.head L).asIdeal.LiesOver l.head.asIdeal
Q : Ideal S
Qlt : Q < (RelSeries.head L).asIdeal
hQ : Q.IsPrime
Qlo : Q.LiesOver q.asIdeal
⊢ (RelSeries.cons L { asIdeal := Q, isPrime := hQ } Qlt).length = (l.cons q lt).length ∧
    (RelSeries.cons L { asIdeal := Q, isPrime := hQ } Qlt).last = { asIdeal := P, isPrime := ⋯ } ∧
      List.map (PrimeSpectrum.comap (algebraMap R S)) (RelSeries.cons L { asIdeal := Q, isPrime := hQ } Qlt).toList =
        (l.cons q lt).toList
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
f g : R
⊢ zeroLocus {g} ⊆ zeroLocus {f} ↔ f ∈ (Ideal.span {g}).radical

Tactic:
zeroLocus_subset_zeroLocus_singleton_iff

Goal state after:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ f ∈ (Ideal.span {g}).radical ↔ f ∈ (Ideal.span {g}).radical
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Goal state before:
pp: G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 ↦ x ^ x_1
a : G
⊢ ∃ a_1, (fun x_1 ↦ f x ^ x_1) a_1 = a

Tactic:
obtain ⟨a, rfl⟩ := hf a

Goal state after:
G : Type u_2
G' : Type u_3
inst✝³ : Group G
inst✝² : Group G'
F : Type u_4
inst✝¹ : FunLike F G' G
inst✝ : MonoidHomClass F G' G
f : F
hf : Function.Surjective ⇑f
x : G'
hx : Function.Surjective fun x_1 ↦ x ^ x_1
a : G'
⊢ ∃ a_1, (fun x_1 ↦ f x ^ x_1) a_1 = f a
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
⊢ ∃ a, (toPiLocalization R) a = x

Tactic:
let algE a := IsLocalization.algEquiv (e.symm a).1.primeCompl
    (Localization.AtPrime (e.symm a).1) (Localization.Away a.1)

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
x : PiLocalization R
f : PrimeSpectrum R → R
hf : ∀ (p : PrimeSpectrum R), ↑(basicOpen (f p)) = {p}
e : PrimeSpectrum R ≃ ↑(Set.range f) := Equiv.ofInjective f ⋯
loc : ∀ (a : ↑(Set.range f)), IsLocalization.AtPrime (Localization.Away ↑a) (e.symm a).asIdeal
algE : (a : ↑(Set.range f)) → Localization.AtPrime (e.symm a).asIdeal ≃ₐ[R] Localization.Away ↑a :=
  fun a ↦
    IsLocalization.algEquiv (e.symm a).asIdeal.primeCompl (Localization.AtPrime (e.symm a).asIdeal)
      (Localization.Away ↑a)
⊢ ∃ a, (toPiLocalization R) a = x
Module: Mathlib.RingTheory.Spectrum.Prime.Topology

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x y : PrimeSpectrum R
h : x ⤳ y
a : R
ha : a ∈ y.asIdeal.primeCompl
⊢ IsUnit ((algebraMap R (Localization.AtPrime x.asIdeal)) ↑⟨a, ha⟩)

Tactic:
← PrimeSpectrum.le_iff_specializes,

Goal state after:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
x y : PrimeSpectrum R
h : x ≤ y
a : R
ha : a ∈ y.asIdeal.primeCompl
⊢ IsUnit ((algebraMap R (Localization.AtPrime x.asIdeal)) ↑⟨a, ha⟩)
Module: Mathlib.GroupTheory.Exponent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Monoid G
inst✝ : Nontrivial G
p : ℕ
hp : Nat.Prime p
hG : exponent G = p
g : G
hg : g ≠ 1
⊢ orderOf g = p

Tactic:
rw [Ne, ← orderOf_eq_one_iff] at hg
    exact Eq.symm <| (hp.dvd_iff_eq hg).mp <| hG ▸ Monoid.order_dvd_exponent g

Goal state after:
Module: Mathlib.GroupTheory.PGroup

Goal state before:
pp: case pos
p : ℕ
G : Type u_1
inst✝¹ : Group G
hp : Fact (Nat.Prime p)
P : Subgroup G
hP : IsPGroup p ↥P
H : Subgroup G
inst✝ : H.Normal
h_cop : H = ⊥
h1 : ¬Nat.card ↥H = 0
h2 : H.index = 0
⊢ P ≤ ⊥ ∨ Disjoint ⊥ P

Tactic:
exact Or.inr disjoint_bot_left

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

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ eval r (reflect (b.natDegree + (1 + c.natDegree)) (map (algebraMap R S) b * 1)) = 0

Tactic:
mul_one,

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap (comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ eval r (reflect (b.natDegree + (1 + c.natDegree)) (map (algebraMap R S) b)) = 0
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: p : ℕ
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Set ι
H : ι → Subgroup G
h : ∀ i ∈ s, IsPGroup p ↥(H i)
hn : ∀ i ∈ s, (H i).Normal
⊢ IsPGroup p ↥(⨆ i ∈ s, H i)

Tactic:
by
  rw [← iSup_subtype'']
  have : ∀ i : s, (H i).Normal := fun i ↦ hn i i.property
  exact iSup_of_normal _ fun i ↦ h i i.property

Goal state after:
Module: Mathlib.GroupTheory.Rank

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝³ : Group G
inst✝² : Group H
inst✝¹ : FG G
inst✝ : FG H
f : G →* H
hf : Surjective ⇑f
S : Finset G
hS1 : S.card = rank G
hS2 : Subgroup.closure ↑S = ⊤
⊢ (Finset.image (⇑f) S).card ≤ rank G

Tactic:
exact Finset.card_image_le.trans_eq hS1

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
⊢ Nat.Prime (orderOf g)

Tactic:
have h (n : ℕ) : orderOf g ∣ n ∨ n.Coprime (orderOf g) := by
    refine (IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).imp ?_ fun h ↦ ?_
    · simp [orderOf_dvd_iff_pow_eq_one]
    · simp only [Nat.coprime_iff_gcd_eq_one]
      have hgn : g ∈ Subgroup.zpowers (g ^ n) := by simp_all only [ne_eq, orderOf_eq_one_iff,
        Subgroup.mem_top]
      exact mem_zpowers_pow_iff.mp hgn

Goal state after:
α : Type u_1
inst✝¹ : CommGroup α
inst✝ : IsSimpleGroup α
g : α
hg : ∀ (x : α), x ∈ Subgroup.zpowers g
hα : orderOf g ≠ 1
h : ∀ (n : ℕ), orderOf g ∣ n ∨ n.Coprime (orderOf g)
⊢ Nat.Prime (orderOf g)
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: α : Type u_1
inst✝ : Group α
p : ℕ
hp : Nat.Prime p
hα : Nat.card α = p ^ 2
this✝ : Finite α
this : Nontrivial α
h_exp : exponent α = p
h_cyc : IsCyclic α
⊢ False

Tactic:
obtain (rfl | rfl) := eq_zero_or_one_of_sq_eq_self <| hα ▸ h_exp ▸ (h_cyc.exponent_eq_card).symm

Goal state after:
case inl
α : Type u_1
inst✝ : Group α
this✝ : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 0
hα : Nat.card α = 0 ^ 2
h_exp : exponent α = 0
⊢ False

case inr
α : Type u_1
inst✝ : Group α
this✝ : Finite α
this : Nontrivial α
h_cyc : IsCyclic α
hp : Nat.Prime 1
hα : Nat.card α = 1 ^ 2
h_exp : exponent α = 1
⊢ False
Module: Mathlib.GroupTheory.Torsion

Goal state before:
pp: case zero
G : Type u_1
inst✝ : CommMonoid G
p : ℕ
hp : Fact (Nat.Prime p)
p' : ℕ
hp' : Fact (Nat.Prime p')
hne : p ≠ p'
g : G
hg' : ∃ n, orderOf g = p' ^ n
hn : orderOf g = p ^ 0
⊢ g = 1

Tactic:
rwa [pow_zero, orderOf_eq_one_iff] at hn

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

Goal state before:
pp: G : Type u_2
inst✝¹ : CommGroup G
hG : IsCyclic G
inst✝ : Finite G
d : ℕ
g : G
h : Subgroup.zpowers g = ⊤
⊢ orderOf ((powMonoidHom d) g) = Nat.card G / (Nat.card G).gcd d

Tactic:
powMonoidHom_apply,

Goal state after:
G : Type u_2
inst✝¹ : CommGroup G
hG : IsCyclic G
inst✝ : Finite G
d : ℕ
g : G
h : Subgroup.zpowers g = ⊤
⊢ orderOf (g ^ d) = Nat.card G / (Nat.card G).gcd d
Module: Mathlib.GroupTheory.SpecificGroups.Cyclic

Goal state before:
pp: case refine_1.inr.inr
M : Type u_4
N : Type u_5
inst✝¹ : Group M
inst✝ : Group N
h : IsCyclic (M × N)
h✝¹ : Finite M
h✝ : Finite N
⊢ (Nat.card M).Coprime (Nat.card N)

Tactic:
apply coprime_card_of_isCyclic_prod

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: G : Type u
inst✝ : Group G
n p : ℕ
hp : Nat.Prime p
h : IsPGroup p G
H : Subgroup G
hn : p ^ n ≤ Nat.card ↥H
H' : Subgroup ↥H
H'card : Nat.card ↥H' = p ^ n
e : ↥H' ≃* ↥(Subgroup.map H.subtype H') := H'.equivMapOfInjective H.subtype ⋯
⊢ Nat.card ↥(Subgroup.map H.subtype H') = Nat.card ↥H'

Tactic:
exact Nat.card_congr e.symm.toEquiv

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case inr
G : Type u
inst✝³ : Group G
inst✝² : Finite G
hnc : ∀ (H : Subgroup G), IsCoatom H → H.Normal
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Finite (Sylow p G)
P : Sylow p G
K : Subgroup G
hK : IsCoatom K
hNK : normalizer ↑P ≤ K
⊢ normalizer ↑↑P = ⊤

Tactic:
· have := hnc _ hK
        have hPK : P ≤ K := le_trans le_normalizer hNK
        refine (hK.1 ?_).elim
        rw [← sup_of_le_right hNK, P.normalizer_sup_eq_top' hPK]

Goal state after:
Module: Mathlib.GroupTheory.Sylow

Goal state before:
pp: case refine_2.right
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
hn : ∀ {p : ℕ} [Fact (Nat.Prime p)] (P : Sylow p G), (↑P).Normal
this✝ : Fintype G
ps : Finset ℕ := ⋯
P : (p : ℕ) → Sylow p G := ⋯
this : (p : ℕ) → Fintype ↥↑(P p)
hcomm : _root_.Pairwise fun p₁ p₂ ↦ ∀ (x y : G), x ∈ P ↑p₁ → y ∈ P ↑p₂ → Commute x y
⊢ Fintype.card ((i : ↥ps) → ↥↑(P ↑i)) = Fintype.card G

Tactic:
· simp only [← Nat.card_eq_fintype_card]
    calc
      Nat.card (∀ p : ps, P p) = ∏ p : ps, Nat.card (P p) := Nat.card_pi
      _ = ∏ p : ps, p.1 ^ (Nat.card G).factorization p.1 := by
        congr 1 with ⟨p, hp⟩
        exact @card_eq_multiplicity _ _ _ p ⟨Nat.prime_of_mem_primeFactors hp⟩ (P p)
      _ = ∏ p ∈ ps, p ^ (Nat.card G).factorization p :=
        (Finset.prod_finset_coe (fun p => p ^ (Nat.card G).factorization p) _)
      _ = (Nat.card G).factorization.prod (· ^ ·) := rfl
      _ = Nat.card G := Nat.prod_factorization_pow_eq_self Nat.card_pos.ne'

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

Goal state before:
pp: M : Type u_4
inst✝³ : AddCommGroup M
R : Type u_6
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ (Module.annihilator R M).IsRadical

Tactic:
rw [← Submodule.annihilator_top, ← sSup_simples_eq_top, sSup_eq_iSup', Submodule.annihilator_iSup]

Goal state after:
M : Type u_4
inst✝³ : AddCommGroup M
R : Type u_6
inst✝² : CommRing R
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ (⨅ i, (↑i).annihilator).IsRadical
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
p : R[X]
f g : PolynomialModule R M
e₁ : (map R' f✝) (p • f) = Polynomial.map (algebraMap R R') p • (map R' f✝) f
e₂ : (map R' f✝) (p • g) = Polynomial.map (algebraMap R R') p • (map R' f✝) g
⊢ Polynomial.map (algebraMap R R') p • (map R' f✝) f + Polynomial.map (algebraMap R R') p • (map R' f✝) g =
    Polynomial.map (algebraMap R R') p • ((map R' f✝) f + (map R' f✝) g)

Tactic:
smul_add

Goal state after:
case add
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f✝ : M →ₗ[R] M'
p : R[X]
f g : PolynomialModule R M
e₁ : (map R' f✝) (p • f) = Polynomial.map (algebraMap R R') p • (map R' f✝) f
e₂ : (map R' f✝) (p • g) = Polynomial.map (algebraMap R R') p • (map R' f✝) g
⊢ Polynomial.map (algebraMap R R') p • (map R' f✝) f + Polynomial.map (algebraMap R R') p • (map R' f✝) g =
    Polynomial.map (algebraMap R R') p • (map R' f✝) f + Polynomial.map (algebraMap R R') p • (map R' f✝) g
Module: Mathlib.Algebra.Polynomial.Module.Basic

Goal state before:
pp: case single.monomial
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ single R' (n✝ + i) (a✝ • f m) = single R' (n✝ + i) ((algebraMap R R') a✝ • f m)

Tactic:
algebraMap_smul

Goal state after:
case single.monomial
R : Type u_2
M : Type u_3
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
R' : Type u_6
M' : Type u_7
inst✝⁵ : CommRing R'
inst✝⁴ : AddCommGroup M'
inst✝³ : Module R' M'
inst✝² : Module R M'
inst✝¹ : Algebra R R'
inst✝ : IsScalarTower R R' M'
f : M →ₗ[R] M'
i : ℕ
m : M
n✝ : ℕ
a✝ : R
⊢ single R' (n✝ + i) (a✝ • f m) = single R' (n✝ + i) (a✝ • f m)
Module: Mathlib.RingTheory.ReesAlgebra

Goal state before:
pp: R : Type u
inst✝ : CommRing R
I : Ideal R
hI : I.FG
⊢ (reesAlgebra I).FG

Tactic:
classical
    obtain ⟨s, hs⟩ := hI
    rw [← adjoin_monomial_eq_reesAlgebra, ← hs]
    use s.image (monomial 1)
    rw [Finset.coe_image]
    change
      _ =
        Algebra.adjoin R
          (Submodule.map (monomial 1 : R →ₗ[R] R[X]) (Submodule.span R ↑s) : Set R[X])
    rw [Submodule.map_span, Algebra.adjoin_span]

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

Goal state before:
pp: case add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
f g : PolynomialModule R M
e₁ : (eval r) (p • f) = Polynomial.eval r p • (eval r) f
e₂ : (eval r) (p • g) = Polynomial.eval r p • (eval r) g
⊢ Polynomial.eval r p • (eval r) f + Polynomial.eval r p • (eval r) g = Polynomial.eval r p • ((eval r) f + (eval r) g)

Tactic:
smul_add

Goal state after:
case add
R : Type u_2
M : Type u_3
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : R[X]
r : R
f g : PolynomialModule R M
e₁ : (eval r) (p • f) = Polynomial.eval r p • (eval r) f
e₂ : (eval r) (p • g) = Polynomial.eval r p • (eval r) g
⊢ Polynomial.eval r p • (eval r) f + Polynomial.eval r p • (eval r) g =
    Polynomial.eval r p • (eval r) f + Polynomial.eval r p • (eval r) g
Module: Mathlib.RingTheory.Finiteness.Nakayama

Goal state before:
pp: 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
hn : N.FG
hin : N ≤ I • N
⊢ ∃ r ∈ I, ∀ n ∈ N, r • n = n

Tactic:
obtain ⟨r, hr, hr'⟩ := exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hn hin
  exact ⟨-(r - 1), I.neg_mem hr, fun n hn => by simpa [sub_smul] using hr' n hn⟩

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
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
⊢ Submodule.span (↥(reesAlgebra I)) (⇑(lsingle R i) '' ↑s) = Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))

Tactic:
← Submodule.span_span_of_tower R,

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
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), single R i '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
⊢ Submodule.span ↥(reesAlgebra I) ↑(Submodule.span R (⇑(lsingle R i) '' ↑s)) =
    Submodule.span (↥(reesAlgebra I)) (single R i '' ↑(F.N i))
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
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ I₁ • ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
⊢ a • ⟨b, hb⟩ ∈ Submodule.comap (f.toLinearMap.restrict h) (Submodule.restrictScalars R (I₂ • ⊤))

Tactic:
simp only [SetLike.mk_smul_mk, smul_eq_mul, Submodule.mem_comap, Submodule.restrictScalars_mem]

Goal state after:
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
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I₁ : Ideal A
I₂ : Ideal B
f : A →ₐ[R] B
h : I₁ ≤ comap f I₂
x : ↥I₁
hx : x ∈ I₁ • ⊤
a : A
ha : a ∈ I₁
b : A
hb : b ∈ I₁
⊢ (f.toLinearMap.restrict h) ⟨a * b, ⋯⟩ ∈ I₂ • ⊤
Module: Mathlib.Algebra.Category.ModuleCat.Projective

Goal state before:
pp: R : Type u
inst✝² : Ring R
P : ModuleCat R
inst✝¹ : Small.{v, u} R
inst✝ : CategoryTheory.Projective P
⊢ Module.Projective R ↑P

Tactic:
refine Module.Projective.of_lifting_property ?_
  intro _ _ _ _ _ _ f g s
  have : Epi (↟f) := (ModuleCat.epi_iff_surjective (↟f)).mpr s
  exact ⟨(Projective.factorThru (↟g) (↟f)).hom,
    ModuleCat.hom_ext_iff.mp <| Projective.factorThru_comp (↟g) (↟f)⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : Cᵒᵖ ⥤ CommRingCat
F : C ⥤ D
S' R : Dᵒᵖ ⥤ CommRingCat
M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
φ : S ⟶ F.op ⋙ R
φ' : S' ⟶ R
d : M.Derivation φ
f : M ⟶ N
X : Cᵒᵖ
a : ↑(S.obj X)
⊢ ((ModuleCat.Hom.hom (f.app (F.op.obj X))).toAddMonoidHom.comp d.d) ((ConcreteCategory.hom (φ.app X)) a) = 0

Tactic:
dsimp
    erw [d_app]
    rw [map_zero]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i j : ι
r : c.Rel i j
⊢ imageSubobject (C.dTo j) = imageSubobject (C.d i j)

Tactic:
by
  rw [C.dTo_eq r]
  apply imageSubobject_iso_comp

Goal state after: