awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
m : M
s : ℕ+
this : Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m 1)) (ArchimedeanClass.mk (mk m s))
⊢ Eq (α := ArchimedeanClass (DivisibleHull M))
    (((OrderHom.comp (β := ArchimedeanClass M) (archimedeanClassOrderHom M) (archimedeanClassOrderHomInv M) :
            ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass (DivisibleHull M)) :
          (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M))
        (ArchimedeanClass.mk (mk m s)) :
      ArchimedeanClass (DivisibleHull M))
    ((OrderHom.id : (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M))
        (ArchimedeanClass.mk (mk m s)) :
      ArchimedeanClass (DivisibleHull M))

Tactic:
simpa [archimedeanClassOrderHom, archimedeanClassOrderHomInv]

Premises used: _private.0.DivisibleHull.archimedeanClassOrderHom, _private.0.DivisibleHull.archimedeanClassOrderHomInv
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
m : M
s : ℕ+
h₁ : Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m 1)) (ArchimedeanClass.mk (mk m s))
⊢ Eq (α := ArchimedeanClass (DivisibleHull M))
    (((OrderHom.comp (β := ArchimedeanClass M) (archimedeanClassOrderHom M) (archimedeanClassOrderHomInv M) :
            ArchimedeanClass (DivisibleHull M) →o ArchimedeanClass (DivisibleHull M)) :
          (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M))
        (ArchimedeanClass.mk (mk m s)) :
      ArchimedeanClass (DivisibleHull M))
    ((OrderHom.id : (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass (DivisibleHull M))
        (ArchimedeanClass.mk (mk m s)) :
      ArchimedeanClass (DivisibleHull M))

Tactic:
suffices ArchimedeanClass.mk (mk m 1) = ArchimedeanClass.mk (mk m s) by
      simpa [archimedeanClassOrderHom, archimedeanClassOrderHomInv]
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
h₂ :
  ∀ (a : ArchimedeanClass M),
    Eq (α := ArchimedeanClass M)
      ((OrderHom.comp (archimedeanClassOrderHomInv M) (archimedeanClassOrderHom M) :
            (a : ArchimedeanClass M) → ArchimedeanClass M)
          a :
        ArchimedeanClass M)
      ((OrderHom.id : (a : ArchimedeanClass M) → ArchimedeanClass M) a : ArchimedeanClass M)
⊢ Eq (α := ArchimedeanClass M →o ArchimedeanClass M)
    (OrderHom.comp (archimedeanClassOrderHomInv M) (archimedeanClassOrderHom M)) OrderHom.id

Tactic:
ext a
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : ArchimedeanClass M
h₂ :
  ∀ (a : M),
    Eq (α := ArchimedeanClass M)
      ((OrderHom.comp (archimedeanClassOrderHomInv M) (archimedeanClassOrderHom M) :
            (a : ArchimedeanClass M) → ArchimedeanClass M)
          (ArchimedeanClass.mk a) :
        ArchimedeanClass M)
      ((OrderHom.id : (a : ArchimedeanClass M) → ArchimedeanClass M) (ArchimedeanClass.mk a) : ArchimedeanClass M)
⊢ Eq (α := ArchimedeanClass M)
    ((OrderHom.comp (archimedeanClassOrderHomInv M) (archimedeanClassOrderHom M) :
          (a : ArchimedeanClass M) → ArchimedeanClass M)
        a :
      ArchimedeanClass M)
    ((OrderHom.id : (a : ArchimedeanClass M) → ArchimedeanClass M) a : ArchimedeanClass M)

Tactic:
induction a with | mk _

Premises used: DivisibleHull.mk
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M_1 : Type u_1
inst : AddCommMonoid M_1
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : LinearOrder M
inst_3 : IsOrderedAddMonoid M
a : M
⊢ Eq (α := ArchimedeanClass M)
    ((OrderHom.comp (archimedeanClassOrderHomInv M) (archimedeanClassOrderHom M) :
          (a : ArchimedeanClass M) → ArchimedeanClass M)
        (ArchimedeanClass.mk a) :
      ArchimedeanClass M)
    ((OrderHom.id : (a : ArchimedeanClass M) → ArchimedeanClass M) (ArchimedeanClass.mk a) : ArchimedeanClass M)

Tactic:
simp [archimedeanClassOrderHom, archimedeanClassOrderHomInv]

Premises used: _private.0.DivisibleHull.archimedeanClassOrderHom, _private.0.DivisibleHull.archimedeanClassOrderHomInv
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
a : ArchimedeanClass M
⊢ Eq (α := ArchimedeanClass (DivisibleHull M))
    ((archimedeanClassOrderIso M : (a : ArchimedeanClass M) → ArchimedeanClass (DivisibleHull M)) a :
      ArchimedeanClass (DivisibleHull M))
    (((ArchimedeanClass.orderHom (coeOrderAddMonoidHom M) : ArchimedeanClass M →o ArchimedeanClass (DivisibleHull M)) :
          (a : ArchimedeanClass M) → ArchimedeanClass (DivisibleHull M))
        a :
      ArchimedeanClass (DivisibleHull M))

Tactic:
rfl

Premises used: Quot.map, Quotient.map', rfl
-- Module: Mathlib.GroupTheory.DivisibleHull
Goal:
M : Type u_2
inst : AddCommGroup M
inst_1 : LinearOrder M
inst_2 : IsOrderedAddMonoid M
m : M
s : ℕ+
⊢ Eq (α := ArchimedeanClass M)
    ((OrderIso.symm (archimedeanClassOrderIso M) : (a : ArchimedeanClass (DivisibleHull M)) → ArchimedeanClass M)
        (ArchimedeanClass.mk (mk m s)) :
      ArchimedeanClass M)
    (ArchimedeanClass.mk m : ArchimedeanClass M)

Tactic:
rfl

Premises used: LocalizedModule.liftOn, ArchimedeanClass.lift, DivisibleHull.liftOn, rfl, toAntisymmetrization, ArchimedeanClass.mk
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
α : Type u_2
inst : Mul α
a : α
s t : Set α
simp_rw : s * {a} * t = Set.image2 (fun (x1 x2 : α) ↦ x1 * a * x2) s t
simp_rw₁ : (fun (x : α) ↦ x * a) '' s * t = Set.image2 (fun (x1 x2 : α) ↦ x1 * a * x2) s t
simp_rw₂ :
  Eq (α := Set α) (Set.image2 (fun (x1 x2 : α) ↦ x1 * x2) ((fun (x : α) ↦ x * a) '' s) t)
    (Set.image2 (fun (x1 x2 : α) ↦ x1 * a * x2) s t)
⊢ doubleCoset a s t = Set.image2 (fun (x1 x2 : α) ↦ x1 * a * x2) s t

Tactic:
simp_rw [doubleCoset, Set.mul_singleton, ← Set.image2_mul, Set.image2_image_left]

Premises used: Set.mul_singleton, Set.image2_image_left, Set.image2_mul, DoubleCoset.doubleCoset
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
α : Type u_2
inst : Mul α
s t : Set α
a b : α
⊢ b ∈ doubleCoset a s t ↔ ∃ x ∈ s, ∃ y ∈ t, b = x * a * y

Tactic:
simp only [doubleCoset_eq_image2, Set.mem_image2, eq_comm]

Premises used: DoubleCoset.doubleCoset_eq_image2, Set.mem_image2, eq_comm
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a : G
⊢ a ∈ doubleCoset a (↑H : Set G) (↑K : Set G)

Tactic:
mem_doubleCoset.mpr ⟨1, H.one_mem, 1, K.one_mem, (one_mul a).symm.trans (mul_one (1 * a)).symm⟩

Premises used: Iff.mpr, HMul.hMul, DoubleCoset.mem_doubleCoset, Subgroup.one_mem, And.intro, Exists.intro, mul_one, OfNat.ofNat, Eq.symm, one_mul, Eq.trans
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : G
hb : b ∈ doubleCoset a (↑H : Set G) (↑K : Set G)
obtain :
  ∀ (h : G) (hh : h ∈ (↑H : Set G)) (k : G) (hk : k ∈ (↑K : Set G))
    (hb : h * a * k ∈ doubleCoset a (↑H : Set G) (↑K : Set G)),
    doubleCoset (h * a * k) (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
⊢ doubleCoset b (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)

Tactic:
obtain ⟨h, hh, k, hk, rfl⟩ := mem_doubleCoset.1 hb

Premises used: DoubleCoset.mem_doubleCoset, Iff.mp, rfl
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a h : G
hh : h ∈ (↑H : Set G)
k : G
hk : k ∈ (↑K : Set G)
hb : h * a * k ∈ doubleCoset a (↑H : Set G) (↑K : Set G)
rw : (↑H : Set G) * {h * a * k} * (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
rw₁ : (↑H : Set G) * {h * a * k} * (↑K : Set G) = (↑H : Set G) * {a} * (↑K : Set G)
rw₂ : (↑H : Set G) * HMul.hMul (α := Set G) {h * a} {k} * (↑K : Set G) = (↑H : Set G) * {a} * (↑K : Set G)
rw₃ : (↑H : Set G) * (HMul.hMul (α := Set G) {h} {a} * {k}) * (↑K : Set G) = (↑H : Set G) * {a} * (↑K : Set G)
rw₄ : (↑H : Set G) * (HMul.hMul (α := Set G) {h} {a} * {k} * (↑K : Set G)) = (↑H : Set G) * {a} * (↑K : Set G)
rw₅ : (↑H : Set G) * (HMul.hMul (α := Set G) {h} {a} * ({k} * (↑K : Set G))) = (↑H : Set G) * {a} * (↑K : Set G)
rw₆ : (↑H : Set G) * (HMul.hMul (α := Set G) {h} {a} * (↑K : Set G)) = (↑H : Set G) * {a} * (↑K : Set G)
rw₇ : (↑H : Set G) * HMul.hMul (α := Set G) {h} {a} * (↑K : Set G) = (↑H : Set G) * {a} * (↑K : Set G)
rw₈ : (↑H : Set G) * {h} * {a} * (↑K : Set G) = (↑H : Set G) * {a} * (↑K : Set G)
rw₉ rw₁₀ : (↑H : Set G) * {a} * (↑K : Set G) = (↑H : Set G) * {a} * (↑K : Set G)
⊢ doubleCoset (h * a * k) (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)

Tactic:
rw [doubleCoset, doubleCoset, ← Set.singleton_mul_singleton, ← Set.singleton_mul_singleton,
    mul_assoc, mul_assoc, Subgroup.singleton_mul_subgroup hk, ← mul_assoc, ← mul_assoc,
    Subgroup.subgroup_mul_singleton hh]

Premises used: mul_assoc, Subgroup.subgroup_mul_singleton, Subgroup.singleton_mul_subgroup, DoubleCoset.doubleCoset, Set.singleton_mul_singleton
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doubleCoset a (↑H : Set G) (↑K : Set G)) (doubleCoset b (↑H : Set G) (↑K : Set G))
⊢ ∃ x ∈ doubleCoset a (↑H : Set G) (↑K : Set G), x ∈ doubleCoset b (↑H : Set G) (↑K : Set G)

Tactic:
rw [Set.not_disjoint_iff] at h

Premises used: Set.not_disjoint_iff
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : G
h : ∃ x ∈ doubleCoset a (↑H : Set G) (↑K : Set G), x ∈ doubleCoset b (↑H : Set G) (↑K : Set G)
simp :
  ∀
    (h :
      ∃ (x : G),
        (∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * a * y) ∧
          ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * b * y),
    ∃ x ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), b = x * a * y
⊢ b ∈ doubleCoset a (↑H : Set G) (↑K : Set G)

Tactic:
simp only [mem_doubleCoset] at *

Premises used: DoubleCoset.mem_doubleCoset
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : G
h :
  ∃ (x : G),
    (∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * a * y) ∧
      ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * b * y
obtain :
  ∀ (l : G) (hl : l ∈ (↑H : Set G)) (r : G) (hr : r ∈ (↑K : Set G)) (y : G) (hy : y ∈ (↑H : Set G)) (r' : G)
    (hr' : r' ∈ (↑K : Set G)) (hrx : y * b * r' = l * a * r), ∃ x ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), b = x * a * y
⊢ ∃ x ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), b = x * a * y

Tactic:
obtain ⟨x, ⟨l, hl, r, hr, hrx⟩, y, hy, ⟨r', hr', rfl⟩⟩ := h

Premises used: rfl
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b l : G
hl : l ∈ (↑H : Set G)
r : G
hr : r ∈ (↑K : Set G)
y : G
hy : y ∈ (↑H : Set G)
r' : G
hr' : r' ∈ (↑K : Set G)
hrx : y * b * r' = l * a * r
⊢ ∃ x ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), b = x * a * y

Tactic:
⟨y⁻¹ * l, H.mul_mem (H.inv_mem hy) hl, r * r'⁻¹, K.mul_mem hr (K.inv_mem hr'), ?_⟩

Premises used: HMul.hMul, Inv.inv, Subgroup.inv_mem, And.intro, Exists.intro, Subgroup.mul_mem
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b l : G
hl : l ∈ (↑H : Set G)
r : G
hr : r ∈ (↑K : Set G)
y : G
hy : y ∈ (↑H : Set G)
r' : G
hr' : r' ∈ (↑K : Set G)
hrx : y * b * r' = l * a * r
refine : b = y⁻¹ * l * a * (r * r'⁻¹)
⊢ ∃ x ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), b = x * a * y

Tactic:
refine ⟨y⁻¹ * l, H.mul_mem (H.inv_mem hy) hl, r * r'⁻¹, K.mul_mem hr (K.inv_mem hr'), ?_⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b l : G
hl : l ∈ (↑H : Set G)
r : G
hr : r ∈ (↑K : Set G)
y : G
hy : y ∈ (↑H : Set G)
r' : G
hr' : r' ∈ (↑K : Set G)
hrx : y * b * r' = l * a * r
rwa : b = y⁻¹ * l * (a * (r * r'⁻¹))
rwa₁ : b = y⁻¹ * (l * (a * (r * r'⁻¹)))
rwa₂ : y * b = l * (a * (r * r'⁻¹))
rwa₃ : y * b = l * a * (r * r'⁻¹)
rwa₄ : y * b = l * a * r * r'⁻¹
rwa₅ rwa₆ rwa₇ rwa₈ : y * b * r' = l * a * r
⊢ b = y⁻¹ * l * a * (r * r'⁻¹)

Tactic:
rwa [mul_assoc, mul_assoc, eq_inv_mul_iff_mul_eq, ← mul_assoc, ← mul_assoc, eq_mul_inv_iff_mul_eq]

Premises used: mul_assoc, eq_inv_mul_iff_mul_eq, eq_mul_inv_iff_mul_eq
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doubleCoset a (↑H : Set G) (↑K : Set G)) (doubleCoset b (↑H : Set G) (↑K : Set G))
⊢ ¬Disjoint (doubleCoset b (↑H : Set G) (↑K : Set G)) (doubleCoset a (↑H : Set G) (↑K : Set G))

Tactic:
rw [disjoint_comm] at h

Premises used: disjoint_comm
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doubleCoset b (↑H : Set G) (↑K : Set G)) (doubleCoset a (↑H : Set G) (↑K : Set G))
⊢ a ∈ doubleCoset b (↑H : Set G) (↑K : Set G)

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

Tactic:
apply doubleCoset_eq_of_mem ha

Premises used: DoubleCoset.doubleCoset_eq_of_mem
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
x y : G
⊢ (setoid (↑H : Set G) (↑K : Set G) : G → G → Prop) x y ↔ ∃ a ∈ H, ∃ b ∈ K, y = a * x * b

Tactic:
Iff.trans
    ⟨fun (hxy : doubleCoset x H K = doubleCoset y H K) => hxy ▸ mem_doubleCoset_self H K y,
      fun hxy => (doubleCoset_eq_of_mem hxy).symm⟩ mem_doubleCoset

Premises used: DoubleCoset.mem_doubleCoset, Iff.intro, Iff.trans, DoubleCoset.doubleCoset_eq_of_mem, Eq.symm
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : ∀ (a b : G), (setoid (↑⊥ : Set G) (↑H : Set G) : G → G → Prop) a b ↔ (QuotientGroup.leftRel H : G → G → Prop) a b
⊢ Eq.{u_1 + 1} (α := G → G → Prop) (⇑(setoid (↑⊥ : Set G) (↑H : Set G)) : G → G → Prop)
    (⇑(QuotientGroup.leftRel H) : G → G → Prop)

Tactic:
ext a b
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
h : (∃ (a_1 : G), Membership.mem (γ := Subgroup G) ⊥ a_1 ∧ ∃ b_1 ∈ H, b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H
⊢ (setoid (↑⊥ : Set G) (↑H : Set G) : G → G → Prop) a b ↔ (QuotientGroup.leftRel H : G → G → Prop) a b

Tactic:
rw [rel_iff, QuotientGroup.leftRel_apply]

Premises used: DoubleCoset.rel_iff, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
h : (∃ (a_1 : G), Membership.mem (γ := Subgroup G) ⊥ a_1 ∧ ∃ b_1 ∈ H, b = a_1 * a * b_1) → a⁻¹ * b ∈ H
h₁ : a⁻¹ * b ∈ H → ∃ (a_2 : G), Membership.mem (γ := Subgroup G) ⊥ a_2 ∧ ∃ b_1 ∈ H, b = a_2 * a * b_1
⊢ (∃ (a_1 : G), Membership.mem (γ := Subgroup G) ⊥ a_1 ∧ ∃ b_1 ∈ H, b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H

Tactic:
constructor
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
hb : b ∈ H
h : a⁻¹ * (a * b) ∈ H
h₁ h₂ h₃ h₄ : b ∈ H
⊢ a⁻¹ * (1 * a * b) ∈ H

Tactic:
rwa [one_mul, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, one_mul
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
rw : b = a * (a⁻¹ * b)
rw₁ rw₂ : b = b
⊢ b = 1 * a * (a⁻¹ * b)

Tactic:
rw [one_mul, mul_inv_cancel_left]

Premises used: mul_inv_cancel_left, one_mul
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ ∃ (a_1 : G), Membership.mem (γ := Subgroup G) ⊥ a_1 ∧ ∃ b_1 ∈ H, b = a_1 * a * b_1

Tactic:
exact ⟨1, rfl, a⁻¹ * b, h, by rw [one_mul, mul_inv_cancel_left]⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
h : ∀ (a b : G), (setoid (↑H : Set G) (↑⊥ : Set G) : G → G → Prop) a b ↔ (QuotientGroup.rightRel H : G → G → Prop) a b
⊢ Eq.{u_1 + 1} (α := G → G → Prop) (⇑(setoid (↑H : Set G) (↑⊥ : Set G)) : G → G → Prop)
    (⇑(QuotientGroup.rightRel H) : G → G → Prop)

Tactic:
ext a b
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
h : (∃ a_1 ∈ H, ∃ (b_1 : G), Membership.mem (γ := Subgroup G) ⊥ b_1 ∧ b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H
⊢ (setoid (↑H : Set G) (↑⊥ : Set G) : G → G → Prop) a b ↔ (QuotientGroup.rightRel H : G → G → Prop) a b

Tactic:
rw [rel_iff, QuotientGroup.rightRel_apply]

Premises used: QuotientGroup.rightRel_apply, DoubleCoset.rel_iff
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
h : (∃ a_1 ∈ H, ∃ (b_1 : G), Membership.mem (γ := Subgroup G) ⊥ b_1 ∧ b = a_1 * a * b_1) → b * a⁻¹ ∈ H
h₁ : b * a⁻¹ ∈ H → ∃ a_2 ∈ H, ∃ (b_1 : G), Membership.mem (γ := Subgroup G) ⊥ b_1 ∧ b = a_2 * a * b_1
⊢ (∃ a_1 ∈ H, ∃ (b_1 : G), Membership.mem (γ := Subgroup G) ⊥ b_1 ∧ b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H

Tactic:
constructor
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
hb : b ∈ H
h : b * a * a⁻¹ ∈ H
h₁ h₂ h₃ h₄ : b ∈ H
⊢ b * a * 1 * a⁻¹ ∈ H

Tactic:
rwa [mul_one, mul_inv_cancel_right]

Premises used: mul_inv_cancel_right, mul_one
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
h : b * a⁻¹ ∈ H
rw : b = b * a⁻¹ * a
rw₁ rw₂ : b = b
⊢ b = b * a⁻¹ * a * 1

Tactic:
rw [mul_one, inv_mul_cancel_right]

Premises used: mul_one, inv_mul_cancel_right
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
h : b * a⁻¹ ∈ H
⊢ ∃ a_1 ∈ H, ∃ (b_1 : G), Membership.mem (γ := Subgroup G) ⊥ b_1 ∧ b = a_1 * a * b_1

Tactic:
exact ⟨b * a⁻¹, h, 1, rfl, by rw [mul_one, inv_mul_cancel_right]⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
a b : G
H K : Subgroup G
⊢ mk H K a = mk H K b ↔ (setoid (↑H : Set G) (↑K : Set G) : G → G → Prop) a b

Tactic:
Quotient.eq

Premises used: Quotient.eq, DoubleCoset.Quotient
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : G
rw : (setoid (↑H : Set G) (↑K : Set G) : G → G → Prop) a b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k
⊢ mk H K a = mk H K b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Tactic:
rw [eq'']

Premises used: DoubleCoset.eq''
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : G
⊢ (setoid (↑H : Set G) (↑K : Set G) : G → G → Prop) a b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Tactic:
rel_iff

Premises used: DoubleCoset.rel_iff
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : G
⊢ (setoid (↑H : Set G) (↑K : Set G) : G → G → Prop) a b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Tactic:
exact rel_iff

Premises used: DoubleCoset.rel_iff
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
q : Quotient (↑H : Set G) (↑K : Set G)
⊢ mk H K (Quotient.out q) = q

Tactic:
Quotient.out_eq' q

Premises used: Quotient.out_eq', DoubleCoset.Quotient
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
g : G
⊢ mk H K (Quotient.out (mk H K g)) = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k

Tactic:
have := eq H K (mk H K g : Quotient ↑H ↑K).out g
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
g : G
this : mk H K (Quotient.out (mk H K g)) = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
⊢ mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k

Tactic:
rw [out_eq'] at this

Premises used: DoubleCoset.out_eq'
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
obtain :
  ∀ (h : G) (h_h : h ∈ H) (k : G) (hk : k ∈ K) (T : g = h * Quotient.out (mk H K g) * k),
    ∃ (h : G) (k : G), h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k
⊢ ∃ (h : G) (k : G), h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k

Tactic:
obtain ⟨h, h_h, k, hk, T⟩ := this.1 rfl

Premises used: Iff.mp, rfl
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
h : G
h_h : h ∈ H
k : G
hk : k ∈ K
T : g = h * Quotient.out (mk H K g) * k
⊢ ∃ (h : G) (k : G), h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k

Tactic:
⟨h⁻¹, k⁻¹, H.inv_mem h_h, K.inv_mem hk, eq_mul_inv_of_mul_eq (eq_inv_mul_of_mul_eq ?_)⟩

Premises used: eq_mul_inv_of_mul_eq, eq_inv_mul_of_mul_eq, 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
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
h : G
h_h : h ∈ H
k : G
hk : k ∈ K
T : g = h * Quotient.out (mk H K g) * k
refine : h * (Quotient.out (mk H K g) * k) = g
⊢ ∃ (h : G) (k : G), h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k

Tactic:
refine ⟨h⁻¹, k⁻¹, H.inv_mem h_h, K.inv_mem hk, eq_mul_inv_of_mul_eq (eq_inv_mul_of_mul_eq ?_)⟩
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
g : G
this : mk H K g = mk H K g ↔ ∃ h ∈ H, ∃ k ∈ K, g = h * Quotient.out (mk H K g) * k
h : G
h_h : h ∈ H
k : G
hk : k ∈ K
T : g = h * Quotient.out (mk H K g) * k
rw : h * Quotient.out (mk H K g) * k = g
rw₁ rw₂ : g = g
⊢ h * (Quotient.out (mk H K g) * k) = g

Tactic:
rw [← mul_assoc, ← T]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : G
h : doubleCoset a (↑H : Set G) (↑K : Set G) = doubleCoset b (↑H : Set G) (↑K : Set G)
rw : ∃ h ∈ H, ∃ k ∈ K, b = h * a * k
⊢ mk H K a = mk H K b

Tactic:
rw [eq]

Premises used: DoubleCoset.eq
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : G
h : doubleCoset a (↑H : Set G) (↑K : Set G) = doubleCoset b (↑H : Set G) (↑K : Set G)
⊢ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Tactic:
mem_doubleCoset.mp (h.symm ▸ mem_doubleCoset_self H K b)

Premises used: DoubleCoset.mem_doubleCoset_self, DoubleCoset.mem_doubleCoset, Eq.rec, Iff.mp, Eq.symm
-- Module: Mathlib.GroupTheory.DoubleCoset
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : G
h : doubleCoset a (↑H : Set G) (↑K : Set G) = doubleCoset b (↑H : Set G) (↑K : Set G)
⊢ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Tactic:
exact mem_doubleCoset.mp (h.symm ▸ mem_doubleCoset_self H K b)

Premises used: DoubleCoset.mem_doubleCoset, Iff.mp
-- 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 : a ∈ quotToDoubleCoset H K i
⊢ mk H K a = i

Tactic:
simp [mk_eq_of_doubleCoset_eq (doubleCoset_eq_of_mem hg)]

Premises used: DoubleCoset.mk_eq_of_doubleCoset_eq, DoubleCoset.doubleCoset_eq_of_mem
-- 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
refine : ∀ (hg : mk H K a = i), a ∈ quotToDoubleCoset H K i
⊢ a ∈ quotToDoubleCoset H K i ↔ mk H K a = i

Tactic:
refine ⟨fun hg ↦ by simp [mk_eq_of_doubleCoset_eq (doubleCoset_eq_of_mem hg)], fun hg ↦ ?_⟩
-- 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 = i
⊢ mk H K a = mk H K (Quotient.out i)

Tactic:
rw [← out_eq' _ _ i] at hg

Premises used: DoubleCoset.out_eq'
-- 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:
mem_doubleCoset.mpr ((eq _ _ _ a).mp hg.symm)

Premises used: Iff.mpr, Set.Mem, DoubleCoset.mem_doubleCoset, DoubleCoset.quotToDoubleCoset, DoubleCoset.eq, Iff.mp, Eq.symm