internlm/Lean-Github huggingface dataset:
Theorem: Finset.card_mulStab_dvd_card_mulStab
Proof state before:
case h.e'_3
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ s.mulStab.card = (map { toFun := Subtype.map id ⋯, inj' := ⋯ } s.mulStab.attach).card

case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Nat.card ↥(stabilizer α t)
Tactic:
simp
Proof state after:
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Nat.card ↥(stabilizer α t)
Theorem: Finset.card_mulStab_dvd_card_mulStab
Proof state before:
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Nat.card ↥(stabilizer α t)
Tactic:
simp [-mem_stabilizer_iff]
Proof state after:
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Fintype.card ↥(stabilizer α t)
Theorem: Finset.card_mulStab_dvd_card_mulStab
Proof state before:
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = Fintype.card ↥(stabilizer α t)
Tactic:
change _ = (t.mulStab.attach.map
  ⟨Subtype.map id fun _ ↦ (mem_mulStab ht).1, Subtype.map_injective _ injective_id⟩).card
Proof state after:
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = (map { toFun := Subtype.map id ⋯, inj' := ⋯ } t.mulStab.attach).card
Theorem: Finset.card_mulStab_dvd_card_mulStab
Proof state before:
case h.e'_4
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : stabilizer α s ≤ stabilizer α t
ht : t.Nonempty
this✝ : Fintype ↥(stabilizer α s) := Finset.fintypeStabilizerOfMulStab hs
this : Fintype ↥(stabilizer α t) := Finset.fintypeStabilizerOfMulStab ht
⊢ t.mulStab.card = (map { toFun := Subtype.map id ⋯, inj' := ⋯ } t.mulStab.attach).card
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.card_mulStab_dvd_card_mulStab
Proof state before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s : Finset α
a : α
hs : s.Nonempty
h : s.mulStab ⊆ ∅.mulStab
⊢ s.mulStab.card ∣ ∅.mulStab.card
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.card_mulStab_mul_card_image_coe'
Proof 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
Proof 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
Theorem: Finset.card_mulStab_mul_card_image_coe'
Proof 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)
Proof 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
Theorem: Finset.card_mulStab_mul_card_image_coe'
Proof 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]
Proof 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
Theorem: Finset.card_mulStab_mul_card_image_coe'
Proof 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 _))
Proof 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
Theorem: Finset.card_mulStab_mul_card_image_coe'
Proof 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
Proof 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
Theorem: Finset.card_mulStab_mul_card_image_coe'
Proof 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
Proof state after:
no goals
Theorem: Finset.card_mulStab_mul_card_image_coe'
Proof 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
Proof state after:
no goals
Theorem: Finset.card_mulStab_mul_card_image_coe'
Proof 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]
Proof state after:
no goals
Theorem: Finset.card_mul_card_eq_mulStab_card_mul_coe
Proof 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
Proof 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
Theorem: Finset.card_mul_card_eq_mulStab_card_mul_coe
Proof 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
Proof 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
Theorem: Finset.card_mul_card_eq_mulStab_card_mul_coe
Proof 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)
Proof 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
Theorem: Finset.card_mul_card_eq_mulStab_card_mul_coe
Proof 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]
Proof 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
Theorem: Finset.card_mul_card_eq_mulStab_card_mul_coe
Proof 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 _)
Proof 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
Theorem: Finset.card_mul_card_eq_mulStab_card_mul_coe
Proof 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
Proof 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
Theorem: Finset.card_mul_card_eq_mulStab_card_mul_coe
Proof 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
Proof state after:
no goals
Theorem: Finset.card_mul_card_eq_mulStab_card_mul_coe
Proof 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
Proof state after:
no goals
Theorem: Finset.card_mul_card_eq_mulStab_card_mul_coe
Proof 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
Proof state after:
no goals
Theorem: Finset.card_mul_card_eq_mulStab_card_mul_coe
Proof 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]
Proof state after:
no goals
Theorem: Finset.card_mulStab_mul_card_image_coe
Proof 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
Proof 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
Theorem: Finset.card_mulStab_mul_card_image_coe
Proof 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
Proof 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
Theorem: Finset.card_mulStab_mul_card_image_coe
Proof 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)))
Proof 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
Theorem: Finset.card_mulStab_mul_card_image_coe
Proof 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))
Proof 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
Theorem: Finset.card_mulStab_mul_card_image_coe
Proof 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
Proof 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
Theorem: Finset.card_mulStab_mul_card_image_coe
Proof 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]
Proof 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