proposition: Lemma Exercise1_11d g: order_fam g -> complete_lattice (order_product g) -> (allf g complete_lattice).
proof: Proof. move=> poa clp i idg; move: (clp) => [p3 p4]. move: (order_product_osr poa) => [og Ha]. move: (Exercise1_11a clp)=> [[a [asg _]] _]. move: (asg); rewrite Ha => /prod_of_substratesP [fgfa da vas]. move: (poa _ idg) => o1. apply: Exercise1_11b => // X Xsr. set (Y:= Lg (domain g) (fun j=> Yo (j = i) X (singleton (Vg a j)))). have sYs: (sub (productb Y) (substrate (order_product g))). rewrite Ha /Y; apply: setXb_monotone1 => //; aww. move=> j jdg; rewrite ! LgV//; Ytac ji; first ue. by move => t; move /set1_P ->; apply: vas. move: (p4 _ sYs)=> [[y ys] _]; move: ys => /(lubP p3 sYs) [[ys uby] luy]. set f := Lg (domain g) (fun i => substrate (Vg g i)). have df: domain f = domain g by rewrite /f; aw. have fgf: fgraph f by rewrite /f; fprops. have pf: productb f = substrate (order_product g) by rewrite Ha. exists (Vg y i); apply /lubP => //; split. split. move: ys; rewrite Ha => /prod_of_substratesP [_ q1 q2]. by move: (q2 _ idg); aw. move=> z zX. have fs: (inc (Lg (domain g)(fun j=> (Yo (j = i) z (Vg a j)))) (productb Y)). apply /setXb_P; rewrite /Y;split;aww. move=> j jdg; rewrite !LgV//; Ytac ji; Ytac0 => //; fprops. move: (uby _ fs)=> /order_product_gleP [_ _ h]. by move: (h _ idg); rewrite LgV//; Ytac0. move=> z [zs zu]. set w:= (Lg (domain g)(fun j=> (Yo (j = i) z (Vg a j)))). have wp: (inc w (productb f)). apply /setXb_P; rewrite /w /f; split;aww. by move=> j jdg; rewrite !LgV//; Ytac ji; [ ue | apply: vas]. have ubw: (upper_bound (order_product g) (productb Y) w). split; first by ue. move=> t tp; apply /order_product_gleP; split => //; try ue. have pa: fgraph Y by rewrite /Y; fprops. move=> j jdg; rewrite /w LgV//. move: tp=> /setXb_P; rewrite /Y; aw; move=> [_ p5 p6]. move: (p6 _ jdg); rewrite LgV//. Ytac ji; Ytac0; first by rewrite ji;apply: zu. by move /set1_P ->; move: (poa _ jdg) => oj; order_tac; apply: vas. move: (luy _ ubw) => /order_product_gleP [_ _ h]. move: (h _ idg); rewrite /w LgV//; rewrite Y_true //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)