mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
x✝ : R
s : ↥⊥
⊢ ↑s * x✝ = x✝ * ↑s

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.10
inst✝ : CommMonoid R
S : Submonoid R
m n : R
s : ↥S
h : m * ↑s = n * ↑s
⊢ ↑s * m = ↑s * n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.OreSet

Goal state before:
pp: R✝ : Type u_1
inst✝² : Monoid R✝
S✝ : Submonoid R✝
inst✝¹ : OreSet S✝
R : Type ?u.10
inst✝ : CommMonoid R
S : Submonoid R
r : R
s : ↥S
⊢ ↑s * r = r * ↑s

Tactic:
by

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
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
t' : κ → Finset ι := fun k ↦ {i ∈ t k | f i ≠ 1}
this : s.biUnion t' = {i ∈ s.biUnion t | f i ≠ 1}
i : κ
hi : i ∈ ↑s
j : κ
hj : j ∈ ↑s
hij : i ≠ j
a : Finset ι
hai : a ⊆ t' i
haj : a ⊆ t' j
k : ι
hk : k ∈ a
hki : k ∈ t i ∧ ¬f k = 1
hkj : k ∈ t j ∧ ¬f k = 1
⊢ k ∈ t i ∩ t j

Tactic:
by

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
f : ι → M
inst✝ : DecidableEq ι
s : Finset κ
t : κ → Finset ι
hs : (↑s).Pairwise fun i j ↦ ∀ k ∈ t i ∩ t j, f k = 1
⊢ ∏ x ∈ s.biUnion t, f x = ∏ x ∈ s, ∏ i ∈ t x, f i

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
β : Type v
inst✝ : AddCommGroup β
f : α → β
x : α
⊢ (lift f) (of x) = f x

Tactic:
by

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
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
j : κ
hj : j ∈ {i ∈ I | f i = f n}.erase n
⊢ g (f j) = 1

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : AddCommGroup β
inst✝ : AddCommGroup γ
a : FreeAbelianGroup α
f : α → β
g : β →+ γ
⊢ (lift (⇑g ∘ f)) a = g ((lift f) a)

Tactic:
by

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
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
h : ∀ j ∈ {i ∈ I | f i = f n}.erase n, g (f j) = 1
⊢ f n = f n

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
⊢ Function.Injective of

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
x : α
h : of x = 0
f : FreeAbelianGroup α →+ ℤ := lift 1
hfx : f (of x) = 1
⊢ f (of x) = 0

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
x : α
⊢ of x ≠ 0

Tactic:
by

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
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
n : κ
I : Finset κ
hn : n ∈ I
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
⊢ ∏ j ∈ I with f j = f n, g (f j) = g (f n)

Tactic:
by

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
inst✝ : DecidableEq ι
f : κ → ι
g : ι → M
I : Finset κ
hf : (↑I).Pairwise fun i j ↦ f i = f j → g (f i) = 1
⊢ ∏ s ∈ image f I, g s = ∏ i ∈ I, g (f i)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
inst✝ : AddCommGroup G
f g : α → G
a : FreeAbelianGroup α
⊢ (lift (f + g)) a = (lift f) a + (lift g) a

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type u
f : FreeAbelianGroup (α → β)
⊢ FreeAbelianGroup α →+ FreeAbelianGroup β

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ : Type u
x✝ : FreeAbelianGroup α✝
x : α✝
ih : id <$> pure x = pure x
⊢ id <$> (-pure x) = -pure x

Tactic:
by

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
inst✝² : DecidableEq ι
inst✝¹ : PartialOrder ι
inst✝ : OrderBot ι
f : κ → ι
g : ι → M
hg_bot : g ⊥ = 1
I : Finset κ
hf_disj : (↑I).PairwiseDisjoint f
⊢ ∏ s ∈ image f I, g s = ∏ i ∈ I, g (f i)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ : Type u
x✝ x y : FreeAbelianGroup α✝
ihx : id <$> x = x
ihy : id <$> y = y
⊢ id <$> (x + y) = x + y

Tactic:
by

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✝ : Unique ι
s : Finset ι
f : ι → M
h : s.Nonempty
⊢ ∏ x ∈ s, f x = f default

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : ι → M
e : ι ≃ κ
⊢ (map e.toEmbedding s).prod (f ∘ ⇑e.symm) = s.prod f

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
s : Finset ι
inst✝ : CommMonoid M
f : κ → M
e : ι ≃ κ
⊢ s.prod (f ∘ ⇑e) = (map e.toEmbedding s).prod f

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
⊢ 0 >>= f >>= g = 0 >>= fun x ↦ f x >>= g

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
⊢ pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : CancelCommMonoid M
s t : Finset ι
f : ι → M
⊢ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i = (∏ i ∈ s \ t, f i) * ∏ i ∈ t, f i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
s : Finset ι
a : ι
inst✝¹ : CommGroup G
inst✝ : DecidableEq ι
ha : a ∉ s
f : ι → G
⊢ (∏ x ∈ insert a s, f x) / f a = ∏ x ∈ s, f x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
s : Finset ι
inst✝¹ : CommGroup G
inst✝ : DecidableEq ι
f : ι → G
a : ι
h : a ∈ s
⊢ ∏ x ∈ s.erase a, f x = (∏ x ∈ s, f x) / f a

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∏ i ∈ range n, f (i + 1) / f i = f n / f 0

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ ∏ i ∈ range n, f i / f (i + 1) = f 0 / f n

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f n = f 0 * ∏ i ∈ range n, f (i + 1) / f i

Tactic:
by

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
f : ℕ → G
n : ℕ
⊢ f n = ∏ i ∈ range (n + 1), if i = 0 then f 0 else f i / f (i - 1)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
s₁ s₂ : Finset ι
inst✝¹ : CommGroup G
inst✝ : DecidableEq ι
f : ι → G
h : s₁ ⊆ s₂
⊢ ∏ x ∈ s₂ \ s₁, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
s₁ s₂ : Finset ι
inst✝¹ : CommGroup G
inst✝ : DecidableEq ι
f : ι → G
⊢ (∏ x ∈ s₂ \ s₁, f x) / ∏ x ∈ s₁ \ s₂, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x : α✝
ih : pure x >>= f >>= g = pure x >>= fun x ↦ f x >>= g
⊢ -pure x >>= f >>= g = -pure x >>= fun x ↦ f x >>= g

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : Sub M
inst✝³ : OrderedSub M
inst✝² : AddLeftMono M
inst✝¹ : AddLeftReflectLE M
inst✝ : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n : ℕ
⊢ ∑ i ∈ range n, (f (i + 1) - f i) = f n - f 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
⊢ #s = ∑ x ∈ s, 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Finset ι
m : ℕ
f : ι → ℕ
h₁ : ∀ x ∈ s, f x = m
⊢ ∑ x ∈ s, f x = #s * m

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
κ : Type u_5
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
⊢ ∑ j ∈ t, #({i ∈ s | g i = j}) = #({i ∈ s | g i ∈ t})

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝ : DecidableEq M
t : ι → Finset M
h : (↑s).PairwiseDisjoint t
⊢ #(s.biUnion t) = ∑ u ∈ s, #(t u)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : DecidableEq M
s : Finset ι
t : ι → Finset M
this : DecidableEq ι
⊢ #(∅.biUnion t) ≤ ∑ a ∈ ∅, #(t a)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : DecidableEq M
s✝ : Finset ι
t : ι → Finset M
this : DecidableEq ι
a : ι
s : Finset ι
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #((insert a s).biUnion t) ≤ #(t a) + #(s.biUnion t)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : DecidableEq M
s✝ : Finset ι
t : ι → Finset M
this : DecidableEq ι
a : ι
s : Finset ι
has : a ∉ s
ih : #(s.biUnion t) ≤ ∑ a ∈ s, #(t a)
⊢ #(t a) + #(s.biUnion t) ≤ ∑ a ∈ insert a s, #(t a)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : DecidableEq M
f : ι → M
s : Finset ι
t : Finset M
H : Set.MapsTo f ↑s ↑t
⊢ #s = ∑ b ∈ t, #({a ∈ s | f a = b})

Tactic:
by

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

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid M
e : ι → κ
he : Injective e
f : ι → M
g : κ → M
h' : ∀ i ∉ Set.range e, g i = 1
h : ∀ (i : ι), f i = g (e i)
⊢ Set.MapsTo e ↑univ ↑univ

Tactic:
by

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

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : Fintype κ
inst✝ : CommMonoid M
e : ι → κ
he : Injective e
f : ι → M
g : κ → M
h' : ∀ i ∉ Set.range e, g i = 1
h : ∀ (i : ι), f i = g (e i)
⊢ ∀ i ∈ univ, i ∉ e '' ↑univ → g i = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ (MulAut.conj g₁) g₂ = ⁅g₁, g₂⁆ * g₂

Tactic:
by

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

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : ι → M
j : κ
⊢ ∀ (x : ι), x ∈ {i | g i = j} ↔ g x = j

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁

Tactic:
by

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

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : ι → M
⊢ ∏ j, ∏ i, f ↑i = ∏ i, f i

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ x + y >>= f >>= g = x + y >>= fun x ↦ f x >>= g

Tactic:
by

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ : G
⊢ f ⁅g₁, g₂⁆ = ⁅f g₁, f g₂⁆

Tactic:
by

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

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : κ → M
j : κ
⊢ ∀ (x : ι), x ∈ {i | g i = j} ↔ g x = j

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g₁ g₂ g₃ : G
⊢ g₃ * ⁅g₁, g₂⁆ * g₃⁻¹ = ⁅g₃ * g₁ * g₃⁻¹, g₃ * g₂ * g₃⁻¹⁆

Tactic:
by

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

Goal state before:
pp: M : Type u_4
κ : Type u_6
ι : Type u_7
inst✝³ : Fintype ι
inst✝² : Fintype κ
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
g : ι → κ
f : κ → M
⊢ ∏ j, ∏ _i, f j = ∏ i, f (g i)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ ⁅a * b, c⁆ = a * ⁅b, c⁆ * a⁻¹ * ⁅a, c⁆

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ ⁅a, b * c⁆ = ⁅a, b⁆ * b * ⁅a, c⁆ * b⁻¹

Tactic:
by

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

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
inst✝ : Unique ι
f : ι → M
⊢ ∏ x, f x = f default

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ ⁅a⁻¹, b⁆ = a⁻¹ * ⁅b, a⁆ * a

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b : G
⊢ ⁅a, b⁻¹⁆ = b⁻¹ * ⁅b, a⁆ * b

Tactic:
by

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

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
inst✝ : Subsingleton ι
f : ι → M
a : ι
⊢ ∏ x, f x = f a

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
f : Prop → M
⊢ ∏ p, f p = f True * f False

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ a * ⁅⁅a⁻¹, b⁆, c⁆ * a⁻¹ * c * ⁅⁅c⁻¹, a⁆, b⁆ * c⁻¹ * b * ⁅⁅b⁻¹, c⁆, a⁆ * b⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ b * ⁅a, ⁅b⁻¹, c⁆⁆ * b⁻¹ * c * ⁅b, ⁅c⁻¹, a⁆⁆ * c⁻¹ * a * ⁅c, ⁅a⁻¹, b⁆⁆ * a⁻¹ = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ ⁅⁅a, b⁆, b * c * b⁻¹⁆ * ⁅⁅b, c⁆, c * a * c⁻¹⁆ * ⁅⁅c, a⁆, a * b * a⁻¹⁆ = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ ⁅a * b * a⁻¹, ⁅c, a⁆⁆ * ⁅c * a * c⁻¹, ⁅b, c⁆⁆ * ⁅b * c * b⁻¹, ⁅a, b⁆⁆ = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ ⁅a * b, c⁆ * ⁅c * a, b⁆ * ⁅b * c, a⁆ = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a b c : G
⊢ ⁅a, b * c⁆ * ⁅b, c * a⁆ * ⁅c, a * b⁆ = 1

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer ↑H₂

Tactic:
by

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

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
⊢ (∏ i, f ↑i) * ∏ i, f ↑i = ∏ i, f i

Tactic:
by

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

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝¹ : Fintype ι
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
h : ∀ (i : ι), f i ≠ 1 → i ∈ s
⊢ ∀ x ∈ univ, x ∉ s → f x = 1

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : CommMonoid M
f : ι → M
x✝ : [].Nodup
⊢ [].toFinset.prod f = (map f []).prod

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_5
inst✝¹ : DecidableEq ι
inst✝ : CommMonoid M
f : ι → M
a : ι
l : List ι
hl : (a :: l).Nodup
⊢ (a :: l).toFinset.prod f = (map f (a :: l)).prod

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
l : List ι
⊢ ∑ a ∈ l.toFinset, count a l = l.length

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
a : M
s : Finset ι
m : ι → Multiset M
⊢ a ∈ ∑ i ∈ s, m i ↔ ∃ i ∈ s, a ∈ m i

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
α : Type u_5
inst✝ : CommMonoid M
m : Multiset ι
s : Finset α
f : ι → α → M
⊢ (map (fun i ↦ ∏ a ∈ s, f i a) m).prod = ∏ a ∈ s, (map (fun i ↦ f i a) m).prod

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
⊢ ∑ a ∈ s.toFinset, count a s = s.card

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ : Type u
x : FreeAbelianGroup α✝
y : FreeAbelianGroup β✝
⊢ Prod.mk <$> x <*> y = (fun b a ↦ (a, b)) <$> y <*> x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
⊢ ∑ a ∈ s, count a m = m.card

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
⊢ ∑ a ∈ s.toFinset, count a s • {a} = s

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥
h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥
⊢ ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ (lift (g ∘ f)) x = (lift g) ((map f) x)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅H, H⁆ = ⊥ ↔ IsMulCommutative ↥H

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
x : FreeAbelianGroup α
⊢ (map id) x = x

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅H, ⊤⁆ = ⊥ ↔ H ≤ center G

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x✝ : α
⊢ ((map g).comp (map f)) (of x✝) = (map (g ∘ f)) (of x✝)

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅⊤, H⁆ = ⊥ ↔ H ≤ center G

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅H, center G⁆ = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ (map (g ∘ f)) x = (map g) ((map f) x)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ ∑ x ∈ s.toFinset, k • (count x s / k) • {x} = ∑ x ∈ s.toFinset, count x s • {x}

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
inst✝ : Mul α
x y : α
⊢ of x * of y = of (x * y)

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Mul α
x y z : FreeAbelianGroup α
⊢ (x + y) * z = x * z + y * z

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Mul α
a : FreeAbelianGroup α
⊢ 0 * a + 0 * a = 0 * a

Tactic:
by

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
h_base : base = Group.conjugatesOfSet base
⊢ (closure base).Normal

Tactic:
by

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Mul α
a : FreeAbelianGroup α
⊢ 0 * a = 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
k : ℕ
h : ∀ a ∈ s, k ∣ count a s
⊢ ∃ u, s = k • u

Tactic:
by

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

Goal state before:
pp: M : Type u_4
ι : Type u_5
inst✝ : CommMonoid M
f : ι → Multiset M
s : Finset ι
⊢ (∑ x ∈ s, f x).prod = ∏ x ∈ s, (f x).prod

Tactic:
by

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

Goal state before:
pp: G : Type u_1
G' : Type u_2
F : Type u_3
inst✝³ : Group G
inst✝² : Group G'
inst✝¹ : FunLike F G G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H H₁ H₂ H₃ K K₁ K₂ : Subgroup G
h₁ : H₁.Normal
h₂ : H₂.Normal
⊢ ⁅H₁, H₂⁆.Normal

Tactic:
by

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
s : Multiset M
⊢ IsUnit s.prod ↔ ∀ a ∈ s, IsUnit a

Tactic:
by

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ ⁅⊤, H⁆ ≤ H ↔ H.Normal

Tactic:
by

Goal state after: