awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
inst : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h_1 : Nonempty α
inhabited_h : Inhabited α
⊢ PartiallyWellOrderedOn {l : List α | ∀ x ∈ l, x ∈ s} (List.SublistForall₂ r)
have 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
Tactic: rw [iff_not_exists_isMinBadSeq List.length]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
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
⊢ False
have hnil : ∀ (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)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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 ≠ []
⊢ False
have inr : ∀ (g : ℕ ↪o ℕ) (hg : ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)).head! (f ((g : (a : ℕ) → ℕ) n)).head!), False
Tactic: obtain ⟨g, hg⟩ := h.exists_monotone_subseq fun n => hf1.1 n _ (List.head!_mem_self (hnil n))
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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!
⊢ False
have 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
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) ?_
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ False
have 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
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) ?_
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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!
⊢ 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
have inr : (f ((g : (a : ℕ) → ℕ) 0)).tail.length < (f ((g : (a : ℕ) → ℕ) 0)).length
Tactic: simp only [if_neg (lt_irrefl (g 0)), Nat.sub_self]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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)).tail.length < (f ((g : (a : ℕ) → ℕ) 0)).length
have inr : (f ((g : (a : ℕ) → ℕ) 0)).length.pred < (f ((g : (a : ℕ) → ℕ) 0)).length
Tactic: rw [List.length_tail, ← Nat.pred_eq_sub_one]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
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
⊢ False
have 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))
Tactic: rw [IsBadSeq] at hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
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))
⊢ False
have 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)
Tactic: push Not at hf'
Cleared hypotheses: hf'
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ x ∈ s
have pos : ∀ (hn : n < (g : (a : ℕ) → ℕ) 0) (hx : x ∈ f n), x ∈ s
Tactic: split_ifs at hx with hn
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ x ∈ s
have neg : ∀ (hn : ¬n < (g : (a : ℕ) → ℕ) 0)
  (hx : x ∈ (f ((g : (a : ℕ) → ℕ) (HSub.hSub (β := ℕ) n ((g : (a : ℕ) → ℕ) 0 : ℕ)))).tail), x ∈ s
Tactic: split_ifs at hx with hn
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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)
⊢ False
have 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
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)]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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)
⊢ False
have pos : ∀ (hn : n < (g : (a : ℕ) → ℕ) 0), False
Tactic: by_cases hn : n < g 0
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ False
have neg : ∀ (hn : ¬n < (g : (a : ℕ) → ℕ) 0), False
Tactic: by_cases hn : n < g 0
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ False
have pos : List.SublistForall₂ r (f m) (f n)
Tactic: apply hf1.2 m n mn
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ List.SublistForall₂ r (f m) (f n)
have 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)
Tactic: rwa [if_pos hn, if_pos (mn.trans hn)] at hmn
Cleared hypotheses: hmn, hn
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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)
⊢ List.SublistForall₂ r (f m) (f n)
have pos₁ : ∀ (hmn : List.SublistForall₂ r (f m) (f n)) (hn : n < (g : (a : ℕ) → ℕ) 0), List.SublistForall₂ r (f m) (f n)
Tactic: rwa [if_pos hn, if_pos (mn.trans hn)] at hmn
Cleared hypotheses: hmn, hn
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
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
⊢ False
have 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
Tactic: obtain ⟨n', rfl⟩ := Nat.exists_eq_add_of_le (not_lt.1 hn)
Cleared hypotheses: n, mn, hmn, hn