Theorem: Reactor.Object.iff_obj?_some (ReactorModel/Objects/Reactor/Theorems/Hierarchical.lean)

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
⊢ Object rtr cpt i o → rtr[cpt][i] = some o
Tactic:
intro ⟨m⟩
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
⊢ rtr[cpt][i] = some (Member.object m)

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
⊢ rtr[cpt][i] = some (Member.object m)
Tactic:
simp [obj?]
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
⊢ (if h : ∃ o, Object rtr cpt i o then some (Exists.choose h) else none) = some (Member.object m)

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
⊢ (if h : ∃ o, Object rtr cpt i o then some (Exists.choose h) else none) = some (Member.object m)
Tactic:
split
State after:
case inl
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h✝ : ∃ o, Object rtr cpt i o
⊢ some (Exists.choose h✝) = some (Member.object m)

case inr
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h✝ : ¬∃ o, Object rtr cpt i o
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∃ o, Object rtr cpt i o
⊢ some (Exists.choose h) = some (Member.object m)
Tactic:
case inl h =>
  have ⟨m', h'⟩ := Object.def.mp h.choose_spec
  simp [←h', m.unique m']
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ¬∃ o, Object rtr cpt i o
⊢ False
Tactic:
case inr h =>
  push_neg at h
  specialize h m.object
  simp [Object.def] at h
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∃ o, Object rtr cpt i o
⊢ some (Exists.choose h) = some (Member.object m)
Tactic:
have ⟨m', h'⟩ := Object.def.mp h.choose_spec
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∃ o, Object rtr cpt i o
m' : Member cpt i rtr
h' : Member.object m' = Exists.choose h
⊢ some (Exists.choose h) = some (Member.object m)

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∃ o, Object rtr cpt i o
m' : Member cpt i rtr
h' : Member.object m' = Exists.choose h
⊢ some (Exists.choose h) = some (Member.object m)
Tactic:
simp [←h', m.unique m']
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ¬∃ o, Object rtr cpt i o
⊢ False
Tactic:
push_neg at h
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∀ (o : Component.type α cpt), ¬Object rtr cpt i o
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ∀ (o : Component.type α cpt), ¬Object rtr cpt i o
⊢ False
Tactic:
specialize h m.object
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ¬Object rtr cpt i (Member.object m)
⊢ False

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
m : Member cpt i rtr
h : ¬Object rtr cpt i (Member.object m)
⊢ False
Tactic:
simp [Object.def] at h
State after:
no goals

State before:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
h : rtr[cpt][i] = some o
⊢ Object rtr cpt i o
Tactic:
simp [obj?] at h
State after:
α : Type
inst✝ : Hierarchical α
rtr : α
cpt : Component
i : Component.idType cpt
o : Component.type α cpt
h : (if h : ∃ o, Object rtr cpt i o then some (Exists.choose h) else none) = some o
⊢ Object rtr cpt i o

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
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

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
State after:
no goals

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'⟩
State after:
no goals

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
State after:
no goals

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
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

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'⟩
State after:
no goals