awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
cover : Eq.{u_1 + 1} (α := Set G) (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)), quotToDoubleCoset H K q) Set.univ
x : Quot (α := G) (⇑(rightRel H) : G → G → Prop)
obtain :
  ∀ (y : G) (hy : ⟦y⟧ = x),
    ∃ (i : Quotient (↑H : Set G) (↑K : Set G)),
      Membership.mem (γ := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop)))
        (Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) x
⊢ ∃ (i : Quotient (↑H : Set G) (↑K : Set G)),
    Membership.mem (γ := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop)))
      (Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) x

Tactic:
obtain ⟨y, hy⟩ := exists_rep x

Premises used: Quotient.exists_rep
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
cover : Eq.{u_1 + 1} (α := Set G) (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)), quotToDoubleCoset H K q) Set.univ
x : Quot (α := G) (⇑(rightRel H) : G → G → Prop)
y : G
hy : ⟦y⟧ = x
contrapose :
  ∀ (cover : ¬∃ (i : Quotient (↑H : Set G) (↑K : Set G)), y ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)),
    ¬Eq.{u_1 + 1} (α := Set G) (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)), quotToDoubleCoset H K q) Set.univ
⊢ ∃ (i : Quotient (↑H : Set G) (↑K : Set G)), y ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)

Tactic:
contrapose cover
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
x : Quot (α := G) (⇑(rightRel H) : G → G → Prop)
y : G
hy : ⟦y⟧ = x
cover : ¬∃ (i : Quotient (↑H : Set G) (↑K : Set G)), y ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)
⊢ y ∉ ⋃ (q : Quotient (↑H : Set G) (↑K : Set G)), quotToDoubleCoset H K q

Tactic:
simpa using cover
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
x : Quot (α := G) (⇑(rightRel H) : G → G → Prop)
y : G
hy : ⟦y⟧ = x
cover : ¬∃ (i : Quotient (↑H : Set G) (↑K : Set G)), y ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)
⊢ ¬Eq.{u_1 + 1} (α := Set G) (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)), quotToDoubleCoset H K q) Set.univ

Tactic:
exact (Set.ne_univ_iff_exists_notMem _).mpr ⟨y, by simpa using cover⟩

Premises used: Iff.mpr, Set.ne_univ_iff_exists_notMem, Exists.intro
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
cover : Eq.{u_1 + 1} (α := Set G) (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)), quotToDoubleCoset H K q) Set.univ
x : Quot (α := G) (⇑(rightRel H) : G → G → Prop)
y : G
hy : ⟦y⟧ = x
have :
  ∀ (i : Quotient (↑H : Set G) (↑K : Set G)) (hi : y ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)),
    ∃ (i : Quotient (↑H : Set G) (↑K : Set G)),
      Membership.mem (γ := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop)))
        (Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) x
⊢ ∃ (i : Quotient (↑H : Set G) (↑K : Set G)),
    Membership.mem (γ := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop)))
      (Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) x

Tactic:
have ⟨i, hi⟩ : ∃ i : Quotient H K, y ∈ doubleCoset (out i) H K := by
    contrapose cover
    exact (Set.ne_univ_iff_exists_notMem _).mpr ⟨y, by simpa using cover⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
cover : Eq.{u_1 + 1} (α := Set G) (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)), quotToDoubleCoset H K q) Set.univ
x : Quot (α := G) (⇑(rightRel H) : G → G → Prop)
y : G
hy : ⟦y⟧ = x
i : Quotient (↑H : Set G) (↑K : Set G)
hi : y ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)
⊢ ∃ (i : Quotient (↑H : Set G) (↑K : Set G)),
    Membership.mem (γ := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop)))
      (Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) x

Tactic:
⟨i, y, hi, hy⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
cover : Eq.{u_1 + 1} (α := Set G) (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)), quotToDoubleCoset H K q) Set.univ
x : Quot (α := G) (⇑(rightRel H) : G → G → Prop)
y : G
hy : ⟦y⟧ = x
i : Quotient (↑H : Set G) (↑K : Set G)
hi : y ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)
⊢ ∃ (i : Quotient (↑H : Set G) (↑K : Set G)),
    Membership.mem (γ := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop)))
      (Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) x

Tactic:
exact ⟨i, y, hi, hy⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht :
  Subset.{u_1} (α := Set (Quot (α := G) (⇑(leftRel K) : G → G → Prop))) Set.univ
    (⋃ i ∈ t, Quot.mk (⇑(leftRel K) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G))
contrapose :
  ∀ (ht : ¬Eq.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ),
    ¬Subset.{u_1} (α := Set (Quot (α := G) (⇑(leftRel K) : G → G → Prop))) Set.univ
        (⋃ i ∈ t, Quot.mk (⇑(leftRel K) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G))
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ

Tactic:
contrapose ht
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : ¬Eq.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
simp :
  Ne.{u_1 + 1} (α := Set (Quot (α := G) (⇑(leftRel K) : G → G → Prop)))
    (⋃ i ∈ t, Quot.mk (⇑(leftRel K) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) Set.univ
⊢ ¬Subset.{u_1} (α := Set (Quot (α := G) (⇑(leftRel K) : G → G → Prop))) Set.univ
      (⋃ i ∈ t, Quot.mk (⇑(leftRel K) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G))

Tactic:
simp only [Set.univ_subset_iff, ← ne_eq] at ⊢ ht

Premises used: Set.univ_subset_iff, ne_eq
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
obtain :
  ∀ (x : G) (hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)),
    Ne.{u_1 + 1} (α := Set (Quot (α := G) (⇑(leftRel K) : G → G → Prop)))
      (⋃ i ∈ t, Quot.mk (⇑(leftRel K) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) Set.univ
⊢ Ne.{u_1 + 1} (α := Set (Quot (α := G) (⇑(leftRel K) : G → G → Prop)))
    (⋃ i ∈ t, Quot.mk (⇑(leftRel K) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) Set.univ

Tactic:
obtain ⟨x, hx⟩ := (Set.ne_univ_iff_exists_notMem _).mp ht

Premises used: Set.ne_univ_iff_exists_notMem, Iff.mp
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)
⊢ Ne.{u_1 + 1} (α := Set (Quot (α := G) (⇑(leftRel K) : G → G → Prop)))
    (⋃ i ∈ t, Quot.mk (⇑(leftRel K) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) Set.univ

Tactic:
(Set.ne_univ_iff_exists_notMem _).mpr ⟨Quot.mk (leftRel K) x, ?_⟩

Premises used: Iff.mpr, Set.ne_univ_iff_exists_notMem, Exists.intro, Setoid.r, Quot.mk
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)
refine :
  Quot.mk (⇑(leftRel K) : G → G → Prop) x ∉
    ⋃ i ∈ t, Quot.mk (⇑(leftRel K) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)
⊢ Ne.{u_1 + 1} (α := Set (Quot (α := G) (⇑(leftRel K) : G → G → Prop)))
    (⋃ i ∈ t, Quot.mk (⇑(leftRel K) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) Set.univ

Tactic:
refine (Set.ne_univ_iff_exists_notMem _).mpr ⟨Quot.mk (leftRel K) x, ?_⟩

Premises used: Iff.mpr, Set.ne_univ_iff_exists_notMem, Exists.intro, Setoid.r, Quot.mk
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)
simp :
  ∀ x_1 ∈ t,
    ∀ x_2 ∈ doubleCoset (out x_1) (↑H : Set G) (↑K : Set G),
      ¬Eq (α := Quot (α := G) (⇑(leftRel K) : G → G → Prop)) (Quot.mk (⇑(leftRel K) : G → G → Prop) x_2)
          (Quot.mk (⇑(leftRel K) : G → G → Prop) x)
⊢ Quot.mk (⇑(leftRel K) : G → G → Prop) x ∉
    ⋃ i ∈ t, Quot.mk (⇑(leftRel K) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)

Tactic:
simp only [Set.mem_iUnion, Set.mem_image, exists_prop, not_exists, not_and]

Premises used: Set.mem_iUnion, Set.mem_image, not_exists, exists_prop, not_and
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
contrapose :
  ∀
    (hx :
      Eq (α := Quot (α := G) (⇑(leftRel K) : G → G → Prop)) (Quot.mk (⇑(leftRel K) : G → G → Prop) q)
        (Quot.mk (⇑(leftRel K) : G → G → Prop) x)),
    Membership.mem (γ := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) x
⊢ ¬Eq (α := Quot (α := G) (⇑(leftRel K) : G → G → Prop)) (Quot.mk (⇑(leftRel K) : G → G → Prop) q)
      (Quot.mk (⇑(leftRel K) : G → G → Prop) x)

Tactic:
contrapose hx
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(leftRel K) : G → G → Prop)) (Quot.mk (⇑(leftRel K) : G → G → Prop) q)
    (Quot.mk (⇑(leftRel K) : G → G → Prop) x)
simp : ∃ i ∈ t, x ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)
⊢ Membership.mem (γ := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) x

Tactic:
simp only [Set.mem_iUnion, exists_prop]

Premises used: Set.mem_iUnion, exists_prop
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(leftRel K) : G → G → Prop)) (Quot.mk (⇑(leftRel K) : G → G → Prop) q)
    (Quot.mk (⇑(leftRel K) : G → G → Prop) x)
⊢ ∃ i ∈ t, x ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)

Tactic:
⟨y, hy, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(leftRel K) : G → G → Prop)) (Quot.mk (⇑(leftRel K) : G → G → Prop) q)
    (Quot.mk (⇑(leftRel K) : G → G → Prop) x)
refine : x ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
⊢ ∃ i ∈ t, x ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)

Tactic:
refine ⟨y, hy, ?_⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(leftRel K) : G → G → Prop)) (Quot.mk (⇑(leftRel K) : G → G → Prop) q)
    (Quot.mk (⇑(leftRel K) : G → G → Prop) x)
rw : ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * q * y
⊢ x ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)

Tactic:
rw [← doubleCoset_eq_of_mem hq, mem_doubleCoset]

Premises used: DoubleCoset.mem_doubleCoset, DoubleCoset.doubleCoset_eq_of_mem
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(leftRel K) : G → G → Prop)) (Quot.mk (⇑(leftRel K) : G → G → Prop) q)
    (Quot.mk (⇑(leftRel K) : G → G → Prop) x)
obtain :
  ∀ (a' : ↥K.op) (ha' : (fun (m : ↥K.op) ↦ m • x) a' = q), ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * q * y
⊢ ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * q * y

Tactic:
obtain ⟨a', ha'⟩ := Quotient.eq.mp hx

Premises used: Iff.mp, Quotient.eq
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(leftRel K) : G → G → Prop)) (Quot.mk (⇑(leftRel K) : G → G → Prop) q)
    (Quot.mk (⇑(leftRel K) : G → G → Prop) x)
a' : ↥K.op
ha' : (fun (m : ↥K.op) ↦ m • x) a' = q
⊢ (↑a' : Gᵐᵒᵖ)⁻¹ ∈ K.op

Tactic:
simp
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(leftRel K) : G → G → Prop)) (Quot.mk (⇑(leftRel K) : G → G → Prop) q)
    (Quot.mk (⇑(leftRel K) : G → G → Prop) x)
a' : ↥K.op
ha' : (fun (m : ↥K.op) ↦ m • x) a' = q
⊢ x = 1 * q * unop (↑a' : Gᵐᵒᵖ)⁻¹

Tactic:
simpa
    using (eq_mul_inv_of_mul_eq ha')

Premises used: eq_mul_inv_of_mul_eq
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(leftRel K) : G → G → Prop)) (Quot.mk (⇑(leftRel K) : G → G → Prop) q)
    (Quot.mk (⇑(leftRel K) : G → G → Prop) x)
a' : ↥K.op
ha' : (fun (m : ↥K.op) ↦ m • x) a' = q
⊢ ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * q * y

Tactic:
exact ⟨1, one_mem H, MulOpposite.unop a'⁻¹, Subgroup.mem_op.mp (by simp), by simpa
    using (eq_mul_inv_of_mul_eq ha')⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht :
  Subset.{u_1} (α := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop))) Set.univ
    (⋃ i ∈ t, Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G))
contrapose :
  ∀ (ht : ¬Eq.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ),
    ¬Subset.{u_1} (α := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop))) Set.univ
        (⋃ i ∈ t, Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G))
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ

Tactic:
contrapose ht
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : ¬Eq.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
simp :
  Ne.{u_1 + 1} (α := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop)))
    (⋃ i ∈ t, Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) Set.univ
⊢ ¬Subset.{u_1} (α := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop))) Set.univ
      (⋃ i ∈ t, Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G))

Tactic:
simp only [Set.univ_subset_iff, ← ne_eq] at ⊢ ht

Premises used: Set.univ_subset_iff, ne_eq
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
obtain :
  ∀ (x : G) (hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)),
    Ne.{u_1 + 1} (α := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop)))
      (⋃ i ∈ t, Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) Set.univ
⊢ Ne.{u_1 + 1} (α := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop)))
    (⋃ i ∈ t, Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) Set.univ

Tactic:
obtain ⟨x, hx⟩ := (Set.ne_univ_iff_exists_notMem _).mp ht

Premises used: Set.ne_univ_iff_exists_notMem, Iff.mp
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)
⊢ Ne.{u_1 + 1} (α := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop)))
    (⋃ i ∈ t, Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) Set.univ

Tactic:
(Set.ne_univ_iff_exists_notMem _).mpr ⟨Quot.mk (rightRel H) x, ?_⟩

Premises used: Iff.mpr, Set.ne_univ_iff_exists_notMem, Exists.intro, Setoid.r, Quot.mk
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)
refine :
  Quot.mk (⇑(rightRel H) : G → G → Prop) x ∉
    ⋃ i ∈ t, Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)
⊢ Ne.{u_1 + 1} (α := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop)))
    (⋃ i ∈ t, Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) Set.univ

Tactic:
refine (Set.ne_univ_iff_exists_notMem _).mpr ⟨Quot.mk (rightRel H) x, ?_⟩

Premises used: Iff.mpr, Set.ne_univ_iff_exists_notMem, Exists.intro, Setoid.r, Quot.mk
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)
simp :
  ∀ x_1 ∈ t,
    ∀ x_2 ∈ doubleCoset (out x_1) (↑H : Set G) (↑K : Set G),
      ¬Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) x_2)
          (Quot.mk (⇑(rightRel H) : G → G → Prop) x)
⊢ Quot.mk (⇑(rightRel H) : G → G → Prop) x ∉
    ⋃ i ∈ t, Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)

Tactic:
simp only [Set.mem_iUnion, Set.mem_image, exists_prop, not_exists, not_and]

Premises used: Set.mem_iUnion, Set.mem_image, not_exists, exists_prop, not_and
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
hx : x ∉ ⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
contrapose :
  ∀
    (hx :
      Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
        (Quot.mk (⇑(rightRel H) : G → G → Prop) x)),
    Membership.mem (γ := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) x
⊢ ¬Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
      (Quot.mk (⇑(rightRel H) : G → G → Prop) x)

Tactic:
contrapose hx
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
    (Quot.mk (⇑(rightRel H) : G → G → Prop) x)
simp : ∃ i ∈ t, x ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)
⊢ Membership.mem (γ := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) x

Tactic:
simp only [Set.mem_iUnion, exists_prop]

Premises used: Set.mem_iUnion, exists_prop
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
    (Quot.mk (⇑(rightRel H) : G → G → Prop) x)
⊢ ∃ i ∈ t, x ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)

Tactic:
⟨y, hy, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
    (Quot.mk (⇑(rightRel H) : G → G → Prop) x)
refine : x ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
⊢ ∃ i ∈ t, x ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)

Tactic:
refine ⟨y, hy, ?_⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
t : Finset (Quotient (↑H : Set G) (↑K : Set G))
ht : Ne.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
x : G
y : Quotient (↑H : Set G) (↑K : Set G)
hy : y ∈ t
q : G
hq : q ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
hx :
  Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
    (Quot.mk (⇑(rightRel H) : G → G → Prop) x)
rw : ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * q * y
⊢ x ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)

Tactic:
rw [← doubleCoset_eq_of_mem hq, mem_doubleCoset]

Premises used: DoubleCoset.mem_doubleCoset, DoubleCoset.doubleCoset_eq_of_mem