internlm/Lean-Github huggingface dataset:
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
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)
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))
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
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
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
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))
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
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
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
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))
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
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
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
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))
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
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
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
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))
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
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
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
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))
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
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
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
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 : α
t : Finset α
⊢ (∅ * t).mulStab.card * (image QuotientGroup.mk ∅ * image QuotientGroup.mk t).card = (∅ * t).card
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.card_mulStab_mul_card_image_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 * ∅).mulStab.card * (image QuotientGroup.mk s * image QuotientGroup.mk ∅).card = (s * ∅).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 α
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]
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 α
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
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 α
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
Proof state after:
no goals
Theorem: Finset.subgroup_mul_card_eq_mul_of_mul_stab_subset
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
h : ↑t * ↑s = ↑t
⊢ Nat.card ↥s * (image QuotientGroup.mk t).card = t.card
Tactic:
have := s.subgroup_mul_card_eq_mul t
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
h : ↑t * ↑s = ↑t
this : Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' ↑t) = Nat.card ↑(↑t * ↑s)
⊢ Nat.card ↥s * (image QuotientGroup.mk t).card = t.card
Theorem: Finset.subgroup_mul_card_eq_mul_of_mul_stab_subset
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
h : ↑t * ↑s = ↑t
this : Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' ↑t) = Nat.card ↑(↑t * ↑s)
⊢ Nat.card ↥s * (image QuotientGroup.mk t).card = t.card
Tactic:
rw [h] at this
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
h : ↑t * ↑s = ↑t
this : Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' ↑t) = Nat.card ↑↑t
⊢ Nat.card ↥s * (image QuotientGroup.mk t).card = t.card
Theorem: Finset.subgroup_mul_card_eq_mul_of_mul_stab_subset
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
h : ↑t * ↑s = ↑t
this : Nat.card ↥s * Nat.card ↑(QuotientGroup.mk '' ↑t) = Nat.card ↑↑t
⊢ Nat.card ↥s * (image QuotientGroup.mk t).card = t.card
Tactic:
simpa
Proof state after:
no goals
Theorem: Finset.subgroup_mul_card_eq_mul_of_mul_stab_subset
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
⊢ ↑t * ↑s = ↑t
Tactic:
apply Set.Subset.antisymm (Set.Subset.trans (Set.mul_subset_mul_left hst) _)
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
⊢ ↑t ⊆ ↑t * ↑s

ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
⊢ ↑t * ↑t.mulStab ⊆ ↑t
Theorem: Finset.subgroup_mul_card_eq_mul_of_mul_stab_subset
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
⊢ ↑t ⊆ ↑t * ↑s
Tactic:
intro x
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
x : α
⊢ x ∈ ↑t → x ∈ ↑t * ↑s
Theorem: Finset.subgroup_mul_card_eq_mul_of_mul_stab_subset
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
x : α
⊢ x ∈ ↑t → x ∈ ↑t * ↑s
Tactic:
rw [Set.mem_mul]
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
x : α
⊢ x ∈ ↑t → ∃ x_1 ∈ ↑t, ∃ y ∈ ↑s, x_1 * y = x
Theorem: Finset.subgroup_mul_card_eq_mul_of_mul_stab_subset
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
x : α
⊢ x ∈ ↑t → ∃ x_1 ∈ ↑t, ∃ y ∈ ↑s, x_1 * y = x
Tactic:
aesop
Proof state after:
no goals
Theorem: Finset.subgroup_mul_card_eq_mul_of_mul_stab_subset
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
⊢ ↑t * ↑t.mulStab ⊆ ↑t
Tactic:
rw [← coe_mul, mul_mulStab]
Proof state after:
no goals
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
⊢ image QuotientGroup.mk t.mulStab = (image QuotientGroup.mk t).mulStab
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 : Subgroup α
hst : ↑s ⊆ ↑∅.mulStab
⊢ image QuotientGroup.mk ∅.mulStab = (image QuotientGroup.mk ∅).mulStab

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
⊢ image QuotientGroup.mk t.mulStab = (image QuotientGroup.mk t).mulStab
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
⊢ image QuotientGroup.mk t.mulStab = (image QuotientGroup.mk t).mulStab
Tactic:
have hti : (image (QuotientGroup.mk (s := s)) t).Nonempty := by aesop
Proof state after:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
⊢ image QuotientGroup.mk t.mulStab = (image QuotientGroup.mk t).mulStab
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
⊢ image QuotientGroup.mk t.mulStab = (image QuotientGroup.mk t).mulStab
Tactic:
ext x
Proof state after:
case inr.a
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
⊢ x ∈ image QuotientGroup.mk t.mulStab ↔ x ∈ (image QuotientGroup.mk t).mulStab
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
case inr.a
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
⊢ x ∈ image QuotientGroup.mk t.mulStab ↔ x ∈ (image QuotientGroup.mk t).mulStab
Tactic:
simp only [mem_image, image_nonempty, mem_mulStab hti]
Proof state after:
case inr.a
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
⊢ (∃ a ∈ t.mulStab, ↑a = x) ↔ x • image QuotientGroup.mk t = image QuotientGroup.mk t
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
case inr.a
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
⊢ (∃ a ∈ t.mulStab, ↑a = x) ↔ x • image QuotientGroup.mk t = image QuotientGroup.mk t
Tactic:
constructor
Proof state after:
case inr.a.mp
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
⊢ (∃ a ∈ t.mulStab, ↑a = x) → x • image QuotientGroup.mk t = image QuotientGroup.mk t

case inr.a.mpr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
⊢ x • image QuotientGroup.mk t = image QuotientGroup.mk t → ∃ a ∈ t.mulStab, ↑a = x
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Subgroup α
hst : ↑s ⊆ ↑∅.mulStab
⊢ image QuotientGroup.mk ∅.mulStab = (image QuotientGroup.mk ∅).mulStab
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
⊢ (image QuotientGroup.mk t).Nonempty
Tactic:
aesop
Proof state after:
no goals
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
case inr.a.mp
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
⊢ (∃ a ∈ t.mulStab, ↑a = x) → x • image QuotientGroup.mk t = image QuotientGroup.mk t
Tactic:
rintro ⟨a, hax⟩
Proof state after:
case inr.a.mp.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a✝ : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
⊢ x • image QuotientGroup.mk t = image QuotientGroup.mk t
Theorem: Finset.mulStab_quotient_commute_subgroup
Proof state before:
case inr.a.mp.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a✝ : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
⊢ x • image QuotientGroup.mk t = image QuotientGroup.mk t
Tactic:
rw [← hax.2]
Proof state after:
case inr.a.mp.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t✝ : Finset α
a✝ : α
s : Subgroup α
t : Finset α
hst : ↑s ⊆ ↑t.mulStab
ht : t.Nonempty
hti : (image QuotientGroup.mk t).Nonempty
x : α ⧸ s
a : α
hax : a ∈ t.mulStab ∧ ↑a = x
⊢ ↑a • image QuotientGroup.mk t = image QuotientGroup.mk t