rw [inv_mul_eq_iff_eq_mul] at hcbyz
case inr.a.mpr.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
b : α
hbt : b ∈ t
ha : y • b ∈ y • t
hayz : (y * b)⁻¹ * z ∈ s
c : α
hct : c ∈ t.mulStab
hcbyz : (y • b)⁻¹ * z = c
⊢ z ∈ y • t
case inr.a.mpr.intro.intro.intro.intro.intro.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
y : α
hyx : ⟦y⟧ = x
z : α
hzt : z ∈ t
hx : image QuotientGroup.mk (y • t) = image QuotientGroup.mk t
b : α
hbt : b ∈ t
ha : y • b ∈ y • t
hayz : (y * b)⁻¹ * z ∈ s
c : α
hct : c ∈ t.mulStab
hcbyz : z = y • b * c
⊢ z ∈ y • t