internlm/Lean-Github huggingface dataset:
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : 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
Tactic:
split at h
Proof state after:
case inl
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
h✝ : ∃ o, Object rtr cpt i o
h : some (Exists.choose h✝) = some o
⊢ Object rtr cpt i o

case inr
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
h✝ : ¬∃ o, Object rtr cpt i o
h : False
⊢ Object rtr cpt i o
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
h✝ : ¬∃ o, Object rtr cpt i o
h : False
⊢ Object rtr cpt i o
Tactic:
case inr => contradiction
Proof state after:
no goals
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
h✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
h' : ∃ o, Object rtr cpt i o
h : some (Exists.choose h') = some o
⊢ Object rtr cpt i o
Tactic:
case inl h h' => 
  have ⟨m', h'⟩ := Object.def.mp h'.choose_spec
  exact Option.some_inj.mp h ▸ h' ▸ ⟨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
h✝ : ¬∃ o, Object rtr cpt i o
h : False
⊢ Object rtr cpt i o
Tactic:
contradiction
Proof state after:
no goals
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
h✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
h' : ∃ o, Object rtr cpt i o
h : some (Exists.choose h') = some o
⊢ Object rtr cpt i o
Tactic:
have ⟨m', h'⟩ := Object.def.mp h'.choose_spec
Proof state after:
α : Type
h✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
h'✝ : ∃ o, Object rtr cpt i o
h : some (Exists.choose h'✝) = some o
m' : Member cpt i rtr
h' : Member.object m' = Exists.choose h'✝
⊢ Object rtr cpt i o
Theorem: Reactor.Object.iff_obj?_some
Proof state before:
α : Type
h✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
h'✝ : ∃ o, Object rtr cpt i o
h : some (Exists.choose h'✝) = some o
m' : Member cpt i rtr
h' : Member.object m' = Exists.choose h'✝
⊢ Object rtr cpt i o
Tactic:
exact Option.some_inj.mp h ▸ h' ▸ ⟨m'⟩
Proof state after:
no goals
Theorem: Reactor.Object.not_iff_obj?_none
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] = none
Tactic:
simp [Option.eq_none_iff_forall_not_mem, iff_obj?_some]
Proof state after:
no goals
Theorem: Reactor.Hierarchical.obj?_some_nested
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
cpt : Component
o : Component.type (Component.type α Component.rtr) cpt
i' : ID
h : rtr{Component.rtr}{i} = some rtr'
ho :
  rtr'[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
Tactic:
have ⟨s, hs⟩ := Object.strict_elim $ Object.iff_obj?_some.mpr ho
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
cpt : Component
o : Component.type (Component.type α Component.rtr) cpt
i' : ID
h : rtr{Component.rtr}{i} = some rtr'
ho :
  rtr'[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
s : StrictMember cpt i' rtr'
hs : StrictMember.object s = o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
Theorem: Reactor.Hierarchical.obj?_some_nested
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
cpt : Component
o : Component.type (Component.type α Component.rtr) cpt
i' : ID
h : rtr{Component.rtr}{i} = some rtr'
ho :
  rtr'[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
s : StrictMember cpt i' rtr'
hs : StrictMember.object s = o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i'
      | Component.rcn => i'
      | Component.val v => i'] =
    some o
Tactic:
exact Object.iff_obj?_some.mp $ hs ▸ ⟨.nested h s⟩
Proof state after:
no goals
Theorem: Reactor.Hierarchical.obj?_some_nested'
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
cpt : Component
i' : Component.idType cpt
o : Component.type (Component.type α Component.rtr) cpt
h : rtr{Component.rtr}{i} = some rtr'
ho : rtr'[cpt][i'] = some o
⊢ ∃ j, rtr[cpt][j] = some o
Tactic:
cases cpt <;> try cases i'
Proof state after:
case val
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
v✝ : Component.Valued
i' : Component.idType (Component.val v✝)
o : Component.type (Component.type α Component.rtr) (Component.val v✝)
ho : rtr'[Component.val v✝][i'] = some o
⊢ ∃ j, rtr[Component.val v✝][j] = some o

case rtr.none
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o

case rtr.some
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
val✝ : ID
ho : rtr'[Component.rtr][some val✝] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o

case rcn
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
i' : Component.idType Component.rcn
o : Component.type (Component.type α Component.rtr) Component.rcn
ho : rtr'[Component.rcn][i'] = some o
⊢ ∃ j, rtr[Component.rcn][j] = some o
Theorem: Reactor.Hierarchical.obj?_some_nested'
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o
Tactic:
case rtr.none =>
  exists i
  exact Object.iff_obj?_some.mp $ obj?_root_some ho ▸ ⟨.final h⟩
Proof state after:
no goals
Theorem: Reactor.Hierarchical.obj?_some_nested'
Proof state before:
case val
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
v✝ : Component.Valued
i' : Component.idType (Component.val v✝)
o : Component.type (Component.type α Component.rtr) (Component.val v✝)
ho : rtr'[Component.val v✝][i'] = some o
⊢ ∃ j, rtr[Component.val v✝][j] = some o

case rtr.some
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
val✝ : ID
ho : rtr'[Component.rtr][some val✝] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o

case rcn
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
i' : Component.idType Component.rcn
o : Component.type (Component.type α Component.rtr) Component.rcn
ho : rtr'[Component.rcn][i'] = some o
⊢ ∃ j, rtr[Component.rcn][j] = some o
Tactic:
all_goals 
  exact ⟨_, obj?_some_nested h ho⟩
Proof state after:
no goals
Theorem: Reactor.Hierarchical.obj?_some_nested'
Proof state before:
case rtr
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
i' : Component.idType Component.rtr
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][i'] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o
Tactic:
cases i'
Proof state after:
case rtr.none
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o

case rtr.some
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
val✝ : ID
ho : rtr'[Component.rtr][some val✝] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o
Theorem: Reactor.Hierarchical.obj?_some_nested'
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ ∃ j, rtr[Component.rtr][j] = some o
Tactic:
exists i
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ rtr[Component.rtr][↑i] = some o
Theorem: Reactor.Hierarchical.obj?_some_nested'
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
o : Component.type (Component.type α Component.rtr) Component.rtr
ho : rtr'[Component.rtr][none] = some o
⊢ rtr[Component.rtr][↑i] = some o
Tactic:
exact Object.iff_obj?_some.mp $ obj?_root_some ho ▸ ⟨.final h⟩
Proof state after:
no goals
Theorem: Reactor.Hierarchical.obj?_some_nested'
Proof state before:
case rcn
α : Type
inst✝ : Hierarchical α
rtr : α
i : ID
rtr' : Component.type α Component.rtr
h : rtr{Component.rtr}{i} = some rtr'
i' : Component.idType Component.rcn
o : Component.type (Component.type α Component.rtr) Component.rcn
ho : rtr'[Component.rcn][i'] = some o
⊢ ∃ j, rtr[Component.rcn][j] = some o
Tactic:
exact ⟨_, obj?_some_nested h ho⟩
Proof state after:
no goals
Theorem: Reactor.Hierarchical.obj?_some_extend
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
c : Component.idType Component.rtr
con : Component.type α Component.rtr
cpt : Component
i : ID
o : Component.type (Component.type α Component.rtr) cpt
ho : rtr[Component.rtr][c] = some con
hc : con{cpt}{i} = some o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some o
Tactic:
have ⟨m⟩ := Object.iff_obj?_some.mpr ho
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
c : Component.idType Component.rtr
cpt : Component
i : ID
o : Component.type (Component.type α Component.rtr) cpt
m : Member Component.rtr c rtr
ho : rtr[Component.rtr][c] = some (Member.object m)
hc : Member.object m{cpt}{i} = some o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some o
Theorem: Reactor.Hierarchical.obj?_some_extend
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
c : Component.idType Component.rtr
cpt : Component
i : ID
o : Component.type (Component.type α Component.rtr) cpt
m : Member Component.rtr c rtr
ho : rtr[Component.rtr][c] = some (Member.object m)
hc : Member.object m{cpt}{i} = some o
⊢ rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some o
Tactic:
exact Object.iff_obj?_some.mp $ m.extend_object hc ▸ ⟨m.extend hc⟩
Proof state after:
no goals
Theorem: Reactor.Hierarchical.obj?_some_split
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
o : Component.type α cpt
i : ID
ho :
  rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some o
⊢ ∃ c con, rtr[Component.rtr][c] = some con ∧ con{cpt}{i} = some o
Tactic:
have ⟨s, hs⟩ := Object.strict_elim $ Object.iff_obj?_some.mpr ho
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
o : Component.type α cpt
i : ID
ho :
  rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some o
s : StrictMember cpt i rtr
hs : StrictMember.object s = o
⊢ ∃ c con, rtr[Component.rtr][c] = some con ∧ con{cpt}{i} = some o
Theorem: Reactor.Hierarchical.obj?_some_split
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
o : Component.type α cpt
i : ID
ho :
  rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some o
s : StrictMember cpt i rtr
hs : StrictMember.object s = o
⊢ ∃ c con, rtr[Component.rtr][c] = some con ∧ con{cpt}{i} = some o
Tactic:
have ⟨c, ⟨m, hm⟩⟩ := s.split'
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
o : Component.type α cpt
i : ID
ho :
  rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some o
s : StrictMember cpt i rtr
hs : StrictMember.object s = o
c : WithTop ID
m : Member Component.rtr c rtr
hm : Member.object m{cpt}{i} = some (StrictMember.object s)
⊢ ∃ c con, rtr[Component.rtr][c] = some con ∧ con{cpt}{i} = some o
Theorem: Reactor.Hierarchical.obj?_some_split
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
o : Component.type α cpt
i : ID
ho :
  rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    some o
s : StrictMember cpt i rtr
hs : StrictMember.object s = o
c : WithTop ID
m : Member Component.rtr c rtr
hm : Member.object m{cpt}{i} = some (StrictMember.object s)
⊢ ∃ c con, rtr[Component.rtr][c] = some con ∧ con{cpt}{i} = some o
Tactic:
exact ⟨c, m.object, Object.iff_obj?_some.mp ⟨m⟩, hs ▸ hm⟩
Proof state after:
no goals
Theorem: Reactor.Hierarchical.get?_some_rtr_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
c₁ : Component.idType Component.rtr
con₁ : Component.type α Component.rtr
c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
ho₁ : rtr[Component.rtr][c₁] = some con₁
ho₂ : rtr[Component.rtr][c₂] = some con₂
hc₁ : con₁{cpt}{j} = some o₁
hc₂ : con₂{cpt}{j} = some o₂
⊢ c₁ = c₂
Tactic:
have ⟨m₁⟩ := Object.iff_obj?_some.mpr ho₁
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
c₁ c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
ho₂ : rtr[Component.rtr][c₂] = some con₂
hc₂ : con₂{cpt}{j} = some o₂
m₁ : Member Component.rtr c₁ rtr
ho₁ : rtr[Component.rtr][c₁] = some (Member.object m₁)
hc₁ : Member.object m₁{cpt}{j} = some o₁
⊢ c₁ = c₂
Theorem: Reactor.Hierarchical.get?_some_rtr_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
c₁ c₂ : Component.idType Component.rtr
con₂ : Component.type α Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
ho₂ : rtr[Component.rtr][c₂] = some con₂
hc₂ : con₂{cpt}{j} = some o₂
m₁ : Member Component.rtr c₁ rtr
ho₁ : rtr[Component.rtr][c₁] = some (Member.object m₁)
hc₁ : Member.object m₁{cpt}{j} = some o₁
⊢ c₁ = c₂
Tactic:
have ⟨m₂⟩ := Object.iff_obj?_some.mpr ho₂
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
c₁ c₂ : Component.idType Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
m₁ : Member Component.rtr c₁ rtr
ho₁ : rtr[Component.rtr][c₁] = some (Member.object m₁)
hc₁ : Member.object m₁{cpt}{j} = some o₁
m₂ : Member Component.rtr c₂ rtr
ho₂ : rtr[Component.rtr][c₂] = some (Member.object m₂)
hc₂ : Member.object m₂{cpt}{j} = some o₂
⊢ c₁ = c₂
Theorem: Reactor.Hierarchical.get?_some_rtr_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
c₁ c₂ : Component.idType Component.rtr
cpt : Component
j : ID
o₁ o₂ : Component.type (Component.type α Component.rtr) cpt
m₁ : Member Component.rtr c₁ rtr
ho₁ : rtr[Component.rtr][c₁] = some (Member.object m₁)
hc₁ : Member.object m₁{cpt}{j} = some o₁
m₂ : Member Component.rtr c₂ rtr
ho₂ : rtr[Component.rtr][c₂] = some (Member.object m₂)
hc₂ : Member.object m₂{cpt}{j} = some o₂
⊢ c₁ = c₂
Tactic:
exact Member.extend_inj $ (m₁.extend hc₁).unique (m₂.extend hc₂)
Proof state after:
no goals
Theorem: Reactor.Hierarchical.obj?_none_to_get?_none
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : ID
ho :
  rtr[cpt][match cpt with
      | Component.rtr => ↑i
      | Component.rcn => i
      | Component.val v => i] =
    none
⊢ rtr{cpt}{i} = none
Tactic:
replace ho := Object.not_iff_obj?_none.mpr ho
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : ID
ho :
  ∀ (o : Component.type α cpt),
    ¬Object rtr cpt
        (match cpt with
        | Component.rtr => ↑i
        | Component.rcn => i
        | Component.val v => i)
        o
⊢ rtr{cpt}{i} = none
Theorem: Reactor.Hierarchical.obj?_none_to_get?_none
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : ID
ho :
  ∀ (o : Component.type α cpt),
    ¬Object rtr cpt
        (match cpt with
        | Component.rtr => ↑i
        | Component.rcn => i
        | Component.val v => i)
        o
⊢ rtr{cpt}{i} = none
Tactic:
by_contra h
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : ID
ho :
  ∀ (o : Component.type α cpt),
    ¬Object rtr cpt
        (match cpt with
        | Component.rtr => ↑i
        | Component.rcn => i
        | Component.val v => i)
        o
h : ¬rtr{cpt}{i} = none
⊢ False
Theorem: Reactor.Hierarchical.obj?_none_to_get?_none
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : ID
ho :
  ∀ (o : Component.type α cpt),
    ¬Object rtr cpt
        (match cpt with
        | Component.rtr => ↑i
        | Component.rcn => i
        | Component.val v => i)
        o
h : ¬rtr{cpt}{i} = none
⊢ False
Tactic:
exact ho _ ⟨.final $ Option.ne_none_iff_exists.mp h |>.choose_spec.symm⟩
Proof state after:
no goals
Theorem: Reactor.Equivalent.obj?_some_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∃ o₁, rtr₁[cpt][i] = some o₁) ↔ ∃ o₂, rtr₂[cpt][i] = some o₂
Tactic:
simp [←Object.iff_obj?_some, Object.equiv_exists_object_iff e]
Proof state after:
no goals
Theorem: Reactor.Equivalent.mem_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ i ∈ rtr₁[cpt] ↔ i ∈ rtr₂[cpt]
Tactic:
simp [Partial.mem_iff, obj?_some_iff e]
Proof state after:
no goals
Theorem: Reactor.Equivalent.ids_eq
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
e : rtr₁ ≈ rtr₂
⊢ Partial.ids (rtr₁[cpt]) = Partial.ids (rtr₂[cpt])
Tactic:
ext1
Proof state after:
case h
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
e : rtr₁ ≈ rtr₂
x✝ : Component.idType cpt
⊢ x✝ ∈ Partial.ids (rtr₁[cpt]) ↔ x✝ ∈ Partial.ids (rtr₂[cpt])
Theorem: Reactor.Equivalent.ids_eq
Proof state before:
case h
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
e : rtr₁ ≈ rtr₂
x✝ : Component.idType cpt
⊢ x✝ ∈ Partial.ids (rtr₁[cpt]) ↔ x✝ ∈ Partial.ids (rtr₂[cpt])
Tactic:
exact mem_iff e
Proof state after:
no goals
Theorem: Reactor.Equivalent.obj?_none_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ rtr₁[cpt][i] = none ↔ rtr₂[cpt][i] = none
Tactic:
simp [←Object.not_iff_obj?_none]
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o) ↔ ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o
Theorem: Reactor.Equivalent.obj?_none_iff
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o) ↔ ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o
Tactic:
constructor
Proof state after:
case mp
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o) → ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o

case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o) → ∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o
Theorem: Reactor.Equivalent.obj?_none_iff
Proof state before:
case mp
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o) → ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o

case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o) → ∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o
Tactic:
all_goals
  intro h o ⟨m⟩
  refine h _ ⟨m.fromEquiv ?_⟩
Proof state after:
case mp
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₂
⊢ rtr₂ ≈ rtr₁

case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₁
⊢ rtr₁ ≈ rtr₂
Theorem: Reactor.Equivalent.obj?_none_iff
Proof state before:
case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
⊢ (∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o) → ∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o
Tactic:
intro h o ⟨m⟩
Proof state after:
case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₁
⊢ False
Theorem: Reactor.Equivalent.obj?_none_iff
Proof state before:
case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₁
⊢ False
Tactic:
refine h _ ⟨m.fromEquiv ?_⟩
Proof state after:
case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₁
⊢ rtr₁ ≈ rtr₂
Theorem: Reactor.Equivalent.obj?_none_iff
Proof state before:
case mp
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₁ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₂
⊢ rtr₂ ≈ rtr₁
Tactic:
exact Equivalent.symm e
Proof state after:
no goals
Theorem: Reactor.Equivalent.obj?_none_iff
Proof state before:
case mpr
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
cpt : Component
i : Component.idType cpt
e : rtr₁ ≈ rtr₂
h : ∀ (o : Component.type α cpt), ¬Object rtr₂ cpt i o
o : Component.type α cpt
m : Member cpt i rtr₁
⊢ rtr₁ ≈ rtr₂
Tactic:
exact e
Proof state after:
no goals
Theorem: Reactor.Equivalent.obj?_rtr_equiv
Proof state before:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
n₁ n₂ : Component.type α Component.rtr
e : rtr₁ ≈ rtr₂
h₁ : rtr₁[Component.rtr][i] = some n₁
h₂ : rtr₂[Component.rtr][i] = some n₂
⊢ n₁ ≈ n₂
Tactic:
have ⟨m₁⟩ := Object.iff_obj?_some.mpr h₁
Proof state after:
α : Type
inst✝ : Hierarchical α
rtr₁ rtr₂ : α
i : Component.idType Component.rtr
n₂ : Component.type α Component.rtr
e : rtr₁ ≈ rtr₂
h₂ : rtr₂[Component.rtr][i] = some n₂
m₁ : Member Component.rtr i rtr₁
h₁ : rtr₁[Component.rtr][i] = some (Member.object m₁)
⊢ Member.object m₁ ≈ n₂