internlm/Lean-Github huggingface dataset:
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
⊢ ¬(a ∈ s ∨ a ∈ 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
h : a ∈ s ∨ a ∈ 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
h : a ∈ s ∨ a ∈ g • s
⊢ False
Tactic:
cases' h with h h
Proof state after:
case 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 α →
              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
h : a ∈ s
⊢ False

case 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 α →
              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
h : a ∈ g • s
⊢ False
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
case 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 α →
              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
h : a ∈ s
⊢ False

case 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 α →
              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
h : a ∈ g • s
⊢ False
Tactic:
exact ha h
Proof state after:
case 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 α →
              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
h : a ∈ g • s
⊢ False
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
case 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 α →
              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
h : a ∈ g • s
⊢ False
Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem] at hga h
Proof state after:
case 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 α →
              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 : g⁻¹ • a ∈ sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
h : g⁻¹ • a ∈ s
⊢ False
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
case 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 α →
              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 : g⁻¹ • a ∈ sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
h : g⁻¹ • a ∈ s
⊢ False
Tactic:
exact hga h
Proof state after:
no goals
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
⊢ 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
h : 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
h : 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
h : 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
h : s ∪ g • s = ⊤
⊢ a ∈ s ∪ g • s
Tactic:
rw [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
h : s ∪ g • s = ⊤
⊢ a ∈ ⊤
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
h : s ∪ g • s = ⊤
⊢ a ∈ ⊤
Tactic:
trivial
Proof state after:
no goals
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)
this : ∃ m < n, Set.ncard t = Nat.succ m
⊢ IsMultiplyPreprimitive G α 2
Tactic:
obtain ⟨m, hmn, htm⟩ := this
Proof state after:
case intro.intro
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)
m : ℕ
hmn : m < n
htm : Set.ncard t = Nat.succ m
⊢ IsMultiplyPreprimitive G α 2
Theorem: is_two_preprimitive_weak_jordan
Proof state before:
case intro.intro
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)
m : ℕ
hmn : m < n
htm : Set.ncard t = Nat.succ m
⊢ IsMultiplyPreprimitive G α 2
Tactic:
exact hrec m hmn hG htm (by
  apply lt_trans _ hsn'
  rw [add_lt_add_iff_left, Nat.succ_lt_succ_iff]
  exact hmn) ht_prim
Proof state after:
no goals
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)
m : ℕ
hmn : m < n
htm : Set.ncard t = Nat.succ m
⊢ 1 + Nat.succ m < Fintype.card α
Tactic:
apply lt_trans _ hsn'
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)
m : ℕ
hmn : m < n
htm : Set.ncard t = Nat.succ m
⊢ 1 + Nat.succ m < 1 + Nat.succ n