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

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
s : StrictMember c j rtr₂
⊢ s ∼ StrictMember.fromLawfulMemUpdate s u
Tactic:
induction u <;> cases s <;> (simp [StrictMember.fromLawfulMemUpdate]; try exact final _ _)
State after:
case final.nested
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
rtr₁✝ rtr₂✝¹ : α
o✝ : Component.type α (Component.val cpt)
a✝⁴ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝¹
a✝³ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝² : rtr₂✝¹{Component.val cpt}{i} = some v
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember c j rtr₂✝
a✝ : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested a✝ a✝¹ ∼ StrictMember.nested ⋯ a✝¹

case nested.nested
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝¹ : ID
rtr₁✝ rtr₂✝¹ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝⁵ : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝¹
a✝⁴ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝
a✝³ : rtr₂✝¹{Component.rtr}{j✝¹} = some n₂✝
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝²
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember c j rtr₂✝
a✝ : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested a✝ a✝¹ ∼
    if hj : j✝ = j✝¹ then StrictMember.nested a✝⁴ (StrictMember.fromLawfulMemUpdate (⋯ ▸ a✝¹) a✝²)
    else StrictMember.nested ⋯ a✝¹

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
rtr₁✝ rtr₂✝¹ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝¹
a✝² : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂✝¹{Component.val cpt}{i} = some v
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝ : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested hn a✝ ∼ StrictMember.nested ⋯ a✝
Tactic:
case final.nested e _ _ _ _ _ hn => exact nested hn (e (c := .rtr) (.inl $ by simp) ▸ hn) (refl _)
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝¹ : ID
rtr₁✝ rtr₂✝¹ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝¹
h₁ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝
h₂ : rtr₂✝¹{Component.rtr}{j✝¹} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested hn m ∼
    if hj : j✝ = j✝¹ then StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)
    else StrictMember.nested ⋯ m
Tactic:
case nested.nested e h₁ h₂ _ hi _ _ m hn =>
  split
  case inl hj => cases hj; cases Option.some_inj.mp $ h₂ ▸ hn; exact nested hn h₁ (hi m)
  case inr hj => exact nested hn (hn ▸ e (.inr hj)) (refl _)
State after:
no goals

State before:
case nested.nested
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝¹ : ID
rtr₁✝ rtr₂✝¹ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝⁵ : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝¹
a✝⁴ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝
a✝³ : rtr₂✝¹{Component.rtr}{j✝¹} = some n₂✝
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝²
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember c j rtr₂✝
a✝ : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested a✝ a✝¹ ∼
    StrictMember.fromLawfulMemUpdate (StrictMember.nested a✝ a✝¹) (LawfulMemUpdate.nested a✝⁵ a✝⁴ a✝³ a✝²)
Tactic:
simp [StrictMember.fromLawfulMemUpdate]
State after:
case nested.nested
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝¹ : ID
rtr₁✝ rtr₂✝¹ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝⁵ : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝¹
a✝⁴ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝
a✝³ : rtr₂✝¹{Component.rtr}{j✝¹} = some n₂✝
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝²
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember c j rtr₂✝
a✝ : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested a✝ a✝¹ ∼
    if hj : j✝ = j✝¹ then StrictMember.nested a✝⁴ (StrictMember.fromLawfulMemUpdate (⋯ ▸ a✝¹) a✝²)
    else StrictMember.nested ⋯ a✝¹

State before:
case nested.final
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝⁴ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
a✝³ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝² : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝¹ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝¹
o✝ : Component.type α c
a✝ : rtr₂✝{c}{j} = some o✝
⊢ StrictMember.final a✝ ∼ StrictMember.final ⋯
Tactic:
try exact final _ _
State after:
no goals

State before:
case nested.final
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝⁴ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
a✝³ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝² : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝¹ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝¹
o✝ : Component.type α c
a✝ : rtr₂✝{c}{j} = some o✝
⊢ StrictMember.final a✝ ∼ StrictMember.final ⋯
Tactic:
exact final _ _
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
rtr₁✝ rtr₂✝¹ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝¹
a✝² : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂✝¹{Component.val cpt}{i} = some v
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝ : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested hn a✝ ∼ StrictMember.nested ⋯ a✝
Tactic:
exact nested hn (e (c := .rtr) (.inl $ by simp) ▸ hn) (refl _)
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
rtr₁✝ rtr₂✝¹ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝¹
a✝² : rtr₁✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂✝¹{Component.val cpt}{i} = some v
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝ : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ Component.rtr ≠ Component.val cpt
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝¹ : ID
rtr₁✝ rtr₂✝¹ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝¹
h₁ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝
h₂ : rtr₂✝¹{Component.rtr}{j✝¹} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested hn m ∼
    if hj : j✝ = j✝¹ then StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)
    else StrictMember.nested ⋯ m
Tactic:
split
State after:
case inl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝¹ : ID
rtr₁✝ rtr₂✝¹ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝¹
h₁ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝
h₂ : rtr₂✝¹{Component.rtr}{j✝¹} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
h✝ : j✝ = j✝¹
⊢ StrictMember.nested hn m ∼ StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)

case inr
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝¹ : ID
rtr₁✝ rtr₂✝¹ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝¹
h₁ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝
h₂ : rtr₂✝¹{Component.rtr}{j✝¹} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
h✝ : ¬j✝ = j✝¹
⊢ StrictMember.nested hn m ∼ StrictMember.nested ⋯ m

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝¹ : ID
rtr₁✝ rtr₂✝¹ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝¹
h₁ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝
h₂ : rtr₂✝¹{Component.rtr}{j✝¹} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
hj : j✝ = j✝¹
⊢ StrictMember.nested hn m ∼ StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)
Tactic:
case inl hj => cases hj; cases Option.some_inj.mp $ h₂ ▸ hn; exact nested hn h₁ (hi m)
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝¹ : ID
rtr₁✝ rtr₂✝¹ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝¹
h₁ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝
h₂ : rtr₂✝¹{Component.rtr}{j✝¹} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
hj : ¬j✝ = j✝¹
⊢ StrictMember.nested hn m ∼ StrictMember.nested ⋯ m
Tactic:
case inr hj => exact nested hn (hn ▸ e (.inr hj)) (refl _)
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝¹ : ID
rtr₁✝ rtr₂✝¹ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝¹
h₁ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝
h₂ : rtr₂✝¹{Component.rtr}{j✝¹} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
hj : j✝ = j✝¹
⊢ StrictMember.nested hn m ∼ StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)
Tactic:
cases hj
State after:
case refl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝ : ID
rtr₁✝ rtr₂✝¹ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝¹
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝¹{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested hn m ∼ StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)

State before:
case refl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝ : ID
rtr₁✝ rtr₂✝¹ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝¹
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝¹{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested hn m ∼ StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)
Tactic:
cases Option.some_inj.mp $ h₂ ▸ hn
State after:
case refl.refl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
m : StrictMember c j n₂✝
hn : rtr₂✝{Component.rtr}{j✝} = some n₂✝
⊢ StrictMember.nested hn m ∼ StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)

State before:
case refl.refl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
m : StrictMember c j n₂✝
hn : rtr₂✝{Component.rtr}{j✝} = some n₂✝
⊢ StrictMember.nested hn m ∼ StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)
Tactic:
exact nested hn h₁ (hi m)
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j j✝¹ : ID
rtr₁✝ rtr₂✝¹ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : rtr₁✝ ≃[Component.rtr][j✝¹] rtr₂✝¹
h₁ : rtr₁✝{Component.rtr}{j✝¹} = some n₁✝
h₂ : rtr₂✝¹{Component.rtr}{j✝¹} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∀ (s : StrictMember c j n₂✝), s ∼ StrictMember.fromLawfulMemUpdate s a✝
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
hj : ¬j✝ = j✝¹
⊢ StrictMember.nested hn m ∼ StrictMember.nested ⋯ m
Tactic:
exact nested hn (hn ▸ e (.inr hj)) (refl _)
State after:
no goals