Theorem: Fin.foldl_eq_foldl_ofFn (LeanColls/MathlibUpstream.lean)

State before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl n f init = List.foldl f init (List.ofFn id)
Tactic:
unfold foldl
State after:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)

State before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)
Tactic:
suffices ∀ init i j (h : i + j = n),
  foldl.loop n f init i =
    List.foldl f init (List.ofFn (n := j) (fun x => Fin.natAdd i x |>.cast h))
  by
    have := this init 0 n (by simp)
    simp at this; rw [this]; rfl
State after:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))

State before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
⊢ ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
intro init i j h
State after:
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i j : ℕ
h : i + j = n
⊢ foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))

State before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i j : ℕ
h : i + j = n
⊢ foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
induction j generalizing init i with
| zero =>
  unfold foldl.loop
  simp at h
  simp [List.drop_eq_nil_of_le, h]
| succ j ih =>
  unfold foldl.loop
  have : i < n := by omega
  simp [this, cast]
  generalize f init _ = init'
  have : (i+1) + j = n := by omega
  specialize ih init' (i+1) this
  rw [ih]; clear ih
  congr
  funext ⟨x,hx⟩; simp; omega
State after:
no goals

State before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)
Tactic:
have := this init 0 n (by simp)
State after:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this✝ :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
this : foldl.loop n f init 0 = List.foldl f init (List.ofFn fun x => cast ⋯ (natAdd 0 x))
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)

State before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this✝ :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
this : foldl.loop n f init 0 = List.foldl f init (List.ofFn fun x => cast ⋯ (natAdd 0 x))
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)
Tactic:
simp at this
State after:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this✝ :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
this : foldl.loop n f init 0 = List.foldl f init (List.ofFn fun x => x.addNat 0)
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)

State before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this✝ :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
this : foldl.loop n f init 0 = List.foldl f init (List.ofFn fun x => x.addNat 0)
⊢ foldl.loop n f init 0 = List.foldl f init (List.ofFn id)
Tactic:
rw [this]
State after:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this✝ :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
this : foldl.loop n f init 0 = List.foldl f init (List.ofFn fun x => x.addNat 0)
⊢ List.foldl f init (List.ofFn fun x => x.addNat 0) = List.foldl f init (List.ofFn id)

State before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this✝ :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
this : foldl.loop n f init 0 = List.foldl f init (List.ofFn fun x => x.addNat 0)
⊢ List.foldl f init (List.ofFn fun x => x.addNat 0) = List.foldl f init (List.ofFn id)
Tactic:
rfl
State after:
no goals

State before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init : α
this :
  ∀ (init : α) (i j : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
⊢ 0 + n = n
Tactic:
simp
State after:
no goals

State before:
case zero
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i : ℕ
h : i + 0 = n
⊢ foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
unfold foldl.loop
State after:
case zero
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i : ℕ
h : i + 0 = n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h (natAdd i x))

State before:
case zero
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i : ℕ
h : i + 0 = n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
simp at h
State after:
case zero
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i : ℕ
h✝ : i + 0 = n
h : i = n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h✝ (natAdd i x))

State before:
case zero
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ init : α
i : ℕ
h✝ : i + 0 = n
h : i = n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h✝ (natAdd i x))
Tactic:
simp [List.drop_eq_nil_of_le, h]
State after:
no goals

State before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
⊢ foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
unfold foldl.loop
State after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h (natAdd i x))

State before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
have : i < n := by omega
State after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h (natAdd i x))

State before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
⊢ (if h : i < n then foldl.loop n f (f init ⟨i, h⟩) (i + 1) else init) =
    List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
Tactic:
simp [this, cast]
State after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
⊢ foldl.loop n f (f init ⟨i, ⋯⟩) (i + 1) = List.foldl f (f init ⟨i, ⋯⟩) (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)

State before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
⊢ foldl.loop n f (f init ⟨i, ⋯⟩) (i + 1) = List.foldl f (f init ⟨i, ⋯⟩) (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Tactic:
generalize f init _ = init'
State after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
init' : α
⊢ foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)

State before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
init' : α
⊢ foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Tactic:
have : (i+1) + j = n := by omega
State after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
⊢ foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)

State before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
⊢ foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Tactic:
specialize ih init' (i+1) this
State after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
ih : foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x))
⊢ foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)

State before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
ih : foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x))
⊢ foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Tactic:
rw [ih]
State after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
ih : foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x))
⊢ List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x)) =
    List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)

State before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
ih : foldl.loop n f init' (i + 1) = List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x))
⊢ List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x)) =
    List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Tactic:
clear ih
State after:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
⊢ List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x)) =
    List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)

State before:
case succ
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
⊢ List.foldl f init' (List.ofFn fun x => cast this (natAdd (i + 1) x)) =
    List.foldl f init' (List.ofFn fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩)
Tactic:
congr
State after:
case succ.e_a.e_f
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
⊢ (fun x => cast this (natAdd (i + 1) x)) = fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩

State before:
case succ.e_a.e_f
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
⊢ (fun x => cast this (natAdd (i + 1) x)) = fun i_1 => ⟨i + (↑i_1 + 1), ⋯⟩
Tactic:
funext ⟨x,hx⟩
State after:
case succ.e_a.e_f.h
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
x : ℕ
hx : x < j
⊢ cast this (natAdd (i + 1) ⟨x, hx⟩) = ⟨i + (↑⟨x, hx⟩ + 1), ⋯⟩

State before:
case succ.e_a.e_f.h
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
x : ℕ
hx : x < j
⊢ cast this (natAdd (i + 1) ⟨x, hx⟩) = ⟨i + (↑⟨x, hx⟩ + 1), ⋯⟩
Tactic:
simp
State after:
case succ.e_a.e_f.h
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
x : ℕ
hx : x < j
⊢ i + 1 + x = i + (x + 1)

State before:
case succ.e_a.e_f.h
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
init : α
i : ℕ
h : i + (j + 1) = n
this✝ : i < n
init' : α
this : i + 1 + j = n
x : ℕ
hx : x < j
⊢ i + 1 + x = i + (x + 1)
Tactic:
omega
State after:
no goals

State before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
⊢ i < n
Tactic:
omega
State after:
no goals

State before:
α : Type u_1
n : ℕ
f : α → Fin n → α
init✝ : α
j : ℕ
ih :
  ∀ (init : α) (i : ℕ) (h : i + j = n),
    foldl.loop n f init i = List.foldl f init (List.ofFn fun x => cast h (natAdd i x))
init : α
i : ℕ
h : i + (j + 1) = n
this : i < n
init' : α
⊢ i + 1 + j = n
Tactic:
omega
State after:
no goals