α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : IsWf s
ht : IsWf t
hsn : Set.Nonempty s
htn : Set.Nonempty t
⊢ min hs hsn * min ht htn ≤ min (_ : IsWf (s * t)) (_ : Set.Nonempty (s * t))
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : IsWf s
ht : IsWf t
hsn : Set.Nonempty s
htn : Set.Nonempty t
⊢ min (_ : IsWf (s * t)) (_ : Set.Nonempty (s * t)) = min hs hsn * min ht htn
refine' le_antisymm (IsWf.min_le _ _ (mem_mul.2 ⟨_, _, hs.min_mem _, ht.min_mem _, rfl⟩)) _
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : IsWf s
ht : IsWf t
hsn : Set.Nonempty s
htn : Set.Nonempty t
⊢ ∀ (b : α), b ∈ s * t → min hs hsn * min ht htn ≤ b
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : IsWf s
ht : IsWf t
hsn : Set.Nonempty s
htn : Set.Nonempty t
⊢ min hs hsn * min ht htn ≤ min (_ : IsWf (s * t)) (_ : Set.Nonempty (s * t))
rw [IsWf.le_min_iff]
case intro.intro.intro.intro
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : IsWf s
ht : IsWf t
hsn : Set.Nonempty s
htn : Set.Nonempty t
x y : α
hx : x ∈ s
hy : y ∈ t
⊢ min hs hsn * min ht htn ≤ (fun x x_1 => x * x_1) x y
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : IsWf s
ht : IsWf t
hsn : Set.Nonempty s
htn : Set.Nonempty t
⊢ ∀ (b : α), b ∈ s * t → min hs hsn * min ht htn ≤ b
rintro _ ⟨x, y, hx, hy, rfl⟩
no goals
case intro.intro.intro.intro
α : Type u_1
s t : Set α
inst✝ : LinearOrderedCancelCommMonoid α
hs : IsWf s
ht : IsWf t
hsn : Set.Nonempty s
htn : Set.Nonempty t
x y : α
hx : x ∈ s
hy : y ∈ t
⊢ min hs hsn * min ht htn ≤ (fun x x_1 => x * x_1) x y
exact mul_le_mul' (hs.min_le _ hx) (ht.min_le _ hy)