mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
f : α → Multiset β
f' : α → List β
h' : ∀ (a : α), f a = ↑(f' a)
this : f = fun a ↦ ↑(f' a)
x✝ : Std.Symm fun a b ↦ a.Disjoint b
⊢ (s.bind f).Nodup ↔ (∀ (a : α), a ∈ s → (f a).Nodup) ∧ Pairwise (Disjoint on f) s

Tactic:
exact Quot.induction_on s <| by
    unfold Function.onFun
    simp [this, List.nodup_flatMap, pairwise_coe_iff_pairwise]

Goal state after:
Module: Mathlib.Data.Multiset.Bind

Goal state before:
pp: α : Type u_1
β : Type v
s : Multiset α
t : Multiset β
l₁ : List α
l₂ : List β
d₁ : Nodup ⟦l₁⟧
d₂ : Nodup ⟦l₂⟧
⊢ (⟦l₁⟧ ×ˢ ⟦l₂⟧).Nodup

Tactic:
simp [List.Nodup.product d₁ d₂]

Goal state after:
Module: Mathlib.Algebra.Group.Pointwise.Set.Finite

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝³ : Monoid α
s t : Set α
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidablePred fun x ↦ x ∈ s
n : ℕ
⊢ DecidablePred fun x ↦ x ∈ s ^ n

Tactic:
by
  induction n with
  | zero =>
    simp only [pow_zero, mem_one]
    infer_instance
  | succ n ih =>
    rw [pow_succ]
    infer_instance

Goal state after:
Module: Mathlib.Algebra.Group.Action.Hom

Goal state before:
pp: M✝ : Type u_1
N : Type u_2
α : Type u_3
inst✝⁵ : Monoid M✝
inst✝⁴ : MulAction M✝ α
R : Type u_4
S : Type u_5
M : Type u_6
inst✝³ : Monoid R
inst✝² : MulAction R M
inst✝¹ : Monoid S
inst✝ : SMul S M
f : R →* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
b : M
⊢ 1 • b = b

Tactic:
rw [← f.map_one, hsmul, one_smul]

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Basic

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Subsemigroup M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
rw [← closure_singleton_le_iff_mem, le_iSup_iff]
  simp only [closure_singleton_le_iff_mem]

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
ι : Sort u_9
κ : Sort u_10
f : ι → Set α
g : κ → Set α
⊢ ⋂ i, f i ∪ ⋂ j, g j = ⋂ i, ⋂ j, f i ∪ g j

Tactic:
union_iInter

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
ι₁ : Sort u_9
κ₁ : Sort u_10
ι₂ : ι₁ → Sort u_11
k₂ : κ₁ → Sort u_12
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ ⋂ i, ⋂ i_1, f i i_1 ∪ ⋂ j₁, ⋂ j₂, g j₁ j₂ = ⋂ i₁, ⋂ i₂, ⋂ j₁, ⋂ j₂, f i₁ i₂ ∪ g j₁ j₂

Tactic:
union_iInter

Goal state after:
Module: Mathlib.Data.Set.Lattice.Image

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set (α → β)
t : Set α
⊢ s.seq t = ⋃ f ∈ s, f '' t

Tactic:
by
  rw [seq_eq_image2, iUnion_image_left]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.Basic

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
p : ι → Submonoid M
m : M
⊢ m ∈ ⨆ i, p i ↔ ∀ (N : Submonoid M), (∀ (i : ι), p i ≤ N) → m ∈ N

Tactic:
rw [← closure_singleton_le_iff_mem, le_iSup_iff]
  simp only [closure_singleton_le_iff_mem]

Goal state after:
Module: Mathlib.Data.Nat.Bits

Goal state before:
pp: case bit
b✝ : Bool
n✝ : ℕ
h : n✝ = 0 → b✝ = true
a✝ : n✝.div2.bits = n✝.bits.tail
⊢ (bit b✝ n✝).div2.bits = (bit b✝ n✝).bits.tail

Tactic:
simp [div2_bit, bits_append_bit _ _ h]

Goal state after:
Module: Mathlib.Logic.Encodable.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Encodable α
inst✝ : Encodable β
s : α ⊕ β
⊢ decodeSum (encodeSum s) = some s

Tactic:
cases s <;> simp [encodeSum, div2_val, decodeSum, encodek]

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Group α
inst✝ : MulAction α β
s : Set β
⊢ ⋃ g, g • s = {a | ∃ g, g • a ∈ s}

Tactic:
simp_rw [← iUnion_ofPred, ← iUnion_inv_smul, ← preimage_smul, preimage]

Goal state after:
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : Preorder M
inst✝¹ : MulRightMono M
inst✝ : MulLeftMono M
l₁ l₂ : List M
h : l₁ <+ l₂
h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a
⊢ l₁.prod ≤ l₂.prod

Tactic:
by
  induction h with
  | slnil => rfl
  | cons a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
  | cons_cons a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    grw [ih' h₁.2]

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y * x⁻¹ * y⁻¹ = 1
⊢ x * y = y * x

Tactic:
rw [mul_assoc, mul_eq_one_iff_eq_inv] at this

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y = (x⁻¹ * y⁻¹)⁻¹
⊢ x * y = y * x
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : normalClosure {⟨g, hg⟩} = ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h : ∀ (x : ↥N), (MulAut.conj c) ↑x ∈ N
x : G
hx : x ∈ N
⊢ x * c * c⁻¹ = x

Tactic:
rw [mul_assoc, mul_inv_cancel, mul_one]

Goal state after:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case right.right
ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a✝ b✝ : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
i✝ : ι
a b : α i✝
hab : s i✝ a b
c : α i✝
hc : s i✝ b c
⊢ Lex r s ⟨i✝, a⟩ ⟨i✝, c⟩

Tactic:
· exact Lex.right _ _ (_root_.trans hab hc)

Goal state after:
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (List.map ofList l.sublists).zip (List.map ofList l.sublists.reverse)
⊢ x.1 + x.2 = ↑l

Tactic:
zip_map,

Goal state after:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ List.map (Prod.map ofList ofList) (l.sublists.zip l.sublists.reverse)
⊢ x.1 + x.2 = ↑l
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ (List.map ofList l.sublists').zip (List.map ofList l.sublists'.reverse)
⊢ x.1 + x.2 = ↑l

Tactic:
zip_map,

Goal state after:
α : Type u_1
l : List α
x : Multiset α × Multiset α
h : x ∈ List.map (Prod.map ofList ofList) (l.sublists'.zip l.sublists'.reverse)
⊢ x.1 + x.2 = ↑l
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
n : ℕ
a : α
l : List α
⊢ l.length.choose (n + 1) + l.length.choose n = (a :: l).length.choose (n + 1)

Tactic:
length_cons,

Goal state after:
α : Type u
n : ℕ
a : α
l : List α
⊢ l.length.choose (n + 1) + l.length.choose n = (l.length + 1).choose (n + 1)
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.revzip
⊢ l₁ ++ l₂ ~ l

Tactic:
rw [revzip] at h

Goal state after:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists.zip l.sublists.reverse
⊢ l₁ ++ l₂ ~ l
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.revzip
⊢ l₁ ++ l₂ ~ l

Tactic:
rw [revzip] at h

Goal state after:
α : Type u
l l₁ l₂ : List α
h : (l₁, l₂) ∈ l.sublists'.zip l.sublists'.reverse
⊢ l₁ ++ l₂ ~ l
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
⊢ s₁.sup f = s₂.sup g

Tactic:
by
  subst hs
  exact Finset.fold_congr hfg

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.inf fun b ↦ f b \ a) = s.inf f \ a

Tactic:
by
  induction hs using Finset.Nonempty.cons_induction with
  | singleton => rw [inf_singleton, inf_singleton]
  | cons _ _ _ _ ih => rw [inf_cons, inf_cons, ih, inf_sdiff]

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : DecidableEq β
s : Finset γ
f : γ → β
hs : (image f s).Nonempty
g : β → α
⊢ (image f s).sup' hs g = s.sup' ⋯ (g ∘ f)

Tactic:
by
  rw [← WithBot.coe_eq_coe]; simp only [coe_sup', sup_image]; rfl

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
s : Set (Set α)
hs : s.Finite
H : ∀ t ∈ s, t.Finite
⊢ (⋃₀ s).Finite

Tactic:
by
  simpa only [sUnion_eq_biUnion] using hs.biUnion H

Goal state after:
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
s : Set α
hs : s.Finite
ι : Type u_1
t : ι → Set α
h : s ⊆ ⋃ i, t i
⊢ ∃ I, I.Finite ∧ s ⊆ ⋃ i ∈ I, t i

Tactic:
by
  have := hs.to_subtype
  choose f hf using show ∀ x : s, ∃ i, x.1 ∈ t i by simpa [subset_def] using h
  refine ⟨range f, finite_range f, fun x hx => ?_⟩
  rw [biUnion_range, mem_iUnion]
  exact ⟨⟨x, hx⟩, hf _⟩

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
⊢ BddAbove (range fun b ↦ ⨆ c, f (b, c))

Tactic:
bddAbove_def

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : ∃ x, ∀ y ∈ range f, y ≤ x
h✝¹ : Nonempty β
h✝ : Nonempty γ
⊢ ∃ x, ∀ y ∈ range fun b ↦ ⨆ c, f (b, c), y ≤ x
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : BddAbove (range f)
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
b : β
⊢ BddAbove (range fun c ↦ f (b, c))

Tactic:
bddAbove_def

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : ConditionallyCompleteLattice α
f : β × γ → α
hf : ∃ x, ∀ y ∈ range f, y ≤ x
h✝¹ : Nonempty β
h✝ : Nonempty γ
h₁ : BddAbove (range fun b ↦ ⨆ c, f (b, c))
b : β
⊢ ∃ x, ∀ y ∈ range fun c ↦ f (b, c), y ≤ x
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
l : List ι
f : ι → α
h : ∃ x ∈ l, sSup ∅ ≤ f x
⊢ ⨆ x ∈ l, f x ∈ map f l

Tactic:
simpa using l.toFinset.ciSup_mem_image f (by simpa using h)

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
inst✝ : ConditionallyCompleteLattice α
ι : Type u_5
ι' : Type u_6
s : Set ι
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i ↦ g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hs : s.Nonempty
hg : BddAbove (range fun i ↦ g ↑i)
this✝ : Nonempty ↑s
i : ι
h : i ∈ s
this : f i ∈ f '' s
⊢ ∃ t, g ↑t = g (f ↑⟨i, h⟩)

Tactic:
exact ⟨⟨f i, this⟩, by simp⟩

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: case mpr
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
n : α
this : OrderBot α
⊢ ((∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i) → ⨅ i, f i = n

Tactic:
rintro ⟨⟨i, rfl⟩, h⟩

Goal state after:
case mpr
α : Type u_1
ι : Sort u_4
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : Nonempty ι
f : ι → α
this : OrderBot α
i : ι
h : ∀ (i_1 : ι), f i ≤ f i_1
⊢ ⨅ i, f i = f i
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
h : Set.range ⇑f = Set.range ⇑g
ef : ↑Set.univ ≃o ↑(⇑f '' Set.univ) := StrictMonoOn.orderIso (⇑f) Set.univ ⋯
eg : ↑Set.univ ≃o ↑(⇑g '' Set.univ) := StrictMonoOn.orderIso (⇑g) Set.univ ⋯
⊢ ⇑f '' Set.univ = ⇑g '' Set.univ

Tactic:
by simpa using! h

Goal state after:
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ {x ∈ Finset.Ico a b | x < c}.val = (Finset.Ico a (min b c)).val

Tactic:
Finset.Ico_filter_lt

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ (Finset.Ico a (min b c)).val = (Finset.Ico a (min b c)).val
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀ h₁ : LocallyFiniteOrderTop α
⊢ h₀ = h₁

Tactic:
obtain ⟨h₀_finset_Ioi, h₀_finset_Ici, h₀_finset_mem_Ici, h₀_finset_mem_Ioi⟩ := h₀
    obtain ⟨h₁_finset_Ioi, h₁_finset_Ici, h₁_finset_mem_Ici, h₁_finset_mem_Ioi⟩ := h₁
    have hIci : h₀_finset_Ici = h₁_finset_Ici := by
      ext a b
      rw [h₀_finset_mem_Ici, h₁_finset_mem_Ici]
    have hIoi : h₀_finset_Ioi = h₁_finset_Ioi := by
      ext a b
      rw [h₀_finset_mem_Ioi, h₁_finset_mem_Ioi]
    simp_rw [hIci, hIoi]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case succ.inr.inr
a n : ℕ
ih : Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))
k l : ℕ
hkl : k % a = l % a
ha : 0 < a
hkn : k ≠ n
hk : k ∈ Ico n (n + a)
hln : l ≠ n
hl : l ∈ Ico n (n + a)
⊢ k = l

Tactic:
· refine ih ?_ ?_ hkl <;> simp only [Finset.mem_coe, hk, hl]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a ≤ x ∧ x ≤ ↑b
⊢ p x

Tactic:
exact hp hx.1 hx.2 a.prop b.prop

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a ≤ b
⊢ Icc a b = cons b (Ico a b) ⋯

Tactic:
by
  classical rw [cons_eq_insert, Ico_insert_right h]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b : α
⊢ insert b (Iio b) = Iic b

Tactic:
by
  ext
  simp_rw [Finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ ∈ [[a₂, b₂]]
h₂ : b₁ ∈ [[a₂, b₂]]
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]

Tactic:
rw [mem_uIcc] at h₁ h₂

Goal state after:
α : Type u_2
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₂ ⊓ b₂ ≤ a₁ ∧ a₁ ≤ a₂ ⊔ b₂
h₂ : a₂ ⊓ b₂ ≤ b₁ ∧ b₁ ≤ a₂ ⊔ b₂
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M✝ : Type u_1
inst✝² : MulOneClass M✝
M : Type u_2
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
c : ↥(center M)
r : M
v : α
⊢ c • r • v = r • c • v

Tactic:
by
    have := Semigroup.mem_center_iff.1 c.2
    simp_rw [Submonoid.smul_def, smul_smul, this]

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case comm
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
a✝ : N
⊢ e.symm (e x * a✝) = e.symm (a✝ * e x)

Tactic:
simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm]

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case left_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
b✝ c✝ : N
⊢ e.symm (e x * (b✝ * c✝)) = e.symm (e x * b✝ * c✝)

Tactic:
simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm]

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: case right_assoc
M : Type u_3
N : Type u_1
F : Type u_2
inst✝³ : EquivLike F M N
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : MulEquivClass F M N
e✝ : F
x : M
hx : x ∈ Set.center M
e : M ≃* N := ⋯
a✝ b✝ : N
⊢ e.symm (a✝ * b✝ * e x) = e.symm (a✝ * (b✝ * e x))

Tactic:
simp only
    [map_mul, e.symm_apply_apply, (hx.comm _).eq, (isMulCentral_iff _).mp hx, ← hx.right_comm]

Goal state after:
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
S : Set M
inst✝ : Group M
a b : M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
⊢ a / b ∈ S.centralizer

Tactic:
by
  simpa only [div_eq_mul_inv] using mul_mem_centralizer ha (inv_mem_centralizer hb)

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
N H : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ ↑(N ⊔ H) = ↑H * ↑N

Tactic:
sup_comm,

Goal state after:
G : Type u_2
inst✝ : Group G
N H : Subgroup G
hLE : H ≤ normalizer ↑N
⊢ ↑(H ⊔ N) = ↑H * ↑N
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
inst✝¹ : Monoid α
inst✝ : DecidableEq α
s : Multiset α
a : α
h : a ∈ s
comm : {x | x ∈ s}.Pairwise Commute
comm' : ∀ x ∈ {x | x ∈ s.erase a}, ∀ x_1 ∈ {x | x ∈ s.erase a}, x ≠ x_1 → Commute x x_1
this : ∀ b ∈ s.erase a, Commute a b
⊢ (s.erase a).noncommProd comm' * a = s.noncommProd comm

Tactic:
rw [← (noncommProd_commute (s.erase a) comm' a this).eq, mul_noncommProd_erase s h comm comm']

Goal state after:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
l : List α
f : α → β
comm : (↑l.toFinset).Pairwise (Commute on f)
hl : l.dedup = l
⊢ l.toFinset.noncommProd f comm = (List.map f l).prod

Tactic:
simp [noncommProd, hl]

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: case mem
M : Type u_1
inst✝ : CommMonoid M
x✝ : M
s : Set M
x : M
hx : x ∈ s
⊢ ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x

Tactic:
exact ⟨Pi.single x 1, {x}, by simp [hx, Pi.single_apply]⟩

Goal state after:
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
⊢ ⇑(r.map f) ≤ Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2

Tactic:
rintro _ _ hxy

Goal state after:
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
i✝¹ i✝ : β
hxy : (r.map f) i✝¹ i✝
⊢ (Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) i✝¹ i✝
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
x✝¹ L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Step (x✝¹ ++ (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝)) (x✝¹ ++ (L₁✝ ++ L₂✝))

Tactic:
by rw [← List.append_assoc, ← List.append_assoc]; constructor

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
F : Type ?u.18
inst✝⁴ : Mul M
inst✝³ : Mul N
inst✝² : Mul P
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
d : Con c.Quotient
x y : M
h : c x y
⊢ d ↑x ↑y

Tactic:
rw [c.eq.2 h]; exact d.refl _

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
a : ι
h : a ∈ {a ∈ s | p a}
⊢ f a = if p a then f a else 1

Tactic:
by rw [if_pos]; simpa using (mem_filter.1 h).2

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L : List (α × Bool)
n✝ n : ℕ
⊢ mk L ^ (n + 1) = mk (List.replicate (n + 1) L).flatten

Tactic:
by rw [pow_succ', pow_mk, mul_mk, List.replicate_succ, List.flatten_cons]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f (of x)⁻¹ = f (of x)⁻¹ * (g (of x) * g (of x)⁻¹)

Tactic:
← _root_.map_mul,

Goal state after:
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f (of x)⁻¹ = f (of x)⁻¹ * g (of x * (of x)⁻¹)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f (of x)⁻¹ * f (of x) * g (of x)⁻¹ = g (of x)⁻¹

Tactic:
← _root_.map_mul,

Goal state after:
α : Type u
M : Type u_1
inst✝ : Monoid M
f g : FreeGroup α →* M
h : ∀ (a : α), f (of a) = g (of a)
x✝ : FreeGroup α
x : α
⊢ f ((of x)⁻¹ * of x) * g (of x)⁻¹ = g (of x)⁻¹
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ ↑s
⊢ (lift f).range ≤ s

Tactic:
rintro _ ⟨⟨L⟩, rfl⟩

Goal state after:
case mk
α : Type u
β : Type v
inst✝ : Group β
f : α → β
s : Subgroup β
H : Set.range f ⊆ ↑s
w✝ : FreeGroup α
L : List (α × Bool)
⊢ (lift f) (Quot.mk Red.Step L) ∈ s
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₂ \ s₁ ∪ s₂ ∩ s₁, g a

Tactic:
prod_union_eq_right (by simp_all),

Goal state after:
ι : Type u_5
M : Type u_6
s₁ s₂ : Finset ι
f g : ι → M
inst✝ : CommMonoid M
h₁ : ∀ a ∈ s₁, a ∉ s₂ → f a = 1
h₂ : ∀ a ∈ s₂, a ∉ s₁ → g a = 1
h : ∀ a ∈ s₁, a ∈ s₂ → f a = g a
| ∏ a ∈ s₂ ∩ s₁, g a
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ ⨆ i, map (MonoidHom.mulSingle M i) (closure ↑(s i)) = Submonoid.pi Set.univ P

Tactic:
hs,

Goal state after:
ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ ⨆ i, map (MonoidHom.mulSingle M i) (P i) = Submonoid.pi Set.univ P
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case h
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ closure ↑s ≤ MonoidHom.mrange e

Tactic:
hs,

Goal state after:
case h
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e P ≤ MonoidHom.mrange e
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case h
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Submonoid.map f (Submonoid.closure ↑s) = ⊤

Tactic:
hs,

Goal state after:
case h
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Submonoid.map f ⊤ = ⊤
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
⊢ FG M'

Tactic:
classical
    obtain ⟨s, hs⟩ := Monoid.fg_def.mp ‹_›
    use s.image f
    rwa [Finset.coe_image, ← MonoidHom.map_mclosure, hs, ← MonoidHom.mrange_eq_map,
      MonoidHom.mrange_eq_top]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
P : Subgroup G
⊢ P.FG ↔ (toAddSubgroup P).FG

Tactic:
by
  rw [Subgroup.fg_iff_submonoid_fg, AddSubgroup.fg_iff_addSubmonoid_fg]
  exact (Subgroup.toSubmonoid P).fg_iff_add_fg

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁴ : Group G
inst✝³ : Group H
N : Subgroup G
nN : N.Normal
I : Type u_5
inst✝² : Group I
M : Subgroup H
O : Subgroup I
inst✝¹ : M.Normal
inst✝ : O.Normal
f : G →* H
g : H →* I
hf : N ≤ Subgroup.comap f M
hg : M ≤ Subgroup.comap g O
hgf : N ≤ Subgroup.comap (g.comp f) O
x✝ : G ⧸ N
x : G
⊢ (map M O g hg) ((map N M f hf) ↑x) = (map N O (g.comp f) hgf) ↑x

Tactic:
simp only [map_mk, MonoidHom.comp_apply]

Goal state after: