internlm/Lean-Github huggingface dataset:
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ object (nested h₁ s₁) = object (nested h₂ s₂)
Tactic:
suffices hj : j₁ = j₂ by subst hj; exact hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) _
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ j₁ = j₂
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ j₁ = j₂
Tactic:
have hs := (nested h₁ s₁ |>.fromEquiv e).unique (nested h₂ s₂)
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : fromEquiv e (nested h₁ s₁) = nested h₂ s₂
⊢ j₁ = j₂
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : fromEquiv e (nested h₁ s₁) = nested h₂ s₂
⊢ j₁ = j₂
Tactic:
simp [fromEquiv] at hs
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : j₁ = j₂ ∧ Exists.choose ⋯ = rtr₂✝ ∧ HEq (fromEquiv ⋯ s₁) s₂
⊢ j₁ = j₂
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hs : j₁ = j₂ ∧ Exists.choose ⋯ = rtr₂✝ ∧ HEq (fromEquiv ⋯ s₁) s₂
⊢ j₁ = j₂
Tactic:
exact hs.left
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
hj : j₁ = j₂
⊢ object (nested h₁ s₁) = object (nested h₂ s₂)
Tactic:
subst hj
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ object (nested h₁ s₁) = object (nested h₂ s₂)
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember Component.rcn i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ object (nested h₁ s₁) = object (nested h₂ s₂)
Tactic:
exact hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) _
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr✝ : α
o✝ : Component.type α Component.rcn
h₁ : rtr✝{Component.rcn}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember Component.rcn i rtr₂✝
h₂ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ object (final h₁) = object (nested h₂ s₂)
Tactic:
injection (final h₁ |>.fromEquiv e).unique (nested h₂ s₂)
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv_rcn_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
h₁ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
s₁ : StrictMember Component.rcn i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember Component.rcn i rtr₂), object s₁ = object s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α Component.rcn
h₂ : rtr₂{Component.rcn}{i} = some o✝
⊢ object (nested h₁ s₁) = object (final h₂)
Tactic:
injection (nested h₁ s₁).unique (final h₂ |>.fromEquiv $ Reactor.Equivalent.symm e)
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
rtr₂ : α
c : Component.Valued
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
h : c ≠ cpt ∨ j ≠ i
s₁ : StrictMember (Component.val c) j rtr₁
s₂ : StrictMember (Component.val c) j rtr₂
⊢ object s₁ = object s₂
Tactic:
induction s₁ generalizing rtr₂ <;> cases s₂ <;> simp [object]
Proof state after:
case final.final
α : 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)
a✝¹ : rtr✝{Component.val c}{j} = some o✝¹
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr✝ rtr₂
o✝ : Component.type α (Component.val c)
a✝ : rtr₂{Component.val c}{j} = some o✝
⊢ o✝¹ = o✝

case final.nested
α : 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)
a✝² : rtr✝{Component.val c}{j} = some o✝
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr✝ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember (Component.val c) j rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ o✝ = object a✝¹

case nested.final
α : 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
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember (Component.val c) j rtr₂✝
a_ih✝ :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object a✝¹ = object s₂
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁✝ rtr₂
o✝ : Component.type α (Component.val c)
a✝ : rtr₂{Component.val c}{j} = some o✝
⊢ object a✝¹ = o✝

case nested.nested
α : 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
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember (Component.val c) j rtr₂✝¹
a_ih✝ :
  ∀ {rtr₂ : α},
    LawfulMemUpdate cpt i v rtr₂✝¹ rtr₂ → ∀ (s₂ : StrictMember (Component.val c) j rtr₂), object a✝² = object s₂
rtr₂ : α
u : LawfulMemUpdate cpt i v rtr₁✝ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember (Component.val c) j rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ object a✝² = object a✝¹
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₂
o✝ : Component.type α (Component.val c)
h₂ : rtr₂{Component.val c}{j} = some o✝
⊢ o✝¹ = o✝
Tactic:
case final.final h₁ _ h₂ =>
  cases u
  case final e => simp_all [e.valued h]
  case nested e => simp_all [e (c := c) (.inl $ by 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₂ : α
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₂✝
⊢ object s₁ = object s₂
Tactic:
case nested.nested j₁ _ h₁ s₁ hi j₂ _ s₂ h₂ => 
  have hj : j₁ = j₂ := by 
    have hs := (nested h₁ s₁ |>.fromEquiv u.equiv).unique (nested h₂ s₂)
    simp [fromEquiv] at hs
    exact hs.left
  subst hj
  cases u
  case final e => 
    cases h₂ ▸ (e (c := .rtr) (j := j₁) (.inl $ by simp)) ▸ h₁
    simp [s₁.unique s₂]
  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✝ : α
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:
case final.nested h₁ _ _ s₂ h₂ =>
  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:
case nested.final h₁ s₁ _ _ h₂ =>
  injection (nested h₁ s₁).unique (final h₂ |>.fromEquiv $ Reactor.Equivalent.symm u.equiv)
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₂
o✝ : Component.type α (Component.val c)
h₂ : rtr₂{Component.val c}{j} = some o✝
⊢ o✝¹ = o✝
Tactic:
cases u
Proof state after:
case final
α : 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₂ : α
o✝¹ : Component.type α (Component.val c)
h₂ : rtr₂{Component.val c}{j} = some o✝¹
o✝ : Component.type α (Component.val cpt)
a✝² : rtr✝{Component.val cpt}{i} = some o✝
a✝¹ : rtr₂{Component.val cpt}{i} = some v
a✝ : rtr✝ ≃[Component.val cpt][i] rtr₂
⊢ o✝² = o✝¹

case nested
α : 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₂ : α
o✝ : Component.type α (Component.val c)
h₂ : rtr₂{Component.val c}{j} = some o✝
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
a✝³ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝² : rtr✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂{Component.rtr}{j✝} = some n₂✝
a✝ : rtr✝ ≃[Component.rtr][j✝] rtr₂
⊢ o✝¹ = o✝
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₂ : α
o✝¹ : Component.type α (Component.val c)
h₂ : rtr₂{Component.val c}{j} = some o✝¹
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₂
⊢ o✝² = o✝¹
Tactic:
case final e => simp_all [e.valued h]
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₂ : α
o✝ : Component.type α (Component.val c)
h₂ : rtr₂{Component.val c}{j} = some o✝
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : 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₂
⊢ o✝¹ = o✝
Tactic:
case nested e => simp_all [e (c := c) (.inl $ by 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✝ : α
o✝² : Component.type α (Component.val c)
h₁ : rtr✝{Component.val c}{j} = some o✝²
rtr₂ : α
o✝¹ : Component.type α (Component.val c)
h₂ : rtr₂{Component.val c}{j} = some o✝¹
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₂
⊢ o✝² = o✝¹
Tactic:
simp_all [e.valued h]
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₂ : α
o✝ : Component.type α (Component.val c)
h₂ : rtr₂{Component.val c}{j} = some o✝
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : 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₂
⊢ o✝¹ = o✝
Tactic:
simp_all [e (c := c) (.inl $ by 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✝ : α
o✝¹ : Component.type α (Component.val c)
h₁ : rtr✝{Component.val c}{j} = some o✝¹
rtr₂ : α
o✝ : Component.type α (Component.val c)
h₂ : rtr₂{Component.val c}{j} = some o✝
j✝ : ID
n₁✝ n₂✝ : Component.type α Component.rtr
a✝² : 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₂
⊢ Component.val c ≠ Component.rtr
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₂ : α
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₂✝
⊢ object s₁ = object s₂
Tactic:
have hj : j₁ = j₂ := by 
  have hs := (nested h₁ s₁ |>.fromEquiv u.equiv).unique (nested h₂ s₂)
  simp [fromEquiv] at hs
  exact hs.left
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₂✝
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₂ : α
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₂✝
hj : j₁ = j₂
⊢ object s₁ = object s₂
Tactic:
subst hj
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₂
rtr₂✝ : Component.type α Component.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:
α : 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₂
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember (Component.val c) j rtr₂✝
h₂ : rtr₂{Component.rtr}{j₁} = some rtr₂✝
⊢ object s₁ = object s₂
Tactic:
cases u
Proof state after:
case final
α : 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
a✝ : rtr₁✝ ≃[Component.val cpt][i] rtr₂
⊢ object s₁ = object s₂

case nested
α : 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
a✝³ : LawfulMemUpdate cpt i v n₁✝ n₂✝
a✝² : rtr₁✝{Component.rtr}{j✝} = some n₁✝
a✝¹ : rtr₂{Component.rtr}{j✝} = some n₂✝
a✝ : rtr₁✝ ≃[Component.rtr][j✝] rtr₂
⊢ 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₂✝
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:
case final e => 
  cases h₂ ▸ (e (c := .rtr) (j := j₁) (.inl $ by simp)) ▸ h₁
  simp [s₁.unique s₂]
Proof state after:
no goals