. rw [<-ap] 
  apply Nat.le_antisymm
  . assumption
  . apply Nat.le_of_not_lt
    assumption
case inr
α : Type u_2
β : Type u_3
γ : Type u_1
as : Array α
bs : Array β
f : α → β → γ
p : size as = size bs
i : Nat
arr : Array γ
ip : i ≤ size as
ap : i = size arr
h✝ : ¬i < size as
⊢ size arr = size as
no goals