[GOAL]
α : Type u_1
s t : Set α
inst✝ : OrderedCancelCommMonoid α
hs : IsPwo s
ht : IsPwo t
⊢ IsPwo (s * t)
[PROOFSTEP]
rw [← image_mul_prod]
[GOAL]
α : Type u_1
s t : Set α
inst✝ : OrderedCancelCommMonoid α
hs : IsPwo s
ht : IsPwo t
⊢ IsPwo ((fun x => x.fst * x.snd) '' s ×ˢ t)
[PROOFSTEP]
exact (hs.prod ht).image_of_monotone (monotone_fst.mul' monotone_snd)
[GOAL]
α : 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
[PROOFSTEP]
refine' le_antisymm (IsWf.min_le _ _ (mem_mul.2 ⟨_, _, hs.min_mem _, ht.min_mem _, rfl⟩)) _
[GOAL]
α : 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))
[PROOFSTEP]
rw [IsWf.le_min_iff]
[GOAL]
α : 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
[PROOFSTEP]
rintro _ ⟨x, y, hx, hy, rfl⟩
[GOAL]
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
[PROOFSTEP]
exact mul_le_mul' (hs.min_le _ hx) (ht.min_le _ hy)
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : Set.IsPwo s
ht : Set.IsPwo t
a : α
u : Set α
hu : Set.IsPwo u
x : α × α
⊢ x ∈ mulAntidiagonal hs ht a ↔ x.fst ∈ s ∧ x.snd ∈ t ∧ x.fst * x.snd = a
[PROOFSTEP]
simp only [mulAntidiagonal, Set.Finite.mem_toFinset, Set.mem_mulAntidiagonal]
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : Set.IsPwo s
ht : Set.IsPwo t
a : α
u : Set α
hu : Set.IsPwo u
x : α × α
⊢ Prod.swap x ∈ mulAntidiagonal hs ht a ↔ x ∈ mulAntidiagonal ht hs a
[PROOFSTEP]
simp only [mem_mulAntidiagonal, Prod.fst_swap, Prod.snd_swap, Set.swap_mem_mulAntidiagonal_aux, Set.mem_mulAntidiagonal]
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : Set.IsPwo s
ht : Set.IsPwo t
a✝ : α
u : Set α
hu : Set.IsPwo u
x : α × α
a : α
x✝ : a ∈ {a | Finset.Nonempty (mulAntidiagonal hs ht a)}
b : α × α
hb : b ∈ mulAntidiagonal hs ht a
⊢ a ∈ s * t
[PROOFSTEP]
rw [mem_mulAntidiagonal] at hb 
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
hs : Set.IsPwo s
ht : Set.IsPwo t
a✝ : α
u : Set α
hu : Set.IsPwo u
x : α × α
a : α
x✝ : a ∈ {a | Finset.Nonempty (mulAntidiagonal hs ht a)}
b : α × α
hb : b.fst ∈ s ∧ b.snd ∈ t ∧ b.fst * b.snd = a
⊢ a ∈ s * t
[PROOFSTEP]
exact ⟨b.1, b.2, hb⟩
[GOAL]
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
⊢ mulAntidiagonal (_ : Set.IsPwo s) (_ : Set.IsPwo t) (Set.IsWf.min hs hns * Set.IsWf.min ht hnt) =
    {(Set.IsWf.min hs hns, Set.IsWf.min ht hnt)}
[PROOFSTEP]
ext ⟨a, b⟩
[GOAL]
case a.mk
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
a b : α
⊢ (a, b) ∈ mulAntidiagonal (_ : Set.IsPwo s) (_ : Set.IsPwo t) (Set.IsWf.min hs hns * Set.IsWf.min ht hnt) ↔
    (a, b) ∈ {(Set.IsWf.min hs hns, Set.IsWf.min ht hnt)}
[PROOFSTEP]
simp only [mem_mulAntidiagonal, mem_singleton, Prod.ext_iff]
[GOAL]
case a.mk
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
a b : α
⊢ a ∈ s ∧ b ∈ t ∧ a * b = Set.IsWf.min hs hns * Set.IsWf.min ht hnt ↔ a = Set.IsWf.min hs hns ∧ b = Set.IsWf.min ht hnt
[PROOFSTEP]
constructor
[GOAL]
case a.mk.mp
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
a b : α
⊢ a ∈ s ∧ b ∈ t ∧ a * b = Set.IsWf.min hs hns * Set.IsWf.min ht hnt → a = Set.IsWf.min hs hns ∧ b = Set.IsWf.min ht hnt
[PROOFSTEP]
rintro ⟨has, hat, hst⟩
[GOAL]
case a.mk.mp.intro.intro
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
a b : α
has : a ∈ s
hat : b ∈ t
hst : a * b = Set.IsWf.min hs hns * Set.IsWf.min ht hnt
⊢ a = Set.IsWf.min hs hns ∧ b = Set.IsWf.min ht hnt
[PROOFSTEP]
obtain rfl := (hs.min_le hns has).eq_of_not_lt fun hlt => (mul_lt_mul_of_lt_of_le hlt <| ht.min_le hnt hat).ne' hst
[GOAL]
case a.mk.mp.intro.intro
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
b : α
hat : b ∈ t
has : Set.IsWf.min hs hns ∈ s
hst : Set.IsWf.min hs hns * b = Set.IsWf.min hs hns * Set.IsWf.min ht hnt
⊢ Set.IsWf.min hs hns = Set.IsWf.min hs hns ∧ b = Set.IsWf.min ht hnt
[PROOFSTEP]
exact ⟨rfl, mul_left_cancel hst⟩
[GOAL]
case a.mk.mpr
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
a b : α
⊢ a = Set.IsWf.min hs hns ∧ b = Set.IsWf.min ht hnt → a ∈ s ∧ b ∈ t ∧ a * b = Set.IsWf.min hs hns * Set.IsWf.min ht hnt
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case a.mk.mpr.intro
α✝ : Type u_1
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_2
inst✝ : LinearOrderedCancelCommMonoid α
s t : Set α
hs : Set.IsWf s
ht : Set.IsWf t
hns : Set.Nonempty s
hnt : Set.Nonempty t
⊢ Set.IsWf.min hs hns ∈ s ∧
    Set.IsWf.min ht hnt ∈ t ∧ Set.IsWf.min hs hns * Set.IsWf.min ht hnt = Set.IsWf.min hs hns * Set.IsWf.min ht hnt
[PROOFSTEP]
exact ⟨hs.min_mem _, ht.min_mem _, rfl⟩
