awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x x_1 : α
⊢ Eq (α := Quotient (orbitRel (↥s.op) α)) (Quotient.mk'' x_1) (↑x : α ⧸ s) ↔ x_1 ∈ x • (↑s : Set α)

Tactic:
simpa [mem_smul_set_iff_inv_smul_mem, ← leftRel_apply, Quotient.eq''] using Setoid.comm' _

Premises used: Quotient.eq'', Set.mem_smul_set_iff_inv_smul_mem, Setoid.comm', QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x : α ⧸ s
H :
  ∀ (z : α),
    MulAction.orbitRel.Quotient.orbit (G := ↥s.op) (↑z : α ⧸ s) =
      Quotient.out (s := leftRel s) (↑z : α ⧸ s) • (↑s : Set α)
⊢ MulAction.orbitRel.Quotient.orbit x = Quotient.out x • (↑s : Set α)

Tactic:
induction x using QuotientGroup.induction_on
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
z : α
⊢ MulAction.orbitRel.Quotient.orbit (G := ↥s.op) (↑z : α ⧸ s) =
    Quotient.out (s := leftRel s) (↑z : α ⧸ s) • (↑s : Set α)

Tactic:
simp only [orbit_mk_eq_smul, ← eq_class_eq_leftCoset, Quotient.out_eq']

Premises used: Quotient.out_eq', QuotientGroup.eq_class_eq_leftCoset, QuotientGroup.orbit_mk_eq_smul
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g : α
x_1 : (↑(g • (↑s : Set α)) : Type u_1)
x : α
property : x ∈ g • (↑s : Set α)
⊢ (↑((fun (x : ↥s) ↦
            (Subtype.mk (p := fun (x : α) ↦ x ∈ g • (↑s : Set α)) (g * (↑x : α)) ⋯ : { x : α // x ∈ g • (↑s : Set α) }))
          ((fun (x : (↑(g • (↑s : Set α)) : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (g⁻¹ * (↑x : α)) ⋯)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ g • (↑s : Set α)) x property))) :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ g • (↑s : Set α)) x property) : α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g_1 : α
x : ↥s
g : α
property : g ∈ s
⊢ (↑((fun (x : (↑(g_1 • (↑s : Set α)) : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) (g_1⁻¹ * (↑x : α)) ⋯)
          ((fun (x : ↥s) ↦
              (Subtype.mk (p := fun (x : α) ↦ x ∈ g_1 • (↑s : Set α)) (g_1 * (↑x : α)) ⋯ :
                { x : α // x ∈ g_1 • (↑s : Set α) }))
            (Subtype.mk (p := fun (x : α) ↦ x ∈ s) g property))) :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) g property) : α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g : α
x_1 : (↑(op g • (↑s : Set α)) : Type u_1)
x : α
property : x ∈ op g • (↑s : Set α)
⊢ (↑((fun (x : ↥s) ↦
            (Subtype.mk (p := fun (x : α) ↦ x ∈ op g • (↑s : Set α)) ((↑x : α) * g) ⋯ :
              { x : α // x ∈ op g • (↑s : Set α) }))
          ((fun (x : (↑(op g • (↑s : Set α)) : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((↑x : α) * g⁻¹) ⋯)
            (Subtype.mk (p := fun (x : α) ↦ x ∈ op g • (↑s : Set α)) x property))) :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ op g • (↑s : Set α)) x property) : α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
g_1 : α
x : ↥s
g : α
property : g ∈ s
⊢ (↑((fun (x : (↑(op g_1 • (↑s : Set α)) : Type u_1)) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((↑x : α) * g_1⁻¹) ⋯)
          ((fun (x : ↥s) ↦
              (Subtype.mk (p := fun (x : α) ↦ x ∈ op g_1 • (↑s : Set α)) ((↑x : α) * g_1) ⋯ :
                { x : α // x ∈ op g_1 • (↑s : Set α) }))
            (Subtype.mk (p := fun (x : α) ↦ x ∈ s) g property))) :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) g property) : α)

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
L : α ⧸ s
rw : { x : α // (↑x : α ⧸ s) = L } ≃ (↑{x : α | Eq (α := α ⧸ s) (↑x : α ⧸ s) (↑(Quotient.out L) : α ⧸ s)} : Type u_1)
⊢ { x : α // (↑x : α ⧸ s) = L } ≃ (↑(Quotient.out L • (↑s : Set α)) : Type u_1)

Tactic:
rw [← eq_class_eq_leftCoset]

Premises used: QuotientGroup.eq_class_eq_leftCoset
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
L : α ⧸ s
simp : { x : α // Quotient.mk'' x = L } ≃ { x : α // Quotient.mk'' x = L }
⊢ { x : α // Quotient.mk'' x = L } ≃
    { x : α // Eq (α := Quotient (leftRel s)) (Quotient.mk'' x) (Quotient.mk'' (Quotient.out L)) }

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x : α // Quotient.mk'' x = L } ≃ { x : α // Quotient.mk'' x = L }

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s : α → α → Prop) b c
rw :
  HMul.hMul (α := ↥t) ((fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) b)⁻¹
      ((fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) c) ∈
    s.subgroupOf t
⊢ (leftRel (s.subgroupOf t) : ↥t → ↥t → Prop)
    ((fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) b)
    ((fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) c)

Tactic:
rw [leftRel_apply]

Premises used: QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s : α → α → Prop) b c
change : ((f (↑b : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
⊢ HMul.hMul (α := ↥t) ((fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) b)⁻¹
      ((fun (g : α) ↦ Subtype.mk (p := fun (x : α) ↦ x ∈ t) ((f (Quotient.mk'' g))⁻¹ * g) ⋯) c) ∈
    s.subgroupOf t

Tactic:
change ((f b)⁻¹ * b)⁻¹ * ((f c)⁻¹ * c) ∈ s

Premises used: HMul.hMul, QuotientGroup.mk, Inv.inv
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s : α → α → Prop) b c
⊢ f (↑b : α ⧸ t) = f (↑c : α ⧸ t)

Tactic:
have key : f b = f c :=
          congr_arg f (Quotient.sound' (leftRel_apply.mpr (h_le (leftRel_apply.mp h))))
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : (leftRel s : α → α → Prop) b c
key : f (↑b : α ⧸ t) = f (↑c : α ⧸ t)
rwa : ((f (↑c : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
rwa₁ : b⁻¹ * (f (↑c : α ⧸ t))⁻¹⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
rwa₂ : b⁻¹ * f (↑c : α ⧸ t) * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s
rwa₃ : b⁻¹ * (f (↑c : α ⧸ t) * ((f (↑c : α ⧸ t))⁻¹ * c)) ∈ s
rwa₄ : b⁻¹ * c ∈ s
rwa₅ rwa₆ rwa₇ rwa₈ : (leftRel s : α → α → Prop) b c
⊢ ((f (↑b : α ⧸ t))⁻¹ * b)⁻¹ * ((f (↑c : α ⧸ t))⁻¹ * c) ∈ s

Tactic:
rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]

Premises used: mul_assoc, inv_inv, mul_inv_rev, mul_inv_cancel_left, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : (leftRel (s.subgroupOf t) : ↥t → ↥t → Prop) b c
rw :
  ∀ (h : b⁻¹ * c ∈ s.subgroupOf t),
    HMul.hMul (α := α) ((fun (b : ↥t) ↦ f a.1 * (↑b : α)) b)⁻¹ ((fun (b : ↥t) ↦ f a.1 * (↑b : α)) c) ∈ s
⊢ (leftRel s : α → α → Prop) ((fun (b : ↥t) ↦ f a.1 * (↑b : α)) b) ((fun (b : ↥t) ↦ f a.1 * (↑b : α)) c)

Tactic:
rw [leftRel_apply] at h ⊢

Premises used: QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : b⁻¹ * c ∈ s.subgroupOf t
change : (f a.1 * (↑b : α))⁻¹ * (f a.1 * (↑c : α)) ∈ s
⊢ HMul.hMul (α := α) ((fun (b : ↥t) ↦ f a.1 * (↑b : α)) b)⁻¹ ((fun (b : ↥t) ↦ f a.1 * (↑b : α)) c) ∈ s

Tactic:
change (f a.1 * b)⁻¹ * (f a.1 * c) ∈ s

Premises used: HMul.hMul, Prod.fst, Subtype.val
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
b c : ↥t
h : b⁻¹ * c ∈ s.subgroupOf t
rwa : (↑b : α)⁻¹ * (f a.1)⁻¹ * (f a.1 * (↑c : α)) ∈ s
rwa₁ : (↑b : α)⁻¹ * ((f a.1)⁻¹ * (f a.1 * (↑c : α))) ∈ s
rwa₂ rwa₃ rwa₄ rwa₅ : (↑b : α)⁻¹ * (↑c : α) ∈ s
⊢ (f a.1 * (↑b : α))⁻¹ * (f a.1 * (↑c : α)) ∈ s

Tactic:
rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, mul_assoc, mul_inv_rev
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : (α ⧸ t) × ↥t ⧸ s.subgroupOf t
⊢ α ⧸ s

Tactic:
refine a.2.map' (fun (b : { x // x ∈ t}) => f a.1 * b) fun b c h => by
      rw [leftRel_apply] at h ⊢
      change (f a.1 * b)⁻¹ * (f a.1 * c) ∈ s
      rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]

Premises used: HMul.hMul, Prod.fst, Quotient.map', Subtype.val, Prod.snd
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
⊢ LeftInverse (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)

Tactic:
Quotient.ind' fun a => ?_

Premises used: Function.LeftInverse, Quotient.ind'
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
refine :
  ∀ (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)
⊢ LeftInverse (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)

Tactic:
refine Quotient.ind' fun a => ?_
-- Module: Mathlib.GroupTheory.Coset.Basic
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)
simp_rw₃ : Eq (α := α ⧸ s) (Quotient.mk'' (f (Quotient.mk'' 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)

Tactic:
simp_rw [Quotient.map'_mk'', id, mul_inv_cancel_left]

Premises used: id, Quotient.map'_mk'', mul_inv_cancel_left
-- Module: Mathlib.GroupTheory.Coset.Basic
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)

Tactic:
Prod.rec ?_

Premises used: Function.LeftInverse, Prod.rec, Function.RightInverse
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
refine :
  ∀ (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)
⊢ 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)

Tactic:
refine Prod.rec ?_
-- Module: Mathlib.GroupTheory.Coset.Basic
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)

Tactic:
Quotient.ind' fun a => ?_

Premises used: Quotient.ind'
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
refine :
  ∀ (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)
⊢ ∀ (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)

Tactic:
refine Quotient.ind' fun a => ?_
-- Module: Mathlib.GroupTheory.Coset.Basic
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)

Tactic:
Quotient.ind' fun b => ?_

Premises used: Quotient.ind'
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
refine :
  ∀ (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)
⊢ ∀ (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)

Tactic:
refine Quotient.ind' fun b => ?_
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : RightInverse f QuotientGroup.mk
a : α
b : ↥t
⊢ 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)
-- Module: Mathlib.GroupTheory.Coset.Basic
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)
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 : α))) ⋯))
    (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)

Tactic:
simp_rw [Quotient.map'_mk'', id, key, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, id, Quotient.map'_mk''
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥s
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
⊢ (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)

Tactic:
simp_rw [leftRel_eq]

Premises used: QuotientGroup.leftRel_eq
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥s
⊢ 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:
id

Premises used: Set.Mem, setOf, id, Set.preimage
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥s
⊢ 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:
exact id

Premises used: id
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t H : Subgroup α
h_1 : s ≤ t
a b : ↥s
h :
  Eq (α := ↥t ⧸ H.subgroupOf t)
    (Quotient.map' (s₁ := leftRel (H.subgroupOf s)) (⇑(inclusion h_1) : (a : ↥s) → ↥t) ⋯ (Quotient.mk'' a))
    (Quotient.map' (s₁ := leftRel (H.subgroupOf s)) (⇑(inclusion h_1) : (a : ↥s) → ↥t) ⋯ (Quotient.mk'' b))
⊢ Eq (α := ↥s ⧸ H.subgroupOf s) (Quotient.mk'' a) (Quotient.mk'' b)

Tactic:
simpa only [Quotient.map'_mk'', QuotientGroup.eq] using h

Premises used: QuotientGroup.eq, Quotient.map'_mk''
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t H : Subgroup α
h : s ≤ t
g : ↥s
⊢ Eq (α := ↥t ⧸ H.subgroupOf t)
    ((quotientSubgroupOfEmbeddingOfLE H h : (a : ↥s ⧸ H.subgroupOf s) → ↥t ⧸ H.subgroupOf t)
        (↑g : ↥s ⧸ H.subgroupOf s) :
      ↥t ⧸ H.subgroupOf t)
    ((↑((inclusion h : (a : ↥s) → ↥t) g) : ↥t ⧸ H.subgroupOf t) : ↥t ⧸ H.subgroupOf t)

Tactic:
rfl

Premises used: Quot.map, Quotient.map', rfl
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥H
simp_rw : a⁻¹ * b ∈ s.subgroupOf H → (id a)⁻¹ * id b ∈ t.subgroupOf H
⊢ (leftRel (s.subgroupOf H) : ↥H → ↥H → Prop) a b → (leftRel (t.subgroupOf H) : ↥H → ↥H → Prop) (id a) (id b)

Tactic:
simp_rw [leftRel_eq]

Premises used: QuotientGroup.leftRel_eq
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t H : Subgroup α
h : s ≤ t
a b : ↥H
⊢ a⁻¹ * b ∈ s.subgroupOf H → (id a)⁻¹ * id b ∈ t.subgroupOf H

Tactic:
apply h
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t H : Subgroup α
h : s ≤ t
g : ↥H
⊢ quotientSubgroupOfMapOfLE H h (↑g : ↥H ⧸ s.subgroupOf H) = (↑g : ↥H ⧸ t.subgroupOf H)

Tactic:
rfl

Premises used: Quotient.map', Subgroup.quotientSubgroupOfMapOfLE, rfl
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h : s ≤ t
a b : α
simp_rw : a⁻¹ * b ∈ s → (id a)⁻¹ * id b ∈ t
⊢ (leftRel s : α → α → Prop) a b → (leftRel t : α → α → Prop) (id a) (id b)

Tactic:
simp_rw [leftRel_eq]

Premises used: QuotientGroup.leftRel_eq
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h : s ≤ t
a b : α
⊢ a⁻¹ * b ∈ s → (id a)⁻¹ * id b ∈ t

Tactic:
apply h
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
h : s ≤ t
g : α
⊢ quotientMapOfLE h (↑g : α ⧸ s) = (↑g : α ⧸ t)

Tactic:
rfl

Premises used: Quotient.map', rfl, Subgroup.quotientMapOfLE