awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
n : ℕ
hn :
  LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
h : LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) ((g : (a : ℕ) → ℕ) n : ℕ)
h₁ : f ((g : (a : ℕ) → ℕ) 0) ≤ f ((g : (a : ℕ) → ℕ) n)
⊢ LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) ((g : (a : ℕ) → ℕ) n : ℕ) ∧ f ((g : (a : ℕ) → ℕ) 0) ≤ f ((g : (a : ℕ) → ℕ) n)

Tactic:
constructor
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
n : ℕ
hn :
  LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
h : ∀ (hx : ¬LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) ((g : (a : ℕ) → ℕ) n : ℕ)), False
⊢ LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) ((g : (a : ℕ) → ℕ) n : ℕ)

Tactic:
by_contra hx
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
n : ℕ
hn :
  LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hx : ¬LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) ((g : (a : ℕ) → ℕ) n : ℕ)
⊢ False

Tactic:
simp_all
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
n : ℕ
hn :
  LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
⊢ f ((g : (a : ℕ) → ℕ) 0) ≤ f ((g : (a : ℕ) → ℕ) n)

Tactic:
Prod.Lex.toLex_le_toLex.mpr <| .inl hn

Premises used: Iff.mpr, Or.inl, Prod.Lex.toLex_le_toLex
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
n : ℕ
hn :
  LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
⊢ f ((g : (a : ℕ) → ℕ) 0) ≤ f ((g : (a : ℕ) → ℕ) n)

Tactic:
exact Prod.Lex.toLex_le_toLex.mpr <| .inl hn

Premises used: Iff.mpr, Prod.Lex.toLex_le_toLex
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
n : ℕ
⊢ Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1

Tactic:
(hhg n).eq_of_not_lt (hc n)

Premises used: LE.le.eq_of_not_lt
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
n : ℕ
⊢ Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1

Tactic:
exact (hhg n).eq_of_not_lt (hc n)

Premises used: LE.le.eq_of_not_lt
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
⊢ ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1

Tactic:
have hhc : ∀ n, (ofLex f (g 0)).1 = (ofLex f (g n)).1 := by
      intro n
      exact (hhg n).eq_of_not_lt (hc n)
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
⊢ ∀ (a : α) (f : ℕ → β),
    (∀ (n : ℕ),
        Membership.mem (γ := Set β)
          {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
          (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))

Tactic:
simp_rw [isPWO_iff_exists_monotone_subseq] at hβ

Premises used: Set.isPWO_iff_exists_monotone_subseq
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hβ :
  ∀ (a : α) (f : ℕ → β),
    (∀ (n : ℕ),
        Membership.mem (γ := Set β)
          {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
          (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
apply :
  ∀ (n : ℕ),
    Membership.mem (γ := Set β)
      {y : β |
        Membership.mem (α := Lex (α × β)) s
          ((toLex : (a : α × β) → Lex (α × β))
              (((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1, y) :
            Lex (α × β))}
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).2
⊢ ∃ (g' : ℕ ↪o ℕ),
    Monotone.{0, u_3} (β := β) fun (n : ℕ) ↦
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) n : ℕ))).2

Tactic:
apply hβ (ofLex f (g 0)).1 fun n ↦ (ofLex f (g n)).2

Premises used: Prod.fst, ofLex, OfNat.ofNat, Prod.snd, DFunLike.coe
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hβ :
  ∀ (a : α) (f : ℕ → β),
    (∀ (n : ℕ),
        Membership.mem (γ := Set β)
          {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
          (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
n : ℕ
rw :
  Membership.mem (γ := Set β)
    {y : β |
      Membership.mem (α := Lex (α × β)) s
        ((toLex : (a : α × β) → Lex (α × β))
            (((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1, y) :
          Lex (α × β))}
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).2
⊢ Membership.mem (γ := Set β)
    {y : β |
      Membership.mem (α := Lex (α × β)) s
        ((toLex : (a : α × β) → Lex (α × β))
            (((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1, y) :
          Lex (α × β))}
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).2

Tactic:
rw [hhc n]
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hβ :
  ∀ (a : α) (f : ℕ → β),
    (∀ (n : ℕ),
        Membership.mem (γ := Set β)
          {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
          (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
n : ℕ
⊢ Membership.mem (γ := Set β)
    {y : β |
      Membership.mem (α := Lex (α × β)) s
        ((toLex : (a : α × β) → Lex (α × β))
            (((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1, y) :
          Lex (α × β))}
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).2

Tactic:
simpa using hf _
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
neg :
  ∀ (g' : ℕ ↪o ℕ)
    (hg' :
      Monotone.{0, u_3} (β := β) fun (n : ℕ) ↦
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) n : ℕ))).2),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n

Tactic:
obtain ⟨g', hg'⟩ : ∃ g' : ℕ ↪o ℕ, Monotone ((fun n ↦ (ofLex f (g (g' n))).2)) := by
      simp_rw [isPWO_iff_exists_monotone_subseq] at hβ
      apply hβ (ofLex f (g 0)).1 fun n ↦ (ofLex f (g n)).2
      intro n
      rw [hhc n]
      simpa using hf _
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : PartialOrder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hα :
  ∀ (f : ℕ → α),
    (∀ (n : ℕ),
        Membership.mem (γ := Set α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s) (f n)) →
      ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
g : ℕ ↪o ℕ
hg :
  Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhg :
  ∀ (n : ℕ),
    LE.le.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hc :
  ∀ (n : ℕ),
    ¬LT.lt.{u_2} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
        ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
hhc :
  ∀ (n : ℕ),
    Eq.{u_2 + 1} (α := α) ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) 0)).1
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1
g' : ℕ ↪o ℕ
hg' :
  Monotone.{0, u_3} (β := β) fun (n : ℕ) ↦
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) n : ℕ))).2
h :
  LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ) : ℕ) ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ) : ℕ) ∧
    f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ)) ≤ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n

Tactic:
use (g (g' 0)), (g (g' 1))

Premises used: OfNat.ofNat, DFunLike.coe