internlm/Lean-Github huggingface dataset:
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)ᶜ < Set.ncard sᶜ + (Set.ncard sᶜ + Set.ncard (s ∪ g • s)ᶜ)
Tactic:
simp only [add_lt_add_iff_left]
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 (g • s)ᶜ < 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 (g • s)ᶜ < Set.ncard sᶜ + Set.ncard (s ∪ g • s)ᶜ
Tactic:
rw [← add_lt_add_iff_left, Set.ncard_add_ncard_compl]
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))
⊢ Nat.card α < Set.ncard (g • s) + (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))
⊢ Nat.card α < Set.ncard (g • s) + (Set.ncard sᶜ + Set.ncard (s ∪ g • s)ᶜ)
Tactic:
rw [MulAction.smul_set_ncard_eq, ← add_assoc, Set.ncard_add_ncard_compl]
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))
⊢ Nat.card α < Nat.card α + 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))
⊢ Nat.card α < Nat.card α + Set.ncard (s ∪ g • s)ᶜ
Tactic:
simp only [lt_add_iff_pos_right]
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))
⊢ 0 < 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))
⊢ 0 < Set.ncard (s ∪ g • s)ᶜ
Tactic:
rw [Set.ncard_pos]
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.Nonempty (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.Nonempty (s ∪ g • s)ᶜ
Tactic:
rw [Set.nonempty_compl]
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))
⊢ s ∪ g • s ≠ 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))
⊢ s ∪ g • s ≠ Set.univ
Tactic:
exact ha
Proof state after:
no goals
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
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)ᶜ
Tactic:
rw [← Nat.card_eq_fintype_card, ← Set.Nat.card_coe_set_eq]
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ᶜ
⊢ Nat.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) = Nat.card ↑(s ∩ g • s)ᶜ
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
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ᶜ
⊢ Nat.card ↥(SubMulAction.ofFixingSubgroup G (s ∩ g • s)) = Nat.card ↑(s ∩ g • s)ᶜ
Tactic:
rfl
Proof state after:
no goals
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
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ᶜ
Tactic:
rw [← SubMulAction.ofFixingSubgroup_carrier G]
Proof state after:
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 (SubMulAction.ofFixingSubgroup G s).carrier
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
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 (SubMulAction.ofFixingSubgroup G s).carrier
Tactic:
rw [← Set.ncard_image_of_injective (Set.univ) (SubMulAction.ofFixingSubgroup G s).inclusion_injective]
Proof state after:
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 (⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)) '' Set.univ) =
    Set.ncard (SubMulAction.ofFixingSubgroup G s).carrier
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
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 (⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)) '' Set.univ) =
    Set.ncard (SubMulAction.ofFixingSubgroup G s).carrier
Tactic:
rw [← SubMulAction.image_inclusion]
Proof state after:
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 (⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)) '' Set.univ) =
    Set.ncard (Set.range ⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)))
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
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 (⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)) '' Set.univ) =
    Set.ncard (Set.range ⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)))
Tactic:
congr
Proof state after:
case h.e'_4.h.e'_6.e_s
α : 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ᶜ
⊢ ⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)) '' Set.univ =
    Set.range ⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s))
Theorem: IsPreprimitive.isPreprimitive_ofFixingSubgroup_inter
Proof state before:
case h.e'_4.h.e'_6.e_s
α : 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ᶜ
⊢ ⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s)) '' Set.univ =
    Set.range ⇑(SubMulAction.inclusion (SubMulAction.ofFixingSubgroup G s))
Tactic:
simp only [Set.image_univ]
Proof state after:
no goals
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
α : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive G α
s : Set α
n : ℕ
hsn : Set.ncard s = Nat.succ n
hsn' : 1 + Nat.succ n < Fintype.card α
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
⊢ IsMultiplyPretransitive G α 2
Tactic:
revert α G
Proof state after:
n : ℕ
⊢ ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
    [inst_3 : DecidableEq α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
n : ℕ
⊢ ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
    [inst_3 : DecidableEq α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
Tactic:
induction' n using Nat.strong_induction_on with n hrec
Proof state after:
case h
n : ℕ
hrec :
  ∀ m < n,
    ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
      [inst_3 : DecidableEq α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          Set.ncard s = Nat.succ m →
            1 + Nat.succ m < Fintype.card α →
              IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
⊢ ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
    [inst_3 : DecidableEq α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case h
n : ℕ
hrec :
  ∀ m < n,
    ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
      [inst_3 : DecidableEq α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          Set.ncard s = Nat.succ m →
            1 + Nat.succ m < Fintype.card α →
              IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
⊢ ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
    [inst_3 : DecidableEq α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
Tactic:
intro α G _ _ _ _ hG s hsn hsn' hs_trans
Proof state after:
case h
n : ℕ
hrec :
  ∀ m < n,
    ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
      [inst_3 : DecidableEq α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          Set.ncard s = Nat.succ m →
            1 + Nat.succ m < Fintype.card α →
              IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
α : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ n
hsn' : 1 + Nat.succ n < Fintype.card α
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
⊢ IsMultiplyPretransitive G α 2
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case h
n : ℕ
hrec :
  ∀ m < n,
    ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
      [inst_3 : DecidableEq α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          Set.ncard s = Nat.succ m →
            1 + Nat.succ m < Fintype.card α →
              IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
α : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ n
hsn' : 1 + Nat.succ n < Fintype.card α
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
⊢ IsMultiplyPretransitive G α 2
Tactic:
have hs_ne_top : s ≠ ⊤ := by
  intro hs
  rw [hs, Set.top_eq_univ, Set.ncard_univ] at hsn
  rw [← hsn, Nat.card_eq_fintype_card, add_lt_iff_neg_right] at hsn'
  contradiction
Proof state after:
case h
n : ℕ
hrec :
  ∀ m < n,
    ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
      [inst_3 : DecidableEq α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          Set.ncard s = Nat.succ m →
            1 + Nat.succ m < Fintype.card α →
              IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
α : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ n
hsn' : 1 + Nat.succ n < Fintype.card α
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
⊢ IsMultiplyPretransitive G α 2
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case h
n : ℕ
hrec :
  ∀ m < n,
    ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
      [inst_3 : DecidableEq α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          Set.ncard s = Nat.succ m →
            1 + Nat.succ m < Fintype.card α →
              IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
α : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ n
hsn' : 1 + Nat.succ n < Fintype.card α
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
⊢ IsMultiplyPretransitive G α 2
Tactic:
have hs_nonempty : s.Nonempty := by
  rw [← Set.ncard_pos, hsn]
  exact Nat.succ_pos n
Proof state after:
case h
n : ℕ
hrec :
  ∀ m < n,
    ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
      [inst_3 : DecidableEq α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          Set.ncard s = Nat.succ m →
            1 + Nat.succ m < Fintype.card α →
              IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
α : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ n
hsn' : 1 + Nat.succ n < Fintype.card α
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
⊢ IsMultiplyPretransitive G α 2
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case h
n : ℕ
hrec :
  ∀ m < n,
    ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
      [inst_3 : DecidableEq α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          Set.ncard s = Nat.succ m →
            1 + Nat.succ m < Fintype.card α →
              IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
α : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ n
hsn' : 1 + Nat.succ n < Fintype.card α
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
⊢ IsMultiplyPretransitive G α 2
Tactic:
cases' Nat.lt_or_ge n.succ 2 with hn hn
Proof state after:
case h.inl
n : ℕ
hrec :
  ∀ m < n,
    ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
      [inst_3 : DecidableEq α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          Set.ncard s = Nat.succ m →
            1 + Nat.succ m < Fintype.card α →
              IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
α : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ n
hsn' : 1 + Nat.succ n < Fintype.card α
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n < 2
⊢ IsMultiplyPretransitive G α 2

case h.inr
n : ℕ
hrec :
  ∀ m < n,
    ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α]
      [inst_3 : DecidableEq α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          Set.ncard s = Nat.succ m →
            1 + Nat.succ m < Fintype.card α →
              IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2
α : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : MulAction G α
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ n
hsn' : 1 + Nat.succ n < Fintype.card α
hs_trans : IsPretransitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
⊢ IsMultiplyPretransitive G α 2