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 : Subgroup G
a b : G
⊢ (∃ a_1 ∈ H, ∃ (b_1 : G), Membership.mem (γ := Subgroup G) ⊥ b_1 ∧ b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H
have h : (∃ a_1 ∈ H, ∃ (b_1 : G), Membership.mem (γ := Subgroup G) ⊥ b_1 ∧ b = a_1 * a * b_1) → b * a⁻¹ ∈ 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 ∈ H, ∃ (b_1 : G), Membership.mem (γ := Subgroup G) ⊥ b_1 ∧ b = a_1 * a * b_1) → b * a⁻¹ ∈ H
⊢ (∃ a_1 ∈ H, ∃ (b_1 : G), Membership.mem (γ := Subgroup G) ⊥ b_1 ∧ b = a_1 * a * b_1) ↔ b * a⁻¹ ∈ H
have h₁ : b * a⁻¹ ∈ H → ∃ a_2 ∈ H, ∃ (b_1 : G), Membership.mem (γ := Subgroup G) ⊥ b_1 ∧ 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
⊢ b * a * 1 * a⁻¹ ∈ H
have h : b * a * a⁻¹ ∈ H
Tactic: rwa [mul_one, mul_inv_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
h : b * a⁻¹ ∈ H
⊢ b = b * a⁻¹ * a * 1
have rw : b = b * a⁻¹ * a
Tactic: rw [mul_one, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
a b : G
h : b * a⁻¹ ∈ H
rw : b = b * a⁻¹ * a
⊢ b = b * a⁻¹ * a * 1
have rw₁ : b = b
Tactic: rw [mul_one, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : G
⊢ mk H K a = mk H K b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k
have rw : (setoid (↑H : Set G) (↑K : Set G) : G → G → Prop) a b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k
Tactic: rw [eq'']
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (hypothesis)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
g : G
⊢ ∃ (h : G) (k : G), h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k
have 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
Tactic: have := eq H K (mk H K g : Quotient ↑H ↑K).out g
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (hypothesis)
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
⊢ ∃ (h : G) (k : G), h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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) (k : G), h ∈ H ∧ k ∈ K ∧ Quotient.out (mk H K g) = h * g * k
have 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
Tactic: obtain ⟨h, h_h, k, hk, T⟩ := this.1 rfl
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
have refine : h * (Quotient.out (mk H K g) * k) = g
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 ?_)⟩
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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 * (Quotient.out (mk H K g) * k) = g
have rw : h * Quotient.out (mk H K g) * k = g
Tactic: rw [← mul_assoc, ← T]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ h * (Quotient.out (mk H K g) * k) = g
have rw₁ : g = g
Tactic: rw [← mul_assoc, ← T]
-- 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 : doubleCoset a (↑H : Set G) (↑K : Set G) = doubleCoset b (↑H : Set G) (↑K : Set G)
⊢ mk H K a = mk H K b
have rw : ∃ h ∈ H, ∃ k ∈ K, b = h * a * k
Tactic: rw [eq]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
i : Quotient (↑H : Set G) (↑K : Set G)
a : G
⊢ a ∈ quotToDoubleCoset H K i ↔ mk H K a = i
have refine : ∀ (hg : mk H K a = i), a ∈ quotToDoubleCoset H K i
Tactic: refine ⟨fun hg ↦ by simp [mk_eq_of_doubleCoset_eq (doubleCoset_eq_of_mem hg)], fun hg ↦ ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (hypothesis)
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
⊢ a ∈ quotToDoubleCoset H K i
have hg₁ : mk H K a = mk H K (Quotient.out i)
Tactic: rw [← out_eq' _ _ i] at hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a b : Quotient (↑H : Set G) (↑K : Set G)
⊢ a ≠ b →
    Disjoint (doubleCoset (Quotient.out a) (↑H : Set G) (↑K : Set G))
      (doubleCoset (Quotient.out b) (↑H : Set G) (↑K : Set G))
have contrapose : ¬Disjoint (doubleCoset (Quotient.out a) (↑H : Set G) (↑K : Set G))
      (doubleCoset (Quotient.out b) (↑H : Set G) (↑K : Set G)) →
  a = b
Tactic: contrapose
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
have 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
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
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
have h : ∃ (i : Quotient (↑H : Set G) (↑K : Set G)), ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out i * y
Tactic: simp only [Set.mem_iUnion, quotToDoubleCoset, mem_doubleCoset, SetLike.mem_coe, Set.mem_univ,
    iff_true]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
x : G
⊢ ∃ (i : Quotient (↑H : Set G) (↑K : Set G)), ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out i * y
have h : ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out (mk H K x) * y
Tactic: use mk H K x
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
x : G
⊢ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * Quotient.out (mk H K x) * y
have 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
Tactic: obtain ⟨h, k, h3, h4, h5⟩ := mk_out_eq_mul H K x
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
have h₁ : x = h⁻¹ * Quotient.out (mk H K x) * k⁻¹
Tactic: refine ⟨h⁻¹, H.inv_mem h3, k⁻¹, K.inv_mem h4, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a : G
⊢ ⋃ (k : ↥K), op (a * (↑k : G)) • (↑H : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a 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)
have h : (∃ (i : ↥K), x * ((↑i : G)⁻¹ * a⁻¹) ∈ H) ↔ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y
Tactic: simp only [mem_rightCoset_iff, mul_inv_rev, Set.mem_iUnion, mem_doubleCoset,
    SetLike.mem_coe]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x : G
⊢ (∃ (i : ↥K), x * ((↑i : G)⁻¹ * a⁻¹) ∈ H) ↔ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y
have h : (∃ (i : ↥K), x * ((↑i : G)⁻¹ * a⁻¹) ∈ H) → ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ (∃ (i : ↥K), x * ((↑i : G)⁻¹ * a⁻¹) ∈ H) ↔ ∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y
have h₁ : (∃ x_1 ∈ H, ∃ y ∈ K, x = x_1 * a * y) → ∃ (i : ↥K), x * ((↑i : G)⁻¹ * a⁻¹) ∈ H
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
have h : x = x * ((↑y⁻¹ : G) * a⁻¹) * a * (↑y : G)
Tactic: refine ⟨x * (y⁻¹ * a⁻¹), h_h, y, y.2, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
have h : x_1 * ((↑(Subtype.mk (p := fun (x : G) ↦ x ∈ K) y hy) : G)⁻¹ * a⁻¹) ∈ H
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
a : G
⊢ ⋃ (h : ↥H), ((↑h : G) * a) • (↑K : Set G) = doubleCoset a (↑H : Set G) (↑K : Set G)
have 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)
Tactic: ext x
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x : G
⊢ Membership.mem (γ := Set G) (⋃ (h : ↥H), ((↑h : G) * a) • (↑K : Set G)) x ↔
    x ∈ doubleCoset a (↑H : Set G) (↑K : Set G)
have h : (∃ (i : ↥H), a⁻¹ * (↑i : G)⁻¹ * x ∈ (↑K : Set G)) ↔ ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * a * y
Tactic: simp only [mem_leftCoset_iff, mul_inv_rev, Set.mem_iUnion, mem_doubleCoset]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
a x : G
⊢ (∃ (i : ↥H), a⁻¹ * (↑i : G)⁻¹ * x ∈ (↑K : Set G)) ↔ ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * a * y
have h : (∃ (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
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ (∃ (i : ↥H), a⁻¹ * (↑i : G)⁻¹ * x ∈ (↑K : Set G)) ↔ ∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * a * y
have h₁ : (∃ x_1 ∈ (↑H : Set G), ∃ y ∈ (↑K : Set G), x = x_1 * a * y) → ∃ (i : ↥H), a⁻¹ * (↑i : G)⁻¹ * x ∈ (↑K : Set G)
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
have h : x = (↑y : G) * a * (a⁻¹ * (↑y⁻¹ : G) * x)
Tactic: refine ⟨y, y.2, a⁻¹ * y⁻¹ * x, h_h, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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)
have h : a⁻¹ * (↑(Subtype.mk (p := fun (x : G) ↦ x ∈ H) x hx) : G)⁻¹ * x_1 ∈ (↑K : Set G)
Tactic: refine ⟨⟨x, hx⟩, ?_⟩
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ _root_.Quotient (setoid (↑⊥ : Set G) (↑H : Set G)) = (G ⧸ H)
have e_s : setoid (↑⊥ : Set G) (↑H : Set G) = leftRel H
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ setoid (↑⊥ : Set G) (↑H : Set G) = leftRel H
have e_s : ∀ (a b : G), (setoid (↑⊥ : Set G) (↑H : Set G) : G → G → Prop) a b ↔ (leftRel H : G → G → Prop) a b
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ _root_.Quotient (setoid (↑H : Set G) (↑⊥ : Set G)) = _root_.Quotient (rightRel H)
have e_s : setoid (↑H : Set G) (↑⊥ : Set G) = rightRel H
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ setoid (↑H : Set G) (↑⊥ : Set G) = rightRel H
have e_s : ∀ (a b : G), (setoid (↑H : Set G) (↑⊥ : Set G) : G → G → Prop) a b ↔ (rightRel H : G → G → Prop) a b
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ 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
have 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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
h : 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
have 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
Tactic: cases nonempty_fintype (Quotient (H : Set G) K)
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ Finite.{u_1 + 1} (Quotient (↑H : Set G) (↑K : Set G))
have simp_rw : Set.Finite.{u_1} (α := Quotient (↑H : Set G) (↑K : Set G)) Set.univ
Tactic: simp_rw [← Set.finite_univ_iff, ← this, I.finite_toSet]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ Finite.{u_1 + 1} (Quotient (↑H : Set G) (↑K : Set G))
have simp_rw₁ : (↑I : Set (Quotient (↑H : Set G) (↑K : Set G))).Finite
Tactic: simp_rw [← Set.finite_univ_iff, ← this, I.finite_toSet]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ Finite.{u_1 + 1} (Quotient (↑H : Set G) (↑K : Set G))
have mpr : (↑I : Set (Quotient (↑H : Set G) (↑K : Set G))) = Set.univ
Tactic: suffices (I : Set (Quotient (H : Set G) K)) = Set.univ by
      simp_rw [← Set.finite_univ_iff, ← this, I.finite_toSet]
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ (↑I : Set (Quotient (↑H : Set G) (↑K : Set G))) = Set.univ
have 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)))
Tactic: rw [Set.eq_univ_iff_forall] at hI ⊢
Cleared hypotheses: hI
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (goal)
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
⊢ Quot.mk (⇑(setoid (↑H : Set G) (↑K : Set G)) : G → G → Prop) g ∈ (↑I : Set (Quotient (↑H : Set G) (↑K : Set G)))
have 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)))
Tactic: obtain ⟨_, ⟨i, _, rfl⟩, T, ⟨hi, rfl⟩, hT : g ∈ quotToDoubleCoset H K i⟩ := hI g
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (hypothesis)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ 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
have cover : 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
-- 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
⊢ 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
have 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
Tactic: rw [Set.iUnion_eq_univ_iff]
-- 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) (⇑(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
have 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
Tactic: obtain ⟨y, hy⟩ := exists_rep x
-- 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) (⇑(leftRel K) : 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) (⇑(leftRel K) : G → G → Prop)
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
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) (⇑(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⟩
-- Lean 4 proof step from Mathlib.GroupTheory.DoubleCoset (hypothesis)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
⊢ 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
have cover : 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
-- 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
⊢ 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
have 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
Tactic: rw [Set.iUnion_eq_univ_iff]
-- 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)
⊢ ∃ (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 obtain : ∀ (y : G) (hy : ⟦y⟧ = x),
  ∃ (i : Quotient (↑H : Set G) (↑K : Set G)),
    Membership.mem (γ := Set (Quot (α := G) (⇑(rightRel H) : G → G → Prop)))
      (Quot.mk (⇑(rightRel H) : G → G → Prop) '' doubleCoset (out i) (↑H : Set G) (↑K : Set G)) x
Tactic: obtain ⟨y, hy⟩ := exists_rep x