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

State before:
C : Type ?u.15125
τ : Type ?u.15124
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
x : τ
j : Fin (size (set cont i x))
⊢ size (set cont i x) = size cont
Tactic:
rw [size_set]
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)
x : τ
j : Fin (size (set cont i x))
⊢ ↑i ≠ ↑j → get (set cont i x) 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)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ get (set cont i x) 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)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ get (set cont i x) 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)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ get (toList (set cont i x)) (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)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ get (toList (set cont i x)) (Fin.cast ⋯ j) = get cont (Fin.cast ⋯ j)
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)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ get (toList (set cont i x)) (Fin.cast ⋯ j) = get (toList cont) (Fin.cast ⋯ (Fin.cast ⋯ j))

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ get (toList (set cont i x)) (Fin.cast ⋯ j) = get (toList cont) (Fin.cast ⋯ (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)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ (toList (set cont i x)).get (Fin.cast ⋯ j) = (toList cont).get (Fin.cast ⋯ j)

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ (toList (set cont i x)).get (Fin.cast ⋯ j) = (toList cont).get (Fin.cast ⋯ j)
Tactic:
rw [List.get_eq_get _ (List.set (toList cont) i x) _ _ (toList_set ..) ?idx_eq]
State after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ ((toList cont).set (↑i) x).get ?m.15919 = (toList cont).get (Fin.cast ⋯ j)

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ Fin ((toList cont).set (↑i) x).length

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑?m.15919

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

C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ Fin ((toList cont).set (↑i) x).length

case idx_eq
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑?m.15919
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)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ (toList cont).get ⟨↑j, ⋯⟩ = (toList cont).get (Fin.cast ⋯ j)

case hj
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ ↑j < ((toList cont).set (↑i) x).length

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

State before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨↑j, ⋯⟩
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)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ (toList cont).get ⟨↑j, ⋯⟩ = (toList cont).get (Fin.cast ⋯ j)
Tactic:
congr
State after:
no goals

State before:
case hj
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
i : Fin (size cont)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ ↑j < ((toList cont).set (↑i) x).length
Tactic:
simpa [← size_def] 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)
x : τ
j : Fin (size (set cont i x))
h : ↑i ≠ ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨↑j, ⋯⟩
Tactic:
simp [h]
State after:
no goals