G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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⁆
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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⁆
apply le_antisymm (commutator_pi_pi_le H K)
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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⁆
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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⁆
rw [pi_le_iff]
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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⁆
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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⁆
intro i hi
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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⁆
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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⁆
rw [map_commutator]
case h₂
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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
case h₂
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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
rw [le_pi_iff]
case h₂
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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
case h₂
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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
intro j _hj
case h₂.intro.intro.intro.intro
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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
case h₂
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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
rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩
case pos
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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

case neg
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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
case h₂.intro.intro.intro.intro
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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
by_cases h : j = i
case pos
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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
case pos
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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
subst h
no goals
case pos
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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
simpa using hx
no goals
case neg
G : Type ?u.102458
G' : Type ?u.102461
F : Type ?u.102464
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_1
inst✝¹ : Finite η
Gs : η → Type u_2
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
simp [h, one_mem]