Theorem: Finset.preimage_image_quotientMk_mulStabilizer (LeanCamCombi/Kneser/MulStab.lean)

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑s) = ↑s
Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
State after:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑∅) = ↑∅

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑s) = ↑s

State before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑∅) = ↑∅
Tactic:
simp
State after:
no goals

State before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑s) = ↑s
Tactic:
rw [preimage_image_quotientMk_stabilizer_eq_mul_mulStab hs s, ← coe_mul, mul_mulStab]
State after:
no goals