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

State before:
α : Type
inst✝¹ : Reactor α
rtr₁ : α
β : Type
cpt : Component
i : ID
inst✝ : Reactor β
rtr₂ : β
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
e : s₁ ∼ s₂
⊢ s₂ ∼ s₁
Tactic:
induction e <;> constructor
State after:
case nested.a
α : Type
inst✝³ : Reactor α
rtr₁ : α
β : Type
cpt : Component
i : ID
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✝ : s₂✝ ∼ s₁✝
⊢ Equivalent s₂✝ s₁✝

State before:
case nested.a
α : Type
inst✝³ : Reactor α
rtr₁ : α
β : Type
cpt : Component
i : ID
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✝ : s₂✝ ∼ s₁✝
⊢ Equivalent s₂✝ s₁✝
Tactic:
assumption
State after:
no goals