[GOAL]
α : Type u_1
n : ℕ
r : α → α → Prop
inst✝ : IsTrans α r
f : Fin (n + 1) → α
a : α
⊢ ((fun x x_1 => x < x_1) ⇒ r) (vecCons a f) (vecCons a f) ↔ r a (f 0) ∧ ((fun x x_1 => x < x_1) ⇒ r) f f
[PROOFSTEP]
simp only [liftFun_iff_succ r, forall_fin_succ, cons_val_succ, cons_val_zero, ← succ_castSucc, castSucc_zero]
[GOAL]
α : Type u_1
inst✝ : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
⊢ Monotone (vecCons a f) ↔ a ≤ f 0 ∧ Monotone f
[PROOFSTEP]
simpa only [monotone_iff_forall_lt] using @liftFun_vecCons α n (· ≤ ·) _ f a
[GOAL]
α : Type u_1
inst✝ : Preorder α
n : ℕ
f : Fin (n + 1) → α
a : α
⊢ Monotone ![1, 2, 2, 3]
[PROOFSTEP]
simp
