awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h_1 : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l : List α | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l : List α | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)).head! (f ((g : (a : ℕ) → ℕ) n)).head!
hf' :
  ∀
    (_ :
      ∀ (n : ℕ),
        Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s}
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)),
    ∃ (m : ℕ) (n : ℕ),
      m < n ∧
        List.SublistForall₂ r
          (if m < (g : (a : ℕ) → ℕ) 0 then f m
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
m n' : ℕ
mn : m < HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n'
hmn :
  List.SublistForall₂ r
    (if m < (g : (a : ℕ) → ℕ) 0 then f m
    else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
    (if HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n' < (g : (a : ℕ) → ℕ) 0 then
      f (HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n')
    else
      (f
          ((g : (a : ℕ) → ℕ)
            (HSub.hSub (β := ℕ) (HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n') ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
hn : ¬HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n' < (g : (a : ℕ) → ℕ) 0
⊢ False
have hmn₁ : List.SublistForall₂ r
  (if m < (g : (a : ℕ) → ℕ) 0 then f m
  else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
  (f ((g : (a : ℕ) → ℕ) n')).tail
Tactic: rw [if_neg hn, add_comm (g 0) n', Nat.add_sub_cancel_right] at hmn
Cleared hypotheses: hmn, hn
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h_1 : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l : List α | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l : List α | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)).head! (f ((g : (a : ℕ) → ℕ) n)).head!
hf' :
  ∀
    (_ :
      ∀ (n : ℕ),
        Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s}
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)),
    ∃ (m : ℕ) (n : ℕ),
      m < n ∧
        List.SublistForall₂ r
          (if m < (g : (a : ℕ) → ℕ) 0 then f m
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
m n' : ℕ
mn : m < HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n'
hmn :
  List.SublistForall₂ r
    (if m < (g : (a : ℕ) → ℕ) 0 then f m
    else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
    (f ((g : (a : ℕ) → ℕ) n')).tail
hn : ¬HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n' < (g : (a : ℕ) → ℕ) 0
⊢ False
have pos : ∀ (hm : m < (g : (a : ℕ) → ℕ) 0) (hmn : List.SublistForall₂ r (f m) (f ((g : (a : ℕ) → ℕ) n')).tail), False
Tactic: split_ifs at hmn with hm
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h_1 : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l : List α | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l : List α | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)).head! (f ((g : (a : ℕ) → ℕ) n)).head!
hf' :
  ∀
    (_ :
      ∀ (n : ℕ),
        Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s}
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)),
    ∃ (m : ℕ) (n : ℕ),
      m < n ∧
        List.SublistForall₂ r
          (if m < (g : (a : ℕ) → ℕ) 0 then f m
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
m n' : ℕ
mn : m < HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n'
hmn :
  List.SublistForall₂ r
    (if m < (g : (a : ℕ) → ℕ) 0 then f m
    else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
    (f ((g : (a : ℕ) → ℕ) n')).tail
hn : ¬HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n' < (g : (a : ℕ) → ℕ) 0
pos : ∀ (hm : m < (g : (a : ℕ) → ℕ) 0) (hmn : List.SublistForall₂ r (f m) (f ((g : (a : ℕ) → ℕ) n')).tail), False
⊢ False
have neg : ∀ (hm : ¬m < (g : (a : ℕ) → ℕ) 0)
  (hmn :
    List.SublistForall₂ r (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail
      (f ((g : (a : ℕ) → ℕ) n')).tail),
  False
Tactic: split_ifs at hmn with hm
Cleared hypotheses: hmn
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h_1 : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l : List α | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l : List α | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)).head! (f ((g : (a : ℕ) → ℕ) n)).head!
hf' :
  ∀
    (_ :
      ∀ (n : ℕ),
        Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s}
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)),
    ∃ (m : ℕ) (n : ℕ),
      m < n ∧
        List.SublistForall₂ r
          (if m < (g : (a : ℕ) → ℕ) 0 then f m
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
m n' : ℕ
mn : m < HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n'
hn : ¬HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n' < (g : (a : ℕ) → ℕ) 0
hm : m < (g : (a : ℕ) → ℕ) 0
hmn : List.SublistForall₂ r (f m) (f ((g : (a : ℕ) → ℕ) n')).tail
⊢ False
have pos : List.SublistForall₂ r (f m) (f ((g : (a : ℕ) → ℕ) n'))
Tactic: apply hf1.2 m (g n') (lt_of_lt_of_le hm (g.monotone n'.zero_le))
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h_1 : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l : List α | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l : List α | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)).head! (f ((g : (a : ℕ) → ℕ) n)).head!
hf' :
  ∀
    (_ :
      ∀ (n : ℕ),
        Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s}
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)),
    ∃ (m : ℕ) (n : ℕ),
      m < n ∧
        List.SublistForall₂ r
          (if m < (g : (a : ℕ) → ℕ) 0 then f m
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
m n' : ℕ
mn : m < HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n'
hn : ¬HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n' < (g : (a : ℕ) → ℕ) 0
hm : ¬m < (g : (a : ℕ) → ℕ) 0
hmn :
  List.SublistForall₂ r (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail
    (f ((g : (a : ℕ) → ℕ) n')).tail
⊢ False
have mn₁ : HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ) < n'
Tactic: rw [← Nat.sub_lt_iff_lt_add' (le_of_not_gt hm)] at mn
Cleared hypotheses: mn, hn, hm, hmn
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h_1 : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l : List α | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l : List α | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)).head! (f ((g : (a : ℕ) → ℕ) n)).head!
hf' :
  ∀
    (_ :
      ∀ (n : ℕ),
        Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s}
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)),
    ∃ (m : ℕ) (n : ℕ),
      m < n ∧
        List.SublistForall₂ r
          (if m < (g : (a : ℕ) → ℕ) 0 then f m
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
m n' : ℕ
mn : HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ) < n'
hn : ¬HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n' < (g : (a : ℕ) → ℕ) 0
hm : ¬m < (g : (a : ℕ) → ℕ) 0
hmn :
  List.SublistForall₂ r (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail
    (f ((g : (a : ℕ) → ℕ) n')).tail
⊢ False
have neg : List.SublistForall₂ r (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ))))
  (f ((g : (a : ℕ) → ℕ) n'))
Tactic: apply hf1.2 _ _ (g.lt_iff_lt.2 mn)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h_1 : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l : List α | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l : List α | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)).head! (f ((g : (a : ℕ) → ℕ) n)).head!
hf' :
  ∀
    (_ :
      ∀ (n : ℕ),
        Membership.mem (γ := Set (List α)) {l : List α | ∀ x ∈ l, x ∈ s}
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)),
    ∃ (m : ℕ) (n : ℕ),
      m < n ∧
        List.SublistForall₂ r
          (if m < (g : (a : ℕ) → ℕ) 0 then f m
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
          (if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
m n' : ℕ
mn : HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ) < n'
hn : ¬HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n' < (g : (a : ℕ) → ℕ) 0
hm : ¬m < (g : (a : ℕ) → ℕ) 0
hmn :
  List.SublistForall₂ r (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail
    (f ((g : (a : ℕ) → ℕ) n')).tail
⊢ List.SublistForall₂ r (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ))))
    (f ((g : (a : ℕ) → ℕ) n'))
have neg : List.SublistForall₂ r
  ((f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).head! ::
    (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
  ((f ((g : (a : ℕ) → ℕ) n')).head! :: (f ((g : (a : ℕ) → ℕ) n')).tail)
Tactic: rw [← List.cons_head!_tail (hnil (g (m - g 0))), ← List.cons_head!_tail (hnil (g 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α : IsPWO.{u_2} (α := α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s)
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
⊢ s.IsPWO
have rw : ∀ (f : ℕ → Lex (α × β)), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
Tactic: rw [IsPWO, partiallyWellOrderedOn_iff_exists_lt]
-- 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α : IsPWO.{u_2} (α := α) ((fun (x : Lex (α × β)) ↦ ((ofLex : (a : Lex (α × β)) → α × β) x).1) '' s)
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
have rw : ∀
  (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), ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
Tactic: rw [isPWO_iff_exists_monotone_subseq] at hα
Cleared hypotheses: hα, hβ, f, 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
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
have obtain : ∀ (g : ℕ ↪o ℕ)
  (hg :
    Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1),
  ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
Tactic: obtain ⟨g, hg⟩ : ∃ (g : (ℕ ↪o ℕ)), Monotone fun n => (ofLex f (g n)).1 :=
    hα (fun n => (ofLex f n).1) (fun k => mem_image_of_mem (fun x => (ofLex x).1) (hf k))
-- 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
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
have 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
Tactic: have hhg : ∀ n, (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1 := fun n => hg n.zero_le
-- 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
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
have pos : ∀
  (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
Tactic: by_cases! hc : ∃ n, (ofLex f (g 0)).1 < (ofLex f (g n)).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
pos :
  ∀
    (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
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
have neg : ∀
  (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
Tactic: by_cases! hc : ∃ n, (ofLex f (g 0)).1 < (ofLex f (g n)).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
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
have pos : ∀ (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),
  ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
Tactic: obtain ⟨n, hn⟩ := hc
Cleared hypotheses: hc
-- 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
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
have h : LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) ((g : (a : ℕ) → ℕ) n : ℕ) ∧ f ((g : (a : ℕ) → ℕ) 0) ≤ f ((g : (a : ℕ) → ℕ) n)
Tactic: use (g 0), (g 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
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 : ℕ) ∧ f ((g : (a : ℕ) → ℕ) 0) ≤ f ((g : (a : ℕ) → ℕ) n)
have h : LT.lt (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) ((g : (a : ℕ) → ℕ) n : ℕ)
Tactic: constructor