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

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
⊢ rtr₁[Component.rcn] = rtr₂[Component.rcn]
Tactic:
funext i
State after:
case h
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
⊢ rtr₁[Component.rcn][i] = rtr₂[Component.rcn][i]

State before:
case h
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
⊢ rtr₁[Component.rcn][i] = rtr₂[Component.rcn][i]
Tactic:
cases ho₁ : rtr₁[.rcn][i]
State after:
case h.none
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
ho₁ : rtr₁[Component.rcn][i] = none
⊢ none = rtr₂[Component.rcn][i]

case h.some
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
val✝ : Component.type α Component.rcn
ho₁ : rtr₁[Component.rcn][i] = some val✝
⊢ some val✝ = rtr₂[Component.rcn][i]

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
ho₁ : rtr₁[Component.rcn][i] = none
⊢ none = rtr₂[Component.rcn][i]
Tactic:
case none => simp [obj?_none_iff e |>.mp ho₁]
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
val✝ : Component.type α Component.rcn
ho₁ : rtr₁[Component.rcn][i] = some val✝
⊢ some val✝ = rtr₂[Component.rcn][i]
Tactic:
case some =>
  have ⟨_, ho₂⟩ := obj?_some_iff e |>.mp ⟨_, ho₁⟩ 
  have ⟨m₁⟩ := Object.iff_obj?_some.mpr ho₁
  have ⟨m₂⟩ := Object.iff_obj?_some.mpr ho₂
  simp [ho₂, m₁.equiv_rcn_eq e m₂]
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
ho₁ : rtr₁[Component.rcn][i] = none
⊢ none = rtr₂[Component.rcn][i]
Tactic:
simp [obj?_none_iff e |>.mp ho₁]
State after:
no goals

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

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
val✝ : Component.type α Component.rcn
ho₁ : rtr₁[Component.rcn][i] = some val✝
w✝ : Component.type α Component.rcn
ho₂ : rtr₂[Component.rcn][i] = some w✝
⊢ some val✝ = rtr₂[Component.rcn][i]
Tactic:
have ⟨m₁⟩ := Object.iff_obj?_some.mpr ho₁
State after:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
w✝ : Component.type α Component.rcn
ho₂ : rtr₂[Component.rcn][i] = some w✝
m₁ : Member Component.rcn i rtr₁
ho₁ : rtr₁[Component.rcn][i] = some (Member.object m₁)
⊢ some (Member.object m₁) = rtr₂[Component.rcn][i]

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
w✝ : Component.type α Component.rcn
ho₂ : rtr₂[Component.rcn][i] = some w✝
m₁ : Member Component.rcn i rtr₁
ho₁ : rtr₁[Component.rcn][i] = some (Member.object m₁)
⊢ some (Member.object m₁) = rtr₂[Component.rcn][i]
Tactic:
have ⟨m₂⟩ := Object.iff_obj?_some.mpr ho₂
State after:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
m₁ : Member Component.rcn i rtr₁
ho₁ : rtr₁[Component.rcn][i] = some (Member.object m₁)
m₂ : Member Component.rcn i rtr₂
ho₂ : rtr₂[Component.rcn][i] = some (Member.object m₂)
⊢ some (Member.object m₁) = rtr₂[Component.rcn][i]

State before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
m₁ : Member Component.rcn i rtr₁
ho₁ : rtr₁[Component.rcn][i] = some (Member.object m₁)
m₂ : Member Component.rcn i rtr₂
ho₂ : rtr₂[Component.rcn][i] = some (Member.object m₂)
⊢ some (Member.object m₁) = rtr₂[Component.rcn][i]
Tactic:
simp [ho₂, m₁.equiv_rcn_eq e m₂]
State after:
no goals