awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
j : ι
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ i ∈ s, H i = H j → Ne (α := G ⧸ H i) (↑(g i) : G ⧸ H i) (↑x : G ⧸ H i)
⊢ ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)

Tactic:
replace hx : ∀ (y : G), y • (H j : Set G) ⊆
        ⋃ i ∈ s.filter (H · ≠ H j), (y * x⁻¹ * g i) • (H i : Set G) := by
      intro y z hz
      simp_rw [Finset.mem_filter, Set.mem_iUnion]
      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))
      rw [mem_leftCoset_iff, SetLike.mem_coe, ← QuotientGroup.eq] at hmem
      refine ⟨i, ⟨hi, fun hij => hx i hi hij ?_⟩, ?_⟩
      · rwa [hmem, eq_comm, QuotientGroup.eq, hij, inv_mul_cancel_left,
          ← SetLike.mem_coe, ← mem_leftCoset_iff]
      · simpa [mem_leftCoset_iff, SetLike.mem_coe, QuotientGroup.eq, mul_assoc] using hmem
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
j : ι
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
K : (k : κ) → Subgroup G := fun (k : κ) ↦ H (↑k.1 : ι)
k : κ
⊢ (↑k.1 : ι) ∈ s ∧ H (↑k.1 : ι) ≠ H j

Tactic:
have := Finset.mem_filter.mp k.1.property
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
j : ι
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
K : (k : κ) → Subgroup G := fun (k : κ) ↦ H (↑k.1 : ι)
k : κ
this : (↑k.1 : ι) ∈ s ∧ H (↑k.1 : ι) ≠ H j
⊢ K k ∈ (Finset.image H s).erase (H j)

Tactic:
Finset.mem_erase.mpr ⟨this.2, Finset.mem_image_of_mem H this.1⟩

Premises used: Iff.mpr, Finset.mem_erase, And.right, And.left, And.intro, Finset.mem_image_of_mem
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
j : ι
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
K : (k : κ) → Subgroup G := fun (k : κ) ↦ H (↑k.1 : ι)
k : κ
this : (↑k.1 : ι) ∈ s ∧ H (↑k.1 : ι) ≠ H j
⊢ K k ∈ (Finset.image H s).erase (H j)

Tactic:
exact Finset.mem_erase.mpr ⟨this.2, Finset.mem_image_of_mem H this.1⟩

Premises used: Iff.mpr, Finset.mem_erase, And.right, And.left, And.intro, Finset.mem_image_of_mem
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
j : ι
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
K : (k : κ) → Subgroup G := fun (k : κ) ↦ H (↑k.1 : ι)
⊢ ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)

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⟩
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
j : ι
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
K : (k : κ) → Subgroup G := fun (k : κ) ↦ H (↑k.1 : ι)
hK' : ∀ (k : κ), K k ∈ (Finset.image H s).erase (H j)
⊢ ∀ (k : κ), K k ≠ H j

Tactic:
have hK (k : κ) : K k ≠ H j := ((Finset.mem_erase.mp (hK' k)).left ·)
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ
j : ι
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
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
y : G
rw :
  ∀
    (hcovers :
      Eq.{u_1 + 1} (α := Set G)
        ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G))
        Set.univ)
    (hj : j ∈ s) (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
    (hn : n = (Finset.image H s).card) (x : G)
    (hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)),
    let κ := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j});
    let f : κ → G := fun (x_1 : κ) ↦
      match (motive := κ → G) x_1 with
      | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
      | (k₁, none) => g (↑k₁ : ι);
    let 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) (y : G),
      ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
⊢ ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)

Tactic:
rw [← s.filter_union_filter_not_eq (H · = H j), Finset.set_biUnion_union] at hcovers

Premises used: Finset.filter_union_filter_not_eq, Finset.set_biUnion_union, Eq
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : ι
hcovers :
  Eq.{u_1 + 1} (α := Set G)
    ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) Set.univ
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
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
y : G
hy : Membership.mem (γ := Set G) (⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) y
inl :
  ∀ (k : ι) (hk : k ∈ {x ∈ s | H x = H j}) (hy : y ∈ g k • (↑(H k) : Set G)),
    ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
⊢ ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)

Tactic:
have ⟨k, hk, hy⟩ := Set.mem_iUnion₂.mp hy
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : ι
hcovers :
  Eq.{u_1 + 1} (α := Set G)
    ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) Set.univ
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
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
y : G
hy_1 : Membership.mem (γ := Set G) (⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) y
k : ι
hk : k ∈ {x ∈ s | H x = H j}
hy : y ∈ g k • (↑(H k) : Set G)
⊢ k ∈ s ∧ H k = H j

Tactic:
simpa using hk
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : ι
hcovers :
  Eq.{u_1 + 1} (α := Set G)
    ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) Set.univ
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
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
y : G
hy_1 : Membership.mem (γ := Set G) (⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) y
k : ι
hk : k ∈ {x ∈ s | H x = H j}
hy : y ∈ g k • (↑(H k) : Set G)
⊢ H k = H j

Tactic:
have hk' : H k = H j := And.right <| by simpa using hk
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : ι
hcovers :
  Eq.{u_1 + 1} (α := Set G)
    ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) Set.univ
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
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
y : G
hy_1 : Membership.mem (γ := Set G) (⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) y
k : ι
hk : k ∈ {x ∈ s | H x = H j}
hy : y ∈ g k • (↑(H k) : Set G)
hk' : H k = H j
inl :
  ∀ (i : ι) (hi : i ∈ {x ∈ s | H x ≠ H j}) (hy : y ∈ (g k * x⁻¹ * g i) • (↑(H i) : Set G)),
    ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
⊢ ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)

Tactic:
have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp (hx (g k) (hk' ▸ hy))
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : ι
hcovers :
  Eq.{u_1 + 1} (α := Set G)
    ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) Set.univ
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
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
y : G
hy_1 : Membership.mem (γ := Set G) (⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) y
k : ι
hk : k ∈ {x ∈ s | H x = H j}
hy_2 : y ∈ g k • (↑(H k) : Set G)
hk' : H k = H j
i : ι
hi : i ∈ {x ∈ s | H x ≠ H j}
hy : y ∈ (g k * x⁻¹ * g i) • (↑(H i) : Set G)
⊢ ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)

Tactic:
⟨⟨⟨i, hi⟩, some ⟨k, hk⟩⟩, Finset.mem_univ _, hy⟩

Premises used: Finset.mem_univ, Option.some, Prod.mk, Subtype.mk, Exists.intro
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : ι
hcovers :
  Eq.{u_1 + 1} (α := Set G)
    ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) Set.univ
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
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
y : G
hy_1 : Membership.mem (γ := Set G) (⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) y
k : ι
hk : k ∈ {x ∈ s | H x = H j}
hy_2 : y ∈ g k • (↑(H k) : Set G)
hk' : H k = H j
i : ι
hi : i ∈ {x ∈ s | H x ≠ H j}
hy : y ∈ (g k * x⁻¹ * g i) • (↑(H i) : Set G)
⊢ ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)

Tactic:
exact ⟨⟨⟨i, hi⟩, some ⟨k, hk⟩⟩, Finset.mem_univ _, hy⟩
-- Module: Mathlib.GroupTheory.CosetCover
Goal:
G : Type u_1
inst : Group G
inst_1 : DecidableEq (Subgroup G)
n : ℕ
ih :
  ∀ m < n,
    ∀ {ι : Type u_2} {H : ι → Subgroup G} {g : ι → G} {s : Finset ι}
      (hcovers : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ s, g i • (↑(H i) : Set G)) Set.univ) (j : ι) (hj : j ∈ s)
      (hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ)
      (hn : 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 : ι
hcovers :
  Eq.{u_1 + 1} (α := Set G)
    ((⋃ x ∈ {x ∈ s | H x = H j}, g x • (↑(H x) : Set G)) ∪ ⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) Set.univ
hj : j ∈ s
hcovers' : Ne.{u_1 + 1} (α := Set G) (⋃ i ∈ {x ∈ s | H x = H j}, g i • (↑(H i) : Set G)) Set.univ
hn : n = (Finset.image H s).card
x : G
hx : ∀ (y : G), y • (↑(H j) : Set G) ⊆ ⋃ i ∈ {x ∈ s | H x ≠ H j}, (y * x⁻¹ * g i) • (↑(H i) : Set G)
κ : Type u_2 := ↥({x ∈ s | H x ≠ H j}) × Option ↥({x ∈ s | H x = H j})
f : κ → G :=
  fun (x_1 : κ) ↦
    match (motive := κ → G) x_1 with
    | (k₁, some k₂) => g (↑k₂ : ι) * x⁻¹ * g (↑k₁ : ι)
    | (k₁, none) => g (↑k₁ : ι)
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
y : G
hy : Membership.mem (γ := Set G) (⋃ x ∈ {a ∈ s | ¬H a = H j}, g x • (↑(H x) : Set G)) y
inr :
  ∀ (i : ι) (hi : i ∈ {a ∈ s | ¬H a = H j}) (hy : y ∈ g i • (↑(H i) : Set G)),
    ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)
⊢ ∃ (i : κ) (_ : Membership.mem (γ := Finset κ) Finset.univ i), y ∈ f i • (↑(K i) : Set G)

Tactic:
have ⟨i, hi, hy⟩ := Set.mem_iUnion₂.mp hy