{G : Type u_1} →
  [inst : Group G] →
    {motive : IsSimpleGroup G → Sort u} →
      ([toNontrivial : Nontrivial G] →
          (eq_bot_or_eq_top_of_normal : ∀ (H : Subgroup G), H.Normal → H = ⊥ ∨ H = ⊤) → motive ⋯) →
        (t : IsSimpleGroup G) → motive t