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

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)
⊢ IsTrans (G × P) (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1)

Tactic:
refine { trans := ?trans }

Result:
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 b c : G × P),
    (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) a b →
      (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) b c → (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) a c

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))
⊢ False

Tactic:
refine mn.ne (g.injective <| (h.natEmbedding _).injective ?_)

Result:
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)

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 b c : G × P),
    (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) a b →
      (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) b c → (Prod.fst ⁻¹'o fun x x_1 => x ≤ x_1) a c

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

Result:
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

Proof state:
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

Tactic:
obtain ⟨m, n, mn, h2'⟩ := h2 (fun x => (h.natEmbedding _) (g x)) fun n => (h.natEmbedding _ _).2

Result:
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))
⊢ 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
⊢ (s.smulAntidiagonal t a).Finite

Tactic:
refine Set.not_infinite.1 fun h => ?_

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
⊢ False