[GOAL]
α : Type u_1
inst✝ : Semigroup α
s : Set α
a b : α
⊢ a *l (b *l s) = a * b *l s
[PROOFSTEP]
simp [leftCoset, rightCoset, (image_comp _ _ _).symm, Function.comp, mul_assoc]
[GOAL]
α : Type u_1
inst✝ : Semigroup α
s : Set α
a b : α
⊢ s *r a *r b = s *r (a * b)
[PROOFSTEP]
simp [leftCoset, rightCoset, (image_comp _ _ _).symm, Function.comp, mul_assoc]
[GOAL]
α : Type u_1
inst✝ : Semigroup α
s : Set α
a b : α
⊢ a *l s *r b = a *l (s *r b)
[PROOFSTEP]
simp [leftCoset, rightCoset, (image_comp _ _ _).symm, Function.comp, mul_assoc]
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Set α
⊢ ∀ (x : α), x ∈ 1 *l s ↔ x ∈ s
[PROOFSTEP]
simp [leftCoset]
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Set α
⊢ ∀ (x : α), x ∈ s *r 1 ↔ x ∈ s
[PROOFSTEP]
simp [rightCoset]
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
this : a * 1 ∈ a *l ↑s
⊢ a ∈ a *l ↑s
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
this : 1 * a ∈ ↑s *r a
⊢ a ∈ ↑s *r a
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a *l ↑s = ↑s
⊢ a ∈ s
[PROOFSTEP]
rw [← SetLike.mem_coe, ← ha]
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : a *l ↑s = ↑s
⊢ a ∈ a *l ↑s
[PROOFSTEP]
exact mem_own_leftCoset s a
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : ↑s *r a = ↑s
⊢ a ∈ s
[PROOFSTEP]
rw [← SetLike.mem_coe, ← ha]
[GOAL]
α : Type u_1
inst✝ : Monoid α
s : Submonoid α
a : α
ha : ↑s *r a = ↑s
⊢ a ∈ ↑s *r a
[PROOFSTEP]
exact mem_own_rightCoset s a
[GOAL]
α : 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 ∈ s
[PROOFSTEP]
simp [Eq.symm, hb]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Set α
x a : α
h : a⁻¹ * x ∈ s
⊢ (fun x => a * x) (a⁻¹ * x) = x
[PROOFSTEP]
simp
[GOAL]
α : 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⁻¹ ∈ s
[PROOFSTEP]
simp [Eq.symm, hb]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Set α
x a : α
h : x * a⁻¹ ∈ s
⊢ (fun x => x * a) (x * a⁻¹) = x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
⊢ ∀ (x : α), x ∈ a *l ↑s ↔ x ∈ ↑s
[PROOFSTEP]
simp [mem_leftCoset_iff, mul_mem_cancel_left (s.inv_mem ha)]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a : α
ha : a ∈ s
b : α
⊢ b ∈ ↑s *r a ↔ b ∈ ↑s
[PROOFSTEP]
simp [mem_rightCoset_iff, mul_mem_cancel_right (s.inv_mem ha)]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
N : Normal s
g a : α
⊢ a ∈ g *l ↑s ↔ a ∈ ↑s *r g
[PROOFSTEP]
simp [mem_leftCoset_iff, mem_rightCoset_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
N : Normal s
g a : α
⊢ g⁻¹ * a ∈ s ↔ a * g⁻¹ ∈ s
[PROOFSTEP]
rw [N.mem_comm_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g *l ↑s = ↑s *r g
a : α
ha : a ∈ s
g : α
⊢ g * a * g⁻¹ ∈ ↑s
[PROOFSTEP]
rw [← mem_rightCoset_iff, ← h]
[GOAL]
α : 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
[PROOFSTEP]
exact mem_leftCoset g ha
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ x *l ↑s = y *l ↑s ↔ x⁻¹ * y ∈ s
[PROOFSTEP]
rw [Set.ext_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ x *l ↑s ↔ x_1 ∈ y *l ↑s) ↔ x⁻¹ * y ∈ s
[PROOFSTEP]
simp_rw [mem_leftCoset_iff, SetLike.mem_coe]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) ↔ x⁻¹ * y ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s) → x⁻¹ * y ∈ s
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ x⁻¹ * y ∈ s
[PROOFSTEP]
apply (h y).mpr
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ y⁻¹ * y ∈ s
[PROOFSTEP]
rw [mul_left_inv]
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
⊢ 1 ∈ s
[PROOFSTEP]
exact s.one_mem
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ x⁻¹ * y ∈ s → ∀ (x_1 : α), x⁻¹ * x_1 ∈ s ↔ y⁻¹ * x_1 ∈ s
[PROOFSTEP]
intro h z
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
[PROOFSTEP]
rw [← mul_inv_cancel_right x⁻¹ y]
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * y⁻¹ * z ∈ s ↔ y⁻¹ * z ∈ s
[PROOFSTEP]
rw [mul_assoc]
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : x⁻¹ * y ∈ s
z : α
⊢ x⁻¹ * y * (y⁻¹ * z) ∈ s ↔ y⁻¹ * z ∈ s
[PROOFSTEP]
exact s.mul_mem_cancel_left h
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ ↑s *r x = ↑s *r y ↔ y * x⁻¹ ∈ s
[PROOFSTEP]
rw [Set.ext_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ ↑s *r x ↔ x_1 ∈ ↑s *r y) ↔ y * x⁻¹ ∈ s
[PROOFSTEP]
simp_rw [mem_rightCoset_iff, SetLike.mem_coe]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ y * x⁻¹ ∈ s
[PROOFSTEP]
apply (h y).mpr
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ y * y⁻¹ ∈ s
[PROOFSTEP]
rw [mul_right_inv]
[GOAL]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ 1 ∈ s
[PROOFSTEP]
exact s.one_mem
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ y * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
[PROOFSTEP]
intro h z
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * x⁻¹ ∈ s ↔ z * y⁻¹ ∈ s
[PROOFSTEP]
rw [← inv_mul_cancel_left y x⁻¹]
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s
[PROOFSTEP]
rw [← mul_assoc]
[GOAL]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s
[PROOFSTEP]
exact s.mul_mem_cancel_right h
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, y * ↑a = x) ↔ ∃ a, x⁻¹ * y = ↑a⁻¹
[PROOFSTEP]
simp only [inv_mul_eq_iff_eq_mul, Subgroup.coe_inv, eq_mul_inv_iff_mul_eq]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, x⁻¹ * y = ↑a⁻¹) ↔ x⁻¹ * y ∈ s
[PROOFSTEP]
simp [exists_inv_mem_iff_exists_mem]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), Setoid.r a b = (a⁻¹ * b ∈ s)
[PROOFSTEP]
simp only [eq_iff_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), Setoid.r a b ↔ a⁻¹ * b ∈ s
[PROOFSTEP]
apply leftRel_apply
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Setoid.r = LeftCosetEquivalence ↑s
[PROOFSTEP]
ext
[GOAL]
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ Setoid.r x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝
[PROOFSTEP]
rw [leftRel_eq]
[GOAL]
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y => x⁻¹ * y ∈ s) x✝¹ x✝ ↔ LeftCosetEquivalence (↑s) x✝¹ x✝
[PROOFSTEP]
exact (leftCoset_eq_iff s).symm
[GOAL]
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x => x ∈ s
x y : α
⊢ Decidable (Setoid.r x y)
[PROOFSTEP]
rw [leftRel_eq]
[GOAL]
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x => x ∈ s
x y : α
⊢ Decidable ((fun x y => x⁻¹ * y ∈ s) x y)
[PROOFSTEP]
exact ‹DecidablePred (· ∈ s)› _
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, ↑a * y = x) ↔ ∃ a, y * x⁻¹ = ↑a⁻¹
[PROOFSTEP]
simp only [mul_inv_eq_iff_eq_mul, Subgroup.coe_inv, eq_inv_mul_iff_mul_eq]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∃ a, y * x⁻¹ = ↑a⁻¹) ↔ y * x⁻¹ ∈ s
[PROOFSTEP]
simp [exists_inv_mem_iff_exists_mem]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), Setoid.r a b = (b * a⁻¹ ∈ s)
[PROOFSTEP]
simp only [eq_iff_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ ∀ (a b : α), Setoid.r a b ↔ b * a⁻¹ ∈ s
[PROOFSTEP]
apply rightRel_apply
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
⊢ Setoid.r = RightCosetEquivalence ↑s
[PROOFSTEP]
ext
[GOAL]
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ Setoid.r x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝
[PROOFSTEP]
rw [rightRel_eq]
[GOAL]
case h.h.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
x✝¹ x✝ : α
⊢ (fun x y => y * x⁻¹ ∈ s) x✝¹ x✝ ↔ RightCosetEquivalence (↑s) x✝¹ x✝
[PROOFSTEP]
exact (rightCoset_eq_iff s).symm
[GOAL]
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x => x ∈ s
x y : α
⊢ Decidable (Setoid.r x y)
[PROOFSTEP]
rw [rightRel_eq]
[GOAL]
α : Type u_1
inst✝¹ : Group α
s : Subgroup α
inst✝ : DecidablePred fun x => x ∈ s
x y : α
⊢ Decidable ((fun x y => y * x⁻¹ ∈ s) x y)
[PROOFSTEP]
exact ‹DecidablePred (· ∈ s)› _
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ Setoid.r a b → Setoid.r ((fun g => g⁻¹) a) ((fun g => g⁻¹) b)
[PROOFSTEP]
rw [leftRel_apply, rightRel_apply]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ b * a⁻¹ ∈ s → ((fun g => g⁻¹) a)⁻¹ * (fun g => g⁻¹) b ∈ s
[PROOFSTEP]
exact fun h =>
  (congr_arg (· ∈ s) (by simp [mul_assoc])).mp
    (s.inv_mem h)
      -- porting note: replace with `by group`
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
h : b * a⁻¹ ∈ s
⊢ (b * a⁻¹)⁻¹ = ((fun g => g⁻¹) a)⁻¹ * (fun g => g⁻¹) b
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ Setoid.r a b → Setoid.r ((fun g => g⁻¹) a) ((fun g => g⁻¹) b)
[PROOFSTEP]
rw [leftRel_apply, rightRel_apply]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ a⁻¹ * b ∈ s → (fun g => g⁻¹) b * ((fun g => g⁻¹) a)⁻¹ ∈ s
[PROOFSTEP]
exact fun h =>
  (congr_arg (· ∈ s) (by simp [mul_assoc])).mp
    (s.inv_mem h)
      -- porting note: replace with `by group`
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
h : a⁻¹ * b ∈ s
⊢ (a⁻¹ * b)⁻¹ = (fun g => g⁻¹) b * ((fun g => g⁻¹) a)⁻¹
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : Quotient (rightRel s)
g : α
⊢ Setoid.r ((fun g => g⁻¹) ((fun g => g⁻¹) g)) g
[PROOFSTEP]
simp only [inv_inv]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : Quotient (rightRel s)
g : α
⊢ Setoid.r g g
[PROOFSTEP]
exact Quotient.exact' rfl
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α ⧸ s
g : α
⊢ Setoid.r ((fun g => g⁻¹) ((fun g => g⁻¹) g)) g
[PROOFSTEP]
simp only [inv_inv]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α ⧸ s
g : α
⊢ Setoid.r g g
[PROOFSTEP]
exact Quotient.exact' rfl
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a b : α
⊢ Setoid.r a b ↔ a⁻¹ * b ∈ s
[PROOFSTEP]
rw [leftRel_apply]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
⊢ Quotient.out' ↑g = g * ↑{ val := g⁻¹ * Quotient.out' ↑g, property := (_ : g⁻¹ * Quotient.out' ↑g ∈ s) }
[PROOFSTEP]
rw [mul_inv_cancel_left]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
a✝ b a : α
hb : b ∈ s
⊢ ↑(a * b) = ↑a
[PROOFSTEP]
rwa [eq', mul_inv_rev, inv_mul_cancel_right, s.inv_mem_iff]
[GOAL]
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
s : Subgroup α
g z : α
⊢ z ∈ {x | ↑x = ↑g} ↔ z ∈ g *l ↑s
[PROOFSTEP]
rw [mem_leftCoset_iff, Set.mem_setOf_eq, eq_comm, QuotientGroup.eq, SetLike.mem_coe]
[GOAL]
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
⊢ mk ⁻¹' (mk '' s) = ⋃ (x : { x // x ∈ N }), (fun x_1 => x_1 * ↑x) ⁻¹' s
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
⊢ x ∈ mk ⁻¹' (mk '' s) ↔ x ∈ ⋃ (x : { x // x ∈ N }), (fun x_1 => x_1 * ↑x) ⁻¹' s
[PROOFSTEP]
simp only [QuotientGroup.eq, SetLike.exists, exists_prop, Set.mem_preimage, Set.mem_iUnion, Set.mem_image, ←
  eq_inv_mul_iff_mul_eq]
[GOAL]
case h
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
⊢ (∃ x_1, x_1 ∈ s ∧ x_1⁻¹ * x ∈ N) ↔ ∃ x_1, x_1 ∈ N ∧ x * x_1 ∈ s
[PROOFSTEP]
exact ⟨fun ⟨y, hs, hN⟩ => ⟨_, N.inv_mem hN, by simpa using hs⟩, fun ⟨z, hz, hxz⟩ => ⟨x * z, hxz, by simpa using hz⟩⟩
[GOAL]
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
x✝ : ∃ x_1, x_1 ∈ s ∧ x_1⁻¹ * x ∈ N
y : α
hs : y ∈ s
hN : y⁻¹ * x ∈ N
⊢ x * (y⁻¹ * x)⁻¹ ∈ s
[PROOFSTEP]
simpa using hs
[GOAL]
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
x : α
x✝ : ∃ x_1, x_1 ∈ N ∧ x * x_1 ∈ s
z : α
hz : z ∈ N
hxz : x * z ∈ s
⊢ (x * z)⁻¹ * x ∈ N
[PROOFSTEP]
simpa using hz
[GOAL]
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
⊢ mk ⁻¹' (mk '' s) = ⋃ (x : { x // x ∈ N }), (fun x_1 => x_1 * ↑x) '' s
[PROOFSTEP]
rw [preimage_image_mk, iUnion_congr_of_surjective (·⁻¹) inv_surjective]
[GOAL]
α : Type u_1
inst✝ : Group α
s✝ : Subgroup α
a b : α
N : Subgroup α
s : Set α
⊢ ∀ (x : { x // x ∈ N }), (fun x_1 => x_1 * ↑x⁻¹) '' s = (fun x_1 => x_1 * ↑x) ⁻¹' s
[PROOFSTEP]
exact fun x ↦ image_mul_right'
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
x✝ : ↑(g *l ↑s)
x : α
hx : x ∈ g *l ↑s
⊢ ↑((fun x => { val := g * ↑x, property := (_ : ∃ a, a ∈ ↑s ∧ (fun x => g * x) a = g * ↑x) })
        ((fun x => { val := g⁻¹ * ↑x, property := (_ : g⁻¹ * ↑x ∈ ↑s) }) { val := x, property := hx })) =
    ↑{ val := x, property := hx }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α
x✝ : { x // x ∈ s }
g : α
hg : g ∈ s
⊢ ↑((fun x => { val := g✝⁻¹ * ↑x, property := (_ : g✝⁻¹ * ↑x ∈ ↑s) })
        ((fun x => { val := g✝ * ↑x, property := (_ : ∃ a, a ∈ ↑s ∧ (fun x => g✝ * x) a = g✝ * ↑x) })
          { val := g, property := hg })) =
    ↑{ val := g, property := hg }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
x✝ : ↑(↑s *r g)
x : α
hx : x ∈ ↑s *r g
⊢ ↑((fun x => { val := ↑x * g, property := (_ : ∃ a, a ∈ ↑s ∧ (fun x => x * g) a = ↑x * g) })
        ((fun x => { val := ↑x * g⁻¹, property := (_ : ↑x * g⁻¹ ∈ ↑s) }) { val := x, property := hx })) =
    ↑{ val := x, property := hx }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
g✝ : α
x✝ : { x // x ∈ s }
g : α
hg : g ∈ s
⊢ ↑((fun x => { val := ↑x * g✝⁻¹, property := (_ : ↑x * g✝⁻¹ ∈ ↑s) })
        ((fun x => { val := ↑x * g✝, property := (_ : ∃ a, a ∈ ↑s ∧ (fun x => x * g✝) a = ↑x * g✝) })
          { val := g, property := hg })) =
    ↑{ val := g, property := hg }
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // ↑x = L } ≃ ↑(Quotient.out' L *l ↑s)
[PROOFSTEP]
rw [← eq_class_eq_leftCoset]
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // ↑x = L } ≃ ↑{x | ↑x = ↑(Quotient.out' L)}
[PROOFSTEP]
show (_root_.Subtype fun x : α => Quotient.mk'' x = L) ≃ _root_.Subtype fun x : α => Quotient.mk'' x = Quotient.mk'' _
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // Quotient.mk'' x = L } ≃ { x // Quotient.mk'' x = Quotient.mk'' (Quotient.out' L) }
[PROOFSTEP]
simp [-Quotient.eq'']
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
L : α ⧸ s
⊢ { x // Quotient.mk'' x = L } ≃ { x // Quotient.mk'' x = L }
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : Setoid.r b c
⊢ Setoid.r ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) b)
    ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) c)
[PROOFSTEP]
rw [leftRel_apply]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : Setoid.r b c
⊢ ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) b)⁻¹ *
      (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) c ∈
    subgroupOf s t
[PROOFSTEP]
change ((f b)⁻¹ * b)⁻¹ * ((f c)⁻¹ * c) ∈ s
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : Setoid.r b c
⊢ ((f ↑b)⁻¹ * b)⁻¹ * ((f ↑c)⁻¹ * c) ∈ s
[PROOFSTEP]
have key : f b = f c := congr_arg f (Quotient.sound' (leftRel_apply.mpr (h_le (leftRel_apply.mp h))))
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α ⧸ s
b c : α
h : Setoid.r b c
key : f ↑b = f ↑c
⊢ ((f ↑b)⁻¹ * b)⁻¹ * ((f ↑c)⁻¹ * c) ∈ s
[PROOFSTEP]
rwa [key, mul_inv_rev, inv_inv, mul_assoc, mul_inv_cancel_left, ← leftRel_apply]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : (α ⧸ t) × { x // x ∈ t } ⧸ subgroupOf s t
⊢ α ⧸ s
[PROOFSTEP]
refine
  a.2.map' (fun (b : { x // x ∈ t }) => f a.1 * b) fun b c h =>
    by
    rw [leftRel_apply] at h ⊢
    change (f a.1 * b)⁻¹ * (f a.1 * c) ∈ s
    rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : (α ⧸ t) × { x // x ∈ t } ⧸ subgroupOf s t
b c : { x // x ∈ t }
h : Setoid.r b c
⊢ Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c)
[PROOFSTEP]
rw [leftRel_apply] at h ⊢
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : (α ⧸ t) × { x // x ∈ t } ⧸ subgroupOf s t
b c : { x // x ∈ t }
h : b⁻¹ * c ∈ subgroupOf s t
⊢ ((fun b => f a.fst * ↑b) b)⁻¹ * (fun b => f a.fst * ↑b) c ∈ s
[PROOFSTEP]
change (f a.1 * b)⁻¹ * (f a.1 * c) ∈ s
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : (α ⧸ t) × { x // x ∈ t } ⧸ subgroupOf s t
b c : { x // x ∈ t }
h : b⁻¹ * c ∈ subgroupOf s t
⊢ (f a.fst * ↑b)⁻¹ * (f a.fst * ↑c) ∈ s
[PROOFSTEP]
rwa [mul_inv_rev, mul_assoc, inv_mul_cancel_left]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
⊢ LeftInverse
    (fun a =>
      Quotient.map' (fun b => f a.fst * ↑b)
        (_ : ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
        a.snd)
    fun a =>
    (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
      Quotient.map' (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
        (_ :
          ∀ (b c : α),
            Setoid.r b c →
              Setoid.r
                ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) b)
                ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                  c))
        a)
[PROOFSTEP]
refine' Quotient.ind' fun a => _
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α
⊢ (fun a =>
        Quotient.map' (fun b => f a.fst * ↑b)
          (_ :
            ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
          a.snd)
      ((fun a =>
          (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
            Quotient.map'
              (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
              (_ :
                ∀ (b c : α),
                  Setoid.r b c →
                    Setoid.r
                      ((fun g =>
                          { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                        b)
                      ((fun g =>
                          { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                        c))
              a))
        (Quotient.mk'' a)) =
    Quotient.mk'' a
[PROOFSTEP]
simp_rw [Quotient.map'_mk'', id.def, mul_inv_cancel_left]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
⊢ Function.RightInverse
    (fun a =>
      Quotient.map' (fun b => f a.fst * ↑b)
        (_ : ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
        a.snd)
    fun a =>
    (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
      Quotient.map' (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
        (_ :
          ∀ (b c : α),
            Setoid.r b c →
              Setoid.r
                ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) }) b)
                ((fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                  c))
        a)
[PROOFSTEP]
refine' Prod.rec _
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
⊢ ∀ (fst : α ⧸ t) (snd : { x // x ∈ t } ⧸ subgroupOf s t),
    (fun a =>
          (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
            Quotient.map'
              (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
              (_ :
                ∀ (b c : α),
                  Setoid.r b c →
                    Setoid.r
                      ((fun g =>
                          { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                        b)
                      ((fun g =>
                          { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                        c))
              a))
        ((fun a =>
            Quotient.map' (fun b => f a.fst * ↑b)
              (_ :
                ∀ (b c : { x // x ∈ t }),
                  Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
              a.snd)
          (fst, snd)) =
      (fst, snd)
[PROOFSTEP]
refine' Quotient.ind' fun a => _
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α
⊢ ∀ (snd : { x // x ∈ t } ⧸ subgroupOf s t),
    (fun a =>
          (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
            Quotient.map'
              (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
              (_ :
                ∀ (b c : α),
                  Setoid.r b c →
                    Setoid.r
                      ((fun g =>
                          { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                        b)
                      ((fun g =>
                          { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                        c))
              a))
        ((fun a =>
            Quotient.map' (fun b => f a.fst * ↑b)
              (_ :
                ∀ (b c : { x // x ∈ t }),
                  Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
              a.snd)
          (Quotient.mk'' a, snd)) =
      (Quotient.mk'' a, snd)
[PROOFSTEP]
refine' Quotient.ind' fun b => _
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α
b : { x // x ∈ t }
⊢ (fun a =>
        (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
          Quotient.map'
            (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
            (_ :
              ∀ (b c : α),
                Setoid.r b c →
                  Setoid.r
                    ((fun g =>
                        { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                      b)
                    ((fun g =>
                        { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                      c))
            a))
      ((fun a =>
          Quotient.map' (fun b => f a.fst * ↑b)
            (_ :
              ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
            a.snd)
        (Quotient.mk'' a, Quotient.mk'' b)) =
    (Quotient.mk'' a, Quotient.mk'' b)
[PROOFSTEP]
have key : Quotient.mk'' (f (Quotient.mk'' a) * b) = Quotient.mk'' a :=
  (QuotientGroup.mk_mul_of_mem (f a) b.2).trans (hf a)
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h_le : s ≤ t
f : α ⧸ t → α
hf : Function.RightInverse f QuotientGroup.mk
a : α
b : { x // x ∈ t }
key : Quotient.mk'' (f (Quotient.mk'' a) * ↑b) = Quotient.mk'' a
⊢ (fun a =>
        (Quotient.map' id (_ : ∀ (b c : α), Setoid.r b c → Setoid.r (id b) (id c)) a,
          Quotient.map'
            (fun g => { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
            (_ :
              ∀ (b c : α),
                Setoid.r b c →
                  Setoid.r
                    ((fun g =>
                        { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                      b)
                    ((fun g =>
                        { val := (f (Quotient.mk'' g))⁻¹ * g, property := (_ : (f (Quotient.mk'' g))⁻¹ * g ∈ t) })
                      c))
            a))
      ((fun a =>
          Quotient.map' (fun b => f a.fst * ↑b)
            (_ :
              ∀ (b c : { x // x ∈ t }), Setoid.r b c → Setoid.r ((fun b => f a.fst * ↑b) b) ((fun b => f a.fst * ↑b) c))
            a.snd)
        (Quotient.mk'' a, Quotient.mk'' b)) =
    (Quotient.mk'' a, Quotient.mk'' b)
[PROOFSTEP]
simp_rw [Quotient.map'_mk'', id.def, key, inv_mul_cancel_left]
[GOAL]
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : { x // x ∈ s }
⊢ Setoid.r a b → Setoid.r (↑(inclusion h) a) (↑(inclusion h) b)
[PROOFSTEP]
simp_rw [leftRel_eq]
[GOAL]
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : { x // x ∈ s }
⊢ a⁻¹ * b ∈ subgroupOf H s → (↑(inclusion h) a)⁻¹ * ↑(inclusion h) b ∈ subgroupOf H t
[PROOFSTEP]
exact id
[GOAL]
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
⊢ ∀ (a₁ a₂ : { x // x ∈ s }),
    Quotient.map' ↑(inclusion h)
          (_ : ∀ (a b : { x // x ∈ s }), Setoid.r a b → Setoid.r (↑(inclusion h) a) (↑(inclusion h) b))
          (Quotient.mk'' a₁) =
        Quotient.map' ↑(inclusion h)
          (_ : ∀ (a b : { x // x ∈ s }), Setoid.r a b → Setoid.r (↑(inclusion h) a) (↑(inclusion h) b))
          (Quotient.mk'' a₂) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂
[PROOFSTEP]
intro a b h
[GOAL]
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h✝ : s ≤ t
a b : { x // x ∈ s }
h :
  Quotient.map' ↑(inclusion h✝)
      (_ : ∀ (a b : { x // x ∈ s }), Setoid.r a b → Setoid.r (↑(inclusion h✝) a) (↑(inclusion h✝) b))
      (Quotient.mk'' a) =
    Quotient.map' ↑(inclusion h✝)
      (_ : ∀ (a b : { x // x ∈ s }), Setoid.r a b → Setoid.r (↑(inclusion h✝) a) (↑(inclusion h✝) b)) (Quotient.mk'' b)
⊢ Quotient.mk'' a = Quotient.mk'' b
[PROOFSTEP]
simpa only [Quotient.map'_mk'', eq'] using h
[GOAL]
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : { x // x ∈ H }
⊢ Setoid.r a b → Setoid.r (id a) (id b)
[PROOFSTEP]
simp_rw [leftRel_eq]
[GOAL]
α : Type u_1
inst✝ : Group α
s t H : Subgroup α
h : s ≤ t
a b : { x // x ∈ H }
⊢ a⁻¹ * b ∈ subgroupOf s H → (id a)⁻¹ * id b ∈ subgroupOf t H
[PROOFSTEP]
apply h
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h : s ≤ t
a b : α
⊢ Setoid.r a b → Setoid.r (id a) (id b)
[PROOFSTEP]
simp_rw [leftRel_eq]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
h : s ≤ t
a b : α
⊢ a⁻¹ * b ∈ s → (id a)⁻¹ * id b ∈ t
[PROOFSTEP]
apply h
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
H : Subgroup α
⊢ ∀ (a₁ a₂ : { x // x ∈ H }),
    (fun q i => quotientSubgroupOfMapOfLE H (_ : iInf f ≤ f i) q) (Quotient.mk'' a₁) =
        (fun q i => quotientSubgroupOfMapOfLE H (_ : iInf f ≤ f i) q) (Quotient.mk'' a₂) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂
[PROOFSTEP]
simp_rw [funext_iff, quotientSubgroupOfMapOfLE_apply_mk, eq', mem_subgroupOf, mem_iInf, imp_self, forall_const]
[GOAL]
α : Type u_1
inst✝ : Group α
s t : Subgroup α
ι : Type u_2
f : ι → Subgroup α
⊢ ∀ (a₁ a₂ : α),
    (fun q i => quotientMapOfLE (_ : iInf f ≤ f i) q) (Quotient.mk'' a₁) =
        (fun q i => quotientMapOfLE (_ : iInf f ≤ f i) q) (Quotient.mk'' a₂) →
      Quotient.mk'' a₁ = Quotient.mk'' a₂
[PROOFSTEP]
simp_rw [funext_iff, quotientMapOfLE_apply_mk, eq', mem_iInf, imp_self, forall_const]
[GOAL]
α : Type u_1
inst✝³ : Group α
s✝ t : Subgroup α
inst✝² : Fintype α
s : Subgroup α
inst✝¹ : Fintype { x // x ∈ s }
inst✝ : DecidablePred fun a => a ∈ s
⊢ Fintype.card α = Fintype.card (α ⧸ s) * Fintype.card { x // x ∈ s }
[PROOFSTEP]
rw [← Fintype.card_prod]
[GOAL]
α : Type u_1
inst✝³ : Group α
s✝ t : Subgroup α
inst✝² : Fintype α
s : Subgroup α
inst✝¹ : Fintype { x // x ∈ s }
inst✝ : DecidablePred fun a => a ∈ s
⊢ Fintype.card α = Fintype.card ((α ⧸ s) × { x // x ∈ s })
[PROOFSTEP]
exact Fintype.card_congr Subgroup.groupEquivQuotientProdSubgroup
[GOAL]
α : Type u_1
inst✝² : Group α
s✝ t : Subgroup α
inst✝¹ : Fintype α
s : Subgroup α
inst✝ : Fintype { x // x ∈ s }
⊢ Fintype.card { x // x ∈ s } ∣ Fintype.card α
[PROOFSTEP]
classical simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]
[GOAL]
α : Type u_1
inst✝² : Group α
s✝ t : Subgroup α
inst✝¹ : Fintype α
s : Subgroup α
inst✝ : Fintype { x // x ∈ s }
⊢ Fintype.card { x // x ∈ s } ∣ Fintype.card α
[PROOFSTEP]
simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]
[GOAL]
α : Type u_1
inst✝² : Group α
s✝ t : Subgroup α
inst✝¹ : Fintype α
s : Subgroup α
inst✝ : DecidablePred fun x => x ∈ s
⊢ Fintype.card (α ⧸ s) ∣ Fintype.card α
[PROOFSTEP]
simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_right ℕ]
[GOAL]
α : Type u_1
inst✝³ : Group α
s t : Subgroup α
H : Type u_2
inst✝² : Group H
inst✝¹ : Fintype α
inst✝ : Fintype H
f : α →* H
hf : Injective ↑f
⊢ card α ∣ card H
[PROOFSTEP]
classical calc
  card α = card (f.range : Subgroup H) := card_congr (Equiv.ofInjective f hf)
  _ ∣ card H := card_subgroup_dvd_card _
[GOAL]
α : Type u_1
inst✝³ : Group α
s t : Subgroup α
H : Type u_2
inst✝² : Group H
inst✝¹ : Fintype α
inst✝ : Fintype H
f : α →* H
hf : Injective ↑f
⊢ card α ∣ card H
[PROOFSTEP]
calc
  card α = card (f.range : Subgroup H) := card_congr (Equiv.ofInjective f hf)
  _ ∣ card H := card_subgroup_dvd_card _
[GOAL]
α : Type u_1
inst✝³ : Group α
s t : Subgroup α
H : Type u_2
inst✝² : Group H
K : Subgroup H
inst✝¹ : Fintype { x // x ∈ K }
f : α →* H
inst✝ : Fintype { x // x ∈ comap f K }
hf : Injective ↑f
⊢ card { x // x ∈ comap f K } ∣ card { x // x ∈ K }
[PROOFSTEP]
haveI : Fintype ((K.comap f).map f) := Fintype.ofEquiv _ (equivMapOfInjective _ _ hf).toEquiv
[GOAL]
α : Type u_1
inst✝³ : Group α
s t : Subgroup α
H : Type u_2
inst✝² : Group H
K : Subgroup H
inst✝¹ : Fintype { x // x ∈ K }
f : α →* H
inst✝ : Fintype { x // x ∈ comap f K }
hf : Injective ↑f
this : Fintype { x // x ∈ map f (comap f K) }
⊢ card { x // x ∈ comap f K } ∣ card { x // x ∈ K }
[PROOFSTEP]
calc
  Fintype.card (K.comap f) = Fintype.card ((K.comap f).map f) := Fintype.card_congr (equivMapOfInjective _ _ hf).toEquiv
  _ ∣ Fintype.card K := card_dvd_of_le (map_comap_le _ _)
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : { x // x ∈ s } × ↑t
⊢ ↑(Quotient.out' ↑a.snd * ↑a.fst) ∈ t
[PROOFSTEP]
rw [mk_mul_of_mem _ a.1.2, out_eq']
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
a : { x // x ∈ s } × ↑t
⊢ ↑a.snd ∈ t
[PROOFSTEP]
exact a.2.2
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
x✝ : ↑(mk ⁻¹' t)
a : α
ha : a ∈ mk ⁻¹' t
⊢ Quotient.out'
        ↑((fun a =>
                ({ val := (Quotient.out' ↑↑a)⁻¹ * ↑a, property := (_ : (Quotient.out' ↑↑a)⁻¹ * ↑a ∈ s) },
                  { val := ↑↑a, property := (_ : ↑a ∈ mk ⁻¹' t) }))
              { val := a, property := ha }).snd *
      ↑((fun a =>
              ({ val := (Quotient.out' ↑↑a)⁻¹ * ↑a, property := (_ : (Quotient.out' ↑↑a)⁻¹ * ↑a ∈ s) },
                { val := ↑↑a, property := (_ : ↑a ∈ mk ⁻¹' t) }))
            { val := a, property := ha }).fst =
    a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
x✝ : { x // x ∈ s } × ↑t
a : α
ha : a ∈ s
x : α ⧸ s
hx : x ∈ t
⊢ (fun a =>
        ({ val := (Quotient.out' ↑↑a)⁻¹ * ↑a, property := (_ : (Quotient.out' ↑↑a)⁻¹ * ↑a ∈ s) },
          { val := ↑↑a, property := (_ : ↑a ∈ mk ⁻¹' t) }))
      ((fun a => { val := Quotient.out' ↑a.snd * ↑a.fst, property := (_ : ↑(Quotient.out' ↑a.snd * ↑a.fst) ∈ t) })
        ({ val := a, property := ha }, { val := x, property := hx })) =
    ({ val := a, property := ha }, { val := x, property := hx })
[PROOFSTEP]
ext
[GOAL]
case h₁.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
x✝ : { x // x ∈ s } × ↑t
a : α
ha : a ∈ s
x : α ⧸ s
hx : x ∈ t
⊢ ↑((fun a =>
            ({ val := (Quotient.out' ↑↑a)⁻¹ * ↑a, property := (_ : (Quotient.out' ↑↑a)⁻¹ * ↑a ∈ s) },
              { val := ↑↑a, property := (_ : ↑a ∈ mk ⁻¹' t) }))
          ((fun a => { val := Quotient.out' ↑a.snd * ↑a.fst, property := (_ : ↑(Quotient.out' ↑a.snd * ↑a.fst) ∈ t) })
            ({ val := a, property := ha }, { val := x, property := hx }))).fst =
    ↑({ val := a, property := ha }, { val := x, property := hx }).fst
[PROOFSTEP]
simp [ha]
[GOAL]
case h₂.a
α : Type u_1
inst✝ : Group α
s : Subgroup α
t : Set (α ⧸ s)
x✝ : { x // x ∈ s } × ↑t
a : α
ha : a ∈ s
x : α ⧸ s
hx : x ∈ t
⊢ ↑((fun a =>
            ({ val := (Quotient.out' ↑↑a)⁻¹ * ↑a, property := (_ : (Quotient.out' ↑↑a)⁻¹ * ↑a ∈ s) },
              { val := ↑↑a, property := (_ : ↑a ∈ mk ⁻¹' t) }))
          ((fun a => { val := Quotient.out' ↑a.snd * ↑a.fst, property := (_ : ↑(Quotient.out' ↑a.snd * ↑a.fst) ∈ t) })
            ({ val := a, property := ha }, { val := x, property := hx }))).snd =
    ↑({ val := a, property := ha }, { val := x, property := hx }).snd
[PROOFSTEP]
simp [ha]
