internlm/Lean-Github huggingface dataset:
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Nontrivial ↥(SubMulAction.ofStabilizer G a)
Tactic:
apply Set.Nontrivial.coe_sort
Proof state after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.Nontrivial ↑(SubMulAction.ofStabilizer G a)
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.Nontrivial ↑(SubMulAction.ofStabilizer G a)
Tactic:
rw [← Set.one_lt_encard_iff_nontrivial]
Proof state after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ 1 < Set.encard ↑(SubMulAction.ofStabilizer G a)
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ 1 < Set.encard ↑(SubMulAction.ofStabilizer G a)
Tactic:
rw [← not_le, ← Nat.cast_one, ← WithTop.add_one_le_coe_succ_iff, not_le]
Proof state after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑(Nat.succ 1) < Set.encard ↑(SubMulAction.ofStabilizer G a) + 1
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑(Nat.succ 1) < Set.encard ↑(SubMulAction.ofStabilizer G a) + 1
Tactic:
rw [← PartENat.withTopEquiv_lt, ← Set.encard_univ] at hsn'
Proof state after:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑(Nat.succ 1) < Set.encard ↑(SubMulAction.ofStabilizer G a) + 1
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case a
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑(Nat.succ 1) < Set.encard ↑(SubMulAction.ofStabilizer G a) + 1
Tactic:
convert hsn'
Proof state after:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑(Nat.succ 1) = PartENat.withTopEquiv 2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑(Nat.succ 1) = PartENat.withTopEquiv 2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Tactic:
simp only [SetLike.coe_sort_coe, Nat.cast_succ, Nat.cast_one]
Proof state after:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑0 + 1 + 1 = PartENat.withTopEquiv 2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑0 + 1 + 1 = PartENat.withTopEquiv 2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Tactic:
rw [← Nat.cast_two]
Proof state after:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑0 + 1 + 1 = PartENat.withTopEquiv ↑2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ ↑0 + 1 + 1 = PartENat.withTopEquiv ↑2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Tactic:
rw [← PartENat.withTopEquiv.symm_apply_eq]
Proof state after:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ PartENat.withTopEquiv.symm (↑0 + 1 + 1) = ↑2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case h.e'_3
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ PartENat.withTopEquiv.symm (↑0 + 1 + 1) = ↑2

case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Tactic:
rfl
Proof state after:
case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ Set.encard ↑(SubMulAction.ofStabilizer G a) + 1 = Set.encard Set.univ
Tactic:
rw [add_comm]
Proof state after:
case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ 1 + Set.encard ↑(SubMulAction.ofStabilizer G a) = Set.encard Set.univ
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
case h.e'_4
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : PartENat.withTopEquiv 2 < Set.encard Set.univ
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
⊢ 1 + Set.encard ↑(SubMulAction.ofStabilizer G a) = Set.encard Set.univ
Tactic:
exact SubMulAction.add_encard_ofStabilizer_eq' a
Proof state after:
no goals
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
⊢ IsPretransitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
Tactic:
rw [isPretransitive_iff_is_one_pretransitive]
Proof state after:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
⊢ IsMultiplyPretransitive (↥(stabilizer G a)) (↥(SubMulAction.ofStabilizer G a)) 1
Theorem: normalClosure_of_stabilizer_eq_top
Proof state before:
α : Type u_1
G : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < PartENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
hG : IsPretransitive G α
this : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : ↑(Subgroup.normalClosure ↑(stabilizer G a)) ⊆ ↑(stabilizer G a)
b c : ↥(SubMulAction.ofStabilizer G a)
hbc : b ≠ c
⊢ IsMultiplyPretransitive (↥(stabilizer G a)) (↥(SubMulAction.ofStabilizer G a)) 1
Tactic:
exact (stabilizer.isMultiplyPretransitive G α hG).mp hG'
Proof state after:
no goals
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
⊢ IsPreprimitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
have hts : s ∩ g • s ≤ s := Set.inter_subset_left s _
Proof state after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
⊢ IsPreprimitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
⊢ IsPreprimitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
have this : IsPretransitive (fixingSubgroup G (s ∩ g • s))
    (SubMulAction.ofFixingSubgroup G (s ∩ g • s)) :=
  isPretransitive_ofFixingSubgroup_inter hs.toIsPretransitive ha
Proof state after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ IsPreprimitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ IsPreprimitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
Tactic:
apply isPreprimitive_of_large_image (f := SubMulAction.ofFixingSubgroup.mapOfInclusion G hts) hs
Proof state after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) <
    2 * Set.ncard (Set.range ⇑(SubMulAction.ofFixingSubgroup.mapOfInclusion G hts))
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) <
    2 * Set.ncard (Set.range ⇑(SubMulAction.ofFixingSubgroup.mapOfInclusion G hts))
Tactic:
rw [← Set.image_univ,
  Set.ncard_image_of_injective _ (SubMulAction.ofFixingSubgroup.mapOfInclusion_injective G _)]
Proof state after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) < 2 * Set.ncard Set.univ
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) < 2 * Set.ncard Set.univ
Tactic:
have this : Set.ncard (s ∩  g • s)ᶜ < 2 * Set.ncard (sᶜ) := by
  rw [Set.compl_inter, ← Nat.add_lt_add_iff_right, Set.ncard_union_add_ncard_inter]
  rw [← Set.compl_union, two_mul, add_assoc]
  simp only [add_lt_add_iff_left]
  rw [← add_lt_add_iff_left, Set.ncard_add_ncard_compl]
  rw [MulAction.smul_set_ncard_eq, ← add_assoc, Set.ncard_add_ncard_compl]
  simp only [lt_add_iff_pos_right]
  rw [Set.ncard_pos]
  rw [Set.nonempty_compl]
  exact ha
Proof state after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) < 2 * Set.ncard Set.univ
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) < 2 * Set.ncard Set.univ
Tactic:
convert this
Proof state after:
case h.e'_3
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Fintype.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) = Set.ncard (s ∩ g • s)ᶜ

case h.e'_4.h.e'_6
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this✝ : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
this : Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
⊢ Set.ncard Set.univ = Set.ncard sᶜ
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Set.ncard (s ∩ g • s)ᶜ < 2 * Set.ncard sᶜ
Tactic:
rw [Set.compl_inter, ← Nat.add_lt_add_iff_right, Set.ncard_union_add_ncard_inter]
Proof state after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Set.ncard sᶜ + Set.ncard (g • s)ᶜ < 2 * Set.ncard sᶜ + Set.ncard (sᶜ ∩ (g • s)ᶜ)
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Set.ncard sᶜ + Set.ncard (g • s)ᶜ < 2 * Set.ncard sᶜ + Set.ncard (sᶜ ∩ (g • s)ᶜ)
Tactic:
rw [← Set.compl_union, two_mul, add_assoc]
Proof state after:
α : Type u_2
G✝ : Type ?u.115687
inst✝⁴ : Group G✝
inst✝³ : MulAction G✝ α
inst✝² : Fintype α
G : Type u_1
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
hs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
g : G
ha : s ∪ g • s ≠ ⊤
hts : s ∩ g • s ≤ s
this : IsPretransitive ↥(fixingSubgroup G (s ∩ g • s)) ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s))
⊢ Set.ncard sᶜ + Set.ncard (g • s)ᶜ < Set.ncard sᶜ + (Set.ncard sᶜ + Set.ncard (s ∪ g • s)ᶜ)