Theorem: is_two_pretransitive_weak_jordan
Proof state before:
case h.inl.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' : 1 + Nat.succ n < Fintype.card α
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn✝ : Nat.succ n < 2
hn : n = 0
a : α
hs_trans : IsPretransitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsMultiplyPretransitive (↥(stabilizer G ?m.143299)) (↥(SubMulAction.ofStabilizer G ?m.143299)) 1

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' : 1 + Nat.succ n < Fintype.card α
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn✝ : Nat.succ n < 2
hn : n = 0
a : α
hs_trans : IsPretransitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ α
Tactic:
rw [← isPretransitive_iff_is_one_pretransitive]
Proof state after:
case h.inl.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' : 1 + Nat.succ n < Fintype.card α
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn✝ : Nat.succ n < 2
hn : n = 0
a : α
hs_trans : IsPretransitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ IsPretransitive ↥(stabilizer G ?m.143299) ↥(SubMulAction.ofStabilizer G ?m.143299)

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' : 1 + Nat.succ n < Fintype.card α
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn✝ : Nat.succ n < 2
hn : n = 0
a : α
hs_trans : IsPretransitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {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' : 1 + Nat.succ n < Fintype.card α
hs_ne_top : s ≠ ⊤
hs_nonempty : Set.Nonempty s
hn✝ : Nat.succ n < 2
hn : n = 0
a : α
hs_trans : IsPretransitive ↥(fixingSubgroup G {a}) ↥(SubMulAction.ofFixingSubgroup G {a})
hsa : s = {a}
⊢ α