Theorem: Reactor.StrictMember.Equivalent.to_eq (ReactorModel/Objects/Reactor/Theorems/Basic.lean)

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr : α
s₁ s₂ : StrictMember cpt i rtr
o₁✝ o₂✝ : Component.type α cpt
h₁ : rtr{cpt}{i} = some o₁✝
h₂ : rtr{cpt}{i} = some o₂✝
⊢ StrictMember.final h₁ = StrictMember.final h₂
Tactic:
simp [Option.some_inj.mp $ h₁ ▸ h₂]
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr : α
s₁ s₂ : StrictMember cpt i rtr
j✝ : ID
n₁✝ n₂✝ : α
s₁✝ : StrictMember cpt i n₁✝
s₂✝ : StrictMember cpt i n₂✝
h₁ : rtr{Component.rtr}{j✝} = some n₁✝
h₂ : rtr{Component.rtr}{j✝} = some n₂✝
e : Equivalent s₁✝ s₂✝
⊢ StrictMember.nested h₁ s₁✝ = StrictMember.nested h₂ s₂✝
Tactic:
cases Option.some_inj.mp $ h₁ ▸ h₂
State after:
case refl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr : α
s₁ s₂ : StrictMember cpt i rtr
j✝ : ID
n₁✝ : α
s₁✝ : StrictMember cpt i n₁✝
h₁ : rtr{Component.rtr}{j✝} = some n₁✝
s₂✝ : StrictMember cpt i n₁✝
h₂ : rtr{Component.rtr}{j✝} = some n₁✝
e : Equivalent s₁✝ s₂✝
⊢ StrictMember.nested h₁ s₁✝ = StrictMember.nested h₂ s₂✝

State before:
case refl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr : α
s₁ s₂ : StrictMember cpt i rtr
j✝ : ID
n₁✝ : α
s₁✝ : StrictMember cpt i n₁✝
h₁ : rtr{Component.rtr}{j✝} = some n₁✝
s₂✝ : StrictMember cpt i n₁✝
h₂ : rtr{Component.rtr}{j✝} = some n₁✝
e : Equivalent s₁✝ s₂✝
⊢ StrictMember.nested h₁ s₁✝ = StrictMember.nested h₂ s₂✝
Tactic:
simp [to_eq e]
State after:
no goals