awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellFoundedSet
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)

Tactic:
Finset.cons_induction ?_ ?_

Premises used: Finset.cons_induction
-- Module: Mathlib.Order.WellFoundedSet
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)
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)
⊢ ∀ (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:
refine Finset.cons_induction ?_ ?_
-- Module: Mathlib.Order.WellFoundedSet
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
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)
⊢ ∃ (g : ℕ ↪o ℕ),
    ∀ ⦃a b : ℕ⦄,
      a ≤ b →
        ∀ (i : ι),
          Membership.mem (γ := Finset ι) ∅ i → r i ((f ∘ (⇑g : (a : ℕ) → ℕ)) a i) ((f ∘ (⇑g : (a : ℕ) → ℕ)) b i)

Tactic:
exists RelEmbedding.refl (· ≤ ·)

Premises used: RelEmbedding.refl, LE.le
-- Module: Mathlib.Order.WellFoundedSet
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
⊢ ∀ ⦃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:
simp only [IsEmpty.forall_iff, imp_true_iff, Finset.notMem_empty]

Premises used: imp_true_iff, Finset.notMem_empty, IsEmpty.forall_iff
-- Module: Mathlib.Order.WellFoundedSet
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
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)
⊢ ∃ (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)

Premises used: Set.PartiallyWellOrderedOn.exists_monotone_subseq
-- Module: Mathlib.Order.WellFoundedSet
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)
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)
⊢ ∃ (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 ·)

Premises used: Function.comp, DFunLike.coe
-- Module: Mathlib.Order.WellFoundedSet
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)

Tactic:
⟨g'.trans g, fun a b hab => (Finset.forall_mem_cons _ _).2 ?_⟩

Premises used: Iff.mpr, Function.comp, Finset.forall_mem_cons, Exists.intro, RelEmbedding.trans, DFunLike.coe
-- Module: Mathlib.Order.WellFoundedSet
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)
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)
⊢ ∃ (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:
refine ⟨g'.trans g, fun a b hab => (Finset.forall_mem_cons _ _).2 ?_⟩
-- Module: Mathlib.Order.WellFoundedSet
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)
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:
⟨hg _ _ (OrderHomClass.mono g' hab), hg' hab⟩

Premises used: OrderHomClass.mono, And.intro
-- Module: Mathlib.Order.WellFoundedSet
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)
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:
exact ⟨hg _ _ (OrderHomClass.mono g' hab), hg' hab⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : IsPreorder α r
h : s.PartiallyWellOrderedOn r
⊢ s.WellFoundedOn fun (a b : α) ↦ r a b ∧ ¬r b a

Tactic:
h.wellFounded

Premises used: WellQuasiOrdered.wellFounded, Subrel, Order.Preimage, Set.WellFoundedOn
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s t : Set α
ht : t.IsPWO
⊢ s ⊆ t → s.IsPWO

Tactic:
ht.mono

Premises used: Set.IsPWO, Set.PartiallyWellOrderedOn.mono
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
h : s.IsPWO
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))

Tactic:
h.exists_monotone_subseq hf

Premises used: Set.PartiallyWellOrderedOn.exists_monotone_subseq, Monotone
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
⊢ IsPWO.{u_2} (α := α) univ ↔ WellQuasiOrderedLE α

Tactic:
partiallyWellOrderedOn_univ_iff.trans (wellQuasiOrderedLE_def _).symm

Premises used: Set.IsPWO, wellQuasiOrderedLE_def, Iff.trans, Set.partiallyWellOrderedOn_univ_iff, Iff.symm
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
h : WellQuasiOrderedLE α
s : Set α
⊢ s.IsPWO

Tactic:
partiallyWellOrderedOn_of_wellQuasiOrdered h.wqo s

Premises used: Set.IsPWO, Set.partiallyWellOrderedOn_of_wellQuasiOrdered, WellQuasiOrderedLE.wqo
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
⊢ s.IsPWO ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (g : ℕ ↪o ℕ), Monotone (α := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))

Tactic:
partiallyWellOrderedOn_iff_exists_monotone_subseq

Premises used: Set.IsPWO, Monotone, Set.partiallyWellOrderedOn_iff_exists_monotone_subseq
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
h : s.IsPWO
⊢ s.IsWF

Tactic:
simpa only [← lt_iff_le_not_ge] using h.wellFoundedOn

Premises used: lt_iff_le_not_ge, Set.PartiallyWellOrderedOn.wellFoundedOn
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set α
t : Set β
hs : s.IsPWO
ht : t.IsPWO
⊢ (s ×ˢ t).IsPWO

Tactic:
hs.prod ht

Premises used: Set.IsPWO, Set.PartiallyWellOrderedOn.prod
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : ι → Type u_6
inst : Finite ι
inst_1 : (i : ι) → Preorder (α i)
s : (i : ι) → Set (α i)
hs : ∀ (i : ι), (s i).IsPWO
⊢ (Set.pi (α := α) univ s).IsPWO

Tactic:
PartiallyWellOrderedOn.pi hs

Premises used: Set.IsPWO, Set.PartiallyWellOrderedOn.pi
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set α
hs : s.IsPWO
f : α → β
hf : MonotoneOn f s
⊢ (f '' s).IsPWO

Tactic:
hs.image_of_monotone_on hf

Premises used: Set.IsPWO, Set.PartiallyWellOrderedOn.image_of_monotone_on
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
s : Set α
hs : s.IsPWO
f : α → β
hf : Monotone f
⊢ (f '' s).IsPWO

Tactic:
hs.image_of_monotone_on (hf.monotoneOn _)

Premises used: Set.IsPWO, Set.PartiallyWellOrderedOn.image_of_monotone_on, Monotone.monotoneOn
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s t : Set α
hs : s.IsPWO
ht : t.IsPWO
⊢ (s ∪ t).IsPWO

Tactic:
hs.union ht

Premises used: Set.IsPWO, Set.PartiallyWellOrderedOn.union
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s t : Set α
⊢ (s ∪ t).IsPWO ↔ s.IsPWO ∧ t.IsPWO

Tactic:
partiallyWellOrderedOn_union

Premises used: Set.IsPWO, Set.partiallyWellOrderedOn_union
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
hs : s.Finite
⊢ s.IsPWO

Tactic:
hs.partiallyWellOrderedOn

Premises used: Set.IsPWO, Set.Finite.partiallyWellOrderedOn
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
inst_1 : Finite α
⊢ s.IsPWO

Tactic:
s.toFinite.isPWO

Premises used: Set.Finite.isPWO, Set.toFinite
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
a : α
⊢ IsPWO (α := α) {a}

Tactic:
(finite_singleton a).isPWO

Premises used: Set.Finite.isPWO, Set.finite_singleton
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
⊢ IsPWO.{u_2} (α := α) ∅

Tactic:
finite_empty.isPWO

Premises used: Set.finite_empty, Set.Finite.isPWO
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
hs : s.Subsingleton
⊢ s.IsPWO

Tactic:
hs.finite.isPWO

Premises used: Set.Finite.isPWO, Set.Subsingleton.finite
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
⊢ (insert a s).IsPWO ↔ s.IsPWO

Tactic:
simp only [← singleton_union, isPWO_union, isPWO_singleton, true_and]

Premises used: Set.singleton_union, Set.isPWO_union, Set.isPWO_singleton, true_and
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
h : s.IsPWO
a : α
⊢ (insert a s).IsPWO

Tactic:
isPWO_insert.2 h

Premises used: Iff.mpr, Set.isPWO_insert
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
hs : s.Finite
⊢ s.IsWF

Tactic:
hs.isPWO.isWF

Premises used: Set.Finite.isPWO, Set.IsPWO.isWF
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
a : α
⊢ IsWF (α := α) {a}

Tactic:
(finite_singleton a).isWF

Premises used: Set.Finite.isWF, Set.finite_singleton
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
hs : s.Subsingleton
⊢ s.IsWF

Tactic:
hs.isPWO.isWF

Premises used: Set.Subsingleton.isPWO, Set.IsPWO.isWF
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
⊢ (insert a s).IsWF ↔ s.IsWF

Tactic:
simp only [← singleton_union, isWF_union, isWF_singleton, true_and]

Premises used: Set.singleton_union, Set.isWF_union, Set.isWF_singleton, true_and
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
h : s.IsWF
a : α
⊢ (insert a s).IsWF

Tactic:
isWF_insert.2 h

Premises used: Iff.mpr, Set.isWF_insert
-- Module: Mathlib.Order.WellFoundedSet
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

Tactic:
⟨hs.wellFounded.min t h, hs.wellFounded.min_mem t h,
    (hs.wellFounded.min t h).2, fun y hy hle => ?_⟩

Premises used: WellQuasiOrdered.wellFounded, WellFounded.min_mem, And.intro, WellFounded.min, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
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 := ⋯
refine :
  ∀ (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
⊢ ∃ b ≤ a, Minimal (fun (x : α) ↦ x ∈ s) b

Tactic:
refine ⟨hs.wellFounded.min t h, hs.wellFounded.min_mem t h,
    (hs.wellFounded.min t h).2, fun y hy hle => ?_⟩
-- Module: Mathlib.Order.WellFoundedSet
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) :
      α)
by_contra :
  ∀
    (hnle :
      ¬(↑(⋯.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
⊢ (↑(⋯.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:
by_contra hnle
-- Module: Mathlib.Order.WellFoundedSet
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) :
      α)
hnle :
  ¬(↑(⋯.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:
hs.wellFounded.not_lt_min t (x := ⟨y, hy⟩) (hle.trans (hs.wellFounded.min_mem t h))
    ⟨hle, hnle⟩

Premises used: WellQuasiOrdered.wellFounded, WellFounded.min_mem, And.intro, WellFounded.not_lt_min, LE.le.trans
-- Module: Mathlib.Order.WellFoundedSet
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) :
      α)
hnle :
  ¬(↑(⋯.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:
exact hs.wellFounded.not_lt_min t (x := ⟨y, hy⟩) (hle.trans (hs.wellFounded.min_mem t h))
    ⟨hle, hnle⟩

Premises used: WellQuasiOrdered.wellFounded, WellFounded.min_mem, And.intro, WellFounded.not_lt_min, LE.le.trans
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
h : s.IsPWO
hs : s.Nonempty
rcases : ∀ (a : α) (ha : a ∈ s), ∃ (a : α), Minimal (fun (x : α) ↦ x ∈ s) a
⊢ ∃ (a : α), Minimal (fun (x : α) ↦ x ∈ s) a

Tactic:
rcases hs with ⟨a, ha⟩