internlm/Lean-Github huggingface dataset:
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
case right.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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this✝ : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
this : Set.ncard t ≠ 0
h : s ⊆ t
⊢ Set.ncard (g • s) ≤ Set.ncard s
Tactic:
rw [smul_set_ncard_eq]
Proof state after:
no goals
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
case right
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this✝ : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
this : Set.ncard t ≠ 0
⊢ Set.ncard t = Set.ncard t
Tactic:
rfl
Proof state after:
no goals
Theorem: is_two_preprimitive_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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
⊢ Set.ncard t ≠ 0
Tactic:
rw [← Nat.pos_iff_ne_zero]
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
⊢ 0 < Set.ncard t
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
case h.a
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
⊢ Set.ncard (s ∪ g • s) < 2 * Nat.succ n
Tactic:
apply lt_of_lt_of_le _ hn2
Proof state after:
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
⊢ Set.ncard (s ∪ g • s) < Fintype.card α
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
⊢ Set.ncard (s ∪ g • s) < Fintype.card α
Tactic:
rw [← not_le]
Proof state after:
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
⊢ ¬Fintype.card α ≤ Set.ncard (s ∪ g • s)
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
⊢ ¬Fintype.card α ≤ Set.ncard (s ∪ g • s)
Tactic:
intro h
Proof state after:
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
h : Fintype.card α ≤ Set.ncard (s ∪ g • s)
⊢ False
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
h : Fintype.card α ≤ Set.ncard (s ∪ g • s)
⊢ False
Tactic:
apply this
Proof state after:
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
h : Fintype.card α ≤ Set.ncard (s ∪ g • s)
⊢ a ∈ s ∪ g • s
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
h : Fintype.card α ≤ Set.ncard (s ∪ g • s)
⊢ a ∈ s ∪ g • s
Tactic:
convert Set.mem_univ a
Proof state after:
case h.e'_5
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
h : Fintype.card α ≤ Set.ncard (s ∪ g • s)
⊢ s ∪ g • s = Set.univ
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
case h.e'_5
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
h : Fintype.card α ≤ Set.ncard (s ∪ g • s)
⊢ s ∪ g • s = Set.univ
Tactic:
apply Set.eq_of_subset_of_ncard_le (Set.subset_univ _) _ Set.finite_univ
Proof state after:
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
h : Fintype.card α ≤ Set.ncard (s ∪ g • s)
⊢ Set.ncard Set.univ ≤ Set.ncard (s ∪ g • s)
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
h : Fintype.card α ≤ Set.ncard (s ∪ g • s)
⊢ Set.ncard Set.univ ≤ Set.ncard (s ∪ g • s)
Tactic:
simp only [Set.ncard_univ, Nat.card_eq_fintype_card]
Proof state after:
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
h : Fintype.card α ≤ Set.ncard (s ∪ g • s)
⊢ Fintype.card α ≤ Set.ncard (s ∪ g • s)
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
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 α →
              IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) → IsMultiplyPreprimitive 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_prim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn : Nat.succ n ≥ 2
hn2 : 2 * Nat.succ n ≥ Fintype.card α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
this : a ∉ s ∪ g • s
ht_prim : IsPreprimitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
h : Fintype.card α ≤ Set.ncard (s ∪ g • s)
⊢ Fintype.card α ≤ Set.ncard (s ∪ g • s)
Tactic:
exact h
Proof state after:
no goals
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
α : Type u_2
G : Type u_1
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
n : ℕ
hsn : Set.ncard s = Nat.succ n
hsn' : 1 + Nat.succ n < Fintype.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
⊢ IsMultiplyPreprimitive G α (1 + Nat.succ n)
Tactic:
revert α G
Proof state after:
n : ℕ
⊢ ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
Theorem: isMultiplyPreprimitive_jordan
Proof state before:
n : ℕ
⊢ ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
Tactic:
induction' n with n hrec
Proof state after:
case zero

⊢ ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ Nat.zero →
          1 + Nat.succ Nat.zero < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ Nat.zero)

case succ
n : ℕ
hrec :
  ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ n →
          1 + Nat.succ n < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ n)
⊢ ∀ {α : Type u_2} {G : Type u_1} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : Fintype α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        Set.ncard s = Nat.succ (Nat.succ n) →
          1 + Nat.succ (Nat.succ n) < Fintype.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s) →
              IsMultiplyPreprimitive G α (1 + Nat.succ (Nat.succ n))