case a.mk
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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)}
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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)}
ext ⟨a, b⟩
case a.mk
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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
case a.mk
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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)}
simp only [mem_mulAntidiagonal, mem_singleton, Prod.ext_iff]
case a.mk.mp
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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

case a.mk.mpr
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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
case a.mk
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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
constructor
case a.mk.mp.intro.intro
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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
case a.mk.mp
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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
rintro ⟨has, hat, hst⟩
case a.mk.mp.intro.intro
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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
case a.mk.mp.intro.intro
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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
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
no goals
case a.mk.mp.intro.intro
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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
exact ⟨rfl, mul_left_cancel hst⟩
case a.mk.mpr.intro
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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
case a.mk.mpr
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a✝ : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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
rintro ⟨rfl, rfl⟩
no goals
case a.mk.mpr.intro
α✝ : Type ?u.14971
inst✝¹ : OrderedCancelCommMonoid α✝
s✝ t✝ : Set α✝
hs✝ : Set.IsPwo s✝
ht✝ : Set.IsPwo t✝
a : α✝
u : Set α✝
hu : Set.IsPwo u
x : α✝ × α✝
α : Type u_1
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
exact ⟨hs.min_mem _, ht.min_mem _, rfl⟩