Theorem: LeanColls.Seq.get_set_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)
x : τ
j : Fin (size (set cont i x))
⊢ ↑i = ↑j → get (set cont i x) j = x
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 = x

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 = x
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)
x : τ
j : Fin (size (set cont i x))
h : ↑i = ↑j
⊢ get (toList (set cont i x)) (Fin.cast ⋯ j) = x

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) = x
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) = x

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) = x
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)
x : τ
j : Fin (size (set cont i x))
h : ↑i = ↑j
⊢ ?m.14719.get ?m.14721 = x

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
⊢ List τ

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 ?m.14719.length

case list_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
⊢ toList (set cont i x) = ?m.14719

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

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) = ?m.14719
Tactic:
case list_eq => apply toList_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))
h : ↑i = ↑j
⊢ (set (toList cont) (Fin.cast ⋯ i) x).get ?m.14721 = x

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 (set (toList cont) (Fin.cast ⋯ 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.14721
Tactic:
apply List.get_set_eq
State after:
case h
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 ⋯ i) < ((toList cont).set (↑(Fin.cast ⋯ 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) = ↑⟨↑(Fin.cast ⋯ i), ?h⟩

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) = ↑⟨↑(Fin.cast ⋯ 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)
x : τ
j : Fin (size (set cont i x))
h : ↑i = ↑j
⊢ toList (set cont i x) = ?m.14719
Tactic:
apply toList_set
State after:
no goals

State before:
case h
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 ⋯ i) < ((toList cont).set (↑(Fin.cast ⋯ i)) x).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)
x : τ
j : Fin (size (set cont i x))
h : ↑i = ↑j
⊢ ↑(Fin.cast ⋯ j) = ↑⟨↑(Fin.cast ⋯ i), ⋯⟩
Tactic:
simp [h]
State after:
no goals