mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
x : α
⊢ x ∈ orbitRel.Quotient.orbit (Quotient.mk'' x)

Tactic:
simp

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
g h : M
Hg : g ∈ Set.center M
u : Mˣ
hu : SemiconjBy (↑u) g h
⊢ g = h

Tactic:
rwa [← u.mul_left_inj, Hg.comm u]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ((fun x ↦ (ofLex x).1) '' s).IsPWO
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
⊢ (∀ (n : ℕ), f n ∈ s) → ∃ m n, m < n ∧ f m ≤ f n

Tactic:
hf

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ((fun x ↦ (ofLex x).1) '' s).IsPWO
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ m n, m < n ∧ f m ≤ f n
Module: Mathlib.Algebra.Group.Support

Goal state before:
pp: α : Type u_1
G : Type u_3
inst✝ : DivisionMonoid G
f g : α → G
⊢ 1 * 1⁻¹ = 1

Tactic:
simp

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ (fun x ↦ (ofLex x).1) '' s) → ∃ g, Monotone (f ∘ ⇑g)
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg : Monotone fun n ↦ (ofLex f (g n)).1
hhg : ∀ (n : ℕ), (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1
hc : ∀ (n : ℕ), ¬(ofLex f (g 0)).1 < (ofLex f (g n)).1
⊢ ∃ m n, m < n ∧ f m ≤ f n

Tactic:
have hhc : ∀ n, (ofLex f (g 0)).1 = (ofLex f (g n)).1 := by
      intro n
      exact (hhg n).eq_of_not_lt (hc n)
    obtain ⟨g', hg'⟩ : ∃ g' : ℕ ↪o ℕ, Monotone ((fun n ↦ (ofLex f (g (g' n))).2)) := by
      simp_rw [isPWO_iff_exists_monotone_subseq] at hβ
      apply hβ (ofLex f (g 0)).1 fun n ↦ (ofLex f (g n)).2
      intro n
      rw [hhc n]
      simpa using! hf _
    use (g (g' 0)), (g (g' 1))
    suffices (f (g (g' 0))) ≤ (f (g (g' 1))) by simpa
    · refine Prod.Lex.toLex_le_toLex.mpr <| .inr ⟨?_, ?_⟩
      · exact (hhc (g' 0)).symm.trans (hhc (g' 1))
      · exact hg' (Nat.zero_le 1)

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
hH : H.Characteristic
⊢ (centralizer ↑H).Characteristic

Tactic:
refine Subgroup.characteristic_iff_comap_le.mpr fun ϕ g hg h hh => ϕ.injective ?_

Goal state after:
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H K : Subgroup G
hH : H.Characteristic
ϕ : G ≃* G
g : G
hg : g ∈ comap ϕ.toMonoidHom (centralizer ↑H)
h : G
hh : h ∈ ↑H
⊢ ϕ (h * g) = ϕ (g * h)
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h
α : Type u_3
β : Type u_4
f : α → β → β
a : α
b : β
a✝ : List α
h : {x | x ∈ a ::ₘ ⟦a✝⟧}.Pairwise fun x y ↦ ∀ (b : β), f x (f y b) = f y (f x b)
h' : {x | x ∈ ⟦a✝⟧}.Pairwise fun x y ↦ ∀ (b : β), f x (f y b) = f y (f x b)
⊢ noncommFoldr f (a ::ₘ ⟦a✝⟧) h b = f a (noncommFoldr f ⟦a✝⟧ h' b)

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u_3
β : Type u_4
f : α → β → β
h : LeftCommutative f
b : β
a✝ : List α
⊢ noncommFoldr f ⟦a✝⟧ ⋯ b = foldr f b ⟦a✝⟧

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u_3
op : α → α → α
assoc : Std.Associative op
a x : α
a✝ : List α
h : {x | x ∈ a ::ₘ ⟦a✝⟧}.Pairwise fun x y ↦ op x y = op y x
h' : {x | x ∈ ⟦a✝⟧}.Pairwise fun x y ↦ op x y = op y x
⊢ noncommFold op (a ::ₘ ⟦a✝⟧) h x = op a (noncommFold op ⟦a✝⟧ h' x)

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u_3
op : α → α → α
assoc : Std.Associative op
inst✝ : Std.Commutative op
a : α
a✝ : List α
⊢ noncommFold op ⟦a✝⟧ ⋯ a = fold op a ⟦a✝⟧

Tactic:
simp

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

Goal state before:
pp: case nil
α : Type u_3
inst✝ : Monoid α
comm : {x | x ∈ ↑[]}.Pairwise Commute
⊢ List.foldr (fun x1 x2 ↦ x1 * x2) 1 [] = [].prod

Tactic:
simp

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ s ^ 0 * ↑(closure s) = ↑(closure s)

Tactic:
simp

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ↑(closure s) * s ^ 0 = ↑(closure s)

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u_3
inst✝ : Monoid α
a : α
a✝ : List α
comm : {x | x ∈ a ::ₘ ⟦a✝⟧}.Pairwise Commute
⊢ (a ::ₘ ⟦a✝⟧).noncommProd comm = a * noncommProd ⟦a✝⟧ ⋯

Tactic:
simp

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

Goal state before:
pp: case h.nil
α : Type u_3
inst✝ : Monoid α
a : α
comm : {x | x ∈ a ::ₘ ⟦[]⟧}.Pairwise Commute
⊢ a * [].prod = [].prod * a

Tactic:
simp

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

Goal state before:
pp: case h.cons.e_a.a
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

Tactic:
simp

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

Goal state before:
pp: case h.cons.e_a.a
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ hd ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

Tactic:
simp

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
n : ℕ
⊢ closure (s ^ n) ≤ closure s

Tactic:
simp

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

Goal state before:
pp: case mk.mk
α : Type u_3
inst✝ : Monoid α
s t : Multiset α
a✝¹ a✝ : List α
comm : {x | x ∈ Quot.mk (⇑(List.isSetoid α)) a✝¹ + Quot.mk (⇑(List.isSetoid α)) a✝}.Pairwise Commute
⊢ (Quot.mk (⇑(List.isSetoid α)) a✝¹ + Quot.mk (⇑(List.isSetoid α)) a✝).noncommProd comm =
    noncommProd (Quot.mk (⇑(List.isSetoid α)) a✝¹) ⋯ * noncommProd (Quot.mk (⇑(List.isSetoid α)) a✝) ⋯

Tactic:
simp

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

Goal state before:
pp: case h
α : Type u_6
inst✝ : CommMonoid α
a✝ : List α
⊢ noncommProd ⟦a✝⟧ ⋯ = prod ⟦a✝⟧

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝ : CommMonoid M
s : Finset ι
e : ι ↪ κ
f : κ → M
⊢ (map e s).prod f = ∏ x ∈ s, f (e x)

Tactic:
simp

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

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ H ≤ MulAut.conj h • H

Tactic:
· rw [subset_pointwise_smul_iff, ← map_inv]
    exact conj_smul_le_of_le (le_refl H) ⟨h⁻¹, H.inv_mem hh⟩

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_3
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid M
e : ι → κ
he : Bijective e
f : ι → M
g : κ → M
h : ∀ (x : ι), f x = g (e x)
⊢ ∀ (i : ι), i ∈ univ ↔ (Equiv.ofBijective e he) i ∈ univ

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : Fintype ι
f : ↥univ → M
⊢ ∀ (x : Subtype (Membership.mem univ)), f x = f ⟨(Equiv.subtypeUnivEquiv ⋯) x, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
l : List (Multiset α)
⊢ Disjoint (sum ⟦l⟧) a ↔ ∀ b ∈ ⟦l⟧, Disjoint b a

Tactic:
rw [quot_mk_to_coe, Multiset.sum_coe]

Goal state after:
α : Type u_6
a : Multiset α
i : Multiset (Multiset α)
l : List (Multiset α)
⊢ Disjoint l.sum a ↔ ∀ b ∈ ↑l, Disjoint b a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: case e'_2
ι : Type u_1
α : Type u_6
i : Finset ι
f : ι → Multiset α
a : Multiset α
⊢ (∀ b ∈ i, Disjoint (f b) a) ↔ ∀ b ∈ map f i.val, Disjoint b a

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_3
β : Type u_6
inst✝ : CommMonoid β
f : α → β
⊢ ∅.noncommProd f ⋯ = ∅.prod f

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List M
hl : ∀ x ∈ l, x ∈ S
⊢ l.prod ∈ S

Tactic:
by
  lift l to List S using hl
  rw [← coe_list_prod]
  exact l.prod.coe_prop

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
S : Submonoid M
m : Multiset M
comm : {x | x ∈ m}.Pairwise Commute
h : ∀ x ∈ m, x ∈ S
⊢ m.noncommProd comm ∈ S

Tactic:
induction m using Quotient.inductionOn with | h l => ?_
  simp only [Multiset.quot_mk_to_coe, Multiset.noncommProd_coe]
  exact Submonoid.list_prod_mem _ h

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
x : M
s : Set M
⊢ ↑∅ ⊆ s ∧ Function.support 0 ⊆ ↑∅ ∧ ∏ a ∈ ∅, a ^ 0 a = 1

Tactic:
simp

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

Goal state before:
pp: case empty
α : Type u_3
β : Type u_4
inst✝ : Monoid β
f g : α → β
comm_ff : (↑∅).Pairwise (Commute on f)
comm_gg : (↑∅).Pairwise (Commute on g)
comm_gf : (↑∅).Pairwise fun x y ↦ Commute (g x) (f y)
⊢ ∅.noncommProd (f * g) ⋯ = ∅.noncommProd f comm_ff * ∅.noncommProd g comm_gg

Tactic:
simp

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

Goal state before:
pp: case convert_3
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ι → M i

Tactic:
intro j

Goal state after:
case convert_3
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
⊢ M i
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i : ι
⊢ ∀ x_1 ∈ insert i (univ.erase i),
    (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M x_1) (x x_1)) = Pi.mulSingle x_1 (x x_1) i

Tactic:
intro j

Goal state after:
case convert_4
ι : Type u_2
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
x : (i : ι) → M i
i j : ι
⊢ j ∈ insert i (univ.erase i) → (Pi.evalMonoidHom M i) ((MonoidHom.mulSingle M j) (x j)) = Pi.mulSingle j (x j) i
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
q : (i : ι) → Quotient (r i)
i : ι
⊢ (fun q ↦ q.liftOn' (fun x i ↦ Quotient.mk'' (x i)) ⋯) ((fun x ↦ Quotient.mk'' fun i ↦ (x i).out) q) i = q i

Tactic:
simp

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

Goal state before:
pp: case h
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Sort u_4
α : ι → Sort u_5
r : (i : ι) → Setoid (α i)
a✝ : (i : ι) → α i
i : ι
⊢ Quotient.mk'' ((fun i ↦ (Quotient.mk'' (a✝ i)).out) i) = Quotient.mk'' (a✝ i)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
a b : α
⊢ Relation.EqvGen r a b ↔ ⊤ ≤ Relation.EqvGen r a b

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x y : M
⊢ sSup (DFunLike.coe '' S) x y ↔ ∃ c ∈ S, c x y

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
⊢ Step ([] ++ L₁) ([] ++ L₂) ↔ Step L₁ L₂

Tactic:
simp

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

Goal state before:
pp: α : Type u
x✝² : List (α × Bool)
x✝¹ : α
x✝ : Bool
fst_eq✝ : x✝¹ = x✝¹
snd_eq✝ : (!x✝) = !x✝
⊢ [] ++ x✝² = [] ++ x✝² ∨ ∃ L₅, Step ([] ++ x✝²) L₅ ∧ Step ([] ++ x✝²) L₅

Tactic:
simp

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

Goal state before:
pp: α : Type u
x✝² : List (α × Bool)
x✝¹ : Bool
x✝ : α
⊢ [] ++ (x✝, !!x✝¹) :: x✝² = [(x✝, x✝¹)] ++ x✝² ∨
    ∃ L₅, Step ([] ++ (x✝, !!x✝¹) :: x✝²) L₅ ∧ Step ([(x✝, x✝¹)] ++ x✝²) L₅

Tactic:
simp

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

Goal state before:
pp: α : Type u
x✝² : List (α × Bool)
x✝¹ : α
x✝ : Bool
⊢ [(x✝¹, x✝)] ++ x✝² = [] ++ (x✝¹, !!x✝) :: x✝² ∨
    ∃ L₅, Step ([(x✝¹, x✝)] ++ x✝²) L₅ ∧ Step ([] ++ (x✝¹, !!x✝) :: x✝²) L₅

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
a : ι
f : ι → M
⊢ {a}.prod f = f a

Tactic:
simp

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

Goal state before:
pp: α : Type u
L L₁₂ L₁ e : List (α × Bool)
a : α
b : Bool
s' : List (α × Bool)
hLL' : ReflTransGen Step L (L₁ ++ s' ++ (a, b) :: (a, !b) :: e)
ih :
  ∀ {L₁_1 L₂ : List (α × Bool)},
    L₁_1 ++ L₂ = L₁ ++ s' ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁_1 ∧ Red L₄ L₂
eq : L₁ ++ (s' ++ e) = L₁ ++ s' ++ e
⊢ L₁ ++ (s' ++ (a, b) :: (a, !b) :: e) = L₁ ++ s' ++ (a, b) :: (a, !b) :: e

Tactic:
simp

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

Goal state before:
pp: α : Type u
L L₁₂ L₂ s : List (α × Bool)
a : α
b : Bool
e' : List (α × Bool)
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: (e' ++ L₂))
ih :
  ∀ {L₁ L₂_1 : List (α × Bool)},
    L₁ ++ L₂_1 = s ++ (a, b) :: (a, !b) :: (e' ++ L₂) → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂_1
eq : s ++ e' ++ L₂ = s ++ (e' ++ L₂)
⊢ s ++ (a, b) :: (a, !b) :: e' ++ L₂ = s ++ (a, b) :: (a, !b) :: (e' ++ L₂)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι → M
g : κ → M
⊢ ∏ x ∈ s.disjSum t, Sum.elim f g x = (∏ x ∈ s, f x) * ∏ x ∈ t, g x

Tactic:
simp

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

Goal state before:
pp: M : Type u_1
N : Type u_2
F : Type u_4
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
c : Con M
f : F
h : ker f ≤ c
hf : Surjective ⇑f
⊢ mapGen ⇑f = mapOfSurjective f h hf

Tactic:
rw [← conGen_of_con (c.mapOfSurjective f h hf)]; rfl

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

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

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
h : b * a⁻¹ ∈ s
⊢ (b * a⁻¹)⁻¹ = a⁻¹⁻¹ * b⁻¹

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
h : a⁻¹ * b ∈ s
⊢ (a⁻¹ * b)⁻¹ = b⁻¹ * a⁻¹⁻¹

Tactic:
simp

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

Goal state before:
pp: case mk.mk.mk
α : Type u
L L₁✝ L₂✝ L₃✝ L₄ : List (α × Bool)
a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
c✝ : FreeGroup α
L₃ : List (α × Bool)
⊢ Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂ * Quot.mk Red.Step L₃ =
    Quot.mk Red.Step L₁ * (Quot.mk Red.Step L₂ * Quot.mk Red.Step L₃)

Tactic:
simp

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

Goal state before:
pp: α : Type u_1
inst✝ : Group α
N : Subgroup α
⊢ {1} * ↑N = ↑N

Tactic:
simp

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

Goal state before:
pp: case not
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y : FreeGroup α
L₁✝ L₂✝ : List (α × Bool)
x✝ : α
b✝ : Bool
⊢ Red.Step (List.map (fun x ↦ (f x.1, x.2)) (L₁✝ ++ (x✝, b✝) :: (x✝, !b✝) :: L₂✝))
    (List.map (fun x ↦ (f x.1, x.2)) (L₁✝ ++ L₂✝))

Tactic:
simp

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

Goal state before:
pp: case mk.mk
α : Type u
L L₁✝ L₂✝ L₃ L₄ : List (α × Bool)
β : Type v
f : α → β
x y a✝ : FreeGroup α
L₁ : List (α × Bool)
b✝ : FreeGroup α
L₂ : List (α × Bool)
⊢ Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₁ * Quot.mk Red.Step L₂) =
    Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₁) *
      Quot.map (List.map fun x ↦ (f x.1, x.2)) ⋯ (Quot.mk Red.Step L₂)

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
a✝ : α
⊢ (map f) (of a✝) = (lift (of ∘ f)) (of a✝)

Tactic:
simp

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
x : FreeGroup α
⊢ ∀ (x : α), (prod.comp (map f)) (of x) = f x

Tactic:
simp

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x : ℤ
⊢ (fun x ↦ ((map fun x ↦ 1) x).sum) ((fun x ↦ of () ^ x) 0) = 0

Tactic:
simp

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

Goal state before:
pp: case C1
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
⊢ (fun x ↦ of default ^ x) ((fun x ↦ ((map 1) x).sum) 1) = 1

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
⊢ (fun x ↦ ((map 1) x).sum) ((fun x ↦ of default ^ x) 0) = 0

Tactic:
simp

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x✝ : FreeGroup α
⊢ (⇑equivIntOfUnique.symm ∘ ⇑Multiplicative.toAdd) ((⇑Multiplicative.ofAdd ∘ ⇑equivIntOfUnique) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x✝ : Multiplicative ℤ
⊢ (⇑Multiplicative.ofAdd ∘ ⇑equivIntOfUnique) ((⇑equivIntOfUnique.symm ∘ ⇑Multiplicative.toAdd) x✝) = x✝

Tactic:
simp

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

Goal state before:
pp: case C1
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
⊢ (fun x ↦ x • FreeAddGroup.of default) ((fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) 0) = 0

Tactic:
simp

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

Goal state before:
pp: case zero
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
⊢ (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) 0) = 0

Tactic:
simp

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

Goal state before:
pp: case succ
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
i✝ : ℕ
a✝ : (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) ↑i✝) = ↑i✝
⊢ (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) (↑i✝ + 1)) = ↑i✝ + 1

Tactic:
simp

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

Goal state before:
pp: case pred
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
i✝ : ℕ
a✝ : (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) (-↑i✝)) = -↑i✝
⊢ (fun x ↦ FreeAddGroup.sum ((FreeAddGroup.map 1) x)) ((fun x ↦ x • FreeAddGroup.of default) (-↑i✝ - 1)) = -↑i✝ - 1

Tactic:
simp

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
inst✝ : Unique α
x y : FreeAddGroup α
⊢ FreeAddGroup.sum ((FreeAddGroup.map 1) (x + y)) =
    FreeAddGroup.sum ((FreeAddGroup.map 1) x) + FreeAddGroup.sum ((FreeAddGroup.map 1) y)

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Set ι
inst✝ : DecidablePred fun x ↦ x ∈ s
f : ι → M
g : ↑s → M
w : ∀ (x : ι) (hx : x ∈ s), f x = g ⟨x, hx⟩
w' : ∀ x ∉ s, f x = 1
⊢ ∀ (x : ι), x ∈ s.toFinset ↔ x ∈ s

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ closure ↑∅ = ⊥

Tactic:
simp

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

Goal state before:
pp: case zero
M : Type u_4
inst✝ : CommMonoid M
u : ℕ → M
N : ℕ
hu : ∀ n ≥ N, u n = 1
⊢ ∏ k ∈ range (N + 0), u k = ∏ k ∈ range N, u k

Tactic:
simp

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

Goal state before:
pp: case zero
M : Type u_4
inst✝ : CommMonoid M
f : ℕ → M
n : ℕ
⊢ ∏ x ∈ range (n + 0), f x = (∏ x ∈ range n, f x) * ∏ x ∈ range 0, f (n + x)

Tactic:
simp

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x✝ : ↥N
⊢ ((mk' N).comp N.subtype) x✝ = 1 x✝

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case intro
M : Type u_1
inst✝¹ : Monoid M
inst✝ : Finite M
val✝ : Fintype M
⊢ FG M

Tactic:
exact ⟨⟨Finset.univ, by rw [Finset.coe_univ]; exact Submonoid.closure_univ⟩⟩

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
b : M
⊢ ∀ (n : ℕ), b ^ n = ∏ _k ∈ range n, b

Tactic:
simp

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → ℕ
a : M
⊢ ∏ i ∈ ∅, a ^ f i = a ^ ∑ i ∈ ∅, f i

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
⊢ closure ↑∅ = ⊥

Tactic:
simp

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

Goal state before:
pp: case H.inl
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ι → M
ih :
  ∀ t ⊂ ∅,
    ∀ (g : (a : ι) → a ∈ t → ι),
      (∀ (a : ι) (ha : a ∈ t), f a * f (g a ha) = 1) →
        (∀ (a : ι) (ha : a ∈ t), f a ≠ 1 → g a ha ≠ a) →
          ∀ (g_mem : ∀ (a : ι) (ha : a ∈ t), g a ha ∈ t), (∀ (a : ι) (ha : a ∈ t), g (g a ha) ⋯ = a) → ∏ x ∈ t, f x = 1
g : (a : ι) → a ∈ ∅ → ι
hg₁ : ∀ (a : ι) (ha : a ∈ ∅), f a * f (g a ha) = 1
hg₃ : ∀ (a : ι) (ha : a ∈ ∅), f a ≠ 1 → g a ha ≠ a
g_mem : ∀ (a : ι) (ha : a ∈ ∅), g a ha ∈ ∅
hg₄ : ∀ (a : ι) (ha : a ∈ ∅), g (g a ha) ⋯ = a
⊢ ∏ x ∈ ∅, f x = 1

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : Monoid M
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
⊢ AddSubmonoid.closure ↑{1} = ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : Monoid M
G : Type u_3
H : Type u_4
inst✝¹ : Group G
inst✝ : AddGroup H
⊢ AddSubgroup.closure ↑{1} = ⊤

Tactic:
simp

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

Goal state before:
pp: G : Type u
inst✝¹ : Group G
A : Type v
inst✝ : CommGroup A
f : G →* A
⊢ commutator G ≤ f.ker

Tactic:
rw [commutator_eq_closure, Subgroup.closure_le]
  rintro x ⟨p, q, rfl⟩
  simp [MonoidHom.mem_ker, mul_right_comm (f p) (f q), commutatorElement_def]

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

Goal state before:
pp: case mk
G : Type u
inst✝¹ : Group G
H : Type v
inst✝ : Group H
e : G ≃* H
x✝ : Abelianization G
a : G
⊢ (Abelianization.map e.symm.toMonoidHom)
      ((Abelianization.map e.toMonoidHom) (Quot.mk (⇑(QuotientGroup.leftRel (commutator G))) a)) =
    Quot.mk (⇑(QuotientGroup.leftRel (commutator G))) a

Tactic:
simp

Goal state after: