-- Mathlib/GroupTheory/CosetCover.lean
theorem exists_finiteIndex_of_leftCoset_cover_aux [DecidableEq (Subgroup G)]
    (j : ι) (hj : j ∈ s) (hcovers' : ⋃ i ∈ s.filter (H · = H j), g i • (H i : Set G) ≠ Set.univ) :
    ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

Proof state:
case ind
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : 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
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ Finset.filter (fun x => H x ≠ H j) s, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 :=
  { x // x ∈ Finset.filter (fun x => H x ≠ H j) s } × Option { x // x ∈ Finset.filter (fun x => H x = H j) s }
f : κ → G :=
  fun x_1 =>
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k => H ↑k.1
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

Tactic:
have hK' (k : κ) : K k ∈ (s.image H).erase (H j) := by
  have := Finset.mem_filter.mp k.1.property
  exact Finset.mem_erase.mpr ⟨this.2, Finset.mem_image_of_mem H this.1⟩

Result:
case ind
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : 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
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ Finset.filter (fun x => H x ≠ H j) s, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 :=
  { x // x ∈ Finset.filter (fun x => H x ≠ H j) s } × Option { x // x ∈ Finset.filter (fun x => H x = H j) s }
f : κ → G :=
  fun x_1 =>
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k => H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
⊢ ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : 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
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
⊢ ∃ i, ∃ (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • ↑(H i)

Tactic:
have ⟨i, hi, hmem⟩ : ∃ i ∈ s, x * (y⁻¹ * z) ∈ g i • (H i : Set G) := by
  simpa using Set.eq_univ_iff_forall.mp hcovers (x * (y⁻¹ * z))

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : 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
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
i : ι
hi : i ∈ s
hmem : x * (y⁻¹ * z) ∈ g i • ↑(H i)
⊢ ∃ i, ∃ (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • ↑(H i)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : 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
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
⊢ ∃ i ∈ s, x * (y⁻¹ * z) ∈ g i • ↑(H i)

Tactic:
simpa using Set.eq_univ_iff_forall.mp hcovers (x * (y⁻¹ * z))

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : Type u_2
H : ι → Subgroup G
g : ι → G
s : Finset ι
j : ι
hj : j ∈ s
hcovers' : ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) ≠ Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • ↑(H j) ⊆ ⋃ i ∈ Finset.filter (fun x => H x ≠ H j) s, (y * x⁻¹ * g i) • ↑(H i)
κ : Type u_2 :=
  { x // x ∈ Finset.filter (fun x => H x ≠ H j) s } × Option { x // x ∈ Finset.filter (fun x => H x = H j) s }
f : κ → G :=
  fun x_1 =>
    match x_1 with
    | (k₁, some k₂) => g ↑k₂ * x⁻¹ * g ↑k₁
    | (k₁, none) => g ↑k₁
K : κ → Subgroup G := fun k => H ↑k.1
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
hK : ∀ (k : κ), K k ≠ H j
hcovers : ∅ = Set.univ
hempty : IsEmpty κ
⊢ False

Tactic:
exact Set.empty_ne_univ hcovers

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : 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
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
i : ι
hi : i ∈ s
hmem : x * (y⁻¹ * z) ∈ g i • ↑(H i)
⊢ ∃ i, ∃ (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • ↑(H i)

Tactic:
rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hmem

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι},
      ⋃ i ∈ s, g i • ↑(H i) = Set.univ →
        ∀ j ∈ s,
          ⋃ i ∈ Finset.filter (fun x => H x = H j) s, g i • ↑(H i) ≠ Set.univ →
            m = (Finset.image H s).card → ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex
ι : 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
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → ↑(g i) ≠ ↑x
y z : G
hz : z ∈ y • ↑(H j)
i : ι
hi : i ∈ s
hmem : ↑(g i) = ↑(x * (y⁻¹ * z))
⊢ ∃ i, ∃ (_ : i ∈ s ∧ H i ≠ H j), z ∈ (y * x⁻¹ * g i) • ↑(H i)