case _ hi e =>
  let ⟨steps, tail⟩ := hi $ e.preserves_nontrivial n
  exact match steps, tail with
  | .refl,                   .none    => ⟨.refl, .some $ .single e⟩ 
  | .refl,                   .some e' => ⟨.refl, .some $ .trans e e'⟩
  | .step (.inst ⟨f, h⟩) f', tl       => ⟨.step (.inst ⟨.trans e f, h⟩) f', tl⟩
  | .step (.time f) f',      tl       => ⟨.step (.inst ⟨.single e, f.closed⟩) $ .step f f', tl⟩
α : Type
inst✝ : Hierarchical α
s₁ s₂ s₁✝ s₂✝ s₃✝ : State α
a✝ : s₂✝ ⇓ s₃✝
hi : State.Nontrivial s₂✝ → Nonempty (Grouped s₂✝ s₃✝)
n : State.Nontrivial s₁✝
e : s₁✝ ↓ₑ s₂✝
⊢ Nonempty (Grouped s₁✝ s₃✝)
no goals