Theorem: Execution.State.Nontrivial.equiv (ReactorModel/Execution/Theorems/State.lean)

State before:
α : Type
inst✝ : Hierarchical α
s s₁ s₂ : State α
e : s₁.rtr ≈ s₂.rtr
n : Nontrivial s₁
⊢ Nontrivial s₂
Tactic:
simp_all [Nontrivial, Equivalent.obj?_rcn_eq e]
State after:
no goals