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

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

State before:
case cons
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
tail_ih✝ :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
h : i = head✝ ∨ i ∈ tail✝
⊢ go rtr cpt vs (head✝ :: tail✝)[Component.val cpt][i] = some v
Tactic:
cases h
State after:
case cons.inl
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
tail_ih✝ :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
h✝ : i = head✝
⊢ go rtr cpt vs (head✝ :: tail✝)[Component.val cpt][i] = some v

case cons.inr
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
tail_ih✝ :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
h✝ : i ∈ tail✝
⊢ go rtr cpt vs (head✝ :: tail✝)[Component.val cpt][i] = some v

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
h : i = head✝
⊢ go rtr cpt vs (head✝ :: tl)[Component.val cpt][i] = some v
Tactic:
case cons.inl tl hi h =>
  subst h
  simp [go, hv]
  have e := @LawfulUpdatable.equiv _ cpt i v _ rtr
  have ⟨_, ho'⟩ := Equivalent.obj?_some_iff e |>.mp ⟨_, ho⟩
  by_cases ht : i ∈ tl
  case pos => exact hi ho' hv ht
  case neg => simp [set.go_preserves ho' (.inr $ .inl ht), ho' ▸ obj?_updated, ho]
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
h : i = head✝
⊢ go rtr cpt vs (head✝ :: tl)[Component.val cpt][i] = some v
Tactic:
subst h
State after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
⊢ go rtr cpt vs (i :: tl)[Component.val cpt][i] = some v

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
⊢ go rtr cpt vs (i :: tl)[Component.val cpt][i] = some v
Tactic:
simp [go, hv]
State after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v

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

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

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Tactic:
by_cases ht : i ∈ tl
State after:
case pos
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
ht : i ∈ tl
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v

case neg
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
ht : i ∉ tl
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
ht : i ∈ tl
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Tactic:
case pos => exact hi ho' hv ht
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
ht : i ∉ tl
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Tactic:
case neg => simp [set.go_preserves ho' (.inr $ .inl ht), ho' ▸ obj?_updated, ho]
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
ht : i ∈ tl
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Tactic:
exact hi ho' hv ht
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
tl : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tl → go rtr cpt vs tl[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
e : rtr ≈ update rtr cpt i v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt i v[Component.val cpt][i] = some w✝
ht : i ∉ tl
⊢ go (update rtr cpt i v) cpt vs tl[Component.val cpt][i] = some v
Tactic:
simp [set.go_preserves ho' (.inr $ .inl ht), ho' ▸ obj?_updated, ho]
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
ht : i ∈ tail✝
⊢ go rtr cpt vs (hd :: tail✝)[Component.val cpt][i] = some v
Tactic:
simp [go]
State after:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
ht : i ∈ tail✝
⊢ (match vs hd with
      | none => go rtr cpt vs tail✝
      | some v => go (update rtr cpt hd v) cpt vs tail✝)[Component.val cpt][i] =
    some v

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
ht : i ∈ tail✝
⊢ (match vs hd with
      | none => go rtr cpt vs tail✝
      | some v => go (update rtr cpt hd v) cpt vs tail✝)[Component.val cpt][i] =
    some v
Tactic:
split
State after:
case h_1
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
ht : i ∈ tail✝
x✝ : Option Value
heq✝ : vs hd = none
⊢ go rtr cpt vs tail✝[Component.val cpt][i] = some v

case h_2
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
ht : i ∈ tail✝
x✝ : Option Value
v✝ : Value
heq✝ : vs hd = some v✝
⊢ go (update rtr cpt hd v✝) cpt vs tail✝[Component.val cpt][i] = some v

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v✝ : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v✝
ht : i ∈ tail✝
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
⊢ go (update rtr cpt hd v) cpt vs tail✝[Component.val cpt][i] = some v✝
Tactic:
case _ v _ =>
  have e := @LawfulUpdatable.equiv _ cpt hd v _ rtr
  have ⟨_, ho'⟩ := Equivalent.obj?_some_iff e |>.mp ⟨_, ho⟩
  exact hi ho' hv ht
State after:
no goals

State before:
case h_1
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v
ht : i ∈ tail✝
x✝ : Option Value
heq✝ : vs hd = none
⊢ go rtr cpt vs tail✝[Component.val cpt][i] = some v
Tactic:
exact hi ho hv ht
State after:
no goals

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

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

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi :
  ∀ {rtr : α} {i : ID} {v : Value} {o : Component.type α (Component.val cpt)},
    rtr[Component.val cpt][i] = some o → vs i = some v → i ∈ tail✝ → go rtr cpt vs tail✝[Component.val cpt][i] = some v
rtr : α
i : ID
v✝ : Value
o : Component.type α (Component.val cpt)
ho : rtr[Component.val cpt][i] = some o
hv : vs i = some v✝
ht : i ∈ tail✝
x✝ : Option Value
v : Value
heq✝ : vs hd = some v
e : rtr ≈ update rtr cpt hd v
w✝ : Component.type α (Component.val cpt)
ho' : update rtr cpt hd v[Component.val cpt][i] = some w✝
⊢ go (update rtr cpt hd v) cpt vs tail✝[Component.val cpt][i] = some v✝
Tactic:
exact hi ho' hv ht
State after:
no goals