case mpr =>
  intro h
  have ⟨t', mem, active⟩ := Array.any_iff_mem_where.mp h
  have ⟨_, equiv⟩ : ∃ t, t ≡ t' := ⟨_, Reaction.Trigger.Equiv.lift t'⟩
  refine .witness equiv mem ?_
  exact Activates.iff_equiv_trigger_activated equiv |>.mpr active
net✝ : Network
exec : Executable net✝
a✝ : ReactorId net✝
reaction : Class.Reaction (Path.class a✝)
⊢ Array.any reaction.val.triggers (fun x => Execution.Executable.triggers.activated exec reaction x) 0
        (Array.size reaction.val.triggers) =
      true →
    Triggers exec reaction
no goals