awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
h : s.IsPWO
a : α
ha : a ∈ s
obtain : ∀ b ≤ a, ∀ (hb : Minimal (fun (x : α) ↦ x ∈ s) b), ∃ (a : α), Minimal (fun (x : α) ↦ x ∈ s) a
⊢ ∃ (a : α), Minimal (fun (x : α) ↦ x ∈ s) a

Tactic:
obtain ⟨b, _, hb⟩ := h.exists_le_minimal ha

Premises used: Set.IsPWO.exists_le_minimal
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
h : s.IsPWO
a : α
ha : a ∈ s
b : α
left : b ≤ a
hb : Minimal (fun (x : α) ↦ x ∈ s) b
⊢ ∃ (a : α), Minimal (fun (x : α) ↦ x ∈ s) a

Tactic:
⟨b, hb⟩

Premises used: Exists.intro
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
h : s.IsPWO
a : α
ha : a ∈ s
b : α
left : b ≤ a
hb : Minimal (fun (x : α) ↦ x ∈ s) b
⊢ ∃ (a : α), Minimal (fun (x : α) ↦ x ∈ s) a

Tactic:
exact ⟨b, hb⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
f : ι → α
s : Set ι
h : (f '' s).IsPWO
hs : s.Nonempty
obtain : ∀ (w : α) (h : Minimal (fun (x : α) ↦ x ∈ f '' s) w), ∃ (i : ι), MinimalFor (fun (x : ι) ↦ x ∈ s) f i
⊢ ∃ (i : ι), MinimalFor (fun (x : ι) ↦ x ∈ s) f i

Tactic:
obtain ⟨_, h⟩ := h.exists_minimal (hs.image _)

Premises used: Set.IsPWO.exists_minimal, Set.Nonempty.image
-- Module: Mathlib.Order.WellFoundedSet
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
obtain :
  ∀ (a : ι) (ha : a ∈ s) (h : Minimal (fun (x : α) ↦ x ∈ f '' s) (f a)), ∃ (i : ι), MinimalFor (fun (x : ι) ↦ x ∈ s) f i
⊢ ∃ (i : ι), MinimalFor (fun (x : ι) ↦ x ∈ s) f i

Tactic:
obtain ⟨a, ha, rfl⟩ := h.1

Premises used: And.left, rfl
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
f : ι → α
s : Set ι
h_1 : (f '' s).IsPWO
hs : s.Nonempty
a : ι
ha : a ∈ s
h : Minimal (fun (x : α) ↦ x ∈ f '' s) (f a)
⊢ ∃ (i : ι), MinimalFor (fun (x : ι) ↦ x ∈ s) f i

Tactic:
⟨a, ha, fun b hb => h.2 (mem_image_of_mem _ hb)⟩

Premises used: And.right, Set.mem_image_of_mem, And.intro, Exists.intro
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
f : ι → α
s : Set ι
h_1 : (f '' s).IsPWO
hs : s.Nonempty
a : ι
ha : a ∈ s
h : Minimal (fun (x : α) ↦ x ∈ f '' s) (f a)
⊢ ∃ (i : ι), MinimalFor (fun (x : ι) ↦ x ∈ s) f i

Tactic:
exact ⟨a, ha, fun b hb => h.2 (mem_image_of_mem _ hb)⟩
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
hs : s.Finite
⊢ s.WellFoundedOn r

Tactic:
letI := partialOrderOfSO r
  hs.isWF

Premises used: Set.Finite.isWF, Set.IsWF
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
a : α
⊢ WellFoundedOn {a} r

Tactic:
(finite_singleton a).wellFoundedOn

Premises used: Set.Finite.wellFoundedOn, Set.finite_singleton
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
hs : s.Subsingleton
⊢ s.WellFoundedOn r

Tactic:
hs.finite.wellFoundedOn

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

Tactic:
simp only [← singleton_union, wellFoundedOn_union, wellFoundedOn_singleton, true_and]

Premises used: Set.singleton_union, Set.wellFoundedOn_union, Set.wellFoundedOn_singleton, true_and
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
a : α
⊢ (s \ {a}).WellFoundedOn r ↔ s.WellFoundedOn r

Tactic:
simp only [← wellFoundedOn_insert (a := a), insert_diff_singleton, mem_insert_iff, true_or,
    insert_eq_of_mem]

Premises used: true_or, Set.insert_eq_of_mem, Set.wellFoundedOn_insert, Set.insert_diff_singleton, Set.mem_insert_iff
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
h : s.WellFoundedOn r
a : α
⊢ (insert a s).WellFoundedOn r

Tactic:
wellFoundedOn_insert.2 h

Premises used: Iff.mpr, Set.wellFoundedOn_insert
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Set α
h : s.WellFoundedOn r
a : α
⊢ (s \ {a}).WellFoundedOn r

Tactic:
wellFoundedOn_sdiff_singleton.2 h

Premises used: Iff.mpr, Set.wellFoundedOn_sdiff_singleton
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
β : Type u_7
r : α → α → Prop
f : β → α
s : Set α
t : Set β
h : MapsTo f t s
hw : s.WellFoundedOn r
⊢ t.WellFoundedOn (r on f)

Tactic:
InvImage.wf (fun x : t ↦ ⟨f x, h x.prop⟩) hw

Premises used: Subrel, InvImage.wf, Order.Preimage, Set.WellFoundedOn
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
β : Type u_7
r : α → α → Prop
f : β → α
s : Set α
t : Set β
h : MapsTo f t s
hw : s.WellFoundedOn r
⊢ t.WellFoundedOn (r on f)

Tactic:
exact InvImage.wf (fun x : t ↦ ⟨f x, h x.prop⟩) hw

Premises used: InvImage.wf
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_6
inst : Preorder α
s : Set α
h : s.WellFoundedOn fun (x1 x2 : α) ↦ x1 < x2
nonempty : s.Nonempty
⊢ ∃ (a : α), Minimal (fun (x : α) ↦ x ∈ s) a

Tactic:
have ⟨m, hm⟩ := WellFoundedLT.exists_minimal ⟨h⟩ univ <| nonempty.elim (⟨⟨·, ·⟩, trivial⟩)
  ⟨m, m.property, fun y hy ↦ hm.right (y := ⟨y, hy⟩) trivial⟩

Premises used: trivial, IsWellFounded.mk, Set.univ, Membership.mem, Exists, Subtype.mk, And.right, _private.0.Set.WellFoundedOn.exists_minimal.match_1, And.intro, WellFoundedLT.exists_minimal, Exists.intro, Subtype.val, Minimal, Exists.elim, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
change :
  (WellQuasiOrdered fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 ≤ x2) ↔ WellFounded fun (x1 x2 : { x : α // x ∈ s }) ↦ x1 < x2
⊢ s.IsPWO ↔ s.IsWF

Tactic:
change WellQuasiOrdered (· ≤ ·) ↔ WellFounded (· < ·)

Premises used: LE.le, LT.lt, WellQuasiOrdered, WellFounded
-- Module: Mathlib.Order.WellFoundedSet
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
rw₂ rw₃ :
  WellFoundedLT.{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

Tactic:
rw [← wellQuasiOrderedLE_def, ← isWellFounded_iff, wellQuasiOrderedLE_iff_wellFoundedLT]

Premises used: wellQuasiOrderedLE_def, wellQuasiOrderedLE_iff_wellFoundedLT, isWellFounded_iff
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : WellFoundedLT α
s : Set α
⊢ s.IsPWO

Tactic:
(IsWF.of_wellFoundedLT s).isPWO

Premises used: Set.IsWF.isPWO, Set.IsWF.of_wellFoundedLT
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : Std.Refl r
s : Finset α
⊢ (↑s : Set α).PartiallyWellOrderedOn r

Tactic:
s.finite_toSet.partiallyWellOrderedOn

Premises used: Set.Finite.partiallyWellOrderedOn, Finset.finite_toSet
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Finset α
⊢ (↑s : Set α).IsPWO

Tactic:
s.partiallyWellOrderedOn

Premises used: Set.IsPWO, Finset.partiallyWellOrderedOn
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Finset α
⊢ (↑s : Set α).IsWF

Tactic:
s.finite_toSet.isWF

Premises used: Set.Finite.isWF, Finset.finite_toSet
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Finset α
⊢ (↑s : Set α).WellFoundedOn r

Tactic:
letI := partialOrderOfSO r
  s.isWF

Premises used: Set.IsWF, Finset.isWF
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Finset ι
f : ι → Set α
⊢ (sup ∅ f).WellFoundedOn r ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (f i).WellFoundedOn r

Tactic:
simp
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s_1 : Finset ι
f : ι → Set α
a : ι
s : Finset ι
ha : a ∉ s
hs : (s.sup f).WellFoundedOn r ↔ ∀ i ∈ s, (f i).WellFoundedOn r
⊢ ((cons a s ha).sup f).WellFoundedOn r ↔ ∀ i ∈ cons a s ha, (f i).WellFoundedOn r

Tactic:
simp [-sup_set_eq_biUnion, hs]

Premises used: Finset.sup_set_eq_biUnion
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : Type u_2
r : α → α → Prop
s : Finset ι
f : ι → Set α
⊢ (sup ∅ f).PartiallyWellOrderedOn r ↔ ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → (f i).PartiallyWellOrderedOn r

Tactic:
simp
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : Type u_2
r : α → α → Prop
s_1 : Finset ι
f : ι → Set α
a : ι
s : Finset ι
ha : a ∉ s
hs : (s.sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r
⊢ ((cons a s ha).sup f).PartiallyWellOrderedOn r ↔ ∀ i ∈ cons a s ha, (f i).PartiallyWellOrderedOn r

Tactic:
simp [-sup_set_eq_biUnion, hs]

Premises used: Finset.sup_set_eq_biUnion
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
s : Finset ι
f : ι → Set α
⊢ (s.sup f).IsWF ↔ ∀ i ∈ s, (f i).IsWF

Tactic:
s.wellFoundedOn_sup

Premises used: Set.IsWF, Finset.wellFoundedOn_sup
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
s : Finset ι
f : ι → Set α
⊢ (s.sup f).IsPWO ↔ ∀ i ∈ s, (f i).IsPWO

Tactic:
s.partiallyWellOrderedOn_sup

Premises used: Set.IsPWO, Finset.partiallyWellOrderedOn_sup
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : Type u_2
r : α → α → Prop
inst : IsStrictOrder α r
s : Finset ι
f : ι → Set α
⊢ Set.WellFoundedOn (⋃ i ∈ s, f i) r ↔ ∀ i ∈ s, (f i).WellFoundedOn r

Tactic:
simpa only [Finset.sup_eq_iSup] using s.wellFoundedOn_sup

Premises used: Finset.sup_eq_iSup, Finset.wellFoundedOn_sup
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : Type u_2
r : α → α → Prop
s : Finset ι
f : ι → Set α
⊢ Set.PartiallyWellOrderedOn (⋃ i ∈ s, f i) r ↔ ∀ i ∈ s, (f i).PartiallyWellOrderedOn r

Tactic:
simpa only [Finset.sup_eq_iSup] using s.partiallyWellOrderedOn_sup

Premises used: Finset.sup_eq_iSup, Finset.partiallyWellOrderedOn_sup
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
s : Finset ι
f : ι → Set α
⊢ Set.IsWF.{u_2} (α := α) (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, (f i).IsWF

Tactic:
s.wellFoundedOn_bUnion

Premises used: Finset.wellFoundedOn_bUnion, Set.IsWF
-- Module: Mathlib.Order.WellFoundedSet
Goal:
ι : Type u_1
α : Type u_2
inst : Preorder α
s : Finset ι
f : ι → Set α
⊢ Set.IsPWO.{u_2} (α := α) (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, (f i).IsPWO

Tactic:
s.partiallyWellOrderedOn_bUnion

Premises used: Set.IsPWO, Finset.partiallyWellOrderedOn_bUnion
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
hs : s.IsWF
hn : s.Nonempty
⊢ hs.min (s := s) hn ∈ s

Tactic:
(WellFounded.min hs univ (nonempty_iff_univ_nonempty.1 hn.to_subtype)).2

Premises used: Set.Mem, Set.univ, Set.Nonempty.to_subtype, Set.nonempty_iff_univ_nonempty, Set.IsWF.min, WellFounded.min, Iff.mp, Subtype.property
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
hs : s.IsWF
hn : s.Nonempty
ha : a ∈ s
⊢ ¬a < hs.min (s := s) hn

Tactic:
hs.not_lt_min univ (mem_univ (⟨a, ha⟩ : s))

Premises used: Set.univ, Subrel, Subtype.mk, Set.IsWF.min, Set.mem_univ, WellFounded.not_lt_min, Order.Preimage
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
hst : s ⊆ t
⊢ ¬hs.min (s := s) hsn < ht.min (s := t) htn

Tactic:
ht.not_lt_min htn (hst (min_mem hs hsn))

Premises used: Set.IsWF.not_lt_min, Set.IsWF.min_mem
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
a : α
hs : IsWF (α := α) {a}
hn : Set.Nonempty (α := α) {a}
⊢ hs.min (s := {a}) hn = a

Tactic:
eq_of_mem_singleton (IsWF.min_mem hs hn)

Premises used: Set.eq_of_mem_singleton, Set.IsWF.min_mem
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
hs : s.IsWF
ha : a ∈ s
hlt : ∀ b ∈ s, b ≠ a → a < b
by_contra : ∀ (h : ¬hs.min (s := s) ⋯ = a), False
⊢ hs.min (s := s) ⋯ = a

Tactic:
by_contra h
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
hs : s.IsWF
ha : a ∈ s
hlt : ∀ b ∈ s, b ≠ a → a < b
h : ¬hs.min (s := s) ⋯ = a
⊢ False

Tactic:
(hs.not_lt_min (nonempty_of_mem ha) ha) (hlt (hs.min (nonempty_of_mem ha))
    (hs.min_mem (nonempty_of_mem ha)) h)

Premises used: Set.IsWF.not_lt_min, Set.IsWF.min_mem, Set.IsWF.min, Set.nonempty_of_mem
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : Preorder α
s : Set α
a : α
hs : s.IsWF
ha : a ∈ s
hlt : ∀ b ∈ s, b ≠ a → a < b
h : ¬hs.min (s := s) ⋯ = a
⊢ False

Tactic:
exact (hs.not_lt_min (nonempty_of_mem ha) ha) (hlt (hs.min (nonempty_of_mem ha))
    (hs.min_mem (nonempty_of_mem ha)) h)

Premises used: Set.IsWF.not_lt_min, Set.IsWF.min_mem, Set.IsWF.min, Set.nonempty_of_mem
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : PartialOrder α
s : Set α
a : α
hs : s.IsWF
ha : a ∈ s
hle : ∀ b ∈ s, a ≤ b
⊢ hs.min (s := s) ⋯ = a

Tactic:
(eq_of_le_of_not_lt (hle (hs.min (nonempty_of_mem ha))
    (hs.min_mem (nonempty_of_mem ha))) (hs.not_lt_min (nonempty_of_mem ha) ha)).symm

Premises used: Set.IsWF.not_lt_min, Set.IsWF.min_mem, Set.IsWF.min, Set.nonempty_of_mem, Eq.symm, eq_of_le_of_not_lt
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
a : α
hs : s.IsWF
hn : s.Nonempty
ha : a ∈ s
⊢ hs.min (s := s) hn ≤ a

Tactic:
le_of_not_gt (hs.not_lt_min hn ha)

Premises used: Set.IsWF.not_lt_min, le_of_not_gt
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : LinearOrder α
s : Set α
a : α
hs : s.IsWF
hn : s.Nonempty
⊢ a ≤ hs.min (s := s) hn ↔ ∀ b ∈ s, a ≤ b

Tactic:
⟨fun ha _b hb => le_trans ha (hs.min_le hn hb), fun h => h _ (hs.min_mem _)⟩

Premises used: Set.IsWF.min_mem, Set.IsWF.min, Iff.intro, Set.IsWF.min_le, le_trans
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
hst : s ⊆ t
⊢ ht.min (s := t) htn ≤ hs.min (s := s) hsn

Tactic:
(IsWF.le_min_iff _ _).2 fun _b hb => ht.min_le htn (hst hb)

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

Tactic:
le_antisymm (le_min (IsWF.min_le_min_of_subset subset_union_left)
    (IsWF.min_le_min_of_subset subset_union_right)) ?_

Premises used: Set.subset_union_right, le_min, Set.subset_union_left, le_antisymm, Set.IsWF.min_le_min_of_subset
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
refine : Min.min (hs.min (s := s) hsn) (ht.min (s := t) htn) ≤ ⋯.min (s := s ∪ t) ⋯
⊢ ⋯.min (s := s ∪ t) ⋯ = Min.min (hs.min (s := s) hsn) (ht.min (s := t) htn)

Tactic:
refine le_antisymm (le_min (IsWF.min_le_min_of_subset subset_union_left)
    (IsWF.min_le_min_of_subset subset_union_right)) ?_

Premises used: Set.subset_union_right, le_min, Set.subset_union_left, le_antisymm, Set.IsWF.min_le_min_of_subset
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
rw : hs.min (s := s) hsn ≤ ⋯.min (s := s ∪ t) ⋯ ∨ ht.min (s := t) htn ≤ ⋯.min (s := s ∪ t) ⋯
⊢ Min.min (hs.min (s := s) hsn) (ht.min (s := t) htn) ≤ ⋯.min (s := s ∪ t) ⋯

Tactic:
rw [min_le_iff]

Premises used: min_le_iff
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ hs.min (s := s) hsn ≤ ⋯.min (s := s ∪ t) ⋯ ∨ ht.min (s := t) htn ≤ ⋯.min (s := s ∪ t) ⋯

Tactic:
((mem_union _ _ _).1 ((hs.union ht).min_mem (union_nonempty.2 (.inl hsn)))).imp
    (hs.min_le _) (ht.min_le _)

Premises used: Set.mem_union, Iff.mpr, Set.union_nonempty, Set.IsWF.min_mem, Set.IsWF.union, Iff.mp, Set.IsWF.min_le, Or.inl, Or.imp
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
inst : LinearOrder α
s t : Set α
hs : s.IsWF
hsn : s.Nonempty
ht : t.IsWF
htn : t.Nonempty
⊢ hs.min (s := s) hsn ≤ ⋯.min (s := s ∪ t) ⋯ ∨ ht.min (s := t) htn ≤ ⋯.min (s := s ∪ t) ⋯

Tactic:
exact ((mem_union _ _ _).1 ((hs.union ht).min_mem (union_nonempty.2 (.inl hsn)))).imp
    (hs.min_le _) (ht.min_le _)

Premises used: Set.mem_union, Iff.mpr, Set.union_nonempty, Set.IsWF.min_mem, Set.IsWF.union, Iff.mp, Set.IsWF.min_le, Or.inl, Or.imp
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
s : Set α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
rw :
  BddBelow s →
    ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2),
      ¬∀ (n : ℕ), Membership.mem (α := α) s ((f : (a : ℕ) → α) n : α)
⊢ BddBelow s → s.WellFoundedOn fun (x1 x2 : α) ↦ x1 < x2

Tactic:
rw [wellFoundedOn_iff_no_descending_seq]

Premises used: Set.wellFoundedOn_iff_no_descending_seq
-- Module: Mathlib.Order.WellFoundedSet
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

Tactic:
infinite_range_of_injective f.injective ?_

Premises used: Set.infinite_range_of_injective, RelEmbedding.injective
-- Module: Mathlib.Order.WellFoundedSet
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 : α)
refine : Set.Finite (α := α) (range (ι := ℕ) (⇑f : (a : ℕ) → α))
⊢ False

Tactic:
refine infinite_range_of_injective f.injective ?_

Premises used: Set.infinite_range_of_injective, RelEmbedding.injective
-- Module: Mathlib.Order.WellFoundedSet
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 : α)
⊢ Set.Finite (α := α) (range (ι := ℕ) (⇑f : (a : ℕ) → α))

Tactic:
(finite_Icc a <| f 0).subset <| range_subset_iff.2 <| fun n =>
    ⟨ha <| hf _,
      antitone_iff_forall_lt.2 (fun a b hab => (f.map_rel_iff.2 hab).le) <| Nat.zero_le _⟩

Premises used: Iff.mpr, Nat.zero_le, LT.lt.le, Set.Finite.subset, Set.finite_Icc, RelEmbedding.map_rel_iff, And.intro, antitone_iff_forall_lt, Set.range_subset_iff, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Order.WellFoundedSet
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 : α)
⊢ Set.Finite (α := α) (range (ι := ℕ) (⇑f : (a : ℕ) → α))

Tactic:
exact (finite_Icc a <| f 0).subset <| range_subset_iff.2 <| fun n =>
    ⟨ha <| hf _,
      antitone_iff_forall_lt.2 (fun a b hab => (f.map_rel_iff.2 hab).le) <| Nat.zero_le _⟩

Premises used: Iff.mpr, Set.Finite.subset, Set.finite_Icc, Set.range_subset_iff, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
s : Set α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ BddAbove s → s.WellFoundedOn fun (x1 x2 : α) ↦ x1 > x2

Tactic:
fun h => h.dual.wellFoundedOn_lt

Premises used: Set.Mem, setOf, BddBelow.wellFoundedOn_lt, Set.preimage, BddAbove.dual, OrderDual
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
s : Set α
inst : Preorder α
inst_1 : LocallyFiniteOrder α
⊢ BddBelow s → s.IsWF

Tactic:
BddBelow.wellFoundedOn_lt

Premises used: BddBelow.wellFoundedOn_lt, Set.IsWF
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
contrapose! : ∀ (hf : ¬BddAbove (f ⁻¹' s)), ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
⊢ BddAbove (f ⁻¹' s)

Tactic:
contrapose! hf
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ¬BddAbove (f ⁻¹' s)
⊢ ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y

Tactic:
rw [not_bddAbove_iff] at hf

Premises used: not_bddAbove_iff
-- Module: Mathlib.Order.WellFoundedSet
Goal:
α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (x : ℕ), ∃ y ∈ f ⁻¹' s, x < y
obtain : ∀ (φ : ℕ → ℕ) (hφm : StrictMono φ) (hφs : ∀ (n : ℕ), φ n ∈ f ⁻¹' s), ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)
⊢ ∃ (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⟩

Premises used: Exists.casesOn, Nat.exists_strictMono_subsequence
-- Module: Mathlib.Order.WellFoundedSet
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
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)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

Tactic:
rw [partiallyWellOrderedOn_iff_exists_lt] at hs

Premises used: Set.partiallyWellOrderedOn_iff_exists_lt
-- Module: Mathlib.Order.WellFoundedSet
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
obtain : ∀ (m n : ℕ) (hmn : m < n) (hr : r (f (φ m)) (f (φ n))), ∃ (m : ℕ) (n : ℕ), m < n ∧ 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
-- Module: Mathlib.Order.WellFoundedSet
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))
h : φ m < φ n ∧ r (f (φ m)) (f (φ n))
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ r (f m) (f n)

Tactic:
use (φ m), (φ n)
-- Module: Mathlib.Order.WellFoundedSet
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 ∧ r (f (φ m)) (f (φ n))

Tactic:
⟨hφm hmn, hr⟩

Premises used: And.intro
-- Module: Mathlib.Order.WellFoundedSet
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 ∧ r (f (φ m)) (f (φ n))

Tactic:
exact ⟨hφm hmn, hr⟩
-- Module: Mathlib.Order.WellFoundedSet
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)

Tactic:
have := hs.bddAbove_preimage hf
-- Module: Mathlib.Order.WellFoundedSet
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)
contrapose! : ∀ (this : ∀ (k : ℕ), ∃ (m : ℕ), k < m ∧ f m ∈ s), ¬BddAbove (f ⁻¹' s)
⊢ ∃ (k : ℕ), ∀ (m : ℕ), k < m → f m ∉ s

Tactic:
contrapose! this