-- Mathlib/GroupTheory/CosetCover.lean
theorem exists_finiteIndex_of_leftCoset_cover : ∃ k ∈ s, (H k).FiniteIndex

Proof state:
case neg
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ¬⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) = Set.univ
i : ι
hi : i ∈ s
left✝ : H i ≠ H j
hfi : (H i).FiniteIndex
⊢ ∃ k ∈ s, (H k).FiniteIndex

Tactic:
exact ⟨i, hi, hfi⟩

Result:
no goals

Proof state:
case pos
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) = Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex

Tactic:
rw [Set.iUnion₂_congr fun i hi => by rw [(Finset.mem_filter.mp hi).right]] at hcovers'

Result:
case pos
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H j) = Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) = Set.univ
i : ι
hi : i ∈ Finset.filter (fun x => H x = H j) s
⊢ g i • ↑(H i) = ?m.107987 i hi

Tactic:
rw [(Finset.mem_filter.mp hi).right]

Result:
no goals

Proof state:
case pos
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H j) = Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex

Tactic:
exact ⟨j, hj, finiteIndex_of_leftCoset_cover_const hcovers'⟩

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ¬⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) = Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex

Tactic:
have ⟨i, hi, _, hfi⟩ :=
  exists_finiteIndex_of_leftCoset_cover_aux hcovers j hj hcovers'

Result:
case neg
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
hcovers' : ¬⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) = Set.univ
i : ι
hi : i ∈ s
left✝ : H i ≠ H j
hfi : (H i).FiniteIndex
⊢ ∃ k ∈ s, (H k).FiniteIndex

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
⊢ ∃ k ∈ s, (H k).FiniteIndex

Tactic:
have ⟨j, hj⟩ : s.Nonempty := Finset.nonempty_iff_ne_empty.mpr fun hempty => by
  rw [hempty, ← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers
  exact Set.empty_ne_univ hcovers

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
j : ι
hj : j ∈ s
⊢ ∃ k ∈ s, (H k).FiniteIndex

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ⋃ i ∈ s, g i • ↑(H i) = Set.univ
hempty : s = ∅
⊢ False

Tactic:
rw [hempty, ← Finset.set_biUnion_coe, Finset.coe_empty, Set.biUnion_empty] at hcovers

Result:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ∅ = Set.univ
hempty : s = ∅
⊢ False

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
hcovers : ∅ = Set.univ
hempty : s = ∅
⊢ False

Tactic:
exact Set.empty_ne_univ hcovers

Result:
no goals