internlm/Lean-Github huggingface dataset:
Theorem: Reactor.Equivalent.obj?_rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
n₂ : Component.type α Component.rtr
e : rtr₁ ≈ rtr₂
h₂ : rtr₂[Component.rtr][i] = some n₂
m₁ : Member Component.rtr i rtr₁
h₁ : rtr₁[Component.rtr][i] = some (Member.object m₁)
⊢ Member.object m₁ ≈ n₂
Tactic:
have ⟨m₂⟩ := Object.iff_obj?_some.mpr h₂
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
e : rtr₁ ≈ rtr₂
m₁ : Member Component.rtr i rtr₁
h₁ : rtr₁[Component.rtr][i] = some (Member.object m₁)
m₂ : Member Component.rtr i rtr₂
h₂ : rtr₂[Component.rtr][i] = some (Member.object m₂)
⊢ Member.object m₁ ≈ Member.object m₂
Theorem: Reactor.Equivalent.obj?_rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
e : rtr₁ ≈ rtr₂
m₁ : Member Component.rtr i rtr₁
h₁ : rtr₁[Component.rtr][i] = some (Member.object m₁)
m₂ : Member Component.rtr i rtr₂
h₂ : rtr₂[Component.rtr][i] = some (Member.object m₂)
⊢ Member.object m₁ ≈ Member.object m₂
Tactic:
exact m₁.rtr_equiv e m₂
Proof state after:
no goals
Theorem: Reactor.Equivalent.obj?_rtr_equiv'
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
n₂ : Component.type α Component.rtr
e : rtr₁ ≈ rtr₂
h₂ : rtr₂[Component.rtr][i] = some n₂
⊢ ∃ n₁, rtr₁[Component.rtr][i] = some n₁ ∧ n₁ ≈ n₂
Tactic:
have ⟨_, h₁⟩ := obj?_some_iff e |>.mpr ⟨_, h₂⟩
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
n₂ : Component.type α Component.rtr
e : rtr₁ ≈ rtr₂
h₂ : rtr₂[Component.rtr][i] = some n₂
w✝ : Component.type α Component.rtr
h₁ : rtr₁[Component.rtr][i] = some w✝
⊢ ∃ n₁, rtr₁[Component.rtr][i] = some n₁ ∧ n₁ ≈ n₂
Theorem: Reactor.Equivalent.obj?_rtr_equiv'
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
n₂ : Component.type α Component.rtr
e : rtr₁ ≈ rtr₂
h₂ : rtr₂[Component.rtr][i] = some n₂
w✝ : Component.type α Component.rtr
h₁ : rtr₁[Component.rtr][i] = some w✝
⊢ ∃ n₁, rtr₁[Component.rtr][i] = some n₁ ∧ n₁ ≈ n₂
Tactic:
exact ⟨_, h₁, Equivalent.obj?_rtr_equiv e h₁ h₂⟩
Proof state after:
no goals
Theorem: Reactor.Equivalent.obj?_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
⊢ rtr₁[Component.rcn] = rtr₂[Component.rcn]
Tactic:
funext i
Proof state after:
case h
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
⊢ rtr₁[Component.rcn][i] = rtr₂[Component.rcn][i]
Theorem: Reactor.Equivalent.obj?_rcn_eq
Proof state before:
case h
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
⊢ rtr₁[Component.rcn][i] = rtr₂[Component.rcn][i]
Tactic:
cases ho₁ : rtr₁[.rcn][i]
Proof state after:
case h.none
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
ho₁ : rtr₁[Component.rcn][i] = none
⊢ none = rtr₂[Component.rcn][i]

case h.some
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
val✝ : Component.type α Component.rcn
ho₁ : rtr₁[Component.rcn][i] = some val✝
⊢ some val✝ = rtr₂[Component.rcn][i]
Theorem: Reactor.Equivalent.obj?_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
ho₁ : rtr₁[Component.rcn][i] = none
⊢ none = rtr₂[Component.rcn][i]
Tactic:
case none => simp [obj?_none_iff e |>.mp ho₁]
Proof state after:
no goals
Theorem: Reactor.Equivalent.obj?_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
val✝ : Component.type α Component.rcn
ho₁ : rtr₁[Component.rcn][i] = some val✝
⊢ some val✝ = rtr₂[Component.rcn][i]
Tactic:
case some =>
  have ⟨_, ho₂⟩ := obj?_some_iff e |>.mp ⟨_, ho₁⟩ 
  have ⟨m₁⟩ := Object.iff_obj?_some.mpr ho₁
  have ⟨m₂⟩ := Object.iff_obj?_some.mpr ho₂
  simp [ho₂, m₁.equiv_rcn_eq e m₂]
Proof state after:
no goals
Theorem: Reactor.Equivalent.obj?_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
ho₁ : rtr₁[Component.rcn][i] = none
⊢ none = rtr₂[Component.rcn][i]
Tactic:
simp [obj?_none_iff e |>.mp ho₁]
Proof state after:
no goals
Theorem: Reactor.Equivalent.obj?_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
val✝ : Component.type α Component.rcn
ho₁ : rtr₁[Component.rcn][i] = some val✝
⊢ some val✝ = rtr₂[Component.rcn][i]
Tactic:
have ⟨_, ho₂⟩ := obj?_some_iff e |>.mp ⟨_, ho₁⟩
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
val✝ : Component.type α Component.rcn
ho₁ : rtr₁[Component.rcn][i] = some val✝
w✝ : Component.type α Component.rcn
ho₂ : rtr₂[Component.rcn][i] = some w✝
⊢ some val✝ = rtr₂[Component.rcn][i]
Theorem: Reactor.Equivalent.obj?_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
val✝ : Component.type α Component.rcn
ho₁ : rtr₁[Component.rcn][i] = some val✝
w✝ : Component.type α Component.rcn
ho₂ : rtr₂[Component.rcn][i] = some w✝
⊢ some val✝ = rtr₂[Component.rcn][i]
Tactic:
have ⟨m₁⟩ := Object.iff_obj?_some.mpr ho₁
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
w✝ : Component.type α Component.rcn
ho₂ : rtr₂[Component.rcn][i] = some w✝
m₁ : Member Component.rcn i rtr₁
ho₁ : rtr₁[Component.rcn][i] = some (Member.object m₁)
⊢ some (Member.object m₁) = rtr₂[Component.rcn][i]
Theorem: Reactor.Equivalent.obj?_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
w✝ : Component.type α Component.rcn
ho₂ : rtr₂[Component.rcn][i] = some w✝
m₁ : Member Component.rcn i rtr₁
ho₁ : rtr₁[Component.rcn][i] = some (Member.object m₁)
⊢ some (Member.object m₁) = rtr₂[Component.rcn][i]
Tactic:
have ⟨m₂⟩ := Object.iff_obj?_some.mpr ho₂
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
m₁ : Member Component.rcn i rtr₁
ho₁ : rtr₁[Component.rcn][i] = some (Member.object m₁)
m₂ : Member Component.rcn i rtr₂
ho₂ : rtr₂[Component.rcn][i] = some (Member.object m₂)
⊢ some (Member.object m₁) = rtr₂[Component.rcn][i]
Theorem: Reactor.Equivalent.obj?_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
e : rtr₁ ≈ rtr₂
i : Component.idType Component.rcn
m₁ : Member Component.rcn i rtr₁
ho₁ : rtr₁[Component.rcn][i] = some (Member.object m₁)
m₂ : Member Component.rcn i rtr₂
ho₂ : rtr₂[Component.rcn][i] = some (Member.object m₂)
⊢ some (Member.object m₁) = rtr₂[Component.rcn][i]
Tactic:
simp [ho₂, m₁.equiv_rcn_eq e m₂]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_some₁
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ ∃ o, rtr₁[Component.val cpt][i] = some o
Tactic:
induction u
Proof state after:
case final
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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
⊢ ∃ o, rtr₁✝[Component.val cpt][i] = some o

case nested
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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✝ : ∃ o, n₁✝[Component.val cpt][i] = some o
⊢ ∃ o, rtr₁✝[Component.val cpt][i] = some o
Theorem: Reactor.LawfulMemUpdate.obj?_some₁
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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
⊢ ∃ o, rtr₁✝[Component.val cpt][i] = some o
Tactic:
case final           => exact ⟨_, get?_some_to_obj?_some ‹_›⟩
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_some₁
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∃ o, n₁✝[Component.val cpt][i] = some o
⊢ ∃ o, rtr₁✝[Component.val cpt][i] = some o
Tactic:
case nested h _ _ hi => exact ⟨_, obj?_some_nested h hi.choose_spec⟩
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_some₁
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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
⊢ ∃ o, rtr₁✝[Component.val cpt][i] = some o
Tactic:
exact ⟨_, get?_some_to_obj?_some ‹_›⟩
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_some₁
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∃ o, n₁✝[Component.val cpt][i] = some o
⊢ ∃ o, rtr₁✝[Component.val cpt][i] = some o
Tactic:
exact ⟨_, obj?_some_nested h hi.choose_spec⟩
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_some₂
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ ∃ o, rtr₂[Component.val cpt][i] = some o
Tactic:
induction u
Proof state after:
case final
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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
⊢ ∃ o, rtr₂✝[Component.val cpt][i] = some o

case nested
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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✝ : ∃ o, n₂✝[Component.val cpt][i] = some o
⊢ ∃ o, rtr₂✝[Component.val cpt][i] = some o
Theorem: Reactor.LawfulMemUpdate.obj?_some₂
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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
⊢ ∃ o, rtr₂✝[Component.val cpt][i] = some o
Tactic:
case final         => exact ⟨_, get?_some_to_obj?_some ‹_›⟩
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_some₂
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∃ o, n₂✝[Component.val cpt][i] = some o
⊢ ∃ o, rtr₂✝[Component.val cpt][i] = some o
Tactic:
case nested h _ hi => exact ⟨_, obj?_some_nested h hi.choose_spec⟩
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_some₂
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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
⊢ ∃ o, rtr₂✝[Component.val cpt][i] = some o
Tactic:
exact ⟨_, get?_some_to_obj?_some ‹_›⟩
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_some₂
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : ∃ o, n₂✝[Component.val cpt][i] = some o
⊢ ∃ o, rtr₂✝[Component.val cpt][i] = some o
Tactic:
exact ⟨_, obj?_some_nested h hi.choose_spec⟩
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
⊢ rtr₂[Component.val c][j] = rtr₁[Component.val c][j]
Tactic:
cases ho₁ : rtr₁[c][j]
Proof state after:
case none
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
ho₁ : rtr₁[Component.val c][j] = none
⊢ rtr₂[Component.val c][j] = none

case some
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
val✝ : Component.type α (Component.val c)
ho₁ : rtr₁[Component.val c][j] = some val✝
⊢ rtr₂[Component.val c][j] = some val✝
Theorem: Reactor.LawfulMemUpdate.obj?_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
ho₁ : rtr₁[Component.val c][j] = none
⊢ rtr₂[Component.val c][j] = none
Tactic:
case none => simp [obj?_none_iff u |>.mp ho₁]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
val✝ : Component.type α (Component.val c)
ho₁ : rtr₁[Component.val c][j] = some val✝
⊢ rtr₂[Component.val c][j] = some val✝
Tactic:
case some =>
  have ⟨_, ho₂⟩ := obj?_some_iff u |>.mp ⟨_, ho₁⟩ 
  have ⟨m₁⟩ := Object.iff_obj?_some.mpr ho₁
  have ⟨m₂⟩ := Object.iff_obj?_some.mpr ho₂
  simp [ho₂, m₁.lawfulMemUpdate_object_preserved u h m₂]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
ho₁ : rtr₁[Component.val c][j] = none
⊢ rtr₂[Component.val c][j] = none
Tactic:
simp [obj?_none_iff u |>.mp ho₁]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
val✝ : Component.type α (Component.val c)
ho₁ : rtr₁[Component.val c][j] = some val✝
⊢ rtr₂[Component.val c][j] = some val✝
Tactic:
have ⟨_, ho₂⟩ := obj?_some_iff u |>.mp ⟨_, ho₁⟩
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
val✝ : Component.type α (Component.val c)
ho₁ : rtr₁[Component.val c][j] = some val✝
w✝ : Component.type α (Component.val c)
ho₂ : rtr₂[Component.val c][j] = some w✝
⊢ rtr₂[Component.val c][j] = some val✝
Theorem: Reactor.LawfulMemUpdate.obj?_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
val✝ : Component.type α (Component.val c)
ho₁ : rtr₁[Component.val c][j] = some val✝
w✝ : Component.type α (Component.val c)
ho₂ : rtr₂[Component.val c][j] = some w✝
⊢ rtr₂[Component.val c][j] = some val✝
Tactic:
have ⟨m₁⟩ := Object.iff_obj?_some.mpr ho₁
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
w✝ : Component.type α (Component.val c)
ho₂ : rtr₂[Component.val c][j] = some w✝
m₁ : Member (Component.val c) j rtr₁
ho₁ : rtr₁[Component.val c][j] = some (Member.object m₁)
⊢ rtr₂[Component.val c][j] = some (Member.object m₁)
Theorem: Reactor.LawfulMemUpdate.obj?_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
w✝ : Component.type α (Component.val c)
ho₂ : rtr₂[Component.val c][j] = some w✝
m₁ : Member (Component.val c) j rtr₁
ho₁ : rtr₁[Component.val c][j] = some (Member.object m₁)
⊢ rtr₂[Component.val c][j] = some (Member.object m₁)
Tactic:
have ⟨m₂⟩ := Object.iff_obj?_some.mpr ho₂
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
m₁ : Member (Component.val c) j rtr₁
ho₁ : rtr₁[Component.val c][j] = some (Member.object m₁)
m₂ : Member (Component.val c) j rtr₂
ho₂ : rtr₂[Component.val c][j] = some (Member.object m₂)
⊢ rtr₂[Component.val c][j] = some (Member.object m₁)
Theorem: Reactor.LawfulMemUpdate.obj?_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
m₁ : Member (Component.val c) j rtr₁
ho₁ : rtr₁[Component.val c][j] = some (Member.object m₁)
m₂ : Member (Component.val c) j rtr₂
ho₂ : rtr₂[Component.val c][j] = some (Member.object m₂)
⊢ rtr₂[Component.val c][j] = some (Member.object m₁)
Tactic:
simp [ho₂, m₁.lawfulMemUpdate_object_preserved u h m₂]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_updated
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ rtr₂[Component.val cpt][i] = (fun x => v) <$> rtr₁[Component.val cpt][i]
Tactic:
induction u
Proof state after:
case final
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]

case nested
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
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₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
Theorem: Reactor.LawfulMemUpdate.obj?_updated
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
Tactic:
case final h₁ h₂ => 
  rw [get?_some_to_obj?_some h₁, get?_some_to_obj?_some h₂, Option.map_some]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_updated
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
Tactic:
case nested h₁ h₂ u hi =>
  have ⟨_, h₁'⟩ := u.obj?_some₁
  have ⟨_, h₂'⟩ := u.obj?_some₂
  rw [obj?_some_nested h₁ h₁', obj?_some_nested h₂ h₂']
  exact h₁' ▸ h₂' ▸ hi
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_updated
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ rtr₁✝ rtr₂✝ : α
o✝ : Component.type α (Component.val cpt)
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝
h₁ : rtr₁✝{Component.val cpt}{i} = some o✝
h₂ : rtr₂✝{Component.val cpt}{i} = some v
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
Tactic:
rw [get?_some_to_obj?_some h₁, get?_some_to_obj?_some h₂, Option.map_some]
Proof state after:
no goals
Theorem: Reactor.LawfulMemUpdate.obj?_updated
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
Tactic:
have ⟨_, h₁'⟩ := u.obj?_some₁
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
w✝ : Component.type α (Component.val cpt)
h₁' : n₁✝[Component.val cpt][i] = some w✝
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
Theorem: Reactor.LawfulMemUpdate.obj?_updated
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
w✝ : Component.type α (Component.val cpt)
h₁' : n₁✝[Component.val cpt][i] = some w✝
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]
Tactic:
have ⟨_, h₂'⟩ := u.obj?_some₂
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
j✝ : ID
rtr₁✝ rtr₂✝ : α
n₁✝ n₂✝ : Component.type α Component.rtr
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂✝
h₁ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
hi : n₂✝[Component.val cpt][i] = (fun x => v) <$> n₁✝[Component.val cpt][i]
w✝¹ : Component.type α (Component.val cpt)
h₁' : n₁✝[Component.val cpt][i] = some w✝¹
w✝ : Component.type α (Component.val cpt)
h₂' : n₂✝[Component.val cpt][i] = some w✝
⊢ rtr₂✝[Component.val cpt][i] = (fun x => v) <$> rtr₁✝[Component.val cpt][i]