case mk.mk
G : Type u_2
inst✝ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
x : G
hx : x ∈ H i
y : G
hy : y ∈ H j
⊢ Commute (↑(Subgroup.subtype (H i)) { val := x, property := hx })
    (↑(Subgroup.subtype (H j)) { val := y, property := hy })
G : Type u_2
inst✝ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
⊢ ∀ (x : { x // x ∈ H i }) (y : { x // x ∈ H j }), Commute (↑(Subgroup.subtype (H i)) x) (↑(Subgroup.subtype (H j)) y)
rintro ⟨x, hx⟩ ⟨y, hy⟩
no goals
case mk.mk
G : Type u_2
inst✝ : Group G
ι : Type u_1
hdec : DecidableEq ι
hfin : Fintype ι
H : ι → Subgroup G
f g : (i : ι) → { x // x ∈ H i }
hcomm : ∀ (i j : ι), i ≠ j → ∀ (x y : G), x ∈ H i → y ∈ H j → Commute x y
i j : ι
hne : i ≠ j
x : G
hx : x ∈ H i
y : G
hy : y ∈ H j
⊢ Commute (↑(Subgroup.subtype (H i)) { val := x, property := hx })
    (↑(Subgroup.subtype (H j)) { val := y, property := hy })
exact hcomm i j hne x y hx hy