Theorem: Reactor.StrictMember.equiv (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
cpt : Component
i : ID
e : rtr₁ ≈ rtr₂
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
⊢ s₁ ∼ s₂
Tactic:
induction s₁ generalizing rtr₂ <;> cases s₂
State after:
case final.final
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝¹ : Component.type α cpt
a✝¹ : rtr✝{cpt}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α cpt
a✝ : rtr₂{cpt}{i} = some o✝
⊢ final a✝¹ ∼ final a✝

case final.nested
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝ : Component.type α cpt
a✝² : rtr✝{cpt}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember cpt i rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ final a✝² ∼ nested a✝ a✝¹

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

case nested.nested
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember cpt i rtr₂✝¹
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), a✝² ∼ s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember cpt i rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ nested a✝³ a✝² ∼ nested a✝ a✝¹

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝¹ : Component.type α cpt
a✝¹ : rtr✝{cpt}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α cpt
a✝ : rtr₂{cpt}{i} = some o✝
⊢ final a✝¹ ∼ final a✝
Tactic:
case final.final => constructor
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ nested h₁ s₁ ∼ nested h₂ s₂
Tactic:
case nested.nested rtr₁ j₁ _ h₁ s₁ hi j₂ _ s₂ h₂ =>
  suffices hj : j₁ = j₂ by 
    subst hj
    exact Equivalent.nested h₁ h₂ $ hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) s₂
  have hs := (nested h₁ s₁ |>.fromEquiv e).unique (nested h₂ s₂)
  simp [fromEquiv] at hs
  exact hs.left
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝ : Component.type α cpt
h₁ : rtr✝{cpt}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ final h₁ ∼ nested h₂ s₂
Tactic:
case final.nested h₁ _ _ s₂ h₂ => 
  injection (final h₁ |>.fromEquiv e).unique (nested h₂ s₂)
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
s₁ : StrictMember cpt i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α cpt
h₂ : rtr₂{cpt}{i} = some o✝
⊢ nested h₁ s₁ ∼ final h₂
Tactic:
case nested.final h₁ s₁ _ _ h₂ =>
  injection (nested h₁ s₁).unique (final h₂ |>.fromEquiv $ Reactor.Equivalent.symm e)
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝¹ : Component.type α cpt
a✝¹ : rtr✝{cpt}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α cpt
a✝ : rtr₂{cpt}{i} = some o✝
⊢ final a✝¹ ∼ final a✝
Tactic:
constructor
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ nested h₁ s₁ ∼ nested h₂ s₂
Tactic:
suffices hj : j₁ = j₂ by 
  subst hj
  exact Equivalent.nested h₁ h₂ $ hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) s₂
State after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ j₁ = j₂

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ j₁ = j₂
Tactic:
have hs := (nested h₁ s₁ |>.fromEquiv e).unique (nested h₂ s₂)
State after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : fromEquiv e (nested h₁ s₁) = nested h₂ s₂
⊢ j₁ = j₂

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : fromEquiv e (nested h₁ s₁) = nested h₂ s₂
⊢ j₁ = j₂
Tactic:
simp [fromEquiv] at hs
State after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : j₁ = j₂ ∧ Exists.choose ⋯ = rtr₂✝ ∧ HEq (fromEquiv ⋯ s₁) s₂
⊢ j₁ = j₂

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : j₁ = j₂ ∧ Exists.choose ⋯ = rtr₂✝ ∧ HEq (fromEquiv ⋯ s₁) s₂
⊢ j₁ = j₂
Tactic:
exact hs.left
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hj : j₁ = j₂
⊢ nested h₁ s₁ ∼ nested h₂ s₂
Tactic:
subst hj
State after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ nested h₁ s₁ ∼ nested h₂ s₂

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ nested h₁ s₁ ∼ nested h₂ s₂
Tactic:
exact Equivalent.nested h₁ h₂ $ hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) s₂
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝ : Component.type α cpt
h₁ : rtr✝{cpt}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ final h₁ ∼ nested h₂ s₂
Tactic:
injection (final h₁ |>.fromEquiv e).unique (nested h₂ s₂)
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
s₁ : StrictMember cpt i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α cpt
h₂ : rtr₂{cpt}{i} = some o✝
⊢ nested h₁ s₁ ∼ final h₂
Tactic:
injection (nested h₁ s₁).unique (final h₂ |>.fromEquiv $ Reactor.Equivalent.symm e)
State after:
no goals