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)
n : ℕ
x : α
hn : n < (g : (a : ℕ) → ℕ) 0
hx : x ∈ f n
⊢ x ∈ s

Tactic:
hf1.1 _ _ hx

Premises used: And.left
-- 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)
n : ℕ
x : α
hn : ¬n < (g : (a : ℕ) → ℕ) 0
hx : x ∈ (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail
⊢ x ∈ s

Tactic:
hf1.1 _ _ (List.tail_subset _ hx)

Premises used: And.left, List.tail_subset
-- 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)
n : ℕ
x : α
hn : n < (g : (a : ℕ) → ℕ) 0
hx : x ∈ f n
⊢ x ∈ s

Tactic:
exacts [hf1.1 _ _ hx, hf1.1 _ _ (List.tail_subset _ hx)]

Premises used: And.left, List.tail_subset
-- 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)
inr :
  ∀ (m n : ℕ) (mn : m < 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 n < (g : (a : ℕ) → ℕ) 0 then f n
        else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)),
    False
⊢ False

Tactic:
obtain ⟨m, n, mn, hmn⟩ := hf' fun n x hx => by
    split_ifs at hx with hn
    exacts [hf1.1 _ _ hx, hf1.1 _ _ (List.tail_subset _ hx)]
-- 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 < 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 n < (g : (a : ℕ) → ℕ) 0 then f n
    else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
pos : ∀ (hn : n < (g : (a : ℕ) → ℕ) 0), False
neg : ∀ (hn : ¬n < (g : (a : ℕ) → ℕ) 0), False
⊢ False

Tactic:
by_cases hn : n < g 0

Premises used: 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 : m < 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 n < (g : (a : ℕ) → ℕ) 0 then f n
    else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
hn : n < (g : (a : ℕ) → ℕ) 0
pos : List.SublistForall₂ r (f m) (f n)
⊢ False

Tactic:
apply hf1.2 m n mn

Premises used: And.right
-- 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 < 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 n < (g : (a : ℕ) → ℕ) 0 then f n
    else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
hn : n < (g : (a : ℕ) → ℕ) 0
pos :
  ∀
    (hmn :
      List.SublistForall₂ r
        (if m < (g : (a : ℕ) → ℕ) 0 then f m
        else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) m ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
        (f n))
    (hn : n < (g : (a : ℕ) → ℕ) 0), List.SublistForall₂ r (f m) (f n)
pos₁ pos₂ pos₃ pos₄ :
  ∀ (hmn : List.SublistForall₂ r (f m) (f n)) (hn : n < (g : (a : ℕ) → ℕ) 0), List.SublistForall₂ r (f m) (f n)
⊢ List.SublistForall₂ r (f m) (f n)

Tactic:
rwa [if_pos hn, if_pos (mn.trans hn)] at hmn

Premises used: if_pos, LT.lt.trans
-- 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 < 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 n < (g : (a : ℕ) → ℕ) 0 then f n
    else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
hn : ¬n < (g : (a : ℕ) → ℕ) 0
neg :
  ∀ (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
⊢ False

Tactic:
obtain ⟨n', rfl⟩ := Nat.exists_eq_add_of_le (not_lt.1 hn)

Premises used: Nat.exists_eq_add_of_le, not_lt, Iff.mp, rfl
-- 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'
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
⊢ 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

Premises used: Nat.add_sub_cancel_right, add_comm, OfNat.ofNat, if_neg, 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 : 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
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
⊢ ¬HAdd.hAdd (α := ℕ) ((g : (a : ℕ) → ℕ) 0 : ℕ) n' < (g : (a : ℕ) → ℕ) 0

Tactic:
rw [if_neg hn, add_comm (g 0) n', Nat.add_sub_cancel_right] at hmn

Premises used: Nat.add_sub_cancel_right, add_comm, OfNat.ofNat, if_neg, 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 : 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
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
⊢ False

Tactic:
split_ifs at hmn with hm
-- 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 m) (f ((g : (a : ℕ) → ℕ) n')).tail
pos : List.SublistForall₂ r (f m) (f ((g : (a : ℕ) → ℕ) n'))
⊢ False

Tactic:
apply hf1.2 m (g n') (lt_of_lt_of_le hm (g.monotone n'.zero_le))

Premises used: Nat.zero_le, OrderEmbedding.monotone, And.right, DFunLike.coe, lt_of_lt_of_le
-- 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 m) (f ((g : (a : ℕ) → ℕ) n')).tail
⊢ List.SublistForall₂ r (f m) (f ((g : (a : ℕ) → ℕ) n'))

Tactic:
_root_.trans hmn (List.tail_sublistForall₂_self _)

Premises used: trans, List.tail_sublistForall₂_self
-- 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 m) (f ((g : (a : ℕ) → ℕ) n')).tail
⊢ List.SublistForall₂ r (f m) (f ((g : (a : ℕ) → ℕ) n'))

Tactic:
exact _root_.trans hmn (List.tail_sublistForall₂_self _)

Premises used: trans, List.tail_sublistForall₂_self