awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
i : Quotient (↑H : Set G) (↑K : Set G)
a : G
hg : mk H K a = mk H K (Quotient.out i)
⊢ a ∈ quotToDoubleCoset H K i

Tactic:
exact mem_doubleCoset.mpr ((eq _ _ _ a).mp hg.symm)

Premises used: Iff.mpr, DoubleCoset.mem_doubleCoset, DoubleCoset.eq, Iff.mp, Eq.symm
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : Quotient (↑H : Set G) (↑K : Set G)
contrapose :
  ¬Disjoint (doubleCoset (Quotient.out a) (↑H : Set G) (↑K : Set G))
        (doubleCoset (Quotient.out b) (↑H : Set G) (↑K : Set G)) →
    a = b
⊢ a ≠ b →
    Disjoint (doubleCoset (Quotient.out a) (↑H : Set G) (↑K : Set G))
      (doubleCoset (Quotient.out b) (↑H : Set G) (↑K : Set G))

Tactic:
contrapose
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : Quotient (↑H : Set G) (↑K : Set G)
h :
  ¬Disjoint (doubleCoset (Quotient.out a) (↑H : Set G) (↑K : Set G))
      (doubleCoset (Quotient.out b) (↑H : Set G) (↑K : Set G))
⊢ a = b

Tactic:
simpa [out_eq'] using mk_eq_of_doubleCoset_eq (eq_of_not_disjoint h)

Premises used: DoubleCoset.eq_of_not_disjoint, DoubleCoset.mk_eq_of_doubleCoset_eq, DoubleCoset.out_eq'
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h :
  ∀ (x : G),
    Membership.mem (γ := Set G) (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)), quotToDoubleCoset H K q) x ↔
      Membership.mem (γ := Set G) Set.univ x
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)), quotToDoubleCoset H K q) Set.univ

Tactic:
ext x
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
x : G
h : ∃ (i : Quotient (↑H : Set G) (↑K : Set G)), ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out i * y
⊢ Membership.mem (γ := Set G) (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)), quotToDoubleCoset H K q) x ↔
    Membership.mem (γ := Set G) Set.univ x

Tactic:
simp only [Set.mem_iUnion, quotToDoubleCoset, mem_doubleCoset, SetLike.mem_coe, Set.mem_univ,
    iff_true]

Premises used: Set.mem_iUnion, iff_true, DoubleCoset.mem_doubleCoset, SetLike.mem_coe, DoubleCoset.quotToDoubleCoset, Set.mem_univ
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
x : G
h : ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out (mk H K x) * y
⊢ ∃ (i : Quotient (↑H : Set G) (↑K : Set G)), ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out i * y

Tactic:
use mk H K x

Premises used: DoubleCoset.mk
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
x : G
h :
  ∀ (h k : G) (h3 : h ∈ H) (h4 : k ∈ K) (h5 : Quotient.out (mk H K x) = h * x * k),
    ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out (mk H K x) * y
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out (mk H K x) * y

Tactic:
obtain ⟨h, k, h3, h4, h5⟩ := mk_out_eq_mul H K x

Premises used: DoubleCoset.mk_out_eq_mul
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out (mk H K x) = h * x * k
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out (mk H K x) * y

Tactic:
⟨h⁻¹, H.inv_mem h3, k⁻¹, K.inv_mem h4, ?_⟩

Premises used: Inv.inv, Subgroup.inv_mem, And.intro, Exists.intro
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out (mk H K x) = h * x * k
h₁ : x = h⁻¹ * Quotient.out (mk H K x) * k⁻¹
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out (mk H K x) * y

Tactic:
refine ⟨h⁻¹, H.inv_mem h3, k⁻¹, K.inv_mem h4, ?_⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
x h k : G
h3 : h ∈ H
h4 : k ∈ K
h5 : Quotient.out (mk H K x) = h * x * k
⊢ x = h⁻¹ * Quotient.out (mk H K x) * k⁻¹

Tactic:
simp only [h5, ← mul_assoc, one_mul, inv_mul_cancel, mul_inv_cancel_right]

Premises used: mul_inv_cancel_right, inv_mul_cancel, mul_assoc, one_mul
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a : G
h :
  ∀ (x : G),
    Membership.mem (γ := Set G) (⋃ (k : ↥K), op (a * (↑k : G)) • (↑H : Set G)) x ↔
      x ∈ doubleCoset a (↑H : Set G) (↑K : Set G)
⊢ ⋃ (k : ↥K), op (a * (↑k : G)) • (↑H : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x : G
h : (∃ (i : ↥K), x * ((↑i : G)⁻¹ * a⁻¹) ∈ H) ↔ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y
⊢ Membership.mem (γ := Set G) (⋃ (k : ↥K), op (a * (↑k : G)) • (↑H : Set G)) x ↔
    x ∈ doubleCoset a (↑H : Set G) (↑K : Set G)

Tactic:
simp only [mem_rightCoset_iff, mul_inv_rev, Set.mem_iUnion, mem_doubleCoset,
    SetLike.mem_coe]

Premises used: Set.mem_iUnion, DoubleCoset.mem_doubleCoset, SetLike.mem_coe, mul_inv_rev, mem_rightCoset_iff
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x : G
h : (∃ (i : ↥K), x * ((↑i : G)⁻¹ * a⁻¹) ∈ H) → ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y
h₁ : (∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y) → ∃ (i : ↥K), x * ((↑i : G)⁻¹ * a⁻¹) ∈ H
⊢ (∃ (i : ↥K), x * ((↑i : G)⁻¹ * a⁻¹) ∈ H) ↔ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y

Tactic:
constructor
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x : G
y : ↥K
h_h : x * ((↑y : G)⁻¹ * a⁻¹) ∈ H
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y

Tactic:
⟨x * (y⁻¹ * a⁻¹), h_h, y, y.2, ?_⟩

Premises used: HMul.hMul, Inv.inv, And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x : G
y : ↥K
h_h : x * ((↑y : G)⁻¹ * a⁻¹) ∈ H
h : x = x * ((↑y⁻¹ : G) * a⁻¹) * a * (↑y : G)
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y

Tactic:
refine ⟨x * (y⁻¹ * a⁻¹), h_h, y, y.2, ?_⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x : G
y : ↥K
h_h : x * ((↑y : G)⁻¹ * a⁻¹) ∈ H
⊢ x = x * ((↑y⁻¹ : G) * a⁻¹) * a * (↑y : G)

Tactic:
simp only [← mul_assoc, inv_mul_cancel_right, InvMemClass.coe_inv]

Premises used: mul_assoc, InvMemClass.coe_inv, inv_mul_cancel_right
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x_1 x : G
hx : x ∈ H
y : G
hy : y ∈ K
hxy : x_1 = x * a * y
⊢ ∃ (i : ↥K), x_1 * ((↑i : G)⁻¹ * a⁻¹) ∈ H

Tactic:
⟨⟨y, hy⟩, ?_⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x_1 x : G
hx : x ∈ H
y : G
hy : y ∈ K
hxy : x_1 = x * a * y
h : x_1 * ((↑(Subtype.mk (p := fun (x : G) ↦ x ∈ K) y hy) : G)⁻¹ * a⁻¹) ∈ H
⊢ ∃ (i : ↥K), x_1 * ((↑i : G)⁻¹ * a⁻¹) ∈ H

Tactic:
refine ⟨⟨y, hy⟩, ?_⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x_1 x : G
hx : x ∈ H
y : G
hy : y ∈ K
hxy : x_1 = x * a * y
⊢ x_1 * ((↑(Subtype.mk (p := fun (x : G) ↦ x ∈ K) y hy) : G)⁻¹ * a⁻¹) ∈ H

Tactic:
simp only [hxy, ← mul_assoc, hx, mul_inv_cancel_right]

Premises used: mul_inv_cancel_right, mul_assoc
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a : G
h :
  ∀ (x : G),
    Membership.mem (γ := Set G) (⋃ (h : ↥H), ((↑h : G) * a) • (↑K : Set G)) x ↔
      x ∈ doubleCoset a (↑H : Set G) (↑K : Set G)
⊢ ⋃ (h : ↥H), ((↑h : G) * a) • (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x : G
h : (∃ (i : ↥H), a⁻¹ * (↑i : G)⁻¹ * x ∈ (↑K : Set G)) ↔ ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * a * y
⊢ Membership.mem (γ := Set G) (⋃ (h : ↥H), ((↑h : G) * a) • (↑K : Set G)) x ↔
    x ∈ doubleCoset a (↑H : Set G) (↑K : Set G)

Tactic:
simp only [mem_leftCoset_iff, mul_inv_rev, Set.mem_iUnion, mem_doubleCoset]

Premises used: mem_leftCoset_iff, Set.mem_iUnion, DoubleCoset.mem_doubleCoset, mul_inv_rev
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x : G
h : (∃ (i : ↥H), a⁻¹ * (↑i : G)⁻¹ * x ∈ (↑K : Set G)) → ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * a * y
h₁ : (∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * a * y) → ∃ (i : ↥H), a⁻¹ * (↑i : G)⁻¹ * x ∈ (↑K : Set G)
⊢ (∃ (i : ↥H), a⁻¹ * (↑i : G)⁻¹ * x ∈ (↑K : Set G)) ↔ ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * a * y

Tactic:
constructor
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x : G
y : ↥H
h_h : a⁻¹ * (↑y : G)⁻¹ * x ∈ (↑K : Set G)
⊢ ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * a * y

Tactic:
⟨y, y.2, a⁻¹ * y⁻¹ * x, h_h, ?_⟩

Premises used: HMul.hMul, Inv.inv, And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x : G
y : ↥H
h_h : a⁻¹ * (↑y : G)⁻¹ * x ∈ (↑K : Set G)
h : x = (↑y : G) * a * (a⁻¹ * (↑y⁻¹ : G) * x)
⊢ ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * a * y

Tactic:
refine ⟨y, y.2, a⁻¹ * y⁻¹ * x, h_h, ?_⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x : G
y : ↥H
h_h : a⁻¹ * (↑y : G)⁻¹ * x ∈ (↑K : Set G)
⊢ x = (↑y : G) * a * (a⁻¹ * (↑y⁻¹ : G) * x)

Tactic:
simp only [← mul_assoc, one_mul, mul_inv_cancel, mul_inv_cancel_right, InvMemClass.coe_inv]

Premises used: mul_inv_cancel_right, mul_assoc, InvMemClass.coe_inv, mul_inv_cancel, one_mul
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x_1 x : G
hx : x ∈ (↑H : Set G)
y : G
hy : y ∈ (↑K : Set G)
hxy : x_1 = x * a * y
⊢ ∃ (i : ↥H), a⁻¹ * (↑i : G)⁻¹ * x_1 ∈ (↑K : Set G)

Tactic:
⟨⟨x, hx⟩, ?_⟩

Premises used: Subtype.mk, Exists.intro
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x_1 x : G
hx : x ∈ (↑H : Set G)
y : G
hy : y ∈ (↑K : Set G)
hxy : x_1 = x * a * y
h : a⁻¹ * (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) x hx) : G)⁻¹ * x_1 ∈ (↑K : Set G)
⊢ ∃ (i : ↥H), a⁻¹ * (↑i : G)⁻¹ * x_1 ∈ (↑K : Set G)

Tactic:
refine ⟨⟨x, hx⟩, ?_⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x_1 x : G
hx : x ∈ (↑H : Set G)
y : G
hy : y ∈ (↑K : Set G)
hxy : x_1 = x * a * y
⊢ a⁻¹ * (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) x hx) : G)⁻¹ * x_1 ∈ (↑K : Set G)

Tactic:
simp only [hxy, ← mul_assoc, hy, one_mul, inv_mul_cancel, inv_mul_cancel_right]

Premises used: inv_mul_cancel, mul_assoc, inv_mul_cancel_right, one_mul
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
e_s : setoid (↑⊥ : Set G) (↑H : Set G) = leftRel H
⊢ _root_.Quotient (setoid (↑⊥ : Set G) (↑H : Set G)) = (G ⧸ H)

Tactic:
congr
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
e_s : ∀ (a b : G), (setoid (↑⊥ : Set G) (↑H : Set G) : G → G → Prop) a b ↔ (leftRel H : G → G → Prop) a b
⊢ setoid (↑⊥ : Set G) (↑H : Set G) = leftRel H

Tactic:
ext
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
⊢ (setoid (↑⊥ : Set G) (↑H : Set G) : G → G → Prop) a b ↔ (leftRel H : G → G → Prop) a b

Tactic:
simp_rw [← bot_rel_eq_leftRel H]

Premises used: DoubleCoset.bot_rel_eq_leftRel
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
e_s : setoid (↑H : Set G) (↑⊥ : Set G) = rightRel H
⊢ _root_.Quotient (setoid (↑H : Set G) (↑⊥ : Set G)) = _root_.Quotient (rightRel H)

Tactic:
congr
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
e_s : ∀ (a b : G), (setoid (↑H : Set G) (↑⊥ : Set G) : G → G → Prop) a b ↔ (rightRel H : G → G → Prop) a b
⊢ setoid (↑H : Set G) (↑⊥ : Set G) = rightRel H

Tactic:
ext
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
⊢ (setoid (↑H : Set G) (↑⊥ : Set G) : G → G → Prop) a b ↔ (rightRel H : G → G → Prop) a b

Tactic:
simp_rw [← rel_bot_eq_right_group_rel H]

Premises used: DoubleCoset.rel_bot_eq_right_group_rel
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
mp :
  Finite.{u_1 + 1} (Quotient (↑H : Set G) (↑K : Set G)) →
    ∃ (I : Finset (Quotient (↑H : Set G) (↑K : Set G))),
      Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ I, quotToDoubleCoset H K i) Set.univ
mpr :
  (∃ (I : Finset (Quotient (↑H : Set G) (↑K : Set G))),
      Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ I, quotToDoubleCoset H K i) Set.univ) →
    Finite.{u_1 + 1} (Quotient (↑H : Set G) (↑K : Set G))
⊢ Finite.{u_1 + 1} (Quotient (↑H : Set G) (↑K : Set G)) ↔
    ∃ (I : Finset (Quotient (↑H : Set G) (↑K : Set G))),
      Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ I, quotToDoubleCoset H K i) Set.univ

Tactic:
constructor
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : Finite.{u_1 + 1} (Quotient (↑H : Set G) (↑K : Set G))
mp :
  ∀ (val : Fintype (Quotient (↑H : Set G) (↑K : Set G))),
    ∃ (I : Finset (Quotient (↑H : Set G) (↑K : Set G))),
      Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ I, quotToDoubleCoset H K i) Set.univ
⊢ ∃ (I : Finset (Quotient (↑H : Set G) (↑K : Set G))),
    Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ I, quotToDoubleCoset H K i) Set.univ

Tactic:
cases nonempty_fintype (Quotient (H : Set G) K)

Premises used: nonempty_fintype, SetLike.coe, DoubleCoset.Quotient
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : Finite.{u_1 + 1} (Quotient (↑H : Set G) (↑K : Set G))
val : Fintype (Quotient (↑H : Set G) (↑K : Set G))
⊢ Eq.{u_1 + 1} (α := Set G)
    (⋃ (i : Quotient (↑H : Set G) (↑K : Set G)),
      ⋃ (_ : Membership.mem (γ := Finset (Quotient (↑H : Set G) (↑K : Set G))) Finset.univ i), quotToDoubleCoset H K i)
    Set.univ

Tactic:
simpa using iUnion_quotToDoubleCoset _ _

Premises used: DoubleCoset.iUnion_quotToDoubleCoset
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : Finite.{u_1 + 1} (Quotient (↑H : Set G) (↑K : Set G))
val : Fintype (Quotient (↑H : Set G) (↑K : Set G))
⊢ ∃ (I : Finset (Quotient (↑H : Set G) (↑K : Set G))),
    Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ I, quotToDoubleCoset H K i) Set.univ

Tactic:
exact ⟨Finset.univ, by simpa using iUnion_quotToDoubleCoset _ _⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
I : Finset (Quotient (↑H : Set G) (↑K : Set G))
hI : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ I, quotToDoubleCoset H K i) Set.univ
this : (↑I : Set (Quotient (↑H : Set G) (↑K : Set G))) = Set.univ
simp_rw : Set.Finite.{u_1} (α := Quotient (↑H : Set G) (↑K : Set G)) Set.univ
simp_rw₁ : (↑I : Set (Quotient (↑H : Set G) (↑K : Set G))).Finite
⊢ Finite.{u_1 + 1} (Quotient (↑H : Set G) (↑K : Set G))

Tactic:
simp_rw [← Set.finite_univ_iff, ← this, I.finite_toSet]

Premises used: Finset.finite_toSet, Set.finite_univ_iff
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
I : Finset (Quotient (↑H : Set G) (↑K : Set G))
hI : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ I, quotToDoubleCoset H K i) Set.univ
mpr : (↑I : Set (Quotient (↑H : Set G) (↑K : Set G))) = Set.univ
⊢ Finite.{u_1 + 1} (Quotient (↑H : Set G) (↑K : Set G))

Tactic:
suffices (I : Set (Quotient (H : Set G) K)) = Set.univ by
      simp_rw [← Set.finite_univ_iff, ← this, I.finite_toSet]
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
I : Finset (Quotient (↑H : Set G) (↑K : Set G))
hI : Eq.{u_1 + 1} (α := Set G) (⋃ i ∈ I, quotToDoubleCoset H K i) Set.univ
mpr :
  ∀ (hI : ∀ (x : G), Membership.mem (γ := Set G) (⋃ i ∈ I, quotToDoubleCoset H K i) x)
    (x : Quotient (↑H : Set G) (↑K : Set G)), x ∈ (↑I : Set (Quotient (↑H : Set G) (↑K : Set G)))
⊢ (↑I : Set (Quotient (↑H : Set G) (↑K : Set G))) = Set.univ

Tactic:
rw [Set.eq_univ_iff_forall] at hI ⊢

Premises used: Set.eq_univ_iff_forall
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
I : Finset (Quotient (↑H : Set G) (↑K : Set G))
hI : ∀ (x : G), Membership.mem (γ := Set G) (⋃ i ∈ I, quotToDoubleCoset H K i) x
x : Quotient (↑H : Set G) (↑K : Set G)
g : G
mpr :
  ∀ (i : Quotient (↑H : Set G) (↑K : Set G)) (hi : i ∈ I) (hT : g ∈ quotToDoubleCoset H K i),
    Quot.mk (⇑(setoid (↑H : Set G) (↑K : Set G)) : G → G → Prop) g ∈ (↑I : Set (Quotient (↑H : Set G) (↑K : Set G)))
⊢ Quot.mk (⇑(setoid (↑H : Set G) (↑K : Set G)) : G → G → Prop) g ∈ (↑I : Set (Quotient (↑H : Set G) (↑K : Set G)))

Tactic:
obtain ⟨_, ⟨i, _, rfl⟩, T, ⟨hi, rfl⟩, hT : g ∈ quotToDoubleCoset H K i⟩ := hI g

Premises used: rfl
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
I : Finset (Quotient (↑H : Set G) (↑K : Set G))
hI : ∀ (x : G), Membership.mem (γ := Set G) (⋃ i ∈ I, quotToDoubleCoset H K i) x
x : Quotient (↑H : Set G) (↑K : Set G)
g : G
i : Quotient (↑H : Set G) (↑K : Set G)
hi : i ∈ I
hT : g ∈ quotToDoubleCoset H K i
⊢ Quot.mk (⇑(setoid (↑H : Set G) (↑K : Set G)) : G → G → Prop) g ∈ (↑I : Set (Quotient (↑H : Set G) (↑K : Set G)))

Tactic:
simpa [← (mem_quotToDoubleCoset_iff _ _).mp hT] using hi

Premises used: Iff.mp, DoubleCoset.mem_quotToDoubleCoset_iff
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)), quotToDoubleCoset H K q) Set.univ

Tactic:
have cover := iUnion_quotToDoubleCoset H K
-- 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
rw :
  ∀ (x : Quot (α := G) (⇑(leftRel K) : G → G → Prop)),
    ∃ (i : Quotient (↑H : Set G) (↑K : Set G)),
      Membership.mem (γ := Set (Quot (α := G) (⇑(leftRel K) : G → G → Prop)))
        (Quot.mk (⇑(leftRel K) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) x
⊢ Eq.{u_1 + 1} (α := Set (Quot (α := G) (⇑(leftRel K) : G → G → Prop)))
    (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)),
      Quot.mk (⇑(leftRel K) : G → G → Prop) '' doubleCoset (out q) (↑H : Set G) (↑K : Set G))
    Set.univ

Tactic:
rw [Set.iUnion_eq_univ_iff]

Premises used: Set.iUnion_eq_univ_iff
-- 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) (⇑(leftRel K) : G → G → Prop)
obtain :
  ∀ (y : G) (hy : ⟦y⟧ = x),
    ∃ (i : Quotient (↑H : Set G) (↑K : Set G)),
      Membership.mem (γ := Set (Quot (α := G) (⇑(leftRel K) : G → G → Prop)))
        (Quot.mk (⇑(leftRel K) : 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) (⇑(leftRel K) : G → G → Prop)))
      (Quot.mk (⇑(leftRel K) : 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) (⇑(leftRel K) : 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) (⇑(leftRel K) : 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) (⇑(leftRel K) : 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) (⇑(leftRel K) : 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) (⇑(leftRel K) : G → G → Prop)))
        (Quot.mk (⇑(leftRel K) : 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) (⇑(leftRel K) : G → G → Prop)))
      (Quot.mk (⇑(leftRel K) : 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) (⇑(leftRel K) : 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) (⇑(leftRel K) : G → G → Prop)))
      (Quot.mk (⇑(leftRel K) : 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) (⇑(leftRel K) : 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) (⇑(leftRel K) : G → G → Prop)))
      (Quot.mk (⇑(leftRel K) : 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
cover : Eq.{u_1 + 1} (α := Set G) (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)), quotToDoubleCoset H K q) Set.univ
rw :
  ∀ (x : Quot (α := G) (⇑(rightRel H) : G → G → Prop)),
    ∃ (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
⊢ Eq.{u_1 + 1} (α := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop)))
    (⋃ (q : Quotient (↑H : Set G) (↑K : Set G)),
      Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out q) (↑H : Set G) (↑K : Set G))
    Set.univ

Tactic:
rw [Set.iUnion_eq_univ_iff]

Premises used: Set.iUnion_eq_univ_iff