Theorem: Reactor.Equivalent.get?_rcn_some_eq (ReactorModel/Objects/Reactor/Theorems/Basic.lean)

State before:
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
i : ID
r₁ r₂ : Component.type α Component.rcn
⊢ rtr₁{Component.rcn}{i} = some r₁ → rtr₁{Component.rcn}{i} = some r₂ → r₁ = r₂
Tactic:
simp_all
State after:
no goals