Theorem: Reactor.Equivalent.obj?_rtr_equiv' (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
n₂ : Component.type α Component.rtr
e : rtr₁ ≈ rtr₂
h₂ : rtr₂[Component.rtr][i] = some n₂
⊢ ∃ n₁, rtr₁[Component.rtr][i] = some n₁ ∧ n₁ ≈ n₂
Tactic:
have ⟨_, h₁⟩ := obj?_some_iff e |>.mpr ⟨_, h₂⟩
State after:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
n₂ : Component.type α Component.rtr
e : rtr₁ ≈ rtr₂
h₂ : rtr₂[Component.rtr][i] = some n₂
w✝ : Component.type α Component.rtr
h₁ : rtr₁[Component.rtr][i] = some w✝
⊢ ∃ n₁, rtr₁[Component.rtr][i] = some n₁ ∧ n₁ ≈ n₂

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
n₂ : Component.type α Component.rtr
e : rtr₁ ≈ rtr₂
h₂ : rtr₂[Component.rtr][i] = some n₂
w✝ : Component.type α Component.rtr
h₁ : rtr₁[Component.rtr][i] = some w✝
⊢ ∃ n₁, rtr₁[Component.rtr][i] = some n₁ ∧ n₁ ≈ n₂
Tactic:
exact ⟨_, h₁, Equivalent.obj?_rtr_equiv e h₁ h₂⟩
State after:
no goals