internlm/Lean-Github huggingface dataset:
Theorem: Finset.inter_mulStab_subset_mulStab_union
Proof state before:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
ht : t.Nonempty
⊢ s.mulStab ∩ t.mulStab ⊆ (s ∪ t).mulStab
Tactic:
intro x hx
Proof state after:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
ht : t.Nonempty
x : α
hx : x ∈ s.mulStab ∩ t.mulStab
⊢ x ∈ (s ∪ t).mulStab
Theorem: Finset.inter_mulStab_subset_mulStab_union
Proof state before:
case inr.inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
ht : t.Nonempty
x : α
hx : x ∈ s.mulStab ∩ t.mulStab
⊢ x ∈ (s ∪ t).mulStab
Tactic:
rw [mem_mulStab (hs.mono subset_union_left), smul_finset_union,
  (mem_mulStab hs).mp (mem_of_mem_inter_left hx),
  (mem_mulStab ht).mp (mem_of_mem_inter_right hx)]
Proof state after:
no goals
Theorem: Finset.inter_mulStab_subset_mulStab_union
Proof state before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
t : Finset α
a : α
⊢ ∅.mulStab ∩ t.mulStab ⊆ (∅ ∪ t).mulStab
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.inter_mulStab_subset_mulStab_union
Proof state before:
case inr.inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
a : α
hs : s.Nonempty
⊢ s.mulStab ∩ ∅.mulStab ⊆ (s ∪ ∅).mulStab
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mulStab_subset_div_left
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
⊢ s.mulStab ⊆ {a} / s
Tactic:
refine fun b hb ↦ mem_div.2 ⟨_, mem_singleton_self _, _, ?_, div_div_cancel _ _⟩
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ s.mulStab
⊢ a / b ∈ s
Theorem: Finset.mulStab_subset_div_left
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ s.mulStab
⊢ a / b ∈ s
Tactic:
rw [mem_mulStab ⟨a, ha⟩] at hb
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b • s = s
⊢ a / b ∈ s
Theorem: Finset.mulStab_subset_div_left
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b • s = s
⊢ a / b ∈ s
Tactic:
rwa [← hb, ← inv_smul_mem_iff, smul_eq_mul, inv_mul_eq_div] at ha
Proof state after:
no goals
Theorem: Finset.subset_mulStab_mul_right
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ t.mulStab ⊆ (s * t).mulStab
Tactic:
rw [mul_comm]
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ t.mulStab ⊆ (t * s).mulStab
Theorem: Finset.subset_mulStab_mul_right
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ t.mulStab ⊆ (t * s).mulStab
Tactic:
exact subset_mulStab_mul_left hs
Proof state after:
no goals
Theorem: Finset.mul_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ s * s.mulStab = s
Tactic:
rw [mul_comm]
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ s.mulStab * s = s
Theorem: Finset.mul_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ s.mulStab * s = s
Tactic:
exact mulStab_mul _
Proof state after:
no goals
Theorem: Finset.mul_mulStab_mul_mul_mul_mulStab_mul
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s * (s * t).mulStab * (t * (s * t).mulStab) = s * t
Tactic:
rw [mul_mul_mul_comm, mulStab_mul_mulStab, mul_mulStab]
Proof state after:
no goals
Theorem: Finset.mul_subset_left_iff
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ s * t ⊆ s ↔ t ⊆ s.mulStab
Tactic:
rw [mul_comm, mul_subset_right_iff hs]
Proof state after:
no goals
Theorem: Finset.mul_subset_left
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ t ⊆ s.mulStab → s * t ⊆ s
Tactic:
rw [mul_comm]
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ t ⊆ s.mulStab → t * s ⊆ s
Theorem: Finset.mul_subset_left
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ t ⊆ s.mulStab → t * s ⊆ s
Tactic:
exact mul_subset_right
Proof state after:
no goals
Theorem: Finset.mulStab_idem
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ s.mulStab.mulStab = s.mulStab
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 : α
⊢ ∅.mulStab.mulStab = ∅.mulStab

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ s.mulStab.mulStab = s.mulStab
Theorem: Finset.mulStab_idem
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ s.mulStab.mulStab = s.mulStab
Tactic:
rw [← coe_inj, coe_mulStab hs, coe_mulStab hs.mulStab, ← stabilizer_coe_finset, coe_mulStab hs]
Proof state after:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ ↑(stabilizer α ↑(stabilizer α s)) = ↑(stabilizer α s)
Theorem: Finset.mulStab_idem
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ ↑(stabilizer α ↑(stabilizer α s)) = ↑(stabilizer α s)
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mulStab_idem
Proof state before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ∅.mulStab.mulStab = ∅.mulStab
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mulStab_smul
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ a : α
s : Finset α
⊢ (a • s).mulStab = s.mulStab
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✝ a : α
⊢ (a • ∅).mulStab = ∅.mulStab

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ a : α
s : Finset α
hs : s.Nonempty
⊢ (a • s).mulStab = s.mulStab
Theorem: Finset.mulStab_smul
Proof state before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a✝ a : α
⊢ (a • ∅).mulStab = ∅.mulStab
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mulStab_smul
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ a : α
s : Finset α
hs : s.Nonempty
⊢ (a • s).mulStab = s.mulStab
Tactic:
rw [← coe_inj, coe_mulStab hs, coe_mulStab hs.smul_finset, stabilizer_smul_eq_right]
Proof state after:
no goals
Theorem: Finset.mulStab_image_coe_quotient
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ (image QuotientGroup.mk s).mulStab = 1
Tactic:
rw [← coe_inj, coe_mulStab (hs.image _), ← stabilizer_coe_finset, ← stabilizer_coe_finset,
  coe_image, coe_one, stabilizer_image_coe_quotient, Subgroup.coe_bot, Set.singleton_one]
Proof state after:
no goals
Theorem: Finset.preimage_image_quotientMk_stabilizer_eq_mul_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
ht : t.Nonempty
s : Finset α
⊢ QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑s) = ↑s * ↑t.mulStab
Tactic:
rw [QuotientGroup.preimage_image_mk_eq_iUnion_smul, mul_comm, Set.iUnion_subtype]
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
ht : t.Nonempty
s : Finset α
⊢ ⋃ x, ⋃ (hx : x ∈ stabilizer α t), ⟨x, hx⟩ • ↑s = ↑t.mulStab * ↑s
Theorem: Finset.preimage_image_quotientMk_stabilizer_eq_mul_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
ht : t.Nonempty
s : Finset α
⊢ ⋃ x, ⋃ (hx : x ∈ stabilizer α t), ⟨x, hx⟩ • ↑s = ↑t.mulStab * ↑s
Tactic:
simp_rw [Subgroup.mk_smul, ← SetLike.mem_coe, ← coe_mulStab ht, ← coe_smul_finset, ← coe_biUnion,
  biUnion_smul_finset, smul_eq_mul, coe_mul]
Proof state after:
no goals
Theorem: Finset.preimage_image_quotientMk_mulStabilizer
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑s) = ↑s
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 : α
⊢ QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑∅) = ↑∅

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑s) = ↑s
Theorem: Finset.preimage_image_quotientMk_mulStabilizer
Proof state before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑∅) = ↑∅
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.preimage_image_quotientMk_mulStabilizer
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ QuotientGroup.mk ⁻¹' (QuotientGroup.mk '' ↑s) = ↑s
Tactic:
rw [preimage_image_quotientMk_stabilizer_eq_mul_mulStab hs s, ← coe_mul, mul_mulStab]
Proof state after:
no goals
Theorem: Finset.pairwiseDisjoint_smul_finset_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ (Set.range fun a => a • s.mulStab).PairwiseDisjoint id
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 : α
⊢ (Set.range fun a => a • ∅.mulStab).PairwiseDisjoint id

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ (Set.range fun a => a • s.mulStab).PairwiseDisjoint id
Theorem: Finset.pairwiseDisjoint_smul_finset_mulStab
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ (Set.range fun a => a • s.mulStab).PairwiseDisjoint id
Tactic:
rintro _ ⟨a, rfl⟩ _ ⟨b, rfl⟩
Proof state after:
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ (fun a => a • s.mulStab) a ≠ (fun a => a • s.mulStab) b →
    (Disjoint on id) ((fun a => a • s.mulStab) a) ((fun a => a • s.mulStab) b)
Theorem: Finset.pairwiseDisjoint_smul_finset_mulStab
Proof state before:
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ (fun a => a • s.mulStab) a ≠ (fun a => a • s.mulStab) b →
    (Disjoint on id) ((fun a => a • s.mulStab) a) ((fun a => a • s.mulStab) b)
Tactic:
simp only [onFun, id_eq]
Proof state after:
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ a • s.mulStab ≠ b • s.mulStab → Disjoint (a • s.mulStab) (b • s.mulStab)
Theorem: Finset.pairwiseDisjoint_smul_finset_mulStab
Proof state before:
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ a • s.mulStab ≠ b • s.mulStab → Disjoint (a • s.mulStab) (b • s.mulStab)
Tactic:
simp_rw [← disjoint_coe, ← coe_injective.ne_iff, coe_smul_finset, coe_mulStab hs]
Proof state after:
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ a • ↑(stabilizer α s) ≠ b • ↑(stabilizer α s) → Disjoint (a • ↑(stabilizer α s)) (b • ↑(stabilizer α s))
Theorem: Finset.pairwiseDisjoint_smul_finset_mulStab
Proof state before:
case inr.intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a✝ : α
s : Finset α
hs : s.Nonempty
a b : α
⊢ a • ↑(stabilizer α s) ≠ b • ↑(stabilizer α s) → Disjoint (a • ↑(stabilizer α s)) (b • ↑(stabilizer α s))
Tactic:
exact Subgroup.pairwiseDisjoint_smul _ (Set.mem_range_self _) (Set.mem_range_self _)
Proof state after:
no goals
Theorem: Finset.pairwiseDisjoint_smul_finset_mulStab
Proof state before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (Set.range fun a => a • ∅.mulStab).PairwiseDisjoint id
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.disjoint_smul_finset_mulStab_mul_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ¬a • s.mulStab ⊆ t * s.mulStab → Disjoint (a • s.mulStab) (t * s.mulStab)
Tactic:
simp_rw [@not_imp_comm (_ ⊆ _), ← smul_eq_mul, ← biUnion_smul_finset, disjoint_biUnion_right,
  Classical.not_forall]
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (∃ x, ∃ (_ : x ∈ t), ¬Disjoint (a • s.mulStab) (x • s.mulStab)) → a • s.mulStab ⊆ t.biUnion fun x => x • s.mulStab
Theorem: Finset.disjoint_smul_finset_mulStab_mul_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ (∃ x, ∃ (_ : x ∈ t), ¬Disjoint (a • s.mulStab) (x • s.mulStab)) → a • s.mulStab ⊆ t.biUnion fun x => x • s.mulStab
Tactic:
rintro ⟨b, hb, h⟩
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a b : α
hb : b ∈ t
h : ¬Disjoint (a • s.mulStab) (b • s.mulStab)
⊢ a • s.mulStab ⊆ t.biUnion fun x => x • s.mulStab
Theorem: Finset.disjoint_smul_finset_mulStab_mul_mulStab
Proof state before:
case intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a b : α
hb : b ∈ t
h : ¬Disjoint (a • s.mulStab) (b • s.mulStab)
⊢ a • s.mulStab ⊆ t.biUnion fun x => x • s.mulStab
Tactic:
rw [s.pairwiseDisjoint_smul_finset_mulStab.eq (Set.mem_range_self _) (Set.mem_range_self _) h]
Proof state after:
case intro.intro
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a b : α
hb : b ∈ t
h : ¬Disjoint (a • s.mulStab) (b • s.mulStab)
⊢ b • s.mulStab ⊆ t.biUnion fun x => x • s.mulStab
Theorem: Finset.card_mulStab_dvd_card
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ s.mulStab.card ∣ s.card
Tactic:
simpa only [mul_mulStab] using s.card_mulStab_dvd_card_mul_mulStab s
Proof state after:
no goals
Theorem: Finset.card_mulStab_le_card
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s.mulStab.card ≤ s.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 α
t : Finset α
a : α
⊢ ∅.mulStab.card ≤ ∅.card

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ s.mulStab.card ≤ s.card
Theorem: Finset.card_mulStab_le_card
Proof state before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
t : Finset α
a : α
⊢ ∅.mulStab.card ≤ ∅.card
Tactic:
rfl
Proof state after:
no goals
Theorem: Finset.card_mulStab_le_card
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ s.mulStab.card ≤ s.card
Tactic:
exact Nat.le_of_dvd hs.card_pos s.card_mulStab_dvd_card
Proof state after:
no goals
Theorem: Finset.card_mulStab_dvd_card_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : s.mulStab ⊆ t.mulStab
⊢ s.mulStab.card ∣ 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 : Finset α
a : α
hs : s.Nonempty
h : s.mulStab ⊆ ∅.mulStab
⊢ s.mulStab.card ∣ ∅.mulStab.card

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : s.mulStab ⊆ t.mulStab
ht : t.Nonempty
⊢ s.mulStab.card ∣ t.mulStab.card
Theorem: Finset.card_mulStab_dvd_card_mulStab
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : CommGroup α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
h : s.mulStab ⊆ t.mulStab
ht : t.Nonempty
⊢ s.mulStab.card ∣ t.mulStab.card
Tactic:
rw [← coe_subset, coe_mulStab hs, coe_mulStab ht, SetLike.coe_subset_coe] at h
Proof state after:
case inr
ι : 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
⊢ s.mulStab.card ∣ t.mulStab.card
Theorem: Finset.card_mulStab_dvd_card_mulStab
Proof state before:
case inr
ι : 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
⊢ s.mulStab.card ∣ t.mulStab.card
Tactic:
letI : Fintype (stabilizer α s) := fintypeStabilizerOfMulStab hs
Proof state after:
case inr
ι : 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
⊢ s.mulStab.card ∣ t.mulStab.card
Theorem: Finset.card_mulStab_dvd_card_mulStab
Proof state before:
case inr
ι : 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
⊢ s.mulStab.card ∣ t.mulStab.card
Tactic:
letI : Fintype (stabilizer α t) := fintypeStabilizerOfMulStab ht
Proof state after:
case inr
ι : 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 ∣ t.mulStab.card
Theorem: Finset.card_mulStab_dvd_card_mulStab
Proof state before:
case inr
ι : 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 ∣ t.mulStab.card
Tactic:
convert Subgroup.card_dvd_of_le h using 1
Proof state after:
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 = Nat.card ↥(stabilizer α s)

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'_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 = Nat.card ↥(stabilizer α s)

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'_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 = Fintype.card ↥(stabilizer α s)

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'_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 = Fintype.card ↥(stabilizer α s)

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:
change _ = (s.mulStab.attach.map
  ⟨Subtype.map id fun _ ↦ (mem_mulStab hs).1, Subtype.map_injective _ injective_id⟩).card
Proof state after:
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)