/-
Copyright (c) 2018 Mitchell Rowett. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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
  `AddGroup` this is `leftAddCoset a s`.
* `rightCoset s a`: the right coset `s * a` for an element `a : α` and a subset `s ⊆ α`, for an
  `AddGroup` this is `rightAddCoset s a`.
* `QuotientGroup.quotient s`: the quotient type representing the left cosets with respect to a
  subgroup `s`, for an `AddGroup` this is `QuotientAddGroup.quotient s`.
* `QuotientGroup.mk`: the canonical map from `α` to `α/s` for a subgroup `s` of `α`, for an
  `AddGroup` this is `QuotientAddGroup.mk`.
* `Subgroup.leftCosetEquivSubgroup`: the natural bijection between a left coset and the subgroup,
  for an `AddGroup` this is `AddSubgroup.leftCosetEquivAddSubgroup`.

## 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.8
Mul α: Type ?u.5
α] (a: α
a : α: Type ?u.5
α) (s: Set α
s : Set: Type ?u.13 → Type ?u.13
Set α: Type ?u.5
α) : Set: Type ?u.16 → Type ?u.16
Set α: Type ?u.5
α :=
  (fun x: ?m.31
x => a: α
a * x: ?m.31
x) '' s: Set α
s
#align left_coset leftCoset: {α : Type u_1} → [inst : Mul α] → α → Set α → Set α
leftCoset
#align left_add_coset leftAddCoset: {α : Type u_1} → [inst : Add α] → α → Set α → Set α
leftAddCoset

/-- The right coset `s * a` for an element `a : α` and a subset `s : Set α` -/
@[to_additive rightAddCoset: {α : Type u_1} → [inst : Add α] → Set α → α → Set α
rightAddCoset
      "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.137
Mul α: Type ?u.134
α] (s: Set α
s : Set: Type ?u.140 → Type ?u.140
Set α: Type ?u.134
α) (a: α
a : α: Type ?u.134
α) : Set: Type ?u.145 → Type ?u.145
Set α: Type ?u.134
α :=
  (fun x: ?m.160
x => x: ?m.160
x * a: α
a) '' s: Set α
s
#align right_coset rightCoset: {α : Type u_1} → [inst : Mul α] → Set α → α → Set α
rightCoset
#align right_add_coset rightAddCoset: {α : Type u_1} → [inst : Add α] → Set α → α → Set α
rightAddCoset

@[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.32123
Mul α: Type ?u.31453
α]

@[to_additive mem_leftAddCoset: ∀ {α : Type u_1} [inst : Add α] {s : Set α} {x : α} (a : α), x ∈ s → a + x ∈ a +l s
mem_leftAddCoset]
theorem mem_leftCoset: ∀ {α : Type u_1} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → a * x ∈ a *l s
mem_leftCoset {s: Set α
s : Set: Type ?u.31465 → Type ?u.31465
Set α: Type ?u.31459
α} {x: α
x : α: Type ?u.31459
α} (a: α
a : α: Type ?u.31459
α) (hxS: x ∈ s
hxS : 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 '' a
mem_image_of_mem (fun b: α
b : α: Type ?u.31459
α => a: α
a * b: α
b) hxS: x ∈ s
hxS
#align mem_left_coset mem_leftCoset: ∀ {α : Type u_1} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → a * x ∈ a *l s
mem_leftCoset
#align mem_left_add_coset mem_leftAddCoset: ∀ {α : Type u_1} [inst : Add α] {s : Set α} {x : α} (a : α), x ∈ s → a + x ∈ a +l s
mem_leftAddCoset

@[to_additive mem_rightAddCoset: ∀ {α : Type u_1} [inst : Add α] {s : Set α} {x : α} (a : α), x ∈ s → x + a ∈ s +r a
mem_rightAddCoset]
theorem mem_rightCoset: ∀ {s : Set α} {x : α} (a : α), x ∈ s → x * a ∈ s *r a
mem_rightCoset {s: Set α
s : Set: Type ?u.31750 → Type ?u.31750
Set α: Type ?u.31744
α} {x: α
x : α: Type ?u.31744
α} (a: α
a : α: Type ?u.31744
α) (hxS: x ∈ s
hxS : 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 '' a
mem_image_of_mem (fun b: α
b : α: Type ?u.31744
α => b: α
b * a: α
a) hxS: x ∈ s
hxS
#align mem_right_coset mem_rightCoset: ∀ {α : Type u_1} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → x * a ∈ s *r a
mem_rightCoset
#align mem_right_add_coset mem_rightAddCoset: ∀ {α : Type u_1} [inst : Add α] {s : Set α} {x : α} (a : α), x ∈ s → x + a ∈ s +r a
mem_rightAddCoset

/-- Equality of two left cosets `a * s` and `b * s`. -/
@[to_additive LeftAddCosetEquivalence: {α : Type u_1} → [inst : Add α] → Set α → α → α → Prop
LeftAddCosetEquivalence "Equality of two left cosets `a + s` and `b + s`."]
def LeftCosetEquivalence: {α : Type u_1} → [inst : Mul α] → Set α → α → α → Prop
LeftCosetEquivalence (s: Set α
s : Set: Type ?u.32036 → Type ?u.32036
Set α: 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 α → α → α → Prop
LeftCosetEquivalence
#align left_add_coset_equivalence LeftAddCosetEquivalence: {α : Type u_1} → [inst : Add α] → Set α → α → α → Prop
LeftAddCosetEquivalence

@[to_additive leftAddCosetEquivalence_rel: ∀ {α : Type u_1} [inst : Add α] (s : Set α), Equivalence (LeftAddCosetEquivalence s)
leftAddCosetEquivalence_rel]
theorem leftCosetEquivalence_rel: ∀ {α : Type u_1} [inst : Mul α] (s : Set α), Equivalence (LeftCosetEquivalence s)
leftCosetEquivalence_rel (s: Set α
s : Set: Type ?u.32126 → Type ?u.32126
Set α: Type ?u.32120
α) : Equivalence: {α : Sort ?u.32129} → (α → α → Prop) → Prop
Equivalence (LeftCosetEquivalence: {α : Type ?u.32131} → [inst : Mul α] → Set α → α → α → Prop
LeftCosetEquivalence 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 r
Equivalence.mk _: Sort ?u.32189
_ (LeftCosetEquivalence: {α : Type ?u.32191} → [inst : Mul α] → Set α → α → α → Prop
LeftCosetEquivalence s: Set α
s) (fun _: ?m.32252
_ => rfl: ∀ {α : Sort ?u.32254} {a : α}, a = a
rfl) Eq.symm: ∀ {α : Sort ?u.32264} {a b : α}, a = b → b = a
Eq.symm Eq.trans: ∀ {α : Sort ?u.32279} {a b c : α}, a = b → b = c → a = c
Eq.trans
#align left_coset_equivalence_rel leftCosetEquivalence_rel: ∀ {α : Type u_1} [inst : Mul α] (s : Set α), Equivalence (LeftCosetEquivalence s)
leftCosetEquivalence_rel
#align left_add_coset_equivalence_rel leftAddCosetEquivalence_rel: ∀ {α : Type u_1} [inst : Add α] (s : Set α), Equivalence (LeftAddCosetEquivalence s)
leftAddCosetEquivalence_rel

/-- Equality of two right cosets `s * a` and `s * b`. -/
@[to_additive RightAddCosetEquivalence: {α : Type u_1} → [inst : Add α] → Set α → α → α → Prop
RightAddCosetEquivalence "Equality of two right cosets `s + a` and `s + b`."]
def RightCosetEquivalence: {α : Type u_1} → [inst : Mul α] → Set α → α → α → Prop
RightCosetEquivalence (s: Set α
s : Set: Type ?u.32333 → Type ?u.32333
Set α: 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 α → α → α → Prop
RightCosetEquivalence
#align right_add_coset_equivalence RightAddCosetEquivalence: {α : Type u_1} → [inst : Add α] → Set α → α → α → Prop
RightAddCosetEquivalence

@[to_additive rightAddCosetEquivalence_rel: ∀ {α : Type u_1} [inst : Add α] (s : Set α), Equivalence (RightAddCosetEquivalence s)
rightAddCosetEquivalence_rel]
theorem rightCosetEquivalence_rel: ∀ {α : Type u_1} [inst : Mul α] (s : Set α), Equivalence (RightCosetEquivalence s)
rightCosetEquivalence_rel (s: Set α
s : Set: Type ?u.32425 → Type ?u.32425
Set α: Type ?u.32419
α) : Equivalence: {α : Sort ?u.32428} → (α → α → Prop) → Prop
Equivalence (RightCosetEquivalence: {α : Type ?u.32430} → [inst : Mul α] → Set α → α → α → Prop
RightCosetEquivalence 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 r
Equivalence.mk _: Sort ?u.32488
_ (RightCosetEquivalence: {α : Type ?u.32490} → [inst : Mul α] → Set α → α → α → Prop
RightCosetEquivalence s: Set α
s) (fun _a: ?m.32551
_a => rfl: ∀ {α : Sort ?u.32553} {a : α}, a = a
rfl) Eq.symm: ∀ {α : Sort ?u.32563} {a b : α}, a = b → b = a
Eq.symm Eq.trans: ∀ {α : Sort ?u.32578} {a b c : α}, a = b → b = c → a = c
Eq.trans
#align right_coset_equivalence_rel rightCosetEquivalence_rel: ∀ {α : Type u_1} [inst : Mul α] (s : Set α), Equivalence (RightCosetEquivalence s)
rightCosetEquivalence_rel
#align right_add_coset_equivalence_rel rightAddCosetEquivalence_rel: ∀ {α : Type u_1} [inst : Add α] (s : Set α), Equivalence (RightAddCosetEquivalence s)
rightAddCosetEquivalence_rel

end CosetMul

section CosetSemigroup

variable [Semigroup: Type ?u.32635 → Type ?u.32635
Semigroup α: 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 s
leftAddCoset_assoc]
theorem leftCoset_assoc: ∀ {α : Type u_1} [inst : Semigroup α] (s : Set α) (a b : α), a *l (b *l s) = a * b *l s
leftCoset_assoc (s: Set α
s : Set: Type ?u.32638 → Type ?u.32638
Set α: 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 := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: 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 = a
symm, 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 s
leftCoset_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 s
leftAddCoset_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.35763
Set α: 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) := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: 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 = a
symm, 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

@[to_additive leftAddCoset_rightAddCoset: ∀ {α : Type u_1} [inst : AddSemigroup α] (s : Set α) (a b : α), a +l s +r b = a +l (s +r b)
leftAddCoset_rightAddCoset]
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.39268
Set α: 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) := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: 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 = a
symm, 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
#align left_add_coset_right_add_coset leftAddCoset_rightAddCoset: ∀ {α : Type u_1} [inst : AddSemigroup α] (s : Set α) (a b : α), a +l s +r b = a +l (s +r b)
leftAddCoset_rightAddCoset

end CosetSemigroup

section CosetMonoid

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

@[to_additive (attr := simp) zero_leftAddCoset: ∀ {α : Type u_1} [inst : AddMonoid α] (s : Set α), 0 +l s = s
zero_leftAddCoset]
theorem one_leftCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Set α), 1 *l s = s
one_leftCoset : 1: ?m.41903
1 *l s: Set α
s = s: Set α
s :=
  Set.ext: ∀ {α : Type ?u.42640} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = b
Set.ext <| by
Goals accomplished! 🐙 α: Type u_1

inst✝: 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 = s
one_leftCoset
#align zero_left_add_coset zero_leftAddCoset: ∀ {α : Type u_1} [inst : AddMonoid α] (s : Set α), 0 +l s = s
zero_leftAddCoset

@[to_additive (attr := simp) rightAddCoset_zero: ∀ {α : Type u_1} [inst : AddMonoid α] (s : Set α), s +r 0 = s
rightAddCoset_zero]
theorem rightCoset_one: ∀ {α : Type u_1} [inst : Monoid α] (s : Set α), s *r 1 = s
rightCoset_one : s: Set α
s *r 1: ?m.44500
1 = s: Set α
s :=
  Set.ext: ∀ {α : Type ?u.45227} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = b
Set.ext <| by
Goals accomplished! 🐙 α: Type u_1

inst✝: 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 = s
rightCoset_one
#align right_add_coset_zero rightAddCoset_zero: ∀ {α : Type u_1} [inst : AddMonoid α] (s : Set α), s +r 0 = s
rightAddCoset_zero

end CosetMonoid

section CosetSubmonoid

open Submonoid

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

@[to_additive mem_own_leftAddCoset: ∀ {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) (a : α), a ∈ a +l ↑s
mem_own_leftAddCoset]
theorem mem_own_leftCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ a *l ↑s
mem_own_leftCoset (a: α
a : α: Type ?u.47374
α) : a: α
a ∈ a: α
a *l s: Submonoid α
s :=
  suffices a: α
a * 1: ?m.48254
1 ∈ a: α
a *l s: Submonoid α
s by simpa
Goals accomplished! 🐙
  mem_leftCoset: ∀ {α : Type ?u.49430} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → a * x ∈ a *l s
mem_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 ∈ s
one_mem s: Submonoid α
s : 1: ?m.49472
1 ∈ s: Submonoid α
s)
#align mem_own_left_coset mem_own_leftCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ a *l ↑s
mem_own_leftCoset
#align mem_own_left_add_coset mem_own_leftAddCoset: ∀ {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) (a : α), a ∈ a +l ↑s
mem_own_leftAddCoset

@[to_additive mem_own_rightAddCoset: ∀ {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) (a : α), a ∈ ↑s +r a
mem_own_rightAddCoset]
theorem mem_own_rightCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ ↑s *r a
mem_own_rightCoset (a: α
a : α: Type ?u.50588
α) : a: α
a ∈ (s: Submonoid α
s : Set: Type ?u.50948 → Type ?u.50948
Set α: Type ?u.50588
α) *r a: α
a :=
  suffices 1: ?m.51470
1 * a: α
a ∈ (s: Submonoid α
s : Set: Type ?u.52240 → Type ?u.52240
Set α: Type ?u.50588
α) *r a: α
a by simpa
Goals accomplished! 🐙
  mem_rightCoset: ∀ {α : Type ?u.52648} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → x * a ∈ s *r a
mem_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 ∈ s
one_mem s: Submonoid α
s : 1: ?m.52690
1 ∈ s: Submonoid α
s)
#align mem_own_right_coset mem_own_rightCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ ↑s *r a
mem_own_rightCoset
#align mem_own_right_add_coset mem_own_rightAddCoset: ∀ {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) (a : α), a ∈ ↑s +r a
mem_own_rightAddCoset

@[to_additive mem_leftAddCoset_leftAddCoset: ∀ {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) {a : α}, a +l ↑s = ↑s → a ∈ s
mem_leftAddCoset_leftAddCoset]
theorem mem_leftCoset_leftCoset: ∀ {a : α}, a *l ↑s = ↑s → a ∈ s
mem_leftCoset_leftCoset {a: α
a : α: Type ?u.53806
α} (ha: a *l ↑s = ↑s
ha : a: α
a *l s: Submonoid α
s = s: Submonoid α
s) : a: α
a ∈ s: Submonoid α
s := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: a *l ↑s = ↑s

a ∈ srw [α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: a *l ↑s = ↑s

a ∈ s← SetLike.mem_coe: ∀ {A : Type ?u.54708} {B : Type ?u.54707} [i : SetLike A B] {p : A} {x : B}, x ∈ ↑p ↔ x ∈ p
SetLike.mem_coe,α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: a *l ↑s = ↑s

a ∈ ↑s α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: a *l ↑s = ↑s

a ∈ s← ha: a *l ↑s = ↑s
haα: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: a *l ↑s = ↑s

a ∈ a *l ↑s]α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: a *l ↑s = ↑s

a ∈ a *l ↑s;α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: a *l ↑s = ↑s

a ∈ a *l ↑s α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: a *l ↑s = ↑s

a ∈ sexact mem_own_leftCoset: ∀ {α : Type ?u.54766} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ a *l ↑s
mem_own_leftCoset s: Submonoid α
s a: α
a
Goals accomplished! 🐙
#align mem_left_coset_left_coset mem_leftCoset_leftCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) {a : α}, a *l ↑s = ↑s → a ∈ s
mem_leftCoset_leftCoset
#align mem_left_add_coset_left_add_coset mem_leftAddCoset_leftAddCoset: ∀ {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) {a : α}, a +l ↑s = ↑s → a ∈ s
mem_leftAddCoset_leftAddCoset

@[to_additive mem_rightAddCoset_rightAddCoset: ∀ {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) {a : α}, ↑s +r a = ↑s → a ∈ s
mem_rightAddCoset_rightAddCoset]
theorem mem_rightCoset_rightCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) {a : α}, ↑s *r a = ↑s → a ∈ s
mem_rightCoset_rightCoset {a: α
a : α: Type ?u.54812
α} (ha: ↑s *r a = ↑s
ha : (s: Submonoid α
s : Set: Type ?u.55123 → Type ?u.55123
Set α: Type ?u.54812
α) *r a: α
a = s: Submonoid α
s) : a: α
a ∈ s: Submonoid α
s := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: ↑s *r a = ↑s

a ∈ srw [α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: ↑s *r a = ↑s

a ∈ s← SetLike.mem_coe: ∀ {A : Type ?u.55716} {B : Type ?u.55715} [i : SetLike A B] {p : A} {x : B}, x ∈ ↑p ↔ x ∈ p
SetLike.mem_coe,α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: ↑s *r a = ↑s

a ∈ ↑s α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: ↑s *r a = ↑s

a ∈ s← ha: ↑s *r a = ↑s
haα: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: ↑s *r a = ↑s

a ∈ ↑s *r a]α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: ↑s *r a = ↑s

a ∈ ↑s *r a;α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: ↑s *r a = ↑s

a ∈ ↑s *r a α: Type u_1

inst✝: Monoid α

s: Submonoid α

a: α

ha: ↑s *r a = ↑s

a ∈ sexact mem_own_rightCoset: ∀ {α : Type ?u.55774} [inst : Monoid α] (s : Submonoid α) (a : α), a ∈ ↑s *r a
mem_own_rightCoset s: Submonoid α
s a: α
a
Goals accomplished! 🐙
#align mem_right_coset_right_coset mem_rightCoset_rightCoset: ∀ {α : Type u_1} [inst : Monoid α] (s : Submonoid α) {a : α}, ↑s *r a = ↑s → a ∈ s
mem_rightCoset_rightCoset
#align mem_right_add_coset_right_add_coset mem_rightAddCoset_rightAddCoset: ∀ {α : Type u_1} [inst : AddMonoid α] (s : AddSubmonoid α) {a : α}, ↑s +r a = ↑s → a ∈ s
mem_rightAddCoset_rightAddCoset

end CosetSubmonoid

section CosetGroup

variable [Group: Type ?u.55834 → Type ?u.55834
Group α: Type ?u.55820
α] {s: Set α
s : Set: Type ?u.55837 → Type ?u.55837
Set α: 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 ∈ s
mem_leftAddCoset_iff]
theorem mem_leftCoset_iff: ∀ (a : α), x ∈ a *l s ↔ a⁻¹ * x ∈ s
mem_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 ∈ s
hb, Eq: (fun x => a * x) b = x
Eq⟩ => by
Goals accomplished! 🐙 α: Type u_1

inst✝: Group α

s: Set α

x, a: α

x✝: x ∈ a *l s

b: α

hb: b ∈ s

Eq: (fun x => a * x) b = x

a⁻¹ * x ∈ ssimp [Eq: (fun x => a * x) b = x
Eq.symm: ∀ {α : Sort ?u.58155} {a b : α}, a = b → b = a
symm, hb: b ∈ s
hb]
Goals accomplished! 🐙) fun h: ?m.57254
h => ⟨a: α
a⁻¹ * x: α
x, h: ?m.57254
h, by
Goals accomplished! 🐙 α: Type u_1

inst✝: Group α

s: Set α

x, a: α

h: a⁻¹ * x ∈ s

(fun x => a * x) (a⁻¹ * x) = xsimp
Goals accomplished! 🐙⟩
#align mem_left_coset_iff mem_leftCoset_iff: ∀ {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ a *l s ↔ a⁻¹ * x ∈ s
mem_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 ∈ s
mem_leftAddCoset_iff

@[to_additive mem_rightAddCoset_iff: ∀ {α : Type u_1} [inst : AddGroup α] {s : Set α} {x : α} (a : α), x ∈ s +r a ↔ x + -a ∈ s
mem_rightAddCoset_iff]
theorem mem_rightCoset_iff: ∀ {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ s *r a ↔ x * a⁻¹ ∈ s
mem_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 ∈ s
hb, Eq: (fun x => x * a) b = x
Eq⟩ => by
Goals accomplished! 🐙 α: Type u_1

inst✝: Group α

s: Set α

x, a: α

x✝: x ∈ s *r a

b: α

hb: b ∈ s

Eq: (fun x => x * a) b = x

x * a⁻¹ ∈ ssimp [Eq: (fun x => x * a) b = x
Eq.symm: ∀ {α : Sort ?u.61092} {a b : α}, a = b → b = a
symm, hb: b ∈ s
hb]
Goals accomplished! 🐙) fun h: ?m.60191
h => ⟨x: α
x * a: α
a⁻¹, h: ?m.60191
h, by
Goals accomplished! 🐙 α: Type u_1

inst✝: Group α

s: Set α

x, a: α

h: x * a⁻¹ ∈ s

(fun x => x * a) (x * a⁻¹) = xsimp
Goals accomplished! 🐙⟩
#align mem_right_coset_iff mem_rightCoset_iff: ∀ {α : Type u_1} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ s *r a ↔ x * a⁻¹ ∈ s
mem_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 ∈ s
mem_rightAddCoset_iff

end CosetGroup

section CosetSubgroup

open Subgroup

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

@[to_additive leftAddCoset_mem_leftAddCoset: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {a : α}, a ∈ s → a +l ↑s = ↑s
leftAddCoset_mem_leftAddCoset]
theorem leftCoset_mem_leftCoset: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → a *l ↑s = ↑s
leftCoset_mem_leftCoset {a: α
a : α: Type ?u.61558
α} (ha: a ∈ s
ha : 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 = b
Set.ext <| by
Goals accomplished! 🐙 α: Type u_1

inst✝: 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 ∈ s
mem_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⁻¹ ∈ H
inv_mem ha: a ∈ s
ha)]
Goals accomplished! 🐙
#align left_coset_mem_left_coset leftCoset_mem_leftCoset: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → a *l ↑s = ↑s
leftCoset_mem_leftCoset
#align left_add_coset_mem_left_add_coset leftAddCoset_mem_leftAddCoset: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {a : α}, a ∈ s → a +l ↑s = ↑s
leftAddCoset_mem_leftAddCoset

@[to_additive rightAddCoset_mem_rightAddCoset: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {a : α}, a ∈ s → ↑s +r a = ↑s
rightAddCoset_mem_rightAddCoset]
theorem rightCoset_mem_rightCoset: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → ↑s *r a = ↑s
rightCoset_mem_rightCoset {a: α
a : α: Type ?u.63747
α} (ha: a ∈ s
ha : a: α
a ∈ s: Subgroup α
s) : (s: Subgroup α
s : Set: Type ?u.63813 → Type ?u.63813
Set α: Type ?u.63747
α) *r a: α
a = s: Subgroup α
s :=
  Set.ext: ∀ {α : Type ?u.64376} {a b : Set α}, (∀ (x : α), x ∈ a ↔ x ∈ b) → a = b
Set.ext fun b: ?m.64385
b => by
Goals accomplished! 🐙 α: Type u_1

inst✝: Group α

s: Subgroup α

a: α

ha: a ∈ s

b: α

b ∈ ↑s *r a ↔ b ∈ ↑ssimp [mem_rightCoset_iff: ∀ {α : Type ?u.64394} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ s *r a ↔ x * a⁻¹ ∈ s
mem_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⁻¹ ∈ H
inv_mem ha: a ∈ s
ha)]
Goals accomplished! 🐙
#align right_coset_mem_right_coset rightCoset_mem_rightCoset: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → ↑s *r a = ↑s
rightCoset_mem_rightCoset
#align right_add_coset_mem_right_add_coset rightAddCoset_mem_rightAddCoset: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {a : α}, a ∈ s → ↑s +r a = ↑s
rightAddCoset_mem_rightAddCoset

@[to_additive: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (a : α), AddAction.orbit { x // x ∈ s } a = ↑s +r a
to_additive]
theorem orbit_subgroup_eq_rightCoset: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) (a : α), MulAction.orbit { x // x ∈ s } a = ↑s *r a
orbit_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 = b
Set.ext fun _b: ?m.66593
_b => ⟨fun ⟨c: { x // x ∈ s }
c, d: (fun x => x • a) c = _b
d⟩ => ⟨c: { x // x ∈ s }
c, c: { x // x ∈ s }
c.2: ∀ {α : Sort ?u.66782} {p : α → Prop} (self : Subtype p), p ↑self
2, d: (fun x => x • a) c = _b
d⟩, fun ⟨c: α
c, d: c ∈ ↑s
d, e: (fun x => x * a) c = _b
e⟩ => ⟨⟨c: α
c, d: c ∈ ↑s
d⟩, e: (fun x => x * a) c = _b
e⟩⟩
#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 a
orbit_subgroup_eq_rightCoset
#align orbit_add_subgroup_eq_right_coset orbit_addSubgroup_eq_rightCoset: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (a : α), AddAction.orbit { x // x ∈ s } a = ↑s +r a
orbit_addSubgroup_eq_rightCoset

@[to_additive: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {a : α}, a ∈ s → AddAction.orbit { x // x ∈ s } a = ↑s
to_additive]
theorem orbit_subgroup_eq_self_of_mem: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → MulAction.orbit { x // x ∈ s } a = ↑s
orbit_subgroup_eq_self_of_mem {a: α
a : α: Type ?u.67223
α} (ha: a ∈ s
ha : 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 a
orbit_subgroup_eq_rightCoset s: Subgroup α
s a: α
a).trans: ∀ {α : Sort ?u.68623} {a b c : α}, a = b → b = c → a = c
trans (rightCoset_mem_rightCoset: ∀ {α : Type ?u.68637} [inst : Group α] (s : Subgroup α) {a : α}, a ∈ s → ↑s *r a = ↑s
rightCoset_mem_rightCoset s: Subgroup α
s ha: a ∈ s
ha)
#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 = ↑s
orbit_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 = ↑s
orbit_addSubgroup_eq_self_of_mem

@[to_additive: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), AddAction.orbit { x // x ∈ s } 0 = ↑s
to_additive]
theorem orbit_subgroup_one_eq_self: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), MulAction.orbit { x // x ∈ s } 1 = ↑s
orbit_subgroup_one_eq_self : MulAction.orbit: (α : Type ?u.68693) → {β : Type ?u.68692} → [inst : Monoid α] → [inst : MulAction α β] → β → Set β
MulAction.orbit s: Subgroup α
s (1: ?m.68844
1 : α: 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 = ↑s
orbit_subgroup_eq_self_of_mem s: Subgroup α
s s: Subgroup α
s.one_mem: ∀ {G : Type ?u.70307} [inst : Group G] (H : Subgroup G), 1 ∈ H
one_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 = ↑s
orbit_subgroup_one_eq_self
#align orbit_add_subgroup_zero_eq_self orbit_addSubgroup_zero_eq_self: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), AddAction.orbit { x // x ∈ s } 0 = ↑s
orbit_addSubgroup_zero_eq_self

@[to_additive eq_addCosets_of_normal: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), AddSubgroup.Normal s → ∀ (g : α), g +l ↑s = ↑s +r g
eq_addCosets_of_normal]
theorem eq_cosets_of_normal: Normal s → ∀ (g : α), g *l ↑s = ↑s *r g
eq_cosets_of_normal (N: Normal s
N : s: Subgroup α
s.Normal: {G : Type ?u.70344} → [inst : Group G] → Subgroup G → Prop
Normal) (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 = b
Set.ext fun a: ?m.70967
a => by
Goals accomplished! 🐙 α: Type u_1

inst✝: Group α

s: Subgroup α

N: Normal s

g, 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 ∈ s
mem_leftCoset_iff, mem_rightCoset_iff: ∀ {α : Type ?u.71008} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ s *r a ↔ x * a⁻¹ ∈ s
mem_rightCoset_iff]α: Type u_1

inst✝: Group α

s: Subgroup α

N: Normal s

g, a: α

g⁻¹ * a ∈ s ↔ a * g⁻¹ ∈ s;α: Type u_1

inst✝: Group α

s: Subgroup α

N: Normal s

g, a: α

g⁻¹ * a ∈ s ↔ a * g⁻¹ ∈ s α: Type u_1

inst✝: Group α

s: Subgroup α

N: Normal s

g, a: α

a ∈ g *l ↑s ↔ a ∈ ↑s *r grw [α: Type u_1

inst✝: Group α

s: Subgroup α

N: Normal s

g, a: α

g⁻¹ * a ∈ s ↔ a * g⁻¹ ∈ sN: Normal s
N.mem_comm_iff: ∀ {G : Type ?u.71530} [inst : Group G] {H : Subgroup G}, Normal H → ∀ {a b : G}, a * b ∈ H ↔ b * a ∈ H
mem_comm_iffα: Type u_1

inst✝: Group α

s: Subgroup α

N: Normal s

g, 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 g
eq_cosets_of_normal
#align eq_add_cosets_of_normal eq_addCosets_of_normal: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), AddSubgroup.Normal s → ∀ (g : α), g +l ↑s = ↑s +r g
eq_addCosets_of_normal

@[to_additive normal_of_eq_addCosets: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), (∀ (g : α), g +l ↑s = ↑s +r g) → AddSubgroup.Normal s
normal_of_eq_addCosets]
theorem normal_of_eq_cosets: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), (∀ (g : α), g *l ↑s = ↑s *r g) → Normal s
normal_of_eq_cosets (h: ∀ (g : α), g *l ↑s = ↑s *r g
h : ∀ 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 → Prop
Normal :=
  ⟨fun a: ?m.72251
a ha: ?m.72254
ha g: ?m.72257
g =>
    show g: ?m.72257
g * a: ?m.72251
a * g: ?m.72257
g⁻¹ ∈ (s: Subgroup α
s : Set: Type ?u.73488 → Type ?u.73488
Set α: Type ?u.71586
α) by rw [α: Type u_1

inst✝: Group α

s: Subgroup α

h: ∀ (g : α), g *l ↑s = ↑s *r g

a: α

ha: a ∈ s

g: α

g * a * g⁻¹ ∈ ↑s← mem_rightCoset_iff: ∀ {α : Type ?u.73606} [inst : Group α] {s : Set α} {x : α} (a : α), x ∈ s *r a ↔ x * a⁻¹ ∈ s
mem_rightCoset_iff,α: Type u_1

inst✝: Group α

s: Subgroup α

h: ∀ (g : α), g *l ↑s = ↑s *r g

a: α

ha: a ∈ s

g: α

g * a ∈ ↑s *r g α: Type u_1

inst✝: Group α

s: Subgroup α

h: ∀ (g : α), g *l ↑s = ↑s *r g

a: α

ha: a ∈ s

g: α

g * a * g⁻¹ ∈ ↑s← h: ∀ (g : α), g *l ↑s = ↑s *r g
hα: Type u_1

inst✝: Group α

s: Subgroup α

h: ∀ (g : α), g *l ↑s = ↑s *r g

a: α

ha: a ∈ s

g: α

g * a ∈ g *l ↑s]α: Type u_1

inst✝: Group α

s: Subgroup α

h: ∀ (g : α), g *l ↑s = ↑s *r g

a: α

ha: a ∈ s

g: α

g * a ∈ g *l ↑s;α: Type u_1

inst✝: Group α

s: Subgroup α

h: ∀ (g : α), g *l ↑s = ↑s *r g

a: α

ha: a ∈ s

g: α

g * a ∈ g *l ↑s α: Type u_1

inst✝: Group α

s: Subgroup α

h: ∀ (g : α), g *l ↑s = ↑s *r g

a: α

ha: a ∈ s

g: α

g * a * g⁻¹ ∈ ↑sexact mem_leftCoset: ∀ {α : Type ?u.73694} [inst : Mul α] {s : Set α} {x : α} (a : α), x ∈ s → a * x ∈ a *l s
mem_leftCoset g: α
g ha: a ∈ s
ha
Goals 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 s
normal_of_eq_cosets
#align normal_of_eq_add_cosets normal_of_eq_addCosets: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), (∀ (g : α), g +l ↑s = ↑s +r g) → AddSubgroup.Normal s
normal_of_eq_addCosets

@[to_additive normal_iff_eq_addCosets: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), AddSubgroup.Normal s ↔ ∀ (g : α), g +l ↑s = ↑s +r g
normal_iff_eq_addCosets]
theorem normal_iff_eq_cosets: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Normal s ↔ ∀ (g : α), g *l ↑s = ↑s *r g
normal_iff_eq_cosets : s: Subgroup α
s.Normal: {G : Type ?u.74085} → [inst : Group G] → Subgroup G → Prop
Normal ↔ ∀ 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 g
eq_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 s
normal_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 g
normal_iff_eq_cosets
#align normal_iff_eq_add_cosets normal_iff_eq_addCosets: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), AddSubgroup.Normal s ↔ ∀ (g : α), g +l ↑s = ↑s +r g
normal_iff_eq_addCosets

@[to_additive leftAddCoset_eq_iff: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {x y : α}, x +l ↑s = y +l ↑s ↔ -x + y ∈ s
leftAddCoset_eq_iff]
theorem leftCoset_eq_iff: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {x y : α}, x *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ s
leftCoset_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 := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

x *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ srw [α: Type u_1

inst✝: 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 ∈ t
Set.ext_iffα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

(∀ (x_1 : α), x_1 ∈ x *l ↑s ↔ x_1 ∈ y *l ↑s) ↔ x⁻¹ * y ∈ s]α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

(∀ (x_1 : α), x_1 ∈ x *l ↑s ↔ x_1 ∈ y *l ↑s) ↔ x⁻¹ * y ∈ s
  α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

x *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ ssimp_rw [α: Type u_1

inst✝: 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 ∈ s
mem_leftCoset_iff,α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

(∀ (x_1 : α), x⁻¹ * x_1 ∈ ↑s ↔ y⁻¹ * x_1 ∈ ↑s) ↔ x⁻¹ * y ∈ s α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

(∀ (x_1 : α), x_1 ∈ x *l ↑s ↔ x_1 ∈ y *l ↑s) ↔ x⁻¹ * y ∈ sSetLike.mem_coeα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s]α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s
  α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

x *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ sconstructorα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mp(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ s
α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mprx⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
  α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

x *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ s·α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mp(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ s α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mp(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ s
α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mprx⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ sintro h: ?a
hα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s

mpx⁻¹ * y ∈ s
    α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mp(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ sapply (h: ?a
h y: α
y).mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mprα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s

mpy⁻¹ * y ∈ s
    α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mp(∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ srw [α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s

mpy⁻¹ * y ∈ smul_left_inv: ∀ {G : Type ?u.76609} [inst : Group G] (a : G), a⁻¹ * a = 1
mul_left_invα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s

mp1 ∈ s]α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s

mp1 ∈ s
    α: Type u_1

inst✝: 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 ∈ H
one_mem
Goals accomplished! 🐙
  α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

x *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ s·α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mprx⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mprx⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ sintro h: ?b
h z: α
zα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: x⁻¹ * y ∈ s

z: α

mprx⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
    α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mprx⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ srw [α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: x⁻¹ * y ∈ s

z: α

mprx⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s← mul_inv_cancel_right: ∀ {G : Type ?u.76680} [inst : Group G] (a b : G), a * b * b⁻¹ = a
mul_inv_cancel_right x: α
x⁻¹ y: α
yα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: x⁻¹ * y ∈ s

z: α

mprx⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s]α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: x⁻¹ * y ∈ s

z: α

mprx⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
    α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mprx⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ srw [α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: x⁻¹ * y ∈ s

z: α

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_1

inst✝: Group α

s: Subgroup α

x, y: α

h: x⁻¹ * y ∈ s

z: α

mprx⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s]α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: x⁻¹ * y ∈ s

z: α

mprx⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s
    α: Type u_1

inst✝: 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: ?b
h
Goals 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 ∈ s
leftCoset_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 ∈ s
leftAddCoset_eq_iff

@[to_additive rightAddCoset_eq_iff: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) {x y : α}, ↑s +r x = ↑s +r y ↔ y + -x ∈ s
rightAddCoset_eq_iff]
theorem rightCoset_eq_iff: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α) {x y : α}, ↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ s
rightCoset_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 := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ srw [α: Type u_1

inst✝: 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 ∈ t
Set.ext_iffα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

(∀ (x_1 : α), x_1 ∈ ↑s *r x ↔ x_1 ∈ ↑s *r y) ↔ y * x⁻¹ ∈ s]α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

(∀ (x_1 : α), x_1 ∈ ↑s *r x ↔ x_1 ∈ ↑s *r y) ↔ y * x⁻¹ ∈ s
  α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ ssimp_rw [α: Type u_1

inst✝: 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⁻¹ ∈ s
mem_rightCoset_iff,α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

(∀ (x_1 : α), x_1 * x⁻¹ ∈ ↑s ↔ x_1 * y⁻¹ ∈ ↑s) ↔ y * x⁻¹ ∈ s α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

(∀ (x_1 : α), x_1 ∈ ↑s *r x ↔ x_1 ∈ ↑s *r y) ↔ y * x⁻¹ ∈ sSetLike.mem_coeα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s]α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s
  α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ sconstructorα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mp(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s
α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mpry * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
  α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ s·α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mp(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mp(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s
α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mpry * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ sintro h: ?a
hα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s

mpy * x⁻¹ ∈ s
    α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mp(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ sapply (h: ?a
h y: α
y).mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mprα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s

mpy * y⁻¹ ∈ s
    α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mp(∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ srw [α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s

mpy * y⁻¹ ∈ smul_right_inv: ∀ {G : Type ?u.79227} [inst : Group G] (a : G), a * a⁻¹ = 1
mul_right_invα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s

mp1 ∈ s]α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s

mp1 ∈ s
    α: Type u_1

inst✝: 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 ∈ H
one_mem
Goals accomplished! 🐙
  α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ s·α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mpry * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mpry * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ sintro h: ?b
h z: α
zα: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: y * x⁻¹ ∈ s

z: α

mprz * x⁻¹ ∈ s ↔ z * y⁻¹ ∈ s
    α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mpry * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ srw [α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: y * x⁻¹ ∈ s

z: α

mprz * x⁻¹ ∈ s ↔ z * y⁻¹ ∈ s← inv_mul_cancel_left: ∀ {G : Type ?u.79296} [inst : Group G] (a b : G), a⁻¹ * (a * b) = b
inv_mul_cancel_left y: α
y x: α
x⁻¹α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: y * x⁻¹ ∈ s

z: α

mprz * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s]α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: y * x⁻¹ ∈ s

z: α

mprz * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s
    α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

mpry * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ srw [α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: y * x⁻¹ ∈ s

z: α

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_1

inst✝: Group α

s: Subgroup α

x, y: α

h: y * x⁻¹ ∈ s

z: α

mprz * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s]α: Type u_1

inst✝: Group α

s: Subgroup α

x, y: α

h: y * x⁻¹ ∈ s

z: α

mprz * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s
    α: Type u_1

inst✝: 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: ?b
h
Goals 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⁻¹ ∈ s
rightCoset_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 ∈ s
rightAddCoset_eq_iff

end CosetSubgroup

-- porting note: see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20to_additive.2Emap_namespace
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 Unit
ToAdditive.insertTranslation `QuotientGroup: Lean.Name
`QuotientGroup `QuotientAddGroup: Lean.Name
`QuotientAddGroup

namespace QuotientGroup

variable [Group: Type ?u.93719 → Type ?u.93719
Group α: Type ?u.90703
α] (s: Subgroup α
s : Subgroup: (G : Type ?u.90726) → [inst : Group G] → Type ?u.90726
Subgroup α: 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
#align quotient_add_group.left_rel QuotientAddGroup.leftRel: {α : Type u_1} → [inst : AddGroup α] → AddSubgroup α → Setoid α
QuotientAddGroup.leftRel

variable {s: ?m.80922
s}

@[to_additive: ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {x y : α}, Setoid.r x y ↔ -x + y ∈ s
to_additive]
theorem leftRel_apply: ∀ {x y : α}, Setoid.r x y ↔ x⁻¹ * y ∈ s
leftRel_apply {x: α
x y: α
y : α: Type ?u.80925
α} : @Setoid.r: {α : Sort ?u.80943} → [self : Setoid α] → α → α → Prop
Setoid.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⁻¹ :=
      by
Goals accomplished! 🐙 α: Type u_1

inst✝: 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 * c
inv_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 = b
eq_mul_inv_iff_mul_eq]
Goals accomplished! 🐙
    _: ?m✝
_ ↔ x: α
x⁻¹ * y: α
y ∈ s: Subgroup α
s := by
Goals accomplished! 🐙 α: Type u_1

inst✝: 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 x
exists_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 ∈ s
QuotientGroup.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 ∈ s
QuotientAddGroup.leftRel_apply

variable (s: ?m.90717
s)

@[to_additive: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), Setoid.r = fun x y => -x + y ∈ s
to_additive]
theorem leftRel_eq: Setoid.r = fun x y => x⁻¹ * y ∈ s
leftRel_eq : @Setoid.r: {α : Sort ?u.90735} → [self : Setoid α] → α → α → Prop
Setoid.r _: Sort ?u.90735
_ (leftRel: {α : Type ?u.90737} → [inst : Group α] → Subgroup α → Setoid α
leftRel s: Subgroup α
s) = fun x: ?m.90770
x y: ?m.90773
y => x: ?m.90770
x⁻¹ * y: ?m.90773
y ∈ 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 = g
funext₂ <| by
Goals accomplished! 🐙
    α: Type u_1

inst✝: 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_1

inst✝: Group α

s: Subgroup α

∀ (a b : α), Setoid.r a b ↔ a⁻¹ * b ∈ s
    α: Type u_1

inst✝: 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 ∈ s
leftRel_apply
Goals accomplished! 🐙
#align quotient_group.left_rel_eq QuotientGroup.leftRel_eq: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Setoid.r = fun x y => x⁻¹ * y ∈ s
QuotientGroup.leftRel_eq
#align quotient_add_group.left_rel_eq QuotientAddGroup.leftRel_eq: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), Setoid.r = fun x y => -x + y ∈ s
QuotientAddGroup.leftRel_eq

theorem leftRel_r_eq_leftCosetEquivalence: Setoid.r = LeftCosetEquivalence ↑s
leftRel_r_eq_leftCosetEquivalence :
    @Setoid.r: {α : Sort ?u.91866} → [self : Setoid α] → α → α → Prop
Setoid.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 α → α → α → Prop
LeftCosetEquivalence s: Subgroup α
s := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: Group α

s: Subgroup α

Setoid.r = LeftCosetEquivalence ↑sextα: Type u_1

inst✝: Group α

s: Subgroup α

x✝¹, x✝: α

h.h.aSetoid.r x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝
  α: Type u_1

inst✝: Group α

s: Subgroup α

Setoid.r = LeftCosetEquivalence ↑srw [α: Type u_1

inst✝: 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 ∈ s
leftRel_eqα: Type u_1

inst✝: Group α

s: Subgroup α

x✝¹, x✝: α

h.h.a(fun x y => x⁻¹ * y ∈ s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝]α: Type u_1

inst✝: Group α

s: Subgroup α

x✝¹, x✝: α

h.h.a(fun x y => x⁻¹ * y ∈ s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝
  α: Type u_1

inst✝: 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 ∈ s
leftCoset_eq_iff s: Subgroup α
s).symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
symm
Goals 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 ↑s
QuotientGroup.leftRel_r_eq_leftCosetEquivalence

@[to_additive: {α : Type u_1} →
  [inst : AddGroup α] → (s : AddSubgroup α) → [inst_1 : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.r
to_additive]
instance leftRelDecidable: [inst : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.r
leftRelDecidable [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 α] → α → α → Prop
r := fun x: ?m.92950
x y: ?m.92953
y => by
Goals accomplished! 🐙
  α: Type ?u.92864

inst✝¹: Group α

s: Subgroup α

inst✝: DecidablePred fun x => x ∈ s

x, y: α

Decidable (Setoid.r x y)rw [α: Type ?u.92864

inst✝¹: Group α

s: Subgroup α

inst✝: DecidablePred fun x => x ∈ s

x, y: α

Decidable (Setoid.r x y)leftRel_eq: ∀ {α : Type ?u.92960} [inst : Group α] (s : Subgroup α), Setoid.r = fun x y => x⁻¹ * y ∈ s
leftRel_eqα: Type ?u.92864

inst✝¹: Group α

s: Subgroup α

inst✝: DecidablePred fun x => x ∈ s

x, y: α

Decidable ((fun x y => x⁻¹ * y ∈ s) x y)]α: Type ?u.92864

inst✝¹: Group α

s: Subgroup α

inst✝: DecidablePred fun x => x ∈ s

x, y: α

Decidable ((fun x y => x⁻¹ * y ∈ s) x y)
  α: Type ?u.92864

inst✝¹: Group α

s: Subgroup α

inst✝: DecidablePred fun x => x ∈ s

x, 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.r
QuotientGroup.leftRelDecidable
#align quotient_add_group.left_rel_decidable QuotientAddGroup.leftRelDecidable: {α : Type u_1} →
  [inst : AddGroup α] → (s : AddSubgroup α) → [inst_1 : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.r
QuotientAddGroup.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.93576
Subgroup α: Type ?u.93560
α) :=
  ⟨fun s: ?m.93593
s => Quotient: {α : Sort ?u.93595} → Setoid α → Sort ?u.93595
Quotient (leftRel: {α : Type ?u.93597} → [inst : Group α] → Subgroup α → Setoid α
leftRel s: ?m.93593
s)⟩

/-- 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
#align quotient_add_group.right_rel QuotientAddGroup.rightRel: {α : Type u_1} → [inst : AddGroup α] → AddSubgroup α → Setoid α
QuotientAddGroup.rightRel

variable {s: ?m.95053
s}

@[to_additive: ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} {x y : α}, Setoid.r x y ↔ y + -x ∈ s
to_additive]
theorem rightRel_apply: ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {x y : α}, Setoid.r x y ↔ y * x⁻¹ ∈ s
rightRel_apply {x: α
x y: α
y : α: Type ?u.95056
α} : @Setoid.r: {α : Sort ?u.95074} → [self : Setoid α] → α → α → Prop
Setoid.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⁻¹ :=
      by
Goals accomplished! 🐙 α: Type u_1

inst✝: 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 * b
mul_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 = c
eq_inv_mul_iff_mul_eq]
Goals accomplished! 🐙
    _: ?m✝
_ ↔ y: α
y * x: α
x⁻¹ ∈ s: Subgroup α
s := by
Goals accomplished! 🐙 α: Type u_1

inst✝: 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 x
exists_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⁻¹ ∈ s
QuotientGroup.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 ∈ s
QuotientAddGroup.rightRel_apply

variable (s: ?m.103695
s)

@[to_additive: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), Setoid.r = fun x y => y + -x ∈ s
to_additive]
theorem rightRel_eq: Setoid.r = fun x y => y * x⁻¹ ∈ s
rightRel_eq : @Setoid.r: {α : Sort ?u.103713} → [self : Setoid α] → α → α → Prop
Setoid.r _: Sort ?u.103713
_ (rightRel: {α : Type ?u.103715} → [inst : Group α] → Subgroup α → Setoid α
rightRel s: Subgroup α
s) = fun x: ?m.103748
x y: ?m.103751
y => y: ?m.103751
y * x: ?m.103748
x⁻¹ ∈ 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 = g
funext₂ <| by
Goals accomplished! 🐙
    α: Type u_1

inst✝: 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_1

inst✝: Group α

s: Subgroup α

∀ (a b : α), Setoid.r a b ↔ b * a⁻¹ ∈ s
    α: Type u_1

inst✝: 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⁻¹ ∈ s
rightRel_apply
Goals accomplished! 🐙
#align quotient_group.right_rel_eq QuotientGroup.rightRel_eq: ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), Setoid.r = fun x y => y * x⁻¹ ∈ s
QuotientGroup.rightRel_eq
#align quotient_add_group.right_rel_eq QuotientAddGroup.rightRel_eq: ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), Setoid.r = fun x y => y + -x ∈ s
QuotientAddGroup.rightRel_eq

theorem rightRel_r_eq_rightCosetEquivalence: Setoid.r = RightCosetEquivalence ↑s
rightRel_r_eq_rightCosetEquivalence :
    @Setoid.r: {α : Sort ?u.104836} → [self : Setoid α] → α → α → Prop
Setoid.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 α → α → α → Prop
RightCosetEquivalence s: Subgroup α
s := by
Goals accomplished! 🐙
  α: Type u_1

inst✝: Group α

s: Subgroup α

Setoid.r = RightCosetEquivalence ↑sextα: Type u_1

inst✝: Group α

s: Subgroup α

x✝¹, x✝: α

h.h.aSetoid.r x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝
  α: Type u_1

inst✝: Group α

s: Subgroup α

Setoid.r = RightCosetEquivalence ↑srw [α: Type u_1

inst✝: 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⁻¹ ∈ s
rightRel_eqα: Type u_1

inst✝: Group α

s: Subgroup α

x✝¹, x✝: α

h.h.a(fun x y => y * x⁻¹ ∈ s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝]α: Type u_1

inst✝: Group α

s: Subgroup α

x✝¹, x✝: α

h.h.a(fun x y => y * x⁻¹ ∈ s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝
  α: Type u_1

inst✝: 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⁻¹ ∈ s
rightCoset_eq_iff s: Subgroup α
s).symm: ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
symm
Goals 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 ↑s
QuotientGroup.rightRel_r_eq_rightCosetEquivalence

@[to_additive: {α : Type u_1} →
  [inst : AddGroup α] → (s : AddSubgroup α) → [inst_1 : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.r
to_additive]
instance rightRelDecidable: [inst : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.r
rightRelDecidable [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 α] → α → α → Prop
r := fun x: ?m.105920
x y: ?m.105923
y => by
Goals accomplished! 🐙
  α: Type ?u.105834

inst✝¹: Group α

s: Subgroup α

inst✝: DecidablePred fun x => x ∈ s

x, y: α

Decidable (Setoid.r x y)rw [α: Type ?u.105834

inst✝¹: Group α

s: Subgroup α

inst✝: DecidablePred fun x => x ∈ s

x, y: α

Decidable (Setoid.r x y)rightRel_eq: ∀ {α : Type ?u.105930} [inst : Group α] (s : Subgroup α), Setoid.r = fun x y => y * x⁻¹ ∈ s
rightRel_eqα: Type ?u.105834

inst✝¹: Group α

s: Subgroup α

inst✝: DecidablePred fun x => x ∈ s

x, y: α

Decidable ((fun x y => y * x⁻¹ ∈ s) x y)]α: Type ?u.105834

inst✝¹: Group α

s: Subgroup α

inst✝: DecidablePred fun x => x ∈ s

x, y: α

Decidable ((fun x y => y * x⁻¹ ∈ s) x y)
  α: Type ?u.105834

inst✝¹: Group α

s: Subgroup α

inst✝: DecidablePred fun x => x ∈ s

x, 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.r
QuotientGroup.rightRelDecidable
#align quotient_add_group.right_rel_decidable QuotientAddGroup.rightRelDecidable: {α : Type u_1} →
  [inst : AddGroup α] → (s : AddSubgroup α) → [inst_1 : DecidablePred fun x => x ∈ s] → DecidableRel Setoid.r
QuotientAddGroup.rightRelDecidable

/-- Right cosets are in bijection with left cosets. -/
@[to_additive: {α : Type u_1} → [inst : AddGroup α] → (s : AddSubgroup α) → Quotient (QuotientAddGroup.rightRel s) ≃ α ⧸ s
to_additive "Right cosets are in bijection with left cosets."]
def quotientRightRelEquivQuotientLeftRel: Quotient (rightRel s) ≃ α ⧸ s
quotientRightRelEquivQuotientLeftRel : Quotient: {α : Sort ?u.106498} → Setoid α → Sort ?u.106498
Quotient (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.106566
g => g: ?m.106566
g⁻¹) fun a: ?m.106731
a b: ?m.106734
b => by
Goals accomplished! 🐙
      α: Type ?u.106482

inst✝: Group α

s: Subgroup α

a, b: α

Setoid.r a b → Setoid.r ((fun g => g⁻¹) a) ((fun g => g⁻¹) b)rw [α: Type ?u.106482

inst✝: 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 ∈ s
leftRel_apply,α: Type ?u.106482

inst✝: Group α

s: Subgroup α

a, b: α

Setoid.r a b → ((fun g => g⁻¹) a)⁻¹ * (fun g => g⁻¹) b ∈ s α: Type ?u.106482

inst✝: 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⁻¹ ∈ s
rightRel_applyα: Type ?u.106482

inst✝: Group α

s: Subgroup α

a, b: α

b * a⁻¹ ∈ s → ((fun g => g⁻¹) a)⁻¹ * (fun g => g⁻¹) b ∈ s]α: Type ?u.106482

inst✝: Group α

s: Subgroup α

a, b: α

b * a⁻¹ ∈ s → ((fun g => g⁻¹) a)⁻¹ * (fun g => g⁻¹) b ∈ s
      α: Type ?u.106482

inst✝: Group α

s: Subgroup α

a, b: α

Setoid.r a b → Setoid.r ((fun g => g⁻¹) a) ((fun g => g⁻¹) b)exact fun h: ?m.107131
h => (congr_arg: ∀ {α : Sort ?u.107134} {β : Sort ?u.107133} {a₁ a₂ : α} (f : α → β), a₁ = a₂ → f a₁ = f a₂
congr_arg (· ∈ s: Subgroup α
s) (α: Type ?u.106482

inst✝: Group α

s: Subgroup α

a, b: α

b * a⁻¹ ∈ s → ((fun g => g⁻¹) a)⁻¹ * (fun g => g⁻¹) b ∈ sby
Goals accomplished! 🐙 α: Type ?u.106482

inst✝: 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⁻¹ ∈ H
inv_mem h: ?m.107131
h)
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.106752
g => g: ?m.106752