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

State before:
C : Type ?u.18089
τ : Type ?u.18088
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
f : τ → τ
j : Fin (size (update cont i f))
⊢ size (update cont i f) = size cont
Tactic:
rw [size_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))
⊢ ↑i ≠ ↑j → get (update cont i f) j = get cont (Fin.cast ⋯ j)
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 = get cont (Fin.cast ⋯ j)

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 = get cont (Fin.cast ⋯ j)
Tactic:
conv => lhs; 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) = get cont (Fin.cast ⋯ j)

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) = get cont (Fin.cast ⋯ j)
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) = get cont (Fin.cast ⋯ j)

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) = get cont (Fin.cast ⋯ j)
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.18568.get ?m.18570 = get cont (Fin.cast ⋯ j)

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.18568.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.18568

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.18570

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.18568
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.18570 = get cont (Fin.cast ⋯ j)

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.18570
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.18570 = get cont (Fin.cast ⋯ j)

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.18570

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.18570 = get cont (Fin.cast ⋯ j)

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.18570
Tactic:
rw [List.get_set_ne _ _ _ ?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
⊢ (toList cont).get ⟨?m.18745, ⋯⟩ = get cont (Fin.cast ⋯ j)

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
⊢ ℕ

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
⊢ ?m.18745 < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length

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 ≠ ?m.18745

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.18745, ?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
⊢ (toList cont).get ⟨?m.18745, ⋯⟩ = get cont (Fin.cast ⋯ j)

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
⊢ ℕ

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
⊢ ?m.18745 < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length

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 ≠ ?m.18745

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.18745, ?h⟩
Tactic:
conv => rhs; 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
⊢ (toList cont).get ⟨?m.18745, ⋯⟩ = get (toList cont) (Fin.cast ⋯ (Fin.cast ⋯ j))

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
⊢ ℕ

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
⊢ ?m.18745 < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length

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 ≠ ?m.18745

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.18745, ?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
⊢ (toList cont).get ⟨?m.18745, ⋯⟩ = get (toList cont) (Fin.cast ⋯ (Fin.cast ⋯ j))

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
⊢ ℕ

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
⊢ ?m.18745 < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length

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 ≠ ?m.18745

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.18745, ?h⟩
Tactic:
rfl
State after:
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
⊢ ↑(Fin.cast ⋯ j) < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length

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 ≠ ↑(Fin.cast ⋯ j)

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) = ↑⟨↑(Fin.cast ⋯ j), ?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
⊢ ↑(Fin.cast ⋯ j) < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length
Tactic:
case h => simpa [size_def, List.instSeqList] using j.isLt
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) = ↑⟨↑(Fin.cast ⋯ j), ⋯⟩
Tactic:
case idx_eq => simp
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 ≠ ↑(Fin.cast ⋯ j)
Tactic:
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
⊢ toList (update cont i f) = ?m.18568
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
⊢ ↑(Fin.cast ⋯ j) < ((toList cont).set (↑i) (f ((toList cont).get (Fin.cast ⋯ i)))).length
Tactic:
simpa [size_def, List.instSeqList] using j.isLt
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) = ↑⟨↑(Fin.cast ⋯ j), ⋯⟩
Tactic:
simp
State after:
no goals