awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : ℕ → α
inl :
  ∀ (g : ℕ ↪o ℕ) (hr : ∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))),
    ∃ (g : ℕ ↪o ℕ),
      (∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) ∨
        ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
inr :
  ∀ (g : ℕ ↪o ℕ) (hnr : ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))),
    ∃ (g : ℕ ↪o ℕ),
      (∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) ∨
        ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ ∃ (g : ℕ ↪o ℕ),
    (∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) ∨
      ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f

Premises used: exists_increasing_or_nonincreasing_subseq'
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))
⊢ ∃ (g : ℕ ↪o ℕ),
    (∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) ∨
      ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
⟨g, Or.intro_left _ fun m n mn => ?_⟩

Premises used: Or.intro_left, Exists.intro
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))
inl : ∀ (m n : ℕ) (mn : m < n), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ ∃ (g : ℕ ↪o ℕ),
    (∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) ∨
      ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
refine ⟨g, Or.intro_left _ fun m n mn => ?_⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))
m n : ℕ
mn : m < n
inl : ∀ (x : ℕ) (mn : m < m.succ + x), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + x)))
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
obtain ⟨x, rfl⟩ := Nat.exists_eq_add_of_le (Nat.succ_le_iff.2 mn)

Premises used: Iff.mpr, Nat.exists_eq_add_of_le, Nat.succ_le_iff, rfl
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))
m : ℕ
mn : m < m.succ + 0
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + 0)))

Tactic:
apply hr
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))
m x : ℕ
ih : ∀ (mn : m < m.succ + x), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + x)))
mn : m < m.succ + (x + 1)
apply : r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ.add x)))
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + (x + 1))))

Tactic:
apply IsTrans.trans _ _ _ _ (hr _)

Premises used: IsTrans.trans
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))
m x : ℕ
ih : ∀ (mn : m < m.succ + x), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + x)))
mn : m < m.succ + (x + 1)
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ.add x)))

Tactic:
ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))

Premises used: Nat.le_add_right, Nat.lt_succ_self, lt_of_lt_of_le
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))
m x : ℕ
ih : ∀ (mn : m < m.succ + x), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + x)))
mn : m < m.succ + (x + 1)
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ.add x)))

Tactic:
exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))

Premises used: Nat.le_add_right, Nat.lt_succ_self, lt_of_lt_of_le
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hr : ∀ (n : ℕ), r (f ((g : (a : ℕ) → ℕ) n)) (f ((g : (a : ℕ) → ℕ) (n + 1)))
m x : ℕ
mn : m < m.succ + x
inl : ∀ (mn : m < m.succ + 0), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + 0)))
inl₁ :
  ∀ (x : ℕ) (ih : ∀ (mn : m < m.succ + x), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + x))))
    (mn : m < m.succ + (x + 1)), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + (x + 1))))
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + x)))

Tactic:
induction x with
    | zero => apply hr
    | succ x ih =>
      apply IsTrans.trans _ _ _ _ (hr _)
      exact ih (lt_of_lt_of_le m.lt_succ_self (Nat.le_add_right _ _))

Premises used: IsTrans.trans
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hnr : ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ ∃ (g : ℕ ↪o ℕ),
    (∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) ∨
      ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
⟨g, Or.intro_right _ hnr⟩

Premises used: Or.intro_right, Exists.intro
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : ℕ → α
g : ℕ ↪o ℕ
hnr : ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
⊢ ∃ (g : ℕ ↪o ℕ),
    (∀ (m n : ℕ), m < n → r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))) ∨
      ∀ (m n : ℕ), m < n → ¬r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))

Tactic:
exact ⟨g, Or.intro_right _ hnr⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
⊢ WellFoundedGT α ↔
    ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)

Tactic:
⟨fun h a => ?_, fun h => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
refine_1 :
  ∀ (h : WellFoundedGT α) (a : ℕ →o α),
    ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
refine_2 :
  ∀
    (h :
      ∀ (a : ℕ →o α),
        ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)),
    WellFoundedGT α
⊢ WellFoundedGT α ↔
    ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)

Tactic:
refine ⟨fun h a => ?_, fun h => ?_⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedGT α
a : ℕ →o α
refine_1 :
  ∀ (n : ℕ)
    (H : ∀ (x : α), Membership.mem (γ := Set α) (Set.range (ι := ℕ) (⇑a : (a : ℕ) → α)) x → ¬(a : (a : ℕ) → α) n < x),
    ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)

Tactic:
obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.wf.has_min _ (Set.range_nonempty a)

Premises used: IsWellFounded.wf, Set.range_nonempty, WellFounded.has_min, DFunLike.coe, rfl
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedGT α
a : ℕ →o α
n : ℕ
H : ∀ (x : α), Membership.mem (γ := Set α) (Set.range (ι := ℕ) (⇑a : (a : ℕ) → α)) x → ¬(a : (a : ℕ) → α) n < x
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)

Tactic:
⟨n, fun m _ => H _ (Set.mem_range_self _)⟩

Premises used: Set.mem_range_self, Exists.intro, DFunLike.coe
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedGT α
a : ℕ →o α
n : ℕ
H : ∀ (x : α), Membership.mem (γ := Set α) (Set.range (ι := ℕ) (⇑a : (a : ℕ) → α)) x → ¬(a : (a : ℕ) → α) n < x
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)

Tactic:
exact ⟨n, fun m _ => H _ (Set.mem_range_self _)⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
h : ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
refine_2 : IsEmpty.{u_1 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1)
⊢ WellFoundedGT α

Tactic:
rw [WellFoundedGT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]

Premises used: WellFoundedGT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
h : ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
⊢ IsEmpty.{u_1 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1)

Tactic:
⟨fun a => ?_⟩

Premises used: IsEmpty.mk
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
h : ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
refine_2 : ∀ (a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1), False
⊢ IsEmpty.{u_1 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1)

Tactic:
refine ⟨fun a => ?_⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
h : ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
refine_2 :
  ∀ (n : ℕ)
    (hn :
      ∀ (m : ℕ),
        n ≤ m →
          ¬LT.lt (α := α)
              ((a.swap (r := fun (x1 x2 : ℕ) ↦ x1 > x2) (s := fun (x1 x2 : α) ↦ x2 < x1).toRelHom (r :=
                        Function.swap (φ := fun (a a_2 : ℕ) ↦ Prop) fun (x1 x2 : ℕ) ↦ x1 > x2) (s :=
                        Function.swap (φ := fun (a a_2 : α) ↦ Prop) fun (x1 x2 : α) ↦ x2 < x1).toOrderHom :
                    (a : ℕ) → α)
                  n :
                α)
              ((a.swap (r := fun (x1 x2 : ℕ) ↦ x1 > x2) (s := fun (x1 x2 : α) ↦ x2 < x1).toRelHom (r :=
                        Function.swap (φ := fun (a a_2 : ℕ) ↦ Prop) fun (x1 x2 : ℕ) ↦ x1 > x2) (s :=
                        Function.swap (φ := fun (a a_2 : α) ↦ Prop) fun (x1 x2 : α) ↦ x2 < x1).toOrderHom :
                    (a : ℕ) → α)
                  m :
                α)),
    False
⊢ False

Tactic:
obtain ⟨n, hn⟩ := h (a.swap : _ →r _).toOrderHom

Premises used: RelHom.toOrderHom
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
h : ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      ¬LT.lt (α := α)
          ((a.swap (r := fun (x1 x2 : ℕ) ↦ x1 > x2) (s := fun (x1 x2 : α) ↦ x2 < x1).toRelHom (r :=
                    Function.swap (φ := fun (a a_2 : ℕ) ↦ Prop) fun (x1 x2 : ℕ) ↦ x1 > x2) (s :=
                    Function.swap (φ := fun (a a_2 : α) ↦ Prop) fun (x1 x2 : α) ↦ x2 < x1).toOrderHom :
                (a : ℕ) → α)
              n :
            α)
          ((a.swap (r := fun (x1 x2 : ℕ) ↦ x1 > x2) (s := fun (x1 x2 : α) ↦ x2 < x1).toRelHom (r :=
                    Function.swap (φ := fun (a a_2 : ℕ) ↦ Prop) fun (x1 x2 : ℕ) ↦ x1 > x2) (s :=
                    Function.swap (φ := fun (a a_2 : α) ↦ Prop) fun (x1 x2 : α) ↦ x2 < x1).toOrderHom :
                (a : ℕ) → α)
              m :
            α)
⊢ False

Tactic:
hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self)

Premises used: Iff.mpr, Nat.lt_succ_self, LT.lt.le, RelEmbedding.map_rel_iff, Nat.succ
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
h : ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1
n : ℕ
hn :
  ∀ (m : ℕ),
    n ≤ m →
      ¬LT.lt (α := α)
          ((a.swap (r := fun (x1 x2 : ℕ) ↦ x1 > x2) (s := fun (x1 x2 : α) ↦ x2 < x1).toRelHom (r :=
                    Function.swap (φ := fun (a a_2 : ℕ) ↦ Prop) fun (x1 x2 : ℕ) ↦ x1 > x2) (s :=
                    Function.swap (φ := fun (a a_2 : α) ↦ Prop) fun (x1 x2 : α) ↦ x2 < x1).toOrderHom :
                (a : ℕ) → α)
              n :
            α)
          ((a.swap (r := fun (x1 x2 : ℕ) ↦ x1 > x2) (s := fun (x1 x2 : α) ↦ x2 < x1).toRelHom (r :=
                    Function.swap (φ := fun (a a_2 : ℕ) ↦ Prop) fun (x1 x2 : ℕ) ↦ x1 > x2) (s :=
                    Function.swap (φ := fun (a a_2 : α) ↦ Prop) fun (x1 x2 : α) ↦ x2 < x1).toOrderHom :
                (a : ℕ) → α)
              m :
            α)
⊢ False

Tactic:
exact hn n.succ n.lt_succ_self.le ((RelEmbedding.map_rel_iff _).2 n.lt_succ_self)

Premises used: Iff.mpr, Nat.lt_succ_self, LT.lt.le, RelEmbedding.map_rel_iff, Nat.succ
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedGT α
a : ℕ →o α
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)

Tactic:
wellFoundedGT_iff_monotone_chain_condition'.1 h a

Premises used: Iff.mp, wellFoundedGT_iff_monotone_chain_condition'
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : PartialOrder α
a :
  ∀ (a : ℕ →o α) (n m : ℕ) (h : n ≤ m),
    ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α) ↔
      Eq (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
⊢ (∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)) ↔
    ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → Eq (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)

Tactic:
congrm ∀ a, ∃ n, ∀ m h, ?_
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : PartialOrder α
a : ℕ →o α
n m : ℕ
h : n ≤ m
a₁ :
  ¬(LE.le (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α) ∧
        Ne (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)) ↔
    Eq (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
⊢ ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α) ↔
    Eq (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)

Tactic:
rw [lt_iff_le_and_ne]

Premises used: lt_iff_le_and_ne
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : PartialOrder α
a : ℕ →o α
n m : ℕ
h : n ≤ m
⊢ ¬(LE.le (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α) ∧
        Ne (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)) ↔
    Eq (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)

Tactic:
simp [a.mono h]

Premises used: OrderHom.mono
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : PartialOrder α
h : WellFoundedGT α
a : ℕ →o α
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → Eq (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)

Tactic:
wellFoundedGT_iff_monotone_chain_condition.1 h a

Premises used: wellFoundedGT_iff_monotone_chain_condition, Iff.mp
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : WellFoundedLT α
f : ℕ → α
hf : Antitone f
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f n = f m

Tactic:
WellFoundedGT.monotone_chain_condition ⟨OrderDual.toDual ∘ f, hf⟩

Premises used: OrderDual.toDual, WellFoundedGT.monotone_chain_condition, Function.comp, OrderHom.mk, OrderDual, DFunLike.coe
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : WellFoundedGT α
a : ℕ →o α
m : ℕ
inl : ∀ (hm : m ≤ monotonicSequenceLimitIndex a), (a : (a : ℕ) → α) m ≤ monotonicSequenceLimit a
inr : ∀ (hm : monotonicSequenceLimitIndex a < m), (a : (a : ℕ) → α) m ≤ monotonicSequenceLimit a
⊢ (a : (a : ℕ) → α) m ≤ monotonicSequenceLimit a

Tactic:
rcases le_or_gt m (monotonicSequenceLimitIndex a) with hm | hm

Premises used: monotonicSequenceLimitIndex, le_or_gt
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : m ≤ monotonicSequenceLimitIndex a
⊢ (a : (a : ℕ) → α) m ≤ monotonicSequenceLimit a

Tactic:
a.monotone hm

Premises used: OrderHom.monotone, monotonicSequenceLimit
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : m ≤ monotonicSequenceLimitIndex a
⊢ (a : (a : ℕ) → α) m ≤ monotonicSequenceLimit a

Tactic:
exact a.monotone hm

Premises used: OrderHom.monotone
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → Eq (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)

Tactic:
obtain h := WellFoundedGT.monotone_chain_condition a

Premises used: WellFoundedGT.monotone_chain_condition
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
h : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → Eq (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
⊢ (a : (a : ℕ) → α) m ≤ monotonicSequenceLimit a

Tactic:
(Nat.sInf_mem (s := {n | ∀ m, n ≤ m → a n = a m}) h m hm.le).ge

Premises used: Eq.ge, Nat.sInf_mem, monotonicSequenceLimitIndex, LT.lt.le, monotonicSequenceLimit
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
h : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → Eq (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
⊢ (a : (a : ℕ) → α) m ≤ monotonicSequenceLimit a

Tactic:
exact (Nat.sInf_mem (s := {n | ∀ m, n ≤ m → a n = a m}) h m hm.le).ge

Premises used: Eq.ge, Nat.sInf_mem, LT.lt.le
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : CompleteLattice α
inst_1 : WellFoundedGT α
a : ℕ →o α
⊢ iSup (ι := ℕ) (⇑a : (a : ℕ) → α) = monotonicSequenceLimit a

Tactic:
(iSup_le (le_monotonicSequenceLimit a)).antisymm (le_iSup a _)

Premises used: LE.le.antisymm, le_iSup, le_monotonicSequenceLimit, iSup_le, DFunLike.coe
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
inst : ConditionallyCompleteLattice α
inst_1 : WellFoundedGT α
a : ℕ →o α
ha : BddAbove (α := α) (Set.range (ι := ℕ) (⇑a : (a : ℕ) → α))
⊢ iSup (ι := ℕ) (⇑a : (a : ℕ) → α) = monotonicSequenceLimit a

Tactic:
(ciSup_le (le_monotonicSequenceLimit a)).antisymm (le_ciSup ha _)

Premises used: LE.le.antisymm, le_monotonicSequenceLimit, le_ciSup, ciSup_le
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
choose :
  ∀ (next : ⦃a : α⦄ → (h : ¬IsMax a) → α) (hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h),
    ∃ (a : ℕ → α), IsMin (a 0) ∧ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
⊢ ∃ (a : ℕ → α), IsMin (a 0) ∧ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
choose next hnext using exists_covBy_of_wellFoundedLT (α := α)

Premises used: exists_covBy_of_wellFoundedLT
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
⊢ Set.Nonempty.{u_2} (α := α) Set.univ

Tactic:
have hα := Set.nonempty_iff_univ_nonempty.mp ‹_›
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
a : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t
⊢ ∃ (a : ℕ → α), IsMin (a 0) ∧ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ (Set.mem_univ _), ?_⟩

Premises used: Iff.mpr, Set.univ, IsWellFounded.wf, And.intro, isMin_iff_forall_not_lt, Exists.intro, Set.mem_univ, WellFounded.not_lt_min
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
a : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t
refine : ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
⊢ ∃ (a : ℕ → α), IsMin (a 0) ∧ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)

Tactic:
refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ (Set.mem_univ _), ?_⟩
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
a : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t
n : ℕ
hn : ¬IsMax (a n)
change : a n ⋖ if ha : IsMax (a n) then a n else next ha
⊢ a n ⋖ a (n + 1)

Tactic:
change a n ⋖ if ha : IsMax (a n) then a n else _

Premises used: IsMax
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
a : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t
n : ℕ
hn : ¬IsMax (a n)
rw : a n ⋖ next hn
⊢ a n ⋖ if ha : IsMax (a n) then a n else next ha

Tactic:
rw [dif_neg hn]

Premises used: dif_neg
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
a : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t
n : ℕ
hn : ¬IsMax (a n)
⊢ a n ⋖ next hn

Tactic:
hnext hn
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
a : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t
n : ℕ
hn : ¬IsMax (a n)
⊢ a n ⋖ next hn

Tactic:
exact hnext hn
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
next : ⦃a : α⦄ → (h : ¬IsMax a) → α
hnext : ∀ ⦃a : α⦄ (h : ¬IsMax a), a ⋖ next h
hα : Set.Nonempty.{u_2} (α := α) Set.univ
a : ℕ → α :=
  fun (t : ℕ) ↦
    Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) ⋯ Set.univ hα)
      (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t
⊢ ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)

Tactic:
have cov n (hn : ¬ IsMax (a n)) : a n ⋖ a (n + 1) := by
    change a n ⋖ if ha : IsMax (a n) then a n else _
    rw [dif_neg hn]
    exact hnext hn