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

State before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ i₂ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
s₁ : StrictMember Component.rtr i₁ rtr
s₂ : StrictMember Component.rtr i₂ rtr
h₁ : object s₁{cpt}{j} = some o₁
h₂ : object s₂{cpt}{j} = some o₂
h : extend s₁ h₁ = extend s₂ h₂
⊢ i₁ = i₂
Tactic:
induction s₁ generalizing i₂ <;> cases s₂
State after:
case final.final
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝¹ : Component.type α Component.rtr
a✝¹ : rtr✝{Component.rtr}{i₁} = some o✝¹
i₂ : ID
h₁ : object (final a✝¹){cpt}{j} = some o₁
o✝ : Component.type α Component.rtr
a✝ : rtr✝{Component.rtr}{i₂} = some o✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : extend (final a✝¹) h₁ = extend (final a✝) h₂
⊢ i₁ = i₂

case final.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝ : Component.type α Component.rtr
a✝² : rtr✝{Component.rtr}{i₁} = some o✝
i₂ : ID
h₁ : object (final a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : extend (final a✝²) h₁ = extend (nested a✝ a✝¹) h₂
⊢ i₁ = i₂

case nested.final
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember Component.rtr i₁ rtr₂✝
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝¹{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝¹ h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝² a✝¹){cpt}{j} = some o₁
o✝ : Component.type α Component.rtr
a✝ : rtr₁✝{Component.rtr}{i₂} = some o✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : extend (nested a✝² a✝¹) h₁ = extend (final a✝) h₂
⊢ i₁ = i₂

case nested.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : extend (nested a✝³ a✝²) h₁ = extend (nested a✝ a✝¹) h₂
⊢ i₁ = i₂

State before:
case final.final
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝¹ : Component.type α Component.rtr
a✝¹ : rtr✝{Component.rtr}{i₁} = some o✝¹
i₂ : ID
h₁ : object (final a✝¹){cpt}{j} = some o₁
o✝ : Component.type α Component.rtr
a✝ : rtr✝{Component.rtr}{i₂} = some o✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : extend (final a✝¹) h₁ = extend (final a✝) h₂
⊢ i₁ = i₂

case final.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝ : Component.type α Component.rtr
a✝² : rtr✝{Component.rtr}{i₁} = some o✝
i₂ : ID
h₁ : object (final a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : extend (final a✝²) h₁ = extend (nested a✝ a✝¹) h₂
⊢ i₁ = i₂

case nested.final
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember Component.rtr i₁ rtr₂✝
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝¹{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝¹ h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝² a✝¹){cpt}{j} = some o₁
o✝ : Component.type α Component.rtr
a✝ : rtr₁✝{Component.rtr}{i₂} = some o✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : extend (nested a✝² a✝¹) h₁ = extend (final a✝) h₂
⊢ i₁ = i₂

case nested.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : extend (nested a✝³ a✝²) h₁ = extend (nested a✝ a✝¹) h₂
⊢ i₁ = i₂
Tactic:
all_goals simp [extend] at h; obtain ⟨hj, hr, h⟩ := h; subst hj hr
State after:
case final.final.intro.intro
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝ : Component.type α Component.rtr
a✝¹ : rtr✝{Component.rtr}{i₁} = some o✝
h₁ : object (final a✝¹){cpt}{j} = some o₁
a✝ : rtr✝{Component.rtr}{i₁} = some o✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : HEq (final h₁) (final h₂)
⊢ i₁ = i₁

case final.nested.intro.intro
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝ : Component.type α Component.rtr
a✝² : rtr✝{Component.rtr}{i₁} = some o✝
i₂ : ID
h₁ : object (final a✝²){cpt}{j} = some o₁
a✝¹ : StrictMember Component.rtr i₂ o✝
a✝ : rtr✝{Component.rtr}{i₁} = some o✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : HEq (final h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂

case nested.final.intro.intro
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember Component.rtr i₁ rtr₂✝
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝¹{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝¹ h₁ = extend s₂ h₂ → i₁ = i₂
h₁ : object (nested a✝² a✝¹){cpt}{j} = some o₁
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : HEq (extend a✝¹ h₁) (final h₂)
⊢ i₁ = j✝

case nested.nested.intro.intro
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝² : StrictMember Component.rtr i₁ rtr₂✝
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂

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

State before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝² : StrictMember Component.rtr i₁ rtr₂✝
hi :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Tactic:
case nested.nested hi _ _ => exact hi $ eq_of_heq h
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝ : Component.type α Component.rtr
a✝² : rtr✝{Component.rtr}{i₁} = some o✝
i₂ : ID
h₁ : object (final a✝²){cpt}{j} = some o₁
a✝¹ : StrictMember Component.rtr i₂ o✝
a✝ : rtr✝{Component.rtr}{i₁} = some o✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : HEq (final h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Tactic:
case final.nested => exact absurd (eq_of_heq h).symm $ StrictMember.extend_not_final _ _ _
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember Component.rtr i₁ rtr₂✝
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝¹{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝¹ h₁ = extend s₂ h₂ → i₁ = i₂
h₁ : object (nested a✝² a✝¹){cpt}{j} = some o₁
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : HEq (extend a✝¹ h₁) (final h₂)
⊢ i₁ = j✝
Tactic:
case nested.final => exact absurd (eq_of_heq h) $ StrictMember.extend_not_final _ _ _
State after:
no goals

State before:
case nested.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : extend (nested a✝³ a✝²) h₁ = extend (nested a✝ a✝¹) h₂
⊢ i₁ = i₂
Tactic:
simp [extend] at h
State after:
case nested.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : j✝¹ = j✝ ∧ rtr₂✝¹ = rtr₂✝ ∧ HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂

State before:
case nested.nested
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : j✝¹ = j✝ ∧ rtr₂✝¹ = rtr₂✝ ∧ HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Tactic:
obtain ⟨hj, hr, h⟩ := h
State after:
case nested.nested.intro.intro
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
hj : j✝¹ = j✝
hr : rtr₂✝¹ = rtr₂✝
h : HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂

State before:
case nested.nested.intro.intro
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
hj : j✝¹ = j✝
hr : rtr₂✝¹ = rtr₂✝
h : HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Tactic:
subst hj hr
State after:
case nested.nested.intro.intro
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝² : StrictMember Component.rtr i₁ rtr₂✝
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂

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

State before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝² : StrictMember Component.rtr i₁ rtr₂✝
hi :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Tactic:
exact hi $ eq_of_heq h
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝ : Component.type α Component.rtr
a✝² : rtr✝{Component.rtr}{i₁} = some o✝
i₂ : ID
h₁ : object (final a✝²){cpt}{j} = some o₁
a✝¹ : StrictMember Component.rtr i₂ o✝
a✝ : rtr✝{Component.rtr}{i₁} = some o✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : HEq (final h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Tactic:
exact absurd (eq_of_heq h).symm $ StrictMember.extend_not_final _ _ _
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember Component.rtr i₁ rtr₂✝
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝¹{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝¹ h₁ = extend s₂ h₂ → i₁ = i₂
h₁ : object (nested a✝² a✝¹){cpt}{j} = some o₁
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : HEq (extend a✝¹ h₁) (final h₂)
⊢ i₁ = j✝
Tactic:
exact absurd (eq_of_heq h) $ StrictMember.extend_not_final _ _ _
State after:
no goals