awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)), y ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)
have 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
Tactic: contrapose cover
Cleared hypotheses: cover
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)),
    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
have 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
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⟩
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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))
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
have 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))
Tactic: contrapose ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ ¬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))
have 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
Tactic: simp only [Set.univ_subset_iff, ← ne_eq] at ⊢ ht
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨x, hx⟩ := (Set.ne_univ_iff_exists_notMem _).mp ht
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
have 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)
Tactic: refine (Set.ne_univ_iff_exists_notMem _).mpr ⟨Quot.mk (leftRel K) x, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ 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)
have 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)
Tactic: simp only [Set.mem_iUnion, Set.mem_image, exists_prop, not_exists, not_and]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ ¬Eq (α := Quot (α := G) (⇑(leftRel K) : G → G → Prop)) (Quot.mk (⇑(leftRel K) : G → G → Prop) q)
      (Quot.mk (⇑(leftRel K) : G → G → Prop) x)
have 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
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ Membership.mem (γ := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) x
have simp : ∃ i ∈ t, x ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)
Tactic: simp only [Set.mem_iUnion, exists_prop]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
have refine : x ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
Tactic: refine ⟨y, hy, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ x ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
have rw : ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * q * y
Tactic: rw [← doubleCoset_eq_of_mem hq, mem_doubleCoset]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * q * y
have 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
Tactic: obtain ⟨a', ha'⟩ := Quotient.eq.mp hx
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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))
⊢ Eq.{u_1 + 1} (α := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) Set.univ
have 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))
Tactic: contrapose ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ ¬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))
have 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
Tactic: simp only [Set.univ_subset_iff, ← ne_eq] at ⊢ ht
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ 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
have 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
Tactic: obtain ⟨x, hx⟩ := (Set.ne_univ_iff_exists_notMem _).mp ht
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
have 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)
Tactic: refine (Set.ne_univ_iff_exists_notMem _).mpr ⟨Quot.mk (rightRel H) x, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ 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)
have 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)
Tactic: simp only [Set.mem_iUnion, Set.mem_image, exists_prop, not_exists, not_and]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ ¬Eq (α := Quot (α := G) (⇑(rightRel H) : G → G → Prop)) (Quot.mk (⇑(rightRel H) : G → G → Prop) q)
      (Quot.mk (⇑(rightRel H) : G → G → Prop) x)
have 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
Tactic: contrapose hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ Membership.mem (γ := Set G) (⋃ q ∈ t, doubleCoset (out q) (↑H : Set G) (↑K : Set G)) x
have simp : ∃ i ∈ t, x ∈ doubleCoset (out i) (↑H : Set G) (↑K : Set G)
Tactic: simp only [Set.mem_iUnion, exists_prop]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
have refine : x ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
Tactic: refine ⟨y, hy, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ x ∈ doubleCoset (out y) (↑H : Set G) (↑K : Set G)
have rw : ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * q * y
Tactic: rw [← doubleCoset_eq_of_mem hq, mem_doubleCoset]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ ∃ (a : ↥H), x = (↑a : G) * q
have obtain : ∀ (a : ↥H) (ha : (↑a : G) * x = q), ∃ (a : ↥H), x = (↑a : G) * q
Tactic: obtain ⟨a, ha⟩ : ∃ a : H, a * x = q := Quotient.eq.mp hx
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
⊢ ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * q * y
have obtain : ∀ (a : ↥H) (ha : x = (↑a : G) * q), ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * q * y
Tactic: obtain ⟨a, ha⟩ : ∃ a : H, x = a * q := by
    obtain ⟨a, ha⟩ : ∃ a : H, a * x = q := Quotient.eq.mp hx
    exact ⟨⟨a⁻¹, by simp⟩, eq_inv_mul_of_mul_eq ha⟩
-- Lean 4 proof step from Mathlib.GroupTheory.EckmannHilton (goal)
Goal:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
⊢ m₁ = m₂
have h : ∀ (a b : X), m₁ a b = m₂ a b
Tactic: funext a b
-- Lean 4 proof step from Mathlib.GroupTheory.EckmannHilton (goal)
Goal:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
⊢ m₁ a b = m₂ a b
have m₃ : m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b)
Tactic: calc
    m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b) := by
      { simp only [one h₁ h₂ distrib, h₂.left_id, h₂.right_id] }
    _ = m₂ a b := by simp only [distrib, h₁.left_id, h₁.right_id]
-- Lean 4 proof step from Mathlib.GroupTheory.EckmannHilton (goal)
Goal:
X : Type u
m₁ m₂ : X → X → X
e₁ e₂ : X
h₁ : IsUnital m₁ e₁
h₂ : IsUnital m₂ e₂
distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
a b : X
m₃ : m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b)
⊢ m₁ a b = m₂ a b
have m₄ : m₁ (m₂ a e₁) (m₂ e₁ b) = m₂ a b
Tactic: calc
    m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b) := by
      { simp only [one h₁ h₂ distrib, h₂.left_id, h₂.right_id] }
    _ = m₂ a b := by simp only [distrib, h₁.left_id, h₁.right_id]
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
⊢ Eq (α := ℕ)
    (if h : ∃ (n : ℕ), 0 < n ∧ ∀ (g : Gᵐᵒᵖ), g ^ n = 1 then
      Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : Gᵐᵒᵖ), g ^ n = 1) h
    else 0)
    (if h : ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1 then Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h
    else 0)
have h₂ : (∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
    (h₁ : b = c) (h₂ : ∀ (h : c), x_1 sorry = u h) (h₃ : ∀ (h : ¬c), y sorry = v h), dite b x_1 y = dite c u v) →
  (∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1) → ∀ (x : ℕ), (∀ (g : Gᵐᵒᵖ), g ^ x = 1) ↔ ∀ (g : G), g ^ x = 1
Tactic: congr!
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h₂ :
  (∀ {b c : Prop} {α : Type} {x : Decidable b} [inst : Decidable c] {x_1 : b → α} {u : c → α} {y : ¬b → α} {v : ¬c → α}
      (h₁ : b = c) (h₂ : ∀ (h : c), x_1 ⋯ = u h) (h₃ : ∀ (h : ¬c), y ⋯ = v h), dite b x_1 y = dite c u v) →
    (∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1) → ∀ (x : ℕ), (∀ (g : Gᵐᵒᵖ), g ^ x = 1) ↔ ∀ (g : G), g ^ x = 1
⊢ Eq (α := ℕ)
    (if h : ∃ (n : ℕ), 0 < n ∧ ∀ (g : Gᵐᵒᵖ), g ^ n = 1 then
      Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : Gᵐᵒᵖ), g ^ n = 1) h
    else 0)
    (if h : ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1 then Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h
    else 0)
have h₁ : ∀ (x : ℕ), (∀ (g : Gᵐᵒᵖ), g ^ x = 1) ↔ ∀ (g : G), g ^ x = 1
Tactic: congr!
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ExponentExists G
g : G
⊢ ∃ (n : ℕ), 0 < n ∧ g ^ n = 1
have h₁ : ∀ (n : ℕ), 0 < n → ∀ (this : ∀ (g : G), g ^ n = 1), g ^ n = 1
Tactic: peel 2 h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
⊢ Ne (α := ℕ) (if h : ExponentExists G then Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h else 0) 0 ↔
    ExponentExists G
have pos : ∀ (h : ExponentExists G), Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h ≠ 0 ↔ ExponentExists G
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
pos : ∀ (h : ExponentExists G), Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h ≠ 0 ↔ ExponentExists G
⊢ Ne (α := ℕ) (if h : ExponentExists G then Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h else 0) 0 ↔
    ExponentExists G
have neg : ∀ (h : ¬ExponentExists G), Ne (α := ℕ) 0 0 ↔ ExponentExists G
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ¬ExponentExists G
⊢ Ne (α := ℕ) 0 0 ↔ ExponentExists G
have neg : Ne (α := ℕ) 0 0 → ExponentExists G
Tactic: tauto
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ¬ExponentExists G
neg : Ne (α := ℕ) 0 0 → ExponentExists G
⊢ Ne (α := ℕ) 0 0 ↔ ExponentExists G
have neg₁ : ExponentExists G → Ne (α := ℕ) 0 0
Tactic: tauto
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
⊢ exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
have pos : ∀ (h : ExponentExists G), exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
Tactic: by_cases h : Monoid.ExponentExists G
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
pos : ∀ (h : ExponentExists G), exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
⊢ exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
have neg : ∀ (h : ¬ExponentExists G), exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
Tactic: by_cases h : Monoid.ExponentExists G
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
h : ExponentExists G
⊢ exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
have h' : Set.Nonempty (α := ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
Tactic: have h' : {d : ℕ | 0 < d ∧ ∀ x : G, x ^ d = 1}.Nonempty := h
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ExponentExists G
h' : Set.Nonempty (α := ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
⊢ exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
have pos : Nat.find (p := fun (n : ℕ) ↦ 0 < n ∧ ∀ (g : G), g ^ n = 1) h =
  Nat.find (p := fun (n : ℕ) ↦ Membership.mem (γ := Set ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1} n) h'
Tactic: rw [Monoid.exponent, dif_pos h, Nat.sInf_def h']
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (hypothesis)
Goal:
G : Type u
inst : Monoid G
h : ¬ExponentExists G
⊢ exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
have this : Eq (α := Set ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1} ∅
Tactic: have : {d | 0 < d ∧ ∀ (x : G), x ^ d = 1} = ∅ :=
      Set.eq_empty_of_forall_notMem fun n hn ↦ h ⟨n, hn⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Exponent (goal)
Goal:
G : Type u
inst : Monoid G
h : ¬ExponentExists G
this : Eq (α := Set ℕ) {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1} ∅
⊢ exponent G = sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1}
have neg : Eq (α := ℕ) 0 (sInf {d : ℕ | 0 < d ∧ ∀ (x : G), x ^ d = 1})
Tactic: rw [Monoid.exponent_eq_zero_iff.mpr h, this, Nat.sInf_empty]