internlm/Lean-Github huggingface dataset:
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:
cases hj
Proof state after:
case refl
α : 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✝
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested hn m ∼ StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)
Theorem: Reactor.StrictMember.Equivalent.fromLawfulMemUpdate
Proof state before:
case refl
α : 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✝
rtr₂✝ : Component.type α Component.rtr
m : StrictMember c j rtr₂✝
hn : rtr₂✝¹{Component.rtr}{j✝} = some rtr₂✝
⊢ StrictMember.nested hn m ∼ StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)
Tactic:
cases Option.some_inj.mp $ h₂ ▸ hn
Proof state after:
case refl.refl
α : 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✝
m : StrictMember c j n₂✝
hn : rtr₂✝{Component.rtr}{j✝} = some n₂✝
⊢ StrictMember.nested hn m ∼ StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)
Theorem: Reactor.StrictMember.Equivalent.fromLawfulMemUpdate
Proof state before:
case refl.refl
α : 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✝
m : StrictMember c j n₂✝
hn : rtr₂✝{Component.rtr}{j✝} = some n₂✝
⊢ StrictMember.nested hn m ∼ StrictMember.nested h₁ (StrictMember.fromLawfulMemUpdate (⋯ ▸ m) a✝)
Tactic:
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:
exact nested hn (hn ▸ e (.inr hj)) (refl _)
Proof state after:
no goals
Theorem: Reactor.StrictMember.Equivalent.fromLawfulUpdate
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
u : LawfulUpdate cpt i v rtr₁ rtr₂
s : StrictMember c j rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s u
Tactic:
cases u
Proof state after:
case update
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
u✝ : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.update u✝)

case notMem
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
h✝ : IsEmpty (Member (Component.val cpt) i rtr₁)
eq✝ : rtr₁ = rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.notMem h✝ eq✝)
Theorem: Reactor.StrictMember.Equivalent.fromLawfulUpdate
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
h✝ : IsEmpty (Member (Component.val cpt) i rtr₁)
eq✝ : rtr₁ = rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.notMem h✝ eq✝)
Tactic:
case notMem   => cases ‹_ = _›; apply refl
Proof state after:
no goals
Theorem: Reactor.StrictMember.Equivalent.fromLawfulUpdate
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.update u)
Tactic:
case update u => exact fromLawfulMemUpdate u s
Proof state after:
no goals
Theorem: Reactor.StrictMember.Equivalent.fromLawfulUpdate
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
h✝ : IsEmpty (Member (Component.val cpt) i rtr₁)
eq✝ : rtr₁ = rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.notMem h✝ eq✝)
Tactic:
cases ‹_ = _›
Proof state after:
case refl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component
j : ID
h✝ : IsEmpty (Member (Component.val cpt) i rtr₁)
s : StrictMember c j rtr₁
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.notMem h✝ ⋯)
Theorem: Reactor.StrictMember.Equivalent.fromLawfulUpdate
Proof state before:
case refl
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
c : Component
j : ID
h✝ : IsEmpty (Member (Component.val cpt) i rtr₁)
s : StrictMember c j rtr₁
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.notMem h✝ ⋯)
Tactic:
apply refl
Proof state after:
no goals
Theorem: Reactor.StrictMember.Equivalent.fromLawfulUpdate
Proof state before:
α : Type
inst✝ : Reactor α
rtr₁ : α
cpt : Component.Valued
i : ID
v : Value
rtr₂ : α
c : Component
j : ID
s : StrictMember c j rtr₂
u : LawfulMemUpdate cpt i v rtr₁ rtr₂
⊢ s ∼ StrictMember.fromLawfulUpdate s (LawfulUpdate.update u)
Tactic:
exact fromLawfulMemUpdate u s
Proof state after:
no goals
Theorem: Reactor.Member.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
i₁ i₂ : Component.idType Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
m₁ : Member Component.rtr i₁ rtr
m₂ : Member Component.rtr i₂ rtr
h₁ : object m₁{cpt}{j} = some o₁
h₂ : object m₂{cpt}{j} = some o₂
h : extend m₁ h₁ = extend m₂ h₂
⊢ i₁ = i₂
Tactic:
cases m₁ <;> cases m₂ <;> simp [Member.extend] at h
Proof state after:
case root.root
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : o₁ = o₂
⊢ ⊤ = ⊤

case root.strict
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.final h₁ = StrictMember.extend a✝ h₂
⊢ ⊤ =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝

case strict.root
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₁ : object (strict a✝){cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : StrictMember.extend a✝ h₁ = StrictMember.final h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝) =
    ⊤

case strict.strict
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝¹ : ID
a✝¹ : StrictMember Component.rtr i✝¹ rtr
h₁ : object (strict a✝¹){cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.extend a✝¹ h₁ = StrictMember.extend a✝ h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝¹
    | Component.rcn => i✝¹
    | Component.val v => i✝¹) =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝
Theorem: Reactor.Member.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : o₁ = o₂
⊢ ⊤ = ⊤
Tactic:
case root.root     => rfl
Proof state after:
no goals
Theorem: Reactor.Member.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝¹ : ID
a✝¹ : StrictMember Component.rtr i✝¹ rtr
h₁ : object (strict a✝¹){cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.extend a✝¹ h₁ = StrictMember.extend a✝ h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝¹
    | Component.rcn => i✝¹
    | Component.val v => i✝¹) =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝
Tactic:
case strict.strict => simp [StrictMember.extend_inj h]
Proof state after:
no goals
Theorem: Reactor.Member.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.final h₁ = StrictMember.extend a✝ h₂
⊢ ⊤ =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝
Tactic:
case root.strict   => exact absurd h.symm $ StrictMember.extend_not_final _ _ _
Proof state after:
no goals
Theorem: Reactor.Member.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₁ : object (strict a✝){cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : StrictMember.extend a✝ h₁ = StrictMember.final h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝) =
    ⊤
Tactic:
case strict.root   => exact absurd h $ StrictMember.extend_not_final _ _ _
Proof state after:
no goals
Theorem: Reactor.Member.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : o₁ = o₂
⊢ ⊤ = ⊤
Tactic:
rfl
Proof state after:
no goals
Theorem: Reactor.Member.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝¹ : ID
a✝¹ : StrictMember Component.rtr i✝¹ rtr
h₁ : object (strict a✝¹){cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.extend a✝¹ h₁ = StrictMember.extend a✝ h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝¹
    | Component.rcn => i✝¹
    | Component.val v => i✝¹) =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝
Tactic:
simp [StrictMember.extend_inj h]
Proof state after:
no goals
Theorem: Reactor.Member.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
h₁ : object root{cpt}{j} = some o₁
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₂ : object (strict a✝){cpt}{j} = some o₂
h : StrictMember.final h₁ = StrictMember.extend a✝ h₂
⊢ ⊤ =
    match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝
Tactic:
exact absurd h.symm $ StrictMember.extend_not_final _ _ _
Proof state after:
no goals
Theorem: Reactor.Member.extend_inj
Proof state before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
i✝ : ID
a✝ : StrictMember Component.rtr i✝ rtr
h₁ : object (strict a✝){cpt}{j} = some o₁
h₂ : object root{cpt}{j} = some o₂
h : StrictMember.extend a✝ h₁ = StrictMember.final h₂
⊢ (match Component.rtr with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝) =
    ⊤
Tactic:
exact absurd h $ StrictMember.extend_not_final _ _ _
Proof state after:
no goals
Theorem: Reactor.Member.Equivalent.symm
Proof state before:
α : Type
inst✝¹ : Reactor α
rtr rtr₁ : α
β : Type
cpt : Component
i : Component.idType cpt
inst✝ : Reactor β
rtr₂ : β
m₁ : Member cpt i rtr₁
m₂ : Member cpt i rtr₂
e : m₁ ∼ m₂
⊢ m₂ ∼ m₁
Tactic:
cases m₁
Proof state after:
case root
α : Type
inst✝¹ : Reactor α
rtr rtr₁ : α
β : Type
inst✝ : Reactor β
rtr₂ : β
m₂ : Member Component.rtr ⊤ rtr₂
e : Member.root ∼ m₂
⊢ m₂ ∼ Member.root

case strict
α : Type
inst✝¹ : Reactor α
rtr rtr₁ : α
β : Type
cpt : Component
inst✝ : Reactor β
rtr₂ : β
i✝ : ID
m₂ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₂
a✝ : StrictMember cpt i✝ rtr₁
e : Member.strict a✝ ∼ m₂
⊢ m₂ ∼ Member.strict a✝
Theorem: Reactor.Member.Equivalent.symm
Proof state before:
α : Type
inst✝¹ : Reactor α
rtr rtr₁ : α
β : Type
inst✝ : Reactor β
rtr₂ : β
m₂ : Member Component.rtr ⊤ rtr₂
e : Member.root ∼ m₂
⊢ m₂ ∼ Member.root
Tactic:
case root => cases m₂; exact root
Proof state after:
no goals
Theorem: Reactor.Member.Equivalent.symm
Proof state before:
α : Type
inst✝¹ : Reactor α
rtr rtr₁ : α
β : Type
cpt : Component
inst✝ : Reactor β
rtr₂ : β
i✝ : ID
m₂ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₂
a✝ : StrictMember cpt i✝ rtr₁
e : Member.strict a✝ ∼ m₂
⊢ m₂ ∼ Member.strict a✝
Tactic:
case strict => cases cpt <;> cases e <;> exact .strict $ StrictMember.Equivalent.symm ‹_›
Proof state after:
no goals
Theorem: Reactor.Member.Equivalent.symm
Proof state before:
α : Type
inst✝¹ : Reactor α
rtr rtr₁ : α
β : Type
inst✝ : Reactor β
rtr₂ : β
m₂ : Member Component.rtr ⊤ rtr₂
e : Member.root ∼ m₂
⊢ m₂ ∼ Member.root
Tactic:
cases m₂
Proof state after:
case root
α : Type
inst✝¹ : Reactor α
rtr rtr₁ : α
β : Type
inst✝ : Reactor β
rtr₂ : β
e : Member.root ∼ Member.root
⊢ Member.root ∼ Member.root
Theorem: Reactor.Member.Equivalent.symm
Proof state before:
case root
α : Type
inst✝¹ : Reactor α
rtr rtr₁ : α
β : Type
inst✝ : Reactor β
rtr₂ : β
e : Member.root ∼ Member.root
⊢ Member.root ∼ Member.root
Tactic:
exact root
Proof state after:
no goals
Theorem: Reactor.Member.Equivalent.symm
Proof state before:
α : Type
inst✝¹ : Reactor α
rtr rtr₁ : α
β : Type
cpt : Component
inst✝ : Reactor β
rtr₂ : β
i✝ : ID
m₂ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₂
a✝ : StrictMember cpt i✝ rtr₁
e : Member.strict a✝ ∼ m₂
⊢ m₂ ∼ Member.strict a✝
Tactic:
cases cpt <;> cases e <;> exact .strict $ StrictMember.Equivalent.symm ‹_›
Proof state after:
no goals
Theorem: Reactor.Member.Equivalent.trans
Proof state before:
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
cpt : Component
i : Component.idType cpt
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
m₁ : Member cpt i rtr₁
m₂ : Member cpt i rtr₂
m₃ : Member cpt i rtr₃
e₁ : m₁ ∼ m₂
e₂ : m₂ ∼ m₃
⊢ m₁ ∼ m₃
Tactic:
cases m₁
Proof state after:
case root
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
m₂ : Member Component.rtr ⊤ rtr₂
m₃ : Member Component.rtr ⊤ rtr₃
e₂ : m₂ ∼ m₃
e₁ : Member.root ∼ m₂
⊢ Member.root ∼ m₃

case strict
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
cpt : Component
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
i✝ : ID
m₂ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₂
m₃ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₃
e₂ : m₂ ∼ m₃
a✝ : StrictMember cpt i✝ rtr₁
e₁ : Member.strict a✝ ∼ m₂
⊢ Member.strict a✝ ∼ m₃
Theorem: Reactor.Member.Equivalent.trans
Proof state before:
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
m₂ : Member Component.rtr ⊤ rtr₂
m₃ : Member Component.rtr ⊤ rtr₃
e₂ : m₂ ∼ m₃
e₁ : Member.root ∼ m₂
⊢ Member.root ∼ m₃
Tactic:
case root => cases m₃; exact root
Proof state after:
no goals
Theorem: Reactor.Member.Equivalent.trans
Proof state before:
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
cpt : Component
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
i✝ : ID
m₂ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₂
m₃ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₃
e₂ : m₂ ∼ m₃
a✝ : StrictMember cpt i✝ rtr₁
e₁ : Member.strict a✝ ∼ m₂
⊢ Member.strict a✝ ∼ m₃
Tactic:
case strict =>
  cases cpt <;> cases e₁ <;> cases e₂ <;> exact .strict $ StrictMember.Equivalent.trans ‹_› ‹_›
Proof state after:
no goals
Theorem: Reactor.Member.Equivalent.trans
Proof state before:
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
m₂ : Member Component.rtr ⊤ rtr₂
m₃ : Member Component.rtr ⊤ rtr₃
e₂ : m₂ ∼ m₃
e₁ : Member.root ∼ m₂
⊢ Member.root ∼ m₃
Tactic:
cases m₃
Proof state after:
case root
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
m₂ : Member Component.rtr ⊤ rtr₂
e₁ : Member.root ∼ m₂
e₂ : m₂ ∼ Member.root
⊢ Member.root ∼ Member.root
Theorem: Reactor.Member.Equivalent.trans
Proof state before:
case root
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
m₂ : Member Component.rtr ⊤ rtr₂
e₁ : Member.root ∼ m₂
e₂ : m₂ ∼ Member.root
⊢ Member.root ∼ Member.root
Tactic:
exact root
Proof state after:
no goals
Theorem: Reactor.Member.Equivalent.trans
Proof state before:
α : Type
inst✝² : Reactor α
rtr rtr₁ : α
β γ : Type
cpt : Component
inst✝¹ : Reactor β
inst✝ : Reactor γ
rtr₂ : β
rtr₃ : γ
i✝ : ID
m₂ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₂
m₃ :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i✝
    | Component.rcn => i✝
    | Component.val v => i✝)
    rtr₃
e₂ : m₂ ∼ m₃
a✝ : StrictMember cpt i✝ rtr₁
e₁ : Member.strict a✝ ∼ m₂
⊢ Member.strict a✝ ∼ m₃
Tactic:
cases cpt <;> cases e₁ <;> cases e₂ <;> exact .strict $ StrictMember.Equivalent.trans ‹_› ‹_›
Proof state after:
no goals
Theorem: Reactor.Object.strict_elim
Proof state before:
α : Type
inst✝ : Reactor α
rtr rtr₁ : α
cpt : Component
o : Component.type α cpt
i : ID
m :
  Member cpt
    (match cpt with
    | Component.rtr => ↑i
    | Component.rcn => i
    | Component.val v => i)
    rtr
⊢ ∃ s, StrictMember.object s = Member.object m
Tactic:
cases cpt <;> cases m <;> exists ‹_›
Proof state after:
no goals
Theorem: Reactor.StrictMember.unique
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
s₁ s₂ : StrictMember cpt i rtr
⊢ s₁ = s₂
Tactic:
injection unique_ids.allEq (.strict s₁) (.strict s₂)
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ rtr₂ : α
cpt : Component
i : ID
e : rtr₁ ≈ rtr₂
s₁ : StrictMember cpt i rtr₁
s₂ : StrictMember cpt i rtr₂
⊢ s₁ ∼ s₂
Tactic:
induction s₁ generalizing rtr₂ <;> cases s₂
Proof state after:
case final.final
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝¹ : Component.type α cpt
a✝¹ : rtr✝{cpt}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α cpt
a✝ : rtr₂{cpt}{i} = some o✝
⊢ final a✝¹ ∼ final a✝

case final.nested
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝ : Component.type α cpt
a✝² : rtr✝{cpt}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember cpt i rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ final a✝² ∼ nested a✝ a✝¹

case nested.final
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr₁✝ : α
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝² : rtr₁✝{Component.rtr}{j✝} = some rtr₂✝
a✝¹ : StrictMember cpt i rtr₂✝
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), a✝¹ ∼ s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
o✝ : Component.type α cpt
a✝ : rtr₂{cpt}{i} = some o✝
⊢ nested a✝² a✝¹ ∼ final a✝

case nested.nested
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr₁✝ : α
j✝¹ : ID
rtr₂✝¹ : Component.type α Component.rtr
a✝³ : rtr₁✝{Component.rtr}{j✝¹} = some rtr₂✝¹
a✝² : StrictMember cpt i rtr₂✝¹
a_ih✝ : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), a✝² ∼ s₂
rtr₂ : α
e : rtr₁✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
a✝¹ : StrictMember cpt i rtr₂✝
a✝ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ nested a✝³ a✝² ∼ nested a✝ a✝¹
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝¹ : Component.type α cpt
a✝¹ : rtr✝{cpt}{i} = some o✝¹
rtr₂ : α
e : rtr✝ ≈ rtr₂
o✝ : Component.type α cpt
a✝ : rtr₂{cpt}{i} = some o✝
⊢ final a✝¹ ∼ final a✝
Tactic:
case final.final => constructor
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁✝ : α
cpt : Component
i : ID
rtr₁ : α
j₁ : ID
rtr₂✝¹ : Component.type α Component.rtr
h₁ : rtr₁{Component.rtr}{j₁} = some rtr₂✝¹
s₁ : StrictMember cpt i rtr₂✝¹
hi : ∀ {rtr₂ : α}, rtr₂✝¹ ≈ rtr₂ → ∀ (s₂ : StrictMember cpt i rtr₂), s₁ ∼ s₂
rtr₂ : α
e : rtr₁ ≈ rtr₂
j₂ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j₂} = some rtr₂✝
⊢ nested h₁ s₁ ∼ nested h₂ s₂
Tactic:
case nested.nested rtr₁ j₁ _ h₁ s₁ hi j₂ _ s₂ h₂ =>
  suffices hj : j₁ = j₂ by 
    subst hj
    exact Equivalent.nested h₁ h₂ $ hi (Equivalent.get?_rtr_some_equiv e h₁ h₂) s₂
  have hs := (nested h₁ s₁ |>.fromEquiv e).unique (nested h₂ s₂)
  simp [fromEquiv] at hs
  exact hs.left
Proof state after:
no goals
Theorem: Reactor.StrictMember.equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr rtr₁ : α
cpt : Component
i : ID
rtr✝ : α
o✝ : Component.type α cpt
h₁ : rtr✝{cpt}{i} = some o✝
rtr₂ : α
e : rtr✝ ≈ rtr₂
j✝ : ID
rtr₂✝ : Component.type α Component.rtr
s₂ : StrictMember cpt i rtr₂✝
h₂ : rtr₂{Component.rtr}{j✝} = some rtr₂✝
⊢ final h₁ ∼ nested h₂ s₂
Tactic:
case final.nested h₁ _ _ s₂ h₂ => 
  injection (final h₁ |>.fromEquiv e).unique (nested h₂ s₂)
Proof state after:
no goals