awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
simp_rw simp_rw₁ :
  Eq (α := α ⧸ s)
    (Quotient.map' (s₁ := leftRel (s.subgroupOf t))
      (fun (b : ↥t) ↦ f (Quotient.map' (s₁ := leftRel s) id ⋯ (Quotient.mk'' a)) * (↑b : α)) ⋯
      (Quotient.map' (s₁ := leftRel s)
        (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ (Quotient.mk'' a)))
    (Quotient.mk'' a)
⊢ Eq (α := α ⧸ s)
    ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
        (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) ⋯ a.2 : Quotient (leftRel s)))
      ((fun (a : α ⧸ s) ↦
          ((Quotient.map' id ⋯ a,
              Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ a) :
            (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
        (Quotient.mk'' a)))
    (Quotient.mk'' a)
have simp_rw₂ : Eq (α := α ⧸ s) (Quotient.mk'' (f (Quotient.mk'' (id a)) * ((f (Quotient.mk'' a))⁻¹ * a))) (Quotient.mk'' a)
Tactic: simp_rw [Quotient.map'_mk'', id, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
simp_rw simp_rw₁ :
  Eq (α := α ⧸ s)
    (Quotient.map' (s₁ := leftRel (s.subgroupOf t))
      (fun (b : ↥t) ↦ f (Quotient.map' (s₁ := leftRel s) id ⋯ (Quotient.mk'' a)) * (↑b : α)) ⋯
      (Quotient.map' (s₁ := leftRel s)
        (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ (Quotient.mk'' a)))
    (Quotient.mk'' a)
simp_rw₂ : Eq (α := α ⧸ s) (Quotient.mk'' (f (Quotient.mk'' (id a)) * ((f (Quotient.mk'' a))⁻¹ * a))) (Quotient.mk'' a)
⊢ Eq (α := α ⧸ s)
    ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
        (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) ⋯ a.2 : Quotient (leftRel s)))
      ((fun (a : α ⧸ s) ↦
          ((Quotient.map' id ⋯ a,
              Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ a) :
            (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
        (Quotient.mk'' a)))
    (Quotient.mk'' a)
have simp_rw₃ : Eq (α := α ⧸ s) (Quotient.mk'' (f (Quotient.mk'' a) * ((f (Quotient.mk'' a))⁻¹ * a))) (Quotient.mk'' a)
Tactic: simp_rw [Quotient.map'_mk'', id, mul_inv_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
⊢ RightInverse (fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦ Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) ⋯ a.2)
    fun (a : α ⧸ s) ↦
    (Quotient.map' id ⋯ a,
      Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ a)
have refine : ∀ (fst : α ⧸ t) (snd : ↥t ⧸ s.subgroupOf t),
  (fun (a : α ⧸ s) ↦
        ((Quotient.map' id sorry a,
            Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) sorry) sorry a) :
          (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
      ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
          (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) sorry a.2 : Quotient (leftRel s)))
        (fst, snd)) =
    (fst, snd)
Tactic: refine Prod.rec ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
⊢ ∀ (fst : α ⧸ t) (snd : ↥t ⧸ s.subgroupOf t),
    (fun (a : α ⧸ s) ↦
          ((Quotient.map' id ⋯ a,
              Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ a) :
            (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
        ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
            (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) ⋯ a.2 : Quotient (leftRel s)))
          (fst, snd)) =
      (fst, snd)
have refine : ∀ (a : α) (snd : ↥t ⧸ s.subgroupOf t),
  Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
    ((fun (a : α ⧸ s) ↦
        ((Quotient.map' id sorry a,
            Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) sorry) sorry a) :
          (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
      ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
          (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) sorry a.2 : Quotient (leftRel s)))
        (Quotient.mk'' a, snd)))
    (Quotient.mk'' a, snd)
Tactic: refine Quotient.ind' fun a => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
⊢ ∀ (snd : ↥t ⧸ s.subgroupOf t),
    Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
      ((fun (a : α ⧸ s) ↦
          ((Quotient.map' id ⋯ a,
              Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ a) :
            (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
        ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
            (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) ⋯ a.2 : Quotient (leftRel s)))
          (Quotient.mk'' a, snd)))
      (Quotient.mk'' a, snd)
have refine : ∀ (b : ↥t),
  Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
    ((fun (a : α ⧸ s) ↦
        ((Quotient.map' id sorry a,
            Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) sorry) sorry a) :
          (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
      ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
          (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) sorry a.2 : Quotient (leftRel s)))
        (Quotient.mk'' a, Quotient.mk'' b)))
    (Quotient.mk'' a, Quotient.mk'' b)
Tactic: refine Quotient.ind' fun b => ?_
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (hypothesis)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
b : ↥t
⊢ Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
    ((fun (a : α ⧸ s) ↦
        ((Quotient.map' id ⋯ a,
            Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ a) :
          (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
      ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
          (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) ⋯ a.2 : Quotient (leftRel s)))
        (Quotient.mk'' a, Quotient.mk'' b)))
    (Quotient.mk'' a, Quotient.mk'' b)
have key : Eq (α := Quotient (leftRel t)) (Quotient.mk'' (f (Quotient.mk'' a) * (↑b : α))) (Quotient.mk'' a)
Tactic: have key : Quotient.mk'' (f (Quotient.mk'' a) * b) = Quotient.mk'' a :=
      (QuotientGroup.mk_mul_of_mem (f a) b.2).trans (hf a)
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
b : ↥t
key : Eq (α := Quotient (leftRel t)) (Quotient.mk'' (f (Quotient.mk'' a) * (↑b : α))) (Quotient.mk'' a)
⊢ Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
    ((fun (a : α ⧸ s) ↦
        ((Quotient.map' id ⋯ a,
            Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ a) :
          (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
      ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
          (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) ⋯ a.2 : Quotient (leftRel s)))
        (Quotient.mk'' a, Quotient.mk'' b)))
    (Quotient.mk'' a, Quotient.mk'' b)
have simp_rw : Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
  (Quotient.map' (s₁ := leftRel s) id sorry
      (Quotient.map' (s₁ := leftRel (s.subgroupOf t)) (fun (b : ↥t) ↦ f (Quotient.mk'' a) * (↑b : α)) sorry
        (Quotient.mk'' b)),
    Quotient.map' (s₁ := leftRel s)
      (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) sorry) sorry
      (Quotient.map' (s₁ := leftRel (s.subgroupOf t)) (fun (b : ↥t) ↦ f (Quotient.mk'' a) * (↑b : α)) sorry
        (Quotient.mk'' b)))
  (Quotient.mk'' a, Quotient.mk'' b)
Tactic: simp_rw [Quotient.map'_mk'', id, key, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
b : ↥t
key : Eq (α := Quotient (leftRel t)) (Quotient.mk'' (f (Quotient.mk'' a) * (↑b : α))) (Quotient.mk'' a)
simp_rw simp_rw₁ :
  Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
    (Quotient.map' (s₁ := leftRel s) id ⋯
        (Quotient.map' (s₁ := leftRel (s.subgroupOf t)) (fun (b : ↥t) ↦ f (Quotient.mk'' a) * (↑b : α)) ⋯
          (Quotient.mk'' b)),
      Quotient.map' (s₁ := leftRel s)
        (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯
        (Quotient.map' (s₁ := leftRel (s.subgroupOf t)) (fun (b : ↥t) ↦ f (Quotient.mk'' a) * (↑b : α)) ⋯
          (Quotient.mk'' b)))
    (Quotient.mk'' a, Quotient.mk'' b)
⊢ Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
    ((fun (a : α ⧸ s) ↦
        ((Quotient.map' id ⋯ a,
            Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ a) :
          (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
      ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
          (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) ⋯ a.2 : Quotient (leftRel s)))
        (Quotient.mk'' a, Quotient.mk'' b)))
    (Quotient.mk'' a, Quotient.mk'' b)
have simp_rw₂ : Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
  (Quotient.mk'' (id (f (Quotient.mk'' a) * (↑b : α))),
    Quotient.mk''
      (Subtype.mk (p := fun (x : α) ↦ x ∈ t)
        ((f (Quotient.mk'' (f (Quotient.mk'' a) * (↑b : α))))⁻¹ * (f (Quotient.mk'' a) * (↑b : α))) sorry))
  (Quotient.mk'' a, Quotient.mk'' b)
Tactic: simp_rw [Quotient.map'_mk'', id, key, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
b : ↥t
key : Eq (α := Quotient (leftRel t)) (Quotient.mk'' (f (Quotient.mk'' a) * (↑b : α))) (Quotient.mk'' a)
simp_rw simp_rw₁ :
  Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
    (Quotient.map' (s₁ := leftRel s) id ⋯
        (Quotient.map' (s₁ := leftRel (s.subgroupOf t)) (fun (b : ↥t) ↦ f (Quotient.mk'' a) * (↑b : α)) ⋯
          (Quotient.mk'' b)),
      Quotient.map' (s₁ := leftRel s)
        (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯
        (Quotient.map' (s₁ := leftRel (s.subgroupOf t)) (fun (b : ↥t) ↦ f (Quotient.mk'' a) * (↑b : α)) ⋯
          (Quotient.mk'' b)))
    (Quotient.mk'' a, Quotient.mk'' b)
simp_rw₂ :
  Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
    (Quotient.mk'' (id (f (Quotient.mk'' a) * (↑b : α))),
      Quotient.mk''
        (Subtype.mk (p := fun (x : α) ↦ x ∈ t)
          ((f (Quotient.mk'' (f (Quotient.mk'' a) * (↑b : α))))⁻¹ * (f (Quotient.mk'' a) * (↑b : α))) ⋯))
    (Quotient.mk'' a, Quotient.mk'' b)
⊢ Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
    ((fun (a : α ⧸ s) ↦
        ((Quotient.map' id ⋯ a,
            Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ a) :
          (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
      ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
          (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) ⋯ a.2 : Quotient (leftRel s)))
        (Quotient.mk'' a, Quotient.mk'' b)))
    (Quotient.mk'' a, Quotient.mk'' b)
have simp_rw₃ : Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
  (Quotient.mk'' (f (Quotient.mk'' a) * (↑b : α)),
    Quotient.mk''
      (Subtype.mk (p := fun (x : α) ↦ x ∈ t)
        ((f (Quotient.mk'' (f (Quotient.mk'' a) * (↑b : α))))⁻¹ * (f (Quotient.mk'' a) * (↑b : α))) sorry))
  (Quotient.mk'' a, Quotient.mk'' b)
Tactic: simp_rw [Quotient.map'_mk'', id, key, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
b : ↥t
key : Eq (α := Quotient (leftRel t)) (Quotient.mk'' (f (Quotient.mk'' a) * (↑b : α))) (Quotient.mk'' a)
simp_rw simp_rw₁ :
  Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
    (Quotient.map' (s₁ := leftRel s) id ⋯
        (Quotient.map' (s₁ := leftRel (s.subgroupOf t)) (fun (b : ↥t) ↦ f (Quotient.mk'' a) * (↑b : α)) ⋯
          (Quotient.mk'' b)),
      Quotient.map' (s₁ := leftRel s)
        (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯
        (Quotient.map' (s₁ := leftRel (s.subgroupOf t)) (fun (b : ↥t) ↦ f (Quotient.mk'' a) * (↑b : α)) ⋯
          (Quotient.mk'' b)))
    (Quotient.mk'' a, Quotient.mk'' b)
simp_rw₂ :
  Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
    (Quotient.mk'' (id (f (Quotient.mk'' a) * (↑b : α))),
      Quotient.mk''
        (Subtype.mk (p := fun (x : α) ↦ x ∈ t)
          ((f (Quotient.mk'' (f (Quotient.mk'' a) * (↑b : α))))⁻¹ * (f (Quotient.mk'' a) * (↑b : α))) ⋯))
    (Quotient.mk'' a, Quotient.mk'' b)
simp_rw₃ :
  Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
    (Quotient.mk'' (f (Quotient.mk'' a) * (↑b : α)),
      Quotient.mk''
        (Subtype.mk (p := fun (x : α) ↦ x ∈ t)
          ((f (Quotient.mk'' (f (Quotient.mk'' a) * (↑b : α))))⁻¹ * (f (Quotient.mk'' a) * (↑b : α))) ⋯))
    (Quotient.mk'' a, Quotient.mk'' b)
⊢ Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
    ((fun (a : α ⧸ s) ↦
        ((Quotient.map' id ⋯ a,
            Quotient.map' (fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) ⋯ a) :
          (α ⧸ t) × ↥t ⧸ s.subgroupOf t))
      ((fun (a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t) ↦
          (Quotient.map' (fun (b : ↥t) ↦ f a.1 * (↑b : α)) ⋯ a.2 : Quotient (leftRel s)))
        (Quotient.mk'' a, Quotient.mk'' b)))
    (Quotient.mk'' a, Quotient.mk'' b)
have simp_rw₄ : Eq (α := (α ⧸ t) × ↥t ⧸ s.subgroupOf t)
  (Quotient.mk'' a,
    Quotient.mk''
      (Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' a))⁻¹ * (f (Quotient.mk'' a) * (↑b : α))) sorry))
  (Quotient.mk'' a, Quotient.mk'' b)
Tactic: simp_rw [Quotient.map'_mk'', id, key, inv_mul_cancel_left]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥s
⊢ (leftRel (H.subgroupOf s) : ↥s → ↥s → Prop) a b →
    (leftRel (H.subgroupOf t) : ↥t → ↥t → Prop) ((inclusion h : (a : ↥s) → ↥t) a : ↥t)
      ((inclusion h : (a : ↥s) → ↥t) b : ↥t)
have simp_rw : a⁻¹ * b ∈ H.subgroupOf s →
  HMul.hMul (α := ↥t) (β := ↥t) (((inclusion h : (a : ↥s) → ↥t) a)⁻¹ : ↥t) ((inclusion h : (a : ↥s) → ↥t) b : ↥t) ∈
    H.subgroupOf t
Tactic: simp_rw [leftRel_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥H
⊢ (leftRel (s.subgroupOf H) : ↥H → ↥H → Prop) a b → (leftRel (t.subgroupOf H) : ↥H → ↥H → Prop) (id a) (id b)
have simp_rw : a⁻¹ * b ∈ s.subgroupOf H → (id a)⁻¹ * id b ∈ t.subgroupOf H
Tactic: simp_rw [leftRel_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h : s ≤ t
a b : α
⊢ (leftRel s : α → α → Prop) a b → (leftRel t : α → α → Prop) (id a) (id b)
have simp_rw : a⁻¹ * b ∈ s → (id a)⁻¹ * id b ∈ t
Tactic: simp_rw [leftRel_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
simp_rw simp_rw₁ :
  ∀ (a₁ a₂ : ↥H),
    (Eq (α := (i : ι) → ↥H ⧸ (f i).subgroupOf H) (fun (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₁))
        fun (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
⊢ ∀ (a₁ a₂ : ↥H),
    Eq (α := (i : ι) → ↥H ⧸ (f i).subgroupOf H)
        ((fun (q : ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₁))
        ((fun (q : ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
have simp_rw₂ : ∀ (a₁ a₂ : ↥H),
  (∀ (x : ι), quotientSubgroupOfMapOfLE H sorry (Quotient.mk'' a₁) = quotientSubgroupOfMapOfLE H sorry (Quotient.mk'' a₂)) →
    Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
Tactic: simp_rw [funext_iff, quotientSubgroupOfMapOfLE_apply_mk, QuotientGroup.eq, mem_subgroupOf,
        mem_iInf, imp_self, forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
simp_rw simp_rw₁ :
  ∀ (a₁ a₂ : ↥H),
    (Eq (α := (i : ι) → ↥H ⧸ (f i).subgroupOf H) (fun (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₁))
        fun (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₂ :
  ∀ (a₁ a₂ : ↥H),
    (∀ (x : ι), quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₁) = quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
⊢ ∀ (a₁ a₂ : ↥H),
    Eq (α := (i : ι) → ↥H ⧸ (f i).subgroupOf H)
        ((fun (q : ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₁))
        ((fun (q : ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
have simp_rw₃ : ∀ (a₁ a₂ : ↥H),
  (∀ (x : ι), Eq (α := ↥H ⧸ (f x).subgroupOf H) (↑a₁ : ↥H ⧸ (f x).subgroupOf H) (↑a₂ : ↥H ⧸ (f x).subgroupOf H)) →
    Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
Tactic: simp_rw [funext_iff, quotientSubgroupOfMapOfLE_apply_mk, QuotientGroup.eq, mem_subgroupOf,
        mem_iInf, imp_self, forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
simp_rw simp_rw₁ :
  ∀ (a₁ a₂ : ↥H),
    (Eq (α := (i : ι) → ↥H ⧸ (f i).subgroupOf H) (fun (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₁))
        fun (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₂ :
  ∀ (a₁ a₂ : ↥H),
    (∀ (x : ι), quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₁) = quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₃ :
  ∀ (a₁ a₂ : ↥H),
    (∀ (x : ι), Eq (α := ↥H ⧸ (f x).subgroupOf H) (↑a₁ : ↥H ⧸ (f x).subgroupOf H) (↑a₂ : ↥H ⧸ (f x).subgroupOf H)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
⊢ ∀ (a₁ a₂ : ↥H),
    Eq (α := (i : ι) → ↥H ⧸ (f i).subgroupOf H)
        ((fun (q : ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₁))
        ((fun (q : ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
have simp_rw₄ : ∀ (a₁ a₂ : ↥H), (∀ (x : ι), a₁⁻¹ * a₂ ∈ (f x).subgroupOf H) → a₁⁻¹ * a₂ ∈ subgroupOf (⨅ (i : ι), f i) H
Tactic: simp_rw [funext_iff, quotientSubgroupOfMapOfLE_apply_mk, QuotientGroup.eq, mem_subgroupOf,
        mem_iInf, imp_self, forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
simp_rw simp_rw₁ :
  ∀ (a₁ a₂ : ↥H),
    (Eq (α := (i : ι) → ↥H ⧸ (f i).subgroupOf H) (fun (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₁))
        fun (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₂ :
  ∀ (a₁ a₂ : ↥H),
    (∀ (x : ι), quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₁) = quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₃ :
  ∀ (a₁ a₂ : ↥H),
    (∀ (x : ι), Eq (α := ↥H ⧸ (f x).subgroupOf H) (↑a₁ : ↥H ⧸ (f x).subgroupOf H) (↑a₂ : ↥H ⧸ (f x).subgroupOf H)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₄ : ∀ (a₁ a₂ : ↥H), (∀ (x : ι), a₁⁻¹ * a₂ ∈ (f x).subgroupOf H) → a₁⁻¹ * a₂ ∈ subgroupOf (⨅ (i : ι), f i) H
⊢ ∀ (a₁ a₂ : ↥H),
    Eq (α := (i : ι) → ↥H ⧸ (f i).subgroupOf H)
        ((fun (q : ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₁))
        ((fun (q : ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
have simp_rw₅ : ∀ (a₁ a₂ : ↥H),
  (∀ (x : ι), (↑(a₁⁻¹ * a₂) : α) ∈ f x) → Membership.mem (γ := Subgroup α) (⨅ (i : ι), f i) (↑(a₁⁻¹ * a₂) : α)
Tactic: simp_rw [funext_iff, quotientSubgroupOfMapOfLE_apply_mk, QuotientGroup.eq, mem_subgroupOf,
        mem_iInf, imp_self, forall_const]
-- Lean 4 proof step from Mathlib.GroupTheory.Coset.Basic (goal)
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
simp_rw simp_rw₁ :
  ∀ (a₁ a₂ : ↥H),
    (Eq (α := (i : ι) → ↥H ⧸ (f i).subgroupOf H) (fun (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₁))
        fun (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₂ :
  ∀ (a₁ a₂ : ↥H),
    (∀ (x : ι), quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₁) = quotientSubgroupOfMapOfLE H ⋯ (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₃ :
  ∀ (a₁ a₂ : ↥H),
    (∀ (x : ι), Eq (α := ↥H ⧸ (f x).subgroupOf H) (↑a₁ : ↥H ⧸ (f x).subgroupOf H) (↑a₂ : ↥H ⧸ (f x).subgroupOf H)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₄ : ∀ (a₁ a₂ : ↥H), (∀ (x : ι), a₁⁻¹ * a₂ ∈ (f x).subgroupOf H) → a₁⁻¹ * a₂ ∈ subgroupOf (⨅ (i : ι), f i) H
simp_rw₅ :
  ∀ (a₁ a₂ : ↥H),
    (∀ (x : ι), (↑(a₁⁻¹ * a₂) : α) ∈ f x) → Membership.mem (γ := Subgroup α) (⨅ (i : ι), f i) (↑(a₁⁻¹ * a₂) : α)
⊢ ∀ (a₁ a₂ : ↥H),
    Eq (α := (i : ι) → ↥H ⧸ (f i).subgroupOf H)
        ((fun (q : ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₁))
        ((fun (q : ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (i : ι) ↦ quotientSubgroupOfMapOfLE H ⋯ q) (Quotient.mk'' a₂)) →
      Eq (α := ↥H ⧸ subgroupOf (⨅ (i : ι), f i) H) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
have simp_rw₆ : ∀ (a₁ a₂ : ↥H), (∀ (x : ι), (↑(a₁⁻¹ * a₂) : α) ∈ f x) → ∀ (x : ι), (↑(a₁⁻¹ * a₂) : α) ∈ f x
Tactic: simp_rw [funext_iff, quotientSubgroupOfMapOfLE_apply_mk, QuotientGroup.eq, mem_subgroupOf,
        mem_iInf, imp_self, forall_const]