case inl
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : IsEmpty α
⊢ PartiallyWellOrderedOn {l | ∀ (x : α), x ∈ l → x ∈ s} (List.SublistForall₂ r)

case inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
⊢ PartiallyWellOrderedOn {l | ∀ (x : α), x ∈ l → x ∈ s} (List.SublistForall₂ r)
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
⊢ PartiallyWellOrderedOn {l | ∀ (x : α), x ∈ l → x ∈ s} (List.SublistForall₂ r)
rcases isEmpty_or_nonempty α
case inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
⊢ PartiallyWellOrderedOn {l | ∀ (x : α), x ∈ l → x ∈ s} (List.SublistForall₂ r)
case inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
⊢ PartiallyWellOrderedOn {l | ∀ (x : α), x ∈ l → x ∈ s} (List.SublistForall₂ r)
inhabit α
case inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
⊢ ¬∃ f,
      IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f ∧
        ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
case inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
⊢ PartiallyWellOrderedOn {l | ∀ (x : α), x ∈ l → x ∈ s} (List.SublistForall₂ r)
rw [iff_not_exists_isMinBadSeq List.length]
case inr.intro.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
⊢ False
case inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
⊢ ¬∃ f,
      IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f ∧
        ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
rintro ⟨f, hf1, hf2⟩
case inr.intro.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
⊢ False
case inr.intro.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
⊢ False
have hnil : ∀ n, f n ≠ List.nil := fun n con =>
  hf1.2 n n.succ n.lt_succ_self (con.symm ▸ List.SublistForall₂.nil)
case this
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
⊢ ∀ (n : ℕ), List.headI (f n) ∈ s

case inr.intro.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
⊢ False
case inr.intro.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
⊢ False
have : ∀ n, (f n).headI ∈ s
case inr.intro.intro.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ False
case inr.intro.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
⊢ False
obtain ⟨g, hg⟩ := h.exists_monotone_subseq (fun n => (f n).headI) this
case inr.intro.intro.intro.refine_2
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  ¬IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} fun n =>
      if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))
⊢ False

case inr.intro.intro.intro.refine_1
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ List.length ((fun n => if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) (↑g 0)) < List.length (f (↑g 0))
case inr.intro.intro.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ False
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) ?_
case inr.intro.intro.intro.refine_1
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ List.length ((fun n => if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) (↑g 0)) < List.length (f (↑g 0))

case inr.intro.intro.intro.refine_2
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  ¬IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} fun n =>
      if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))
⊢ False
case inr.intro.intro.intro.refine_2
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  ¬IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} fun n =>
      if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))
⊢ False

case inr.intro.intro.intro.refine_1
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ List.length ((fun n => if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) (↑g 0)) < List.length (f (↑g 0))
swap
case inr.intro.intro.intro.refine_2
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  ¬((∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) ∧
      ∀ (m n : ℕ),
        m < n →
          ¬List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
              (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))))
⊢ False
case inr.intro.intro.intro.refine_2
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  ¬IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} fun n =>
      if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))
⊢ False
rw [IsBadSeq] at hf'
case inr.intro.intro.intro.refine_2
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
⊢ False
case inr.intro.intro.intro.refine_2
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  ¬((∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) ∧
      ∀ (m n : ℕ),
        m < n →
          ¬List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
              (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))))
⊢ False
push_neg at hf'
case inr.intro.intro.intro.refine_2.intro.intro.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
⊢ False
case inr.intro.intro.intro.refine_2
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
⊢ False
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)]
case pos
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
hn : n < ↑g 0
⊢ False

case neg
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
hn : ¬n < ↑g 0
⊢ False
case inr.intro.intro.intro.refine_2.intro.intro.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
⊢ False
by_cases hn : n < g 0
no goals
case inl
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : IsEmpty α
⊢ PartiallyWellOrderedOn {l | ∀ (x : α), x ∈ l → x ∈ s} (List.SublistForall₂ r)
exact subsingleton_of_subsingleton.partiallyWellOrderedOn
case this
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
⊢ ∀ (n : ℕ), List.headI (f n) ∈ s
case this
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
⊢ ∀ (n : ℕ), List.headI (f n) ∈ s
simp only [Set.range_subset_iff, Function.comp_apply]
no goals
case this
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
⊢ ∀ (n : ℕ), List.headI (f n) ∈ s
exact fun n => hf1.1 n _ (List.head!_mem_self (hnil n))
case inr.intro.intro.intro.refine_1
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ List.length (List.tail (f (↑g 0))) < List.length (f (↑g 0))
case inr.intro.intro.intro.refine_1
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ List.length ((fun n => if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) (↑g 0)) < List.length (f (↑g 0))
simp only [if_neg (lt_irrefl (g 0)), tsub_self]
case inr.intro.intro.intro.refine_1
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ Nat.pred (List.length (f (↑g 0))) < List.length (f (↑g 0))
case inr.intro.intro.intro.refine_1
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ List.length (List.tail (f (↑g 0))) < List.length (f (↑g 0))
rw [List.length_tail, ← Nat.pred_eq_sub_one]
no goals
case inr.intro.intro.intro.refine_1
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
⊢ Nat.pred (List.length (f (↑g 0))) < List.length (f (↑g 0))
exact Nat.pred_lt fun con => hnil _ (List.length_eq_zero.1 con)
case inl
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
n : ℕ
x : α
hn : n < ↑g 0
hx : x ∈ f n
⊢ x ∈ s

case inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
n : ℕ
x : α
hn : ¬n < ↑g 0
hx : x ∈ List.tail (f (↑g (n - ↑g 0)))
⊢ x ∈ s
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
n : ℕ
x : α
hx : x ∈ if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))
⊢ x ∈ s
split_ifs at hx with hn
no goals
case inl
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
n : ℕ
x : α
hn : n < ↑g 0
hx : x ∈ f n
⊢ x ∈ s

case inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
n : ℕ
x : α
hn : ¬n < ↑g 0
hx : x ∈ List.tail (f (↑g (n - ↑g 0)))
⊢ x ∈ s
exacts [hf1.1 _ _ hx, hf1.1 _ _ (List.tail_subset _ hx)]
case pos
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
hn : n < ↑g 0
⊢ List.SublistForall₂ r (f m) (f n)
case pos
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
hn : n < ↑g 0
⊢ False
apply hf1.2 m n mn
no goals
case pos
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
hn : n < ↑g 0
⊢ List.SublistForall₂ r (f m) (f n)
rwa [if_pos hn, if_pos (mn.trans hn)] at hmn
case neg.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if ↑g 0 + n' < ↑g 0 then f (↑g 0 + n') else List.tail (f (↑g (↑g 0 + n' - ↑g 0))))
hn : ¬↑g 0 + n' < ↑g 0
⊢ False
case neg
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n : ℕ
mn : m < n
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
hn : ¬n < ↑g 0
⊢ False
obtain ⟨n', rfl⟩ := exists_add_of_le (not_lt.1 hn)
case neg.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hmn : List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
hn : ¬↑g 0 + n' < ↑g 0
⊢ False
case neg.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hmn :
  List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
    (if ↑g 0 + n' < ↑g 0 then f (↑g 0 + n') else List.tail (f (↑g (↑g 0 + n' - ↑g 0))))
hn : ¬↑g 0 + n' < ↑g 0
⊢ False
rw [if_neg hn, add_comm (g 0) n', add_tsub_cancel_right] at hmn
case neg.intro.inl
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hn : ¬↑g 0 + n' < ↑g 0
hm : m < ↑g 0
hmn : List.SublistForall₂ r (f m) (List.tail (f (↑g n')))
⊢ False

case neg.intro.inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hn : ¬↑g 0 + n' < ↑g 0
hm : ¬m < ↑g 0
hmn : List.SublistForall₂ r (List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
⊢ False
case neg.intro
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hmn : List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
hn : ¬↑g 0 + n' < ↑g 0
⊢ False
split_ifs at hmn with hm
case neg.intro.inl
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hn : ¬↑g 0 + n' < ↑g 0
hm : m < ↑g 0
hmn : List.SublistForall₂ r (f m) (List.tail (f (↑g n')))
⊢ List.SublistForall₂ r (f m) (f (↑g n'))
case neg.intro.inl
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hn : ¬↑g 0 + n' < ↑g 0
hm : m < ↑g 0
hmn : List.SublistForall₂ r (f m) (List.tail (f (↑g n')))
⊢ False
apply hf1.2 m (g n') (lt_of_lt_of_le hm (g.monotone n'.zero_le))
no goals
case neg.intro.inl
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hn : ¬↑g 0 + n' < ↑g 0
hm : m < ↑g 0
hmn : List.SublistForall₂ r (f m) (List.tail (f (↑g n')))
⊢ List.SublistForall₂ r (f m) (f (↑g n'))
exact _root_.trans hmn (List.tail_sublistForall₂_self _)
case neg.intro.inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m - ↑g 0 < n'
hn : ¬↑g 0 + n' < ↑g 0
hm : ¬m < ↑g 0
hmn : List.SublistForall₂ r (List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
⊢ False
case neg.intro.inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m < ↑g 0 + n'
hn : ¬↑g 0 + n' < ↑g 0
hm : ¬m < ↑g 0
hmn : List.SublistForall₂ r (List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
⊢ False
rw [← tsub_lt_iff_left (le_of_not_lt hm)] at mn
case neg.intro.inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m - ↑g 0 < n'
hn : ¬↑g 0 + n' < ↑g 0
hm : ¬m < ↑g 0
hmn : List.SublistForall₂ r (List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
⊢ List.SublistForall₂ r (f (↑g (m - ↑g 0))) (f (↑g n'))
case neg.intro.inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m - ↑g 0 < n'
hn : ¬↑g 0 + n' < ↑g 0
hm : ¬m < ↑g 0
hmn : List.SublistForall₂ r (List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
⊢ False
apply hf1.2 _ _ (g.lt_iff_lt.2 mn)
case neg.intro.inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m - ↑g 0 < n'
hn : ¬↑g 0 + n' < ↑g 0
hm : ¬m < ↑g 0
hmn : List.SublistForall₂ r (List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
⊢ List.SublistForall₂ r (List.head! (f (↑g (m - ↑g 0))) :: List.tail (f (↑g (m - ↑g 0))))
    (List.head! (f (↑g n')) :: List.tail (f (↑g n')))
case neg.intro.inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m - ↑g 0 < n'
hn : ¬↑g 0 + n' < ↑g 0
hm : ¬m < ↑g 0
hmn : List.SublistForall₂ r (List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
⊢ List.SublistForall₂ r (f (↑g (m - ↑g 0))) (f (↑g n'))
rw [← List.cons_head!_tail (hnil (g (m - g 0))), ← List.cons_head!_tail (hnil (g n'))]
no goals
case neg.intro.inr
ι : Type ?u.147263
α : Type u_1
β : Type ?u.147269
r✝ r : α → α → Prop
inst✝¹ : IsRefl α r
inst✝ : IsTrans α r
s : Set α
h : PartiallyWellOrderedOn s r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ (x : α), x ∈ l → x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ (x : α), x ∈ l → x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
this : ∀ (n : ℕ), List.headI (f n) ∈ s
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (List.headI (f (↑g m))) (List.headI (f (↑g n)))
hf' :
  (∀ (n : ℕ), (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0)))) ∈ {l | ∀ (x : α), x ∈ l → x ∈ s}) →
    ∃ m n,
      m < n ∧
        List.SublistForall₂ r (if m < ↑g 0 then f m else List.tail (f (↑g (m - ↑g 0))))
          (if n < ↑g 0 then f n else List.tail (f (↑g (n - ↑g 0))))
m n' : ℕ
mn : m - ↑g 0 < n'
hn : ¬↑g 0 + n' < ↑g 0
hm : ¬m < ↑g 0
hmn : List.SublistForall₂ r (List.tail (f (↑g (m - ↑g 0)))) (List.tail (f (↑g n')))
⊢ List.SublistForall₂ r (List.head! (f (↑g (m - ↑g 0))) :: List.tail (f (↑g (m - ↑g 0))))
    (List.head! (f (↑g n')) :: List.tail (f (↑g n')))
exact List.SublistForall₂.cons (hg _ _ (le_of_lt mn)) hmn