Theorem: Reactor.set_updated (ReactorModel/Objects/Reactor/Theorems/Accessible.lean)

State before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
⊢ set rtr cpt vs[Component.val cpt] = vs
Tactic:
simp [set_updated', bind, Option.bind]
State after:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
⊢ (fun i =>
      match rtr[Component.val cpt][i], fun x => some (Option.getD (vs i) x) with
      | none, x => none
      | some a, b => b a) =
    vs

State before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
⊢ (fun i =>
      match rtr[Component.val cpt][i], fun x => some (Option.getD (vs i) x) with
      | none, x => none
      | some a, b => b a) =
    vs
Tactic:
ext1 i
State after:
case h
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
⊢ (match rtr[Component.val cpt][i], fun x => some (Option.getD (vs i) x) with
    | none, x => none
    | some a, b => b a) =
    vs i

State before:
case h
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
⊢ (match rtr[Component.val cpt][i], fun x => some (Option.getD (vs i) x) with
    | none, x => none
    | some a, b => b a) =
    vs i
Tactic:
split
State after:
case h.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
heq✝ : rtr[Component.val cpt][i] = none
⊢ none = vs i

case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
heq✝ : rtr[Component.val cpt][i] = some a✝
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i

State before:
case h.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
heq✝ : rtr[Component.val cpt][i] = none
⊢ none = vs i

case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
heq✝ : rtr[Component.val cpt][i] = some a✝
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
all_goals
  case' _ hn =>
    simp [Partial.ids, Set.ext_iff] at h
    specialize h i
    simp [hn] at h
State after:
case h.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
hn : rtr[Component.val cpt][i] = none
h : ∀ (x : Value), ¬vs i = some x
⊢ none = vs i

case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : ∃ b, vs i = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i

State before:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
heq✝ : rtr[Component.val cpt][i] = some a✝
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
case' _ hn =>
  simp [Partial.ids, Set.ext_iff] at h
  specialize h i
  simp [hn] at h
State after:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : ∃ b, vs i = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i

State before:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
h : Partial.ids vs = Partial.ids (rtr[Component.val cpt])
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
simp [Partial.ids, Set.ext_iff] at h
State after:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : ∀ (x : ID), (∃ b, vs x = some b) ↔ ∃ b, rtr[Component.val cpt][x] = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i

State before:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : ∀ (x : ID), (∃ b, vs x = some b) ↔ ∃ b, rtr[Component.val cpt][x] = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
specialize h i
State after:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : (∃ b, vs i = some b) ↔ ∃ b, rtr[Component.val cpt][i] = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i

State before:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : (∃ b, vs i = some b) ↔ ∃ b, rtr[Component.val cpt][i] = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
simp [hn] at h
State after:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : ∃ b, vs i = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i

State before:
case h.h_1
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
hn : rtr[Component.val cpt][i] = none
h : ∀ (x : Value), ¬vs i = some x
⊢ none = vs i
Tactic:
exact Option.eq_none_iff_forall_not_mem.mpr h |>.symm
State after:
no goals

State before:
case h.h_2
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
h : ∃ b, vs i = some b
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
obtain ⟨_, h⟩ := h
State after:
case h.h_2.intro
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
w✝ : Value
h : vs i = some w✝
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i

State before:
case h.h_2.intro
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
vs : ID ⇀ Value
cpt : Component.Valued
i : Component.idType (Component.val cpt)
x✝¹ : Option (Component.type α (Component.val cpt))
x✝ : Component.type α (Component.val cpt) → Option (Component.type α (Component.val cpt))
a✝ : Component.type α (Component.val cpt)
hn : rtr[Component.val cpt][i] = some a✝
w✝ : Value
h : vs i = some w✝
⊢ (fun x => some (Option.getD (vs i) x)) a✝ = vs i
Tactic:
simp [h]
State after:
no goals