awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Coset.Basic
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₂) : α)
simp_rw₆ : ∀ (a₁ a₂ : ↥H), (∀ (x : ι), (↑(a₁⁻¹ * a₂) : α) ∈ f x) → ∀ (x : ι), (↑(a₁⁻¹ * a₂) : α) ∈ f x
simp_rw₇ : ∀ (a₁ a₂ : ↥H), True
⊢ ∀ (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₂)

Tactic:
simp_rw [funext_iff, quotientSubgroupOfMapOfLE_apply_mk, QuotientGroup.eq, mem_subgroupOf,
        mem_iInf, imp_self, forall_const]

Premises used: Subgroup.mem_iInf, funext_iff, QuotientGroup.eq, Subgroup.quotientSubgroupOfMapOfLE_apply_mk, imp_self, forall_const, Subgroup.mem_subgroupOf
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
g : ↥H
i : ι
⊢ Eq.{u_1 + 1} (α := ↥H ⧸ (f i).subgroupOf H)
    ((quotientiInfSubgroupOfEmbedding f H :
          (a : ↥H ⧸ (⨅ (i : ι), f i).subgroupOf H) → (i : ι) → ↥H ⧸ (f i).subgroupOf H)
        (↑g : ↥H ⧸ (⨅ (i : ι), f i).subgroupOf H) i :
      ↥H ⧸ (f i).subgroupOf H)
    ((↑g : ↥H ⧸ (f i).subgroupOf H) : ↥H ⧸ (f i).subgroupOf H)

Tactic:
rfl

Premises used: Quot.map, Quotient.map', Subgroup.quotientSubgroupOfMapOfLE, rfl
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
simp_rw simp_rw₁ :
  ∀ (a₁ a₂ : α),
    (Eq (α := (i : ι) → α ⧸ f i) (fun (i : ι) ↦ quotientMapOfLE ⋯ (Quotient.mk'' a₁)) fun (i : ι) ↦
        quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₂ :
  ∀ (a₁ a₂ : α),
    (∀ (x : ι), quotientMapOfLE ⋯ (Quotient.mk'' a₁) = quotientMapOfLE ⋯ (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₃ :
  ∀ (a₁ a₂ : α),
    (∀ (x : ι), Eq (α := α ⧸ f x) (↑a₁ : α ⧸ f x) (↑a₂ : α ⧸ f x)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)
simp_rw₄ : ∀ (a₁ a₂ : α), (∀ (x : ι), a₁⁻¹ * a₂ ∈ f x) → Membership.mem (γ := Subgroup α) (⨅ (i : ι), f i) (a₁⁻¹ * a₂)
simp_rw₅ : ∀ (a₁ a₂ : α), (∀ (x : ι), a₁⁻¹ * a₂ ∈ f x) → ∀ (x : ι), a₁⁻¹ * a₂ ∈ f x
simp_rw₆ : ∀ (a₁ a₂ : α), True
⊢ ∀ (a₁ a₂ : α),
    Eq (α := (i : ι) → α ⧸ f i)
        ((fun (q : HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (i : ι) ↦ quotientMapOfLE ⋯ q)
          (Quotient.mk'' a₁))
        ((fun (q : HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (i : ι) ↦ quotientMapOfLE ⋯ q)
          (Quotient.mk'' a₂)) →
      Eq (α := HasQuotient.Quotient α (B := Subgroup α) (⨅ (i : ι), f i)) (Quotient.mk'' a₁) (Quotient.mk'' a₂)

Tactic:
simp_rw [funext_iff, quotientMapOfLE_apply_mk, QuotientGroup.eq, mem_iInf, imp_self,
        forall_const]

Premises used: Subgroup.mem_iInf, funext_iff, QuotientGroup.eq, imp_self, forall_const, Subgroup.quotientMapOfLE_apply_mk
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
ι : Type u_2
f : ι → Subgroup α
g : α
i : ι
⊢ Eq.{u_1 + 1} (α := α ⧸ f i)
    ((quotientiInfEmbedding f : (a : α ⧸ ⨅ (i : ι), f i) → (i : ι) → α ⧸ f i) (↑g : α ⧸ ⨅ (i : ι), f i) i : α ⧸ f i)
    ((↑g : α ⧸ f i) : α ⧸ f i)

Tactic:
rfl

Premises used: Quot.map, Quotient.map', rfl, Subgroup.quotientMapOfLE
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a x : α
rw :
  Membership.mem (α := H) (γ := Set H) (singleton (α := H) ((f : (a : α) → H) a : H)) ((f : (a : α) → H) x : H) ↔
    x ∈ a • (↑f.ker : Set α)
rw₁ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ x ∈ a • (↑f.ker : Set α)
rw₂ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ (↑f.ker : Set α)
rw₃ : Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔ a⁻¹ • x ∈ f.ker
rw₄ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) (a⁻¹ • x) : H) (1 : H)
rw₅ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) (a⁻¹ * x) : H) (1 : H)
rw₆ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    HMul.hMul (α := H) (β := H) ((f : (a : α) → H) a⁻¹ : H) ((f : (a : α) → H) x : H) = 1
rw₇ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    HMul.hMul (α := H) (β := H) (((f : (a : α) → H) a)⁻¹ : H) ((f : (a : α) → H) x : H) = 1
rw₈ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) x : H) ((f : (a : α) → H) a : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) a : H) ((f : (a : α) → H) x : H)
rw₉ rw₁₀ :
  Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) a : H) ((f : (a : α) → H) x : H) ↔
    Eq.{u_2 + 1} (α := H) ((f : (a : α) → H) a : H) ((f : (a : α) → H) x : H)
⊢ Membership.mem (γ := Set α) (preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) a : H))) x ↔
    x ∈ a • (↑f.ker : Set α)

Tactic:
rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker,
        smul_eq_mul, map_mul, map_inv, inv_mul_eq_one, eq_comm]

Premises used: map_inv, MonoidHom.mem_ker, eq_comm, map_mul, Set.mem_singleton_iff, SetLike.mem_coe, Set.mem_smul_set_iff_inv_smul_mem, smul_eq_mul, Set.mem_preimage, inv_mul_eq_one
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a : α
g : (↑(preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) a : H))) : Type u_1)
⊢ (↑((f.fiberEquivKer a : (a : (↑((⇑f : (a : α) → H) ⁻¹' {(f : (a : α) → H) a}) : Type u_1)) → ↥f.ker) g) : α) =
    a⁻¹ * (↑g : α)

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Set.image, rfl
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a : α
g : ↥f.ker
⊢ (↑(((f.fiberEquivKer a).symm : (a_1 : ↥f.ker) → (↑((⇑f : (a : α) → H) ⁻¹' {(f : (a : α) → H) a}) : Type u_1)) g) :
      α) =
    a * (↑g : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a b : α
g : (↑(preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) a : H))) : Type u_1)
⊢ (↑((f.fiberEquiv a b :
            (a : (↑((⇑f : (a : α) → H) ⁻¹' {(f : (a : α) → H) a}) : Type u_1)) →
              (↑((⇑f : (a : α) → H) ⁻¹' {(f : (a : α) → H) b}) : Type u_1))
          g) :
      α) =
    b * (a⁻¹ * (↑g : α))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Set.image, rfl
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
a b : α
g : (↑(preimage (β := H) (⇑f : (a : α) → H) (singleton (α := H) ((f : (a : α) → H) b : H))) : Type u_1)
⊢ (↑(((f.fiberEquiv a b).symm :
            (a_1 : (↑((⇑f : (a : α) → H) ⁻¹' {(f : (a : α) → H) b}) : Type u_1)) →
              (↑((⇑f : (a : α) → H) ⁻¹' {(f : (a : α) → H) a}) : Type u_1))
          g) :
      α) =
    a * (b⁻¹ * (↑g : α))

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Set.image, rfl
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : ↥s × (↑t : Type u_1)
rw : (↑a.2 : α ⧸ s) ∈ t
⊢ (↑(Quotient.out (↑a.2 : α ⧸ s) * (↑a.1 : α)) : α ⧸ s) ∈ t

Tactic:
rw [mk_mul_of_mem _ a.1.2, out_eq']

Premises used: QuotientGroup.out_eq', QuotientGroup.mk_mul_of_mem, Prod.fst, Subtype.property
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : ↥s × (↑t : Type u_1)
⊢ (↑a.2 : α ⧸ s) ∈ t

Tactic:
a.2.2

Premises used: Prod.snd, Subtype.property
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : ↥s × (↑t : Type u_1)
⊢ (↑a.2 : α ⧸ s) ∈ t

Tactic:
exact a.2.2

Premises used: Prod.snd, Subtype.property
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set (α ⧸ s)
x : (↑(mk ⁻¹' t) : Type u_1)
a : α
property : a ∈ mk ⁻¹' t
⊢ HMul.hMul (α := α)
      (Quotient.out (s := leftRel s)
        (↑((fun (a : (↑(mk ⁻¹' t) : Type u_1)) ↦
                  (Subtype.mk (p := fun (x : α) ↦ x ∈ s)
                      ((Quotient.out (s := leftRel s) (↑(↑a : α) : α ⧸ s))⁻¹ * (↑a : α)) ⋯,
                    Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) (↑(↑a : α) : α ⧸ s) ⋯))
                (Subtype.mk (p := fun (x : α) ↦ x ∈ mk ⁻¹' t) a property)).2 :
          α ⧸ s))
      (↑((fun (a : (↑(mk ⁻¹' t) : Type u_1)) ↦
                (Subtype.mk (p := fun (x : α) ↦ x ∈ s)
                    ((Quotient.out (s := leftRel s) (↑(↑a : α) : α ⧸ s))⁻¹ * (↑a : α)) ⋯,
                  Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) (↑(↑a : α) : α ⧸ s) ⋯))
              (Subtype.mk (p := fun (x : α) ↦ x ∈ mk ⁻¹' t) a property)).1 :
        α) =
    a

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set (α ⧸ s)
x_1 : ↥s × (↑t : Type u_1)
a : α
ha : a ∈ s
x : α ⧸ s
hx : x ∈ t
fst :
  (↑((fun (a : (↑(mk ⁻¹' t) : Type u_1)) ↦
              (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((Quotient.out (s := leftRel s) (↑(↑a : α) : α ⧸ s))⁻¹ * (↑a : α))
                  ⋯,
                Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) (↑(↑a : α) : α ⧸ s) ⋯))
            ((fun (a : ↥s × (↑t : Type u_1)) ↦
                (Subtype.mk (p := fun (x : α) ↦ x ∈ mk ⁻¹' t) (Quotient.out (↑a.2 : α ⧸ s) * (↑a.1 : α)) ⋯ :
                  { x : α // x ∈ mk ⁻¹' t }))
              (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx))).1 :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx).1 : α)
snd :
  (↑((fun (a : (↑(mk ⁻¹' t) : Type u_1)) ↦
              (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((Quotient.out (s := leftRel s) (↑(↑a : α) : α ⧸ s))⁻¹ * (↑a : α))
                  ⋯,
                Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) (↑(↑a : α) : α ⧸ s) ⋯))
            ((fun (a : ↥s × (↑t : Type u_1)) ↦
                (Subtype.mk (p := fun (x : α) ↦ x ∈ mk ⁻¹' t) (Quotient.out (↑a.2 : α ⧸ s) * (↑a.1 : α)) ⋯ :
                  { x : α // x ∈ mk ⁻¹' t }))
              (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx))).2 :
      α ⧸ s) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx).2 : α ⧸ s)
⊢ (fun (a : (↑(mk ⁻¹' t) : Type u_1)) ↦
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((Quotient.out (s := leftRel s) (↑(↑a : α) : α ⧸ s))⁻¹ * (↑a : α)) ⋯,
          Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) (↑(↑a : α) : α ⧸ s) ⋯))
      ((fun (a : ↥s × (↑t : Type u_1)) ↦
          (Subtype.mk (p := fun (x : α) ↦ x ∈ mk ⁻¹' t) (Quotient.out (↑a.2 : α ⧸ s) * (↑a.1 : α)) ⋯ :
            { x : α // x ∈ mk ⁻¹' t }))
        (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx)) =
    (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx)

Tactic:
ext
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set (α ⧸ s)
x_1 : ↥s × (↑t : Type u_1)
a : α
ha : a ∈ s
x : α ⧸ s
hx : x ∈ t
⊢ (↑((fun (a : (↑(mk ⁻¹' t) : Type u_1)) ↦
              (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((Quotient.out (s := leftRel s) (↑(↑a : α) : α ⧸ s))⁻¹ * (↑a : α))
                  ⋯,
                Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) (↑(↑a : α) : α ⧸ s) ⋯))
            ((fun (a : ↥s × (↑t : Type u_1)) ↦
                (Subtype.mk (p := fun (x : α) ↦ x ∈ mk ⁻¹' t) (Quotient.out (↑a.2 : α ⧸ s) * (↑a.1 : α)) ⋯ :
                  { x : α // x ∈ mk ⁻¹' t }))
              (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx))).1 :
      α) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx).1 : α)

Tactic:
simp [ha]
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set (α ⧸ s)
x_1 : ↥s × (↑t : Type u_1)
a : α
ha : a ∈ s
x : α ⧸ s
hx : x ∈ t
⊢ (↑((fun (a : (↑(mk ⁻¹' t) : Type u_1)) ↦
              (Subtype.mk (p := fun (x : α) ↦ x ∈ s) ((Quotient.out (s := leftRel s) (↑(↑a : α) : α ⧸ s))⁻¹ * (↑a : α))
                  ⋯,
                Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) (↑(↑a : α) : α ⧸ s) ⋯))
            ((fun (a : ↥s × (↑t : Type u_1)) ↦
                (Subtype.mk (p := fun (x : α) ↦ x ∈ mk ⁻¹' t) (Quotient.out (↑a.2 : α ⧸ s) * (↑a.1 : α)) ⋯ :
                  { x : α // x ∈ mk ⁻¹' t }))
              (Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx))).2 :
      α ⧸ s) =
    (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ s) a ha, Subtype.mk (p := fun (x : α ⧸ s) ↦ x ∈ t) x hx).2 : α ⧸ s)

Tactic:
simp [ha]
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
H : Subgroup α
simp_rw :
  Eq.{u_1 + 1} (α := Set α) (⋃ (x : orbitRel.Quotient (↥H.op) α), Quotient.out x • (↑H : Set α))
    (⋃ (x : α ⧸ H), Quotient.out x • (↑H : Set α))
⊢ Eq.{u_1 + 1} (α := Set α) univ (⋃ (x : α ⧸ H), Quotient.out x • (↑H : Set α))

Tactic:
simp_rw [univ_eq_iUnion_orbit H.op, orbit_eq_out_smul]

Premises used: Membership.mem, MulAction.univ_eq_iUnion_orbit, Subtype, Subgroup.op, QuotientGroup.orbit_eq_out_smul
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
H : Subgroup α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (x : orbitRel.Quotient (↥H.op) α), Quotient.out x • (↑H : Set α))
    (⋃ (x : α ⧸ H), Quotient.out x • (↑H : Set α))

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
x y : α
h : (leftRel ⊥ : α → α → Prop) x y
rwa : ∀ (h : Membership.mem (γ := Subgroup α) ⊥ (x⁻¹ * y)), (id x)⁻¹ * id y = 1
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (h : x⁻¹ * y = 1), (id x)⁻¹ * id y = 1
⊢ (id x)⁻¹ * id y = 1

Tactic:
rwa [leftRel_apply, Subgroup.mem_bot] at h

Premises used: Subgroup.mem_bot, QuotientGroup.leftRel_apply
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
x : HasQuotient.Quotient α (B := Subgroup α) ⊥
h :
  ∀ (a : α),
    Eq (α := HasQuotient.Quotient α (B := Subgroup α) ⊥) (↑(Quotient.lift (s := leftRel ⊥) id ⋯ ⟦a⟧) : α ⧸ ⊥) ⟦a⟧
⊢ (↑(Quotient.lift id ⋯ x) : α ⧸ ⊥) = x

Tactic:
induction x using Quotient.inductionOn
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
a : α
⊢ Eq (α := HasQuotient.Quotient α (B := Subgroup α) ⊥) (↑(Quotient.lift (s := leftRel ⊥) id ⋯ ⟦a⟧) : α ⧸ ⊥) ⟦a⟧

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Basic
Goal:
α : Type u_1
inst : Group α
x : α
⊢ Quotient.lift (s := leftRel ⊥) id ⋯ (↑x : α ⧸ ⊥) = x

Tactic:
simp
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
inst_1 : Finite α
⊢ Finite.{u_1 + 1} (α ⧸ s)

Tactic:
Quotient.finite _

Premises used: Quotient.finite
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
inst_1 : Fintype (α ⧸ s)
⊢ Fintype.card.{u_1} (Quotient (rightRel s)) = Fintype.card.{u_1} (α ⧸ s)

Tactic:
Fintype.ofEquiv_card (QuotientGroup.quotientRightRelEquivQuotientLeftRel s).symm

Premises used: QuotientGroup.quotientRightRelEquivQuotientLeftRel, Fintype.ofEquiv_card, Equiv.symm
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
rw : Nat.card α = Nat.card.{u_1} ((α ⧸ s) × ↥s)
⊢ Nat.card α = Nat.card.{u_1} (α ⧸ s) * Nat.card.{u_1} ↥s

Tactic:
rw [← Nat.card_prod]

Premises used: Nat.card_prod
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card.{u_1} ((α ⧸ s) × ↥s)

Tactic:
Nat.card_congr Subgroup.groupEquivQuotientProdSubgroup

Premises used: Subgroup.groupEquivQuotientProdSubgroup, Nat.card_congr
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ Nat.card α = Nat.card.{u_1} ((α ⧸ s) × ↥s)

Tactic:
exact Nat.card_congr Subgroup.groupEquivQuotientProdSubgroup

Premises used: Subgroup.groupEquivQuotientProdSubgroup, Nat.card_congr
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set α
rw : (↑(t * (↑s : Set α)) : Type u_1) ≃ ↥s × (↑(QuotientGroup.mk '' t) : Type u_1)
⊢ Nat.card.{u_1} (↑(t * (↑s : Set α)) : Type u_1) =
    Nat.card.{u_1} ↥s * Nat.card.{u_1} (↑(QuotientGroup.mk '' t) : Type u_1)

Tactic:
rw [← Nat.card_prod, Nat.card_congr]

Premises used: Nat.card_congr, Nat.card_prod
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set α
apply :
  (↑(t * (↑s : Set α)) : Type u_1) ≃ (↑(Set.preimage (β := α ⧸ s) QuotientGroup.mk (QuotientGroup.mk '' t)) : Type u_1)
⊢ (↑(t * (↑s : Set α)) : Type u_1) ≃ ↥s × (↑(QuotientGroup.mk '' t) : Type u_1)

Tactic:
apply Equiv.trans _ (QuotientGroup.preimageMkEquivSubgroupProdSet _ _)

Premises used: Equiv.trans, QuotientGroup.preimageMkEquivSubgroupProdSet
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set α
rw : (↑(t * (↑s : Set α)) : Type u_1) ≃ (↑(⋃ (x : ↥s), (fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' t) : Type u_1)
⊢ (↑(t * (↑s : Set α)) : Type u_1) ≃ (↑(Set.preimage (β := α ⧸ s) QuotientGroup.mk (QuotientGroup.mk '' t)) : Type u_1)

Tactic:
rw [QuotientGroup.preimage_image_mk]

Premises used: QuotientGroup.preimage_image_mk
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set α
h : ⋃ (x : ↥s), (fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' t = t * (↑s : Set α)
⊢ (↑(t * (↑s : Set α)) : Type u_1) ≃ (↑(⋃ (x : ↥s), (fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' t) : Type u_1)

Tactic:
convert! Equiv.refl ↑(t * s)

Premises used: HMul.hMul, Set.Elem, SetLike.coe, Equiv.refl
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
t : Set α
⊢ ⋃ (x : ↥s), (fun (x_1 : α) ↦ x_1 * (↑x : α)) ⁻¹' t = t * (↑s : Set α)

Tactic:
aesop (add simp [Set.mem_mul])

Premises used: Set.mem_mul
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ Nat.card.{u_1} ↥s ∣ Nat.card α

Tactic:
simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]

Premises used: Subgroup.card_eq_card_quotient_mul_card_subgroup, dvd_mul_left
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ Nat.card.{u_1} ↥s ∣ Nat.card α

Tactic:
classical simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]

Premises used: Subgroup.card_eq_card_quotient_mul_card_subgroup, dvd_mul_left
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ Nat.card.{u_1} (α ⧸ s) ∣ Nat.card α

Tactic:
simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_right ℕ]

Premises used: Subgroup.card_eq_card_quotient_mul_card_subgroup, dvd_mul_right
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := H) (⇑f : (a : α) → H)
⊢ Nat.card α = Nat.card.{u_2} ↥f.range

Tactic:
Nat.card_congr (Equiv.ofInjective f hf)

Premises used: Equiv.ofInjective, Nat.card_congr, DFunLike.coe
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := H) (⇑f : (a : α) → H)
⊢ Nat.card.{u_2} ↥f.range ∣ Nat.card H

Tactic:
card_subgroup_dvd_card _

Premises used: Subgroup.card_subgroup_dvd_card
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := H) (⇑f : (a : α) → H)
⊢ Nat.card α ∣ Nat.card H

Tactic:
calc
      Nat.card α = Nat.card (f.range : Subgroup H) := Nat.card_congr (Equiv.ofInjective f hf)
      _ ∣ Nat.card H := card_subgroup_dvd_card _

Premises used: MonoidHom.range, Membership.mem, Subtype, Nat.card, Equiv.ofInjective, Nat.card_congr, Subgroup.card_subgroup_dvd_card, DFunLike.coe
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
f : α →* H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := H) (⇑f : (a : α) → H)
⊢ Nat.card α ∣ Nat.card H

Tactic:
classical calc
      Nat.card α = Nat.card (f.range : Subgroup H) := Nat.card_congr (Equiv.ofInjective f hf)
      _ ∣ Nat.card H := card_subgroup_dvd_card _

Premises used: MonoidHom.range, Membership.mem, Subtype, Nat.card, Equiv.ofInjective, Nat.card_congr, Subgroup.card_subgroup_dvd_card, DFunLike.coe
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
H K : Subgroup α
hHK : H ≤ K
⊢ Nat.card.{u_1} ↥H ∣ Nat.card.{u_1} ↥K

Tactic:
card_dvd_of_injective (inclusion hHK) (inclusion_injective hHK)

Premises used: Subgroup.card_dvd_of_injective, Subgroup.inclusion, Subgroup.inclusion_injective
-- Module: Mathlib.GroupTheory.Coset.Card
Goal:
α : Type u_1
inst : Group α
H : Type u_2
inst_1 : Group H
K : Subgroup H
f : α →* H
hf : Function.Injective.{u_1 + 1, u_2 + 1} (α := α) (β := H) (⇑f : (a : α) → H)
⊢ Nat.card.{u_1} ↥(comap f K) ∣ Nat.card.{u_2} ↥K

Tactic:
calc Nat.card (K.comap f) = Nat.card ((K.comap f).map f) :=
      Nat.card_congr (equivMapOfInjective _ _ hf).toEquiv
    _ ∣ Nat.card K := card_dvd_of_le (map_comap_le _ _)

Premises used: Trans.trans, MulEquiv.toEquiv, Nat.card_congr, Subgroup.card_dvd_of_le, Subgroup.map_comap_le, Subgroup.equivMapOfInjective
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
⊢ (∃ (a : ↥s), y * (↑a : α) = x) ↔ ∃ (a : ↥s), x⁻¹ * y = (↑a⁻¹ : α)

Tactic:
simp only [inv_mul_eq_iff_eq_mul, Subgroup.coe_inv, eq_mul_inv_iff_mul_eq]

Premises used: Subgroup.coe_inv, eq_mul_inv_iff_mul_eq, inv_mul_eq_iff_eq_mul
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
x y : α
⊢ (∃ (a : ↥s), x⁻¹ * y = (↑a⁻¹ : α)) ↔ x⁻¹ * y ∈ s

Tactic:
simp [exists_inv_mem_iff_exists_mem]

Premises used: exists_inv_mem_iff_exists_mem
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
simp : ∀ (a b : α), (leftRel s : α → α → Prop) a b ↔ a⁻¹ * b ∈ s
⊢ ∀ (a b : α), (leftRel s : α → α → Prop) a b = (a⁻¹ * b ∈ s)

Tactic:
simp only [eq_iff_iff]

Premises used: eq_iff_iff
-- Module: Mathlib.GroupTheory.Coset.Defs
Goal:
α : Type u_1
inst : Group α
s : Subgroup α
⊢ ∀ (a b : α), (leftRel s : α → α → Prop) a b ↔ a⁻¹ * b ∈ s

Tactic:
apply leftRel_apply

Premises used: QuotientGroup.leftRel_apply