Theorem: isMultiplyPreprimitive_jordan
Proof state before:
case refine'_2.a
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✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer G a)) t)
this : n + 2 = 1 + Nat.succ n
⊢ ?refine'_2.n + Nat.succ (Nat.succ n) < ?refine'_2.n + Set.ncard {a}ᶜ

case refine'_2.n
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✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer G a)) t)
this : n + 2 = 1 + Nat.succ n
⊢ ℕ
Tactic:
rw [Set.ncard_add_ncard_compl]
Proof state after:
case refine'_2.a
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✝¹ : MulAction G α
inst✝ : Fintype α
hG : IsPreprimitive G α
s : Set α
hsn : Set.ncard s = Nat.succ (Nat.succ n)
hα : 1 + Nat.succ (Nat.succ n) < Fintype.card α
hGs : IsPreprimitive ↥(fixingSubgroup G s) ↥(SubMulAction.ofFixingSubgroup G s)
a : α
t : Set ↥(SubMulAction.ofStabilizer G a)
left✝ : a ∈ s
hst : s = insert a (Subtype.val '' t)
ha' : a ∉ Subtype.val '' t
ht_prim : IsPreprimitive ↥(stabilizer G a) ↥(SubMulAction.ofStabilizer G a)
hGs' : IsPreprimitive ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(SubMulAction.ofFixingSubgroup (↥(stabilizer G a)) t)
this : n + 2 = 1 + Nat.succ n
⊢ Set.ncard {a} + Nat.succ (Nat.succ n) < Nat.card α