Theorem: LeanColls.Seq.get_update_eq (LeanColls/Classes/Seq.lean)

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
⊢ ↑i = ↑j → get (update cont i f) j = f (get cont i)
Tactic:
intro h
State after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ get (update cont i f) j = f (get cont i)

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ get (update cont i f) j = f (get cont i)
Tactic:
rw [get_def]
State after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ get (toList (update cont i f)) (Fin.cast ⋯ j) = f (get cont i)

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ get (toList (update cont i f)) (Fin.cast ⋯ j) = f (get cont i)
Tactic:
simp [List.instSeqList]
State after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ (toList (update cont i f)).get (Fin.cast ⋯ j) = f (get cont i)

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ (toList (update cont i f)).get (Fin.cast ⋯ j) = f (get cont i)
Tactic:
rw [List.get_eq_get _ _ _ _ ?list_eq ?idx_eq]
State after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ ?m.17492.get ?m.17494 = f (get cont i)

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ List τ

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ Fin ?m.17492.length

case list_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ toList (update cont i f) = ?m.17492

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑?m.17494

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ toList (update cont i f) = ?m.17492
Tactic:
case list_eq =>
  apply toList_update
State after:
no goals

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ (update (toList cont) (Fin.cast ⋯ i) f).get ?m.17494 = f (get cont i)

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ Fin (update (toList cont) (Fin.cast ⋯ i) f).length

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑?m.17494
Tactic:
simp [List.instSeqList]
State after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).get ?m.17494 = f (get cont i)

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ Fin (update (toList cont) (Fin.cast ⋯ i) f).length

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑?m.17494

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).get ?m.17494 = f (get cont i)

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ Fin (update (toList cont) (Fin.cast ⋯ i) f).length

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑?m.17494
Tactic:
rw [List.get_set_eq _ _ _ ?h]
State after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ f ((toList cont).get (Fin.cast ⋯ i)) = f (get cont i)

case h
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ ↑i < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨↑i, ?h⟩

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ ↑i < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length
Tactic:
case h => simp [← size_def]
State after:
no goals

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨↑i, ⋯⟩
Tactic:
case idx_eq => simp [h]
State after:
no goals

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ f ((toList cont).get (Fin.cast ⋯ i)) = f (get cont i)
Tactic:
rw [get_def]
State after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ f ((toList cont).get (Fin.cast ⋯ i)) = f (get (toList cont) (Fin.cast ⋯ i))

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ f ((toList cont).get (Fin.cast ⋯ i)) = f (get (toList cont) (Fin.cast ⋯ i))
Tactic:
simp [List.instSeqList]
State after:
no goals

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ toList (update cont i f) = ?m.17492
Tactic:
apply toList_update
State after:
no goals

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ ↑i < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length
Tactic:
simp [← size_def]
State after:
no goals

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
h : ↑i = ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨↑i, ⋯⟩
Tactic:
simp [h]
State after:
no goals