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

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

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

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

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

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝¹ : Component.type α Component.rcn
h₁ : rtr✝{Component.rcn}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α Component.rcn
h₂ : rtr₂{Component.rcn}{i} = some o✝
⊢ object (final h₁) = object (final h₂)
Tactic:
case final.final h₁ _ h₂ => exact Equivalent.get?_rcn_some_eq e h₁ h₂
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ object (nested h₁ s₁) = object (nested h₂ s₂)
Tactic:
case nested.nested j₁ _ h₁ s₁ hi j₂ _ s₂ h₂ => 
  suffices hj : j₁ = j₂ by subst hj; exact hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) _ 
  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₁ : α
i : ID
rtr✝ : α
o✝ : Component.type α Component.rcn
h₁ : rtr✝{Component.rcn}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ object (final h₁) = object (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₁ : α
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
s₁ : StrictMember Component.rcn i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α Component.rcn
h₂ : rtr₂{Component.rcn}{i} = some o✝
⊢ object (nested h₁ s₁) = object (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₁ : α
i : ID
rtr✝ : α
o✝¹ : Component.type α Component.rcn
h₁ : rtr✝{Component.rcn}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α Component.rcn
h₂ : rtr₂{Component.rcn}{i} = some o✝
⊢ object (final h₁) = object (final h₂)
Tactic:
exact Equivalent.get?_rcn_some_eq e h₁ h₂
State after:
no goals

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

State before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn 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₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn 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₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn 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₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn 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₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn 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₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hj : j₁ = j₂
⊢ object (nested h₁ s₁) = object (nested h₂ s₂)
Tactic:
subst hj
State after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ object (nested h₁ s₁) = object (nested h₂ s₂)

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

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

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