-- Mathlib/GroupTheory/Commutator/Finite.lean
theorem commutator_pi_pi_of_finite {η : Type*} [Finite η] {Gs : η → Type*} [∀ i, Group (Gs i)]
    (H K : ∀ i, Subgroup (Gs i)) : ⁅Subgroup.pi Set.univ H, Subgroup.pi Set.univ K⁆ =
    Subgroup.pi Set.univ fun i => ⁅H i, K i⁆

Proof state:
case h₂
η : 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 ∈ Set.univ, map (Pi.evalMonoidHom Gs i_1) (map (MonoidHom.mulSingle Gs i) (K i)) ≤ K i_1

Tactic:
intro j _hj

Result:
case h₂
η : 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 Gs j) (map (MonoidHom.mulSingle Gs i) (K i)) ≤ K j

Proof state:
case pos
η : 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 Gs j) ((MonoidHom.mulSingle Gs j) x) ∈ K j

Tactic:
simpa using hx

Result:
no goals

Proof state:
case neg
η : 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 Gs j) ((MonoidHom.mulSingle Gs i) x) ∈ K j

Tactic:
simp [h, one_mem]

Result:
no goals

Proof state:
η : 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.mulSingle Gs i) ⁅H i, K i⁆ → hi ∈ ⁅pi Set.univ H, pi Set.univ K⁆

Tactic:
rw [map_commutator]

Result:
η : 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.mulSingle Gs i) (H i), map (MonoidHom.mulSingle Gs i) (K i)⁆ →
    hi ∈ ⁅pi Set.univ H, pi Set.univ K⁆

Proof state:
case h₂.intro.intro.intro.intro
η : 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 Gs j) ((MonoidHom.mulSingle Gs i) x) ∈ K j

Tactic:
by_cases h : j = i

Result:
case pos
η : 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 Gs j) ((MonoidHom.mulSingle Gs i) x) ∈ K j

case neg
η : 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 Gs j) ((MonoidHom.mulSingle Gs i) x) ∈ K j

Proof state:
case h₂
η : 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 Gs j) (map (MonoidHom.mulSingle Gs i) (K i)) ≤ K j

Tactic:
rintro _ ⟨_, ⟨x, hx, rfl⟩, rfl⟩

Result:
case h₂.intro.intro.intro.intro
η : 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 Gs j) ((MonoidHom.mulSingle Gs i) x) ∈ K j

Proof state:
η : 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⁆

Tactic:
rw [pi_le_iff]

Result:
η : Type u_1
inst✝¹ : Finite η
Gs : η → Type u_2
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ ∀ (i : η), map (MonoidHom.mulSingle Gs i) ⁅H i, K i⁆ ≤ ⁅pi Set.univ H, pi Set.univ K⁆

Proof state:
η : 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⁆

Tactic:
apply le_antisymm (commutator_pi_pi_le H K)

Result:
η : 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⁆

Proof state:
case pos
η : 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 Gs j) ((MonoidHom.mulSingle Gs i) x) ∈ K j

Tactic:
subst h

Result:
case pos
η : 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 Gs j) ((MonoidHom.mulSingle Gs j) x) ∈ K j

Proof state:
case h₂
η : 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.mulSingle Gs i) (K i) ≤ pi Set.univ K

Tactic:
rw [le_pi_iff]

Result:
case h₂
η : 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 ∈ Set.univ, map (Pi.evalMonoidHom Gs i_1) (map (MonoidHom.mulSingle Gs i) (K i)) ≤ K i_1

Proof state:
η : Type u_1
inst✝¹ : Finite η
Gs : η → Type u_2
inst✝ : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ ∀ (i : η), map (MonoidHom.mulSingle Gs i) ⁅H i, K i⁆ ≤ ⁅pi Set.univ H, pi Set.univ K⁆

Tactic:
intro i hi

Result:
η : 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.mulSingle Gs i) ⁅H i, K i⁆ → hi ∈ ⁅pi Set.univ H, pi Set.univ K⁆