awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
h : ∀ (m n : ℕ), m ≤ n → (↑(fs m) : ℕ → α) m = (↑(fs n) : ℕ → α) m
⊢ ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
⟨fun n => (fs n).1 n, ⟨fun n => (fs n).2.1.1 n, fun m n mn => ?_⟩, fun n g hg1 hg2 => ?_⟩

Premises used: And.left, And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
h : ∀ (m n : ℕ), m ≤ n → (↑(fs m) : ℕ → α) m = (↑(fs n) : ℕ → α) m
refine_1 : ∀ (m n : ℕ) (mn : m < n), ¬r ((fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) m) ((fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) n)
refine_2 :
  ∀ (n : ℕ) (g : ℕ → α) (hg1 : ∀ m < n, (fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) m = g m)
    (hg2 : rk (g n) < rk ((fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) n)), ¬IsBadSeq r s g
⊢ ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
refine ⟨fun n => (fs n).1 n, ⟨fun n => (fs n).2.1.1 n, fun m n mn => ?_⟩, fun n g hg1 hg2 => ?_⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
h : ∀ (m n : ℕ), m ≤ n → (↑(fs m) : ℕ → α) m = (↑(fs n) : ℕ → α) m
m n : ℕ
mn : m < n
refine_1 : ¬r ((↑(fs m) : ℕ → α) m) ((↑(fs n) : ℕ → α) n)
⊢ ¬r ((fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) m) ((fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) n)

Tactic:
dsimp
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
h : ∀ (m n : ℕ), m ≤ n → (↑(fs m) : ℕ → α) m = (↑(fs n) : ℕ → α) m
m n : ℕ
mn : m < n
refine_1 : ¬r ((↑(fs n) : ℕ → α) m) ((↑(fs n) : ℕ → α) n)
⊢ ¬r ((↑(fs m) : ℕ → α) m) ((↑(fs n) : ℕ → α) n)

Tactic:
rw [h m n mn.le]

Premises used: LT.lt.le
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
h : ∀ (m n : ℕ), m ≤ n → (↑(fs m) : ℕ → α) m = (↑(fs n) : ℕ → α) m
m n : ℕ
mn : m < n
⊢ ¬r ((↑(fs n) : ℕ → α) m) ((↑(fs n) : ℕ → α) n)

Tactic:
(fs n).2.1.2 m n mn

Premises used: And.right, And.left, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
h : ∀ (m n : ℕ), m ≤ n → (↑(fs m) : ℕ → α) m = (↑(fs n) : ℕ → α) m
m n : ℕ
mn : m < n
⊢ ¬r ((↑(fs n) : ℕ → α) m) ((↑(fs n) : ℕ → α) n)

Tactic:
exact (fs n).2.1.2 m n mn

Premises used: And.right, And.left, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
h : ∀ (m n : ℕ), m ≤ n → (↑(fs m) : ℕ → α) m = (↑(fs n) : ℕ → α) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) m = g m
hg2 : rk (g n) < rk ((fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) n)
⊢ ¬IsBadSeq r s g

Tactic:
(fs n).2.2 g (fun m mn => ?_) hg2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
h : ∀ (m n : ℕ), m ≤ n → (↑(fs m) : ℕ → α) m = (↑(fs n) : ℕ → α) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) m = g m
hg2 : rk (g n) < rk ((fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) n)
refine_2 : ∀ (m : ℕ) (mn : m < n), (↑(fs n) : ℕ → α) m = g m
⊢ ¬IsBadSeq r s g

Tactic:
refine (fs n).2.2 g (fun m mn => ?_) hg2

Premises used: And.right, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s x f })
      (Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f)
        (↑(minBadSeqOfBadSeq r rk s 0 f0 hf0) : ℕ → α) ⋯)
      (fun (n : ℕ) (fn : { f : ℕ → α // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }) ↦
        Subtype.mk (p := fun (f : ℕ → α) ↦ IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f)
          (↑(minBadSeqOfBadSeq r rk s (n + 1) (↑fn : ℕ → α) ⋯) : ℕ → α) ⋯)
      t
h : ∀ (m n : ℕ), m ≤ n → (↑(fs m) : ℕ → α) m = (↑(fs n) : ℕ → α) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) m = g m
hg2 : rk (g n) < rk ((fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) n)
m : ℕ
mn : m < n
refine_2 : (↑(fs m) : ℕ → α) m = g m
refine_2₁ refine_2₂ : (↑(fs m) : ℕ → α) m = (fun (n : ℕ) ↦ (↑(fs n) : ℕ → α) n) m
⊢ (↑(fs n) : ℕ → α) m = g m

Tactic:
rw [← h m n mn.le, ← hg1 m mn]

Premises used: LT.lt.le
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
rw : (∃ (x : ℕ → α), IsBadSeq r s x) ↔ ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
⊢ s.PartiallyWellOrderedOn r ↔ ¬∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
rw [iff_forall_not_isBadSeq, ← not_exists, not_congr]

Premises used: not_exists, not_congr, Set.PartiallyWellOrderedOn.iff_forall_not_isBadSeq
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
mp : (∃ (x : ℕ → α), IsBadSeq r s x) → ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f
mpr : (∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f) → ∃ (x : ℕ → α), IsBadSeq r s x
⊢ (∃ (x : ℕ → α), IsBadSeq r s x) ↔ ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
constructor
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ (x : ℕ → α), IsBadSeq r s x) → ∃ (f : ℕ → α), IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f

Tactic:
apply exists_min_bad_of_exists_bad

Premises used: Set.PartiallyWellOrderedOn.exists_min_bad_of_exists_bad
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f : ℕ → α
hf1 : IsBadSeq r s f
⊢ ∃ (x : ℕ → α), IsBadSeq r s x

Tactic:
⟨f, hf1⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f : ℕ → α
hf1 : IsBadSeq r s f
⊢ ∃ (x : ℕ → α), IsBadSeq r s x

Tactic:
exact ⟨f, hf1⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
inl : IsEmpty α → PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)
inr : Nonempty α → PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)
⊢ PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)

Tactic:
rcases isEmpty_or_nonempty α

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h_1 : IsEmpty α
⊢ PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)

Tactic:
subsingleton_of_subsingleton.partiallyWellOrderedOn

Premises used: Set.Subsingleton.partiallyWellOrderedOn, Set.subsingleton_of_subsingleton
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h_1 : IsEmpty α
⊢ PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)

Tactic:
exact subsingleton_of_subsingleton.partiallyWellOrderedOn

Premises used: Set.Subsingleton.partiallyWellOrderedOn, Set.subsingleton_of_subsingleton
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h_1 : Nonempty α
inr : ∀ (inhabited_h : Inhabited α), PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)
⊢ PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)

Tactic:
inhabit α
-- 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 α
inr :
  ¬∃ (f : ℕ → List α),
      IsBadSeq (List.SublistForall₂ r) {l : List α | ∀ x ∈ l, x ∈ s} f ∧
        ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l : List α | ∀ x ∈ l, x ∈ s} n f
⊢ PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)

Tactic:
rw [iff_not_exists_isMinBadSeq List.length]

Premises used: Set.PartiallyWellOrderedOn.iff_not_exists_isMinBadSeq, List.length
-- 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
⊢ ∀ (n : ℕ), f n ≠ []

Tactic:
have hnil : ∀ n, f n ≠ List.nil := fun n con =>
    hf1.2 n n.succ n.lt_succ_self (con.symm ▸ List.SublistForall₂.nil)
-- 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 ≠ []
inr :
  ∀ (g : ℕ ↪o ℕ) (hg : ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)).head! (f ((g : (a : ℕ) → ℕ) n)).head!), False
⊢ False

Tactic:
obtain ⟨g, hg⟩ := h.exists_monotone_subseq fun n => hf1.1 n _ (List.head!_mem_self (hnil n))

Premises used: List.head!_mem_self, Set.PartiallyWellOrderedOn.exists_monotone_subseq, List.head!, 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!
inr :
  ∀
    (hf' :
      ¬IsBadSeq (List.SublistForall₂ r) {l : List α | ∀ x ∈ l, x ∈ s} fun (n : ℕ) ↦
          if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail),
    False
inr₁ :
  List.length.{u_2} (α := α)
      ((fun (n : ℕ) ↦
          if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
        ((g : (a : ℕ) → ℕ) 0)) <
    (f ((g : (a : ℕ) → ℕ) 0)).length
⊢ False

Tactic:
have hf' :=
    hf2 (g 0) (fun n => if n < g 0 then f n else List.tail (f (g (n - g 0))))
      (fun m hm => (if_pos hm).symm) ?_
-- 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!
inr : (f ((g : (a : ℕ) → ℕ) 0)).tail.length < (f ((g : (a : ℕ) → ℕ) 0)).length
⊢ List.length.{u_2} (α := α)
      ((fun (n : ℕ) ↦
          if n < (g : (a : ℕ) → ℕ) 0 then f n
          else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail)
        ((g : (a : ℕ) → ℕ) 0)) <
    (f ((g : (a : ℕ) → ℕ) 0)).length

Tactic:
simp only [if_neg (lt_irrefl (g 0)), Nat.sub_self]

Premises used: lt_irrefl, Nat.sub_self, 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!
inr : (f ((g : (a : ℕ) → ℕ) 0)).length.pred < (f ((g : (a : ℕ) → ℕ) 0)).length
⊢ (f ((g : (a : ℕ) → ℕ) 0)).tail.length < (f ((g : (a : ℕ) → ℕ) 0)).length

Tactic:
rw [List.length_tail, ← Nat.pred_eq_sub_one]

Premises used: Nat.pred_eq_sub_one, List.length_tail
-- 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!
⊢ (f ((g : (a : ℕ) → ℕ) 0)).length.pred < (f ((g : (a : ℕ) → ℕ) 0)).length

Tactic:
Nat.pred_lt fun con => hnil _ (List.length_eq_zero_iff.1 con)

Premises used: Nat.pred_lt, Iff.mp, OfNat.ofNat, DFunLike.coe, List.length_eq_zero_iff
-- 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!
⊢ (f ((g : (a : ℕ) → ℕ) 0)).length.pred < (f ((g : (a : ℕ) → ℕ) 0)).length

Tactic:
exact Nat.pred_lt fun con => hnil _ (List.length_eq_zero_iff.1 con)

Premises used: Nat.pred_lt, Iff.mp, List.length_eq_zero_iff
-- 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' :
  ¬IsBadSeq (List.SublistForall₂ r) {l : List α | ∀ x ∈ l, x ∈ s} fun (n : ℕ) ↦
      if n < (g : (a : ℕ) → ℕ) 0 then f n
      else (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail
⊢ ¬((∀ (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))

Tactic:
rw [IsBadSeq] at hf'

Premises used: Set.PartiallyWellOrderedOn.IsBadSeq
-- 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 : ℕ),
        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)

Tactic:
push Not at hf'

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

Tactic:
split_ifs at hx with hn