simp [*]
α : Type
inst✝ : Reactor α
rtr₁ : α
i : ID
rtr₂ : α
j : ID
c cpt : Component.Valued
e : rtr₁ ≃[Component.val cpt][i] rtr₂
h : c ≠ cpt ∨ j ≠ i
⊢ c ≠ cpt → Component.val c ≠ Component.val cpt ∨ j ≠ i
no goals