α : Type u_1
G : Type ?u.364481
M : Type ?u.364484
R : Type ?u.364487
A : Type ?u.364490
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : OrderedCancelCommMonoid α
s : Set α
hpos : ∀ (x : α), x ∈ s → 1 ≤ x
h : IsPwo s
⊢ IsPwo (List.prod '' {l | ∀ (x : α), x ∈ l → x ∈ s})
α : Type u_1
G : Type ?u.364481
M : Type ?u.364484
R : Type ?u.364487
A : Type ?u.364490
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : OrderedCancelCommMonoid α
s : Set α
hpos : ∀ (x : α), x ∈ s → 1 ≤ x
h : IsPwo s
⊢ IsPwo ↑(Submonoid.closure s)
rw [Submonoid.closure_eq_image_prod]
no goals
α : Type u_1
G : Type ?u.364481
M : Type ?u.364484
R : Type ?u.364487
A : Type ?u.364490
inst✝² : Monoid M
inst✝¹ : AddMonoid A
inst✝ : OrderedCancelCommMonoid α
s : Set α
hpos : ∀ (x : α), x ∈ s → 1 ≤ x
h : IsPwo s
⊢ ∀ (a₁ : List α),
    a₁ ∈ {l | ∀ (x : α), x ∈ l → x ∈ s} →
      ∀ (a₂ : List α),
        a₂ ∈ {l | ∀ (x : α), x ∈ l → x ∈ s} →
          List.SublistForall₂ (fun x x_1 => x ≤ x_1) a₁ a₂ → List.prod a₁ ≤ List.prod a₂
exact fun l1 _ l2 hl2 h12 => h12.prod_le_prod' fun x hx => hpos x <| hl2 x hx