Big Op L hom weak

@[rocq_alias big_opL_commute1]theorem bigOpL_hom_weak [H : WeakMonoidHomomorphism op₁ op₂ unit₁ unit₂ R f] {l : List B}    (Φ : Nat → B → M₁) (hne : l ≠ []) :    R (f ([^ op₁ list] k ↦ x ∈ l, Φ k x)) ([^ op₂ list] k ↦ x ∈ l, f (Φ k x)) :=  match l with  | .nil => absurd rfl hne  | .cons _ .nil => H.rel_proper (H.map_ne.eqv op_right_id) op_right_id |>.mpr H.rel_refl  | .cons _ (.cons y ys) =>    H.rel_trans (H.map_op) <| H.op_proper H.rel_refl <| bigOpL_hom_weak _ (List.cons_ne_nil y ys)