Theorem: Finset.card_mulStab_mul_card_image_coe' (LeanCamCombi/Kneser/MulStab.lean)

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

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

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

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

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

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

State before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s t : Finset α
ht : t.Nonempty
this : ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑s)) ≃ ↥(stabilizer α t) × ↑(QuotientGroup.mk '' ↑s)
that : ↥(stabilizer α t) = { x // x ∈ t.mulStab }
temp : ↑(↑s * ↑t.mulStab) ≃ { x // x ∈ t.mulStab } × ↑(QuotientGroup.mk '' ↑s)
⊢ t.mulStab.card * (image QuotientGroup.mk s).card = (s * t.mulStab).card
Tactic:
simpa only [coe_sort_coe, ← coe_mul, Fintype.card_prod, Fintype.card_coe, Fintype.card_ofFinset,
  toFinset_coe, mem_image, Set.mem_image, mem_coe, forall_const, eq_comm]
  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 : α
s : Finset α
⊢ ∅.mulStab.card * (image QuotientGroup.mk s).card = (s * ∅.mulStab).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 α
ht : t.Nonempty
this : ↑(QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑s)) ≃ ↥(stabilizer α t) × ↑(QuotientGroup.mk '' ↑s)
⊢ ↥(stabilizer α t) = { x // x ∈ t.mulStab }
Tactic:
rw [← SetLike.coe_sort_coe, ← coe_mulStab ht, Finset.coe_sort_coe]
State after:
no goals