awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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 : ℕ+
⊢ 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))
have h₁ : Eq (α := ArchimedeanClass (DivisibleHull M)) (ArchimedeanClass.mk (mk m 1)) (ArchimedeanClass.mk (mk m s))
Tactic: suffices ArchimedeanClass.mk (mk m 1) = ArchimedeanClass.mk (mk m s) by
      simpa [archimedeanClassOrderHom, archimedeanClassOrderHomInv]
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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
⊢ Eq (α := ArchimedeanClass M →o ArchimedeanClass M)
    (OrderHom.comp (archimedeanClassOrderHomInv M) (archimedeanClassOrderHom M)) OrderHom.id
have 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)
Tactic: ext a
-- Lean 4 proof step from Mathlib.GroupTheory.DivisibleHull (goal)
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
⊢ 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)
have 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)
Tactic: induction a with | mk _
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
α : Type u_2
inst : Mul α
a : α
s t : Set α
⊢ doubleCoset a s t = Set.image2 (fun (x1 x2 : α) ↦ x1 * a * x2) s t
have simp_rw : s * {a} * 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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ doubleCoset a s t = Set.image2 (fun (x1 x2 : α) ↦ x1 * a * x2) s t
have simp_rw₁ : (fun (x : α) ↦ x * 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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ doubleCoset a s t = Set.image2 (fun (x1 x2 : α) ↦ x1 * a * x2) s t
have 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)
Tactic: simp_rw [doubleCoset, Set.mul_singleton, ← Set.image2_mul, Set.image2_image_left]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ doubleCoset b (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
have 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)
Tactic: obtain ⟨h, hh, k, hk, rfl⟩ := mem_doubleCoset.1 hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ doubleCoset (h * a * k) (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
have rw : (↑H : Set G) * {h * a * k} * (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ doubleCoset (h * a * k) (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
have rw₁ : (↑H : Set G) * {h * a * k} * (↑K : Set G) = (↑H : Set G) * {a} * (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ doubleCoset (h * a * k) (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
have rw₂ : (↑H : Set G) * HMul.hMul (α := Set G) {h * a} {k} * (↑K : Set G) = (↑H : Set G) * {a} * (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ doubleCoset (h * a * k) (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
have rw₃ : (↑H : Set G) * (HMul.hMul (α := Set G) {h} {a} * {k}) * (↑K : Set G) = (↑H : Set G) * {a} * (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ doubleCoset (h * a * k) (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
have rw₄ : (↑H : Set G) * (HMul.hMul (α := Set G) {h} {a} * {k} * (↑K : Set G)) = (↑H : Set G) * {a} * (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ doubleCoset (h * a * k) (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
have rw₅ : (↑H : Set G) * (HMul.hMul (α := Set G) {h} {a} * ({k} * (↑K : Set G))) = (↑H : Set G) * {a} * (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ doubleCoset (h * a * k) (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
have rw₆ : (↑H : Set G) * (HMul.hMul (α := Set G) {h} {a} * (↑K : Set G)) = (↑H : Set G) * {a} * (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ doubleCoset (h * a * k) (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
have rw₇ : (↑H : Set G) * HMul.hMul (α := Set G) {h} {a} * (↑K : Set G) = (↑H : Set G) * {a} * (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ doubleCoset (h * a * k) (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
have rw₈ : (↑H : Set G) * {h} * {a} * (↑K : Set G) = (↑H : Set G) * {a} * (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ doubleCoset (h * a * k) (↑H : Set G) (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
have rw₉ : (↑H : Set G) * {a} * (↑K : Set G) = (↑H : Set G) * {a} * (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (hypothesis)
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))
⊢ b ∈ doubleCoset a (↑H : Set G) (↑K : Set G)
have h₁ : ∃ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ b ∈ doubleCoset a (↑H : Set G) (↑K : Set G)
have 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
Tactic: simp only [mem_doubleCoset] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ ∃ x ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), b = x * a * y
have 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
Tactic: obtain ⟨x, ⟨l, hl, r, hr, hrx⟩, y, hy, ⟨r', hr', rfl⟩⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
have refine : b = y⁻¹ * l * a * (r * r'⁻¹)
Tactic: refine ⟨y⁻¹ * l, H.mul_mem (H.inv_mem hy) hl, r * r'⁻¹, K.mul_mem hr (K.inv_mem hr'), ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ b = y⁻¹ * l * a * (r * r'⁻¹)
have rwa : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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'⁻¹))
⊢ b = y⁻¹ * l * a * (r * r'⁻¹)
have rwa₁ : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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'⁻¹)))
⊢ b = y⁻¹ * l * a * (r * r'⁻¹)
have rwa₂ : y * b = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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'⁻¹))
⊢ b = y⁻¹ * l * a * (r * r'⁻¹)
have rwa₃ : y * b = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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'⁻¹)
⊢ b = y⁻¹ * l * a * (r * r'⁻¹)
have rwa₄ : y * b = 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]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (hypothesis)
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))
⊢ doubleCoset a (↑H : Set G) (↑K : Set G) = doubleCoset b (↑H : Set G) (↑K : Set G)
have h₁ : ¬Disjoint (doubleCoset b (↑H : Set G) (↑K : Set G)) (doubleCoset a (↑H : Set G) (↑K : Set G))
Tactic: rw [disjoint_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (hypothesis)
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))
⊢ doubleCoset a (↑H : Set G) (↑K : Set G) = doubleCoset b (↑H : Set G) (↑K : Set G)
have ha : a ∈ doubleCoset b (↑H : Set G) (↑K : Set G)
Tactic: have ha : a ∈ doubleCoset b H K := mem_doubleCoset_of_not_disjoint h
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Eq.{u_1 + 1} (α := G → G → Prop) (⇑(setoid (↑⊥ : Set G) (↑H : Set G)) : G → G → Prop)
    (⇑(QuotientGroup.leftRel H) : G → G → Prop)
have h : ∀ (a b : G), (setoid (↑⊥ : Set G) (↑H : Set G) : G → G → Prop) a b ↔ (QuotientGroup.leftRel H : G → G → Prop) a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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 ↔ (QuotientGroup.leftRel H : G → G → Prop) a b
have h : (∃ (a_1 : G), Membership.mem (γ := Subgroup G) ⊥ a_1 ∧ ∃ b_1 ∈ H, b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H
Tactic: rw [rel_iff, QuotientGroup.leftRel_apply]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
⊢ (∃ (a_1 : G), Membership.mem (γ := Subgroup G) ⊥ a_1 ∧ ∃ b_1 ∈ H, b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H
have h : (∃ (a_1 : G), Membership.mem (γ := Subgroup G) ⊥ a_1 ∧ ∃ b_1 ∈ H, b = a_1 * a * b_1) → a⁻¹ * b ∈ H
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ (∃ (a_1 : G), Membership.mem (γ := Subgroup G) ⊥ a_1 ∧ ∃ b_1 ∈ H, b = a_1 * a * b_1) ↔ a⁻¹ * b ∈ H
have h₁ : a⁻¹ * b ∈ H → ∃ (a_2 : G), Membership.mem (γ := Subgroup G) ⊥ a_2 ∧ ∃ b_1 ∈ H, b = a_2 * a * b_1
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
hb : b ∈ H
⊢ a⁻¹ * (1 * a * b) ∈ H
have h : a⁻¹ * (a * b) ∈ H
Tactic: rwa [one_mul, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
⊢ b = 1 * a * (a⁻¹ * b)
have rw : b = a * (a⁻¹ * b)
Tactic: rw [one_mul, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
h : a⁻¹ * b ∈ H
rw : b = a * (a⁻¹ * b)
⊢ b = 1 * a * (a⁻¹ * b)
have rw₁ : b = b
Tactic: rw [one_mul, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ Eq.{u_1 + 1} (α := G → G → Prop) (⇑(setoid (↑H : Set G) (↑⊥ : Set G)) : G → G → Prop)
    (⇑(QuotientGroup.rightRel H) : G → G → Prop)
have h : ∀ (a b : G), (setoid (↑H : Set G) (↑⊥ : Set G) : G → G → Prop) a b ↔ (QuotientGroup.rightRel H : G → G → Prop) a b
Tactic: ext a b
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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 ↔ (QuotientGroup.rightRel H : G → G → Prop) a b
have h : (∃ a_1 ∈ H, ∃ (b_1 : G), Membership.mem (γ := Subgroup G) ⊥ b_1 ∧ b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H
Tactic: rw [rel_iff, QuotientGroup.rightRel_apply]