internlm/Lean-Github huggingface dataset:
Theorem: Reactor.StrictMember.extend_inj
Proof state before:
case nested.nested.intro.intro
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember Component.rtr i₁ rtr₂✝¹
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝¹} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
hj : j✝¹ = j✝
hr : rtr₂✝¹ = rtr₂✝
h : HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Tactic:
subst hj hr
Proof state after:
case nested.nested.intro.intro
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝² : StrictMember Component.rtr i₁ rtr₂✝
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Theorem: Reactor.StrictMember.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝ : Component.type α Component.rtr
a✝¹ : rtr✝{Component.rtr}{i₁} = some o✝
h₁ : object (final a✝¹){cpt}{j} = some o₁
a✝ : rtr✝{Component.rtr}{i₁} = some o✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : HEq (final h₁) (final h₂)
⊢ i₁ = i₁
Tactic:
rfl
Proof state after:
no goals
Theorem: Reactor.StrictMember.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝² : StrictMember Component.rtr i₁ rtr₂✝
hi :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝²{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝² h₁ = extend s₂ h₂ → i₁ = i₂
i₂ : ID
h₁ : object (nested a✝³ a✝²){cpt}{j} = some o₁
a✝¹ : StrictMember Component.rtr i₂ rtr₂✝
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : HEq (extend a✝² h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Tactic:
exact hi $ eq_of_heq h
Proof state after:
no goals
Theorem: Reactor.StrictMember.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr✝ : α
o✝ : Component.type α Component.rtr
a✝² : rtr✝{Component.rtr}{i₁} = some o✝
i₂ : ID
h₁ : object (final a✝²){cpt}{j} = some o₁
a✝¹ : StrictMember Component.rtr i₂ o✝
a✝ : rtr✝{Component.rtr}{i₁} = some o✝
h₂ : object (nested a✝ a✝¹){cpt}{j} = some o₂
h : HEq (final h₁) (extend a✝¹ h₂)
⊢ i₁ = i₂
Tactic:
exact absurd (eq_of_heq h).symm $ StrictMember.extend_not_final _ _ _
Proof state after:
no goals
Theorem: Reactor.StrictMember.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr : α
i₁ : ID
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember Component.rtr i₁ rtr₂✝
a_ih✝ :
  ∀ {i₂ : ID} {s₂ : StrictMember Component.rtr i₂ rtr₂✝} {h₁ : object a✝¹{cpt}{j} = some o₁}
    {h₂ : object s₂{cpt}{j} = some o₂}, extend a✝¹ h₁ = extend s₂ h₂ → i₁ = i₂
h₁ : object (nested a✝² a✝¹){cpt}{j} = some o₁
a✝ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
h₂ : object (final a✝){cpt}{j} = some o₂
h : HEq (extend a✝¹ h₁) (final h₂)
⊢ i₁ = j✝
Tactic:
exact absurd (eq_of_heq h) $ StrictMember.extend_not_final _ _ _
Proof state after:
no goals
Theorem: Reactor.StrictMember.extend_split
Proof state before:
α : Type
inst✝ : Reactor α
rtr : α
cpt : Component
i' : ID
rtr' : Component.type α Component.rtr
i : ID
s : StrictMember cpt i' rtr'
h : rtr{Component.rtr}{i} = some rtr'
⊢ extend ↑(split s h).snd ⋯ = nested h s
Tactic:
induction s generalizing rtr i <;> simp [extend]
Proof state after:
case nested
α : Type
inst✝ : Reactor α
cpt : Component
i' : ID
rtr' rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
a✝¹ : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝ : StrictMember cpt i' rtr₂✝
a_ih✝ : ∀ {rtr : α} {i : ID} (h : rtr{Component.rtr}{i} = some rtr₂✝), extend ↑(split a✝ h).snd ⋯ = nested h a✝
rtr : α
i : ID
h : rtr{Component.rtr}{i} = some rtr₁✝
⊢ extend ↑(split a✝ a✝¹).2 ⋯ = nested a✝¹ a✝
Theorem: Reactor.StrictMember.extend_split
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component
i' : ID
rtr' rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
h' : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝ : StrictMember cpt i' rtr₂✝
hi : ∀ {rtr : α} {i : ID} (h : rtr{Component.rtr}{i} = some rtr₂✝), extend ↑(split a✝ h).snd ⋯ = nested h a✝
rtr : α
i : ID
h : rtr{Component.rtr}{i} = some rtr₁✝
⊢ extend ↑(split a✝ h').2 ⋯ = nested h' a✝
Tactic:
case nested h' _ hi => exact hi h'
Proof state after:
no goals
Theorem: Reactor.StrictMember.extend_split
Proof state before:
α : Type
inst✝ : Reactor α
cpt : Component
i' : ID
rtr' rtr₁✝ : Component.type α Component.rtr
j✝ : ID
rtr₂✝ : Component.type (Component.type α Component.rtr) Component.rtr
h' : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝ : StrictMember cpt i' rtr₂✝
hi : ∀ {rtr : α} {i : ID} (h : rtr{Component.rtr}{i} = some rtr₂✝), extend ↑(split a✝ h).snd ⋯ = nested h a✝
rtr : α
i : ID
h : rtr{Component.rtr}{i} = some rtr₁✝
⊢ extend ↑(split a✝ h').2 ⋯ = nested h' a✝
Tactic:
exact hi h'
Proof state after:
no goals
Theorem: Reactor.StrictMember.Equivalent.symm
Proof state before:
α : Type
inst✝¹ : Reactor α
rtr₁ : α
β : Type
cpt : Component
i : ID
inst✝ : Reactor β
rtr₂ : β
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
e : s₁ ∼ s₂
⊢ s₂ ∼ s₁
Tactic:
induction e <;> constructor
Proof state after:
case nested.a
α : Type
inst✝³ : Reactor α
rtr₁ : α
β : Type
cpt : Component
i : ID
inst✝² : Reactor β
rtr₂ : β
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
α✝ β✝ : Type
cpt✝ : Component
i✝ j✝ : ID
inst✝¹ : Reactor α✝
inst✝ : Reactor β✝
rtr₁✝ : α✝
rtr₂✝ : β✝
n₁✝ : α✝
n₂✝ : β✝
s₁✝ : StrictMember cpt✝ i✝ n₁✝
s₂✝ : StrictMember cpt✝ i✝ n₂✝
h₁✝ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂✝ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : Equivalent s₁✝ s₂✝
a_ih✝ : s₂✝ ∼ s₁✝
⊢ Equivalent s₂✝ s₁✝
Theorem: Reactor.StrictMember.Equivalent.symm
Proof state before:
case nested.a
α : Type
inst✝³ : Reactor α
rtr₁ : α
β : Type
cpt : Component
i : ID
inst✝² : Reactor β
rtr₂ : β
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
α✝ β✝ : Type
cpt✝ : Component
i✝ j✝ : ID
inst✝¹ : Reactor α✝
inst✝ : Reactor β✝
rtr₁✝ : α✝
rtr₂✝ : β✝
n₁✝ : α✝
n₂✝ : β✝
s₁✝ : StrictMember cpt✝ i✝ n₁✝
s₂✝ : StrictMember cpt✝ i✝ n₂✝
h₁✝ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂✝ : rtr₂✝{Component.rtr}{j✝} = some n₂✝
a✝ : Equivalent s₁✝ s₂✝
a_ih✝ : s₂✝ ∼ s₁✝
⊢ Equivalent s₂✝ s₁✝
Tactic:
assumption
Proof state after:
no goals
Theorem: Reactor.StrictMember.Equivalent.trans
Proof state before:
α : Type
inst✝² : Reactor α
rtr₁ : α
β γ : Type
cpt : Component
i : ID
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
s₃ : StrictMember cpt i rtr₃
e₁ : s₁ ∼ s₂
e₂ : s₂ ∼ s₃
⊢ s₁ ∼ s₃
Tactic:
induction e₁ generalizing rtr₃ <;> cases e₂ <;> constructor <;> try assumption
Proof state after:
case nested.nested.a
α : Type
inst✝⁴ : Reactor α
rtr₁ : α
β γ : Type
cpt : Component
i : ID
inst✝³ : Reactor β
inst✝² : Reactor γ
rtr₂ : β
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
α✝ β✝ : Type
cpt✝ : Component
i✝ j✝ : ID
inst✝¹ : Reactor α✝
inst✝ : Reactor β✝
rtr₁✝ : α✝
rtr₂✝ : β✝
n₁✝ : α✝
n₂✝¹ : β✝
s₁✝ : StrictMember cpt✝ i✝ n₁✝
s₂✝¹ : StrictMember cpt✝ i✝ n₂✝¹
h₁✝¹ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂✝¹ : rtr₂✝{Component.rtr}{j✝} = some n₂✝¹
a✝¹ : Equivalent s₁✝ s₂✝¹
a_ih✝ : ∀ {rtr₃ : γ} {s₃ : StrictMember cpt✝ i✝ rtr₃}, s₂✝¹ ∼ s₃ → s₁✝ ∼ s₃
rtr₃ n₂✝ : γ
s₂✝ : StrictMember cpt✝ i✝ n₂✝
h₂✝ : rtr₃{Component.rtr}{j✝} = some n₂✝
h₁✝ : rtr₂✝{Component.rtr}{j✝} = some n₂✝¹
a✝ : Equivalent s₂✝¹ s₂✝
⊢ Equivalent s₁✝ s₂✝
Theorem: Reactor.StrictMember.Equivalent.trans
Proof state before:
α : Type
inst✝⁴ : Reactor α
rtr₁ : α
β γ : Type
cpt : Component
i : ID
inst✝³ : Reactor β
inst✝² : Reactor γ
rtr₂ : β
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
α✝ β✝ : Type
cpt✝ : Component
i✝ j✝ : ID
inst✝¹ : Reactor α✝
inst✝ : Reactor β✝
rtr₁✝ : α✝
rtr₂✝ : β✝
n₁✝ : α✝
n₂✝¹ : β✝
s₁✝ : StrictMember cpt✝ i✝ n₁✝
s₂✝¹ : StrictMember cpt✝ i✝ n₂✝¹
h₁✝¹ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂✝¹ : rtr₂✝{Component.rtr}{j✝} = some n₂✝¹
a✝ : Equivalent s₁✝ s₂✝¹
hi₁ : ∀ {rtr₃ : γ} {s₃ : StrictMember cpt✝ i✝ rtr₃}, s₂✝¹ ∼ s₃ → s₁✝ ∼ s₃
rtr₃ n₂✝ : γ
s₂✝ : StrictMember cpt✝ i✝ n₂✝
h₂✝ : rtr₃{Component.rtr}{j✝} = some n₂✝
h₁✝ : rtr₂✝{Component.rtr}{j✝} = some n₂✝¹
hi₂ : Equivalent s₂✝¹ s₂✝
⊢ Equivalent s₁✝ s₂✝
Tactic:
case nested.nested hi₁ _ _ _ _ hi₂ => exact hi₁ hi₂
Proof state after:
no goals
Theorem: Reactor.StrictMember.Equivalent.trans
Proof state before:
case nested.refl.a
α : Type
inst✝³ : Reactor α
rtr₁ : α
β γ : Type
cpt : Component
i : ID
inst✝² : Reactor β
inst✝¹ : Reactor γ
rtr₂ : β
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
α✝ : Type
cpt✝ : Component
i✝ j✝ : ID
inst✝ : Reactor α✝
rtr₁✝ n₁✝ : α✝
s₁✝ : StrictMember cpt✝ i✝ n₁✝
h₁✝ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
rtr₃ n₂✝ : γ
s₂✝ : StrictMember cpt✝ i✝ n₂✝
a✝ : Equivalent s₁✝ s₂✝
a_ih✝ : ∀ {rtr₃ : γ} {s₃ : StrictMember cpt✝ i✝ rtr₃}, s₂✝ ∼ s₃ → s₁✝ ∼ s₃
h₂✝ : rtr₃{Component.rtr}{j✝} = some n₂✝
⊢ Equivalent s₁✝ s₂✝
Tactic:
assumption
Proof state after:
no goals
Theorem: Reactor.StrictMember.Equivalent.trans
Proof state before:
α : Type
inst✝⁴ : Reactor α
rtr₁ : α
β γ : Type
cpt : Component
i : ID
inst✝³ : Reactor β
inst✝² : Reactor γ
rtr₂ : β
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
α✝ β✝ : Type
cpt✝ : Component
i✝ j✝ : ID
inst✝¹ : Reactor α✝
inst✝ : Reactor β✝
rtr₁✝ : α✝
rtr₂✝ : β✝
n₁✝ : α✝
n₂✝¹ : β✝
s₁✝ : StrictMember cpt✝ i✝ n₁✝
s₂✝¹ : StrictMember cpt✝ i✝ n₂✝¹
h₁✝¹ : rtr₁✝{Component.rtr}{j✝} = some n₁✝
h₂✝¹ : rtr₂✝{Component.rtr}{j✝} = some n₂✝¹
a✝ : Equivalent s₁✝ s₂✝¹
hi₁ : ∀ {rtr₃ : γ} {s₃ : StrictMember cpt✝ i✝ rtr₃}, s₂✝¹ ∼ s₃ → s₁✝ ∼ s₃
rtr₃ n₂✝ : γ
s₂✝ : StrictMember cpt✝ i✝ n₂✝
h₂✝ : rtr₃{Component.rtr}{j✝} = some n₂✝
h₁✝ : rtr₂✝{Component.rtr}{j✝} = some n₂✝¹
hi₂ : Equivalent s₂✝¹ s₂✝
⊢ Equivalent s₁✝ s₂✝
Tactic:
exact hi₁ hi₂
Proof state after:
no goals
Theorem: Reactor.StrictMember.Equivalent.to_eq
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr : α
s₁ s₂ : StrictMember cpt i rtr
o₁✝ o₂✝ : Component.type α cpt
h₁ : rtr{cpt}{i} = some o₁✝
h₂ : rtr{cpt}{i} = some o₂✝
⊢ StrictMember.final h₁ = StrictMember.final h₂
Tactic:
simp [Option.some_inj.mp $ h₁ ▸ h₂]
Proof state after:
no goals
Theorem: Reactor.StrictMember.Equivalent.to_eq
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr : α
s₁ s₂ : StrictMember cpt i rtr
j✝ : ID
n₁✝ n₂✝ : α
s₁✝ : StrictMember cpt i n₁✝
s₂✝ : StrictMember cpt i n₂✝
h₁ : rtr{Component.rtr}{j✝} = some n₁✝
h₂ : rtr{Component.rtr}{j✝} = some n₂✝
e : Equivalent s₁✝ s₂✝
⊢ StrictMember.nested h₁ s₁✝ = StrictMember.nested h₂ s₂✝
Tactic:
cases Option.some_inj.mp $ h₁ ▸ h₂
Proof state after:
case refl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr : α
s₁ s₂ : StrictMember cpt i rtr
j✝ : ID
n₁✝ : α
s₁✝ : StrictMember cpt i n₁✝
h₁ : rtr{Component.rtr}{j✝} = some n₁✝
s₂✝ : StrictMember cpt i n₁✝
h₂ : rtr{Component.rtr}{j✝} = some n₁✝
e : Equivalent s₁✝ s₂✝
⊢ StrictMember.nested h₁ s₁✝ = StrictMember.nested h₂ s₂✝
Theorem: Reactor.StrictMember.Equivalent.to_eq
Proof state before:
case refl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component
i : ID
rtr : α
s₁ s₂ : StrictMember cpt i rtr
j✝ : ID
n₁✝ : α
s₁✝ : StrictMember cpt i n₁✝
h₁ : rtr{Component.rtr}{j✝} = some n₁✝
s₂✝ : StrictMember cpt i n₁✝
h₂ : rtr{Component.rtr}{j✝} = some n₁✝
e : Equivalent s₁✝ s₂✝
⊢ StrictMember.nested h₁ s₁✝ = StrictMember.nested h₂ s₂✝
Tactic:
simp [to_eq e]
Proof state after:
no goals
Theorem: Reactor.StrictMember.Equivalent.fromLawfulMemUpdate
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
s : StrictMember c j rtr₂
⊢ s ∼ StrictMember.fromLawfulMemUpdate s u
Tactic:
induction u <;> cases s <;> (simp [StrictMember.fromLawfulMemUpdate]; try exact final _ _)
Proof state after:
case final.nested
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
rtr₁✝ rtr₂✝¹ : α
o✝ : Component.type α (Component.val cpt)
a✝⁴ : rtr₁✝ ≃[Component.val cpt][i] rtr₂✝¹
a✝³ : rtr₁✝{Component.val cpt}{i} = some o✝
a✝² : rtr₂✝¹{Component.val cpt}{i} = some v
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember c j rtr₂✝
a✝ : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested a✝ a✝¹ ∼ StrictMember.nested ⋯ a✝¹

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

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