awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsStrictOrder α r
f : ℕ → α
H : ∀ (n : ℕ), r (f (n + 1)) (f n)
⊢ (⇑(natGT (r := r) f H) : (a : ℕ) → α) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsStrictOrder α r
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
k : ℕ
rw :
  Nonempty.{u_1 + 1}
    { f_1 : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r //
      Membership.mem (α := α) (γ := Set α) (Set.range (ι := ℕ) (⇑f_1 : (a : ℕ) → α)) ((f : (a : ℕ) → α) k : α) }
⊢ ¬Acc r ((f : (a : ℕ) → α) k)

Tactic:
rw [acc_iff_isEmpty_subtype_mem_range, not_isEmpty_iff]

Premises used: RelEmbedding.acc_iff_isEmpty_subtype_mem_range, not_isEmpty_iff
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsStrictOrder α r
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
k : ℕ
⊢ Nonempty.{u_1 + 1}
    { f_1 : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r //
      Membership.mem (α := α) (γ := Set α) (Set.range (ι := ℕ) (⇑f_1 : (a : ℕ) → α)) ((f : (a : ℕ) → α) k : α) }

Tactic:
⟨⟨f, k, rfl⟩⟩

Premises used: Nonempty.intro, Subtype.mk, Exists.intro, rfl
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsStrictOrder α r
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
k : ℕ
⊢ Nonempty.{u_1 + 1}
    { f_1 : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r //
      Membership.mem (α := α) (γ := Set α) (Set.range (ι := ℕ) (⇑f_1 : (a : ℕ) → α)) ((f : (a : ℕ) → α) k : α) }

Tactic:
exact ⟨⟨f, k, rfl⟩⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsStrictOrder α r
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
rw : Nonempty.{u_1 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r)
⊢ ¬WellFounded r

Tactic:
rw [wellFounded_iff_isEmpty, not_isEmpty_iff]

Premises used: not_isEmpty_iff, RelEmbedding.wellFounded_iff_isEmpty
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsStrictOrder α r
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
⊢ Nonempty.{u_1 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r)

Tactic:
⟨f⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsStrictOrder α r
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
⊢ Nonempty.{u_1 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r)

Tactic:
exact ⟨f⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedLT α
f : ℕ → α
hf : StrictAnti f
n : ℕ
⊢ n < n + 1

Tactic:
simp
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
inst_1 : WellFoundedGT α
f : ℕ → α
⊢ ¬StrictMono f

Tactic:
not_strictAnti_of_wellFoundedLT (α := αᵒᵈ) f

Premises used: StrictMono, not_strictAnti_of_wellFoundedLT
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
s : Set ℕ
inst : Infinite (↑s : Type)
⊢ ℕ ≃o (↑s : Type)

Tactic:
exact
    RelIso.ofSurjective
      (RelEmbedding.orderEmbeddingOfLTEmbedding
        (RelEmbedding.natLT (Nat.Subtype.ofNat s) fun n => Nat.Subtype.lt_succ_self _))
      Nat.Subtype.ofNat_surjective

Premises used: RelEmbedding.natLT, Nat.Subtype.lt_succ_self, Nat.Subtype.ofNat, RelEmbedding.orderEmbeddingOfLTEmbedding, RelIso.ofSurjective, Nat.Subtype.ofNat_surjective
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
s : Set ℕ
inst : Infinite (↑s : Type)
⊢ ℕ ≃o (↑s : Type)

Tactic:
classical
  exact
    RelIso.ofSurjective
      (RelEmbedding.orderEmbeddingOfLTEmbedding
        (RelEmbedding.natLT (Nat.Subtype.ofNat s) fun n => Nat.Subtype.lt_succ_self _))
      Nat.Subtype.ofNat_surjective
-- Module: Mathlib.Order.OrderIsoNat
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
⊢ (⇑(orderEmbeddingOfSet s) : (a : ℕ) → ℕ) = Subtype.val (p := fun (x : ℕ) ↦ x ∈ s) ∘ Subtype.ofNat s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrderIsoNat
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
⊢ (orderEmbeddingOfSet s : (a : ℕ) → ℕ) n = (↑(Subtype.ofNat s n) : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrderIsoNat
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
dP : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
simp : ofNat s n = ofNat s n
⊢ (orderIsoOfNat s : (a : ℕ) → (↑s : Type)) n = ofNat s n

Tactic:
simp only [orderIsoOfNat, RelIso.ofSurjective_apply,
    RelEmbedding.orderEmbeddingOfLTEmbedding_apply, RelEmbedding.coe_natLT]

Premises used: Nat.Subtype.orderIsoOfNat, RelIso.ofSurjective_apply, RelEmbedding.coe_natLT, RelEmbedding.orderEmbeddingOfLTEmbedding_apply
-- Module: Mathlib.Order.OrderIsoNat
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
dP : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
⊢ ofNat s n = ofNat s n

Tactic:
congr!
-- Module: Mathlib.Order.OrderIsoNat
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
inst_1 : DecidablePred fun (x : ℕ) ↦ x ∈ s
⊢ Set.range (ι := ℕ) (⇑(orderEmbeddingOfSet s) : (a : ℕ) → ℕ) = s

Tactic:
Subtype.coe_comp_ofNat_range

Premises used: Nat.Subtype.coe_comp_ofNat_range
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ Infinite (↑(e ⁻¹' s) : Type) ∨ Infinite (↑(e ⁻¹' t) : Type)

Tactic:
simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
        Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]

Premises used: Iff.mpr, Set.infinite_coe_iff, Set.preimage_union, Set.eq_univ_of_forall, Set.infinite_univ, Set.infinite_union, Set.mem_preimage
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ Infinite (↑(e ⁻¹' s) : Type) ∨ Infinite (↑(e ⁻¹' t) : Type)

Tactic:
have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
      simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
        Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
this : Infinite (↑(e ⁻¹' s) : Type) ∨ Infinite (↑(e ⁻¹' t) : Type)
inl :
  Infinite (↑(e ⁻¹' s) : Type) →
    ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
inr :
  Infinite (↑(e ⁻¹' t) : Type) →
    ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
⊢ ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t

Tactic:
cases this
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h : Infinite (↑(e ⁻¹' s) : Type)
⊢ ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t

Tactic:
⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩

Premises used: Nat.Subtype.ofNat, Set.preimage, Exists.intro, Nat.orderEmbeddingOfSet, Or.inl, Subtype.property
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h : Infinite (↑(e ⁻¹' t) : Type)
⊢ ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t

Tactic:
⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩

Premises used: Nat.Subtype.ofNat, Set.preimage, Exists.intro, Nat.orderEmbeddingOfSet, Or.inr, Subtype.property
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
h : Infinite (↑(e ⁻¹' s) : Type)
⊢ ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t

Tactic:
exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
      ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
have : Infinite (↑(e ⁻¹' s) : Type) ∨ Infinite (↑(e ⁻¹' t) : Type)
have₁ :
  ∀ (this : Infinite (↑(e ⁻¹' s) : Type) ∨ Infinite (↑(e ⁻¹' t) : Type)),
    ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
have₂ : Infinite (↑(e ⁻¹' s) : Type) ∨ Infinite (↑(e ⁻¹' t) : Type)
have₃ have₄ :
  ∀ (this : Infinite (↑(e ⁻¹' s) : Type) ∨ Infinite (↑(e ⁻¹' t) : Type)),
    ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
inl :
  Infinite (↑(e ⁻¹' s) : Type) →
    ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
inr :
  Infinite (↑(e ⁻¹' t) : Type) →
    ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
⊢ ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t

Tactic:
classical
    have : Infinite (e ⁻¹' s) ∨ Infinite (e ⁻¹' t) := by
      simp only [Set.infinite_coe_iff, ← Set.infinite_union, ← Set.preimage_union,
        Set.eq_univ_of_forall fun n => Set.mem_preimage.2 (he n), Set.infinite_univ]
    cases this
    exacts [⟨Nat.orderEmbeddingOfSet (e ⁻¹' s), Or.inl fun n => (Nat.Subtype.ofNat (e ⁻¹' s) _).2⟩,
      ⟨Nat.orderEmbeddingOfSet (e ⁻¹' t), Or.inr fun n => (Nat.Subtype.ofNat (e ⁻¹' t) _).2⟩]
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
pos :
  ∀ (hbad : Infinite (↑bad : Type)),
    ∃ (g : ℕ ↪o ℕ),
      (∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))) ∨
        ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
neg :
  ∀ (hbad : ¬Infinite (↑bad : Type)),
    ∃ (g : ℕ ↪o ℕ),
      (∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))) ∨
        ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ ∃ (g : ℕ ↪o ℕ),
    (∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))) ∨
      ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
by_cases hbad : Infinite bad

Premises used: Set.Elem, Infinite
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite (↑bad : Type)
⊢ ∃ (g : ℕ ↪o ℕ),
    (∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))) ∨
      ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => ?_⟩

Premises used: Or.intro_right, Exists.intro, Nat.orderEmbeddingOfSet
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite (↑bad : Type)
pos :
  ∀ (m n : ℕ) (mn : m < n),
    ¬r (f ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) m)) (f ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) n))
⊢ ∃ (g : ℕ ↪o ℕ),
    (∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))) ∨
      ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
refine ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => ?_⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite (↑bad : Type)
m n : ℕ
mn : m < n
⊢ Membership.mem (α := ℕ) (γ := Set ℕ) (Set.range (ι := ℕ) (⇑(Nat.orderEmbeddingOfSet bad) : (a : ℕ) → ℕ))
    ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) m : ℕ)

Tactic:
have h := @Set.mem_range_self _ _ ↑(Nat.orderEmbeddingOfSet bad) m
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite (↑bad : Type)
m n : ℕ
mn : m < n
h :
  Membership.mem (α := ℕ) (γ := Set ℕ) (Set.range (ι := ℕ) (⇑(Nat.orderEmbeddingOfSet bad) : (a : ℕ) → ℕ))
    ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) m : ℕ)
⊢ Membership.mem (α := ℕ) bad ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) m : ℕ)

Tactic:
rw [Nat.orderEmbeddingOfSet_range bad] at h

Premises used: Nat.orderEmbeddingOfSet_range
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite (↑bad : Type)
m n : ℕ
mn : m < n
h : Membership.mem (α := ℕ) bad ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) m : ℕ)
⊢ ¬r (f ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) m)) (f ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) n))

Tactic:
h _ ((OrderEmbedding.lt_iff_lt _).2 mn)

Premises used: Iff.mpr, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : Infinite (↑bad : Type)
m n : ℕ
mn : m < n
h : Membership.mem (α := ℕ) bad ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) m : ℕ)
⊢ ¬r (f ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) m)) (f ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) n))

Tactic:
exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)

Premises used: Iff.mpr, OrderEmbedding.lt_iff_lt
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : ¬Infinite (↑bad : Type)
⊢ bad.Finite

Tactic:
rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad

Premises used: Classical.not_not, Set.infinite_coe_iff, Set.Infinite
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
pos : ∀ (he : hbad.toFinset (s := bad).Nonempty), ∃ (m : ℕ), ∀ (n : ℕ), m ≤ n → n ∉ bad
neg : ∀ (he : ¬hbad.toFinset (s := bad).Nonempty), ∃ (m : ℕ), ∀ (n : ℕ), m ≤ n → n ∉ bad
⊢ ∃ (m : ℕ), ∀ (n : ℕ), m ≤ n → n ∉ bad

Tactic:
by_cases he : hbad.toFinset.Nonempty

Premises used: Set.Finite.toFinset, Finset.Nonempty
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
he : hbad.toFinset (s := bad).Nonempty
⊢ ∃ (m : ℕ), ∀ (n : ℕ), m ≤ n → n ∉ bad

Tactic:
⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
              Nat.not_succ_le_self _
                (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩

Premises used: Iff.mpr, Set.Finite.mem_toFinset, Finset.max', Finset.le_max', Set.Finite.toFinset, Exists.intro, LE.le.trans, Nat.succ, Nat.not_succ_le_self
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
he : hbad.toFinset (s := bad).Nonempty
⊢ ∃ (m : ℕ), ∀ (n : ℕ), m ≤ n → n ∉ bad

Tactic:
refine
            ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
              Nat.not_succ_le_self _
                (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
he : ¬hbad.toFinset (s := bad).Nonempty
⊢ ∃ (m : ℕ), ∀ (n : ℕ), m ≤ n → n ∉ bad

Tactic:
⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩

Premises used: Iff.mpr, Set.Finite.mem_toFinset, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
he : ¬hbad.toFinset (s := bad).Nonempty
⊢ ∃ (m : ℕ), ∀ (n : ℕ), m ≤ n → n ∉ bad

Tactic:
exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
neg :
  ∀ (m : ℕ) (hm : ∀ (n : ℕ), m ≤ n → n ∉ bad),
    ∃ (g : ℕ ↪o ℕ),
      (∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))) ∨
        ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ ∃ (g : ℕ ↪o ℕ),
    (∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))) ∨
      ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → n ∉ bad := by
        by_cases he : hbad.toFinset.Nonempty
        · refine
            ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
              Nat.not_succ_le_self _
                (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
        · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n : ℕ
⊢ n + m ∉ bad

Tactic:
have h := hm _ (Nat.le_add_left m n)
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n : ℕ
h : n + m ∉ bad
⊢ ∃ (x : ℕ), n + m < x ∧ r (f (n + m)) (f x)

Tactic:
simp only [bad, exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h

Premises used: Classical.not_not, Set.mem_setOf_eq, exists_prop, Classical.not_forall
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n : ℕ
h : ∃ (x : ℕ), n + m < x ∧ r (f (n + m)) (f x)
obtain : ∀ (n' : ℕ) (hn1 : n + m < n') (hn2 : r (f (n + m)) (f n')), ∃ (n' : ℕ), n < n' ∧ r (f (n + m)) (f (n' + m))
⊢ ∃ (n' : ℕ), n < n' ∧ r (f (n + m)) (f (n' + m))

Tactic:
obtain ⟨n', hn1, hn2⟩ := h
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
⊢ n < n + n' - n - m

Tactic:
lia
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
refine : r (f (n + m)) (f (n + n' - n - m + m))
⊢ ∃ (n' : ℕ), n < n' ∧ r (f (n + m)) (f (n' + m))

Tactic:
refine ⟨n + n' - n - m, by lia, ?_⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
⊢ r (f (n + m)) (f n')

Tactic:
hn2
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
h : n + n' - n - m + m = n'
⊢ r (f (n + m)) (f (n + n' - n - m + m))

Tactic:
convert! hn2
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
n n' : ℕ
hn1 : n + m < n'
hn2 : r (f (n + m)) (f n')
⊢ n + n' - n - m + m = n'

Tactic:
lia
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
⊢ ∀ (n : ℕ), ∃ (n' : ℕ), n < n' ∧ r (f (n + m)) (f (n' + m))

Tactic:
have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) := by
        intro n
        have h := hm _ (Nat.le_add_left m n)
        simp only [bad, exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h
        obtain ⟨n', hn1, hn2⟩ := h
        refine ⟨n + n' - n - m, by lia, ?_⟩
        convert! hn2
        lia
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
h : ∀ (n : ℕ), ∃ (n' : ℕ), n < n' ∧ r (f (n + m)) (f (n' + m))
g' : ℕ → ℕ :=
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) m fun (n : ℕ) (gn : (fun (x : ℕ) ↦ ℕ) n) ↦
    Nat.find (p := fun (n : ℕ) ↦ gn < n ∧ r (f (gn + m)) (f (n + m))) ⋯
⊢ ∃ (g : ℕ ↪o ℕ),
    (∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))) ∨
      ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
              Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding,
          Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩

Premises used: RelEmbedding.natLT, Or.intro_left, And.right, And.left, HAdd.hAdd, RelEmbedding.orderEmbeddingOfLTEmbedding, Exists.intro, Nat.add_lt_add_right, Nat.find_spec
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
m : ℕ
hm : ∀ (n : ℕ), m ≤ n → n ∉ bad
h : ∀ (n : ℕ), ∃ (n' : ℕ), n < n' ∧ r (f (n + m)) (f (n' + m))
g' : ℕ → ℕ :=
  Nat.rec (motive := fun (x : ℕ) ↦ ℕ) m fun (n : ℕ) (gn : (fun (x : ℕ) ↦ ℕ) n) ↦
    Nat.find (p := fun (n : ℕ) ↦ gn < n ∧ r (f (gn + m)) (f (n + m))) ⋯
⊢ ∃ (g : ℕ ↪o ℕ),
    (∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))) ∨
      ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
exact
        ⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
              Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding,
          Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
let let₁ let₂ :
  ∃ (g : ℕ ↪o ℕ),
    (∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))) ∨
      ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
pos :
  let bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)};
  ∀ (hbad : Infinite (↑bad : Type)),
    ∃ (g : ℕ ↪o ℕ),
      (∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))) ∨
        ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
neg neg₁ :
  let bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)};
  ∀ (hbad : ¬Infinite (↑bad : Type)),
    ∃ (g : ℕ ↪o ℕ),
      (∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))) ∨
        ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ ∃ (g : ℕ ↪o ℕ),
    (∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))) ∨
      ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
classical
    let bad : Set ℕ := { m | ∀ n, m < n → ¬r (f m) (f n) }
    by_cases hbad : Infinite bad
    · refine ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => ?_⟩
      have h := @Set.mem_range_self _ _ ↑(Nat.orderEmbeddingOfSet bad) m
      rw [Nat.orderEmbeddingOfSet_range bad] at h
      exact h _ ((OrderEmbedding.lt_iff_lt _).2 mn)
    · rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad
      obtain ⟨m, hm⟩ : ∃ m, ∀ n, m ≤ n → n ∉ bad := by
        by_cases he : hbad.toFinset.Nonempty
        · refine
            ⟨(hbad.toFinset.max' he).succ, fun n hn nbad =>
              Nat.not_succ_le_self _
                (hn.trans (hbad.toFinset.le_max' n (hbad.mem_toFinset.2 nbad)))⟩
        · exact ⟨0, fun n _ nbad => he ⟨n, hbad.mem_toFinset.2 nbad⟩⟩
      have h : ∀ n : ℕ, ∃ n' : ℕ, n < n' ∧ r (f (n + m)) (f (n' + m)) := by
        intro n
        have h := hm _ (Nat.le_add_left m n)
        simp only [bad, exists_prop, not_not, Set.mem_setOf_eq, not_forall] at h
        obtain ⟨n', hn1, hn2⟩ := h
        refine ⟨n + n' - n - m, by lia, ?_⟩
        convert! hn2
        lia
      let g' : ℕ → ℕ := @Nat.rec (fun _ => ℕ) m fun n gn => Nat.find (h gn)
      exact
        ⟨(RelEmbedding.natLT (fun n => g' n + m) fun n =>
              Nat.add_lt_add_right (Nat.find_spec (h (g' n))).1 m).orderEmbeddingOfLTEmbedding,
          Or.intro_left _ fun n => (Nat.find_spec (h (g' n))).2⟩

Premises used: Classical.not_not, Set.infinite_coe_iff, Set.Infinite