Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Mitchell Rowett, Scott Morrison

! This file was ported from Lean 3 source module group_theory.coset
! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Quotient
import Mathlib.Data.Fintype.Prod
import Mathlib.GroupTheory.GroupAction.Basic
import Mathlib.GroupTheory.Subgroup.MulOpposite

/-!
# Cosets

This file develops the basic theory of left and right cosets.

## Main definitions

* `leftCoset a s`: the left coset `a * s` for an element `a : α` and a subset `s ⊆ α`, for an
* `rightCoset s a`: the right coset `s * a` for an element `a : α` and a subset `s ⊆ α`, for an
* `QuotientGroup.quotient s`: the quotient type representing the left cosets with respect to a
* `QuotientGroup.mk`: the canonical map from `α` to `α/s` for a subgroup `s` of `α`, for an
* `Subgroup.leftCosetEquivSubgroup`: the natural bijection between a left coset and the subgroup,

## Notation

* `a *l s`: for `leftCoset a s`.
* `a +l s`: for `leftAddCoset a s`.
* `s *r a`: for `rightCoset s a`.
* `s +r a`: for `rightAddCoset s a`.

* `G ⧸ H` is the quotient of the (additive) group `G` by the (additive) subgroup `H`
-/

open Set Function

variable {α: Type ?u.92864α : Type _: Type (?u.47374+1)Type _}

/-- The left coset `a * s` for an element `a : α` and a subset `s : Set α` -/
@[to_additive leftAddCoset: {α : Type u_1} → [inst : Add α] → α → Set α → Set αleftAddCoset "The left coset `a+s` for an element `a : α` and a subset `s : set α`"]
def leftCoset: {α : Type u_1} → [inst : Mul α] → α → Set α → Set αleftCoset [Mul: Type ?u.8 → Type ?u.8Mul α: Type ?u.5α] (a: αa : α: Type ?u.5α) (s: Set αs : Set: Type ?u.13 → Type ?u.13Set α: Type ?u.5α) : Set: Type ?u.16 → Type ?u.16Set α: Type ?u.5α :=
(fun x: ?m.31x => a: αa * x: ?m.31x) '' s: Set αs
#align left_coset leftCoset: {α : Type u_1} → [inst : Mul α] → α → Set α → Set αleftCoset

/-- The right coset `s * a` for an element `a : α` and a subset `s : Set α` -/
"The right coset `s+a` for an element `a : α` and a subset `s : set α`"]
def rightCoset: {α : Type u_1} → [inst : Mul α] → Set α → α → Set αrightCoset [Mul: Type ?u.137 → Type ?u.137Mul α: Type ?u.134α] (s: Set αs : Set: Type ?u.140 → Type ?u.140Set α: Type ?u.134α) (a: αa : α: Type ?u.134α) : Set: Type ?u.145 → Type ?u.145Set α: Type ?u.134α :=
(fun x: ?m.160x => x: ?m.160x * a: αa) '' s: Set αs
#align right_coset rightCoset: {α : Type u_1} → [inst : Mul α] → Set α → α → Set αrightCoset

@[inherit_doc]
scoped[Coset] infixl:70 " *l " => leftCoset: {α : Type u_1} → [inst : Mul α] → α → Set α → Set αleftCoset

@[inherit_doc]
scoped[Coset] infixl:70 " +l " => leftAddCoset: {α : Type u_1} → [inst : Add α] → α → Set α → Set αleftAddCoset

@[inherit_doc]
scoped[Coset] infixl:70 " *r " => rightCoset: {α : Type u_1} → [inst : Mul α] → Set α → α → Set αrightCoset

@[inherit_doc]
scoped[Coset] infixl:70 " +r " => rightAddCoset: {α : Type u_1} → [inst : Add α] → Set α → α → Set αrightAddCoset

open Coset

section CosetMul

variable [Mul: Type ?u.32123 → Type ?u.32123Mul α: Type ?u.31453α]

@[to_additive mem_leftAddCoset: ∀ {α : Type u_1} [inst : Add α] {s : Set α} {x : α} (a : α), x ∈ s → a + x ∈ a +l smem_leftAddCoset]
theorem mem_leftCoset: ∀ {α : Type u_1} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → a * x ∈ a *l smem_leftCoset {s: Set αs : Set: Type ?u.31465 → Type ?u.31465Set α: Type ?u.31459α} {x: αx : α: Type ?u.31459α} (a: αa : α: Type ?u.31459α) (hxS: x ∈ shxS : x: αx ∈ s: Set αs) : a: αa * x: αx ∈ a: αa *l s: Set αs :=
mem_image_of_mem: ∀ {α : Type ?u.31627} {β : Type ?u.31628} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' amem_image_of_mem (fun b: αb : α: Type ?u.31459α => a: αa * b: αb) hxS: x ∈ shxS
#align mem_left_coset mem_leftCoset: ∀ {α : Type u_1} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → a * x ∈ a *l smem_leftCoset
#align mem_left_add_coset mem_leftAddCoset: ∀ {α : Type u_1} [inst : Add α] {s : Set α} {x : α} (a : α), x ∈ s → a + x ∈ a +l smem_leftAddCoset

@[to_additive mem_rightAddCoset: ∀ {α : Type u_1} [inst : Add α] {s : Set α} {x : α} (a : α), x ∈ s → x + a ∈ s +r amem_rightAddCoset]
theorem mem_rightCoset: ∀ {s : Set α} {x : α} (a : α), x ∈ s → x * a ∈ s *r amem_rightCoset {s: Set αs : Set: Type ?u.31750 → Type ?u.31750Set α: Type ?u.31744α} {x: αx : α: Type ?u.31744α} (a: αa : α: Type ?u.31744α) (hxS: x ∈ shxS : x: αx ∈ s: Set αs) : x: αx * a: αa ∈ s: Set αs *r a: αa :=
mem_image_of_mem: ∀ {α : Type ?u.31913} {β : Type ?u.31914} (f : α → β) {x : α} {a : Set α}, x ∈ a → f x ∈ f '' amem_image_of_mem (fun b: αb : α: Type ?u.31744α => b: αb * a: αa) hxS: x ∈ shxS
#align mem_right_coset mem_rightCoset: ∀ {α : Type u_1} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → x * a ∈ s *r amem_rightCoset
#align mem_right_add_coset mem_rightAddCoset: ∀ {α : Type u_1} [inst : Add α] {s : Set α} {x : α} (a : α), x ∈ s → x + a ∈ s +r amem_rightAddCoset

/-- Equality of two left cosets `a * s` and `b * s`. -/
@[to_additive LeftAddCosetEquivalence: {α : Type u_1} → [inst : Add α] → Set α → α → α → PropLeftAddCosetEquivalence "Equality of two left cosets `a + s` and `b + s`."]
def LeftCosetEquivalence: {α : Type u_1} → [inst : Mul α] → Set α → α → α → PropLeftCosetEquivalence (s: Set αs : Set: Type ?u.32036 → Type ?u.32036Set α: Type ?u.32030α) (a: αa b: αb : α: Type ?u.32030α) :=
a: αa *l s: Set αs = b: αb *l s: Set αs
#align left_coset_equivalence LeftCosetEquivalence: {α : Type u_1} → [inst : Mul α] → Set α → α → α → PropLeftCosetEquivalence

theorem leftCosetEquivalence_rel: ∀ {α : Type u_1} [inst : Mul α] (s : Set α), Equivalence (LeftCosetEquivalence s)leftCosetEquivalence_rel (s: Set αs : Set: Type ?u.32126 → Type ?u.32126Set α: Type ?u.32120α) : Equivalence: {α : Sort ?u.32129} → (α → α → Prop) → PropEquivalence (LeftCosetEquivalence: {α : Type ?u.32131} → [inst : Mul α] → Set α → α → α → PropLeftCosetEquivalence s: Set αs) :=
@Equivalence.mk: ∀ {α : Sort ?u.32189} {r : α → α → Prop},
(∀ (x : α), r x x) → (∀ {x y : α}, r x y → r y x) → (∀ {x y z : α}, r x y → r y z → r x z) → Equivalence rEquivalence.mk _: Sort ?u.32189_ (LeftCosetEquivalence: {α : Type ?u.32191} → [inst : Mul α] → Set α → α → α → PropLeftCosetEquivalence s: Set αs) (fun _: ?m.32252_ => rfl: ∀ {α : Sort ?u.32254} {a : α}, a = arfl) Eq.symm: ∀ {α : Sort ?u.32264} {a b : α}, a = b → b = aEq.symm Eq.trans: ∀ {α : Sort ?u.32279} {a b c : α}, a = b → b = c → a = cEq.trans
#align left_coset_equivalence_rel leftCosetEquivalence_rel: ∀ {α : Type u_1} [inst : Mul α] (s : Set α), Equivalence (LeftCosetEquivalence s)leftCosetEquivalence_rel

/-- Equality of two right cosets `s * a` and `s * b`. -/
@[to_additive RightAddCosetEquivalence: {α : Type u_1} → [inst : Add α] → Set α → α → α → PropRightAddCosetEquivalence "Equality of two right cosets `s + a` and `s + b`."]
def RightCosetEquivalence: {α : Type u_1} → [inst : Mul α] → Set α → α → α → PropRightCosetEquivalence (s: Set αs : Set: Type ?u.32333 → Type ?u.32333Set α: Type ?u.32327α) (a: αa b: αb : α: Type ?u.32327α) :=
s: Set αs *r a: αa = s: Set αs *r b: αb
#align right_coset_equivalence RightCosetEquivalence: {α : Type u_1} → [inst : Mul α] → Set α → α → α → PropRightCosetEquivalence

theorem rightCosetEquivalence_rel: ∀ {α : Type u_1} [inst : Mul α] (s : Set α), Equivalence (RightCosetEquivalence s)rightCosetEquivalence_rel (s: Set αs : Set: Type ?u.32425 → Type ?u.32425Set α: Type ?u.32419α) : Equivalence: {α : Sort ?u.32428} → (α → α → Prop) → PropEquivalence (RightCosetEquivalence: {α : Type ?u.32430} → [inst : Mul α] → Set α → α → α → PropRightCosetEquivalence s: Set αs) :=
@Equivalence.mk: ∀ {α : Sort ?u.32488} {r : α → α → Prop},
(∀ (x : α), r x x) → (∀ {x y : α}, r x y → r y x) → (∀ {x y z : α}, r x y → r y z → r x z) → Equivalence rEquivalence.mk _: Sort ?u.32488_ (RightCosetEquivalence: {α : Type ?u.32490} → [inst : Mul α] → Set α → α → α → PropRightCosetEquivalence s: Set αs) (fun _a: ?m.32551_a => rfl: ∀ {α : Sort ?u.32553} {a : α}, a = arfl) Eq.symm: ∀ {α : Sort ?u.32563} {a b : α}, a = b → b = aEq.symm Eq.trans: ∀ {α : Sort ?u.32578} {a b c : α}, a = b → b = c → a = cEq.trans
#align right_coset_equivalence_rel rightCosetEquivalence_rel: ∀ {α : Type u_1} [inst : Mul α] (s : Set α), Equivalence (RightCosetEquivalence s)rightCosetEquivalence_rel

end CosetMul

section CosetSemigroup

variable [Semigroup: Type ?u.32635 → Type ?u.32635Semigroup α: Type ?u.32626α]

@[to_additive (attr := simp) leftAddCoset_assoc: ∀ {α : Type u_1} [inst : AddSemigroup α] (s : Set α) (a b : α), a +l (b +l s) = (a + b) +l sleftAddCoset_assoc]
theorem leftCoset_assoc: ∀ {α : Type u_1} [inst : Semigroup α] (s : Set α) (a b : α), a *l (b *l s) = a * b *l sleftCoset_assoc (s: Set αs : Set: Type ?u.32638 → Type ?u.32638Set α: Type ?u.32632α) (a: αa b: αb : α: Type ?u.32632α) : a: αa *l (b: αb *l s: Set αs) = a: αa * b: αb *l s: Set αs := byGoals accomplished! 🐙
α: Type u_1inst✝: Semigroup αs: Set αa, b: αa *l (b *l s) = a * b *l ssimp [leftCoset: {α : Type ?u.34181} → [inst : Mul α] → α → Set α → Set αleftCoset, rightCoset: {α : Type ?u.34196} → [inst : Mul α] → Set α → α → Set αrightCoset, (image_comp: ∀ {α : Type ?u.34212} {β : Type ?u.34214} {γ : Type ?u.34213} (f : β → γ) (g : α → β) (a : Set α),
f ∘ g '' a = f '' (g '' a)image_comp _: ?m.34216 → ?m.34217_ _: ?m.34215 → ?m.34216_ _: Set ?m.34215_).symm: ∀ {α : Sort ?u.34221} {a b : α}, a = b → b = asymm, Function.comp: {α : Sort ?u.34276} → {β : Sort ?u.34275} → {δ : Sort ?u.34274} → (β → δ) → (α → β) → α → δFunction.comp, mul_assoc: ∀ {G : Type ?u.34286} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc]Goals accomplished! 🐙
#align left_coset_assoc leftCoset_assoc: ∀ {α : Type u_1} [inst : Semigroup α] (s : Set α) (a b : α), a *l (b *l s) = a * b *l sleftCoset_assoc
#align left_add_coset_assoc leftAddCoset_assoc: ∀ {α : Type u_1} [inst : AddSemigroup α] (s : Set α) (a b : α), a +l (b +l s) = (a + b) +l sleftAddCoset_assoc

@[to_additive (attr := simp) rightAddCoset_assoc: ∀ {α : Type u_1} [inst : AddSemigroup α] (s : Set α) (a b : α), s +r a +r b = s +r (a + b)rightAddCoset_assoc]
theorem rightCoset_assoc: ∀ (s : Set α) (a b : α), s *r a *r b = s *r (a * b)rightCoset_assoc (s: Set αs : Set: Type ?u.35763 → Type ?u.35763Set α: Type ?u.35757α) (a: αa b: αb : α: Type ?u.35757α) : s: Set αs *r a: αa *r b: αb = s: Set αs *r (a: αa * b: αb) := byGoals accomplished! 🐙
α: Type u_1inst✝: Semigroup αs: Set αa, b: αs *r a *r b = s *r (a * b)simp [leftCoset: {α : Type ?u.37309} → [inst : Mul α] → α → Set α → Set αleftCoset, rightCoset: {α : Type ?u.37324} → [inst : Mul α] → Set α → α → Set αrightCoset, (image_comp: ∀ {α : Type ?u.37340} {β : Type ?u.37342} {γ : Type ?u.37341} (f : β → γ) (g : α → β) (a : Set α),
f ∘ g '' a = f '' (g '' a)image_comp _: ?m.37344 → ?m.37345_ _: ?m.37343 → ?m.37344_ _: Set ?m.37343_).symm: ∀ {α : Sort ?u.37349} {a b : α}, a = b → b = asymm, Function.comp: {α : Sort ?u.37404} → {β : Sort ?u.37403} → {δ : Sort ?u.37402} → (β → δ) → (α → β) → α → δFunction.comp, mul_assoc: ∀ {G : Type ?u.37414} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc]Goals accomplished! 🐙
#align right_coset_assoc rightCoset_assoc: ∀ {α : Type u_1} [inst : Semigroup α] (s : Set α) (a b : α), s *r a *r b = s *r (a * b)rightCoset_assoc
#align right_add_coset_assoc rightAddCoset_assoc: ∀ {α : Type u_1} [inst : AddSemigroup α] (s : Set α) (a b : α), s +r a +r b = s +r (a + b)rightAddCoset_assoc

theorem leftCoset_rightCoset: ∀ {α : Type u_1} [inst : Semigroup α] (s : Set α) (a b : α), a *l s *r b = a *l (s *r b)leftCoset_rightCoset (s: Set αs : Set: Type ?u.39268 → Type ?u.39268Set α: Type ?u.39262α) (a: αa b: αb : α: Type ?u.39262α) : a: αa *l s: Set αs *r b: αb = a: αa *l (s: Set αs *r b: αb) := byGoals accomplished! 🐙
α: Type u_1inst✝: Semigroup αs: Set αa, b: αa *l s *r b = a *l (s *r b)simp [leftCoset: {α : Type ?u.39931} → [inst : Mul α] → α → Set α → Set αleftCoset, rightCoset: {α : Type ?u.39946} → [inst : Mul α] → Set α → α → Set αrightCoset, (image_comp: ∀ {α : Type ?u.39962} {β : Type ?u.39964} {γ : Type ?u.39963} (f : β → γ) (g : α → β) (a : Set α),
f ∘ g '' a = f '' (g '' a)image_comp _: ?m.39966 → ?m.39967_ _: ?m.39965 → ?m.39966_ _: Set ?m.39965_).symm: ∀ {α : Sort ?u.39971} {a b : α}, a = b → b = asymm, Function.comp: {α : Sort ?u.40026} → {β : Sort ?u.40025} → {δ : Sort ?u.40024} → (β → δ) → (α → β) → α → δFunction.comp, mul_assoc: ∀ {G : Type ?u.40036} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc]Goals accomplished! 🐙
#align left_coset_right_coset leftCoset_rightCoset: ∀ {α : Type u_1} [inst : Semigroup α] (s : Set α) (a b : α), a *l s *r b = a *l (s *r b)leftCoset_rightCoset

end CosetSemigroup

section CosetMonoid

variable [Monoid: Type ?u.41892 → Type ?u.41892Monoid α: Type ?u.41889α] (s: Set αs : Set: Type ?u.41886 → Type ?u.41886Set α: Type ?u.44483α)

@[to_additive (attr := simp) zero_leftAddCoset: ∀ {α : Type u_1} [inst : AddMonoid α] (s : Set α), 0 +l s = szero_leftAddCoset]
theorem one_leftCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Set α), 1 *l s = sone_leftCoset : 1: ?m.419031 *l s: Set αs = s: Set αs :=
Set.ext: ∀ {α : Type ?u.42640} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = bSet.ext <| byGoals accomplished! 🐙 α: Type u_1inst✝: Monoid αs: Set α∀ (x : α), x ∈ 1 *l s ↔ x ∈ ssimp [leftCoset: {α : Type ?u.42649} → [inst : Mul α] → α → Set α → Set αleftCoset]Goals accomplished! 🐙
#align one_left_coset one_leftCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Set α), 1 *l s = sone_leftCoset

@[to_additive (attr := simp) rightAddCoset_zero: ∀ {α : Type u_1} [inst : AddMonoid α] (s : Set α), s +r 0 = srightAddCoset_zero]
theorem rightCoset_one: ∀ {α : Type u_1} [inst : Monoid α] (s : Set α), s *r 1 = srightCoset_one : s: Set αs *r 1: ?m.445001 = s: Set αs :=
Set.ext: ∀ {α : Type ?u.45227} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = bSet.ext <| byGoals accomplished! 🐙 α: Type u_1inst✝: Monoid αs: Set α∀ (x : α), x ∈ s *r 1 ↔ x ∈ ssimp [rightCoset: {α : Type ?u.45236} → [inst : Mul α] → Set α → α → Set αrightCoset]Goals accomplished! 🐙
#align right_coset_one rightCoset_one: ∀ {α : Type u_1} [inst : Monoid α] (s : Set α), s *r 1 = srightCoset_one

end CosetMonoid

section CosetSubmonoid

open Submonoid

variable [Monoid: Type ?u.53809 → Type ?u.53809Monoid α: Type ?u.47070α] (s: Submonoid αs : Submonoid: (M : Type ?u.47076) → [inst : MulOneClass M] → Type ?u.47076Submonoid α: Type ?u.47070α)

theorem mem_own_leftCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ a *l ↑smem_own_leftCoset (a: αa : α: Type ?u.47374α) : a: αa ∈ a: αa *l s: Submonoid αs :=
suffices a: αa * 1: ?m.482541 ∈ a: αa *l s: Submonoid αs by simpaGoals accomplished! 🐙
mem_leftCoset: ∀ {α : Type ?u.49430} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → a * x ∈ a *l smem_leftCoset a: αa (one_mem: ∀ {S : Type ?u.49831} {M : Type ?u.49830} [inst : One M] [inst_1 : SetLike S M] [self : OneMemClass S M] (s : S), 1 ∈ sone_mem s: Submonoid αs : 1: ?m.494721 ∈ s: Submonoid αs)
#align mem_own_left_coset mem_own_leftCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ a *l ↑smem_own_leftCoset

theorem mem_own_rightCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ ↑s *r amem_own_rightCoset (a: αa : α: Type ?u.50588α) : a: αa ∈ (s: Submonoid αs : Set: Type ?u.50948 → Type ?u.50948Set α: Type ?u.50588α) *r a: αa :=
suffices 1: ?m.514701 * a: αa ∈ (s: Submonoid αs : Set: Type ?u.52240 → Type ?u.52240Set α: Type ?u.50588α) *r a: αa by simpaGoals accomplished! 🐙
mem_rightCoset: ∀ {α : Type ?u.52648} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → x * a ∈ s *r amem_rightCoset a: αa (one_mem: ∀ {S : Type ?u.53049} {M : Type ?u.53048} [inst : One M] [inst_1 : SetLike S M] [self : OneMemClass S M] (s : S), 1 ∈ sone_mem s: Submonoid αs : 1: ?m.526901 ∈ s: Submonoid αs)
#align mem_own_right_coset mem_own_rightCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ ↑s *r amem_own_rightCoset

theorem mem_leftCoset_leftCoset: ∀ {a : α}, a *l ↑s = ↑s → a ∈ smem_leftCoset_leftCoset {a: αa : α: Type ?u.53806α} (ha: a *l ↑s = ↑sha : a: αa *l s: Submonoid αs = s: Submonoid αs) : a: αa ∈ s: Submonoid αs := byGoals accomplished! 🐙
α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: a *l ↑s = ↑sa ∈ srw [α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: a *l ↑s = ↑sa ∈ s← SetLike.mem_coe: ∀ {A : Type ?u.54708} {B : Type ?u.54707} [i : SetLike A B] {p : A} {x : B}, x ∈ ↑p ↔ x ∈ pSetLike.mem_coe,α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: a *l ↑s = ↑sa ∈ ↑s α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: a *l ↑s = ↑sa ∈ s← ha: a *l ↑s = ↑shaα: Type u_1inst✝: Monoid αs: Submonoid αa: αha: a *l ↑s = ↑sa ∈ a *l ↑s]α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: a *l ↑s = ↑sa ∈ a *l ↑s;α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: a *l ↑s = ↑sa ∈ a *l ↑s α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: a *l ↑s = ↑sa ∈ sexact mem_own_leftCoset: ∀ {α : Type ?u.54766} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ a *l ↑smem_own_leftCoset s: Submonoid αs a: αaGoals accomplished! 🐙
#align mem_left_coset_left_coset mem_leftCoset_leftCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) {a : α}, a *l ↑s = ↑s → a ∈ smem_leftCoset_leftCoset

theorem mem_rightCoset_rightCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) {a : α}, ↑s *r a = ↑s → a ∈ smem_rightCoset_rightCoset {a: αa : α: Type ?u.54812α} (ha: ↑s *r a = ↑sha : (s: Submonoid αs : Set: Type ?u.55123 → Type ?u.55123Set α: Type ?u.54812α) *r a: αa = s: Submonoid αs) : a: αa ∈ s: Submonoid αs := byGoals accomplished! 🐙
α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: ↑s *r a = ↑sa ∈ srw [α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: ↑s *r a = ↑sa ∈ s← SetLike.mem_coe: ∀ {A : Type ?u.55716} {B : Type ?u.55715} [i : SetLike A B] {p : A} {x : B}, x ∈ ↑p ↔ x ∈ pSetLike.mem_coe,α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: ↑s *r a = ↑sa ∈ ↑s α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: ↑s *r a = ↑sa ∈ s← ha: ↑s *r a = ↑shaα: Type u_1inst✝: Monoid αs: Submonoid αa: αha: ↑s *r a = ↑sa ∈ ↑s *r a]α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: ↑s *r a = ↑sa ∈ ↑s *r a;α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: ↑s *r a = ↑sa ∈ ↑s *r a α: Type u_1inst✝: Monoid αs: Submonoid αa: αha: ↑s *r a = ↑sa ∈ sexact mem_own_rightCoset: ∀ {α : Type ?u.55774} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ ↑s *r amem_own_rightCoset s: Submonoid αs a: αaGoals accomplished! 🐙
#align mem_right_coset_right_coset mem_rightCoset_rightCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) {a : α}, ↑s *r a = ↑s → a ∈ smem_rightCoset_rightCoset

end CosetSubmonoid

section CosetGroup

variable [Group: Type ?u.55834 → Type ?u.55834Group α: Type ?u.55820α] {s: Set αs : Set: Type ?u.55837 → Type ?u.55837Set α: Type ?u.55820α} {x: αx : α: Type ?u.58767α}

@[to_additive mem_leftAddCoset_iff: ∀ {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α), x ∈ a +l s ↔ -a + x ∈ smem_leftAddCoset_iff]
theorem mem_leftCoset_iff: ∀ (a : α), x ∈ a *l s ↔ a⁻¹ * x ∈ smem_leftCoset_iff (a: αa : α: Type ?u.55831α) : x: αx ∈ a: αa *l s: Set αs ↔ a: αa⁻¹ * x: αx ∈ s: Set αs :=
Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)Iff.intro (fun ⟨b: αb, hb: b ∈ shb, Eq: (fun x => a * x) b = xEq⟩ => byGoals accomplished! 🐙 α: Type u_1inst✝: Group αs: Set αx, a: αx✝: x ∈ a *l sb: αhb: b ∈ sEq: (fun x => a * x) b = xa⁻¹ * x ∈ ssimp [Eq: (fun x => a * x) b = xEq.symm: ∀ {α : Sort ?u.58155} {a b : α}, a = b → b = asymm, hb: b ∈ shb]Goals accomplished! 🐙) fun h: ?m.57254h => ⟨a: αa⁻¹ * x: αx, h: ?m.57254h, byGoals accomplished! 🐙 α: Type u_1inst✝: Group αs: Set αx, a: αh: a⁻¹ * x ∈ s(fun x => a * x) (a⁻¹ * x) = xsimpGoals accomplished! 🐙⟩
#align mem_left_coset_iff mem_leftCoset_iff: ∀ {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ a *l s ↔ a⁻¹ * x ∈ smem_leftCoset_iff
#align mem_left_add_coset_iff mem_leftAddCoset_iff: ∀ {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α), x ∈ a +l s ↔ -a + x ∈ smem_leftAddCoset_iff

@[to_additive mem_rightAddCoset_iff: ∀ {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α), x ∈ s +r a ↔ x + -a ∈ smem_rightAddCoset_iff]
theorem mem_rightCoset_iff: ∀ {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ s *r a ↔ x * a⁻¹ ∈ smem_rightCoset_iff (a: αa : α: Type ?u.58767α) : x: αx ∈ s: Set αs *r a: αa ↔ x: αx * a: αa⁻¹ ∈ s: Set αs :=
Iff.intro: ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)Iff.intro (fun ⟨b: αb, hb: b ∈ shb, Eq: (fun x => x * a) b = xEq⟩ => byGoals accomplished! 🐙 α: Type u_1inst✝: Group αs: Set αx, a: αx✝: x ∈ s *r ab: αhb: b ∈ sEq: (fun x => x * a) b = xx * a⁻¹ ∈ ssimp [Eq: (fun x => x * a) b = xEq.symm: ∀ {α : Sort ?u.61092} {a b : α}, a = b → b = asymm, hb: b ∈ shb]Goals accomplished! 🐙) fun h: ?m.60191h => ⟨x: αx * a: αa⁻¹, h: ?m.60191h, byGoals accomplished! 🐙 α: Type u_1inst✝: Group αs: Set αx, a: αh: x * a⁻¹ ∈ s(fun x => x * a) (x * a⁻¹) = xsimpGoals accomplished! 🐙⟩
#align mem_right_coset_iff mem_rightCoset_iff: ∀ {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ s *r a ↔ x * a⁻¹ ∈ smem_rightCoset_iff
#align mem_right_add_coset_iff mem_rightAddCoset_iff: ∀ {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α), x ∈ s +r a ↔ x + -a ∈ smem_rightAddCoset_iff

end CosetGroup

section CosetSubgroup

open Subgroup

variable [Group: Type ?u.68680 → Type ?u.68680Group α: Type ?u.61544α] (s: Subgroup αs : Subgroup: (G : Type ?u.67229) → [inst : Group G] → Type ?u.67229Subgroup α: Type ?u.61544α)

theorem leftCoset_mem_leftCoset: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → a *l ↑s = ↑sleftCoset_mem_leftCoset {a: αa : α: Type ?u.61558α} (ha: a ∈ sha : a: αa ∈ s: Subgroup αs) : a: αa *l s: Subgroup αs = s: Subgroup αs :=
Set.ext: ∀ {α : Type ?u.62185} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = bSet.ext <| byGoals accomplished! 🐙 α: Type u_1inst✝: Group αs: Subgroup αa: αha: a ∈ s∀ (x : α), x ∈ a *l ↑s ↔ x ∈ ↑ssimp [mem_leftCoset_iff: ∀ {α : Type ?u.62195} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ a *l s ↔ a⁻¹ * x ∈ smem_leftCoset_iff, mul_mem_cancel_left: ∀ {G : Type ?u.62228} [inst : Group G] {S : Type ?u.62229} {H : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G]
{x y : G}, x ∈ H → (x * y ∈ H ↔ y ∈ H)mul_mem_cancel_left (s: Subgroup αs.inv_mem: ∀ {G : Type ?u.62238} [inst : Group G] (H : Subgroup G) {x : G}, x ∈ H → x⁻¹ ∈ Hinv_mem ha: a ∈ sha)]Goals accomplished! 🐙
#align left_coset_mem_left_coset leftCoset_mem_leftCoset: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → a *l ↑s = ↑sleftCoset_mem_leftCoset

theorem rightCoset_mem_rightCoset: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → ↑s *r a = ↑srightCoset_mem_rightCoset {a: αa : α: Type ?u.63747α} (ha: a ∈ sha : a: αa ∈ s: Subgroup αs) : (s: Subgroup αs : Set: Type ?u.63813 → Type ?u.63813Set α: Type ?u.63747α) *r a: αa = s: Subgroup αs :=
Set.ext: ∀ {α : Type ?u.64376} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = bSet.ext fun b: ?m.64385b => byGoals accomplished! 🐙 α: Type u_1inst✝: Group αs: Subgroup αa: αha: a ∈ sb: αb ∈ ↑s *r a ↔ b ∈ ↑ssimp [mem_rightCoset_iff: ∀ {α : Type ?u.64394} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ s *r a ↔ x * a⁻¹ ∈ smem_rightCoset_iff, mul_mem_cancel_right: ∀ {G : Type ?u.64427} [inst : Group G] {S : Type ?u.64428} {H : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G]
{x y : G}, x ∈ H → (y * x ∈ H ↔ y ∈ H)mul_mem_cancel_right (s: Subgroup αs.inv_mem: ∀ {G : Type ?u.64437} [inst : Group G] (H : Subgroup G) {x : G}, x ∈ H → x⁻¹ ∈ Hinv_mem ha: a ∈ sha)]Goals accomplished! 🐙
#align right_coset_mem_right_coset rightCoset_mem_rightCoset: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → ↑s *r a = ↑srightCoset_mem_rightCoset

@[to_additive: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (a : α), AddAction.orbit { x // x ∈ s } a = ↑s +r ato_additive]
theorem orbit_subgroup_eq_rightCoset: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) (a : α), MulAction.orbit { x // x ∈ s } a = ↑s *r aorbit_subgroup_eq_rightCoset (a: αa : α: Type ?u.64873α) : MulAction.orbit: (α : Type ?u.64891) → {β : Type ?u.64890} → [inst : Monoid α] → [inst : MulAction α β] → β → Set βMulAction.orbit s: Subgroup αs a: αa = s: Subgroup αs *r a: αa :=
Set.ext: ∀ {α : Type ?u.66584} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = bSet.ext fun _b: ?m.66593_b => ⟨fun ⟨c: { x // x ∈ s }c, d: (fun x => x • a) c = _bd⟩ => ⟨c: { x // x ∈ s }c, c: { x // x ∈ s }c.2: ∀ {α : Sort ?u.66782} {p : α → Prop} (self : Subtype p), p ↑self2, d: (fun x => x • a) c = _bd⟩, fun ⟨c: αc, d: c ∈ ↑sd, e: (fun x => x * a) c = _be⟩ => ⟨⟨c: αc, d: c ∈ ↑sd⟩, e: (fun x => x * a) c = _be⟩⟩
#align orbit_subgroup_eq_right_coset orbit_subgroup_eq_rightCoset: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) (a : α), MulAction.orbit { x // x ∈ s } a = ↑s *r aorbit_subgroup_eq_rightCoset

@[to_additive: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {a : α}, a ∈ s → AddAction.orbit { x // x ∈ s } a = ↑sto_additive]
theorem orbit_subgroup_eq_self_of_mem: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → MulAction.orbit { x // x ∈ s } a = ↑sorbit_subgroup_eq_self_of_mem {a: αa : α: Type ?u.67223α} (ha: a ∈ sha : a: αa ∈ s: Subgroup αs) : MulAction.orbit: (α : Type ?u.67286) → {β : Type ?u.67285} → [inst : Monoid α] → [inst : MulAction α β] → β → Set βMulAction.orbit s: Subgroup αs a: αa = s: Subgroup αs :=
(orbit_subgroup_eq_rightCoset: ∀ {α : Type ?u.68612} [inst : Group α] (s : Subgroup α) (a : α), MulAction.orbit { x // x ∈ s } a = ↑s *r aorbit_subgroup_eq_rightCoset s: Subgroup αs a: αa).trans: ∀ {α : Sort ?u.68623} {a b c : α}, a = b → b = c → a = ctrans (rightCoset_mem_rightCoset: ∀ {α : Type ?u.68637} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → ↑s *r a = ↑srightCoset_mem_rightCoset s: Subgroup αs ha: a ∈ sha)
#align orbit_subgroup_eq_self_of_mem orbit_subgroup_eq_self_of_mem: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → MulAction.orbit { x // x ∈ s } a = ↑sorbit_subgroup_eq_self_of_mem
#align orbit_add_subgroup_eq_self_of_mem orbit_addSubgroup_eq_self_of_mem: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {a : α}, a ∈ s → AddAction.orbit { x // x ∈ s } a = ↑sorbit_addSubgroup_eq_self_of_mem

theorem orbit_subgroup_one_eq_self: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), MulAction.orbit { x // x ∈ s } 1 = ↑sorbit_subgroup_one_eq_self : MulAction.orbit: (α : Type ?u.68693) → {β : Type ?u.68692} → [inst : Monoid α] → [inst : MulAction α β] → β → Set βMulAction.orbit s: Subgroup αs (1: ?m.688441 : α: Type ?u.68677α) = s: Subgroup αs :=
orbit_subgroup_eq_self_of_mem: ∀ {α : Type ?u.70287} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → MulAction.orbit { x // x ∈ s } a = ↑sorbit_subgroup_eq_self_of_mem s: Subgroup αs s: Subgroup αs.one_mem: ∀ {G : Type ?u.70307} [inst : Group G] (H : Subgroup G), 1 ∈ Hone_mem
#align orbit_subgroup_one_eq_self orbit_subgroup_one_eq_self: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), MulAction.orbit { x // x ∈ s } 1 = ↑sorbit_subgroup_one_eq_self

theorem eq_cosets_of_normal: Normal s → ∀ (g : α), g *l ↑s = ↑s *r geq_cosets_of_normal (N: Normal sN : s: Subgroup αs.Normal: {G : Type ?u.70344} → [inst : Group G] → Subgroup G → PropNormal) (g: αg : α: Type ?u.70330α) : g: αg *l s: Subgroup αs = s: Subgroup αs *r g: αg :=
Set.ext: ∀ {α : Type ?u.70958} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = bSet.ext fun a: ?m.70967a => byGoals accomplished! 🐙 α: Type u_1inst✝: Group αs: Subgroup αN: Normal sg, a: αa ∈ g *l ↑s ↔ a ∈ ↑s *r gsimp [mem_leftCoset_iff: ∀ {α : Type ?u.70976} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ a *l s ↔ a⁻¹ * x ∈ smem_leftCoset_iff, mem_rightCoset_iff: ∀ {α : Type ?u.71008} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ s *r a ↔ x * a⁻¹ ∈ smem_rightCoset_iff]α: Type u_1inst✝: Group αs: Subgroup αN: Normal sg, a: αg⁻¹ * a ∈ s ↔ a * g⁻¹ ∈ s;α: Type u_1inst✝: Group αs: Subgroup αN: Normal sg, a: αg⁻¹ * a ∈ s ↔ a * g⁻¹ ∈ s α: Type u_1inst✝: Group αs: Subgroup αN: Normal sg, a: αa ∈ g *l ↑s ↔ a ∈ ↑s *r grw [α: Type u_1inst✝: Group αs: Subgroup αN: Normal sg, a: αg⁻¹ * a ∈ s ↔ a * g⁻¹ ∈ sN: Normal sN.mem_comm_iff: ∀ {G : Type ?u.71530} [inst : Group G] {H : Subgroup G}, Normal H → ∀ {a b : G}, a * b ∈ H ↔ b * a ∈ Hmem_comm_iffα: Type u_1inst✝: Group αs: Subgroup αN: Normal sg, a: αa * g⁻¹ ∈ s ↔ a * g⁻¹ ∈ s]Goals accomplished! 🐙
#align eq_cosets_of_normal eq_cosets_of_normal: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Normal s → ∀ (g : α), g *l ↑s = ↑s *r geq_cosets_of_normal

theorem normal_of_eq_cosets: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), (∀ (g : α), g *l ↑s = ↑s *r g) → Normal snormal_of_eq_cosets (h: ∀ (g : α), g *l ↑s = ↑s *r gh : ∀ g: αg : α: Type ?u.71586α, g: αg *l s: Subgroup αs = s: Subgroup αs *r g: αg) : s: Subgroup αs.Normal: {G : Type ?u.72204} → [inst : Group G] → Subgroup G → PropNormal :=
⟨fun a: ?m.72251a ha: ?m.72254ha g: ?m.72257g =>
show g: ?m.72257g * a: ?m.72251a * g: ?m.72257g⁻¹ ∈ (s: Subgroup αs : Set: Type ?u.73488 → Type ?u.73488Set α: Type ?u.71586α) by rw [α: Type u_1inst✝: Group αs: Subgroup αh: ∀ (g : α), g *l ↑s = ↑s *r ga: αha: a ∈ sg: αg * a * g⁻¹ ∈ ↑s← mem_rightCoset_iff: ∀ {α : Type ?u.73606} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ s *r a ↔ x * a⁻¹ ∈ smem_rightCoset_iff,α: Type u_1inst✝: Group αs: Subgroup αh: ∀ (g : α), g *l ↑s = ↑s *r ga: αha: a ∈ sg: αg * a ∈ ↑s *r g α: Type u_1inst✝: Group αs: Subgroup αh: ∀ (g : α), g *l ↑s = ↑s *r ga: αha: a ∈ sg: αg * a * g⁻¹ ∈ ↑s← h: ∀ (g : α), g *l ↑s = ↑s *r ghα: Type u_1inst✝: Group αs: Subgroup αh: ∀ (g : α), g *l ↑s = ↑s *r ga: αha: a ∈ sg: αg * a ∈ g *l ↑s]α: Type u_1inst✝: Group αs: Subgroup αh: ∀ (g : α), g *l ↑s = ↑s *r ga: αha: a ∈ sg: αg * a ∈ g *l ↑s;α: Type u_1inst✝: Group αs: Subgroup αh: ∀ (g : α), g *l ↑s = ↑s *r ga: αha: a ∈ sg: αg * a ∈ g *l ↑s α: Type u_1inst✝: Group αs: Subgroup αh: ∀ (g : α), g *l ↑s = ↑s *r ga: αha: a ∈ sg: αg * a * g⁻¹ ∈ ↑sexact mem_leftCoset: ∀ {α : Type ?u.73694} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → a * x ∈ a *l smem_leftCoset g: αg ha: a ∈ shaGoals accomplished! 🐙⟩
#align normal_of_eq_cosets normal_of_eq_cosets: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), (∀ (g : α), g *l ↑s = ↑s *r g) → Normal snormal_of_eq_cosets

theorem normal_iff_eq_cosets: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Normal s ↔ ∀ (g : α), g *l ↑s = ↑s *r gnormal_iff_eq_cosets : s: Subgroup αs.Normal: {G : Type ?u.74085} → [inst : Group G] → Subgroup G → PropNormal ↔ ∀ g: αg : α: Type ?u.74071α, g: αg *l s: Subgroup αs = s: Subgroup αs *r g: αg :=
⟨@eq_cosets_of_normal: ∀ {α : Type ?u.74706} [inst : Group α] (s : Subgroup α), Normal s → ∀ (g : α), g *l ↑s = ↑s *r geq_cosets_of_normal _: Type ?u.74706_ _ s: Subgroup αs, normal_of_eq_cosets: ∀ {α : Type ?u.74727} [inst : Group α] (s : Subgroup α), (∀ (g : α), g *l ↑s = ↑s *r g) → Normal snormal_of_eq_cosets s: Subgroup αs⟩
#align normal_iff_eq_cosets normal_iff_eq_cosets: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Normal s ↔ ∀ (g : α), g *l ↑s = ↑s *r gnormal_iff_eq_cosets

@[to_additive leftAddCoset_eq_iff: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {x y : α}, x +l ↑s = y +l ↑s ↔ -x + y ∈ sleftAddCoset_eq_iff]
theorem leftCoset_eq_iff: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {x y : α}, x *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ sleftCoset_eq_iff {x: αx y: αy : α: Type ?u.74756α} : leftCoset: {α : Type ?u.74775} → [inst : Mul α] → α → Set α → Set αleftCoset x: αx s: Subgroup αs = leftCoset: {α : Type ?u.75282} → [inst : Mul α] → α → Set α → Set αleftCoset y: αy s: Subgroup αs ↔ x: αx⁻¹ * y: αy ∈ s: Subgroup αs := byGoals accomplished! 🐙
α: Type u_1inst✝: Group αs: Subgroup αx, y: αx *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ srw [α: Type u_1inst✝: Group αs: Subgroup αx, y: αx *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ sSet.ext_iff: ∀ {α : Type ?u.76092} {s t : Set α}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ tSet.ext_iffα: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x_1 ∈ x *l ↑s ↔ x_1 ∈ y *l ↑s) ↔ x⁻¹ * y ∈ s]α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x_1 ∈ x *l ↑s ↔ x_1 ∈ y *l ↑s) ↔ x⁻¹ * y ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αx *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ ssimp_rw [α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x_1 ∈ x *l ↑s ↔ x_1 ∈ y *l ↑s) ↔ x⁻¹ * y ∈ smem_leftCoset_iff: ∀ {α : Type ?u.76279} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ a *l s ↔ a⁻¹ * x ∈ smem_leftCoset_iff,α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x⁻¹ * x_1 ∈ ↑s ↔ y⁻¹ * x_1 ∈ ↑s) ↔ x⁻¹ * y ∈ s α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x_1 ∈ x *l ↑s ↔ x_1 ∈ y *l ↑s) ↔ x⁻¹ * y ∈ sSetLike.mem_coeα: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s]α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αx *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ sconstructorα: Type u_1inst✝: Group αs: Subgroup αx, y: αmp(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ sα: Type u_1inst✝: Group αs: Subgroup αx, y: αmprx⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αx *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ s·α: Type u_1inst✝: Group αs: Subgroup αx, y: αmp(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ s α: Type u_1inst✝: Group αs: Subgroup αx, y: αmp(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ sα: Type u_1inst✝: Group αs: Subgroup αx, y: αmprx⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ sintro h: ?ahα: Type u_1inst✝: Group αs: Subgroup αx, y: αh: ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ smpx⁻¹ * y ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αmp(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ sapply (h: ?ah y: αy).mpr: ∀ {a b : Prop}, (a ↔ b) → b → amprα: Type u_1inst✝: Group αs: Subgroup αx, y: αh: ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ smpy⁻¹ * y ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αmp(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ srw [α: Type u_1inst✝: Group αs: Subgroup αx, y: αh: ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ smpy⁻¹ * y ∈ smul_left_inv: ∀ {G : Type ?u.76609} [inst : Group G] (a : G), a⁻¹ * a = 1mul_left_invα: Type u_1inst✝: Group αs: Subgroup αx, y: αh: ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ smp1 ∈ s]α: Type u_1inst✝: Group αs: Subgroup αx, y: αh: ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ smp1 ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αmp(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ sexact s: Subgroup αs.one_mem: ∀ {G : Type ?u.76662} [inst : Group G] (H : Subgroup G), 1 ∈ Hone_memGoals accomplished! 🐙
α: Type u_1inst✝: Group αs: Subgroup αx, y: αx *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ s·α: Type u_1inst✝: Group αs: Subgroup αx, y: αmprx⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s α: Type u_1inst✝: Group αs: Subgroup αx, y: αmprx⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ sintro h: ?bh z: αzα: Type u_1inst✝: Group αs: Subgroup αx, y: αh: x⁻¹ * y ∈ sz: αmprx⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αmprx⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ srw [α: Type u_1inst✝: Group αs: Subgroup αx, y: αh: x⁻¹ * y ∈ sz: αmprx⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s← mul_inv_cancel_right: ∀ {G : Type ?u.76680} [inst : Group G] (a b : G), a * b * b⁻¹ = amul_inv_cancel_right x: αx⁻¹ y: αyα: Type u_1inst✝: Group αs: Subgroup αx, y: αh: x⁻¹ * y ∈ sz: αmprx⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s]α: Type u_1inst✝: Group αs: Subgroup αx, y: αh: x⁻¹ * y ∈ sz: αmprx⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αmprx⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ srw [α: Type u_1inst✝: Group αs: Subgroup αx, y: αh: x⁻¹ * y ∈ sz: αmprx⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ smul_assoc: ∀ {G : Type ?u.76856} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assocα: Type u_1inst✝: Group αs: Subgroup αx, y: αh: x⁻¹ * y ∈ sz: αmprx⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s]α: Type u_1inst✝: Group αs: Subgroup αx, y: αh: x⁻¹ * y ∈ sz: αmprx⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αmprx⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ sexact s: Subgroup αs.mul_mem_cancel_left: ∀ {G : Type ?u.77240} [inst : Group G] (H : Subgroup G) {x y : G}, x ∈ H → (x * y ∈ H ↔ y ∈ H)mul_mem_cancel_left h: ?bhGoals accomplished! 🐙
#align left_coset_eq_iff leftCoset_eq_iff: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {x y : α}, x *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ sleftCoset_eq_iff
#align left_add_coset_eq_iff leftAddCoset_eq_iff: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {x y : α}, x +l ↑s = y +l ↑s ↔ -x + y ∈ sleftAddCoset_eq_iff

@[to_additive rightAddCoset_eq_iff: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {x y : α}, ↑s +r x = ↑s +r y ↔ y + -x ∈ srightAddCoset_eq_iff]
theorem rightCoset_eq_iff: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {x y : α}, ↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ srightCoset_eq_iff {x: αx y: αy : α: Type ?u.77349α} : rightCoset: {α : Type ?u.77368} → [inst : Mul α] → Set α → α → Set αrightCoset (↑s: Subgroup αs) x: αx = rightCoset: {α : Type ?u.77958} → [inst : Mul α] → Set α → α → Set αrightCoset s: Subgroup αs y: αy ↔ y: αy * x: αx⁻¹ ∈ s: Subgroup αs := byGoals accomplished! 🐙
α: Type u_1inst✝: Group αs: Subgroup αx, y: α↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ srw [α: Type u_1inst✝: Group αs: Subgroup αx, y: α↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ sSet.ext_iff: ∀ {α : Type ?u.78852} {s t : Set α}, s = t ↔ ∀ (x : α), x ∈ s ↔ x ∈ tSet.ext_iffα: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x_1 ∈ ↑s *r x ↔ x_1 ∈ ↑s *r y) ↔ y * x⁻¹ ∈ s]α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x_1 ∈ ↑s *r x ↔ x_1 ∈ ↑s *r y) ↔ y * x⁻¹ ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: α↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ ssimp_rw [α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x_1 ∈ ↑s *r x ↔ x_1 ∈ ↑s *r y) ↔ y * x⁻¹ ∈ smem_rightCoset_iff: ∀ {α : Type ?u.79039} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ s *r a ↔ x * a⁻¹ ∈ smem_rightCoset_iff,α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x_1 * x⁻¹ ∈ ↑s ↔ x_1 * y⁻¹ ∈ ↑s) ↔ y * x⁻¹ ∈ s α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x_1 ∈ ↑s *r x ↔ x_1 ∈ ↑s *r y) ↔ y * x⁻¹ ∈ sSetLike.mem_coeα: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s]α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: α↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ sconstructorα: Type u_1inst✝: Group αs: Subgroup αx, y: αmp(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ sα: Type u_1inst✝: Group αs: Subgroup αx, y: αmpry * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: α↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ s·α: Type u_1inst✝: Group αs: Subgroup αx, y: αmp(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s α: Type u_1inst✝: Group αs: Subgroup αx, y: αmp(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ sα: Type u_1inst✝: Group αs: Subgroup αx, y: αmpry * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ sintro h: ?ahα: Type u_1inst✝: Group αs: Subgroup αx, y: αh: ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ smpy * x⁻¹ ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αmp(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ sapply (h: ?ah y: αy).mpr: ∀ {a b : Prop}, (a ↔ b) → b → amprα: Type u_1inst✝: Group αs: Subgroup αx, y: αh: ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ smpy * y⁻¹ ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αmp(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ srw [α: Type u_1inst✝: Group αs: Subgroup αx, y: αh: ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ smpy * y⁻¹ ∈ smul_right_inv: ∀ {G : Type ?u.79227} [inst : Group G] (a : G), a * a⁻¹ = 1mul_right_invα: Type u_1inst✝: Group αs: Subgroup αx, y: αh: ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ smp1 ∈ s]α: Type u_1inst✝: Group αs: Subgroup αx, y: αh: ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ smp1 ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αmp(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ sexact s: Subgroup αs.one_mem: ∀ {G : Type ?u.79278} [inst : Group G] (H : Subgroup G), 1 ∈ Hone_memGoals accomplished! 🐙
α: Type u_1inst✝: Group αs: Subgroup αx, y: α↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ s·α: Type u_1inst✝: Group αs: Subgroup αx, y: αmpry * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s α: Type u_1inst✝: Group αs: Subgroup αx, y: αmpry * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ sintro h: ?bh z: αzα: Type u_1inst✝: Group αs: Subgroup αx, y: αh: y * x⁻¹ ∈ sz: αmprz * x⁻¹ ∈ s ↔ z * y⁻¹ ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αmpry * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ srw [α: Type u_1inst✝: Group αs: Subgroup αx, y: αh: y * x⁻¹ ∈ sz: αmprz * x⁻¹ ∈ s ↔ z * y⁻¹ ∈ s← inv_mul_cancel_left: ∀ {G : Type ?u.79296} [inst : Group G] (a b : G), a⁻¹ * (a * b) = binv_mul_cancel_left y: αy x: αx⁻¹α: Type u_1inst✝: Group αs: Subgroup αx, y: αh: y * x⁻¹ ∈ sz: αmprz * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s]α: Type u_1inst✝: Group αs: Subgroup αx, y: αh: y * x⁻¹ ∈ sz: αmprz * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αmpry * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ srw [α: Type u_1inst✝: Group αs: Subgroup αx, y: αh: y * x⁻¹ ∈ sz: αmprz * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s← mul_assoc: ∀ {G : Type ?u.79472} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assocα: Type u_1inst✝: Group αs: Subgroup αx, y: αh: y * x⁻¹ ∈ sz: αmprz * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s]α: Type u_1inst✝: Group αs: Subgroup αx, y: αh: y * x⁻¹ ∈ sz: αmprz * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s
α: Type u_1inst✝: Group αs: Subgroup αx, y: αmpry * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ sexact s: Subgroup αs.mul_mem_cancel_right: ∀ {G : Type ?u.79856} [inst : Group G] (H : Subgroup G) {x y : G}, x ∈ H → (y * x ∈ H ↔ y ∈ H)mul_mem_cancel_right h: ?bhGoals accomplished! 🐙
#align right_coset_eq_iff rightCoset_eq_iff: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {x y : α}, ↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ srightCoset_eq_iff
#align right_add_coset_eq_iff rightAddCoset_eq_iff: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {x y : α}, ↑s +r x = ↑s +r y ↔ y + -x ∈ srightAddCoset_eq_iff

end CosetSubgroup

run_cmd Lean.Elab.Command.liftCoreM: {α : Type} → Lean.CoreM α → Lean.Elab.Command.CommandElabM αLean.Elab.Command.liftCoreM <| ToAdditive.insertTranslation: Lean.Name → Lean.Name → optParam Bool true → Lean.CoreM UnitToAdditive.insertTranslation `QuotientGroup: Lean.Name`QuotientGroup `QuotientAddGroup: Lean.Name`QuotientAddGroup

namespace QuotientGroup

variable [Group: Type ?u.93719 → Type ?u.93719Group α: Type ?u.90703α] (s: Subgroup αs : Subgroup: (G : Type ?u.90726) → [inst : Group G] → Type ?u.90726Subgroup α: Type ?u.80212α)

/-- The equivalence relation corresponding to the partition of a group by left cosets
of a subgroup.-/
@[to_additive: {α : Type u_1} → [inst : AddGroup α] → AddSubgroup α → Setoid αto_additive "The equivalence relation corresponding to the partition of a group by left cosets
of a subgroup."]
def leftRel: {α : Type u_1} → [inst : Group α] → Subgroup α → Setoid αleftRel : Setoid: Sort ?u.80240 → Sort (max1?u.80240)Setoid α: Type ?u.80226α :=
MulAction.orbitRel: (α : Type ?u.80243) → (β : Type ?u.80242) → [inst : Group α] → [inst : MulAction α β] → Setoid βMulAction.orbitRel (Subgroup.opposite: {G : Type ?u.80244} → [inst : Group G] → Subgroup G ≃ Subgroup GᵐᵒᵖSubgroup.opposite s: Subgroup αs) α: Type ?u.80226α
#align quotient_group.left_rel QuotientGroup.leftRel: {α : Type u_1} → [inst : Group α] → Subgroup α → Setoid αQuotientGroup.leftRel

variable {s: ?m.80922s}

@[to_additive: ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {x y : α}, Setoid.r x y ↔ -x + y ∈ sto_additive]
theorem leftRel_apply: ∀ {x y : α}, Setoid.r x y ↔ x⁻¹ * y ∈ sleftRel_apply {x: αx y: αy : α: Type ?u.80925α} : @Setoid.r: {α : Sort ?u.80943} → [self : Setoid α] → α → α → PropSetoid.r _: Sort ?u.80943_ (leftRel: {α : Type ?u.80945} → [inst : Group α] → Subgroup α → Setoid αleftRel s: Subgroup αs) x: αx y: αy ↔ x: αx⁻¹ * y: αy ∈ s: Subgroup αs :=
calc
(∃ a: { x // x ∈ ↑Subgroup.opposite s }a : Subgroup.opposite: {G : Type ?u.81877} → [inst : Group G] → Subgroup G ≃ Subgroup GᵐᵒᵖSubgroup.opposite s: Subgroup αs, y: αy * MulOpposite.unop: {α : Type ?u.82027} → αᵐᵒᵖ → αMulOpposite.unop a: { x // x ∈ ↑Subgroup.opposite s }a = x: αx) ↔ ∃ a: { x // x ∈ s }a : s: Subgroup αs, y: αy * a: { x // x ∈ s }a = x: αx :=
s: Subgroup αs.oppositeEquiv: {G : Type ?u.83593} → [inst : Group G] → (H : Subgroup G) → { x // x ∈ H } ≃ { x // x ∈ ↑Subgroup.opposite H }oppositeEquiv.symm: {α : Sort ?u.83597} → {β : Sort ?u.83596} → α ≃ β → β ≃ αsymm.exists_congr_left: ∀ {α : Sort ?u.83602} {β : Sort ?u.83603} (f : α ≃ β) {p : α → Prop}, (∃ a, p a) ↔ ∃ b, p (↑f.symm b)exists_congr_left
_: ?m✝_ ↔ ∃ a: { x // x ∈ s }a : s: Subgroup αs, x: αx⁻¹ * y: αy = a: { x // x ∈ s }a⁻¹ :=
byGoals accomplished! 🐙 α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∃ a, y * ↑a = x) ↔ ∃ a, x⁻¹ * y = ↑a⁻¹simp only [inv_mul_eq_iff_eq_mul: ∀ {G : Type ?u.84746} [inst : Group G] {a b c : G}, a⁻¹ * b = c ↔ b = a * cinv_mul_eq_iff_eq_mul, Subgroup.coe_inv: ∀ {G : Type ?u.84777} [inst : Group G] (H : Subgroup G) (x : { x // x ∈ H }), ↑x⁻¹ = (↑x)⁻¹Subgroup.coe_inv, eq_mul_inv_iff_mul_eq: ∀ {G : Type ?u.84790} [inst : Group G] {a b c : G}, a = b * c⁻¹ ↔ a * c = beq_mul_inv_iff_mul_eq]Goals accomplished! 🐙
_: ?m✝_ ↔ x: αx⁻¹ * y: αy ∈ s: Subgroup αs := byGoals accomplished! 🐙 α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∃ a, x⁻¹ * y = ↑a⁻¹) ↔ x⁻¹ * y ∈ ssimp [exists_inv_mem_iff_exists_mem: ∀ {G : Type ?u.85101} [inst : Group G] {S : Type ?u.85102} {H : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G]
{P : G → Prop}, (∃ x, x ∈ H ∧ P x⁻¹) ↔ ∃ x, x ∈ H ∧ P xexists_inv_mem_iff_exists_mem]Goals accomplished! 🐙
#align quotient_group.left_rel_apply QuotientGroup.leftRel_apply: ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {x y : α}, Setoid.r x y ↔ x⁻¹ * y ∈ sQuotientGroup.leftRel_apply
#align quotient_add_group.left_rel_apply QuotientAddGroup.leftRel_apply: ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {x y : α}, Setoid.r x y ↔ -x + y ∈ sQuotientAddGroup.leftRel_apply

variable (s: ?m.90717s)

@[to_additive: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), Setoid.r = fun x y => -x + y ∈ sto_additive]
theorem leftRel_eq: Setoid.r = fun x y => x⁻¹ * y ∈ sleftRel_eq : @Setoid.r: {α : Sort ?u.90735} → [self : Setoid α] → α → α → PropSetoid.r _: Sort ?u.90735_ (leftRel: {α : Type ?u.90737} → [inst : Group α] → Subgroup α → Setoid αleftRel s: Subgroup αs) = fun x: ?m.90770x y: ?m.90773y => x: ?m.90770x⁻¹ * y: ?m.90773y ∈ s: Subgroup αs :=
funext₂: ∀ {α : Sort ?u.91531} {β : α → Sort ?u.91532} {γ : (a : α) → β a → Sort ?u.91530} {f g : (a : α) → (b : β a) → γ a b},
(∀ (a : α) (b : β a), f a b = g a b) → f = gfunext₂ <| byGoals accomplished! 🐙
α: Type u_1inst✝: Group αs: Subgroup α∀ (a b : α), Setoid.r a b = (a⁻¹ * b ∈ s)simp only [eq_iff_iff: ∀ {p q : Prop}, p = q ↔ (p ↔ q)eq_iff_iff]α: Type u_1inst✝: Group αs: Subgroup α∀ (a b : α), Setoid.r a b ↔ a⁻¹ * b ∈ s
α: Type u_1inst✝: Group αs: Subgroup α∀ (a b : α), Setoid.r a b = (a⁻¹ * b ∈ s)apply leftRel_apply: ∀ {α : Type ?u.91764} [inst : Group α] {s : Subgroup α} {x y : α}, Setoid.r x y ↔ x⁻¹ * y ∈ sleftRel_applyGoals accomplished! 🐙
#align quotient_group.left_rel_eq QuotientGroup.leftRel_eq: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Setoid.r = fun x y => x⁻¹ * y ∈ sQuotientGroup.leftRel_eq

theorem leftRel_r_eq_leftCosetEquivalence: Setoid.r = LeftCosetEquivalence ↑sleftRel_r_eq_leftCosetEquivalence :
@Setoid.r: {α : Sort ?u.91866} → [self : Setoid α] → α → α → PropSetoid.r _: Sort ?u.91866_ (QuotientGroup.leftRel: {α : Type ?u.91868} → [inst : Group α] → Subgroup α → Setoid αQuotientGroup.leftRel s: Subgroup αs) = LeftCosetEquivalence: {α : Type ?u.91900} → [inst : Mul α] → Set α → α → α → PropLeftCosetEquivalence s: Subgroup αs := byGoals accomplished! 🐙
α: Type u_1inst✝: Group αs: Subgroup αSetoid.r = LeftCosetEquivalence ↑sextα: Type u_1inst✝: Group αs: Subgroup αx✝¹, x✝: αh.h.aSetoid.r x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝
α: Type u_1inst✝: Group αs: Subgroup αSetoid.r = LeftCosetEquivalence ↑srw [α: Type u_1inst✝: Group αs: Subgroup αx✝¹, x✝: αh.h.aSetoid.r x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝leftRel_eq: ∀ {α : Type ?u.92748} [inst : Group α] (s : Subgroup α), Setoid.r = fun x y => x⁻¹ * y ∈ sleftRel_eqα: Type u_1inst✝: Group αs: Subgroup αx✝¹, x✝: αh.h.a(fun x y => x⁻¹ * y ∈ s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝]α: Type u_1inst✝: Group αs: Subgroup αx✝¹, x✝: αh.h.a(fun x y => x⁻¹ * y ∈ s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝
α: Type u_1inst✝: Group αs: Subgroup αSetoid.r = LeftCosetEquivalence ↑sexact (leftCoset_eq_iff: ∀ {α : Type ?u.92822} [inst : Group α] (s : Subgroup α) {x y : α}, x *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ sleftCoset_eq_iff s: Subgroup αs).symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)symmGoals accomplished! 🐙
#align quotient_group.left_rel_r_eq_left_coset_equivalence QuotientGroup.leftRel_r_eq_leftCosetEquivalence: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Setoid.r = LeftCosetEquivalence ↑sQuotientGroup.leftRel_r_eq_leftCosetEquivalence

@[to_additive: {α : Type u_1} →
[inst : AddGroup α] → (s : AddSubgroup α) → [inst_1 : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.rto_additive]
instance leftRelDecidable: [inst : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.rleftRelDecidable [DecidablePred: {α : Sort ?u.92878} → (α → Prop) → Sort (max1?u.92878)DecidablePred (· ∈ s: Subgroup αs)] : DecidableRel: {α : Sort ?u.92923} → (α → α → Prop) → Sort (max1?u.92923)DecidableRel (leftRel: {α : Type ?u.92925} → [inst : Group α] → Subgroup α → Setoid αleftRel s: Subgroup αs).r: {α : Sort ?u.92933} → [self : Setoid α] → α → α → Propr := fun x: ?m.92950x y: ?m.92953y => byGoals accomplished! 🐙
α: Type ?u.92864inst✝¹: Group αs: Subgroup αinst✝: DecidablePred fun x => x ∈ sx, y: αDecidable (Setoid.r x y)rw [α: Type ?u.92864inst✝¹: Group αs: Subgroup αinst✝: DecidablePred fun x => x ∈ sx, y: αDecidable (Setoid.r x y)leftRel_eq: ∀ {α : Type ?u.92960} [inst : Group α] (s : Subgroup α), Setoid.r = fun x y => x⁻¹ * y ∈ sleftRel_eqα: Type ?u.92864inst✝¹: Group αs: Subgroup αinst✝: DecidablePred fun x => x ∈ sx, y: αDecidable ((fun x y => x⁻¹ * y ∈ s) x y)]α: Type ?u.92864inst✝¹: Group αs: Subgroup αinst✝: DecidablePred fun x => x ∈ sx, y: αDecidable ((fun x y => x⁻¹ * y ∈ s) x y)
α: Type ?u.92864inst✝¹: Group αs: Subgroup αinst✝: DecidablePred fun x => x ∈ sx, y: αDecidable (Setoid.r x y)exact ‹DecidablePred (· ∈ s)› _: α_Goals accomplished! 🐙
#align quotient_group.left_rel_decidable QuotientGroup.leftRelDecidable: {α : Type u_1} → [inst : Group α] → (s : Subgroup α) → [inst_1 : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.rQuotientGroup.leftRelDecidable
[inst : AddGroup α] → (s : AddSubgroup α) → [inst_1 : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.rQuotientAddGroup.leftRelDecidable

/-- `α ⧸ s` is the quotient type representing the left cosets of `s`.
If `s` is a normal subgroup, `α ⧸ s` is a group -/
@[to_additive: {α : Type u_1} → [inst : AddGroup α] → HasQuotient α (AddSubgroup α)to_additive "`α ⧸ s` is the quotient type representing the left cosets of `s`.  If `s` is a normal
subgroup, `α ⧸ s` is a group"]
instance: {α : Type u_1} → [inst : Group α] → HasQuotient α (Subgroup α)instance : HasQuotient: outParam (Type ?u.93575) → Type ?u.93574 → Type (max(?u.93575+1)(?u.93574+1))HasQuotient α: Type ?u.93560α (Subgroup: (G : Type ?u.93576) → [inst : Group G] → Type ?u.93576Subgroup α: Type ?u.93560α) :=
⟨fun s: ?m.93593s => Quotient: {α : Sort ?u.93595} → Setoid α → Sort ?u.93595Quotient (leftRel: {α : Type ?u.93597} → [inst : Group α] → Subgroup α → Setoid αleftRel s: ?m.93593s)⟩

/-- The equivalence relation corresponding to the partition of a group by right cosets of a
subgroup. -/
@[to_additive: {α : Type u_1} → [inst : AddGroup α] → AddSubgroup α → Setoid αto_additive "The equivalence relation corresponding to the partition of a group by right cosets
of a subgroup."]
def rightRel: Setoid αrightRel : Setoid: Sort ?u.93730 → Sort (max1?u.93730)Setoid α: Type ?u.93716α :=
MulAction.orbitRel: (α : Type ?u.93733) → (β : Type ?u.93732) → [inst : Group α] → [inst : MulAction α β] → Setoid βMulAction.orbitRel s: Subgroup αs α: Type ?u.93716α
#align quotient_group.right_rel QuotientGroup.rightRel: {α : Type u_1} → [inst : Group α] → Subgroup α → Setoid αQuotientGroup.rightRel

variable {s: ?m.95053s}

@[to_additive: ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {x y : α}, Setoid.r x y ↔ y + -x ∈ sto_additive]
theorem rightRel_apply: ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {x y : α}, Setoid.r x y ↔ y * x⁻¹ ∈ srightRel_apply {x: αx y: αy : α: Type ?u.95056α} : @Setoid.r: {α : Sort ?u.95074} → [self : Setoid α] → α → α → PropSetoid.r _: Sort ?u.95074_ (rightRel: {α : Type ?u.95076} → [inst : Group α] → Subgroup α → Setoid αrightRel s: Subgroup αs) x: αx y: αy ↔ y: αy * x: αx⁻¹ ∈ s: Subgroup αs :=
calc
(∃ a: { x // x ∈ s }a : s: Subgroup αs, (a: { x // x ∈ s }a : α: Type ?u.95056α) * y: αy = x: αx) ↔ ∃ a: { x // x ∈ s }a : s: Subgroup αs, y: αy * x: αx⁻¹ = a: { x // x ∈ s }a⁻¹ :=
byGoals accomplished! 🐙 α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∃ a, ↑a * y = x) ↔ ∃ a, y * x⁻¹ = ↑a⁻¹simp only [mul_inv_eq_iff_eq_mul: ∀ {G : Type ?u.97996} [inst : Group G] {a b c : G}, a * b⁻¹ = c ↔ a = c * bmul_inv_eq_iff_eq_mul, Subgroup.coe_inv: ∀ {G : Type ?u.98027} [inst : Group G] (H : Subgroup G) (x : { x // x ∈ H }), ↑x⁻¹ = (↑x)⁻¹Subgroup.coe_inv, eq_inv_mul_iff_mul_eq: ∀ {G : Type ?u.98040} [inst : Group G] {a b c : G}, a = b⁻¹ * c ↔ b * a = ceq_inv_mul_iff_mul_eq]Goals accomplished! 🐙
_: ?m✝_ ↔ y: αy * x: αx⁻¹ ∈ s: Subgroup αs := byGoals accomplished! 🐙 α: Type u_1inst✝: Group αs: Subgroup αx, y: α(∃ a, y * x⁻¹ = ↑a⁻¹) ↔ y * x⁻¹ ∈ ssimp [exists_inv_mem_iff_exists_mem: ∀ {G : Type ?u.98351} [inst : Group G] {S : Type ?u.98352} {H : S} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G]
{P : G → Prop}, (∃ x, x ∈ H ∧ P x⁻¹) ↔ ∃ x, x ∈ H ∧ P xexists_inv_mem_iff_exists_mem]Goals accomplished! 🐙
#align quotient_group.right_rel_apply QuotientGroup.rightRel_apply: ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {x y : α}, Setoid.r x y ↔ y * x⁻¹ ∈ sQuotientGroup.rightRel_apply
#align quotient_add_group.right_rel_apply QuotientAddGroup.rightRel_apply: ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {x y : α}, Setoid.r x y ↔ y + -x ∈ sQuotientAddGroup.rightRel_apply

variable (s: ?m.103695s)

@[to_additive: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), Setoid.r = fun x y => y + -x ∈ sto_additive]
theorem rightRel_eq: Setoid.r = fun x y => y * x⁻¹ ∈ srightRel_eq : @Setoid.r: {α : Sort ?u.103713} → [self : Setoid α] → α → α → PropSetoid.r _: Sort ?u.103713_ (rightRel: {α : Type ?u.103715} → [inst : Group α] → Subgroup α → Setoid αrightRel s: Subgroup αs) = fun x: ?m.103748x y: ?m.103751y => y: ?m.103751y * x: ?m.103748x⁻¹ ∈ s: Subgroup αs :=
funext₂: ∀ {α : Sort ?u.104509} {β : α → Sort ?u.104510} {γ : (a : α) → β a → Sort ?u.104508}
{f g : (a : α) → (b : β a) → γ a b}, (∀ (a : α) (b : β a), f a b = g a b) → f = gfunext₂ <| byGoals accomplished! 🐙
α: Type u_1inst✝: Group αs: Subgroup α∀ (a b : α), Setoid.r a b = (b * a⁻¹ ∈ s)simp only [eq_iff_iff: ∀ {p q : Prop}, p = q ↔ (p ↔ q)eq_iff_iff]α: Type u_1inst✝: Group αs: Subgroup α∀ (a b : α), Setoid.r a b ↔ b * a⁻¹ ∈ s
α: Type u_1inst✝: Group αs: Subgroup α∀ (a b : α), Setoid.r a b = (b * a⁻¹ ∈ s)apply rightRel_apply: ∀ {α : Type ?u.104740} [inst : Group α] {s : Subgroup α} {x y : α}, Setoid.r x y ↔ y * x⁻¹ ∈ srightRel_applyGoals accomplished! 🐙
#align quotient_group.right_rel_eq QuotientGroup.rightRel_eq: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Setoid.r = fun x y => y * x⁻¹ ∈ sQuotientGroup.rightRel_eq

theorem rightRel_r_eq_rightCosetEquivalence: Setoid.r = RightCosetEquivalence ↑srightRel_r_eq_rightCosetEquivalence :
@Setoid.r: {α : Sort ?u.104836} → [self : Setoid α] → α → α → PropSetoid.r _: Sort ?u.104836_ (QuotientGroup.rightRel: {α : Type ?u.104838} → [inst : Group α] → Subgroup α → Setoid αQuotientGroup.rightRel s: Subgroup αs) = RightCosetEquivalence: {α : Type ?u.104870} → [inst : Mul α] → Set α → α → α → PropRightCosetEquivalence s: Subgroup αs := byGoals accomplished! 🐙
α: Type u_1inst✝: Group αs: Subgroup αSetoid.r = RightCosetEquivalence ↑sextα: Type u_1inst✝: Group αs: Subgroup αx✝¹, x✝: αh.h.aSetoid.r x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝
α: Type u_1inst✝: Group αs: Subgroup αSetoid.r = RightCosetEquivalence ↑srw [α: Type u_1inst✝: Group αs: Subgroup αx✝¹, x✝: αh.h.aSetoid.r x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝rightRel_eq: ∀ {α : Type ?u.105718} [inst : Group α] (s : Subgroup α), Setoid.r = fun x y => y * x⁻¹ ∈ srightRel_eqα: Type u_1inst✝: Group αs: Subgroup αx✝¹, x✝: αh.h.a(fun x y => y * x⁻¹ ∈ s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝]α: Type u_1inst✝: Group αs: Subgroup αx✝¹, x✝: αh.h.a(fun x y => y * x⁻¹ ∈ s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝
α: Type u_1inst✝: Group αs: Subgroup αSetoid.r = RightCosetEquivalence ↑sexact (rightCoset_eq_iff: ∀ {α : Type ?u.105792} [inst : Group α] (s : Subgroup α) {x y : α}, ↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ srightCoset_eq_iff s: Subgroup αs).symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)symmGoals accomplished! 🐙
#align quotient_group.right_rel_r_eq_right_coset_equivalence QuotientGroup.rightRel_r_eq_rightCosetEquivalence: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Setoid.r = RightCosetEquivalence ↑sQuotientGroup.rightRel_r_eq_rightCosetEquivalence

@[to_additive: {α : Type u_1} →
[inst : AddGroup α] → (s : AddSubgroup α) → [inst_1 : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.rto_additive]
instance rightRelDecidable: [inst : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.rrightRelDecidable [DecidablePred: {α : Sort ?u.105848} → (α → Prop) → Sort (max1?u.105848)DecidablePred (· ∈ s: Subgroup αs)] : DecidableRel: {α : Sort ?u.105893} → (α → α → Prop) → Sort (max1?u.105893)DecidableRel (rightRel: {α : Type ?u.105895} → [inst : Group α] → Subgroup α → Setoid αrightRel s: Subgroup αs).r: {α : Sort ?u.105903} → [self : Setoid α] → α → α → Propr := fun x: ?m.105920x y: ?m.105923y => byGoals accomplished! 🐙
α: Type ?u.105834inst✝¹: Group αs: Subgroup αinst✝: DecidablePred fun x => x ∈ sx, y: αDecidable (Setoid.r x y)rw [α: Type ?u.105834inst✝¹: Group αs: Subgroup αinst✝: DecidablePred fun x => x ∈ sx, y: αDecidable (Setoid.r x y)rightRel_eq: ∀ {α : Type ?u.105930} [inst : Group α] (s : Subgroup α), Setoid.r = fun x y => y * x⁻¹ ∈ srightRel_eqα: Type ?u.105834inst✝¹: Group αs: Subgroup αinst✝: DecidablePred fun x => x ∈ sx, y: αDecidable ((fun x y => y * x⁻¹ ∈ s) x y)]α: Type ?u.105834inst✝¹: Group αs: Subgroup αinst✝: DecidablePred fun x => x ∈ sx, y: αDecidable ((fun x y => y * x⁻¹ ∈ s) x y)
α: Type ?u.105834inst✝¹: Group αs: Subgroup αinst✝: DecidablePred fun x => x ∈ sx, y: αDecidable (Setoid.r x y)exact ‹DecidablePred (· ∈ s)› _: α_Goals accomplished! 🐙
#align quotient_group.right_rel_decidable QuotientGroup.rightRelDecidable: {α : Type u_1} → [inst : Group α] → (s : Subgroup α) → [inst_1 : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.rQuotientGroup.rightRelDecidable
[inst : AddGroup α] → (s : AddSubgroup α) → [inst_1 : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.rQuotientAddGroup.rightRelDecidable

/-- Right cosets are in bijection with left cosets. -/
@[to_additive: {α : Type u_1} → [inst : AddGroup α] → (s : AddSubgroup α) → Quotient (QuotientAddGroup.rightRel s) ≃ α ⧸ sto_additive "Right cosets are in bijection with left cosets."]
def quotientRightRelEquivQuotientLeftRel: Quotient (rightRel s) ≃ α ⧸ squotientRightRelEquivQuotientLeftRel : Quotient: {α : Sort ?u.106498} → Setoid α → Sort ?u.106498Quotient (QuotientGroup.rightRel: {α : Type ?u.106500} → [inst : Group α] → Subgroup α → Setoid αQuotientGroup.rightRel s: Subgroup αs) ≃ α: Type ?u.106482α ⧸ s: Subgroup αs
where
toFun :=
Quotient.map': {α : Sort ?u.106556} →
{β : Sort ?u.106555} →
{s₁ : Setoid α} → {s₂ : Setoid β} → (f : α → β) → (Setoid.r ⇒ Setoid.r) f f → Quotient s₁ → Quotient s₂Quotient.map' (fun g: ?m.106566g => g: ?m.106566g⁻¹) fun a: ?m.106731a b: ?m.106734b => byGoals accomplished! 🐙
α: Type ?u.106482inst✝: Group αs: Subgroup αa, b: αSetoid.r a b → Setoid.r ((fun g => g⁻¹) a) ((fun g => g⁻¹) b)rw [α: Type ?u.106482inst✝: Group αs: Subgroup αa, b: αSetoid.r a b → Setoid.r ((fun g => g⁻¹) a) ((fun g => g⁻¹) b)leftRel_apply: ∀ {α : Type ?u.106908} [inst : Group α] {s : Subgroup α} {x y : α}, Setoid.r x y ↔ x⁻¹ * y ∈ sleftRel_apply,α: Type ?u.106482inst✝: Group αs: Subgroup αa, b: αSetoid.r a b → ((fun g => g⁻¹) a)⁻¹ * (fun g => g⁻¹) b ∈ s α: Type ?u.106482inst✝: Group αs: Subgroup αa, b: αSetoid.r a b → Setoid.r ((fun g => g⁻¹) a) ((fun g => g⁻¹) b)rightRel_apply: ∀ {α : Type ?u.107060} [inst : Group α] {s : Subgroup α} {x y : α}, Setoid.r x y ↔ y * x⁻¹ ∈ srightRel_applyα: Type ?u.106482inst✝: Group αs: Subgroup αa, b: αb * a⁻¹ ∈ s → ((fun g => g⁻¹) a)⁻¹ * (fun g => g⁻¹) b ∈ s]α: Type ?u.106482inst✝: Group αs: Subgroup αa, b: αb * a⁻¹ ∈ s → ((fun g => g⁻¹) a)⁻¹ * (fun g => g⁻¹) b ∈ s
α: Type ?u.106482inst✝: Group αs: Subgroup αa, b: αSetoid.r a b → Setoid.r ((fun g => g⁻¹) a) ((fun g => g⁻¹) b)exact fun h: ?m.107131h => (congr_arg: ∀ {α : Sort ?u.107134} {β : Sort ?u.107133} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂congr_arg (· ∈ s: Subgroup αs) (α: Type ?u.106482inst✝: Group αs: Subgroup αa, b: αb * a⁻¹ ∈ s → ((fun g => g⁻¹) a)⁻¹ * (fun g => g⁻¹) b ∈ sbyGoals accomplished! 🐙 α: Type ?u.106482inst✝: Group αs: Subgroup αa, b: αh: b * a⁻¹ ∈ s(b * a⁻¹)⁻¹ = ((fun g => g⁻¹) a)⁻¹ * (fun g => g⁻¹) bsimp [mul_assoc: ∀ {G : Type ?u.107206} [inst : Semigroup G] (a b c : G), a * b * c = a * (b * c)mul_assoc]Goals accomplished! 🐙)).mp: ∀ {α β : Sort ?u.107186}, α = β → α → βmp (s: Subgroup αs.inv_mem: ∀ {G : Type ?u.107196} [inst : Group G] (H : Subgroup G) {x : G}, x ∈ H → x⁻¹ ∈ Hinv_mem h: ?m.107131h)Goals accomplished! 🐙
-- porting note: replace with `by group`
invFun :=
Quotient.map': {α : Sort ?u.106744} →
{β : Sort ?u.106743} →
{s₁ : Setoid α} → {s₂ : Setoid β} → (f : α → β) → (Setoid.r ⇒ Setoid.r) f f → Quotient s₁ → Quotient s₂Quotient.map' (fun g: ?m.106752g => g: ?m.106752```