awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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))
have inl : ∀ (m n : ℕ) (mn : m < n), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
Tactic: refine ⟨g, Or.intro_left _ fun m n mn => ?_⟩
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) n))
have inl : ∀ (x : ℕ) (mn : m < m.succ + x), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + x)))
Tactic: obtain ⟨x, rfl⟩ := Nat.exists_eq_add_of_le (Nat.succ_le_iff.2 mn)
Cleared hypotheses: n, mn
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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 + (x + 1))))
have apply : r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ.add x)))
Tactic: apply IsTrans.trans _ _ _ _ (hr _)
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + x)))
have inl : ∀ (mn : m < m.succ + 0), r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + 0)))
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 _ _))
Cleared hypotheses: x, mn
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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)))
⊢ r (f ((g : (a : ℕ) → ℕ) m)) (f ((g : (a : ℕ) → ℕ) (m.succ + x)))
have 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))))
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 _ _))
Cleared hypotheses: x, mn
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ WellFoundedGT α ↔
    ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
have refine_1 : ∀ (h : WellFoundedGT α) (a : ℕ →o α),
  ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
Tactic: refine ⟨fun h a => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
inst : Preorder α
refine_1 :
  ∀ (h : WellFoundedGT α) (a : ℕ →o α),
    ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
⊢ WellFoundedGT α ↔
    ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
have refine_2 : ∀
  (h :
    ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)),
  WellFoundedGT α
Tactic: refine ⟨fun h a => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedGT α
a : ℕ →o α
⊢ ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
have 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 : α)
Tactic: obtain ⟨x, ⟨n, rfl⟩, H⟩ := h.wf.has_min _ (Set.range_nonempty a)
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
inst : Preorder α
h : ∀ (a : ℕ →o α), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
⊢ WellFoundedGT α
have refine_2 : IsEmpty.{u_1 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1)
Tactic: rw [WellFoundedGT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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)
have refine_2 : ∀ (a : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x2 < x1), False
Tactic: refine ⟨fun a => ?_⟩
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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
⊢ False
have 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
Tactic: obtain ⟨n, hn⟩ := h (a.swap : _ →r _).toOrderHom
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
inst : PartialOrder α
⊢ (∀ (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 : α)
have a : ∀ (a : ℕ →o α) (n m : ℕ) (h : n ≤ m),
  ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α) ↔
    Eq (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
Tactic: congrm ∀ a, ∃ n, ∀ m h, ?_
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
inst : PartialOrder α
a : ℕ →o α
n m : ℕ
h : n ≤ m
⊢ ¬LT.lt (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α) ↔
    Eq (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
have a₁ : ¬(LE.le (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α) ∧
      Ne (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)) ↔
  Eq (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
Tactic: rw [lt_iff_le_and_ne]
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : WellFoundedGT α
a : ℕ →o α
m : ℕ
⊢ (a : (a : ℕ) → α) m ≤ monotonicSequenceLimit a
have inl : ∀ (hm : m ≤ monotonicSequenceLimitIndex a), (a : (a : ℕ) → α) m ≤ monotonicSequenceLimit a
Tactic: rcases le_or_gt m (monotonicSequenceLimitIndex a) with hm | hm
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : WellFoundedGT α
a : ℕ →o α
m : ℕ
inl : ∀ (hm : m ≤ monotonicSequenceLimitIndex a), (a : (a : ℕ) → α) m ≤ monotonicSequenceLimit a
⊢ (a : (a : ℕ) → α) m ≤ monotonicSequenceLimit a
have inr : ∀ (hm : monotonicSequenceLimitIndex a < m), (a : (a : ℕ) → α) m ≤ monotonicSequenceLimit a
Tactic: rcases le_or_gt m (monotonicSequenceLimitIndex a) with hm | hm
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (hypothesis)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : WellFoundedGT α
a : ℕ →o α
m : ℕ
hm : monotonicSequenceLimitIndex a < m
⊢ (a : (a : ℕ) → α) m ≤ monotonicSequenceLimit a
have h : ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → Eq (α := α) ((a : (a : ℕ) → α) n : α) ((a : (a : ℕ) → α) m : α)
Tactic: obtain h := WellFoundedGT.monotone_chain_condition a
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_2
inst : Preorder α
inst_1 : Nonempty α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
⊢ ∃ (a : ℕ → α), IsMin (a 0) ∧ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
have 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)
Tactic: choose next hnext using exists_covBy_of_wellFoundedLT (α := α)
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (hypothesis)
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
⊢ ∃ (a : ℕ → α), IsMin (a 0) ∧ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
have hα : Set.Nonempty.{u_2} (α := α) Set.univ
Tactic: have hα := Set.nonempty_iff_univ_nonempty.mp ‹_›
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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)
have refine : ∃ (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 _), ?_⟩
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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 ⋖ if ha : IsMax (a n) then a n else next ha
have rw : a n ⋖ next hn
Tactic: rw [dif_neg hn]
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (hypothesis)
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 : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
have cov : ∀ (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
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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
cov : ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)
⊢ ∃ (n : ℕ), IsMax (a n)
have by_contra! : ∀ (this : ∀ (n : ℕ), ¬IsMax (a n)), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (hypothesis)
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
cov : ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)
⊢ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
have H : ∃ (n : ℕ), IsMax (a n)
Tactic: have H : ∃ n, IsMax (a n) := by
    by_contra!
    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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
let let₁ let₂ : ∃ (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)
have let₃ : let a : ℕ → α := fun (t : ℕ) ↦
  Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) sorry Set.univ hα)
    (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t;
∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
Tactic: classical
  let a : ℕ → α := Nat.rec (wfl.wf.min _ hα) fun _n a ↦ if ha : IsMax a then a else next ha
  refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ (Set.mem_univ _), ?_⟩
  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
  have H : ∃ n, IsMax (a n) := by
    by_contra!
    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf
  exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ (wellFounded_lt.not_lt_min _ · h)⟩
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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
let let₁ let₂ : ∃ (a : ℕ → α), IsMin (a 0) ∧ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
let₃ :
  let 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 : ℕ), 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)
have let₄ : let a : ℕ → α := fun (t : ℕ) ↦
  Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) sorry Set.univ hα)
    (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t;
∀ (cov : ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)), ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
Tactic: classical
  let a : ℕ → α := Nat.rec (wfl.wf.min _ hα) fun _n a ↦ if ha : IsMax a then a else next ha
  refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ (Set.mem_univ _), ?_⟩
  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
  have H : ∃ n, IsMax (a n) := by
    by_contra!
    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf
  exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ (wellFounded_lt.not_lt_min _ · h)⟩
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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
let let₁ let₂ : ∃ (a : ℕ → α), IsMin (a 0) ∧ ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
let₃ :
  let 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 : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
let₄ :
  let 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;
  ∀ (cov : ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)), ∃ (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)
have let₅ : let a : ℕ → α := fun (t : ℕ) ↦
  Nat.rec (motive := fun (x : ℕ) ↦ α) (WellFounded.min (r := fun (x1 x2 : α) ↦ x1 < x2) sorry Set.univ hα)
    (fun (_n : ℕ) (a : α) ↦ if ha : IsMax a then a else next ha) t;
∀ (cov : ∀ (n : ℕ) (hn : ¬IsMax (a n)), a n ⋖ a (n + 1)) (H : ∃ (n : ℕ), IsMax (a n)),
  ∃ (n : ℕ), IsMax (a n) ∧ ∀ i < n, a i ⋖ a (i + 1)
Tactic: classical
  let a : ℕ → α := Nat.rec (wfl.wf.min _ hα) fun _n a ↦ if ha : IsMax a then a else next ha
  refine ⟨a, isMin_iff_forall_not_lt.mpr fun _ ↦ wfl.wf.not_lt_min _ (Set.mem_univ _), ?_⟩
  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
  have H : ∃ n, IsMax (a n) := by
    by_contra!
    exact (RelEmbedding.natGT a fun n ↦ (cov n (this n)).1).not_wellFounded wfg.wf
  exact ⟨_, wellFounded_lt.min_mem _ H, fun i h ↦ cov _ (wellFounded_lt.not_lt_min _ · h)⟩
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_2
inst : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
S : Set α := Set.Icc x y
hS : BoundedOrder (↑S : Type u_2) := { top := ⟨y, ⋯⟩, le_top := ⋯, bot := ⟨x, ⋯⟩, bot_le := ⋯ }
⊢ ∃ (a : ℕ → α), a 0 = x ∧ ∃ (n : ℕ), a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)
have obtain : ∀ (a : ℕ → (↑S : Type u_2)) (h₁ : IsMin (a 0)) (n : ℕ) (h₂ : IsMax (a n)) (e : ∀ i < n, a i ⋖ a (i + 1)),
  ∃ (a : ℕ → α), a 0 = x ∧ ∃ (n : ℕ), a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)
Tactic: obtain ⟨a, h₁, n, h₂, e⟩ := exists_covBy_seq_of_wellFoundedLT_wellFoundedGT S
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (hypothesis)
Goal:
α : Type u_2
inst : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
S : Set α := Set.Icc x y
hS : BoundedOrder (↑S : Type u_2) := { top := ⟨y, ⋯⟩, le_top := ⋯, bot := ⟨x, ⋯⟩, bot_le := ⋯ }
a : ℕ → (↑S : Type u_2)
h₁ : IsMin (a 0)
n : ℕ
h₂ : IsMax (a n)
e : ∀ i < n, a i ⋖ a (i + 1)
⊢ ∃ (a : ℕ → α), a 0 = x ∧ ∃ (n : ℕ), a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)
have h₃ : (↑(a 0) : α) = (↑⊥ : α)
Tactic: simp only [isMin_iff_eq_bot, Subtype.ext_iff, isMax_iff_eq_top] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (hypothesis)
Goal:
α : Type u_2
inst : PartialOrder α
wfl : WellFoundedLT α
wfg : WellFoundedGT α
x y : α
h : x ≤ y
S : Set α := Set.Icc x y
hS : BoundedOrder (↑S : Type u_2) := { top := ⟨y, ⋯⟩, le_top := ⋯, bot := ⟨x, ⋯⟩, bot_le := ⋯ }
a : ℕ → (↑S : Type u_2)
h₁ : IsMin (a 0)
n : ℕ
h₂ : IsMax (a n)
e : ∀ i < n, a i ⋖ a (i + 1)
h₃ : (↑(a 0) : α) = (↑⊥ : α)
⊢ ∃ (a : ℕ → α), a 0 = x ∧ ∃ (n : ℕ), a n = y ∧ ∀ i < n, a i ⋖ a (i + 1)
have h₄ : (↑(a n) : α) = (↑⊤ : α)
Tactic: simp only [isMin_iff_eq_bot, Subtype.ext_iff, isMax_iff_eq_top] at h₁ h₂
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.Order.Part (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
x y : α
h : x ≤ y
a : γ
⊢ Membership.mem (γ := Part γ) ((fun (x : α) ↦ (f x).bind (g x)) x) a →
    Membership.mem (γ := Part γ) ((fun (x : α) ↦ (f x).bind (g x)) y) a
have simp : ∀ (x_1 : β), x_1 ∈ f x → a ∈ g x x_1 → ∃ (a_3 : β), a_3 ∈ f y ∧ a ∈ g y a_3
Tactic: simp only [and_imp, Part.mem_bind_iff, exists_imp]
-- Lean 4 proof step from Mathlib.Order.Part (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
x y : α
h : x ≤ y
a : γ
⊢ Membership.mem (γ := Part γ) ((fun (x : α) ↦ (f x).bind (g x)) y) a →
    Membership.mem (γ := Part γ) ((fun (x : α) ↦ (f x).bind (g x)) x) a
have simp : ∀ (x_1 : β), x_1 ∈ f y → a ∈ g y x_1 → ∃ (a_3 : β), a_3 ∈ f x ∧ a ∈ g x a_3
Tactic: simp only [and_imp, Part.mem_bind_iff, exists_imp]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ p ((partialSups f : (a : ι) → α) i) ↔ ∀ j ≤ i, p (f j)
have rw : (Iic i).sup (p ∘ f) ↔ ∀ j ≤ i, p (f j)
Tactic: rw [partialSups_apply, comp_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p, sup'_eq_sup]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
rw : (Iic i).sup (p ∘ f) ↔ ∀ j ≤ i, p (f j)
⊢ p ((partialSups f : (a : ι) → α) i) ↔ ∀ j ≤ i, p (f j)
have rw₁ : ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)
Tactic: rw [partialSups_apply, comp_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p, sup'_eq_sup]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
x y : α
⊢ p (x ⊔ y) = max (p x) (p y)
have rw : (p x ∧ p y) = max (p x) (p y)
Tactic: rw [hp]
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
⊢ p ((partialSups f : (a : ι) → α) i) ↔ ∀ j ≤ i, p (f j)
have rw : p ((Iic i).sup' sorry f) ↔ ∀ j ≤ i, p (f j)
Tactic: classical
  rw [partialSups_apply, comp_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p, sup'_eq_sup]
  · change (Iic i).inf (p ∘ f) ↔ _
    simp [Finset.inf_eq_iInf]
  · intro x y
    rw [hp]
    rfl
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
rw : p ((Iic i).sup' ⋯ f) ↔ ∀ j ≤ i, p (f j)
⊢ p ((partialSups f : (a : ι) → α) i) ↔ ∀ j ≤ i, p (f j)
have rw₁ : (Iic i).sup' sorry (p ∘ f) ↔ ∀ j ≤ i, p (f j)
Tactic: classical
  rw [partialSups_apply, comp_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p, sup'_eq_sup]
  · change (Iic i).inf (p ∘ f) ↔ _
    simp [Finset.inf_eq_iInf]
  · intro x y
    rw [hp]
    rfl
-- Lean 4 proof step from Mathlib.Order.PartialSups (goal)
Goal:
α : Type u_1
ι : Type u_3
inst : SemilatticeSup α
inst_1 : Preorder ι
inst_2 : LocallyFiniteOrderBot ι
f : ι → α
p : α → Prop
hp : ∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b
i : ι
rw : p ((Iic i).sup' ⋯ f) ↔ ∀ j ≤ i, p (f j)
rw₁ : (Iic i).sup' ⋯ (p ∘ f) ↔ ∀ j ≤ i, p (f j)
⊢ p ((partialSups f : (a : ι) → α) i) ↔ ∀ j ≤ i, p (f j)
have rw₂ : ∀ (x y : α), p (x ⊔ y) = max (p x) (p y)
Tactic: classical
  rw [partialSups_apply, comp_sup'_eq_sup'_comp (γ := Propᵒᵈ) _ p, sup'_eq_sup]
  · change (Iic i).inf (p ∘ f) ↔ _
    simp [Finset.inf_eq_iInf]
  · intro x y
    rw [hp]
    rfl