mathlib-initiative/mathlib-tactics huggingface dataset:
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 >>= fun x ↦ f x >>= g) = -(pure x >>= fun x ↦ f x >>= g)

Tactic:
]

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₂, f x = ∏ x ∈ s₂, f x

Tactic:
]

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 : ℕ
⊢ f 0 = f 0

Tactic:
]

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 >>= f) + (y >>= f) >>= g = x + y >>= fun x ↦ f x >>= g

Tactic:
]

Goal state after:
α : 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 >>= f) + (y >>= f) >>= g = x + y >>= fun x ↦ f x >>= g
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✝ n : ℕ
a✝ : n < n✝
h₁ : f n ≤ f (n + 1)
h₂ : f 0 ≤ f n
⊢ f (n + 1) - f 0 = f (n + 1) - f 0

Tactic:
]

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 = ∑ _x ∈ s, m

Tactic:
]

Goal state after:
ι : Type u_1
s : Finset ι
m : ℕ
f : ι → ℕ
h₁ : ∀ x ∈ s, f x = m
⊢ ∑ x ∈ s, f x = ∑ _x ∈ s, m
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 >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun x ↦ f x >>= g

Tactic:
]

Goal state after:
α : 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 >>= f >>= g) + (y >>= f >>= g) = x + y >>= fun x ↦ f x >>= g
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) ≤ #(t a) + #(s.biUnion t)

Tactic:
]

Goal state after:
ι : 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) ≤ #(t a) + #(s.biUnion t)
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 >>= fun x ↦ f x >>= g) + (y >>= fun x ↦ f x >>= g) = x + y >>= fun x ↦ f x >>= g

Tactic:
]

Goal state after:
α : 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 >>= fun x ↦ f x >>= g) + (y >>= fun x ↦ f x >>= g) = x + y >>= fun x ↦ f x >>= g
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 = ∏ j, ∏ i with g i = j, f i

Tactic:
]

Goal state after:
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 = ∏ j, ∏ i with g i = j, f i
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 >>= fun x ↦ f x >>= g) + (y >>= fun x ↦ f x >>= g) = (x >>= fun x ↦ f x >>= g) + (y >>= fun x ↦ f x >>= g)

Tactic:
]

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₁

Tactic:
]

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 = ∏ j, ∏ i with g i = j, f j

Tactic:
]

Goal state after:
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 = ∏ j, ∏ i with g i = j, f j
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
]

Goal state after:
case pure
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
p : α✝
⊢ Prod.mk p <$> y = (fun b a ↦ (a, b)) <$> y <*> pure p
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
rw [map_pure, pure_seq]

Goal state after:
case pure
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
p : α✝
⊢ Prod.mk p <$> y = (fun b a ↦ (a, b)) <$> y <*> pure p
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.zero
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
⊢ 0 = 0

Tactic:
]

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
⊢ f default = f default

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.pure
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
q : β✝
⊢ pure (p, q) = pure (p, q)

Tactic:
]

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 : ι
this : Unique ι
⊢ f a = f a

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.neg
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
q : β✝
ih : Prod.mk p <$> pure q = (fun b a ↦ (a, b)) <$> pure q <*> pure p
⊢ -((fun b a ↦ (a, b)) <$> pure q <*> pure p) = -((fun b a ↦ (a, b)) <$> pure q <*> pure p)

Tactic:
]

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
s : Finset ι := {x | p x}.toFinset
⊢ (∏ a ∈ s, f a) * ∏ a ∈ sᶜ, f a = ∏ i, f i

pp: case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ sᶜ ↔ ¬p x

pp: case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ s ↔ p x

Tactic:
]

Goal state after:
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ (∏ a ∈ s, f a) * ∏ a ∈ sᶜ, f a = ∏ i, f i

case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ sᶜ ↔ ¬p x

case h
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ ∀ (x : ι), x ∈ s ↔ p x
Module: Mathlib.GroupTheory.Commutator.Basic

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

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ (∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ ⊥) ↔ H₁ ≤ centralizer ↑H₂
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
p : G
_hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ q * p = p * q ↔ q * p = p * q

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
y₁ y₂ : FreeAbelianGroup β✝
ih1 : Prod.mk p <$> y₁ = (fun b a ↦ (a, b)) <$> y₁ <*> pure p
ih2 : Prod.mk p <$> y₂ = (fun b a ↦ (a, b)) <$> y₂ <*> pure p
⊢ ((fun b a ↦ (a, b)) <$> y₁ <*> pure p) + ((fun b a ↦ (a, b)) <$> y₂ <*> pure p) =
    ((fun b a ↦ (a, b)) <$> y₁ <*> pure p) + ((fun b a ↦ (a, b)) <$> y₂ <*> pure p)

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
]

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 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * 1⁻¹ * z⁻¹ * y * 1⁻¹ * y⁻¹ * x⁻¹ = 1

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ H₃ : Subgroup G
h1 : ∀ g₁ ∈ H₂, ∀ g₂ ∈ H₃, ∀ h ∈ ↑H₁, ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ g₁ ∈ H₃, ∀ g₂ ∈ H₁, ∀ h ∈ ↑H₂, ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * 1⁻¹ * z⁻¹ * y * 1⁻¹ * y⁻¹ * x⁻¹ = 1
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
⊢ ∑ x ∈ s with count x m ≠ 0, count x m = ∑ a ∈ m.toFinset, count a m

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
⊢ ∑ x ∈ s with count x m ≠ 0, count x m = ∑ a ∈ m.toFinset, count a m
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Multiset ι
⊢ s = s

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ IsMulCommutative ↥H ↔ IsMulCommutative ↥H

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
]

Goal state after:
α : Type u
x : FreeAbelianGroup α
⊢ (AddMonoidHom.id (FreeAbelianGroup α)) x = x
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H ≤ center G ↔ H ≤ center G

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
]

Goal state after:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ((map g).comp (map f)) x = (map g) ((map f) x)
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 : ι
hx : x ∈ s.toFinset
⊢ count x s • {x} = count x s • {x}

Tactic:
]

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 (Group.conjugatesOfSet base)).Normal

Tactic:
]

Goal state after:
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 (Group.conjugatesOfSet base)).Normal
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of.of
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
⊢ of (L1 * (L2 * L3)) = of (L1 * (L2 * L3))

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 L1 : α
ih : of L1 * of L2 * of L3 = of L1 * (of L2 * of L3)
⊢ -(of L1 * (of L2 * of L3)) = -(of L1 * (of L2 * of L3))

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H₁ H₂ : Subgroup G
inst✝¹ : H₁.Normal
inst✝ : H₂.Normal
h : Disjoint H₁ H₂
⊢ ⊥ ≤ ⊥

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
L3 L2 : α
x₁ x₂ : FreeAbelianGroup α
ih₁ : x₁ * of L2 * of L3 = x₁ * (of L2 * of L3)
ih₂ : x₂ * of L2 * of L3 = x₂ * (of L2 * of L3)
⊢ x₁ * (of L2 * of L3) + x₂ * (of L2 * of L3) = x₁ * (of L2 * of L3) + x₂ * (of L2 * of L3)

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
g : G
hg : g ∈ H₁
g₁ : G
hg₁ : g₁ ∈ H₁
g₂ : G
hg₂ : g₂ ∈ H₂
⊢ ⁅g * g₁, g₂⁆ ∈ ⁅H₁, H₂⁆

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
g : G
hg : g ∈ H₁
g₁ : G
hg₁ : g₁ ∈ H₁
g₂ : G
hg₂ : g₂ ∈ H₂
⊢ ⁅g * g₁, g₂⁆ ∈ ⁅H₁, H₂⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 L2 : α
ih : x * of L2 * of L3 = x * (of L2 * of L3)
⊢ -(x * (of L2 * of L3)) = -(x * (of L2 * of L3))

Tactic:
]

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

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

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ H₂ ≤ normalizer ↑⁅H₂, H₁⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 : α
y₁ y₂ : FreeAbelianGroup α
ih₁ : x * y₁ * of L3 = x * (y₁ * of L3)
ih₂ : x * y₂ * of L3 = x * (y₂ * of L3)
⊢ x * (y₁ * of L3) + x * (y₂ * of L3) = x * (y₁ * of L3) + x * (y₂ * of L3)

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y : FreeAbelianGroup α
L3 : α
ih : x * y * of L3 = x * (y * of L3)
⊢ -(x * (y * of L3)) = -(x * (y * of L3))

Tactic:
]

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

Goal state before:
pp: case right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ f ⁅p, q⁆ ∈ map f ⁅H₁, H₂⁆

Tactic:
]

Goal state after:
case right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ f ⁅p, q⁆ ∈ map f ⁅H₁, H₂⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x y z₁ z₂ : FreeAbelianGroup α
ih₁ : x * y * z₁ = x * (y * z₁)
ih₂ : x * y * z₂ = x * (y * z₂)
⊢ x * (y * z₁) + x * (y * z₂) = x * (y * z₁) + x * (y * z₂)

Tactic:
]

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

Goal state before:
pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ∀ g₁ ∈ H₁.prod K₁, ∀ g₂ ∈ H₂.prod K₂, ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆

Tactic:
]

Goal state after:
case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ∀ g₁ ∈ H₁.prod K₁, ∀ g₂ ∈ H₂.prod K₂, ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆ ∧
    map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
]

Goal state after:
case a
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆ ∧
    map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
L : α
⊢ of L = of L

Tactic:
]

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

Goal state before:
pp: case a.left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inl G G') H₁, map (MonoidHom.inl G G') H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
]

Goal state after:
case a.left
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inl G G') H₁, map (MonoidHom.inl G G') H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
L : α
ih : (lift fun x₂ ↦ of (1 * x₂)) (of L) = of L
⊢ -of L = -of L

Tactic:
]

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

Goal state before:
pp: case a.right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inr G G') K₁, map (MonoidHom.inr G G') K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆

Tactic:
]

Goal state after:
case a.right
G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inr G G') K₁, map (MonoidHom.inr G G') K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x1 x2 : FreeAbelianGroup α
ih1 : (lift fun x₂ ↦ of (1 * x₂)) x1 = x1
ih2 : (lift fun x₂ ↦ of (1 * x₂)) x2 = x2
⊢ x1 + x2 = x1 + x2

Tactic:
]

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, H⁆

Tactic:
]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₁ ↦ of (x₁ * 1)) x = x

Tactic:
]

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x : FreeAbelianGroup α
⊢ (lift fun x₁ ↦ of (x₁ * 1)) x = x
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ IsMulCommutative G ↔ IsMulCommutative G

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⁅⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆, ⊤⁆ = ⊥

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ ⁅⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆, ⊤⁆ = ⊥
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
this : ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
⊢ ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
this : ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
⊢ ⁅⁅⊤, centralizer ↑(commutator G)⁆, centralizer ↑(commutator G)⁆ = ⊥
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case neg
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
L : α
ih : (lift fun x₁ ↦ of (x₁ * 1)) (of L) = of L
⊢ -of L = -of L

Tactic:
]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ centralizer ↑(commutator G) ≤ centralizer ↑⁅⊤, centralizer ↑(commutator G)⁆

Tactic:
]

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ centralizer ↑(commutator G) ≤ centralizer ↑⁅⊤, centralizer ↑(commutator G)⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case h
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ^ 2 * ↑h * (↑h)⁻¹ * g⁻¹ = g

Tactic:
]

Goal state after:
case h
G : Type u_1
inst✝ : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h) g (g ^ 2)
⊢ g ^ 2 * ↑h * (↑h)⁻¹ * g⁻¹ = g
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ ⁅map f ⊤, map f ⊤⁆ = ⁅f.range, f.range⁆

Tactic:
]

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ ⁅map f ⊤, map f ⊤⁆ = ⁅f.range, f.range⁆
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case hx
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ Codisjoint ⊤ f.ker

Tactic:
]

Goal state after:
case hx
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ Codisjoint ⊤ f.ker
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: case hx
G : Type u_1
inst✝¹ : Group G
H : Type u_4
inst✝ : Group H
f : G →* H
⊢ ⊤ = ⊤

Tactic:
]

Goal state after: