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

State before:
α : Type
inst✝² : Reactor α
rtr₁ : α
β γ : Type
cpt : Component
i : ID
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
s₃ : StrictMember cpt i rtr₃
e₁ : s₁ ∼ s₂
e₂ : s₂ ∼ s₃
⊢ s₁ ∼ s₃
Tactic:
induction e₁ generalizing rtr₃ <;> cases e₂ <;> constructor <;> try assumption
State after:
case nested.nested.a
α : Type
inst✝⁴ : Reactor α
rtr₁ : α
β γ : Type
cpt : Component
i : ID
inst✝³ : Reactor β
inst✝² : Reactor γ
rtr₂ : β
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
α✝ β✝ : Type
cpt✝ : Component
i✝ j✝ : ID
inst✝¹ : Reactor α✝
inst✝ : Reactor β✝
rtr₁✝ : α✝
rtr₂✝ : β✝
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₂✝¹
a✝¹ : Equivalent s₁✝ s₂✝¹
a_ih✝ : ∀ {rtr₃ : γ} {s₃ : StrictMember cpt✝ i✝ rtr₃}, s₂✝¹ ∼ s₃ → s₁✝ ∼ s₃
rtr₃ n₂✝ : γ
s₂✝ : StrictMember cpt✝ i✝ n₂✝
h₂✝ : rtr₃{Component.rtr}{j✝} = some n₂✝
h₁✝ : rtr₂✝{Component.rtr}{j✝} = some n₂✝¹
a✝ : Equivalent s₂✝¹ s₂✝
⊢ Equivalent s₁✝ s₂✝

State before:
α : Type
inst✝⁴ : Reactor α
rtr₁ : α
β γ : Type
cpt : Component
i : ID
inst✝³ : Reactor β
inst✝² : Reactor γ
rtr₂ : β
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
α✝ β✝ : Type
cpt✝ : Component
i✝ j✝ : ID
inst✝¹ : Reactor α✝
inst✝ : Reactor β✝
rtr₁✝ : α✝
rtr₂✝ : β✝
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₂✝¹
a✝ : Equivalent s₁✝ s₂✝¹
hi₁ : ∀ {rtr₃ : γ} {s₃ : StrictMember cpt✝ i✝ rtr₃}, s₂✝¹ ∼ s₃ → s₁✝ ∼ s₃
rtr₃ n₂✝ : γ
s₂✝ : StrictMember cpt✝ i✝ n₂✝
h₂✝ : rtr₃{Component.rtr}{j✝} = some n₂✝
h₁✝ : rtr₂✝{Component.rtr}{j✝} = some n₂✝¹
hi₂ : Equivalent s₂✝¹ s₂✝
⊢ Equivalent s₁✝ s₂✝
Tactic:
case nested.nested hi₁ _ _ _ _ hi₂ => exact hi₁ hi₂
State after:
no goals

State before:
case nested.refl.a
α : Type
inst✝³ : Reactor α
rtr₁ : α
β γ : Type
cpt : Component
i : ID
inst✝² : Reactor β
inst✝¹ : Reactor γ
rtr₂ : β
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
α✝ : Type
cpt✝ : Component
i✝ j✝ : ID
inst✝ : Reactor α✝
rtr₁✝ n₁✝ : α✝
s₁✝ : StrictMember cpt✝ i✝ n₁✝
h₁✝ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
rtr₃ n₂✝ : γ
s₂✝ : StrictMember cpt✝ i✝ n₂✝
a✝ : Equivalent s₁✝ s₂✝
a_ih✝ : ∀ {rtr₃ : γ} {s₃ : StrictMember cpt✝ i✝ rtr₃}, s₂✝ ∼ s₃ → s₁✝ ∼ s₃
h₂✝ : rtr₃{Component.rtr}{j✝} = some n₂✝
⊢ Equivalent s₁✝ s₂✝
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst✝⁴ : Reactor α
rtr₁ : α
β γ : Type
cpt : Component
i : ID
inst✝³ : Reactor β
inst✝² : Reactor γ
rtr₂ : β
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
α✝ β✝ : Type
cpt✝ : Component
i✝ j✝ : ID
inst✝¹ : Reactor α✝
inst✝ : Reactor β✝
rtr₁✝ : α✝
rtr₂✝ : β✝
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₂✝¹
a✝ : Equivalent s₁✝ s₂✝¹
hi₁ : ∀ {rtr₃ : γ} {s₃ : StrictMember cpt✝ i✝ rtr₃}, s₂✝¹ ∼ s₃ → s₁✝ ∼ s₃
rtr₃ n₂✝ : γ
s₂✝ : StrictMember cpt✝ i✝ n₂✝
h₂✝ : rtr₃{Component.rtr}{j✝} = some n₂✝
h₁✝ : rtr₂✝{Component.rtr}{j✝} = some n₂✝¹
hi₂ : Equivalent s₂✝¹ s₂✝
⊢ Equivalent s₁✝ s₂✝
Tactic:
exact hi₁ hi₂
State after:
no goals