case intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ index H ≠ 0
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : Finite (G ⧸ H)
⊢ index H ≠ 0
cases nonempty_fintype (G ⧸ H)
case intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ Fintype.card (G ⧸ H) ≠ 0
case intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ index H ≠ 0
rw [index_eq_card]
no goals
case intro
G : Type u_1
inst✝ : Group G
H K L : Subgroup G
hH : Finite (G ⧸ H)
val✝ : Fintype (G ⧸ H)
⊢ Fintype.card (G ⧸ H) ≠ 0
exact Fintype.card_ne_zero