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

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⟩
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⟩)

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]
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⟩)

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, *])
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, ⋯⟩

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'
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, ⋯⟩

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
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, ⋯⟩

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]
State after:
no goals

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

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, *]
State after:
no goals