no goals
ι : Type u_2
α : Type ?u.82437
M : Type u_1
N : Type ?u.82443
P : Type ?u.82446
M₀ : Type ?u.82449
G : Type ?u.82452
R : Type ?u.82455
inst✝⁵ : Monoid M
inst✝⁴ : Monoid N
inst✝³ : Monoid P
l✝ l₁ l₂ : List M
a : M
inst✝² : Preorder M
inst✝¹ : CovariantClass M M (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : CovariantClass M M (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
l : List ι
f g : ι → M
h : ∀ (i : ι), i ∈ l → f i ≤ g i
⊢ Forall₂ (fun x x_1 => x ≤ x_1) (map f l) (map g l)
simpa