Theorem: Reactor.Hierarchical.get?_some_rtr_eq (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
ho₁ : rtr[Component.rtr][c₁] = some con₁
ho₂ : rtr[Component.rtr][c₂] = some con₂
hc₁ : con₁{cpt}{j} = some o₁
hc₂ : con₂{cpt}{j} = some o₂
⊢ c₁ = c₂
Tactic:
have ⟨m₁⟩ := Object.iff_obj?_some.mpr ho₁
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
c₁ c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
ho₂ : rtr[Component.rtr][c₂] = some con₂
hc₂ : con₂{cpt}{j} = some o₂
m₁ : Member Component.rtr c₁ rtr
ho₁ : rtr[Component.rtr][c₁] = some (Member.object m₁)
hc₁ : Member.object m₁{cpt}{j} = some o₁
⊢ c₁ = c₂

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
c₁ c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
ho₂ : rtr[Component.rtr][c₂] = some con₂
hc₂ : con₂{cpt}{j} = some o₂
m₁ : Member Component.rtr c₁ rtr
ho₁ : rtr[Component.rtr][c₁] = some (Member.object m₁)
hc₁ : Member.object m₁{cpt}{j} = some o₁
⊢ c₁ = c₂
Tactic:
have ⟨m₂⟩ := Object.iff_obj?_some.mpr ho₂
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
c₁ c₂ : Component.idType Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
m₁ : Member Component.rtr c₁ rtr
ho₁ : rtr[Component.rtr][c₁] = some (Member.object m₁)
hc₁ : Member.object m₁{cpt}{j} = some o₁
m₂ : Member Component.rtr c₂ rtr
ho₂ : rtr[Component.rtr][c₂] = some (Member.object m₂)
hc₂ : Member.object m₂{cpt}{j} = some o₂
⊢ c₁ = c₂

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
c₁ c₂ : Component.idType Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
m₁ : Member Component.rtr c₁ rtr
ho₁ : rtr[Component.rtr][c₁] = some (Member.object m₁)
hc₁ : Member.object m₁{cpt}{j} = some o₁
m₂ : Member Component.rtr c₂ rtr
ho₂ : rtr[Component.rtr][c₂] = some (Member.object m₂)
hc₂ : Member.object m₂{cpt}{j} = some o₂
⊢ c₁ = c₂
Tactic:
exact Member.extend_inj $ (m₁.extend hc₁).unique (m₂.extend hc₂)
State after:
no goals