no goals
α : Type u
β : Type v
γ : Type w
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β → γ
head✝ : β
bs : List β
⊢ length (pointwise f [] (head✝ :: bs)) = max (length []) (length (head✝ :: bs))
simp only [pointwise, length, length_map, max_eq_right (Nat.zero_le (length bs + 1))]
no goals
α : Type u
β : Type v
γ : Type w
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β → γ
head✝ : α
as : List α
⊢ length (pointwise f (head✝ :: as) []) = max (length (head✝ :: as)) (length [])
simp only [pointwise, length, length_map, max_eq_left (Nat.zero_le (length as + 1))]
no goals
α : Type u
β : Type v
γ : Type w
inst✝¹ : Inhabited α
inst✝ : Inhabited β
f : α → β → γ
head✝¹ : α
as : List α
head✝ : β
bs : List β
⊢ length (pointwise f (head✝¹ :: as) (head✝ :: bs)) = max (length (head✝¹ :: as)) (length (head✝ :: bs))
simp only [pointwise, length, Nat.max_succ_succ, @length_pointwise _ as bs]