dsimp
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k i : Nat
x : α' i
⊢ g₂' i (f' i x) = f' (i + 1) (g₁' i x)
α : Type u
β : Type v
n : Nat
f : α → β
g₁ : Fin n → α → α
g₂ : Fin n → β → β
init : α
H : ∀ (i : Fin n) (a : α), g₂ i (f a) = f (g₁ i a)
α' : Nat → Type u := fun i => i ≤ n → α
β' : Nat → Type v := fun i => i ≤ n → β
f' : (i : Nat) → α' i → β' i := fun i ha hi => f (ha hi)
g₁' : (i : Nat) → α' i → α' (i + 1) := fun i x hi => g₁ { val := i, isLt := hi } (x (_ : i ≤ n))
g₂' : (i : Nat) → β' i → β' (i + 1) := fun i y hi => g₂ { val := i, isLt := hi } (y (_ : i ≤ n))
init' : α' 0 := fun x => init
k i : Nat
x : α' i
⊢ (fun hi => g₂ { val := i, isLt := hi } (f (x (_ : i ≤ n)))) = fun hi =>
    f (g₁ { val := i, isLt := hi } (x (_ : i ≤ n)))