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 α
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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).mulStab.card * (image QuotientGroup.mk ∅ * image QuotientGroup.mk t).card = (∅ * 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).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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 * ∅).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk ∅).card = (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).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card
Tactic:
have := QuotientGroup.preimageMkEquivSubgroupProdSet (stabilizer α (s * t))
  ((s +ˢ stabilizer α (s * t)) * (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 * QuotientGroup.mk '' ↑t)) ≃
    ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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 * QuotientGroup.mk '' ↑t)) ≃
    ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card
Tactic:
have image_coe_mul :
  ((s * t) +ˢ stabilizer α (s * t)) = (s +ˢ stabilizer α (s * t)) * (t +ˢ stabilizer α (s * t)) :=
  Set.image_mul (QuotientGroup.mk' (stabilizer α (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 * QuotientGroup.mk '' ↑t)) ≃
    ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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 * QuotientGroup.mk '' ↑t)) ≃
    ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card
Tactic:
rw [← image_coe_mul, ← coe_mul, preimage_image_quotientMk_mulStabilizer, coe_mul, image_coe_mul]
  at this
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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card
Tactic:
have that :
  (stabilizer α (s * t) × ↥((s +ˢ stabilizer α (s * t)) * (t +ˢ stabilizer α (s * t)))) =
    ((s * t).mulStab × ↥((s +ˢ stabilizer α (s * t)) * (t +ˢ stabilizer α (s * t)))) := 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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card
Tactic:
have temp := this.trans (Equiv.cast that)
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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp : ↑(↑s * ↑t) ≃ { x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp : ↑(↑s * ↑t) ≃ { x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card
Tactic:
replace temp := Fintype.card_congr 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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp :
  Fintype.card ↑(↑s * ↑t) =
    Fintype.card ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp :
  Fintype.card ↑(↑s * ↑t) =
    Fintype.card ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card
Tactic:
simp_rw [← Finset.coe_mul s t] 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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp :
  Fintype.card ↑↑(s * t) =
    Fintype.card ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp :
  Fintype.card ↑↑(s * t) =
    Fintype.card ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card
Tactic:
simp only [Fintype.card_prod, Fintype.card_coe] 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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp : Fintype.card ↑↑(s * t) = (s * t).mulStab.card * Fintype.card ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp : Fintype.card ↑↑(s * t) = (s * t).mulStab.card * Fintype.card ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card
Tactic:
have h1 : Fintype.card ((s * t : Finset α) : Set α) = Fintype.card (s * t) := by congr
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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp : Fintype.card ↑↑(s * t) = (s * t).mulStab.card * Fintype.card ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
h1 : Fintype.card ↑↑(s * t) = Fintype.card { x // x ∈ s * t }
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp : Fintype.card ↑↑(s * t) = (s * t).mulStab.card * Fintype.card ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
h1 : Fintype.card ↑↑(s * t) = Fintype.card { x // x ∈ s * t }
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card
Tactic:
have h2 : (s +ˢ stabilizer α (s * t)) * (t +ˢ stabilizer α (s * t)) =
  ↑((s +ₛ stabilizer α (s * t)) * (t +ₛ stabilizer α (s * t))) := by simp
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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp : Fintype.card ↑↑(s * t) = (s * t).mulStab.card * Fintype.card ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
h1 : Fintype.card ↑↑(s * t) = Fintype.card { x // x ∈ s * t }
h2 : QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t = ↑(image QuotientGroup.mk s * image QuotientGroup.mk t)
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp : Fintype.card ↑↑(s * t) = (s * t).mulStab.card * Fintype.card ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
h1 : Fintype.card ↑↑(s * t) = Fintype.card { x // x ∈ s * t }
h2 : QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t = ↑(image QuotientGroup.mk s * image QuotientGroup.mk t)
⊢ (s * t).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk t).card = (s * t).card
Tactic:
sorry
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).mulStab.card * (image QuotientGroup.mk ∅ * image QuotientGroup.mk t).card = (∅ * 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 * ∅).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk ∅).card = (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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
⊢ (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
Tactic:
rw [← SetLike.coe_sort_coe, ← coe_mulStab (hs.mul ht), Finset.coe_sort_coe]
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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp : Fintype.card ↑↑(s * t) = (s * t).mulStab.card * Fintype.card ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
⊢ Fintype.card ↑↑(s * t) = Fintype.card { x // x ∈ s * t }
Tactic:
congr
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 : ↑(↑s * ↑t) ≃ ↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
image_coe_mul : QuotientGroup.mk '' (↑s * ↑t) = QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t
that :
  (↥(stabilizer α (s * t)) × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)) =
    ({ x // x ∈ (s * t).mulStab } × ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t))
temp : Fintype.card ↑↑(s * t) = (s * t).mulStab.card * Fintype.card ↑(QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t)
h1 : Fintype.card ↑↑(s * t) = Fintype.card { x // x ∈ s * t }
⊢ QuotientGroup.mk '' ↑s * QuotientGroup.mk '' ↑t = ↑(image QuotientGroup.mk s * image QuotientGroup.mk t)
Tactic:
simp
State after:
no goals