case h
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ (last n)
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (↑castSucc i)
i : Fin n
y : α✝ (↑castSucc i)
z : α✝ (last n)
α : Type u_1
β : Type u_2
g : α → β
q : Fin (Nat.succ n) → α
j : Fin n
⊢ (g ∘ init q) j = init (g ∘ q) j
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ (last n)
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (↑castSucc i)
i : Fin n
y : α✝ (↑castSucc i)
z : α✝ (last n)
α : Type u_1
β : Type u_2
g : α → β
q : Fin (Nat.succ n) → α
⊢ g ∘ init q = init (g ∘ q)
ext j
no goals
case h
m n : ℕ
α✝ : Fin (n + 1) → Type u
x : α✝ (last n)
q✝ : (i : Fin (n + 1)) → α✝ i
p : (i : Fin n) → α✝ (↑castSucc i)
i : Fin n
y : α✝ (↑castSucc i)
z : α✝ (last n)
α : Type u_1
β : Type u_2
g : α → β
q : Fin (Nat.succ n) → α
j : Fin n
⊢ (g ∘ init q) j = init (g ∘ q) j
simp [init]