Theorem: Array.foldl_ofFn_eq (Algdata/Data/Array/Lemmas.lean)

State before:
α✝ α : Type u
β : Type v
init : β
g : β → α → β
n : Nat
f : Fin n → α
⊢ foldl g init (ofFn f) 0 (size (ofFn f)) = Fin.foldAll (flip g ∘ f) init
Tactic:
rw [Array.foldl_eq_foldl_data']
State after:
α✝ α : Type u
β : Type v
init : β
g : β → α → β
n : Nat
f : Fin n → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init

State before:
α✝ α : Type u
β : Type v
init : β
g : β → α → β
n : Nat
f : Fin n → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
Tactic:
induction n generalizing init
State after:
case zero
α✝ α : Type u
β : Type v
g : β → α → β
init : β
f : Fin Nat.zero → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init

case succ
α✝ α : Type u
β : Type v
g : β → α → β
n✝ : Nat
n_ih✝ : ∀ {init : β} {f : Fin n✝ → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n✝) → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init

State before:
α✝ α : Type u
β : Type v
g : β → α → β
init : β
f : Fin Nat.zero → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
Tactic:
case zero => rfl
State after:
no goals

State before:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
Tactic:
case succ n h_ind =>
  rw [ofFn_succ']; dsimp [List.foldl]; rw [h_ind, Fin.foldAll_succ]; rfl
State after:
no goals

State before:
α✝ α : Type u
β : Type v
g : β → α → β
init : β
f : Fin Nat.zero → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
Tactic:
rfl
State after:
no goals

State before:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
Tactic:
rw [ofFn_succ']
State after:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ List.foldl g init (f { val := 0, isLt := (_ : 0 < Nat.succ n) } :: (ofFn (f ∘ Fin.succ)).data) =
    Fin.foldAll (flip g ∘ f) init

State before:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ List.foldl g init (f { val := 0, isLt := (_ : 0 < Nat.succ n) } :: (ofFn (f ∘ Fin.succ)).data) =
    Fin.foldAll (flip g ∘ f) init
Tactic:
dsimp [List.foldl]
State after:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ List.foldl g (g init (f 0)) (ofFn (f ∘ Fin.succ)).data = Fin.foldAll (flip g ∘ f) init

State before:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ List.foldl g (g init (f 0)) (ofFn (f ∘ Fin.succ)).data = Fin.foldAll (flip g ∘ f) init
Tactic:
rw [h_ind, Fin.foldAll_succ]
State after:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ Fin.foldAll (flip g ∘ f ∘ Fin.succ) (g init (f 0)) = Fin.foldAll ((flip g ∘ f) ∘ Fin.succ) ((flip g ∘ f) 0 init)

State before:
α✝ α : Type u
β : Type v
g : β → α → β
n : Nat
h_ind : ∀ {init : β} {f : Fin n → α}, List.foldl g init (ofFn f).data = Fin.foldAll (flip g ∘ f) init
init : β
f : Fin (Nat.succ n) → α
⊢ Fin.foldAll (flip g ∘ f ∘ Fin.succ) (g init (f 0)) = Fin.foldAll ((flip g ∘ f) ∘ Fin.succ) ((flip g ∘ f) 0 init)
Tactic:
rfl
State after:
no goals