no goals
α : Type u
n : ℕ
f : Fin n → α
i : Fin (length (ofFn f))
⊢ length (ofFn f) = n
simp
α : Type u
n : ℕ
f : Fin n → α
i : Fin (length (ofFn f))
this : (Array.ofFn f)[↑i] = f { val := ↑i, isLt := (_ : ↑i < n) }
⊢ get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)
α : Type u
n : ℕ
f : Fin n → α
i : Fin (length (ofFn f))
⊢ get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)
have := Array.getElem_ofFn f i (by simpa using i.2)
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  (Array.ofFn f)[↑{ val := i, isLt := hi }] =
    f { val := ↑{ val := i, isLt := hi }, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } = f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := hi })
α : Type u
n : ℕ
f : Fin n → α
i : Fin (length (ofFn f))
this : (Array.ofFn f)[↑i] = f { val := ↑i, isLt := (_ : ↑i < n) }
⊢ get (ofFn f) i = f (↑(Fin.cast (_ : length (ofFn f) = n)) i)
cases' i with i hi
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } = f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := hi })
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  (Array.ofFn f)[↑{ val := i, isLt := hi }] =
    f { val := ↑{ val := i, isLt := hi }, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } = f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := hi })
simp only [getElem, Array.get] at this
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } = f { val := i, isLt := (_ : i < n) }
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } = f (↑(Fin.cast (_ : length (ofFn f) = n)) { val := i, isLt := hi })
simp only [Fin.cast_mk]
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } =
    get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) }
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } = f { val := i, isLt := (_ : i < n) }
rw [← this]
no goals
case mk
α : Type u
n : ℕ
f : Fin n → α
i : ℕ
hi : i < length (ofFn f)
this :
  get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) } =
    f { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < n) }
⊢ get (ofFn f) { val := i, isLt := hi } =
    get (Array.ofFn f).data { val := i, isLt := (_ : ↑{ val := i, isLt := hi } < Array.size (Array.ofFn f)) }
congr <;> simp [ofFn]
no goals
α : Type u
n : ℕ
f : Fin n → α
i : Fin (length (ofFn f))
⊢ ↑i < Array.size (Array.ofFn f)
simpa using i.2