awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : ι → Type u_6
inst : Finite ι
r : (i : ι) → α i → α i → Prop
inst_1 : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this_1 : Fintype ι
this_2 : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
this :
  ∀ (t : Finset ι) (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
      ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
⊢ (pi (α := α) univ s).PartiallyWellOrderedOn fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
have rw : ∀ (f : ℕ → (i : ι) → α i),
  (∀ (n : ℕ), f n ∈ pi (α := α) univ s) →
    ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → ∀ (i : ι), r i (f ((g : (a : ℕ) → ℕ) m) i) (f ((g : (a : ℕ) → ℕ) n) i)
Tactic: rw [partiallyWellOrderedOn_iff_exists_monotone_subseq]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_6
inst : Finite ι
r : (i : ι) → α i → α i → Prop
inst_1 : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this_1 : Fintype ι
this_2 : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
this :
  ∀ (t : Finset ι) (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
      ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ), f n ∈ pi (α := α) univ s
⊢ ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → ∀ (i : ι), r i (f ((g : (a : ℕ) → ℕ) m) i) (f ((g : (a : ℕ) → ℕ) n) i)
have hf₁ : ∀ (n : ℕ) (i : ι), f n i ∈ s i
Tactic: simp only [mem_pi, mem_univ, forall_const] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : ι → Type u_6
inst : Finite ι
r : (i : ι) → α i → α i → Prop
inst_1 : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
⊢ (pi (α := α) univ s).PartiallyWellOrderedOn fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
have suffices : ∀ (t : Finset ι) (f : ℕ → (i : ι) → α i),
  (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
    ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
Tactic: suffices ∀ (t : Finset ι), ∀ (f : ℕ → ∀ i, α i), (∀ n i, f n i ∈ s i) →
    ∃ g : ℕ ↪o ℕ, ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i, i ∈ t → r i ((f ∘ g) a i) ((f ∘ g) b i) by
    rw [partiallyWellOrderedOn_iff_exists_monotone_subseq]
    intro f hf
    simp only [mem_pi, mem_univ, forall_const] at hf
    simpa only [Finset.mem_univ, true_imp_iff] using this Finset.univ f hf
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : ι → Type u_6
inst : Finite ι
r : (i : ι) → α i → α i → Prop
inst_1 : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
⊢ ∀ (t : Finset ι) (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
      ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
have refine_1 : ∀ (f : ℕ → (i : ι) → α i),
  (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
    ∃ (g : ℕ ↪o ℕ),
      ∀ ⦃a b : ℕ⦄,
        a ≤ b →
          ∀ (i : ι),
            Membership.mem (γ := Finset ι) ∅ i → r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
Tactic: refine Finset.cons_induction ?_ ?_
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : ι → Type u_6
inst : Finite ι
r : (i : ι) → α i → α i → Prop
inst_1 : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
refine_1 :
  ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
      ∃ (g : ℕ ↪o ℕ),
        ∀ ⦃a b : ℕ⦄,
          a ≤ b →
            ∀ (i : ι),
              Membership.mem (γ := Finset ι) ∅ i → r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
⊢ ∀ (t : Finset ι) (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
      ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
have refine_2 : ∀ (a : ι) (s_1 : Finset ι) (h : a ∉ s_1),
  (∀ (f : ℕ → (i : ι) → α i),
      (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
        ∃ (g : ℕ ↪o ℕ),
          ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ s_1, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)) →
    ∀ (f : ℕ → (i : ι) → α i),
      (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
        ∃ (g : ℕ ↪o ℕ),
          ∀ ⦃a_3 b : ℕ⦄,
            a_3 ≤ b → ∀ i ∈ Finset.cons a s_1 h, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a_3 i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
Tactic: refine Finset.cons_induction ?_ ?_
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : ι → Type u_6
inst : Finite ι
r : (i : ι) → α i → α i → Prop
inst_1 : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ) (i : ι), f n i ∈ s i
⊢ ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b →
        ∀ (i : ι),
          Membership.mem (γ := Finset ι) ∅ i → r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
have refine_1 : ∀ ⦃a b : ℕ⦄,
  a ≤ b →
    ∀ (i : ι),
      Membership.mem (γ := Finset ι) ∅ i →
        r i ((f ∘ (⇑(RelEmbedding.refl fun (x1 x2 : ℕ) ↦ x1 ≤ x2) : (a : ℕ) → ℕ)) a i)
          ((f ∘ (⇑(RelEmbedding.refl fun (x1 x2 : ℕ) ↦ x1 ≤ x2) : (a : ℕ) → ℕ)) b i)
Tactic: exists RelEmbedding.refl (· ≤ ·)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : ι → Type u_6
inst : Finite ι
r : (i : ι) → α i → α i → Prop
inst_1 : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
t : Finset ι
hi : i ∉ t
ih :
  ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
      ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ) (i : ι), f n i ∈ s i
⊢ ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i_1) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i_1)
have refine_2 : ∀ (g : ℕ ↪o ℕ) (hg : ∀ (m n : ℕ), m ≤ n → r i (f ((g : (a : ℕ) → ℕ) m) i) (f ((g : (a : ℕ) → ℕ) n) i)),
  ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i_1) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i_1)
Tactic: obtain ⟨g, hg⟩ := (hs i).exists_monotone_subseq (hf · i)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : ι → Type u_6
inst : Finite ι
r : (i : ι) → α i → α i → Prop
inst_1 : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
t : Finset ι
hi : i ∉ t
ih :
  ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
      ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ) (i : ι), f n i ∈ s i
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r i (f ((g : (a : ℕ) → ℕ) m) i) (f ((g : (a : ℕ) → ℕ) n) i)
⊢ ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i_1) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i_1)
have refine_2 : ∀ (g' : ℕ ↪o ℕ)
  (hg' :
    ∀ ⦃a b : ℕ⦄,
      a ≤ b →
        ∀ i ∈ t,
          r i (Function.comp (β := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ)) (⇑g' : (a : ℕ) → ℕ) a i)
            (Function.comp (β := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ)) (⇑g' : (a : ℕ) → ℕ) b i)),
  ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i_1) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i_1)
Tactic: obtain ⟨g', hg'⟩ := ih (f ∘ g) (hf <| g ·)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : ι → Type u_6
inst : Finite ι
r : (i : ι) → α i → α i → Prop
inst_1 : ∀ (i : ι), IsPreorder (α i) (r i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).PartiallyWellOrderedOn (r i)
this_1 : Fintype ι
this : IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)
i : ι
t : Finset ι
hi : i ∉ t
ih :
  ∀ (f : ℕ → (i : ι) → α i),
    (∀ (n : ℕ) (i : ι), f n i ∈ s i) →
      ∃ (g : ℕ ↪o ℕ), ∀ ⦃a b : ℕ⦄, a ≤ b → ∀ i ∈ t, r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)
f : ℕ → (i : ι) → α i
hf : ∀ (n : ℕ) (i : ι), f n i ∈ s i
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r i (f ((g : (a : ℕ) → ℕ) m) i) (f ((g : (a : ℕ) → ℕ) n) i)
g' : ℕ ↪o ℕ
hg' :
  ∀ ⦃a b : ℕ⦄,
    a ≤ b →
      ∀ i ∈ t,
        r i (Function.comp (β := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ)) (⇑g' : (a : ℕ) → ℕ) a i)
          (Function.comp (β := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ)) (⇑g' : (a : ℕ) → ℕ) b i)
⊢ ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b → ∀ i_1 ∈ Finset.cons i t hi, r i_1 ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i_1) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i_1)
have refine_2 : ∀ (a b : ℕ) (hab : a ≤ b),
  r i
      ((f ∘
          (⇑(RelEmbedding.trans (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (t :=
                fun (x1 x2 : ℕ) ↦ x1 ≤ x2) g' g) :
            (a : ℕ) → ℕ))
        a i)
      ((f ∘
          (⇑(RelEmbedding.trans (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (t :=
                fun (x1 x2 : ℕ) ↦ x1 ≤ x2) g' g) :
            (a : ℕ) → ℕ))
        b i) ∧
    ∀ x ∈ t,
      r x
        ((f ∘
            (⇑(RelEmbedding.trans (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (t :=
                  fun (x1 x2 : ℕ) ↦ x1 ≤ x2) g' g) :
              (a : ℕ) → ℕ))
          a x)
        ((f ∘
            (⇑(RelEmbedding.trans (r := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (s := fun (x1 x2 : ℕ) ↦ x1 ≤ x2) (t :=
                  fun (x1 x2 : ℕ) ↦ x1 ≤ x2) g' g) :
              (a : ℕ) → ℕ))
          b x)
Tactic: refine ⟨g'.trans g, fun a b hab => (Finset.forall_mem_cons _ _).2 ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
hs : s.IsPWO
ha : a ∈ s
t : Set (↑s : Type u_2) := {x : (↑s : Type u_2) | (↑x : α) ≤ a}
h : t.Nonempty := ⋯
⊢ ∃ b ≤ a, Minimal (fun (x : α) ↦ x ∈ s) b
have refine : ∀ (y : α) (hy : (fun (x : α) ↦ x ∈ s) y)
  (hle :
    y ≤
      (↑(sorry.min (r := fun (a b : { x : α // x ∈ s }) ↦
            Subrel (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α) ↦ x ∈ s) a b ∧
              ¬Subrel (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α) ↦ x ∈ s) b a)
            t h) :
        α)),
  (↑(sorry.min (r := fun (a b : { x : α // x ∈ s }) ↦
          Subrel (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α) ↦ x ∈ s) a b ∧
            ¬Subrel (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α) ↦ x ∈ s) b a)
          t h) :
      α) ≤
    y
Tactic: refine ⟨hs.wellFounded.min t h, hs.wellFounded.min_mem t h,
    (hs.wellFounded.min t h).2, fun y hy hle => ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
hs : s.IsPWO
ha : a ∈ s
t : Set (↑s : Type u_2) := {x : (↑s : Type u_2) | (↑x : α) ≤ a}
h : t.Nonempty := ⋯
y : α
hy : (fun (x : α) ↦ x ∈ s) y
hle :
  y ≤
    (↑(⋯.min (r := fun (a b : { x : α // x ∈ s }) ↦
          Subrel (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α) ↦ x ∈ s) a b ∧
            ¬Subrel (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α) ↦ x ∈ s) b a)
          t h) :
      α)
⊢ (↑(⋯.min (r := fun (a b : { x : α // x ∈ s }) ↦
          Subrel (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α) ↦ x ∈ s) a b ∧
            ¬Subrel (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α) ↦ x ∈ s) b a)
          t h) :
      α) ≤
    y
have by_contra : ∀
  (hnle :
    ¬(↑(sorry.min (r := fun (a b : { x : α // x ∈ s }) ↦
              Subrel (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α) ↦ x ∈ s) a b ∧
                ¬Subrel (fun (x1 x2 : α) ↦ x1 ≤ x2) (fun (x : α) ↦ x ∈ s) b a)
              t h) :
          α) ≤
        y),
  False
Tactic: by_contra hnle
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
inst : Preorder α
s : Set α
h : s.IsPWO
hs : s.Nonempty
⊢ ∃ (a : α), Minimal (fun (x : α) ↦ x ∈ s) a
have rcases : ∀ (a : α) (ha : a ∈ s), ∃ (a : α), Minimal (fun (x : α) ↦ x ∈ s) a
Tactic: rcases hs with ⟨a, ha⟩
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
inst : Preorder α
s : Set α
h : s.IsPWO
a : α
ha : a ∈ s
⊢ ∃ (a : α), Minimal (fun (x : α) ↦ x ∈ s) a
have obtain : ∀ b ≤ a, ∀ (hb : Minimal (fun (x : α) ↦ x ∈ s) b), ∃ (a : α), Minimal (fun (x : α) ↦ x ∈ s) a
Tactic: obtain ⟨b, _, hb⟩ := h.exists_le_minimal ha
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
f : ι → α
s : Set ι
h : (f '' s).IsPWO
hs : s.Nonempty
⊢ ∃ (i : ι), MinimalFor (fun (x : ι) ↦ x ∈ s) f i
have obtain : ∀ (w : α) (h : Minimal (fun (x : α) ↦ x ∈ f '' s) w), ∃ (i : ι), MinimalFor (fun (x : ι) ↦ x ∈ s) f i
Tactic: obtain ⟨_, h⟩ := h.exists_minimal (hs.image _)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
f : ι → α
s : Set ι
h_1 : (f '' s).IsPWO
hs : s.Nonempty
w : α
h : Minimal (fun (x : α) ↦ x ∈ f '' s) w
⊢ ∃ (i : ι), MinimalFor (fun (x : ι) ↦ x ∈ s) f i
have obtain : ∀ (a : ι) (ha : a ∈ s) (h : Minimal (fun (x : α) ↦ x ∈ f '' s) (f a)), ∃ (i : ι), MinimalFor (fun (x : ι) ↦ x ∈ s) f i
Tactic: obtain ⟨a, ha, rfl⟩ := h.1
Cleared hypotheses: w, h
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
⊢ s.IsPWO ↔ s.IsWF
have change : (WellQuasiOrdered fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 ≤ x2) ↔ WellFounded fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 < x2
Tactic: change WellQuasiOrdered (· ≤ ·) ↔ WellFounded (· < ·)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
⊢ (WellQuasiOrdered fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 ≤ x2) ↔ WellFounded fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 < x2
have rw : WellQuasiOrderedLE.{u_2} { x : α // x ∈ s } ↔ WellFounded fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 < x2
Tactic: rw [← wellQuasiOrderedLE_def, ← isWellFounded_iff, wellQuasiOrderedLE_iff_wellFoundedLT]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
rw : WellQuasiOrderedLE.{u_2} { x : α // x ∈ s } ↔ WellFounded fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 < x2
⊢ (WellQuasiOrdered fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 ≤ x2) ↔ WellFounded fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 < x2
have rw₁ : WellQuasiOrderedLE.{u_2} { x : α // x ∈ s } ↔
  IsWellFounded.{u_2} { x : α // x ∈ s } fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 < x2
Tactic: rw [← wellQuasiOrderedLE_def, ← isWellFounded_iff, wellQuasiOrderedLE_iff_wellFoundedLT]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
rw : WellQuasiOrderedLE.{u_2} { x : α // x ∈ s } ↔ WellFounded fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 < x2
rw₁ :
  WellQuasiOrderedLE.{u_2} { x : α // x ∈ s } ↔
    IsWellFounded.{u_2} { x : α // x ∈ s } fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 < x2
⊢ (WellQuasiOrdered fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 ≤ x2) ↔ WellFounded fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 < x2
have rw₂ : WellFoundedLT.{u_2} { x : α // x ∈ s } ↔
  IsWellFounded.{u_2} { x : α // x ∈ s } fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 < x2
Tactic: rw [← wellQuasiOrderedLE_def, ← isWellFounded_iff, wellQuasiOrderedLE_iff_wellFoundedLT]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
hs : s.IsWF
ha : a ∈ s
hlt : ∀ b ∈ s, b ≠ a → a < b
⊢ hs.min (s := s) ⋯ = a
have by_contra : ∀ (h : ¬hs.min (s := s) sorry = a), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ ⋯.min (s := s ∪ t) ⋯ = Min.min (hs.min (s := s) hsn) (ht.min (s := t) htn)
have refine : Min.min (hs.min (s := s) hsn) (ht.min (s := t) htn) ≤ sorry.min (s := s ∪ t) sorry
Tactic: refine le_antisymm (le_min (IsWF.min_le_min_of_subset subset_union_left)
    (IsWF.min_le_min_of_subset subset_union_right)) ?_
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
inst : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ Min.min (hs.min (s := s) hsn) (ht.min (s := t) htn) ≤ ⋯.min (s := s ∪ t) ⋯
have rw : hs.min (s := s) hsn ≤ sorry.min (s := s ∪ t) sorry ∨ ht.min (s := t) htn ≤ sorry.min (s := s ∪ t) sorry
Tactic: rw [min_le_iff]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
s : Set α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ BddBelow s → s.WellFoundedOn fun (x1 x2 : α) ↦ x1 < x2
have rw : BddBelow s →
  ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2),
    ¬∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
Tactic: rw [wellFoundedOn_iff_no_descending_seq]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
s : Set α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
a : α
ha : a ∈ lowerBounds s
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2
hf : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
⊢ False
have refine : Set.Finite (α := α) (range (ι := ℕ) (⇑f : (a : ℕ) → α))
Tactic: refine infinite_range_of_injective f.injective ?_
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
⊢ BddAbove (f ⁻¹' s)
have contrapose! : ∀ (hf : ¬BddAbove (f ⁻¹' s)), ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
Tactic: contrapose! hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ¬BddAbove (f ⁻¹' s)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
have hf₁ : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
Tactic: rw [not_bddAbove_iff] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
have obtain : ∀ (φ : ℕ → ℕ) (hφm : StrictMono φ) (hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s), ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
Tactic: obtain ⟨φ, hφm, hφs⟩ := Nat.exists_strictMono_subsequence
    fun n ↦ (hf n).casesOn fun m h ↦ h.casesOn fun hs hmn ↦ Exists.intro m ⟨hmn, hs⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
φ : ℕ → ℕ
hφm : StrictMono φ
hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
have rw : ∀ (hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)) {f : ℕ → α}
  (hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y) (φ : ℕ → ℕ) (hφm : StrictMono φ) (hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s),
  ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
Tactic: rw [partiallyWellOrderedOn_iff_exists_lt] at hs
Cleared hypotheses: hs, f, hf, φ, hφm, hφs
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
φ : ℕ → ℕ
hφm : StrictMono φ
hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
have obtain : ∀ (m n : ℕ) (hmn : m < n) (hr : r (f (φ m)) (f (φ n))), ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
Tactic: obtain ⟨m, n, hmn, hr⟩ := hs (fun n ↦ f (φ n)) hφs
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
φ : ℕ → ℕ
hφm : StrictMono φ
hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s
m n : ℕ
hmn : m < n
hr : r (f (φ m)) (f (φ n))
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
have h : φ m < φ n ∧ r (f (φ m)) (f (φ n))
Tactic: use (φ m), (φ n)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
⊢ ∃ (k : ℕ), ∀ (m : ℕ), k < m → f m ∉ s
have this : BddAbove (f ⁻¹' s)
Tactic: have := hs.bddAbove_preimage hf
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
this : BddAbove (f ⁻¹' s)
⊢ ∃ (k : ℕ), ∀ (m : ℕ), k < m → f m ∉ s
have contrapose! : ∀ (this : ∀ (k : ℕ), ∃ (m : ℕ), k < m ∧ f m ∈ s), ¬BddAbove (f ⁻¹' s)
Tactic: contrapose! this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (goal)
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
⊢ s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f
have rw : (∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)) ↔ ∀ (f : ℕ → α), ¬IsBadSeq r s f
Tactic: rw [partiallyWellOrderedOn_iff_exists_lt]
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r_1 r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
⊢ { g : ℕ → α // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
have h : ∃ (k : ℕ) (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
Tactic: have h : ∃ (k : ℕ) (g : ℕ → α), (∀ m, m < n → f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k :=
      ⟨_, f, fun _ _ => rfl, hf, rfl⟩
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r_1 r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ (k : ℕ) (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
⊢ { g : ℕ → α // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
have h1 : ∀ m < n,
  f m =
    Classical.choose (p := fun (x : ℕ → α) ↦
      (∀ m < n, f m = x m) ∧
        IsBadSeq r s x ∧
          rk (x n) =
            Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
      sorry m
Tactic: obtain ⟨h1, h2, h3⟩ := Classical.choose_spec (Nat.find_spec h)
-- Lean 4 proof step from Mathlib.Order.WellFoundedSet (hypothesis)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
π : ι → Type u_5
r_1 r : α → α → Prop
rk : α → ℕ
s : Set α
n : ℕ
f : ℕ → α
hf : IsBadSeq r s f
h : ∃ (k : ℕ) (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = k
h1 :
  ∀ m < n,
    f m =
      Classical.choose (p := fun (x : ℕ → α) ↦
        (∀ m < n, f m = x m) ∧
          IsBadSeq r s x ∧
            rk (x n) =
              Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
        ⋯ m
⊢ { g : ℕ → α // (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ IsMinBadSeq r rk s n g }
have h2 : IsBadSeq r s
  (Classical.choose (p := fun (x : ℕ → α) ↦
    (∀ m < n, f m = x m) ∧
      IsBadSeq r s x ∧
        rk (x n) =
          Nat.find (p := fun (n_1 : ℕ) ↦ ∃ (g : ℕ → α), (∀ m < n, f m = g m) ∧ IsBadSeq r s g ∧ rk (g n) = n_1) h)
    sorry)
Tactic: obtain ⟨h1, h2, h3⟩ := Classical.choose_spec (Nat.find_spec h)