Theorem: Reactor.LawfulMemUpdate.equiv (ReactorModel/Objects/Reactor/Theorems/Basic.lean)

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ rtr₁ ≈ rtr₂
Tactic:
induction u <;> constructor
State after:
case final.mem_get?_iff
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}

case final.get?_rcn_some_eq
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂

case final.get?_rtr_some_equiv
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂

case nested.mem_get?_iff
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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✝ : n₁✝ ≈ n₂✝
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}

case nested.get?_rcn_some_eq
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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✝ : n₁✝ ≈ n₂✝
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂

case nested.get?_rtr_some_equiv
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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✝ : n₁✝ ≈ n₂✝
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
Tactic:
case final.mem_get?_iff e h₁ h₂ =>
  intro c j
  by_cases hc : c = cpt <;> try subst hc
  case neg => exact e.mem_iff (.inl hc)
  case pos =>
    by_cases hj : j = i <;> try subst hj
    case neg => exact e.mem_iff (.inr hj)
    case pos => simp [Partial.mem_iff, h₁, h₂]
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
Tactic:
case final.get?_rcn_some_eq e _ _ =>
  intro j _ _ h₁ h₂
  have h := e (c := .rcn) (j := j) (.inl $ by simp)
  simp_all
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
Tactic:
case final.get?_rtr_some_equiv e _ _ =>
  intro j _ _ h₁ h₂
  have h := e (c := .rtr) (j := j) (.inl $ by simp)
  simp_all
  apply Equivalent.refl
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
Tactic:
case nested.mem_get?_iff j _ _ _ _ e h₁ h₂ _ _ =>
  intro c j'
  by_cases hc : c = .rtr <;> try subst hc
  case neg => exact e.mem_iff (.inl hc)
  case pos => 
    by_cases hj : j' = j <;> try subst hj
    case neg => exact e.mem_iff (.inr hj)
    case pos => simp [Partial.mem_iff, h₁, h₂]
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
Tactic:
case nested.get?_rcn_some_eq e h₁ h₂ _ _ =>
  intro j _ _ h₁ h₂
  have h := e (c := .rcn) (j := j) (.inl $ by simp)
  simp_all
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : 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₂✝
hi : n₁✝ ≈ n₂✝
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
Tactic:
case nested.get?_rtr_some_equiv j _ _ _ _ e _ _ _ hi =>
  intro j' n₁' n₂' h₁' h₂'
  by_cases hj : j' = j <;> try subst hj
  case pos => simp_all; assumption
  case neg => 
    have := e (c := .rtr) (j := j') (.inr hj)
    simp_all
    apply Equivalent.refl
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
Tactic:
intro c j
State after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
c : Component
j : ID
⊢ j ∈ rtr₁✝{c} ↔ j ∈ rtr₂✝{c}

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
c : Component
j : ID
⊢ j ∈ rtr₁✝{c} ↔ j ∈ rtr₂✝{c}
Tactic:
by_cases hc : c = cpt <;> try subst hc
State after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}

case neg
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
c : Component
j : ID
hc : ¬c = Component.val cpt
⊢ j ∈ rtr₁✝{c} ↔ j ∈ rtr₂✝{c}

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
c : Component
j : ID
hc : ¬c = Component.val cpt
⊢ j ∈ rtr₁✝{c} ↔ j ∈ rtr₂✝{c}
Tactic:
case neg => exact e.mem_iff (.inl hc)
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
case pos =>
  by_cases hj : j = i <;> try subst hj
  case neg => exact e.mem_iff (.inr hj)
  case pos => simp [Partial.mem_iff, h₁, h₂]
State after:
no goals

State before:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
c : Component
j : ID
hc : c = Component.val cpt
⊢ j ∈ rtr₁✝{c} ↔ j ∈ rtr₂✝{c}
Tactic:
subst hc
State after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
c : Component
j : ID
hc : ¬c = Component.val cpt
⊢ j ∈ rtr₁✝{c} ↔ j ∈ rtr₂✝{c}
Tactic:
exact e.mem_iff (.inl hc)
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
by_cases hj : j = i <;> try subst hj
State after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
j : ID
e : rtr₁✝ ≃[Component.val cpt][j] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{j} = some o✝
h₂ : rtr₂✝{Component.val cpt}{j} = some v
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}

case neg
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
hj : ¬j = i
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
hj : ¬j = i
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
case neg => exact e.mem_iff (.inr hj)
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
j : ID
e : rtr₁✝ ≃[Component.val cpt][j] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{j} = some o✝
h₂ : rtr₂✝{Component.val cpt}{j} = some v
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
case pos => simp [Partial.mem_iff, h₁, h₂]
State after:
no goals

State before:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
hj : j = i
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
subst hj
State after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
j : ID
e : rtr₁✝ ≃[Component.val cpt][j] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{j} = some o✝
h₂ : rtr₂✝{Component.val cpt}{j} = some v
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
j : ID
hj : ¬j = i
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
exact e.mem_iff (.inr hj)
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
j : ID
e : rtr₁✝ ≃[Component.val cpt][j] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{j} = some o✝
h₂ : rtr₂✝{Component.val cpt}{j} = some v
⊢ j ∈ rtr₁✝{Component.val cpt} ↔ j ∈ rtr₂✝{Component.val cpt}
Tactic:
simp [Partial.mem_iff, h₁, h₂]
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
Tactic:
intro j _ _ h₁ h₂
State after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
⊢ r₁✝ = r₂✝

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
⊢ r₁✝ = r₂✝
Tactic:
have h := e (c := .rcn) (j := j) (.inl $ by simp)
State after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
h : rtr₁✝{Component.rcn}{j} = rtr₂✝{Component.rcn}{j}
⊢ r₁✝ = r₂✝

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
h : rtr₁✝{Component.rcn}{j} = rtr₂✝{Component.rcn}{j}
⊢ r₁✝ = r₂✝
Tactic:
simp_all
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
⊢ Component.rcn ≠ Component.val cpt
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
Tactic:
intro j _ _ h₁ h₂
State after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₂✝
⊢ Equivalent n₁✝ n₂✝

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₂✝
⊢ Equivalent n₁✝ n₂✝
Tactic:
have h := e (c := .rtr) (j := j) (.inl $ by simp)
State after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₂✝
h : rtr₁✝{Component.rtr}{j} = rtr₂✝{Component.rtr}{j}
⊢ Equivalent n₁✝ n₂✝

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₂✝
h : rtr₁✝{Component.rtr}{j} = rtr₂✝{Component.rtr}{j}
⊢ Equivalent n₁✝ n₂✝
Tactic:
simp_all
State after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : n₂✝ = n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₁✝
h : rtr₁✝{Component.rtr}{j} = some n₁✝
⊢ Equivalent n₁✝ n₁✝

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : n₂✝ = n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₁✝
h : rtr₁✝{Component.rtr}{j} = some n₁✝
⊢ Equivalent n₁✝ n₁✝
Tactic:
apply Equivalent.refl
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ 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
n₁✝ n₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j} = some n₂✝
⊢ Component.rtr ≠ Component.val cpt
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
⊢ ∀ (cpt : Component) (i : ID), i ∈ rtr₁✝{cpt} ↔ i ∈ rtr₂✝{cpt}
Tactic:
intro c j'
State after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
c : Component
j' : ID
⊢ j' ∈ rtr₁✝{c} ↔ j' ∈ rtr₂✝{c}

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
c : Component
j' : ID
⊢ j' ∈ rtr₁✝{c} ↔ j' ∈ rtr₂✝{c}
Tactic:
by_cases hc : c = .rtr <;> try subst hc
State after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}

case neg
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
c : Component
j' : ID
hc : ¬c = Component.rtr
⊢ j' ∈ rtr₁✝{c} ↔ j' ∈ rtr₂✝{c}

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
c : Component
j' : ID
hc : ¬c = Component.rtr
⊢ j' ∈ rtr₁✝{c} ↔ j' ∈ rtr₂✝{c}
Tactic:
case neg => exact e.mem_iff (.inl hc)
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
case pos => 
  by_cases hj : j' = j <;> try subst hj
  case neg => exact e.mem_iff (.inr hj)
  case pos => simp [Partial.mem_iff, h₁, h₂]
State after:
no goals

State before:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
c : Component
j' : ID
hc : c = Component.rtr
⊢ j' ∈ rtr₁✝{c} ↔ j' ∈ rtr₂✝{c}
Tactic:
subst hc
State after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
c : Component
j' : ID
hc : ¬c = Component.rtr
⊢ j' ∈ rtr₁✝{c} ↔ j' ∈ rtr₂✝{c}
Tactic:
exact e.mem_iff (.inl hc)
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
by_cases hj : j' = j <;> try subst hj
State after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j'} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}

case neg
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
hj : ¬j' = j
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
hj : ¬j' = j
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
case neg => exact e.mem_iff (.inr hj)
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j'} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
case pos => simp [Partial.mem_iff, h₁, h₂]
State after:
no goals

State before:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
hj : j' = j
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
subst hj
State after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j'} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
hj : ¬j' = j
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
exact e.mem_iff (.inr hj)
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j' : ID
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j'} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ j' ∈ rtr₁✝{Component.rtr} ↔ j' ∈ rtr₂✝{Component.rtr}
Tactic:
simp [Partial.mem_iff, h₁, h₂]
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
⊢ ∀ {i : ID} {r₁ r₂ : Component.type α Component.rcn},
    rtr₁✝{Component.rcn}{i} = some r₁ → rtr₂✝{Component.rcn}{i} = some r₂ → r₁ = r₂
Tactic:
intro j _ _ h₁ h₂
State after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
⊢ r₁✝ = r₂✝

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
⊢ r₁✝ = r₂✝
Tactic:
have h := e (c := .rcn) (j := j) (.inl $ by simp)
State after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
h : rtr₁✝{Component.rcn}{j} = rtr₂✝{Component.rcn}{j}
⊢ r₁✝ = r₂✝

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
h : rtr₁✝{Component.rcn}{j} = rtr₂✝{Component.rcn}{j}
⊢ r₁✝ = r₂✝
Tactic:
simp_all
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
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₂✝
a_ih✝ : n₁✝ ≈ n₂✝
j : ID
r₁✝ r₂✝ : Component.type α Component.rcn
h₁ : rtr₁✝{Component.rcn}{j} = some r₁✝
h₂ : rtr₂✝{Component.rcn}{j} = some r₂✝
⊢ Component.rcn ≠ Component.rtr
Tactic:
simp
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : 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₂✝
hi : n₁✝ ≈ n₂✝
⊢ ∀ {i : ID} {n₁ n₂ : Component.type α Component.rtr},
    rtr₁✝{Component.rtr}{i} = some n₁ → rtr₂✝{Component.rtr}{i} = some n₂ → Equivalent n₁ n₂
Tactic:
intro j' n₁' n₂' h₁' h₂'
State after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : 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₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
⊢ Equivalent n₁' n₂'

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : 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₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
⊢ Equivalent n₁' n₂'
Tactic:
by_cases hj : j' = j <;> try subst hj
State after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ Equivalent n₁' n₂'

case neg
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : 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₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
hj : ¬j' = j
⊢ Equivalent n₁' n₂'

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ Equivalent n₁' n₂'
Tactic:
case pos => simp_all; assumption
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : 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₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
hj : ¬j' = j
⊢ Equivalent n₁' n₂'
Tactic:
case neg => 
  have := e (c := .rtr) (j := j') (.inr hj)
  simp_all
  apply Equivalent.refl
State after:
no goals

State before:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : 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₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
hj : j' = j
⊢ Equivalent n₁' n₂'
Tactic:
subst hj
State after:
case pos
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ Equivalent n₁' n₂'

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂✝{Component.rtr}{j'} = some n₂✝
⊢ Equivalent n₁' n₂'
Tactic:
simp_all
State after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
hi : n₁' ≈ n₂'
h₁' : n₁✝ = n₁'
h₂' : n₂✝ = n₂'
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁'
a✝ : rtr₂✝{Component.rtr}{j'} = some n₂'
⊢ Equivalent n₁' n₂'

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : LawfulMemUpdate cpt i v n₁✝ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
hi : n₁' ≈ n₂'
h₁' : n₁✝ = n₁'
h₂' : n₂✝ = n₂'
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁'
a✝ : rtr₂✝{Component.rtr}{j'} = some n₂'
⊢ Equivalent n₁' n₂'
Tactic:
assumption
State after:
no goals

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : 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₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
hj : ¬j' = j
⊢ Equivalent n₁' n₂'
Tactic:
have := e (c := .rtr) (j := j') (.inr hj)
State after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : 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₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
hj : ¬j' = j
this : rtr₁✝{Component.rtr}{j'} = rtr₂✝{Component.rtr}{j'}
⊢ Equivalent n₁' n₂'

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : 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₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : rtr₁✝{Component.rtr}{j'} = some n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₂'
hj : ¬j' = j
this : rtr₁✝{Component.rtr}{j'} = rtr₂✝{Component.rtr}{j'}
⊢ Equivalent n₁' n₂'
Tactic:
simp_all
State after:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : 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₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : n₂' = n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₁'
hj : ¬j' = j
this : rtr₁✝{Component.rtr}{j'} = some n₁'
⊢ Equivalent n₁' n₁'

State before:
α : Type
inst✝ : Reactor α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁ : α
j : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
e : 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₂✝
hi : n₁✝ ≈ n₂✝
j' : ID
n₁' n₂' : Component.type α Component.rtr
h₁' : n₂' = n₁'
h₂' : rtr₂✝{Component.rtr}{j'} = some n₁'
hj : ¬j' = j
this : rtr₁✝{Component.rtr}{j'} = some n₁'
⊢ Equivalent n₁' n₁'
Tactic:
apply Equivalent.refl
State after:
no goals