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₁ n₂ : Component.type α Component.rtr
e : rtr₁ ≈ rtr₂
h₁ : rtr₁[Component.rtr][i] = some n₁
h₂ : rtr₂[Component.rtr][i] = some n₂
⊢ n₁ ≈ n₂
Tactic:
have ⟨m₁⟩ := Object.iff_obj?_some.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₂
m₁ : Member Component.rtr i rtr₁
h₁ : rtr₁[Component.rtr][i] = some (Member.object m₁)
⊢ Member.object m₁ ≈ 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₂
m₁ : Member Component.rtr i rtr₁
h₁ : rtr₁[Component.rtr][i] = some (Member.object m₁)
⊢ Member.object m₁ ≈ n₂
Tactic:
have ⟨m₂⟩ := Object.iff_obj?_some.mpr h₂
State after:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
e : rtr₁ ≈ rtr₂
m₁ : Member Component.rtr i rtr₁
h₁ : rtr₁[Component.rtr][i] = some (Member.object m₁)
m₂ : Member Component.rtr i rtr₂
h₂ : rtr₂[Component.rtr][i] = some (Member.object m₂)
⊢ Member.object m₁ ≈ Member.object m₂

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
e : rtr₁ ≈ rtr₂
m₁ : Member Component.rtr i rtr₁
h₁ : rtr₁[Component.rtr][i] = some (Member.object m₁)
m₂ : Member Component.rtr i rtr₂
h₂ : rtr₂[Component.rtr][i] = some (Member.object m₂)
⊢ Member.object m₁ ≈ Member.object m₂
Tactic:
exact m₁.rtr_equiv e m₂
State after:
no goals