G : Type u_1
inst✝ : Group G
V : Set G
⊢ 0 ∈ Finset.card '' {t | ∅ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V} ∨
    Finset.card '' {t | ∅ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V} = ∅
G : Type u_1
inst✝ : Group G
V : Set G
⊢ index ∅ V = 0
simp only [index, Nat.sInf_eq_zero]
case h
G : Type u_1
inst✝ : Group G
V : Set G
⊢ 0 ∈ Finset.card '' {t | ∅ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
G : Type u_1
inst✝ : Group G
V : Set G
⊢ 0 ∈ Finset.card '' {t | ∅ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V} ∨
    Finset.card '' {t | ∅ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V} = ∅
left
case h
G : Type u_1
inst✝ : Group G
V : Set G
⊢ ∅ ∈ {t | ∅ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V} ∧ Finset.card ∅ = 0
case h
G : Type u_1
inst✝ : Group G
V : Set G
⊢ 0 ∈ Finset.card '' {t | ∅ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V}
use ∅
no goals
case h
G : Type u_1
inst✝ : Group G
V : Set G
⊢ ∅ ∈ {t | ∅ ⊆ ⋃ (g : G) (_ : g ∈ t), (fun h => g * h) ⁻¹' V} ∧ Finset.card ∅ = 0
simp only [Finset.card_empty, empty_subset, mem_setOf_eq, eq_self_iff_true, and_self_iff]