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

State before:
α : Type
inst✝¹ : Accessible α
rtr : α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
ids : List ID
⊢ rtr ≈ go rtr cpt vs ids
Tactic:
induction ids generalizing rtr <;> simp [go]
State after:
case nil
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
rtr : α
⊢ rtr ≈ rtr

case cons
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
head✝ : ID
tail✝ : List ID
tail_ih✝ : ∀ {rtr : α}, rtr ≈ go rtr cpt vs tail✝
rtr : α
⊢ rtr ≈
    match vs head✝ with
    | none => go rtr cpt vs tail✝
    | some v => go (update rtr cpt head✝ v) cpt vs tail✝

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
rtr : α
⊢ rtr ≈ rtr
Tactic:
case nil     => exact .refl _
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi : ∀ {rtr : α}, rtr ≈ go rtr cpt vs tail✝
rtr : α
⊢ rtr ≈
    match vs hd with
    | none => go rtr cpt vs tail✝
    | some v => go (update rtr cpt hd v) cpt vs tail✝
Tactic:
case cons hd _ hi =>
  cases vs hd
  case none => exact hi
  case some => exact Equivalent.trans LawfulUpdatable.equiv hi
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
rtr : α
⊢ rtr ≈ rtr
Tactic:
exact .refl _
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi : ∀ {rtr : α}, rtr ≈ go rtr cpt vs tail✝
rtr : α
⊢ rtr ≈
    match vs hd with
    | none => go rtr cpt vs tail✝
    | some v => go (update rtr cpt hd v) cpt vs tail✝
Tactic:
cases vs hd
State after:
case none
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi : ∀ {rtr : α}, rtr ≈ go rtr cpt vs tail✝
rtr : α
⊢ rtr ≈
    match none with
    | none => go rtr cpt vs tail✝
    | some v => go (update rtr cpt hd v) cpt vs tail✝

case some
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi : ∀ {rtr : α}, rtr ≈ go rtr cpt vs tail✝
rtr : α
val✝ : Value
⊢ rtr ≈
    match some val✝ with
    | none => go rtr cpt vs tail✝
    | some v => go (update rtr cpt hd v) cpt vs tail✝

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi : ∀ {rtr : α}, rtr ≈ go rtr cpt vs tail✝
rtr : α
⊢ rtr ≈
    match none with
    | none => go rtr cpt vs tail✝
    | some v => go (update rtr cpt hd v) cpt vs tail✝
Tactic:
case none => exact hi
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi : ∀ {rtr : α}, rtr ≈ go rtr cpt vs tail✝
rtr : α
val✝ : Value
⊢ rtr ≈
    match some val✝ with
    | none => go rtr cpt vs tail✝
    | some v => go (update rtr cpt hd v) cpt vs tail✝
Tactic:
case some => exact Equivalent.trans LawfulUpdatable.equiv hi
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi : ∀ {rtr : α}, rtr ≈ go rtr cpt vs tail✝
rtr : α
⊢ rtr ≈
    match none with
    | none => go rtr cpt vs tail✝
    | some v => go (update rtr cpt hd v) cpt vs tail✝
Tactic:
exact hi
State after:
no goals

State before:
α : Type
inst✝¹ : Accessible α
inst✝ : Finite α
cpt : Component.Valued
vs : ID ⇀ Value
hd : ID
tail✝ : List ID
hi : ∀ {rtr : α}, rtr ≈ go rtr cpt vs tail✝
rtr : α
val✝ : Value
⊢ rtr ≈
    match some val✝ with
    | none => go rtr cpt vs tail✝
    | some v => go (update rtr cpt hd v) cpt vs tail✝
Tactic:
exact Equivalent.trans LawfulUpdatable.equiv hi
State after:
no goals