awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g : (n : ℕ) → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
m n : ℕ
hlt : m < n
hmn : r (g m) (g n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)

Tactic:
⟨m, n, hlt, hf _ (hgs m) _ (hgs n) hmn⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
g : (n : ℕ) → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n
m n : ℕ
hlt : m < n
hmn : r (g m) (g n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)

Tactic:
exact ⟨m, n, hlt, hf _ (hgs m) _ (hgs n) hmn⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
by_contra! : ∀ (hi : s.Infinite), False
⊢ s.Finite

Tactic:
by_contra! hi
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
hi : s.Infinite
obtain :
  ∀ (m n : ℕ) (hmn : m < n)
    (h :
      Subrel r (fun (x : α) ↦ x ∈ s) ((Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_2)) m)
        ((Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_2)) n)),
    False
⊢ False

Tactic:
obtain ⟨m, n, hmn, h⟩ := hp (hi.natEmbedding _)

Premises used: Set.Infinite.natEmbedding, DFunLike.coe
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
hi : s.Infinite
m n : ℕ
hmn : m < n
h :
  Subrel r (fun (x : α) ↦ x ∈ s) ((Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_2)) m)
    ((Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_2)) n)
⊢ False

Tactic:
hmn.ne ((hi.natEmbedding _).injective <| Subtype.val_injective <|
    ha.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)

Premises used: Subtype.val_injective, Set.Infinite.natEmbedding, Function.Embedding.injective, IsAntichain.eq, DFunLike.coe, LT.lt.ne, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
ha : IsAntichain r s
hp : s.PartiallyWellOrderedOn r
hi : s.Infinite
m n : ℕ
hmn : m < n
h :
  Subrel r (fun (x : α) ↦ x ∈ s) ((Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_2)) m)
    ((Infinite.natEmbedding s hi : (a : ℕ) → (↑s : Type u_2)) n)
⊢ False

Tactic:
exact hmn.ne ((hi.natEmbedding _).injective <| Subtype.val_injective <|
    ha.eq (hi.natEmbedding _ m).2 (hi.natEmbedding _ n).2 h)

Premises used: Subtype.val_injective, Set.Infinite.natEmbedding, Function.Embedding.injective, IsAntichain.eq, DFunLike.coe, LT.lt.ne, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
hs : s.Finite
⊢ s.PartiallyWellOrderedOn r

Tactic:
hs.to_subtype.wellQuasiOrdered _

Premises used: Set.PartiallyWellOrderedOn, Finite.wellQuasiOrdered
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
hs : IsAntichain r s
⊢ s.PartiallyWellOrderedOn r ↔ s.Finite

Tactic:
⟨hs.finite_of_partiallyWellOrderedOn, Finite.partiallyWellOrderedOn⟩

Premises used: Set.Finite.partiallyWellOrderedOn, Iff.intro, IsAntichain.finite_of_partiallyWellOrderedOn
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : Std.Refl r
a : α
⊢ PartiallyWellOrderedOn {a} r

Tactic:
(finite_singleton a).partiallyWellOrderedOn

Premises used: Set.Finite.partiallyWellOrderedOn, Set.finite_singleton
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
hs : s.Subsingleton
⊢ s.PartiallyWellOrderedOn r

Tactic:
hs.finite.partiallyWellOrderedOn

Premises used: Set.Finite.partiallyWellOrderedOn, Set.Subsingleton.finite
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
a : α
inst : Std.Refl r
⊢ (insert a s).PartiallyWellOrderedOn r ↔ s.PartiallyWellOrderedOn r

Tactic:
simp only [← singleton_union, partiallyWellOrderedOn_union,
    partiallyWellOrderedOn_singleton, true_and]

Premises used: Set.singleton_union, Set.partiallyWellOrderedOn_singleton, Set.partiallyWellOrderedOn_union, true_and
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
h : s.PartiallyWellOrderedOn r
a : α
⊢ (insert a s).PartiallyWellOrderedOn r

Tactic:
partiallyWellOrderedOn_insert.2 h

Premises used: Iff.mpr, Set.partiallyWellOrderedOn_insert
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
⊢ s.PartiallyWellOrderedOn r ↔ ∀ t ⊆ s, IsAntichain r t → t.Finite

Tactic:
⟨fun h t ht hrt => hrt.finite_of_partiallyWellOrderedOn (h.mono ht), ?_⟩

Premises used: Iff.intro, IsAntichain.finite_of_partiallyWellOrderedOn, Set.PartiallyWellOrderedOn.mono
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
refine : (∀ t ⊆ s, IsAntichain r t → t.Finite) → s.PartiallyWellOrderedOn r
⊢ s.PartiallyWellOrderedOn r ↔ ∀ t ⊆ s, IsAntichain r t → t.Finite

Tactic:
refine ⟨fun h t ht hrt => hrt.finite_of_partiallyWellOrderedOn (h.mono ht), ?_⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
rw :
  (∀ t ⊆ s, IsAntichain r t → t.Finite) → ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
⊢ (∀ t ⊆ s, IsAntichain r t → t.Finite) → s.PartiallyWellOrderedOn r

Tactic:
rw [partiallyWellOrderedOn_iff_exists_lt]

Premises used: Set.partiallyWellOrderedOn_iff_exists_lt
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
by_contra! : ∀ (H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)), False
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

Tactic:
by_contra! H
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
⊢ False

Tactic:
infinite_range_of_injective (fun m n hmn => ?_) (hs _ (range_subset_iff.2 hf) ?_)

Premises used: Iff.mpr, Set.infinite_range_of_injective, Set.range_subset_iff
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
refine_1 : ∀ (m n : ℕ) (hmn : f m = f n), m = n
refine_2 : IsAntichain r (range f)
⊢ False

Tactic:
refine infinite_range_of_injective (fun m n hmn => ?_) (hs _ (range_subset_iff.2 hf) ?_)

Premises used: Iff.mpr, Set.infinite_range_of_injective, Set.range_subset_iff
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
refine_1 : ∀ (h : m < n), m = n
refine_1₁ : ∀ (h : m = n), m = n
refine_1₂ : ∀ (h : n < m), m = n
⊢ m = n

Tactic:
obtain h | h | h := lt_trichotomy m n

Premises used: lt_trichotomy
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ m = n

Tactic:
(H _ _ h ?_).elim

Premises used: False.elim
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
refine_1 : r (f m) (f n)
⊢ m = n

Tactic:
refine (H _ _ h ?_).elim

Premises used: False.elim
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
refine_1 : r (f n) (f n)
⊢ r (f m) (f n)

Tactic:
rw [hmn]
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ r (f n) (f n)

Tactic:
refl _

Premises used: refl
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m < n
⊢ r (f n) (f n)

Tactic:
exact refl _

Premises used: refl
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m = n
⊢ m = n

Tactic:
h
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : m = n
⊢ m = n

Tactic:
exact h
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ m = n

Tactic:
(H _ _ h ?_).elim

Premises used: False.elim
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
refine_1 : r (f n) (f m)
⊢ m = n

Tactic:
refine (H _ _ h ?_).elim

Premises used: False.elim
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
refine_1 : r (f n) (f n)
⊢ r (f n) (f m)

Tactic:
rw [hmn]
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ r (f n) (f n)

Tactic:
refl _

Premises used: refl
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m = f n
h : n < m
⊢ r (f n) (f n)

Tactic:
exact refl _

Premises used: refl
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m ≠ f n
refine_2 : ∀ (h : m < n), rᶜ (f m) (f n)
refine_2₁ : ∀ (h : n < m), rᶜ (f m) (f n)
⊢ rᶜ (f m) (f n)

Tactic:
obtain h | h := (ne_of_apply_ne _ hmn).lt_or_gt

Premises used: ne_of_apply_ne, Ne.lt_or_gt
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m ≠ f n
h : m < n
⊢ rᶜ (f m) (f n)

Tactic:
H _ _ h
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m ≠ f n
h : m < n
⊢ rᶜ (f m) (f n)

Tactic:
exact H _ _ h
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m ≠ f n
h : n < m
⊢ rᶜ (f m) (f n)

Tactic:
mt symm (H _ _ h)

Premises used: mt, symm
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : Std.Refl r
inst_1 : Std.Symm r
hs : ∀ t ⊆ s, IsAntichain r t → t.Finite
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
H : ∀ (m n : ℕ) (_ : m < n), ¬r (f m) (f n)
m n : ℕ
hmn : f m ≠ f n
h : n < m
⊢ rᶜ (f m) (f n)

Tactic:
exact mt symm (H _ _ h)

Premises used: mt, symm
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : IsPreorder α r
h : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
WellQuasiOrdered.exists_monotone_subseq h fun n ↦ ⟨_, hf n⟩

Premises used: Subrel, Subtype.mk, WellQuasiOrdered.exists_monotone_subseq, Order.Preimage
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : IsPreorder α r
mpr :
  (∀ (f : ℕ → α),
      (∀ (n : ℕ), f n ∈ s) →
        ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) →
    s.PartiallyWellOrderedOn r
⊢ s.PartiallyWellOrderedOn r ↔
    ∀ (f : ℕ → α),
      (∀ (n : ℕ), f n ∈ s) → ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
use PartiallyWellOrderedOn.exists_monotone_subseq

Premises used: Set.PartiallyWellOrderedOn.exists_monotone_subseq
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : IsPreorder α r
mpr :
  (∀ (f : ℕ → α),
      (∀ (n : ℕ), f n ∈ s) →
        ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) →
    ∀ (f : ℕ → { x : α // x ∈ s }),
      ∃ (g : ℕ ↪o ℕ),
        ∀ (m n : ℕ), m ≤ n → Subrel r (fun (x : α) ↦ x ∈ s) (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ (∀ (f : ℕ → α),
      (∀ (n : ℕ), f n ∈ s) →
        ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) →
    s.PartiallyWellOrderedOn r

Tactic:
rw [PartiallyWellOrderedOn, wellQuasiOrdered_iff_exists_monotone_subseq]

Premises used: Set.PartiallyWellOrderedOn, wellQuasiOrdered_iff_exists_monotone_subseq
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : IsPreorder α r
⊢ (∀ (f : ℕ → α),
      (∀ (n : ℕ), f n ∈ s) →
        ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) →
    ∀ (f : ℕ → { x : α // x ∈ s }),
      ∃ (g : ℕ ↪o ℕ),
        ∀ (m n : ℕ), m ≤ n → Subrel r (fun (x : α) ↦ x ∈ s) (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
fun H f ↦ H _ fun n ↦ (f n).2

Premises used: Subrel, Subtype.val, Order.Preimage, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
inst : IsPreorder α r
⊢ (∀ (f : ℕ → α),
      (∀ (n : ℕ), f n ∈ s) →
        ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) →
    ∀ (f : ℕ → { x : α // x ∈ s }),
      ∃ (g : ℕ ↪o ℕ),
        ∀ (m n : ℕ), m ≤ n → Subrel r (fun (x : α) ↦ x ∈ s) (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
exact fun H f ↦ H _ fun n ↦ (f n).2
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
rw : ∀ (f : ℕ → α × β), (∀ (n : ℕ), f n ∈ s ×ˢ t) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2
⊢ (s ×ˢ t).PartiallyWellOrderedOn fun (x y : α × β) ↦ r x.1 y.1 ∧ r' x.2 y.2

Tactic:
rw [partiallyWellOrderedOn_iff_exists_lt]

Premises used: Set.partiallyWellOrderedOn_iff_exists_lt
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
obtain :
  ∀ (g₁ : ℕ ↪o ℕ) (h₁ : ∀ (m n : ℕ), m ≤ n → r (f ((g₁ : (a : ℕ) → ℕ) m)).1 (f ((g₁ : (a : ℕ) → ℕ) n)).1),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2

Tactic:
obtain ⟨g₁, h₁⟩ := hs.exists_monotone_subseq fun n => (hf n).1

Premises used: Set.PartiallyWellOrderedOn.exists_monotone_subseq, And.left
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r (f ((g₁ : (a : ℕ) → ℕ) m)).1 (f ((g₁ : (a : ℕ) → ℕ) n)).1
obtain :
  ∀ (m n : ℕ) (hlt : m < n) (hle : r' (f ((g₁ : (a : ℕ) → ℕ) m)).2 (f ((g₁ : (a : ℕ) → ℕ) n)).2),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2

Tactic:
obtain ⟨m, n, hlt, hle⟩ := ht.exists_lt fun n => (hf _).2

Premises used: And.right, Set.PartiallyWellOrderedOn.exists_lt
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r (f ((g₁ : (a : ℕ) → ℕ) m)).1 (f ((g₁ : (a : ℕ) → ℕ) n)).1
m n : ℕ
hlt : m < n
hle : r' (f ((g₁ : (a : ℕ) → ℕ) m)).2 (f ((g₁ : (a : ℕ) → ℕ) n)).2
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2

Tactic:
⟨g₁ m, g₁ n, g₁.strictMono hlt, h₁ _ _ hlt.le, hle⟩

Premises used: OrderEmbedding.strictMono, LT.lt.le, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
s : Set α
inst : IsPreorder α r
t : Set β
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r'
f : ℕ → α × β
hf : ∀ (n : ℕ), f n ∈ s ×ˢ t
g₁ : ℕ ↪o ℕ
h₁ : ∀ (m n : ℕ), m ≤ n → r (f ((g₁ : (a : ℕ) → ℕ) m)).1 (f ((g₁ : (a : ℕ) → ℕ) n)).1
m n : ℕ
hlt : m < n
hle : r' (f ((g₁ : (a : ℕ) → ℕ) m)).2 (f ((g₁ : (a : ℕ) → ℕ) n)).2
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m).1 (f n).1 ∧ r' (f m).2 (f n).2

Tactic:
exact ⟨g₁ m, g₁ n, g₁.strictMono hlt, h₁ _ _ hlt.le, hle⟩
-- 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)
haveI :
  ∀ (this : Fintype ι),
    (pi (α := α) univ s).PartiallyWellOrderedOn 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)

Tactic:
haveI := Fintype.ofFinite ι
-- 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 : Fintype ι
⊢ IsPreorder ((i : ι) → α i) fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
haveI : IsPreorder (∀ i, α i) (fun a b : ∀ i, α i => ∀ i, r i (a i) (b i)) :=
    { refl a i := refl (a i)
      trans a b c hab hbc i := _root_.trans (hab i) (hbc i) }
-- 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_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)
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)
⊢ (pi (α := α) univ s).PartiallyWellOrderedOn fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (b i)

Tactic:
rw [partiallyWellOrderedOn_iff_exists_monotone_subseq]

Premises used: Set.partiallyWellOrderedOn_iff_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_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
⊢ ∀ (n : ℕ) (i : ι), f n i ∈ s i

Tactic:
simp only [mem_pi, mem_univ, forall_const] at hf

Premises used: Set.mem_pi, Set.mem_univ, forall_const
-- 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_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 : ℕ) (i : ι), f n i ∈ s i
⊢ ∃ (g : ℕ ↪o ℕ), ∀ (m n : ℕ), m ≤ n → ∀ (i : ι), r i (f ((g : (a : ℕ) → ℕ) m) i) (f ((g : (a : ℕ) → ℕ) n) i)

Tactic:
simpa only [Finset.mem_univ, true_imp_iff] using this Finset.univ f hf

Premises used: Finset.mem_univ, Finset.univ, true_imp_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)
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)
⊢ (pi (α := α) univ s).PartiallyWellOrderedOn fun (a b : (i : ι) → α i) ↦ ∀ (i : ι), r i (a i) (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