rw [← hax.2]
case inr.a.mp.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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
⊢ x • image QuotientGroup.mk t = image QuotientGroup.mk t
case inr.a.mp.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
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
⊢ ↑a • image QuotientGroup.mk t = image QuotientGroup.mk t