-- Mathlib/Order/WellFoundedSet.lean
theorem partiallyWellOrderedOn_sublistForall₂ (r : α → α → Prop) [IsRefl α r] [IsTrans α r]
    {s : Set α} (h : s.PartiallyWellOrderedOn r) :
    { l : List α | ∀ x, x ∈ l → x ∈ s }.PartiallyWellOrderedOn (List.SublistForall₂ r)

Proof state:
case inr.intro.intro.intro.refine_1
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), (f n).headI ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI
⊢ ((fun n => if n < g 0 then f n else (f (g (n - g 0))).tail) (g 0)).length < (f (g 0)).length

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

Result:
case inr.intro.intro.intro.refine_1
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), (f n).headI ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI
⊢ (f (g 0)).tail.length < (f (g 0)).length

Proof state:
case neg
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), (f n).headI ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m - g 0 < n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ List.SublistForall₂ r (f (g (m - g 0))) (f (g n'))

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

Result:
case neg
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), (f n).headI ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n' : ℕ
mn : m - g 0 < n'
hn : ¬g 0 + n' < g 0
hm : ¬m < g 0
hmn : List.SublistForall₂ r (f (g (m - g 0))).tail (f (g n')).tail
⊢ List.SublistForall₂ r ((f (g (m - g 0))).head! :: (f (g (m - g 0))).tail) ((f (g n')).head! :: (f (g n')).tail)

Proof state:
case inr.intro.intro
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
⊢ False

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)

Result:
case inr.intro.intro
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
⊢ False

Proof state:
case inl
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : IsEmpty α
⊢ {l | ∀ x ∈ l, x ∈ s}.PartiallyWellOrderedOn (List.SublistForall₂ r)

Tactic:
exact subsingleton_of_subsingleton.partiallyWellOrderedOn

Result:
no goals

Proof state:
case inr.intro.intro.intro.refine_2.intro.intro.intro
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), (f n).headI ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
    (if n < g 0 then f n else (f (g (n - g 0))).tail)
⊢ False

Tactic:
by_cases hn : n < g 0

Result:
case pos
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), (f n).headI ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
    (if n < g 0 then f n else (f (g (n - g 0))).tail)
hn : n < g 0
⊢ False

case neg
α : Type u_2
r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), (f n).headI ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).headI (f (g n)).headI
hf' :
  (∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
          (if n < g 0 then f n else (f (g (n - g 0))).tail)
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
    (if n < g 0 then f n else (f (g (n - g 0))).tail)
hn : ¬n < g 0
⊢ False