awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellFoundedSet
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
⊢ HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ) < n'

Tactic:
rw [← Nat.sub_lt_iff_lt_add' (le_of_not_gt hm)] at mn

Premises used: le_of_not_gt, Nat.sub_lt_iff_lt_add'
-- Module: Mathlib.Order.WellFoundedSet
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
mn₁ : HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ) < n'
⊢ ¬HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n' < (g : (a : ℕ) → ℕ) 0

Tactic:
rw [← Nat.sub_lt_iff_lt_add' (le_of_not_gt hm)] at mn

Premises used: le_of_not_gt, Nat.sub_lt_iff_lt_add'
-- Module: Mathlib.Order.WellFoundedSet
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
mn₁ : HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ) < n'
hn₁ : ¬HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n' < (g : (a : ℕ) → ℕ) 0
⊢ ¬m < (g : (a : ℕ) → ℕ) 0

Tactic:
rw [← Nat.sub_lt_iff_lt_add' (le_of_not_gt hm)] at mn

Premises used: le_of_not_gt, Nat.sub_lt_iff_lt_add'
-- Module: Mathlib.Order.WellFoundedSet
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
mn₁ : HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ) < n'
hn₁ : ¬HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n' < (g : (a : ℕ) → ℕ) 0
hm₁ : ¬m < (g : (a : ℕ) → ℕ) 0
⊢ List.SublistForall₂ r (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail
    (f ((g : (a : ℕ) → ℕ) n')).tail

Tactic:
rw [← Nat.sub_lt_iff_lt_add' (le_of_not_gt hm)] at mn

Premises used: le_of_not_gt, Nat.sub_lt_iff_lt_add'
-- Module: Mathlib.Order.WellFoundedSet
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
neg :
  List.SublistForall₂ r (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ))))
    (f ((g : (a : ℕ) → ℕ) n'))
⊢ False

Tactic:
apply hf1.2 _ _ (g.lt_iff_lt.2 mn)

Premises used: Iff.mpr, And.right, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Order.WellFoundedSet
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
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)
⊢ List.SublistForall₂ r (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ))))
    (f ((g : (a : ℕ) → ℕ) n'))

Tactic:
rw [← List.cons_head!_tail (hnil (g (m - g 0))), ← List.cons_head!_tail (hnil (g n'))]

Premises used: HSub.hSub, List.cons_head!_tail, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Order.WellFoundedSet
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 : ℕ)))).head! ::
      (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
    ((f ((g : (a : ℕ) → ℕ) n')).head! :: (f ((g : (a : ℕ) → ℕ) n')).tail)

Tactic:
List.SublistForall₂.cons (hg _ _ (le_of_lt mn)) hmn

Premises used: List.SublistForall₂.cons, le_of_lt
-- Module: Mathlib.Order.WellFoundedSet
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 : ℕ)))).head! ::
      (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
    ((f ((g : (a : ℕ) → ℕ) n')).head! :: (f ((g : (a : ℕ) → ℕ) n')).tail)

Tactic:
exact List.SublistForall₂.cons (hg _ _ (le_of_lt mn)) hmn

Premises used: List.SublistForall₂.cons, le_of_lt
-- Module: Mathlib.Order.WellFoundedSet
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 (α × β))}
rw : ∀ (f : ℕ → Lex (α × β)), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n
⊢ s.IsPWO

Tactic:
rw [IsPWO, partiallyWellOrderedOn_iff_exists_lt]

Premises used: Set.IsPWO, Set.partiallyWellOrderedOn_iff_exists_lt
-- Module: Mathlib.Order.WellFoundedSet
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
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
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n

Tactic:
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 : ℕ) → ℕ))
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 ℕ),
    Monotone.{0, u_2} (β := α) fun (n : ℕ) ↦
      ((ofLex : (a : Lex (ℕ → Lex (α × β))) → ℕ → Lex (α × β)) f ((g : (a : ℕ) → ℕ) n)).1

Tactic:
hα (fun n => (ofLex f n).1) (fun k => mem_image_of_mem (fun x => (ofLex x).1) (hf k))

Premises used: Prod.fst, ofLex, 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 : ℕ) → ℕ))
hβ :
  ∀ (a : α),
    IsPWO.{u_3} (α := β)
      {y : β | Membership.mem (α := Lex (α × β)) s ((toLex : (a : α × β) → Lex (α × β)) (a, y) : Lex (α × β))}
f : ℕ → Lex (α × β)
hf : ∀ (n : ℕ), f n ∈ s
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
⊢ ∃ (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))

Premises used: Prod.fst, Nat, OrderEmbedding, ofLex, 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 : ℕ) → ℕ))
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
⊢ ∀ (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
-- 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
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
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
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n

Tactic:
by_cases! hc : ∃ n, (ofLex f (g 0)).1 < (ofLex f (g n)).1

Premises used: Prod.fst, ofLex, OfNat.ofNat, 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 : ℕ) → ℕ))
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
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
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n

Tactic:
obtain ⟨n, hn⟩ := hc
-- 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 : ℕ) ∧ f ((g : (a : ℕ) → ℕ) 0) ≤ f ((g : (a : ℕ) → ℕ) n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ f m ≤ f n

Tactic:
use (g 0), (g n)

Premises used: OfNat.ofNat, DFunLike.coe