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

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
⊢ (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card
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 : α
t : Finset α
⊢ (∅ * t).card = (∅ * t).mulStab.card * (image QuotientGroup.mk (∅ * t)).card

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
⊢ (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card

State before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
⊢ (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card
Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty
State after:
case inr.inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ (s * ∅).card = (s * ∅).mulStab.card * (image QuotientGroup.mk (s * ∅)).card

case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card

State before:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
⊢ (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card
Tactic:
have := QuotientGroup.preimageMkEquivSubgroupProdSet _ $ ↑(s * t) +ˢ stabilizer α (s * t)
State after:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑(s * t))) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑(s * t))
⊢ (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card

State before:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑(s * t))) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑(s * t))
⊢ (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card
Tactic:
have that : ↥(stabilizer α (s * t)) = ↥(s * t).mulStab := by
  rw [← SetLike.coe_sort_coe, ← coe_mulStab (hs.mul ht), Finset.coe_sort_coe]
State after:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑(s * t))) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑(s * t))
that : ↥(stabilizer α (s * t)) = { x // x ∈ (s * t).mulStab }
⊢ (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card

State before:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑(s * t))) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑(s * t))
that : ↥(stabilizer α (s * t)) = { x // x ∈ (s * t).mulStab }
⊢ (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card
Tactic:
have temp := this.trans $ (Equiv.cast that).prodCongr (Equiv.refl _)
State after:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑(s * t))) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑(s * t))
that : ↥(stabilizer α (s * t)) = { x // x ∈ (s * t).mulStab }
temp :
  ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑(s * t))) ≃
    { x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑(s * t))
⊢ (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card

State before:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑(s * t))) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑(s * t))
that : ↥(stabilizer α (s * t)) = { x // x ∈ (s * t).mulStab }
temp :
  ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑(s * t))) ≃
    { x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑(s * t))
⊢ (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card
Tactic:
rw [preimage_image_quotientMk_mulStabilizer] at temp
State after:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑(s * t))) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑(s * t))
that : ↥(stabilizer α (s * t)) = { x // x ∈ (s * t).mulStab }
temp : ↑↑(s * t) ≃ { x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑(s * t))
⊢ (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card

State before:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑(s * t))) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑(s * t))
that : ↥(stabilizer α (s * t)) = { x // x ∈ (s * t).mulStab }
temp : ↑↑(s * t) ≃ { x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑(s * t))
⊢ (s * t).card = (s * t).mulStab.card * (image QuotientGroup.mk (s * t)).card
Tactic:
simpa [-coe_mul] using Fintype.card_congr temp
State after:
no goals

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

State before:
case inr.inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ (s * ∅).card = (s * ∅).mulStab.card * (image QuotientGroup.mk (s * ∅)).card
Tactic:
simp
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
hs : s.Nonempty
ht : t.Nonempty
this :
  ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑(s * t))) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑(s * t))
⊢ ↥(stabilizer α (s * t)) = { x // x ∈ (s * t).mulStab }
Tactic:
rw [← SetLike.coe_sort_coe, ← coe_mulStab (hs.mul ht), Finset.coe_sort_coe]
State after:
no goals