Theorem: LeanColls.Seq.get_update (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))
⊢ get (update cont i f) j = if ↑i = ↑j then f (get cont (Fin.cast ⋯ j)) else get cont (Fin.cast ⋯ j)
Tactic:
rcases i with ⟨i,hi⟩
State after:
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
f : τ → τ
i : ℕ
hi : i < size cont
j : Fin (size (update cont ⟨i, hi⟩ f))
⊢ get (update cont ⟨i, hi⟩ f) j = if ↑⟨i, hi⟩ = ↑j then f (get cont (Fin.cast ⋯ j)) else get cont (Fin.cast ⋯ j)

State before:
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
f : τ → τ
i : ℕ
hi : i < size cont
j : Fin (size (update cont ⟨i, hi⟩ f))
⊢ get (update cont ⟨i, hi⟩ f) j = if ↑⟨i, hi⟩ = ↑j then f (get cont (Fin.cast ⋯ j)) else get cont (Fin.cast ⋯ j)
Tactic:
rcases j with ⟨j,hj⟩
State after:
case mk.mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
f : τ → τ
i : ℕ
hi : i < size cont
j : ℕ
hj : j < size (update cont ⟨i, hi⟩ f)
⊢ get (update cont ⟨i, hi⟩ f) ⟨j, hj⟩ =
    if ↑⟨i, hi⟩ = ↑⟨j, hj⟩ then f (get cont (Fin.cast ⋯ ⟨j, hj⟩)) else get cont (Fin.cast ⋯ ⟨j, hj⟩)

State before:
case mk.mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
f : τ → τ
i : ℕ
hi : i < size cont
j : ℕ
hj : j < size (update cont ⟨i, hi⟩ f)
⊢ get (update cont ⟨i, hi⟩ f) ⟨j, hj⟩ =
    if ↑⟨i, hi⟩ = ↑⟨j, hj⟩ then f (get cont (Fin.cast ⋯ ⟨j, hj⟩)) else get cont (Fin.cast ⋯ ⟨j, hj⟩)
Tactic:
by_cases i = j <;> simp [*]
State after:
no goals