awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
⊢ a ∈ range f
have hf' : (f ⁻¹' s).Nonempty
Tactic: have hf' : (f ⁻¹' s).Nonempty := by
    obtain ⟨b, hb⟩ := hs₀
    obtain ⟨c, rfl⟩ := hs hb
    exact ⟨c, hb⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
⊢ a ∈ range f
have this : Nonempty α
Tactic: have : Nonempty α := ⟨a⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this_1 : Nonempty α
this_2 : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
⊢ a ∈ range f
have hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s))
Tactic: have hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s)) :=
    isLUB_csSup hf' ⟨a, fun b hb ↦ hf.strictMono.le_apply.trans (ha.1 hb)⟩
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this_1 : Nonempty α
this_2 : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s))
⊢ a ∈ range f
have ha' : IsLUB (f '' f ⁻¹' s) (f (sSup (f ⁻¹' s)))
Tactic: have ha' := hf.map_isLUB hfl hf'
-- Lean 4 proof step from Mathlib.Order.IsNormal (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this_1 : Nonempty α
this_2 : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s))
ha' : IsLUB (f '' f ⁻¹' s) (f (sSup (f ⁻¹' s)))
⊢ a ∈ range f
have ha'₁ : IsLUB s (f (sSup (f ⁻¹' s)))
Tactic: rw [image_preimage_eq_of_subset hs] at ha'
Cleared hypotheses: ha'
-- Lean 4 proof step from Mathlib.Order.IsNormal (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : WellFoundedLT α
f : α → α
hf : IsNormal f
s : Set α
hs : s ⊆ range f
hs₀ : s.Nonempty
h : DirectedOn (fun (x1 x2 : α) ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
hf' : (f ⁻¹' s).Nonempty
this_1 : Nonempty α
this_2 : OrderBot α := WellFoundedLT.toOrderBot α
this : ConditionallyCompleteLinearOrderBot α := WellFoundedLT.conditionallyCompleteLinearOrderBot α
hfl : IsLUB (f ⁻¹' s) (sSup (f ⁻¹' s))
ha' : IsLUB s (f (sSup (f ⁻¹' s)))
⊢ a ∈ range f
have obtain : ∀ (ha : IsLUB s (f (sSup (f ⁻¹' s)))), f (sSup (f ⁻¹' s)) ∈ range f
Tactic: obtain rfl := ha.unique ha'
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : ∀ (hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ x (n + 1) ≤ y (n + 1)
have succ : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)
Tactic: refine (hx _ n.lt_succ_self).trans ((hf <| ihn ?_ ?_).trans (hy _ n.lt_succ_self))
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : ∀ (hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n ≤ y n
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
succ : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)
⊢ x (n + 1) ≤ y (n + 1)
have succ₁ : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
Tactic: refine (hx _ n.lt_succ_self).trans ((hf <| ihn ?_ ?_).trans (hy _ n.lt_succ_self))
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
h₀ : x 0 ≤ y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
⊢ x n ≤ y n
have zero : ∀ (hx : ∀ (k : ℕ), k < 0 → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)), x 0 ≤ y 0
Tactic: induction n with
  | zero => exact h₀
  | succ n ihn =>
    refine (hx _ n.lt_succ_self).trans ((hf <| ihn ?_ ?_).trans (hy _ n.lt_succ_self))
    · exact fun k hk => hx _ (hk.trans n.lt_succ_self)
    · exact fun k hk => hy _ (hk.trans n.lt_succ_self)
Cleared hypotheses: n, hx, hy
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
h₀ : x 0 ≤ y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
zero : ∀ (hx : ∀ (k : ℕ), k < 0 → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)), x 0 ≤ y 0
⊢ x n ≤ y n
have succ : ∀ (n : ℕ)
  (ihn : ∀ (hx : ∀ (k : ℕ), k < n → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n ≤ y n)
  (hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) ≤ f (x k)) (hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)),
  x (n + 1) ≤ y (n + 1)
Tactic: induction n with
  | zero => exact h₀
  | succ n ihn =>
    refine (hx _ n.lt_succ_self).trans ((hf <| ihn ?_ ?_).trans (hy _ n.lt_succ_self))
    · exact fun k hk => hx _ (hk.trans n.lt_succ_self)
    · exact fun k hk => hy _ (hk.trans n.lt_succ_self)
Cleared hypotheses: n, hx, hy
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  ∀ (hn : 0 < n) (hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n < y n
hn : 0 < n + 1
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ x (n + 1) < y (n + 1)
have succ : x n ≤ y n
Tactic: suffices x n ≤ y n from (hx n n.lt_succ_self).trans_le ((hf this).trans <| hy n n.lt_succ_self)
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  ∀ (hn : 0 < n + 1) (hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k))
    (hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)), x (n + 1) < y (n + 1)
hn : 0 < n + 1 + 1
hx : ∀ (k : ℕ), k < n + 1 + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 + 1 → f (y k) ≤ y (k + 1)
⊢ x (n + 1) ≤ y (n + 1)
have succ : ∀ (k : ℕ) (hk : k < n + 1), k < n + 1 + 1
Tactic: refine (ihn n.zero_lt_succ (fun k hk => hx _ ?_) fun k hk => hy _ ?_).le
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  ∀ (hn : 0 < n) (hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n < y n
hn : 0 < n + 1
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ x n ≤ y n
have succ : ∀
  (ihn :
    ∀ (hn : LT.lt (α := ℕ) 0 0) (hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k))
      (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)), x 0 < y 0)
  (hn : 0 < HAdd.hAdd (α := ℕ) 0 1) (hx : ∀ (k : ℕ), k < HAdd.hAdd (α := ℕ) 0 1 → x (k + 1) < f (x k))
  (hy : ∀ (k : ℕ), k < HAdd.hAdd (α := ℕ) 0 1 → f (y k) ≤ y (k + 1)), x 0 ≤ y 0
Tactic: cases n with
  | zero => exact h₀
  | succ n =>
    refine (ihn n.zero_lt_succ (fun k hk => hx _ ?_) fun k hk => hy _ ?_).le <;>
    exact hk.trans n.succ.lt_succ_self
Cleared hypotheses: n, ihn, hn, hx, hy
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn :
  ∀ (hn : 0 < n) (hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)), x n < y n
hn : 0 < n + 1
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
succ :
  ∀
    (ihn :
      ∀ (hn : LT.lt (α := ℕ) 0 0) (hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k))
        (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)), x 0 < y 0)
    (hn : 0 < HAdd.hAdd (α := ℕ) 0 1) (hx : ∀ (k : ℕ), k < HAdd.hAdd (α := ℕ) 0 1 → x (k + 1) < f (x k))
    (hy : ∀ (k : ℕ), k < HAdd.hAdd (α := ℕ) 0 1 → f (y k) ≤ y (k + 1)), x 0 ≤ y 0
⊢ x n ≤ y n
have succ₁ : ∀ (n : ℕ)
  (ihn :
    ∀ (hn : 0 < n + 1) (hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k))
      (hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)), x (n + 1) < y (n + 1))
  (hn : 0 < n + 1 + 1) (hx : ∀ (k : ℕ), k < n + 1 + 1 → x (k + 1) < f (x k))
  (hy : ∀ (k : ℕ), k < n + 1 + 1 → f (y k) ≤ y (k + 1)), x (n + 1) ≤ y (n + 1)
Tactic: cases n with
  | zero => exact h₀
  | succ n =>
    refine (ihn n.zero_lt_succ (fun k hk => hx _ ?_) fun k hk => hy _ ?_).le <;>
    exact hk.trans n.succ.lt_succ_self
Cleared hypotheses: n, ihn, hn, hx, hy
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
hn : 0 < n
h₀ : x 0 ≤ y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
⊢ x n < y n
have zero : ∀ (hn : LT.lt (α := ℕ) 0 0) (hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)),
  x 0 < y 0
Tactic: induction n with
  | zero => exact hn.false.elim
  | succ n ihn =>
  suffices x n ≤ y n from (hx n n.lt_succ_self).trans_le ((hf this).trans <| hy n n.lt_succ_self)
  cases n with
  | zero => exact h₀
  | succ n =>
    refine (ihn n.zero_lt_succ (fun k hk => hx _ ?_) fun k hk => hy _ ?_).le <;>
    exact hk.trans n.succ.lt_succ_self
Cleared hypotheses: n, hn, hx, hy
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
hn : 0 < n
h₀ : x 0 ≤ y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
zero :
  ∀ (hn : LT.lt (α := ℕ) 0 0) (hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k))
    (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)), x 0 < y 0
⊢ x n < y n
have succ : ∀ (n : ℕ)
  (ihn :
    ∀ (hn : 0 < n) (hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)),
      x n < y n)
  (hn : 0 < n + 1) (hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)),
  x (n + 1) < y (n + 1)
Tactic: induction n with
  | zero => exact hn.false.elim
  | succ n ihn =>
  suffices x n ≤ y n from (hx n n.lt_succ_self).trans_le ((hf this).trans <| hy n n.lt_succ_self)
  cases n with
  | zero => exact h₀
  | succ n =>
    refine (ihn n.zero_lt_succ (fun k hk => hx _ ?_) fun k hk => hy _ ?_).le <;>
    exact hk.trans n.succ.lt_succ_self
Cleared hypotheses: n, hn, hx, hy
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
⊢ x n < y n
have zero : ∀ (hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)), x 0 < y 0
Tactic: cases n
Cleared hypotheses: n, hx, hy
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
n : ℕ
h₀ : x 0 < y 0
hx : ∀ (k : ℕ), k < n → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)
zero : ∀ (hx : ∀ (k : ℕ), k < 0 → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < 0 → f (y k) ≤ y (k + 1)), x 0 < y 0
⊢ x n < y n
have succ : ∀ (n : ℕ) (hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)) (hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)),
  x (n + 1) < y (n + 1)
Tactic: cases n
Cleared hypotheses: n, hx, hy
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
⊢ (h ∘ g^[n]) x ≤ (f^[n] ∘ h) x
have h₀ : (h ∘ g^[0]) x ≤ (f^[0] ∘ h) x
Tactic: apply hf.seq_le_seq n
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
h₀ : (h ∘ g^[0]) x ≤ (f^[0] ∘ h) x
⊢ (h ∘ g^[n]) x ≤ (f^[n] ∘ h) x
have hx : ∀ (k : ℕ), k < n → (h ∘ g^[k + 1]) x ≤ f ((h ∘ g^[k]) x)
Tactic: apply hf.seq_le_seq n
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
β : Type u_2
g : β → β
h : β → α
hf : Monotone f
H : h ∘ g ≤ f ∘ h
n : ℕ
x : β
h₀ : (h ∘ g^[0]) x ≤ (f^[0] ∘ h) x
hx : ∀ (k : ℕ), k < n → (h ∘ g^[k + 1]) x ≤ f ((h ∘ g^[k]) x)
⊢ (h ∘ g^[n]) x ≤ (f^[n] ∘ h) x
have hy : ∀ (k : ℕ), k < n → f ((f^[k] ∘ h) x) ≤ (f^[k + 1] ∘ h) x
Tactic: apply hf.seq_le_seq n
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
h : id ≤ f
n : ℕ
x : α
⊢ f^[n] x ≤ f^[n + 1] x
have rw : f^[n] x ≤ f (f^[n] x)
Tactic: rw [iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
⊢ f^[n] x ≤ g^[n] x
have h₀ : f^[0] x ≤ f^[0] x
Tactic: apply hf.seq_le_seq n
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
h₀ : f^[0] x ≤ f^[0] x
⊢ f^[n] x ≤ g^[n] x
have hx₁ : ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
Tactic: apply hf.seq_le_seq n
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n : ℕ
h₀ : f^[0] x ≤ f^[0] x
hx₁ : ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
⊢ f^[n] x ≤ g^[n] x
have hy : ∀ (k : ℕ), k < n → f (g^[k] x) ≤ g^[k + 1] x
Tactic: apply hf.seq_le_seq n
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : Monotone g
x : α
hx : f x ≤ g x
n k : ℕ
h_1 : k < n
⊢ f^[k + 1] x ≤ f (f^[k] x)
have hx₁ : f (f^[k] x) ≤ f (f^[k] x)
Tactic: rw [iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x
have h₀ : f^[0] x ≤ f^[0] x
Tactic: apply hf.seq_pos_lt_seq_of_le_of_lt hn
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
h₀ : f^[0] x ≤ f^[0] x
⊢ f^[n] x < g^[n] x
have hx₁ : ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
Tactic: apply hf.seq_pos_lt_seq_of_le_of_lt hn
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
h₀ : f^[0] x ≤ f^[0] x
hx₁ : ∀ (k : ℕ), k < n → f^[k + 1] x ≤ f (f^[k] x)
⊢ f^[n] x < g^[n] x
have hy : ∀ (k : ℕ), k < n → f (g^[k] x) < g^[k + 1] x
Tactic: apply hf.seq_pos_lt_seq_of_le_of_lt hn
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
hx : f x < g x
n : ℕ
hn : 0 < n
k : ℕ
h_1 : k < n
⊢ f^[k + 1] x ≤ f (f^[k] x)
have hx₁ : f (f^[k] x) ≤ f (f^[k] x)
Tactic: rw [iterate_succ_apply']
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x ↔ f x < g x
have inl : ∀ (H : f x < g x), f^[n] x < g^[n] x ↔ f x < g x
Tactic: rcases lt_trichotomy (f x) (g x) with (H | H | H)
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
inl : ∀ (H : f x < g x), f^[n] x < g^[n] x ↔ f x < g x
⊢ f^[n] x < g^[n] x ↔ f x < g x
have inr : ∀ (H : f x = g x), f^[n] x < g^[n] x ↔ f x < g x
Tactic: rcases lt_trichotomy (f x) (g x) with (H | H | H)
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
inl : ∀ (H : f x < g x), f^[n] x < g^[n] x ↔ f x < g x
inr : ∀ (H : f x = g x), f^[n] x < g^[n] x ↔ f x < g x
⊢ f^[n] x < g^[n] x ↔ f x < g x
have inr₁ : ∀ (H : g x < f x), f^[n] x < g^[n] x ↔ f x < g x
Tactic: rcases lt_trichotomy (f x) (g x) with (H | H | H)
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n + 1] x
have rw : f^[n] x ≤ f^[n] (f x)
Tactic: rw [iterate_succ_apply]
-- Lean 4 proof step from Mathlib.Order.Iterate (goal)
Goal:
α : Type u_1
inst : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n + 1] x
have rw : f^[n] x < f^[n] (f x)
Tactic: rw [iterate_succ_apply]
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y : X
hxz : @IsMaximal _ inst _ x (x ⊔ y)
hyz : @IsMaximal _ inst _ y (x ⊔ y)
⊢ @IsMaximal _ inst _ (x ⊓ y) y
have rw : @IsMaximal _ inst _ (y ⊓ x) y
Tactic: rw [inf_comm]
-- Lean 4 proof step from Mathlib.Order.JordanHolder (hypothesis)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y : X
hxz : @IsMaximal _ inst _ x (x ⊔ y)
hyz : @IsMaximal _ inst _ y (x ⊔ y)
⊢ @IsMaximal _ inst _ (y ⊓ x) y
have hxz₁ : @IsMaximal _ inst _ x (y ⊔ x)
Tactic: rw [sup_comm] at hxz hyz
Cleared hypotheses: hxz, hyz
-- Lean 4 proof step from Mathlib.Order.JordanHolder (hypothesis)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y : X
hxz : @IsMaximal _ inst _ x (x ⊔ y)
hyz : @IsMaximal _ inst _ y (x ⊔ y)
hxz₁ : @IsMaximal _ inst _ x (y ⊔ x)
⊢ @IsMaximal _ inst _ (y ⊓ x) y
have hyz₁ : @IsMaximal _ inst _ y (y ⊔ x)
Tactic: rw [sup_comm] at hxz hyz
Cleared hypotheses: hxz, hyz
-- Lean 4 proof step from Mathlib.Order.JordanHolder (hypothesis)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : @IsMaximal _ inst _ x b
hyb : @IsMaximal _ inst _ y b
⊢ @IsMaximal _ inst _ a y
have hb : x ⊔ y = b
Tactic: have hb : x ⊔ y = b := sup_eq_of_isMaximal hxb hyb hxy
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x b a y : X
ha : x ⊓ y = a
hxy : x ≠ y
hxb : @IsMaximal _ inst _ x b
hyb : @IsMaximal _ inst _ y b
hb : x ⊔ y = b
⊢ @IsMaximal _ inst _ a y
have substs : ∀ (hxb : @IsMaximal _ inst _ x (x ⊔ y)) (hyb : @IsMaximal _ inst _ y (x ⊔ y)), @IsMaximal _ inst _ (x ⊓ y) y
Tactic: substs a b
Cleared hypotheses: b, a, ha, hxb, hyb, hb
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
x y a b : X
hm : @IsMaximal _ inst _ x a
ha : x ⊔ y = a
hb : x ⊓ y = b
⊢ @Iso _ inst _ (x, a) (b, y)
have substs : ∀ (hm : @IsMaximal _ inst _ x (x ⊔ y)), @Iso _ inst _ (x, x ⊔ y) (x ⊓ y, y)
Tactic: substs a b
Cleared hypotheses: a, b, hm, ha, hb
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ x ≤ y ∨ y ≤ x
have rcases : ∀
  (i :
    Fin
      (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) +
        1))
  (hx :
    s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i ∈
      s),
  s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i ≤
      y ∨
    y ≤
      s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i
Tactic: rcases Set.mem_range.1 hx with ⟨i, rfl⟩
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
y : X
hy : y ∈ s
i :
  Fin
    (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1)
hx :
  s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      i ∈
    s
⊢ s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i ≤
      y ∨
    y ≤
      s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i
have rcases : ∀
  (j :
    Fin
      (s.length (r :=
          {x : X × X |
            match (motive := X × X → Prop) x with
            | (x, y) => @IsMaximal _ inst _ x y}) +
        1))
  (hy :
    s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        j ∈
      s),
  s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i ≤
      s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        j ∨
    s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        j ≤
      s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i
Tactic: rcases Set.mem_range.1 hy with ⟨j, rfl⟩
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Order.JordanHolder (goal)
Goal:
X : Type u
inst : Lattice X
inst_1 : JordanHolderLattice X
s : CompositionSeries X
i :
  Fin
    (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1)
hx :
  s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      i ∈
    s
j :
  Fin
    (s.length (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y}) +
      1)
hy :
  s.toFun (r :=
      {x : X × X |
        match (motive := X × X → Prop) x with
        | (x, y) => @IsMaximal _ inst _ x y})
      j ∈
    s
⊢ s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i ≤
      s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        j ∨
    s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        j ≤
      s.toFun (r :=
        {x : X × X |
          match (motive := X × X → Prop) x with
          | (x, y) => @IsMaximal _ inst _ x y})
        i
have rw : i ≤ j ∨ j ≤ i
Tactic: rw [s.strictMono.le_iff_le, s.strictMono.le_iff_le]