Theorem: Reactor.Member.extend_inj (ReactorModel/Objects/Reactor/Theorems/Basic.lean)

State before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
i₁ i₂ : Component.idType Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
m₁ : Member Component.rtr i₁ rtr
m₂ : Member Component.rtr i₂ rtr
h₁ : object m₁{cpt}{j} = some o₁
h₂ : object m₂{cpt}{j} = some o₂
h : extend m₁ h₁ = extend m₂ h₂
⊢ i₁ = i₂
Tactic:
cases m₁ <;> cases m₂ <;> simp [Member.extend] at h
State after:
case root.root
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : o₁ = o₂
⊢ ⊤ = ⊤

case root.strict
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.final h₁ = StrictMember.extend a✝ h₂
⊢ ⊤ =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝

case strict.root
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₁ : object (strict a✝){cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : StrictMember.extend a✝ h₁ = StrictMember.final h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝) =
    ⊤

case strict.strict
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝¹ : ID
a✝¹ : StrictMember Component.rtr i✝¹ rtr
h₁ : object (strict a✝¹){cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.extend a✝¹ h₁ = StrictMember.extend a✝ h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝¹
    | Component.rcn => i✝¹
    | Component.val v => i✝¹) =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝

State before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : o₁ = o₂
⊢ ⊤ = ⊤
Tactic:
case root.root     => rfl
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝¹ : ID
a✝¹ : StrictMember Component.rtr i✝¹ rtr
h₁ : object (strict a✝¹){cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.extend a✝¹ h₁ = StrictMember.extend a✝ h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝¹
    | Component.rcn => i✝¹
    | Component.val v => i✝¹) =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝
Tactic:
case strict.strict => simp [StrictMember.extend_inj h]
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.final h₁ = StrictMember.extend a✝ h₂
⊢ ⊤ =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝
Tactic:
case root.strict   => exact absurd h.symm $ StrictMember.extend_not_final _ _ _
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₁ : object (strict a✝){cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : StrictMember.extend a✝ h₁ = StrictMember.final h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝) =
    ⊤
Tactic:
case strict.root   => exact absurd h $ StrictMember.extend_not_final _ _ _
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : o₁ = o₂
⊢ ⊤ = ⊤
Tactic:
rfl
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝¹ : ID
a✝¹ : StrictMember Component.rtr i✝¹ rtr
h₁ : object (strict a✝¹){cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.extend a✝¹ h₁ = StrictMember.extend a✝ h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝¹
    | Component.rcn => i✝¹
    | Component.val v => i✝¹) =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝
Tactic:
simp [StrictMember.extend_inj h]
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.final h₁ = StrictMember.extend a✝ h₂
⊢ ⊤ =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝
Tactic:
exact absurd h.symm $ StrictMember.extend_not_final _ _ _
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₁ : object (strict a✝){cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : StrictMember.extend a✝ h₁ = StrictMember.final h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝) =
    ⊤
Tactic:
exact absurd h $ StrictMember.extend_not_final _ _ _
State after:
no goals