awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
tfae_2_to_3 : ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r
⊢ ∀ (a_1 : WellFoundedOn {b : α | TransGen r b a} r), Acc r a

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
tfae_2_to_3 : ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r
⊢ ∀ (a_1 : WellFoundedOn {b : α | TransGen r b a} r), Acc r a

Tactic:
fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_)

Premises used: WellFounded.apply, Acc.of_fibration, Subtype.mk, Relation.TransGen.single, Subtype.val, Acc.intro
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
tfae_2_to_3 : ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r
refine :
  ∀ (h : WellFoundedOn {b : α | TransGen r b a} r) (b : α) (hb : r b a),
    Fibration (α := { x : α // Membership.mem (γ := Set α) {b : α | TransGen r b a} x })
      (Subrel r fun (x : α) ↦ Membership.mem (γ := Set α) {b : α | TransGen r b a} x) r
      (Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Set α) {b : α | TransGen r b a} x))
⊢ ∀ (a_1 : WellFoundedOn {b : α | TransGen r b a} r), Acc r a

Tactic:
refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_)

Premises used: Acc.intro
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
tfae_2_to_3 : ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r
h : WellFoundedOn {b : α | TransGen r b a} r
b : α
hb : r b a
⊢ Fibration (α := { x : α // Membership.mem (γ := Set α) {b : α | TransGen r b a} x })
    (Subrel r fun (x : α) ↦ Membership.mem (γ := Set α) {b : α | TransGen r b a} x) r
    (Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Set α) {b : α | TransGen r b a} x))

Tactic:
fun ⟨c, hc⟩ d h => ⟨⟨d, .head h hc⟩, h, rfl⟩

Premises used: _private.0.Set.WellFoundedOn.acc_iff_wellFoundedOn.match_1, Relation.TransGen.head, setOf, Membership.mem, Exists, Subrel, Subtype.mk, And, And.intro, Relation.TransGen, Exists.intro, Subtype.val, Relation.Fibration, Eq, rfl
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
tfae_2_to_3 : ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r
h : WellFoundedOn {b : α | TransGen r b a} r
b : α
hb : r b a
⊢ Fibration (α := { x : α // Membership.mem (γ := Set α) {b : α | TransGen r b a} x })
    (Subrel r fun (x : α) ↦ Membership.mem (γ := Set α) {b : α | TransGen r b a} x) r
    (Subtype.val (p := fun (x : α) ↦ Membership.mem (γ := Set α) {b : α | TransGen r b a} x))

Tactic:
exact fun ⟨c, hc⟩ d h => ⟨⟨d, .head h hc⟩, h, rfl⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
tfae_2_to_3 : ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r
⊢ ∀ (a_1 : WellFoundedOn {b : α | TransGen r b a} r), Acc r a

Tactic:
tfae_have 3 → 1 := by
    refine fun h => Acc.intro _ (fun b hb => (h.apply ⟨b, .single hb⟩).of_fibration Subtype.val ?_)
    exact fun ⟨c, hc⟩ d h => ⟨⟨d, .head h hc⟩, h, rfl⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
r : α → α → Prop
a : α
tfae_1_to_2 : ∀ (a_1 : Acc r a), WellFoundedOn {b : α | ReflTransGen r b a} r
tfae_2_to_3 : ∀ (a_1 : WellFoundedOn {b : α | ReflTransGen r b a} r), WellFoundedOn {b : α | TransGen r b a} r
tfae_3_to_1 : ∀ (a_1 : WellFoundedOn {b : α | TransGen r b a} r), Acc r a
⊢ [Acc r a, WellFoundedOn {b : α | ReflTransGen r b a} r, WellFoundedOn {b : α | TransGen r b a} r].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
simp :
  Nonempty.{u_2 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s) ↔
    ∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)
⊢ s.WellFoundedOn r ↔
    ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)

Tactic:
simp only [wellFoundedOn_iff, RelEmbedding.wellFounded_iff_isEmpty, ← not_exists, ←
    not_nonempty_iff, not_iff_not]

Premises used: not_iff_not, not_exists, Set.wellFoundedOn_iff, not_nonempty_iff, RelEmbedding.wellFounded_iff_isEmpty
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
mp :
  Nonempty.{u_2 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s) →
    ∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)
mpr :
  (∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)) →
    Nonempty.{u_2 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s)
⊢ Nonempty.{u_2 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s) ↔
    ∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)

Tactic:
constructor
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf :
  ∀ {a b : ℕ},
    r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ∧
        Membership.mem (α := α) s ((f : (a : ℕ) → α) a : α) ∧ Membership.mem (α := α) s ((f : (a : ℕ) → α) b : α) ↔
      a > b
⊢ ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)

Tactic:
have H : ∀ n, f n ∈ s := fun n => (hf.2 n.lt_succ_self).2.2
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf :
  ∀ {a b : ℕ},
    r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ∧
        Membership.mem (α := α) s ((f : (a : ℕ) → α) a : α) ∧ Membership.mem (α := α) s ((f : (a : ℕ) → α) b : α) ↔
      a > b
H : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
⊢ ∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)

Tactic:
⟨⟨f, ?_⟩, H⟩

Premises used: RelEmbedding.mk, Exists.intro
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf :
  ∀ {a b : ℕ},
    r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ∧
        Membership.mem (α := α) s ((f : (a : ℕ) → α) a : α) ∧ Membership.mem (α := α) s ((f : (a : ℕ) → α) b : α) ↔
      a > b
H : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
mp : ∀ {a b : ℕ}, r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ↔ a > b
⊢ ∃ (x : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ∀ (n : ℕ), Membership.mem (α := α) s ((x : (a : ℕ) → α) n : α)

Tactic:
refine ⟨⟨f, ?_⟩, H⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf :
  ∀ {a b : ℕ},
    r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ∧
        Membership.mem (α := α) s ((f : (a : ℕ) → α) a : α) ∧ Membership.mem (α := α) s ((f : (a : ℕ) → α) b : α) ↔
      a > b
H : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
⊢ ∀ {a b : ℕ}, r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ↔ a > b

Tactic:
simpa only [H, and_true] using @hf

Premises used: and_true
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ↔ a > b
hfs : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
⊢ Nonempty.{u_2 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s)

Tactic:
⟨⟨f, ?_⟩⟩

Premises used: RelEmbedding.mk, Nonempty.intro
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ↔ a > b
hfs : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
mpr :
  ∀ {a b : ℕ},
    r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ∧
        Membership.mem (α := α) s ((f : (a : ℕ) → α) a : α) ∧ Membership.mem (α := α) s ((f : (a : ℕ) → α) b : α) ↔
      a > b
⊢ Nonempty.{u_2 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (a b : α) ↦ r a b ∧ a ∈ s ∧ b ∈ s)

Tactic:
refine ⟨⟨f, ?_⟩⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
f : ℕ ↪ α
hf : ∀ {a b : ℕ}, r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ↔ a > b
hfs : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
⊢ ∀ {a b : ℕ},
    r ((f : (a : ℕ) → α) a) ((f : (a : ℕ) → α) b) ∧
        Membership.mem (α := α) s ((f : (a : ℕ) → α) a : α) ∧ Membership.mem (α := α) s ((f : (a : ℕ) → α) b : α) ↔
      a > b

Tactic:
simpa only [hfs, and_true] using @hf

Premises used: and_true
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s t : Set α
hs : s.WellFoundedOn r
ht : t.WellFoundedOn r
rw :
  ∀ (hs : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α))
    (ht : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) t ((f : (a : ℕ) → α) n : α))
    (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) (s ∪ t) ((f : (a : ℕ) → α) n : α)
⊢ (s ∪ t).WellFoundedOn r

Tactic:
rw [wellFoundedOn_iff_no_descending_seq] at *

Premises used: Set.wellFoundedOn_iff_no_descending_seq
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
ht : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) t ((f : (a : ℕ) → α) n : α)
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
hf : ∀ (n : ℕ), Membership.mem (α := α) (s ∪ t) ((f : (a : ℕ) → α) n : α)
inl :
  ∀ (g : ℕ ↪o ℕ) (hg : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) ((g : (a : ℕ) → ℕ) n : ℕ) : α)), False
inr :
  ∀ (g : ℕ ↪o ℕ) (hg : ∀ (n : ℕ), Membership.mem (α := α) t ((f : (a : ℕ) → α) ((g : (a : ℕ) → ℕ) n : ℕ) : α)), False
⊢ False

Tactic:
rcases Nat.exists_subseq_of_forall_mem_union f hf with ⟨g, hg | hg⟩

Premises used: Nat.exists_subseq_of_forall_mem_union, DFunLike.coe
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
ht : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) t ((f : (a : ℕ) → α) n : α)
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
hf : ∀ (n : ℕ), Membership.mem (α := α) (s ∪ t) ((f : (a : ℕ) → α) n : α)
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) ((g : (a : ℕ) → ℕ) n : ℕ) : α)
⊢ False

Tactic:
hs (g.dual.ltEmbedding.trans f) hg

Premises used: OrderEmbedding.ltEmbedding, RelEmbedding.trans, OrderEmbedding.dual
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
ht : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) t ((f : (a : ℕ) → α) n : α)
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
hf : ∀ (n : ℕ), Membership.mem (α := α) (s ∪ t) ((f : (a : ℕ) → α) n : α)
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), Membership.mem (α := α) t ((f : (a : ℕ) → α) ((g : (a : ℕ) → ℕ) n : ℕ) : α)
⊢ False

Tactic:
ht (g.dual.ltEmbedding.trans f) hg

Premises used: OrderEmbedding.ltEmbedding, RelEmbedding.trans, OrderEmbedding.dual
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s t : Set α
hs : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
ht : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r), ¬∀ (n : ℕ), Membership.mem (α := α) t ((f : (a : ℕ) → α) n : α)
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
hf : ∀ (n : ℕ), Membership.mem (α := α) (s ∪ t) ((f : (a : ℕ) → α) n : α)
g : ℕ ↪o ℕ
hg : ∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) ((g : (a : ℕ) → ℕ) n : ℕ) : α)
⊢ False

Tactic:
exacts [hs (g.dual.ltEmbedding.trans f) hg, ht (g.dual.ltEmbedding.trans f) hg]

Premises used: OrderEmbedding.ltEmbedding, RelEmbedding.trans, OrderEmbedding.dual
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s t : Set α
⊢ (s ∪ t).WellFoundedOn r ↔ s.WellFoundedOn r ∧ t.WellFoundedOn r

Tactic:
⟨fun h => ⟨h.subset subset_union_left, h.subset subset_union_right⟩, fun h =>
    h.1.union h.2⟩

Premises used: Set.subset_union_right, Set.subset_union_left, And.right, And.left, And.intro, Iff.intro, Set.WellFoundedOn.subset, Set.WellFoundedOn.union
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : LT α
⊢ IsWF.{u_2} (α := α) ∅

Tactic:
wellFounded_of_isEmpty _

Premises used: wellFounded_of_isEmpty, Set.IsWF, Set.WellFoundedOn
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : LT α
s t : Set α
h : t.IsWF
st : s ⊆ t
⊢ s.IsWF

Tactic:
h.subset st

Premises used: Set.IsWF, Set.WellFoundedOn.subset
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : LT α
⊢ IsWF.{u_2} (α := α) univ ↔ WellFoundedLT α

Tactic:
simp [IsWF, wellFoundedOn_iff, isWellFounded_iff]

Premises used: Set.wellFoundedOn_iff, isWellFounded_iff, Set.IsWF
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : LT α
h : WellFoundedLT α
s : Set α
⊢ s.IsWF

Tactic:
(Set.isWF_univ_iff.2 h).mono s.subset_univ

Premises used: Iff.mpr, Set.subset_univ, Set.IsWF.mono, Set.isWF_univ_iff
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s t : Set α
hs : s.IsWF
ht : t.IsWF
⊢ (s ∪ t).IsWF

Tactic:
hs.union ht

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

Tactic:
wellFoundedOn_union

Premises used: Set.IsWF, Set.wellFoundedOn_union
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
⊢ s.IsWF ↔ ∀ (f : ℕ → α), StrictAnti f → ¬∀ (n : ℕ), f n ∈ s

Tactic:
wellFoundedOn_iff_no_descending_seq.trans
    ⟨fun H f hf => H ⟨⟨f, hf.injective⟩, hf.lt_iff_gt⟩, fun H f => H f fun _ _ => f.map_rel_iff.2⟩

Premises used: Iff.mpr, RelEmbedding.mk, Function.Embedding.mk, Set.wellFoundedOn_iff_no_descending_seq, RelEmbedding.map_rel_iff, Iff.intro, Iff.trans, StrictAnti.injective, Set.IsWF, StrictAnti.lt_iff_gt, DFunLike.coe
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (n : ℕ), f n ∈ s
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

Tactic:
hs fun n ↦ ⟨_, hf n⟩

Premises used: Subrel, Subtype.mk, Order.Preimage
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
⊢ s.PartiallyWellOrderedOn r ↔ ∀ (f : ℕ → α), (∀ (n : ℕ), f n ∈ s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

Tactic:
⟨PartiallyWellOrderedOn.exists_lt, fun hf f ↦ hf _ fun n ↦ (f n).2⟩

Premises used: Set.PartiallyWellOrderedOn.exists_lt, Iff.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
⊢ ∀ (x : α), Membership.mem (γ := Set α) univ x

Tactic:
simp
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
ht : t.PartiallyWellOrderedOn r
h : s ⊆ t
⊢ s.PartiallyWellOrderedOn r

Tactic:
fun f ↦ ht (Set.inclusion h ∘ f)

Premises used: Set.PartiallyWellOrderedOn, Set.Mem, Function.comp, Subrel, Set.inclusion, WellQuasiOrdered, Order.Preimage
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
h : WellQuasiOrdered r
s : Set α
⊢ s.PartiallyWellOrderedOn r

Tactic:
(partiallyWellOrderedOn_univ_iff.mpr h).mono s.subset_univ

Premises used: Iff.mpr, Set.subset_univ, Set.partiallyWellOrderedOn_univ_iff, Set.PartiallyWellOrderedOn.mono
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
⊢ PartiallyWellOrderedOn ∅ r

Tactic:
wellQuasiOrdered_of_isEmpty _

Premises used: Set.PartiallyWellOrderedOn, wellQuasiOrdered_of_isEmpty
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x : α // x ∈ s ∪ t }
inl :
  ∀ (g : ℕ ↪o ℕ) (hgs : ∀ (n : ℕ), (↑(f ((g : (a : ℕ) → ℕ) n)) : α) ∈ s),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)
inr :
  ∀ (g : ℕ ↪o ℕ) (hgt : ∀ (n : ℕ), (↑(f ((g : (a : ℕ) → ℕ) n)) : α) ∈ t),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
obtain ⟨g, hgs | hgt⟩ := Nat.exists_subseq_of_forall_mem_union _ fun x ↦ (f x).2

Premises used: Nat.exists_subseq_of_forall_mem_union, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x : α // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), (↑(f ((g : (a : ℕ) → ℕ) n)) : α) ∈ s
inl :
  ∀ (m n : ℕ) (hlt : m < n) (hr : r (↑(f ((g : (a : ℕ) → ℕ) m)) : α) (↑(f ((g : (a : ℕ) → ℕ) n)) : α)),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
rcases hs.exists_lt hgs with ⟨m, n, hlt, hr⟩

Premises used: Set.PartiallyWellOrderedOn.exists_lt
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x : α // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), (↑(f ((g : (a : ℕ) → ℕ) n)) : α) ∈ s
m n : ℕ
hlt : m < n
hr : r (↑(f ((g : (a : ℕ) → ℕ) m)) : α) (↑(f ((g : (a : ℕ) → ℕ) n)) : α)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
⟨g m, g n, g.strictMono hlt, hr⟩

Premises used: OrderEmbedding.strictMono, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x : α // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgs : ∀ (n : ℕ), (↑(f ((g : (a : ℕ) → ℕ) n)) : α) ∈ s
m n : ℕ
hlt : m < n
hr : r (↑(f ((g : (a : ℕ) → ℕ) m)) : α) (↑(f ((g : (a : ℕ) → ℕ) n)) : α)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
exact ⟨g m, g n, g.strictMono hlt, hr⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x : α // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), (↑(f ((g : (a : ℕ) → ℕ) n)) : α) ∈ t
inr :
  ∀ (m n : ℕ) (hlt : m < n) (hr : r (↑(f ((g : (a : ℕ) → ℕ) m)) : α) (↑(f ((g : (a : ℕ) → ℕ) n)) : α)),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
rcases ht.exists_lt hgt with ⟨m, n, hlt, hr⟩

Premises used: Set.PartiallyWellOrderedOn.exists_lt
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x : α // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), (↑(f ((g : (a : ℕ) → ℕ) n)) : α) ∈ t
m n : ℕ
hlt : m < n
hr : r (↑(f ((g : (a : ℕ) → ℕ) m)) : α) (↑(f ((g : (a : ℕ) → ℕ) n)) : α)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
⟨g m, g n, g.strictMono hlt, hr⟩

Premises used: OrderEmbedding.strictMono, And.intro, Exists.intro, DFunLike.coe
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
hs : s.PartiallyWellOrderedOn r
ht : t.PartiallyWellOrderedOn r
f : ℕ → { x : α // x ∈ s ∪ t }
g : ℕ ↪o ℕ
hgt : ∀ (n : ℕ), (↑(f ((g : (a : ℕ) → ℕ) n)) : α) ∈ t
m n : ℕ
hlt : m < n
hr : r (↑(f ((g : (a : ℕ) → ℕ) m)) : α) (↑(f ((g : (a : ℕ) → ℕ) n)) : α)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ Subrel r (fun (x : α) ↦ x ∈ s ∪ t) (f m) (f n)

Tactic:
exact ⟨g m, g n, g.strictMono hlt, hr⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s t : Set α
⊢ (s ∪ t).PartiallyWellOrderedOn r ↔ s.PartiallyWellOrderedOn r ∧ t.PartiallyWellOrderedOn r

Tactic:
⟨fun h ↦ ⟨h.mono subset_union_left, h.mono subset_union_right⟩, fun h ↦ h.1.union h.2⟩

Premises used: Set.subset_union_right, Set.subset_union_left, And.right, And.left, And.intro, Iff.intro, Set.PartiallyWellOrderedOn.union, Set.PartiallyWellOrderedOn.mono
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
β : Type u_3
r : α → α → Prop
r' : β → β → Prop
f : α → β
s : Set α
hs : s.PartiallyWellOrderedOn r
hf : ∀ a₁ ∈ s, ∀ a₂ ∈ s, r a₁ a₂ → r' (f a₁) (f a₂)
rw :
  ∀ (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₂)) (f_1 : ℕ → β),
    (∀ (n : ℕ), f_1 n ∈ f '' s) → ∃ (m : ℕ) (n : ℕ), m < n ∧ r' (f_1 m) (f_1 n)
⊢ (f '' s).PartiallyWellOrderedOn r'

Tactic:
rw [partiallyWellOrderedOn_iff_exists_lt] at *

Premises used: Set.partiallyWellOrderedOn_iff_exists_lt
-- 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' : ℕ → β
hg' : ∀ (n : ℕ), g' n ∈ f '' s
choose :
  ∀ (g : (n : ℕ) → α) (hgs : ∀ (n : ℕ), g n ∈ s) (heq : ∀ (n : ℕ), f (g n) = g' n),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ r' (g' m) (g' n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r' (g' m) (g' n)

Tactic:
choose g hgs heq using hg'
-- 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' : ℕ → β
g : (n : ℕ) → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = g' n
⊢ f ∘ g = g'

Tactic:
funext heq

Premises used: funext
-- 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' : ℕ → β
g : (n : ℕ) → α
hgs : ∀ (n : ℕ), g n ∈ s
heq : ∀ (n : ℕ), f (g n) = g' n
obtain : ∀ (heq : ∀ (n : ℕ), f (g n) = (f ∘ g) n), ∃ (m : ℕ) (n : ℕ), m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r' (g' m) (g' n)

Tactic:
obtain rfl : f ∘ g = g' := funext heq

Premises used: funext, rfl
-- 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
obtain : ∀ (m n : ℕ) (hlt : m < n) (hmn : r (g m) (g n)), ∃ (m : ℕ) (n : ℕ), m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r' ((f ∘ g) m) ((f ∘ g) n)

Tactic:
obtain ⟨m, n, hlt, hmn⟩ := hs g hgs