awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.OrdContinuous (goal)
Goal:
α : Type u
β : Type v
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
s : Set α
⊢ f (sSup s) = ⨆ x ∈ s, f x
have rw : sSup (f '' s) = ⨆ x ∈ s, f x
Tactic: rw [hf.map_sSup', sSup_image]
-- Lean 4 proof step from Mathlib.Order.OrdContinuous (goal)
Goal:
α : Type u
β : Type v
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
s : Set α
rw : sSup (f '' s) = ⨆ x ∈ s, f x
⊢ f (sSup s) = ⨆ x ∈ s, f x
have rw₁ : Eq.{v + 1} (α := β) (⨆ a ∈ s, f a) (⨆ x ∈ s, f x)
Tactic: rw [hf.map_sSup', sSup_image]
-- Lean 4 proof step from Mathlib.Order.OrdContinuous (goal)
Goal:
α : Type u
β : Type v
ι : Sort x
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
g : ι → α
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
have simp : sSup (range.{v, x} (ι := ι) (f ∘ fun (i : ι) ↦ g i)) = sSup (range fun (i : ι) ↦ f (g i))
Tactic: simp only [iSup, hf.map_sSup', ← range_comp]
-- Lean 4 proof step from Mathlib.Order.OrdContinuous (goal)
Goal:
α : Type u
β : Type v
ι : Sort x
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Nonempty ι
f : α → β
hf : LeftOrdContinuous f
g : ι → α
hg : BddAbove (range g)
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)
have simp : sSup (range (f ∘ g)) = sSup (range fun (i : ι) ↦ f (g i))
Tactic: simp only [iSup, hf.map_csSup (range_nonempty _) hg, ← range_comp]
-- Lean 4 proof step from Mathlib.Order.OrderDual (goal)
Goal:
α : Type u_1
inst : LT α
T : Std.Trichotomous.{u_1 + 1} (α := α) LT.lt
a b : αᵒᵈ
⊢ ¬a < b → ¬b < a → a = b
have rw : ¬a < b → ¬b < a → b = a
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Order.OrderDual (goal)
Goal:
α_1 : Type u_1
α : Type u_2
inst : LinearOrder α
a b : αᵒᵈ
⊢ compare a b = compareOfLessAndEq a b
have simp : (if b < a then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
  if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
Tactic: simp only [compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, eq_comm]
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsStrictOrder α r
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
k : ℕ
⊢ ¬Acc r ((f : (a : ℕ) → α) k)
have 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 : α) }
Tactic: rw [acc_iff_isEmpty_subtype_mem_range, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsStrictOrder α r
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r
⊢ ¬WellFounded r
have rw : Nonempty.{u_1 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r r)
Tactic: rw [wellFounded_iff_isEmpty, not_isEmpty_iff]
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
s : Set ℕ
inst : Infinite (↑s : Type)
dP : DecidablePred fun (x : ℕ) ↦ x ∈ s
n : ℕ
⊢ (orderIsoOfNat s : (a : ℕ) → (↑s : Type)) n = ofNat s n
have simp : ofNat s n = ofNat s n
Tactic: simp only [orderIsoOfNat, RelIso.ofSurjective_apply,
    RelEmbedding.orderEmbeddingOfLTEmbedding_apply, RelEmbedding.coe_natLT]
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (hypothesis)
Goal:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
have this : 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]
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
this : Infinite (↑(e ⁻¹' s) : Type) ∨ Infinite (↑(e ⁻¹' t) : Type)
⊢ ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
have inl : Infinite (↑(e ⁻¹' s) : Type) →
  ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
Tactic: cases this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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
⊢ ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
have inr : Infinite (↑(e ⁻¹' t) : Type) →
  ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
Tactic: cases this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
⊢ ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
have have : Infinite (↑(e ⁻¹' s) : Type) ∨ Infinite (↑(e ⁻¹' t) : Type)
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⟩]
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
s t : Set α
e : ℕ → α
he : ∀ (n : ℕ), e n ∈ s ∪ t
have : Infinite (↑(e ⁻¹' s) : Type) ∨ Infinite (↑(e ⁻¹' t) : Type)
⊢ ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
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
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⟩]
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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
⊢ ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
have inl : Infinite (↑(e ⁻¹' s) : Type) →
  ∃ (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⟩]
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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
⊢ ∃ (g : ℕ ↪o ℕ), (∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ s) ∨ ∀ (n : ℕ), e ((g : (a : ℕ) → ℕ) n) ∈ t
have inr : Infinite (↑(e ⁻¹' t) : Type) →
  ∃ (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⟩]
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f 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))
have 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))
Tactic: by_cases hbad : Infinite bad
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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))
⊢ ∃ (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))
have 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))
Tactic: by_cases hbad : Infinite bad
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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))
have pos : ∀ (m n : ℕ) (mn : m < n),
  ¬r (f ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) m)) (f ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) n))
Tactic: refine ⟨Nat.orderEmbeddingOfSet bad, Or.intro_right _ fun m n mn => ?_⟩
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (hypothesis)
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
⊢ ¬r (f ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) m)) (f ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) n))
have h : 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
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (hypothesis)
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 : ℕ)
⊢ ¬r (f ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) m)) (f ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) n))
have h₁ : Membership.mem (α := ℕ) bad ((Nat.orderEmbeddingOfSet bad : (a : ℕ) → ℕ) m : ℕ)
Tactic: rw [Nat.orderEmbeddingOfSet_range bad] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (hypothesis)
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))
have hbad₁ : bad.Finite
Tactic: rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad
Cleared hypotheses: hbad
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
⊢ ∃ (m : ℕ), ∀ (n : ℕ), m ≤ n → n ∉ bad
have pos : ∀ (he : hbad.toFinset (s := bad).Nonempty), ∃ (m : ℕ), ∀ (n : ℕ), m ≤ n → n ∉ bad
Tactic: by_cases he : hbad.toFinset.Nonempty
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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
⊢ ∃ (m : ℕ), ∀ (n : ℕ), m ≤ n → n ∉ bad
have neg : ∀ (he : ¬hbad.toFinset (s := bad).Nonempty), ∃ (m : ℕ), ∀ (n : ℕ), m ≤ n → n ∉ bad
Tactic: by_cases he : hbad.toFinset.Nonempty
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m : ℕ | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
⊢ ∃ (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))
have 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))
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⟩⟩
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (hypothesis)
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))
have h : n + m ∉ bad
Tactic: have h := hm _ (Nat.le_add_left m n)
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (hypothesis)
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
⊢ ∃ (n' : ℕ), n < n' ∧ r (f (n + m)) (f (n' + m))
have h₁ : ∃ (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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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)
⊢ ∃ (n' : ℕ), n < n' ∧ r (f (n + m)) (f (n' + m))
have obtain : ∀ (n' : ℕ) (hn1 : n + m < n') (hn2 : r (f (n + m)) (f n')), ∃ (n' : ℕ), n < n' ∧ r (f (n + m)) (f (n' + m))
Tactic: obtain ⟨n', hn1, hn2⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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' ∧ r (f (n + m)) (f (n' + m))
have refine : r (f (n + m)) (f (n + n' - n - m + m))
Tactic: refine ⟨n + n' - n - m, by lia, ?_⟩
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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 + n' - n - m + m))
have h : n + n' - n - m + m = n'
Tactic: convert! hn2
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (hypothesis)
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
⊢ ∃ (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))
have h : ∀ (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
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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))
⊢ ∃ (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))
have 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))
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⟩
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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))
⊢ ∃ (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))
have 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))
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⟩
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
Goal:
α : Type u_1
r : α → α → Prop
inst : IsTrans α r
f : ℕ → α
⊢ ∃ (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 : ∀ (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: obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f
-- Lean 4 proof step from Mathlib.Order.OrderIsoNat (goal)
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))
⊢ ∃ (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 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))
Tactic: obtain ⟨g, hr | hnr⟩ := exists_increasing_or_nonincreasing_subseq' r f