Theorem: Reactor.RootEqualUpTo.valued (ReactorModel/Objects/Reactor/Theorems/Basic.lean)

State before:
α : 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
Tactic:
simp [*]
State after:
no goals