[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
s t : Set α
a : α
x : α × α
⊢ Prod.swap x ∈ mulAntidiagonal s t a ↔ x ∈ mulAntidiagonal t s a
[PROOFSTEP]
simp [mul_comm, and_left_comm]
[GOAL]
α : Type u_1
inst✝ : CommSemigroup α
s t : Set α
a : α
x : α × α
⊢ x.snd ∈ s ∧ x.fst ∈ t ∧ x.snd * x.fst = a ↔ x ∈ mulAntidiagonal t s a
[PROOFSTEP]
simp [mul_comm, and_left_comm]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).fst = (↑y).fst
⊢ a = (↑y).fst * (↑x).snd
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).fst = (↑y).fst
⊢ a = (↑x).fst * (↑x).snd
[PROOFSTEP]
exact x.2.2.2.symm
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).snd = (↑y).snd
⊢ a = (↑x).fst * (↑y).snd
[PROOFSTEP]
rw [← h]
[GOAL]
α : Type u_1
inst✝ : CancelCommMonoid α
s t : Set α
a : α
x y : ↑(mulAntidiagonal s t a)
h : (↑x).snd = (↑y).snd
⊢ a = (↑x).fst * (↑x).snd
[PROOFSTEP]
exact x.2.2.2.symm
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
⊢ Set.Finite (mulAntidiagonal s t a)
[PROOFSTEP]
refine' not_infinite.1 fun h => _
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
h : Set.Infinite (mulAntidiagonal s t a)
⊢ False
[PROOFSTEP]
have h1 : (mulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o (· ≤ ·)) := fun f hf =>
  hs (Prod.fst ∘ f) fun n => (mem_mulAntidiagonal.1 (hf n)).1
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
h : Set.Infinite (mulAntidiagonal s t a)
h1 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
⊢ False
[PROOFSTEP]
have h2 : (mulAntidiagonal s t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o (· ≤ ·)) := fun f hf =>
  ht (Prod.snd ∘ f) fun n => (mem_mulAntidiagonal.1 (hf n)).2.1
[GOAL]
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
h : Set.Infinite (mulAntidiagonal s t a)
h1 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
h2 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)
⊢ False
[PROOFSTEP]
obtain ⟨g, hg⟩ := h1.exists_monotone_subseq (fun n => h.natEmbedding _ n) fun n => (h.natEmbedding _ n).2
[GOAL]
case intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
h : Set.Infinite (mulAntidiagonal s t a)
h1 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
h2 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g m))
        ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g n))
⊢ False
[PROOFSTEP]
obtain ⟨m, n, mn, h2'⟩ := h2 (fun x => (h.natEmbedding _) (g x)) fun n => (h.natEmbedding _ _).2
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
h : Set.Infinite (mulAntidiagonal s t a)
h1 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
h2 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g m))
        ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g n))
m n : ℕ
mn : m < n
h2' :
  (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1) ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g m))
    ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g n))
⊢ False
[PROOFSTEP]
refine' mn.ne (g.injective <| (h.natEmbedding _).injective _)
[GOAL]
case intro.intro.intro.intro
α : Type u_1
inst✝ : OrderedCancelCommMonoid α
s t : Set α
a✝ : α
x y : ↑(mulAntidiagonal s t a✝)
hs : IsPwo s
ht : IsPwo t
a : α
h : Set.Infinite (mulAntidiagonal s t a)
h1 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
h2 : PartiallyWellOrderedOn (mulAntidiagonal s t a) (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g m))
        ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g n))
m n : ℕ
mn : m < n
h2' :
  (Prod.snd ⁻¹'o fun x x_1 => x ≤ x_1) ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g m))
    ↑(↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g n))
⊢ ↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g m) = ↑(Infinite.natEmbedding (mulAntidiagonal s t a) h) (↑g n)
[PROOFSTEP]
exact eq_of_fst_le_fst_of_snd_le_snd _ _ _ (hg _ _ mn.le) h2'
