case nested.get?_rtr_some_equiv j _ _ _ _ e _ _ _ hi =>
  intro j' n₁' n₂' h₁' h₂'
  by_cases hj : j' = j <;> try subst hj
  case pos => simp_all; assumption
  case neg => 
    have := e (c := .rtr) (j := j') (.inr hj)
    simp_all
    apply Equivalent.refl
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j] rtr₂✝
a✝² : rtr₁✝{Component.rtr}{j} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
no goals