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

State before:
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
cpt : Component
i : Component.idType cpt
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
m₁ : Member cpt i rtr₁
m₂ : Member cpt i rtr₂
m₃ : Member cpt i rtr₃
e₁ : m₁ ∼ m₂
e₂ : m₂ ∼ m₃
⊢ m₁ ∼ m₃
Tactic:
cases m₁
State after:
case root
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
m₂ : Member Component.rtr ⊤ rtr₂
m₃ : Member Component.rtr ⊤ rtr₃
e₂ : m₂ ∼ m₃
e₁ : Member.root ∼ m₂
⊢ Member.root ∼ m₃

case strict
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
cpt : Component
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
i✝ : ID
m₂ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₂
m₃ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₃
e₂ : m₂ ∼ m₃
a✝ : StrictMember cpt i✝ rtr₁
e₁ : Member.strict a✝ ∼ m₂
⊢ Member.strict a✝ ∼ m₃

State before:
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
m₂ : Member Component.rtr ⊤ rtr₂
m₃ : Member Component.rtr ⊤ rtr₃
e₂ : m₂ ∼ m₃
e₁ : Member.root ∼ m₂
⊢ Member.root ∼ m₃
Tactic:
case root => cases m₃; exact root
State after:
no goals

State before:
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
cpt : Component
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
i✝ : ID
m₂ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₂
m₃ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₃
e₂ : m₂ ∼ m₃
a✝ : StrictMember cpt i✝ rtr₁
e₁ : Member.strict a✝ ∼ m₂
⊢ Member.strict a✝ ∼ m₃
Tactic:
case strict =>
  cases cpt <;> cases e₁ <;> cases e₂ <;> exact .strict $ StrictMember.Equivalent.trans ‹_› ‹_›
State after:
no goals

State before:
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
m₂ : Member Component.rtr ⊤ rtr₂
m₃ : Member Component.rtr ⊤ rtr₃
e₂ : m₂ ∼ m₃
e₁ : Member.root ∼ m₂
⊢ Member.root ∼ m₃
Tactic:
cases m₃
State after:
case root
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
m₂ : Member Component.rtr ⊤ rtr₂
e₁ : Member.root ∼ m₂
e₂ : m₂ ∼ Member.root
⊢ Member.root ∼ Member.root

State before:
case root
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
m₂ : Member Component.rtr ⊤ rtr₂
e₁ : Member.root ∼ m₂
e₂ : m₂ ∼ Member.root
⊢ Member.root ∼ Member.root
Tactic:
exact root
State after:
no goals

State before:
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
cpt : Component
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
i✝ : ID
m₂ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₂
m₃ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₃
e₂ : m₂ ∼ m₃
a✝ : StrictMember cpt i✝ rtr₁
e₁ : Member.strict a✝ ∼ m₂
⊢ Member.strict a✝ ∼ m₃
Tactic:
cases cpt <;> cases e₁ <;> cases e₂ <;> exact .strict $ StrictMember.Equivalent.trans ‹_› ‹_›
State after:
no goals