internlm/Lean-Github huggingface dataset:
Theorem: SimpleGraph.not_isContained_kill
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
⊢ (Subgraph.map (Hom.ofLE ⋯) H').edgeSet.Nonempty
Tactic:
rw [Subgraph.edgeSet_map]
Proof state after:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
⊢ (Sym2.map ⇑(Hom.ofLE ⋯) '' H'.edgeSet).Nonempty
Theorem: SimpleGraph.not_isContained_kill
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
hG : G ≠ ⊥
H' : (H \ fromEdgeSet (⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})).Subgraph
hGH' : Nonempty (G ≃g H'.coe)
⊢ (Sym2.map ⇑(Hom.ofLE ⋯) '' H'.edgeSet).Nonempty
Tactic:
exact (aux hG hGH').image _
Proof state after:
no goals
Theorem: SimpleGraph.le_card_edgeFinset_kill
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
⊢ H.edgeFinset.card - G.copyCount H ≤ (G.kill H).edgeFinset.card
Tactic:
obtain rfl | hG := eq_or_ne G ⊥
Proof state after:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
⊢ H.edgeFinset.card - ⊥.copyCount H ≤ (⊥.kill H).edgeFinset.card

case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
⊢ H.edgeFinset.card - G.copyCount H ≤ (G.kill H).edgeFinset.card
Theorem: SimpleGraph.le_card_edgeFinset_kill
Proof state before:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
⊢ H.edgeFinset.card - G.copyCount H ≤ (G.kill H).edgeFinset.card
Tactic:
let f (H' : {H' : H.Subgraph // Nonempty (G ≃g H'.coe)}) := (aux hG H'.2).some
Proof state after:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ H.edgeFinset.card - G.copyCount H ≤ (G.kill H).edgeFinset.card
Theorem: SimpleGraph.le_card_edgeFinset_kill
Proof state before:
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ H.edgeFinset.card - G.copyCount H ≤ (G.kill H).edgeFinset.card
Tactic:
calc
  _ = H.edgeFinset.card - card {H' : H.Subgraph // Nonempty (G ≃g H'.coe)} := ?_
  _ ≤ H.edgeFinset.card - (univ.image f).card := Nat.sub_le_sub_left card_image_le _
  _ = H.edgeFinset.card - (Set.range f).toFinset.card := by rw [Set.toFinset_range]
  _ ≤ (H.edgeFinset \ (Set.range f).toFinset).card := le_card_sdiff ..
  _ = (G.kill H).edgeFinset.card := ?_
Proof state after:
case inr.calc_1
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ H.edgeFinset.card - G.copyCount H = H.edgeFinset.card - Fintype.card { H' // Nonempty (G ≃g H'.coe) }

case inr.calc_2
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ (H.edgeFinset \ (Set.range f).toFinset).card = (G.kill H).edgeFinset.card
Theorem: SimpleGraph.le_card_edgeFinset_kill
Proof state before:
case inr.calc_2
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ (H.edgeFinset \ (Set.range f).toFinset).card = (G.kill H).edgeFinset.card
Tactic:
simp only [kill_of_ne_bot, hG, Ne, not_false_iff, Set.iUnion_singleton_eq_range,
  Set.toFinset_card, Fintype.card_ofFinset, edgeSet_deleteEdges]
Proof state after:
case inr.calc_2
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ (H.edgeFinset \ (Set.range f).toFinset).card =
    Fintype.card ↑(H.edgeSet \ ⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})
Theorem: SimpleGraph.le_card_edgeFinset_kill
Proof state before:
case inr.calc_2
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ (H.edgeFinset \ (Set.range f).toFinset).card =
    Fintype.card ↑(H.edgeSet \ ⋃ H', ⋃ (hH' : Nonempty (G ≃g H'.coe)), {⋯.some})
Tactic:
simp only [Finset.sdiff_eq_inter_compl, Set.diff_eq, ← Set.iUnion_singleton_eq_range, coe_sdiff,
  Set.coe_toFinset, coe_filter, Set.sep_mem_eq, Set.iUnion_subtype, ← Fintype.card_coe,
  ← Finset.coe_sort_coe, coe_inter, coe_compl, Set.coe_toFinset, Set.compl_iUnion,
  Fintype.card_ofFinset]
Proof state after:
no goals
Theorem: SimpleGraph.le_card_edgeFinset_kill
Proof state before:
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
⊢ H.edgeFinset.card - ⊥.copyCount H ≤ (⊥.kill H).edgeFinset.card
Tactic:
simp
Proof state after:
no goals
Theorem: SimpleGraph.le_card_edgeFinset_kill
Proof state before:
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ H.edgeFinset.card - (image f univ).card = H.edgeFinset.card - (Set.range f).toFinset.card
Tactic:
rw [Set.toFinset_range]
Proof state after:
no goals
Theorem: SimpleGraph.le_card_edgeFinset_kill
Proof state before:
case inr.calc_1
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ H.edgeFinset.card - G.copyCount H = H.edgeFinset.card - Fintype.card { H' // Nonempty (G ≃g H'.coe) }
Tactic:
simp only [Set.toFinset_card]
Proof state after:
case inr.calc_1
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ Fintype.card ↑H.edgeSet - G.copyCount H = Fintype.card ↑H.edgeSet - Fintype.card { H' // Nonempty (G ≃g H'.coe) }
Theorem: SimpleGraph.le_card_edgeFinset_kill
Proof state before:
case inr.calc_1
α : Type u_1
β : Type u_2
γ : Type u_3
G G₁ G₂ G₃ : SimpleGraph α
H : SimpleGraph β
I : SimpleGraph γ
inst✝¹ : Fintype ↑H.edgeSet
inst✝ : Fintype β
hG : G ≠ ⊥
f : { H' // Nonempty (G ≃g H'.coe) } → Sym2 β := fun H' => ⋯.some
⊢ Fintype.card ↑H.edgeSet - G.copyCount H = Fintype.card ↑H.edgeSet - Fintype.card { H' // Nonempty (G ≃g H'.coe) }
Tactic:
rw [← Set.toFinset_card, ← edgeFinset, copyCount, ← card_subtype, subtype_univ, card_univ]
Proof state after:
no goals
Theorem: Finset.mem_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ a ∈ s.mulStab ↔ a • s = s
Tactic:
rw [mulStab, mem_filter, mem_div, and_iff_right_of_imp]
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ a • s = s → ∃ b ∈ s, ∃ c ∈ s, b / c = a
Theorem: Finset.mem_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ a • s = s → ∃ b ∈ s, ∃ c ∈ s, b / c = a
Tactic:
obtain ⟨b, hb⟩ := hs
Proof state after:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a b : α
hb : b ∈ s
⊢ a • s = s → ∃ b ∈ s, ∃ c ∈ s, b / c = a
Theorem: Finset.mem_mulStab
Proof state before:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a b : α
hb : b ∈ s
⊢ a • s = s → ∃ b ∈ s, ∃ c ∈ s, b / c = a
Tactic:
exact fun h ↦ ⟨_, by rw [← h]; exact smul_mem_smul_finset hb, _, hb, mul_div_cancel_right _ _⟩
Proof state after:
no goals
Theorem: Finset.mem_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a b : α
hb : b ∈ s
h : a • s = s
⊢ a * b ∈ s
Tactic:
rw [← h]
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a b : α
hb : b ∈ s
h : a • s = s
⊢ a * b ∈ a • s
Theorem: Finset.mem_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a b : α
hb : b ∈ s
h : a • s = s
⊢ a * b ∈ a • s
Tactic:
exact smul_mem_smul_finset hb
Proof state after:
no goals
Theorem: Finset.mulStab_subset_div_right
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
⊢ s.mulStab ⊆ s / {a}
Tactic:
refine fun b hb ↦ mem_div.2 ⟨_, ?_, _, mem_singleton_self _, mul_div_cancel_right _ _⟩
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ s.mulStab
⊢ b * a ∈ s
Theorem: Finset.mulStab_subset_div_right
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b ∈ s.mulStab
⊢ b * a ∈ s
Tactic:
rw [mem_mulStab ⟨a, ha⟩] at hb
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b • s = s
⊢ b * a ∈ s
Theorem: Finset.mulStab_subset_div_right
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b • s = s
⊢ b * a ∈ s
Tactic:
rw [← hb]
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b • s = s
⊢ b * a ∈ b • s
Theorem: Finset.mulStab_subset_div_right
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s
b : α
hb : b • s = s
⊢ b * a ∈ b • s
Tactic:
exact smul_mem_smul_finset ha
Proof state after:
no goals
Theorem: Finset.coe_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ ↑s.mulStab = ↑(stabilizer α s)
Tactic:
ext
Proof state after:
case h
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
x✝ : α
⊢ x✝ ∈ ↑s.mulStab ↔ x✝ ∈ ↑(stabilizer α s)
Theorem: Finset.coe_mulStab
Proof state before:
case h
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
x✝ : α
⊢ x✝ ∈ ↑s.mulStab ↔ x✝ ∈ ↑(stabilizer α s)
Tactic:
simp [mem_mulStab hs]
Proof state after:
no goals
Theorem: Finset.mem_mulStab_iff_subset_smul_finset
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ a ∈ s.mulStab ↔ s ⊆ a • s
Tactic:
rw [← mem_coe, coe_mulStab hs, SetLike.mem_coe, mem_stabilizer_finset_iff_subset_smul_finset]
Proof state after:
no goals
Theorem: Finset.mem_mulStab_iff_smul_finset_subset
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ a ∈ s.mulStab ↔ a • s ⊆ s
Tactic:
rw [← mem_coe, coe_mulStab hs, SetLike.mem_coe, mem_stabilizer_finset_iff_smul_finset_subset]
Proof state after:
no goals
Theorem: Finset.mem_mulStab'
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ a ∈ s.mulStab ↔ ∀ ⦃b : α⦄, b ∈ s → a • b ∈ s
Tactic:
rw [← mem_coe, coe_mulStab hs, SetLike.mem_coe, mem_stabilizer_finset']
Proof state after:
no goals
Theorem: Finset.mulStab_empty
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ∅.mulStab = ∅
Tactic:
simp [mulStab]
Proof state after:
no goals
Theorem: Finset.mulStab_singleton
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ a : α
⊢ {a}.mulStab = 1
Tactic:
simp [mulStab, singleton_one, filter_true_of_mem]
Proof state after:
no goals
Theorem: Finset.Nonempty.of_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s.mulStab.Nonempty → s.Nonempty
Tactic:
simp_rw [nonempty_iff_ne_empty, not_imp_not]
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s = ∅ → s.mulStab = ∅
Theorem: Finset.Nonempty.of_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s = ∅ → s.mulStab = ∅
Tactic:
rintro rfl
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
t : Finset α
a : α
⊢ ∅.mulStab = ∅
Theorem: Finset.Nonempty.of_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
t : Finset α
a : α
⊢ ∅.mulStab = ∅
Tactic:
exact mulStab_empty
Proof state after:
no goals
Theorem: Finset.card_mulStab_eq_one
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s.mulStab.card = 1 ↔ s.mulStab = 1
Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, card_one]⟩
Proof state after:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
h : s.mulStab.card = 1
⊢ s.mulStab = 1
Theorem: Finset.card_mulStab_eq_one
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
h : s.mulStab.card = 1
⊢ s.mulStab = 1
Tactic:
obtain ⟨a, ha⟩ := card_eq_one.1 h
Proof state after:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
h : s.mulStab.card = 1
a : α
ha : s.mulStab = {a}
⊢ s.mulStab = 1
Theorem: Finset.card_mulStab_eq_one
Proof state before:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
h : s.mulStab.card = 1
a : α
ha : s.mulStab = {a}
⊢ s.mulStab = 1
Tactic:
rw [ha]
Proof state after:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
h : s.mulStab.card = 1
a : α
ha : s.mulStab = {a}
⊢ {a} = 1
Theorem: Finset.card_mulStab_eq_one
Proof state before:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
h : s.mulStab.card = 1
a : α
ha : s.mulStab = {a}
⊢ {a} = 1
Tactic:
rw [eq_singleton_iff_nonempty_unique_mem, mulStab_nonempty, ← one_mem_mulStab] at ha
Proof state after:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
h : s.mulStab.card = 1
a : α
ha : 1 ∈ s.mulStab ∧ ∀ x ∈ s.mulStab, x = a
⊢ {a} = 1
Theorem: Finset.card_mulStab_eq_one
Proof state before:
case intro
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
h : s.mulStab.card = 1
a : α
ha : 1 ∈ s.mulStab ∧ ∀ x ∈ s.mulStab, x = a
⊢ {a} = 1
Tactic:
rw [← ha.2 _ ha.1, singleton_one]
Proof state after:
no goals
Theorem: Finset.card_mulStab_eq_one
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
h : s.mulStab = 1
⊢ s.mulStab.card = 1
Tactic:
rw [h, card_one]
Proof state after:
no goals
Theorem: Finset.subset_mulStab_mul_left
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ht : t.Nonempty
⊢ s.mulStab ⊆ (s * t).mulStab
Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
Proof state after:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
t : Finset α
a : α
ht : t.Nonempty
⊢ ∅.mulStab ⊆ (∅ * t).mulStab

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ht : t.Nonempty
hs : s.Nonempty
⊢ s.mulStab ⊆ (s * t).mulStab
Theorem: Finset.subset_mulStab_mul_left
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ht : t.Nonempty
hs : s.Nonempty
⊢ s.mulStab ⊆ (s * t).mulStab
Tactic:
simp_rw [subset_iff, mem_mulStab hs, mem_mulStab (hs.mul ht)]
Proof state after:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ht : t.Nonempty
hs : s.Nonempty
⊢ ∀ ⦃x : α⦄, x • s = s → x • (s * t) = s * t
Theorem: Finset.subset_mulStab_mul_left
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ht : t.Nonempty
hs : s.Nonempty
⊢ ∀ ⦃x : α⦄, x • s = s → x • (s * t) = s * t
Tactic:
rintro a h
Proof state after:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
ht : t.Nonempty
hs : s.Nonempty
a : α
h : a • s = s
⊢ a • (s * t) = s * t
Theorem: Finset.subset_mulStab_mul_left
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a✝ : α
ht : t.Nonempty
hs : s.Nonempty
a : α
h : a • s = s
⊢ a • (s * t) = s * t
Tactic:
rw [← smul_mul_assoc, h]
Proof state after:
no goals
Theorem: Finset.subset_mulStab_mul_left
Proof state before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
t : Finset α
a : α
ht : t.Nonempty
⊢ ∅.mulStab ⊆ (∅ * t).mulStab
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mulStab_mul
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ s.mulStab * s = s
Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
Proof state after:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ∅.mulStab * ∅ = ∅

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ s.mulStab * s = s
Theorem: Finset.mulStab_mul
Proof state before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ∅.mulStab * ∅ = ∅
Tactic:
exact mul_empty _
Proof state after:
no goals
Theorem: Finset.mulStab_mul
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ s.mulStab * s = s
Tactic:
simp only [← coe_inj, hs, coe_mul, coe_mulStab, ← stabilizer_coe_finset, stabilizer_mul_self]
Proof state after:
no goals
Theorem: Finset.mul_subset_right_iff
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ht : t.Nonempty
⊢ s * t ⊆ t ↔ s ⊆ t.mulStab
Tactic:
simp_rw [← smul_eq_mul, ← biUnion_smul_finset, biUnion_subset,
  ← mem_mulStab_iff_smul_finset_subset ht, subset_iff]
Proof state after:
no goals
Theorem: Finset.mul_subset_right
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s ⊆ t.mulStab → s * t ⊆ t
Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty
Proof state after:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s ⊆ ∅.mulStab → s * ∅ ⊆ ∅

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ht : t.Nonempty
⊢ s ⊆ t.mulStab → s * t ⊆ t
Theorem: Finset.mul_subset_right
Proof state before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ s ⊆ ∅.mulStab → s * ∅ ⊆ ∅
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mul_subset_right
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ht : t.Nonempty
⊢ s ⊆ t.mulStab → s * t ⊆ t
Tactic:
exact (mul_subset_right_iff ht).2
Proof state after:
no goals
Theorem: Finset.smul_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s.mulStab
⊢ 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✝¹ : Group α
inst✝ : DecidableEq α
t : Finset α
a : α
ha : a ∈ ∅.mulStab
⊢ a • ∅.mulStab = ∅.mulStab

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s.mulStab
hs : s.Nonempty
⊢ a • s.mulStab = s.mulStab
Theorem: Finset.smul_mulStab
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ s.mulStab
hs : s.Nonempty
⊢ a • s.mulStab = s.mulStab
Tactic:
rw [← mem_coe, coe_mulStab hs, SetLike.mem_coe] at ha
Proof state after:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ stabilizer α s
hs : s.Nonempty
⊢ a • s.mulStab = s.mulStab
Theorem: Finset.smul_mulStab
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
ha : a ∈ stabilizer α s
hs : s.Nonempty
⊢ a • s.mulStab = s.mulStab
Tactic:
rw [← coe_inj, coe_smul_finset, coe_mulStab hs, Subgroup.smul_coe ha]
Proof state after:
no goals
Theorem: Finset.smul_mulStab
Proof state before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
t : Finset α
a : α
ha : a ∈ ∅.mulStab
⊢ a • ∅.mulStab = ∅.mulStab
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mulStab_mul_mulStab
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
⊢ s.mulStab * 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✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ∅.mulStab * ∅.mulStab = ∅.mulStab

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ s.mulStab * s.mulStab = s.mulStab
Theorem: Finset.mulStab_mul_mulStab
Proof state before:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ ∅.mulStab * ∅.mulStab = ∅.mulStab
Tactic:
simp
Proof state after:
no goals
Theorem: Finset.mulStab_mul_mulStab
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s✝ t : Finset α
a : α
s : Finset α
hs : s.Nonempty
⊢ s.mulStab * s.mulStab = s.mulStab
Tactic:
simp_rw [← smul_eq_mul, ← biUnion_smul_finset, biUnion_congr rfl fun _ ↦ smul_mulStab,
  ← sup_eq_biUnion, sup_const hs.mulStab]
Proof state after:
no goals
Theorem: Finset.inter_mulStab_subset_mulStab_union
Proof state before:
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
⊢ s.mulStab ∩ t.mulStab ⊆ (s ∪ t).mulStab
Tactic:
obtain rfl | hs := s.eq_empty_or_nonempty
Proof state after:
case inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
t : Finset α
a : α
⊢ ∅.mulStab ∩ t.mulStab ⊆ (∅ ∪ t).mulStab

case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ s.mulStab ∩ t.mulStab ⊆ (s ∪ t).mulStab
Theorem: Finset.inter_mulStab_subset_mulStab_union
Proof state before:
case inr
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s t : Finset α
a : α
hs : s.Nonempty
⊢ s.mulStab ∩ t.mulStab ⊆ (s ∪ t).mulStab
Tactic:
obtain rfl | ht := t.eq_empty_or_nonempty
Proof state after:
case inr.inl
ι : Type u_1
α : Type u_2
inst✝¹ : Group α
inst✝ : DecidableEq α
s : Finset α
a : α
hs : s.Nonempty
⊢ s.mulStab ∩ ∅.mulStab ⊆ (s ∪ ∅).mulStab

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