by_cases h₁ : ∃ o, rtr₁{.rcn}{i} = some o
case h
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}
case pos
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ∃ o, rtr₁{Component.rcn}{i} = some o
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}

case neg
α : Type
inst✝ : Reactor α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : ID
h₁ : ¬∃ o, rtr₁{Component.rcn}{i} = some o
⊢ rtr₂{Component.rcn}{i} = rtr₁{Component.rcn}{i}