-- Mathlib/Data/Set/SMulAntidiagonal.lean
theorem finite_of_isPWO (hs : s.IsPWO) (ht : t.IsPWO) (a) : (smulAntidiagonal s t a).Finite

Proof state:
case intro.intro.intro.intro
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 => x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 => x1 ≤ x2)
isrfl : IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
istrns : IsTrans (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x1 x2 => x1 ≤ x2) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g m))
        ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g n))
m n : ℕ
mn : m < n
h2' :
  (Prod.snd ⁻¹'o fun x1 x2 => x1 ≤ x2) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g m))
    ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g n))
⊢ (Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g m) = (Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g n)

Tactic:
exact eq_of_fst_le_fst_of_snd_le_snd (hg _ _ mn.le) h2'

Result:
no goals

Proof state:
case trans
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 => x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 => x1 ≤ x2)
isrfl : IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
⊢ ∀ (a : G), P → ∀ (a_1 : G), P → ∀ (a_2 : G), P → a ≤ a_1 → a_1 ≤ a_2 → a ≤ a_2

Tactic:
exact fun a _ a_1 _ a_2 _ a_3 a_4 ↦ Preorder.le_trans a a_1 a_2 a_3 a_4

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 => x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 => x1 ≤ x2)
isrfl : IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
istrns : IsTrans (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
⊢ False

Tactic:
obtain ⟨g, hg⟩ :=
  h1.exists_monotone_subseq (fun n => h.natEmbedding _ n) fun n => (h.natEmbedding _ n).2

Result:
case intro
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 => x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 => x1 ≤ x2)
isrfl : IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
istrns : IsTrans (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
g : ℕ ↪o ℕ
hg :
  ∀ (m n : ℕ),
    m ≤ n →
      (Prod.fst ⁻¹'o fun x1 x2 => x1 ≤ x2) ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g m))
        ↑((Infinite.natEmbedding (s.smulAntidiagonal t a) h) (g n))
⊢ False

Proof state:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 => x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 => x1 ≤ x2)
⊢ IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)

Tactic:
refine { refl := ?refl }

Result:
case refl
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 => x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 => x1 ≤ x2)
⊢ ∀ (a : G × P), (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) a a

Proof state:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 => x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 => x1 ≤ x2)
isrfl : IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
⊢ False

Tactic:
have istrns : IsTrans (G × P) (Prod.fst ⁻¹'o fun x x_1 ↦ x ≤ x_1) := by
  refine { trans := ?trans }
  simp_all only [Order.Preimage, Prod.forall]
  exact fun a _ a_1 _ a_2 _ a_3 a_4 ↦ Preorder.le_trans a a_1 a_2 a_3 a_4

Result:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 => x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 => x1 ≤ x2)
isrfl : IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
istrns : IsTrans (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
⊢ False

Proof state:
case refl
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 => x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 => x1 ≤ x2)
⊢ ∀ (a : G × P), (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) a a

Tactic:
simp_all only [Order.Preimage, le_refl, Prod.forall, implies_true]

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 => x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 => x1 ≤ x2)
⊢ False

Tactic:
have isrfl : IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 ↦ x ≤ x_1) := by
  refine { refl := ?refl }
  simp_all only [Order.Preimage, le_refl, Prod.forall, implies_true]

Result:
G : Type u_1
P : Type u_2
s : Set G
t : Set P
inst✝³ : PartialOrder G
inst✝² : PartialOrder P
inst✝¹ : SMul G P
inst✝ : IsOrderedCancelSMul G P
hs : s.IsPWO
ht : t.IsPWO
a : P
h : (s.smulAntidiagonal t a).Infinite
h1 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.fst ⁻¹'o fun x1 x2 => x1 ≤ x2)
h2 : (s.smulAntidiagonal t a).PartiallyWellOrderedOn (Prod.snd ⁻¹'o fun x1 x2 => x1 ≤ x2)
isrfl : IsRefl (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)
⊢ False