α : 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⁻¹ ∈ s
rw [Set.ext_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⁻¹ ∈ s
simp_rw [mem_rightCoset_iff, SetLike.mem_coe]
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s

case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ y * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s
constructor
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
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s
intro h
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
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
apply (h y).mpr
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ 1 ∈ s
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
rw [mul_right_inv]
no goals
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ 1 ∈ s
exact s.one_mem
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * x⁻¹ ∈ s ↔ z * y⁻¹ ∈ s
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ y * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
intro h z
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * x⁻¹ ∈ s ↔ z * y⁻¹ ∈ s
rw [← inv_mul_cancel_left y x⁻¹]
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s
rw [← mul_assoc]
no goals
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s
exact s.mul_mem_cancel_right h