case intro.intro
F : Type ?u.160142
α : Type u_1
β : Type ?u.160148
γ : Type ?u.160151
inst✝ : OrderedCommMonoid α
A B : Set α
bA : α
hbA : bA ∈ upperBounds A
bB : α
hbB : bB ∈ upperBounds B
⊢ BddAbove (A * B)
F : Type ?u.160142
α : Type u_1
β : Type ?u.160148
γ : Type ?u.160151
inst✝ : OrderedCommMonoid α
A B : Set α
⊢ BddAbove A → BddAbove B → BddAbove (A * B)
rintro ⟨bA, hbA⟩ ⟨bB, hbB⟩
case intro.intro
F : Type ?u.160142
α : Type u_1
β : Type ?u.160148
γ : Type ?u.160151
inst✝ : OrderedCommMonoid α
A B : Set α
bA : α
hbA : bA ∈ upperBounds A
bB : α
hbB : bB ∈ upperBounds B
⊢ bA * bB ∈ upperBounds (A * B)
case intro.intro
F : Type ?u.160142
α : Type u_1
β : Type ?u.160148
γ : Type ?u.160151
inst✝ : OrderedCommMonoid α
A B : Set α
bA : α
hbA : bA ∈ upperBounds A
bB : α
hbB : bB ∈ upperBounds B
⊢ BddAbove (A * B)
use bA * bB
case intro.intro.intro.intro.intro.intro
F : Type ?u.160142
α : Type u_1
β : Type ?u.160148
γ : Type ?u.160151
inst✝ : OrderedCommMonoid α
A B : Set α
bA : α
hbA : bA ∈ upperBounds A
bB : α
hbB : bB ∈ upperBounds B
xa xb : α
hxa : xa ∈ A
hxb : xb ∈ B
⊢ (fun x x_1 => x * x_1) xa xb ≤ bA * bB
case intro.intro
F : Type ?u.160142
α : Type u_1
β : Type ?u.160148
γ : Type ?u.160151
inst✝ : OrderedCommMonoid α
A B : Set α
bA : α
hbA : bA ∈ upperBounds A
bB : α
hbB : bB ∈ upperBounds B
⊢ bA * bB ∈ upperBounds (A * B)
rintro x ⟨xa, xb, hxa, hxb, rfl⟩
no goals
case intro.intro.intro.intro.intro.intro
F : Type ?u.160142
α : Type u_1
β : Type ?u.160148
γ : Type ?u.160151
inst✝ : OrderedCommMonoid α
A B : Set α
bA : α
hbA : bA ∈ upperBounds A
bB : α
hbB : bB ∈ upperBounds B
xa xb : α
hxa : xa ∈ A
hxb : xb ∈ B
⊢ (fun x x_1 => x * x_1) xa xb ≤ bA * bB
exact mul_le_mul' (hbA hxa) (hbB hxb)