internlm/Lean-Github huggingface dataset:
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
j' : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂{Component.rtr}{j'} = some n₂✝
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂
⊢ object s₁ = object s₂
Tactic:
case nested j' _ _ u _ _ e =>
  by_cases hj : j₁ = j'
  case neg => 
    cases h₂ ▸ (e (c := .rtr) (j := j₁) (.inr hj)) ▸ h₁
    simp [s₁.unique s₂]
  case pos => 
    simp_all [hj]
    exact hi (h₁ ▸ h₂ ▸ u) _
Proof state after:
no goals
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁✝ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ j₁ = j₂
Tactic:
have hs := (nested h₁ s₁ |>.fromEquiv u.equiv).unique (nested h₂ s₂)
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁✝ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : fromEquiv ⋯ (nested h₁ s₁) = nested h₂ s₂
⊢ j₁ = j₂
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁✝ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : fromEquiv ⋯ (nested h₁ s₁) = nested h₂ s₂
⊢ j₁ = j₂
Tactic:
simp [fromEquiv] at hs
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁✝ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : j₁ = j₂ ∧ Exists.choose ⋯ = rtr₂✝ ∧ HEq (fromEquiv ⋯ s₁) s₂
⊢ j₁ = j₂
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁✝ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : j₁ = j₂ ∧ Exists.choose ⋯ = rtr₂✝ ∧ HEq (fromEquiv ⋯ s₁) s₂
⊢ j₁ = j₂
Tactic:
exact hs.left
Proof state after:
no goals
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
o✝ : Component.type α (Component.val cpt)
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂{Component.val cpt}{i} = some v
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ object s₁ = object s₂
Tactic:
cases h₂ ▸ (e (c := .rtr) (j := j₁) (.inl $ by simp)) ▸ h₁
Proof state after:
case refl
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝
s₁ : StrictMember (Component.val c) j rtr₂✝
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂{Component.val cpt}{i} = some v
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ object s₁ = object s₂
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
case refl
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝
s₁ : StrictMember (Component.val c) j rtr₂✝
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
o✝ : Component.type α (Component.val cpt)
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂{Component.val cpt}{i} = some v
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ object s₁ = object s₂
Tactic:
simp [s₁.unique s₂]
Proof state after:
no goals
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
o✝ : Component.type α (Component.val cpt)
a✝¹ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝ : rtr₂{Component.val cpt}{i} = some v
e : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ Component.rtr ≠ Component.val cpt
Tactic:
simp
Proof state after:
no goals
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
j' : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂{Component.rtr}{j'} = some n₂✝
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂
⊢ object s₁ = object s₂
Tactic:
by_cases hj : j₁ = j'
Proof state after:
case pos
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
j' : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂{Component.rtr}{j'} = some n₂✝
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂
hj : j₁ = j'
⊢ object s₁ = object s₂

case neg
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
j' : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂{Component.rtr}{j'} = some n₂✝
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂
hj : ¬j₁ = j'
⊢ object s₁ = object s₂
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
j' : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂{Component.rtr}{j'} = some n₂✝
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂
hj : ¬j₁ = j'
⊢ object s₁ = object s₂
Tactic:
case neg => 
  cases h₂ ▸ (e (c := .rtr) (j := j₁) (.inr hj)) ▸ h₁
  simp [s₁.unique s₂]
Proof state after:
no goals
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
j' : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂{Component.rtr}{j'} = some n₂✝
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂
hj : j₁ = j'
⊢ object s₁ = object s₂
Tactic:
case pos => 
  simp_all [hj]
  exact hi (h₁ ▸ h₂ ▸ u) _
Proof state after:
no goals
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
j' : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂{Component.rtr}{j'} = some n₂✝
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂
hj : ¬j₁ = j'
⊢ object s₁ = object s₂
Tactic:
cases h₂ ▸ (e (c := .rtr) (j := j₁) (.inr hj)) ▸ h₁
Proof state after:
case refl
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝
s₁ : StrictMember (Component.val c) j rtr₂✝
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
j' : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂{Component.rtr}{j'} = some n₂✝
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂
hj : ¬j₁ = j'
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ object s₁ = object s₂
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
case refl
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝
s₁ : StrictMember (Component.val c) j rtr₂✝
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
j' : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂{Component.rtr}{j'} = some n₂✝
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂
hj : ¬j₁ = j'
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ object s₁ = object s₂
Tactic:
simp [s₁.unique s₂]
Proof state after:
no goals
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember (Component.val c) j rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
j' : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some n₁✝
a✝ : rtr₂{Component.rtr}{j'} = some n₂✝
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂
hj : j₁ = j'
⊢ object s₁ = object s₂
Tactic:
simp_all [hj]
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
s₁ : StrictMember (Component.val c) j rtr₂✝¹
rtr₂ : α
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
j' : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
h : ¬c = cpt ∨ ¬j = i
h₁ : n₁✝ = rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
h₂ : n₂✝ = rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some rtr₂✝¹
a✝ : rtr₂{Component.rtr}{j'} = some rtr₂✝
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂
hj : j₁ = j'
⊢ object s₁ = object s₂
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
s₁ : StrictMember (Component.val c) j rtr₂✝¹
rtr₂ : α
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
j' : ID
n₁✝ n₂✝ : Component.type α Component.rtr
u : LawfulMemUpdate cpt i v n₁✝ n₂✝
h : ¬c = cpt ∨ ¬j = i
h₁ : n₁✝ = rtr₂✝¹
hi :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
h₂ : n₂✝ = rtr₂✝
a✝¹ : rtr₁✝{Component.rtr}{j'} = some rtr₂✝¹
a✝ : rtr₂{Component.rtr}{j'} = some rtr₂✝
e : rtr₁✝ ≃[Component.rtr][j'] rtr₂
hj : j₁ = j'
⊢ object s₁ = object s₂
Tactic:
exact hi (h₁ ▸ h₂ ▸ u) _
Proof state after:
no goals
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr✝ : α
o✝ : Component.type α (Component.val c)
h₁ : rtr✝{Component.val c}{j} = some o✝
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr✝ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ o✝ = object s₂
Tactic:
injection (final h₁ |>.fromEquiv u.equiv).unique (nested h₂ s₂)
Proof state after:
no goals
Theorem: Reactor.StrictMember.lawfulMemUpdate_object_preserved
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component.Valued
j : ID
h : c ≠ cpt ∨ j ≠ i
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
s₁ : StrictMember (Component.val c) j rtr₂✝
a_ih✝ :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object s₁ = object s₂
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁✝ rtr₂
o✝ : Component.type α (Component.val c)
h₂ : rtr₂{Component.val c}{j} = some o✝
⊢ object s₁ = o✝
Tactic:
injection (nested h₁ s₁).unique (final h₂ |>.fromEquiv $ Reactor.Equivalent.symm u.equiv)
Proof state after:
no goals
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
⊢ Object rtr cpt i o → rtr[cpt][i] = some o
Tactic:
intro ⟨m⟩
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
⊢ rtr[cpt][i] = some (Member.object m)
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
⊢ rtr[cpt][i] = some (Member.object m)
Tactic:
simp [obj?]
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
⊢ (if h : ∃ o, Object rtr cpt i o then some (Exists.choose h) else none) = some (Member.object m)
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
⊢ (if h : ∃ o, Object rtr cpt i o then some (Exists.choose h) else none) = some (Member.object m)
Tactic:
split
Proof state after:
case inl
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h✝ : ∃ o, Object rtr cpt i o
⊢ some (Exists.choose h✝) = some (Member.object m)

case inr
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h✝ : ¬∃ o, Object rtr cpt i o
⊢ False
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∃ o, Object rtr cpt i o
⊢ some (Exists.choose h) = some (Member.object m)
Tactic:
case inl h =>
  have ⟨m', h'⟩ := Object.def.mp h.choose_spec
  simp [←h', m.unique m']
Proof state after:
no goals
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ¬∃ o, Object rtr cpt i o
⊢ False
Tactic:
case inr h =>
  push_neg at h
  specialize h m.object
  simp [Object.def] at h
Proof state after:
no goals
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∃ o, Object rtr cpt i o
⊢ some (Exists.choose h) = some (Member.object m)
Tactic:
have ⟨m', h'⟩ := Object.def.mp h.choose_spec
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∃ o, Object rtr cpt i o
m' : Member cpt i rtr
h' : Member.object m' = Exists.choose h
⊢ some (Exists.choose h) = some (Member.object m)
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∃ o, Object rtr cpt i o
m' : Member cpt i rtr
h' : Member.object m' = Exists.choose h
⊢ some (Exists.choose h) = some (Member.object m)
Tactic:
simp [←h', m.unique m']
Proof state after:
no goals
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ¬∃ o, Object rtr cpt i o
⊢ False
Tactic:
push_neg at h
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∀ (o : Component.type α cpt), ¬Object rtr cpt i o
⊢ False
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∀ (o : Component.type α cpt), ¬Object rtr cpt i o
⊢ False
Tactic:
specialize h m.object
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ¬Object rtr cpt i (Member.object m)
⊢ False
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ¬Object rtr cpt i (Member.object m)
⊢ False
Tactic:
simp [Object.def] at h
Proof state after:
no goals
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
h : rtr[cpt][i] = some o
⊢ Object rtr cpt i o
Tactic:
simp [obj?] at h
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
h : (if h : ∃ o, Object rtr cpt i o then some (Exists.choose h) else none) = some o
⊢ Object rtr cpt i o