[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
⊢ ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁
[PROOFSTEP]
rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
⊢ ⁅g₁, g₂⁆⁻¹ = ⁅g₂, g₁⁆
[PROOFSTEP]
simp_rw [commutatorElement_def, mul_inv_rev, inv_inv, mul_assoc]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
⊢ ↑f ⁅g₁, g₂⁆ = ⁅↑f g₁, ↑f g₂⁆
[PROOFSTEP]
simp_rw [commutatorElement_def, map_mul f, map_inv f]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
⊢ ⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer ↑H₂
[PROOFSTEP]
rw [eq_bot_iff, commutator_le]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
⊢ (∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ⁅g₁, g₂⁆ ∈ ⊥) ↔ H₁ ≤ centralizer ↑H₂
[PROOFSTEP]
refine' forall_congr' fun p => forall_congr' fun _hp => forall_congr' fun q => forall_congr' fun hq => _
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
p : G
_hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅p, q⁆ ∈ ⊥ ↔ q * p = p * q
[PROOFSTEP]
rw [mem_bot, commutatorElement_eq_one_iff_mul_comm, eq_comm]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ⁅⁅H₂, H₃⁆, H₁⁆ = ⊥
h2 : ⁅⁅H₃, H₁⁆, H₂⁆ = ⊥
⊢ ⁅⁅H₁, H₂⁆, H₃⁆ = ⊥
[PROOFSTEP]
simp_rw [commutator_eq_bot_iff_le_centralizer, commutator_le, mem_centralizer_iff_commutator_eq_one, ←
  commutatorElement_def] at h1 h2 ⊢
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ ↑H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ ↑H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
⊢ ∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ∀ (h : G), h ∈ ↑H₃ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
[PROOFSTEP]
intro x hx y hy z hz
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ ↑H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ ↑H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ ⁅z, ⁅x, y⁆⁆ = 1
[PROOFSTEP]
trans x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ ↑H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ ↑H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ ⁅z, ⁅x, y⁆⁆ = x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹
[PROOFSTEP]
group
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ ↑H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), h ∈ ↑H₂ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
x : G
hx : x ∈ H₁
y : G
hy : y ∈ H₂
z : G
hz : z ∈ ↑H₃
⊢ x * z * ⁅y, ⁅z⁻¹, x⁻¹⁆⁆⁻¹ * z⁻¹ * y * ⁅x⁻¹, ⁅y⁻¹, z⁆⁆⁻¹ * y⁻¹ * x⁻¹ = 1
[PROOFSTEP]
rw [h1 _ (H₂.inv_mem hy) _ hz _ (H₁.inv_mem hx), h2 _ (H₃.inv_mem hz) _ (H₁.inv_mem hx) _ hy]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h1 : ∀ (g₁ : G), g₁ ∈ H₂ → ∀ (g₂ : G), g₂ ∈ H₃ → ∀ (h : G), h ∈ ↑H₁ → ⁅h, ⁅g₁, g₂⁆⁆ = 1
h2 : ∀ (g₁ : G), g₁ ∈ H₃ → ∀ (g₂ : G), g₂ ∈ H₁ → ∀ (h : G), 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
[PROOFSTEP]
group
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
⊢ Normal ⁅H₁, H₂⁆
[PROOFSTEP]
let base : Set G := {x | ∃ g₁ ∈ H₁, ∃ g₂ ∈ H₂, ⁅g₁, g₂⁆ = x}
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
⊢ Normal ⁅H₁, H₂⁆
[PROOFSTEP]
change (closure base).Normal
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
⊢ Normal (closure base)
[PROOFSTEP]
suffices h_base : base = Group.conjugatesOfSet base
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
h_base : base = Group.conjugatesOfSet base
⊢ Normal (closure base)
[PROOFSTEP]
rw [h_base]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
h_base : base = Group.conjugatesOfSet base
⊢ Normal (closure (Group.conjugatesOfSet base))
[PROOFSTEP]
exact Subgroup.normalClosure_normal
[GOAL]
case h_base
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
⊢ base = Group.conjugatesOfSet base
[PROOFSTEP]
refine' Set.Subset.antisymm Group.subset_conjugatesOfSet fun a h => _
[GOAL]
case h_base
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
a : G
h : a ∈ Group.conjugatesOfSet base
⊢ a ∈ base
[PROOFSTEP]
simp_rw [Group.mem_conjugatesOfSet_iff, isConj_iff] at h 
[GOAL]
case h_base
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
a : G
h : ∃ a_1, a_1 ∈ {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x} ∧ ∃ c, c * a_1 * c⁻¹ = a
⊢ a ∈ base
[PROOFSTEP]
rcases h with ⟨b, ⟨c, hc, e, he, rfl⟩, d, rfl⟩
[GOAL]
case h_base.intro.intro.intro.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
h₁ : Normal H₁
h₂ : Normal H₂
base : Set G := {x | ∃ g₁, g₁ ∈ H₁ ∧ ∃ g₂, g₂ ∈ H₂ ∧ ⁅g₁, g₂⁆ = x}
c : G
hc : c ∈ H₁
e : G
he : e ∈ H₂
d : G
⊢ d * ⁅c, e⁆ * d⁻¹ ∈ base
[PROOFSTEP]
exact ⟨_, h₁.conj_mem c hc d, _, h₂.conj_mem e he d, (conjugate_commutatorElement c e d).symm⟩
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
⊢ map f ⁅H₁, H₂⁆ = ⁅map f H₁, map f H₂⁆
[PROOFSTEP]
simp_rw [le_antisymm_iff, map_le_iff_le_comap, commutator_le, mem_comap, map_commutatorElement]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
⊢ (∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ⁅↑f g₁, ↑f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆) ∧
    ∀ (g₁ : G'), g₁ ∈ map f H₁ → ∀ (g₂ : G'), g₂ ∈ map f H₂ → ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
[PROOFSTEP]
constructor
[GOAL]
case left
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
⊢ ∀ (g₁ : G), g₁ ∈ H₁ → ∀ (g₂ : G), g₂ ∈ H₂ → ⁅↑f g₁, ↑f g₂⁆ ∈ ⁅map f H₁, map f H₂⁆
[PROOFSTEP]
intro p hp q hq
[GOAL]
case left
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ H₁
q : G
hq : q ∈ H₂
⊢ ⁅↑f p, ↑f q⁆ ∈ ⁅map f H₁, map f H₂⁆
[PROOFSTEP]
exact commutator_mem_commutator (mem_map_of_mem _ hp) (mem_map_of_mem _ hq)
[GOAL]
case right
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
⊢ ∀ (g₁ : G'), g₁ ∈ map f H₁ → ∀ (g₂ : G'), g₂ ∈ map f H₂ → ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
[PROOFSTEP]
rintro _ ⟨p, hp, rfl⟩ _ ⟨q, hq, rfl⟩
[GOAL]
case right.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ ⁅↑f p, ↑f q⁆ ∈ map f ⁅H₁, H₂⁆
[PROOFSTEP]
rw [← map_commutatorElement]
[GOAL]
case right.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f✝ : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ ↑H₁
q : G
hq : q ∈ ↑H₂
⊢ ↑f ⁅p, q⁆ ∈ map f ⁅H₁, H₂⁆
[PROOFSTEP]
exact mem_map_of_mem _ (commutator_mem_commutator hp hq)
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅prod H₁ K₁, prod H₂ K₂⁆ = prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅prod H₁ K₁, prod H₂ K₂⁆ ≤ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
[PROOFSTEP]
rw [commutator_le]
[GOAL]
case a
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ∀ (g₁ : G × G'), g₁ ∈ prod H₁ K₁ → ∀ (g₂ : G × G'), g₂ ∈ prod H₂ K₂ → ⁅g₁, g₂⁆ ∈ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
[PROOFSTEP]
rintro ⟨p₁, p₂⟩ ⟨hp₁, hp₂⟩ ⟨q₁, q₂⟩ ⟨hq₁, hq₂⟩
[GOAL]
case a.mk.intro.mk.intro
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
p₁ : G
p₂ : G'
hp₁ : (p₁, p₂).fst ∈ ↑H₁.toSubmonoid
hp₂ : (p₁, p₂).snd ∈ ↑K₁.toSubmonoid
q₁ : G
q₂ : G'
hq₁ : (q₁, q₂).fst ∈ ↑H₂.toSubmonoid
hq₂ : (q₁, q₂).snd ∈ ↑K₂.toSubmonoid
⊢ ⁅(p₁, p₂), (q₁, q₂)⁆ ∈ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆
[PROOFSTEP]
exact ⟨commutator_mem_commutator hp₁ hq₁, commutator_mem_commutator hp₂ hq₂⟩
[GOAL]
case a
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ prod ⁅H₁, H₂⁆ ⁅K₁, K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
[PROOFSTEP]
rw [prod_le_iff]
[GOAL]
case a
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆ ∧
    map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
[PROOFSTEP]
constructor
[GOAL]
case a.left
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
[PROOFSTEP]
rw [map_commutator]
[GOAL]
case a.left
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inl G G') H₁, map (MonoidHom.inl G G') H₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
[PROOFSTEP]
apply commutator_mono
[GOAL]
case a.left.h₁
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₁ ≤ prod H₁ K₁
[PROOFSTEP]
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl, MonoidHom.fst_comp_inr,
  MonoidHom.snd_comp_inr]
[GOAL]
case a.left.h₂
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') H₂ ≤ prod H₂ K₂
[PROOFSTEP]
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl, MonoidHom.fst_comp_inr,
  MonoidHom.snd_comp_inr]
[GOAL]
case a.right
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
[PROOFSTEP]
rw [map_commutator]
[GOAL]
case a.right
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅map (MonoidHom.inr G G') K₁, map (MonoidHom.inr G G') K₂⁆ ≤ ⁅prod H₁ K₁, prod H₂ K₂⁆
[PROOFSTEP]
apply commutator_mono
[GOAL]
case a.right.h₁
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₁ ≤ prod H₁ K₁
[PROOFSTEP]
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl, MonoidHom.fst_comp_inr,
  MonoidHom.snd_comp_inr]
[GOAL]
case a.right.h₂
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝² : Group G
inst✝¹ : Group G'
inst✝ : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁✝ K₂✝ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') K₂ ≤ prod H₂ K₂
[PROOFSTEP]
simp [le_prod_iff, map_map, MonoidHom.fst_comp_inl, MonoidHom.snd_comp_inl, MonoidHom.fst_comp_inr,
  MonoidHom.snd_comp_inr]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ ⁅pi Set.univ H, pi Set.univ K⁆ = pi Set.univ fun i => ⁅H i, K i⁆
[PROOFSTEP]
classical
apply le_antisymm (commutator_pi_pi_le H K)
· rw [pi_le_iff]
  intro i hi
  rw [map_commutator]
  apply commutator_mono <;>
    · rw [le_pi_iff]
      intro j _hj
      rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩
      by_cases h : j = i
      · subst h
        simpa using hx
      · simp [h, one_mem]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ ⁅pi Set.univ H, pi Set.univ K⁆ = pi Set.univ fun i => ⁅H i, K i⁆
[PROOFSTEP]
apply le_antisymm (commutator_pi_pi_le H K)
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ (pi Set.univ fun i => ⁅H i, K i⁆) ≤ ⁅pi Set.univ H, pi Set.univ K⁆
[PROOFSTEP]
rw [pi_le_iff]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ ∀ (i : η), map (MonoidHom.single (fun i => Gs i) i) ⁅H i, K i⁆ ≤ ⁅pi Set.univ H, pi Set.univ K⁆
[PROOFSTEP]
intro i hi
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ hi ∈ map (MonoidHom.single (fun i => Gs i) i) ⁅H i, K i⁆ → hi ∈ ⁅pi Set.univ H, pi Set.univ K⁆
[PROOFSTEP]
rw [map_commutator]
[GOAL]
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ hi ∈ ⁅map (MonoidHom.single (fun i => Gs i) i) (H i), map (MonoidHom.single (fun i => Gs i) i) (K i)⁆ →
    hi ∈ ⁅pi Set.univ H, pi Set.univ K⁆
[PROOFSTEP]
apply commutator_mono
[GOAL]
case h₁
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ map (MonoidHom.single (fun i => Gs i) i) (H i) ≤ pi Set.univ H
[PROOFSTEP]
rw [le_pi_iff]
[GOAL]
case h₁
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ ∀ (i_1 : η),
    i_1 ∈ Set.univ → map (Pi.evalMonoidHom (fun i => Gs i) i_1) (map (MonoidHom.single (fun i => Gs i) i) (H i)) ≤ H i_1
[PROOFSTEP]
intro j _hj
[GOAL]
case h₁
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
⊢ map (Pi.evalMonoidHom (fun i => Gs i) j) (map (MonoidHom.single (fun i => Gs i) i) (H i)) ≤ H j
[PROOFSTEP]
rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩
[GOAL]
case h₁.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(H i)
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) i) x) ∈ H j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(H i)
h : j = i
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) i) x) ∈ H j
[PROOFSTEP]
subst h
[GOAL]
case pos
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs j
hx : x ∈ ↑(H j)
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) j) x) ∈ H j
[PROOFSTEP]
simpa using hx
[GOAL]
case neg
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(H i)
h : ¬j = i
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) i) x) ∈ H j
[PROOFSTEP]
simp [h, one_mem]
[GOAL]
case h₂
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ map (MonoidHom.single (fun i => Gs i) i) (K i) ≤ pi Set.univ K
[PROOFSTEP]
rw [le_pi_iff]
[GOAL]
case h₂
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
⊢ ∀ (i_1 : η),
    i_1 ∈ Set.univ → map (Pi.evalMonoidHom (fun i => Gs i) i_1) (map (MonoidHom.single (fun i => Gs i) i) (K i)) ≤ K i_1
[PROOFSTEP]
intro j _hj
[GOAL]
case h₂
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
⊢ map (Pi.evalMonoidHom (fun i => Gs i) j) (map (MonoidHom.single (fun i => Gs i) i) (K i)) ≤ K j
[PROOFSTEP]
rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩
[GOAL]
case h₂.intro.intro.intro.intro
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(K i)
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) i) x) ∈ K j
[PROOFSTEP]
by_cases h : j = i
[GOAL]
case pos
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(K i)
h : j = i
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) i) x) ∈ K j
[PROOFSTEP]
subst h
[GOAL]
case pos
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs j
hx : x ∈ ↑(K j)
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) j) x) ∈ K j
[PROOFSTEP]
simpa using hx
[GOAL]
case neg
G : Type u_1
G' : Type u_2
F : Type u_3
inst✝⁴ : Group G
inst✝³ : Group G'
inst✝² : MonoidHomClass F G G'
f : F
g₁ g₂ g₃ g : G
H₁ H₂ H₃ K₁ K₂ : Subgroup G
η : Type u_4
inst✝¹ : Finite η
Gs : η → Type u_5
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
i : η
hi : (i : η) → Gs i
j : η
_hj : j ∈ Set.univ
x : Gs i
hx : x ∈ ↑(K i)
h : ¬j = i
⊢ ↑(Pi.evalMonoidHom (fun i => Gs i) j) (↑(MonoidHom.single (fun i => Gs i) i) x) ∈ K j
[PROOFSTEP]
simp [h, one_mem]
