awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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 : ℕ)
⊢ LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) ((g : (a : ℕ) → ℕ) n : ℕ) ∧ f ((g : (a : ℕ) → ℕ) 0) ≤ f ((g : (a : ℕ) → ℕ) n)
have h₁ : f ((g : (a : ℕ) → ℕ) 0) ≤ f ((g : (a : ℕ) → ℕ) n)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) ((g : (a : ℕ) → ℕ) n : ℕ)
have h : ∀ (hx : ¬LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) ((g : (a : ℕ) → ℕ) n : ℕ)), False
Tactic: by_contra hx
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
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
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
have 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
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)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
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 ℕ),
    Monotone.{0, u_3} (β := β) fun (n : ℕ) ↦
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) n : ℕ))).2
have 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 : ℕ) → ℕ))
Tactic: simp_rw [isPWO_iff_exists_monotone_subseq] at hβ
Cleared hypotheses: hβ
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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 : ℕ) → ℕ))
⊢ ∃ (g' : ℕ ↪o ℕ),
    Monotone.{0, u_3} (β := β) fun (n : ℕ) ↦
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) n : ℕ))).2
have 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
Tactic: apply hβ (ofLex f (g 0)).1 fun n ↦ (ofLex f (g n)).2
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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 : ℕ) → ℕ) 0)).1, y) :
          Lex (α × β))}
    ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).2
have 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
Tactic: rw [hhc n]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
have 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
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 _
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
have 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 : ℕ))
Tactic: use (g (g' 0)), (g (g' 1))
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ) : ℕ) ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ) : ℕ) ∧
    f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ)) ≤ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))
have h : f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ)) ≤ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))
Tactic: suffices (f (g (g' 0))) ≤ (f (g (g' 1))) by simpa
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ)) ≤ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))
have h : (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ))).1 = (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))).1
Tactic: refine Prod.Lex.toLex_le_toLex.mpr <| .inr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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 : (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ))).1 = (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))).1
⊢ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ)) ≤ f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))
have h₁ : (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 0 : ℕ))).2 ≤ (f ((g : (a : ℕ) → ℕ) ((g' : (a : ℕ) → ℕ) 1 : ℕ))).2
Tactic: refine Prod.Lex.toLex_le_toLex.mpr <| .inr ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
⊢ {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
have h : ∀ (x : β),
  Membership.mem (γ := Set β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} x ↔
    x ∈ f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
⊢ IsPWO.{u_3} (α := β)
    {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
have h : {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
  f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
Tactic: have h : {y | toLex (a, y) ∈ s} = f '' (s ∩ (fun x ↦ (ofLex x).1) ⁻¹' {a}) := by
    ext x
    simp [f]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
h :
  {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
⊢ IsPWO.{u_3} (α := β)
    {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
have rw : (f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})).IsPWO
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
h :
  {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
⊢ (f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})).IsPWO
have apply : MonotoneOn f (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
Tactic: apply IsPWO.image_of_monotoneOn (hαβ.mono inter_subset_left)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set (Lex (α × β))
hαβ : s.IsPWO
a : α
f : Lex (α × β) → β := fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).2
h :
  {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))} =
    f '' (s ∩ preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a})
b : Lex (α × β)
hb :
  Membership.mem (γ := Set (Lex (α × β)))
    (preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a}) b
c : Lex (α × β)
hc :
  Membership.mem (γ := Set (Lex (α × β)))
    (preimage (β := α) (fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) {a}) c
hbc : b ≤ c
⊢ f b ≤ f c
have hb₁ : ((ofLex : (a : Lex (α × β)) → α × β) b).1 = a
Tactic: simp only [mem_preimage, mem_singleton_iff] at hb hc
Cleared hypotheses: hb, hc