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

State before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
i : ID
cpt : Component.Valued
ids : List ID
c : Component.Valued
o : Component.type α (Component.val c)
vs : ID ⇀ Value
ho : rtr[Component.val c][i] = some o
h : c ≠ cpt ∨ i ∉ ids ∨ vs i = none
⊢ go rtr cpt vs ids[Component.val c][i] = some o
Tactic:
induction ids generalizing rtr o <;> simp_all [go]
State after:
case cons
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
h : ¬c = cpt ∨ ¬(i = head✝ ∨ i ∈ tail✝) ∨ vs i = none
⊢ (match vs head✝ with
      | none => go rtr cpt vs tail✝
      | some v => go (update rtr cpt head✝ v) cpt vs tail✝)[Component.val c][i] =
    some o

State before:
case cons
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
h : ¬c = cpt ∨ ¬(i = head✝ ∨ i ∈ tail✝) ∨ vs i = none
⊢ (match vs head✝ with
      | none => go rtr cpt vs tail✝
      | some v => go (update rtr cpt head✝ v) cpt vs tail✝)[Component.val c][i] =
    some o
Tactic:
split <;> cases h <;> try cases ‹_ ∨ _›
State after:
case cons.h_1.inl
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
heq✝ : vs head✝ = none
h✝ : ¬c = cpt
⊢ go rtr cpt vs tail✝[Component.val c][i] = some o

case cons.h_1.inr.inl
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
heq✝ : vs head✝ = none
h✝ : ¬(i = head✝ ∨ i ∈ tail✝)
⊢ go rtr cpt vs tail✝[Component.val c][i] = some o

case cons.h_1.inr.inr
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
heq✝ : vs head✝ = none
h✝ : vs i = none
⊢ go rtr cpt vs tail✝[Component.val c][i] = some o

case cons.h_2.inl
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v✝ : Value
heq✝ : vs head✝ = some v✝
h✝ : ¬c = cpt
⊢ go (update rtr cpt head✝ v✝) cpt vs tail✝[Component.val c][i] = some o

case cons.h_2.inr.inl
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v✝ : Value
heq✝ : vs head✝ = some v✝
h✝ : ¬(i = head✝ ∨ i ∈ tail✝)
⊢ go (update rtr cpt head✝ v✝) cpt vs tail✝[Component.val c][i] = some o

case cons.h_2.inr.inr
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v✝ : Value
heq✝ : vs head✝ = some v✝
h✝ : vs i = none
⊢ go (update rtr cpt head✝ v✝) cpt vs tail✝[Component.val c][i] = some o

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
heq✝ : vs head✝ = none
h : ¬c = cpt
⊢ go rtr cpt vs tail✝[Component.val c][i] = some o
Tactic:
case _ hi _ _ h => exact hi ho $ .inl h
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
heq✝ : vs head✝ = none
h : ¬(i = head✝ ∨ i ∈ tail✝)
⊢ go rtr cpt vs tail✝[Component.val c][i] = some o
Tactic:
case _ hi _ _ h => exact hi ho $ .inr $ .inl (not_or.mp h).right
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
heq✝ : vs head✝ = none
h : vs i = none
⊢ go rtr cpt vs tail✝[Component.val c][i] = some o
Tactic:
case _ hi _ _ h => exact hi ho $ .inr $ .inr h
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬c = cpt
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
case inl hd tl hi _ v _ h =>
  have e := @LawfulUpdatable.equiv _ cpt ‹_› v _ rtr
  have ⟨_, ho'⟩ := Equivalent.obj?_some_iff e |>.mp ⟨_, ho⟩
  simp [hi ho' $ .inl h]
  injection ho' ▸ ho ▸ obj?_preserved_cpt h
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬(i = hd ∨ i ∈ tl)
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
case inr.inl hd tl hi _ v _ h =>
  have e := @LawfulUpdatable.equiv _ cpt ‹_› v _ rtr
  have ⟨_, ho'⟩ := Equivalent.obj?_some_iff e |>.mp ⟨_, ho⟩
  push_neg at h
  simp [hi ho' $ .inr $ .inl h.right]
  injection ho' ▸ ho ▸ obj?_preserved_id h.left
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
case inr.inr hd tl hi _ v _ h =>
  have hh : i ≠ hd := by by_contra; simp_all
  have ho' := ho ▸ (@LawfulUpdatable.lawful _ _ rtr cpt hd v).obj?_preserved (c := c) (.inr hh)
  exact hi ho' (.inr $ .inr h)
State after:
no goals

State before:
case cons.h_2.inr
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v✝ : Value
heq✝ : vs head✝ = some v✝
h✝ : ¬(i = head✝ ∨ i ∈ tail✝) ∨ vs i = none
⊢ go (update rtr cpt head✝ v✝) cpt vs tail✝[Component.val c][i] = some o
Tactic:
cases ‹_ ∨ _›
State after:
case cons.h_2.inr.inl
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v✝ : Value
heq✝ : vs head✝ = some v✝
h✝ : ¬(i = head✝ ∨ i ∈ tail✝)
⊢ go (update rtr cpt head✝ v✝) cpt vs tail✝[Component.val c][i] = some o

case cons.h_2.inr.inr
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
tail_ih✝ :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v✝ : Value
heq✝ : vs head✝ = some v✝
h✝ : vs i = none
⊢ go (update rtr cpt head✝ v✝) cpt vs tail✝[Component.val c][i] = some o

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
heq✝ : vs head✝ = none
h : ¬c = cpt
⊢ go rtr cpt vs tail✝[Component.val c][i] = some o
Tactic:
exact hi ho $ .inl h
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
heq✝ : vs head✝ = none
h : ¬(i = head✝ ∨ i ∈ tail✝)
⊢ go rtr cpt vs tail✝[Component.val c][i] = some o
Tactic:
exact hi ho $ .inr $ .inl (not_or.mp h).right
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o →
      ¬c = cpt ∨ i ∉ tail✝ ∨ vs i = none → go rtr cpt vs tail✝[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
heq✝ : vs head✝ = none
h : vs i = none
⊢ go rtr cpt vs tail✝[Component.val c][i] = some o
Tactic:
exact hi ho $ .inr $ .inr h
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬c = cpt
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
have e := @LawfulUpdatable.equiv _ cpt ‹_› v _ rtr
State after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬c = cpt
e : rtr ≈ update rtr cpt hd v
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬c = cpt
e : rtr ≈ update rtr cpt hd v
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
have ⟨_, ho'⟩ := Equivalent.obj?_some_iff e |>.mp ⟨_, ho⟩
State after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬c = cpt
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬c = cpt
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
simp [hi ho' $ .inl h]
State after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬c = cpt
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
⊢ w✝ = o

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬c = cpt
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
⊢ w✝ = o
Tactic:
injection ho' ▸ ho ▸ obj?_preserved_cpt h
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬(i = hd ∨ i ∈ tl)
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
have e := @LawfulUpdatable.equiv _ cpt ‹_› v _ rtr
State after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬(i = hd ∨ i ∈ tl)
e : rtr ≈ update rtr cpt hd v
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬(i = hd ∨ i ∈ tl)
e : rtr ≈ update rtr cpt hd v
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
have ⟨_, ho'⟩ := Equivalent.obj?_some_iff e |>.mp ⟨_, ho⟩
State after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬(i = hd ∨ i ∈ tl)
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : ¬(i = hd ∨ i ∈ tl)
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
push_neg at h
State after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
h : i ≠ hd ∧ i ∉ tl
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
h : i ≠ hd ∧ i ∉ tl
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
simp [hi ho' $ .inr $ .inl h.right]
State after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
h : i ≠ hd ∧ i ∉ tl
⊢ w✝ = o

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val c)
ho' : update rtr cpt hd v[Component.val c][i] = some w✝
h : i ≠ hd ∧ i ∉ tl
⊢ w✝ = o
Tactic:
injection ho' ▸ ho ▸ obj?_preserved_id h.left
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
have hh : i ≠ hd := by by_contra; simp_all
State after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
hh : i ≠ hd
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
hh : i ≠ hd
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
have ho' := ho ▸ (@LawfulUpdatable.lawful _ _ rtr cpt hd v).obj?_preserved (c := c) (.inr hh)
State after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
hh : i ≠ hd
ho' : update rtr cpt hd v[Component.val c][i] = some o
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
hh : i ≠ hd
ho' : update rtr cpt hd v[Component.val c][i] = some o
⊢ go (update rtr cpt hd v) cpt vs tl[Component.val c][i] = some o
Tactic:
exact hi ho' (.inr $ .inr h)
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
⊢ i ≠ hd
Tactic:
by_contra
State after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
a✝ : i = hd
⊢ False

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
i : ID
cpt c : Component.Valued
vs : ID ⇀ Value
hd : ID
tl : List ID
rtr : α
o : Component.type α (Component.val c)
hi :
  ∀ {rtr : α} {o : Component.type α (Component.val c)},
    rtr[Component.val c][i] = some o → ¬c = cpt ∨ i ∉ tl ∨ vs i = none → go rtr cpt vs tl[Component.val c][i] = some o
ho : rtr[Component.val c][i] = some o
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
h : vs i = none
a✝ : i = hd
⊢ False
Tactic:
simp_all
State after:
no goals