internlm/Lean-Github huggingface dataset:
Theorem: is_two_pretransitive_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 α →
              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
⊢ n = 0
Tactic:
rw [← le_zero_iff]
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 α →
              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
⊢ n ≤ 0
Theorem: is_two_pretransitive_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 α →
              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
⊢ n ≤ 0
Tactic:
apply Nat.le_of_succ_le_succ
Proof state after:
case 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 α →
              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
⊢ Nat.succ n ≤ Nat.succ 0
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case 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 α →
              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
⊢ Nat.succ n ≤ Nat.succ 0
Tactic:
apply Nat.le_of_lt_succ
Proof state after:
case a.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 α →
              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
⊢ Nat.succ n < Nat.succ (Nat.succ 0)
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case a.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 α →
              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
⊢ Nat.succ n < Nat.succ (Nat.succ 0)
Tactic:
exact hn
Proof state after:
no goals
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case h.inr.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
hn1 : 2 * Nat.succ n < Fintype.card α
⊢ IsMultiplyPretransitive G α 2
Tactic:
have : 1 < s.ncard := by rw [hsn]; exact hn
Proof state after:
case h.inr.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
hn1 : 2 * Nat.succ n < Fintype.card α
this : 1 < Set.ncard s
⊢ IsMultiplyPretransitive G α 2
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case h.inr.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
hn1 : 2 * Nat.succ n < Fintype.card α
this : 1 < Set.ncard s
⊢ IsMultiplyPretransitive G α 2
Tactic:
rw [Set.one_lt_ncard] at this
Proof state after:
case h.inr.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
hn1 : 2 * Nat.succ n < Fintype.card α
this : ∃ a ∈ s, ∃ b ∈ s, a ≠ b
⊢ IsMultiplyPretransitive G α 2
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case h.inr.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
hn1 : 2 * Nat.succ n < Fintype.card α
this : ∃ a ∈ s, ∃ b ∈ s, a ≠ b
⊢ IsMultiplyPretransitive G α 2
Tactic:
obtain ⟨a, ha, b, hb, hab⟩ := this
Proof state after:
case h.inr.inl.intro.intro.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 α →
              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
hn1 : 2 * Nat.succ n < Fintype.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
⊢ IsMultiplyPretransitive G α 2
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case h.inr.inl.intro.intro.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 α →
              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
hn1 : 2 * Nat.succ n < Fintype.card α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≠ b
⊢ IsMultiplyPretransitive G α 2
Tactic:
obtain ⟨g, hga, hgb⟩ := Rudio hG s (Set.toFinite s) hs_nonempty hs_ne_top a b hab
Proof state after:
case h.inr.inl.intro.intro.intro.intro.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 α →
              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
hn1 : 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
⊢ IsMultiplyPretransitive G α 2
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case h.inr.inl.intro.intro.intro.intro.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 α →
              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
hn1 : 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
⊢ IsMultiplyPretransitive G α 2
Tactic:
let t := s ∩ g • s
Proof state after:
case h.inr.inl.intro.intro.intro.intro.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 α →
              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
hn1 : 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
⊢ IsMultiplyPretransitive G α 2
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case h.inr.inl.intro.intro.intro.intro.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 α →
              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
hn1 : 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
⊢ IsMultiplyPretransitive G α 2
Tactic:
have ht_trans : IsPretransitive (fixingSubgroup G t)
  (SubMulAction.ofFixingSubgroup G t) :=
    isPretransitive_ofFixingSubgroup_inter hs_trans (by
      apply Set.ncard_pigeonhole_compl'
      rw [smul_set_ncard_eq, hsn, ← two_mul]
      exact hn1)
Proof state after:
case h.inr.inl.intro.intro.intro.intro.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 α →
              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
hn1 : 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
ht_trans : IsPretransitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
⊢ IsMultiplyPretransitive G α 2
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case h.inr.inl.intro.intro.intro.intro.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 α →
              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
hn1 : 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
ht_trans : IsPretransitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
⊢ IsMultiplyPretransitive G α 2
Tactic:
suffices ∃ m, m < n ∧ t.ncard = Nat.succ m by
  obtain ⟨m, hmn, htm⟩ := this
  apply hrec m hmn hG htm _ ht_trans
  apply lt_trans _ hsn'
  rw [add_lt_add_iff_left, Nat.succ_lt_succ_iff]
  exact hmn
Proof state after:
case h.inr.inl.intro.intro.intro.intro.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 α →
              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
hn1 : 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
ht_trans : IsPretransitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
⊢ ∃ m < n, Set.ncard t = Nat.succ m
Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case h.inr.inl.intro.intro.intro.intro.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 α →
              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
hn1 : 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
ht_trans : IsPretransitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
⊢ ∃ m < n, Set.ncard t = Nat.succ m
Tactic:
use t.ncard.pred
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
hn : Nat.succ n ≥ 2
hn1 : 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
ht_trans : IsPretransitive ↥(fixingSubgroup G t) ↥(SubMulAction.ofFixingSubgroup G t)
⊢ Nat.pred (Set.ncard t) < n ∧ Set.ncard t = Nat.succ (Nat.pred (Set.ncard t))