internlm/Lean-Github huggingface dataset:
Theorem: LeanColls.Seq.size_cons
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
x : τ
⊢ size (cons x cont) = size cont + 1
Tactic:
simp [size_def, List.instSeqList]
Proof state after:
no goals
Theorem: LeanColls.Seq.size_snoc
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
cont : C
x : τ
⊢ size (snoc cont x) = size cont + 1
Tactic:
simp [size_def, List.instSeqList]
Proof state after:
no goals
Theorem: LeanColls.Seq.size_append
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
c1 c2 : C
⊢ size (c1 ++ c2) = size c1 + size c2
Tactic:
simp [size_def]
Proof state after:
no goals
Theorem: LeanColls.Seq.size_singleton
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
x : τ
⊢ size (singleton x) = 1
Tactic:
simp [size_def]
Proof state after:
no goals
Theorem: LeanColls.Seq.size_ofFn
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
⊢ size (ofFn f) = n
Tactic:
simp [size_def, toList_ofFn, List.instSeqList]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_ofFn
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : Fin (size (ofFn f))
⊢ get (ofFn f) i = f (Fin.cast ⋯ i)
Tactic:
rcases i with ⟨i,hi⟩
Proof state after:
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
⊢ get (ofFn f) ⟨i, hi⟩ = f (Fin.cast ⋯ ⟨i, hi⟩)
Theorem: LeanColls.Seq.get_ofFn
Proof state before:
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
⊢ get (ofFn f) ⟨i, hi⟩ = f (Fin.cast ⋯ ⟨i, hi⟩)
Tactic:
rw [get_def]
Proof state after:
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
⊢ get (toList (ofFn f)) (Fin.cast ⋯ ⟨i, hi⟩) = f (Fin.cast ⋯ ⟨i, hi⟩)
Theorem: LeanColls.Seq.get_ofFn
Proof state before:
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
⊢ get (toList (ofFn f)) (Fin.cast ⋯ ⟨i, hi⟩) = f (Fin.cast ⋯ ⟨i, hi⟩)
Tactic:
suffices ∀ L (_h : L = ofFn f) (hi' : i < L.length),
  get L ⟨i,hi'⟩ = f ⟨i, size_ofFn (C := C) f ▸ hi⟩
  from this _ (toList_ofFn _) (by simp at hi; simp [List.instSeqList, *])
Proof state after:
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
⊢ ∀ (L : List τ), L = ofFn f → ∀ (hi' : i < L.length), get L ⟨i, hi'⟩ = f ⟨i, ⋯⟩
Theorem: LeanColls.Seq.get_ofFn
Proof state before:
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
⊢ ∀ (L : List τ), L = ofFn f → ∀ (hi' : i < L.length), get L ⟨i, hi'⟩ = f ⟨i, ⋯⟩
Tactic:
intro L hL hi'
Proof state after:
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
L : List τ
hL : L = ofFn f
hi' : i < L.length
⊢ get L ⟨i, hi'⟩ = f ⟨i, ⋯⟩
Theorem: LeanColls.Seq.get_ofFn
Proof state before:
case mk
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
L : List τ
hL : L = ofFn f
hi' : i < L.length
⊢ get L ⟨i, hi'⟩ = f ⟨i, ⋯⟩
Tactic:
cases hL
Proof state after:
case mk.refl
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
hi' : i < (ofFn f).length
⊢ get (ofFn f) ⟨i, hi'⟩ = f ⟨i, ⋯⟩
Theorem: LeanColls.Seq.get_ofFn
Proof state before:
case mk.refl
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
hi' : i < (ofFn f).length
⊢ get (ofFn f) ⟨i, hi'⟩ = f ⟨i, ⋯⟩
Tactic:
simp [List.instSeqList]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_ofFn
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi : i < size (ofFn f)
this : ∀ (L : List τ), L = ofFn f → ∀ (hi' : i < L.length), get L ⟨i, hi'⟩ = f ⟨i, ⋯⟩
⊢ i < (toList (ofFn f)).length
Tactic:
simp at hi
Proof state after:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi✝ : i < size (ofFn f)
this : ∀ (L : List τ), L = ofFn f → ∀ (hi' : i < L.length), get L ⟨i, hi'⟩ = f ⟨i, ⋯⟩
hi : i < n
⊢ i < (toList (ofFn f)).length
Theorem: LeanColls.Seq.get_ofFn
Proof state before:
C : Type u_1
τ : Type u_2
inst✝¹ : Seq C τ
inst✝ : LawfulSeq C τ
n : ℕ
f : Fin n → τ
i : ℕ
hi✝ : i < size (ofFn f)
this : ∀ (L : List τ), L = ofFn f → ∀ (hi' : i < L.length), get L ⟨i, hi'⟩ = f ⟨i, ⋯⟩
hi : i < n
⊢ i < (toList (ofFn f)).length
Tactic:
simp [List.instSeqList, *]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_set_eq
Proof 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
Proof 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
Theorem: LeanColls.Seq.get_set_eq
Proof 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]
Proof 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
Theorem: LeanColls.Seq.get_set_eq
Proof 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]
Proof 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
Theorem: LeanColls.Seq.get_set_eq
Proof 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]
Proof 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
Theorem: LeanColls.Seq.get_set_eq
Proof 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
Proof state after:
no goals
Theorem: LeanColls.Seq.get_set_eq
Proof 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
Proof 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⟩
Theorem: LeanColls.Seq.get_set_eq
Proof 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]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_set_eq
Proof 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
Proof state after:
no goals
Theorem: LeanColls.Seq.get_set_eq
Proof 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]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_set_eq
Proof 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]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_set_ne
Proof 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]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_set_ne
Proof 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
Proof 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)
Theorem: LeanColls.Seq.get_set_ne
Proof 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]
Proof 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)
Theorem: LeanColls.Seq.get_set_ne
Proof 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]
Proof 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))
Theorem: LeanColls.Seq.get_set_ne
Proof 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]
Proof 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)
Theorem: LeanColls.Seq.get_set_ne
Proof 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]
Proof 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
Theorem: LeanColls.Seq.get_set_ne
Proof 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]
Proof 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⟩
Theorem: LeanColls.Seq.get_set_ne
Proof 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]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_set_ne
Proof 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
Proof state after:
no goals
Theorem: LeanColls.Seq.get_set_ne
Proof 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
Proof state after:
no goals
Theorem: LeanColls.Seq.get_set_ne
Proof 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]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_set
Proof 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))
⊢ get (set cont i x) j = if ↑i = ↑j then x else get cont (Fin.cast ⋯ j)
Tactic:
by_cases i.val = j.val <;> simp [*]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_eq
Proof 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
Proof 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)
Theorem: LeanColls.Seq.get_update_eq
Proof 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]
Proof 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)
Theorem: LeanColls.Seq.get_update_eq
Proof 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]
Proof 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)
Theorem: LeanColls.Seq.get_update_eq
Proof 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]
Proof 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
Theorem: LeanColls.Seq.get_update_eq
Proof 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
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_eq
Proof 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]
Proof 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
Theorem: LeanColls.Seq.get_update_eq
Proof 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]
Proof 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⟩
Theorem: LeanColls.Seq.get_update_eq
Proof 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]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_eq
Proof 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]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_eq
Proof 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]
Proof 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))
Theorem: LeanColls.Seq.get_update_eq
Proof 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]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_eq
Proof 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
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_eq
Proof 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]
Proof state after:
no goals
Theorem: LeanColls.Seq.get_update_eq
Proof 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]
Proof state after:
no goals