awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ Eq.{u_4 + 1} (α := γ) ((f (ωSup c) : (a : β) → γ) (g (ωSup c)) : γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)
have rw : Eq.{u_4 + 1} (α := γ)
  ((ωSup (c.map { toFun := f, monotone' := sorry : α →o β →𝒄 γ }) : (a : β) → γ)
      (ωSup (c.map { toFun := g, monotone' := sorry : α →o β })) :
    γ)
  (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := sorry }) : γ)
Tactic: rw [hf.map_ωSup, hg.map_ωSup]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ Eq.{u_4 + 1} (α := γ)
    ((ωSup (c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }) : (a : β) → γ)
        (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })) :
      γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)
have simp : ωSup
    (((c.map { toFun := f, monotone' := sorry : α →o β →𝒄 γ }).map toMono).map
      (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := sorry : α →o β })))) =
  ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := sorry })
Tactic: simp only [ωSup_def, ωSup_apply]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ ωSup
      (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })))) =
    ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ })
have a : ωSup
    (((c.map { toFun := f, monotone' := sorry : α →o β →𝒄 γ }).map toMono).map
      (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := sorry : α →o β })))) ≤
  ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := sorry })
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
a :
  ωSup
      (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })))) ≤
    ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ })
⊢ ωSup
      (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })))) =
    ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ })
have a₁ : ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := sorry }) ≤
  ωSup
    (((c.map { toFun := f, monotone' := sorry : α →o β →𝒄 γ }).map toMono).map
      (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := sorry : α →o β }))))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ ωSup
      (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })))) ≤
    ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ })
have a : ∀ (i : ℕ),
  LE.le (α := γ)
    ((((c.map { toFun := f, monotone' := sorry : α →o β →𝒄 γ }).map toMono).map
            (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := sorry : α →o β }))) :
          (a : ℕ) → γ)
        i :
      γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := sorry }) : γ)
Tactic: apply ωSup_le
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ LE.le (α := γ)
    ((((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
            (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β }))) :
          (a : ℕ) → γ)
        i :
      γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)
have a : LE.le.{u_4} (α := γ)
  ((f ((c : (a : ℕ) → α) i) : (a : β) → γ) (ωSup (c.map { toFun := g, monotone' := sorry : α →o β })) : γ)
  (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := sorry }) : γ)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ LE.le.{u_4} (α := γ)
    ((f ((c : (a : ℕ) → α) i) : (a : β) → γ) (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })) : γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)
have a : ωSup ((c.map { toFun := g, monotone' := sorry : α →o β }).map (↑(f ((c : (a : ℕ) → α) i)) : β →o γ)) ≤
  ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := sorry })
Tactic: rw [(f (c i)).continuous]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ ωSup ((c.map { toFun := g, monotone' := ⋯ : α →o β }).map (↑(f ((c : (a : ℕ) → α) i)) : β →o γ)) ≤
    ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ })
have a : ∀ (i_1 : ℕ),
  LE.le (α := γ)
    (((c.map { toFun := g, monotone' := sorry : α →o β }).map (↑(f ((c : (a : ℕ) → α) i)) : β →o γ) : (a : ℕ) → γ) i_1 : γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := sorry }) : γ)
Tactic: apply ωSup_le
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ LE.le (α := γ)
    (((c.map { toFun := g, monotone' := ⋯ : α →o β }).map (↑(f ((c : (a : ℕ) → α) i)) : β →o γ) : (a : ℕ) → γ) j : γ)
    (ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) : γ)
have a : LE.le (α := γ)
  (((c.map { toFun := g, monotone' := sorry : α →o β }).map (↑(f ((c : (a : ℕ) → α) i)) : β →o γ) : (a : ℕ) → γ) j : γ)
  ((c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := sorry } : (a : ℕ) → γ) (max i j) : γ)
Tactic: apply le_ωSup_of_le (i ⊔ j)
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ LE.le (α := γ)
    (((c.map { toFun := g, monotone' := ⋯ : α →o β }).map (↑(f ((c : (a : ℕ) → α) i)) : β →o γ) : (a : ℕ) → γ) j : γ)
    ((c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ } : (a : ℕ) → γ) (max i j) : γ)
have a : f ((c : (a : ℕ) → α) i) ≤ f ((c.toOrderHom : (a : ℕ) → α) (max i j))
Tactic: apply apply_mono
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
a : f ((c : (a : ℕ) → α) i) ≤ f ((c.toOrderHom : (a : ℕ) → α) (max i j))
⊢ LE.le (α := γ)
    (((c.map { toFun := g, monotone' := ⋯ : α →o β }).map (↑(f ((c : (a : ℕ) → α) i)) : β →o γ) : (a : ℕ) → γ) j : γ)
    ((c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ } : (a : ℕ) → γ) (max i j) : γ)
have a₁ : ((c.map { toFun := g, monotone' := sorry : α →o β }).toOrderHom : (a : ℕ) → β) j ≤
  g ((c.toOrderHom : (a : ℕ) → α) (max i j))
Tactic: apply apply_mono
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ ωSup (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ }) ≤
    ωSup
      (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β }))))
have a : ∀ (i : ℕ),
  (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := sorry } : (a : ℕ) → γ) i ≤
    ωSup
      (((c.map { toFun := f, monotone' := sorry : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := sorry : α →o β }))))
Tactic: simp only [ωSup_le_iff]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ (c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ } : (a : ℕ) → γ) i ≤
    ωSup
      (((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β }))))
have a : LE.le (α := γ) ((c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := sorry } : (a : ℕ) → γ) i : γ)
  ((((c.map { toFun := f, monotone' := sorry : α →o β →𝒄 γ }).map toMono).map
          (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := sorry : α →o β }))) :
        (a : ℕ) → γ)
      i :
    γ)
Tactic: apply le_ωSup_of_le i
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ LE.le (α := γ) ((c.map { toFun := fun (x : α) ↦ (f x : (a : β) → γ) (g x), monotone' := ⋯ } : (a : ℕ) → γ) i : γ)
    ((((c.map { toFun := f, monotone' := ⋯ : α →o β →𝒄 γ }).map toMono).map
            (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β }))) :
          (a : ℕ) → γ)
        i :
      γ)
have a : g ((c.toOrderHom : (a : ℕ) → α) i) ≤ ωSup (c.map { toFun := g, monotone' := sorry : α →o β })
Tactic: apply (f (c i)).monotone
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β
inst_2 : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i : ℕ
⊢ g ((c.toOrderHom : (a : ℕ) → α) i) ≤ ωSup (c.map { toFun := g, monotone' := ⋯ : α →o β })
have a : g ((c.toOrderHom : (a : ℕ) → α) i) ≤ g ((c.toOrderHom : (a : ℕ) → α) i)
Tactic: apply le_ωSup_of_le i
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
ι : Sort u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β_1
inst_2 : OmegaCompletePartialOrder γ_1
inst_3 : OmegaCompletePartialOrder δ
β γ : Type v
f : ContinuousHom.{u_2, v} α (Part β)
g : ContinuousHom.{u_2, v} α (β → Part γ)
c : Chain α
⊢ (OrderHom.partBind (↑f : α →o Part β) g.toOrderHom).toFun (ωSup c) =
    ωSup (c.map (OrderHom.partBind (↑f : α →o Part β) g.toOrderHom))
have rw : OrderHom.toFun (OrderHom.partBind (↑f : α →o Part β) (↑g : α →o β → Part γ)) (ωSup c) =
  Bind.bind (α := β) ((f : (a : α) → Part β) (ωSup c)) ((g : (a : α) → β → Part γ) (ωSup c))
Tactic: rw [ωSup_bind, ← f.continuous, g.toOrderHom_eq_coe, ← g.continuous]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
ι : Sort u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β_1
inst_2 : OmegaCompletePartialOrder γ_1
inst_3 : OmegaCompletePartialOrder δ
β γ : Type v
f : β → γ
g : ContinuousHom.{u_2, v} α (Part β)
⊢ Eq (α := α → Part γ) (fun (x : α) ↦ f <$> (g : (a : α) → Part β) x) (⇑(g.bind (const (pure ∘ f))) : (a : α) → Part γ)
have h : ∀ (x : α), Eq (α := Part γ) (f <$> (g : (a : α) → Part β) x) ((g.bind (const (pure ∘ f)) : (a : α) → Part γ) x)
Tactic: ext1
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
ι : Sort u_1
α : Type u_2
β_1 : Type u_3
γ_1 : Type u_4
δ : Type u_5
inst : OmegaCompletePartialOrder α
inst_1 : OmegaCompletePartialOrder β_1
inst_2 : OmegaCompletePartialOrder γ_1
inst_3 : OmegaCompletePartialOrder δ
β γ : Type v
f : ContinuousHom.{u_2, v} α (Part (β → γ))
g : ContinuousHom.{u_2, v} α (Part β)
⊢ Eq (α := α → Part γ) (fun (x : α) ↦ (f : (a : α) → Part (β → γ)) x <*> (g : (a : α) → Part β) x)
    (⇑(f.bind (flip (_root_.flip map g))) : (a : α) → Part γ)
have h : ∀ (x : α) (a : γ),
  Membership.mem (γ := Part γ) ((f : (a : α) → Part (β → γ)) x <*> (g : (a : α) → Part β) x) a ↔
    Membership.mem (γ := Part γ) ((f.bind (flip (_root_.flip map g)) : (a : α) → Part γ) x : Part γ) a
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
⊢ Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) (ωSup (iterateChain (↑f : α →o α) x h))
have rw : ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α)) = ωSup (iterateChain (↑f : α →o α) x h)
Tactic: rw [mem_fixedPoints, IsFixedPt, f.continuous]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
⊢ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α)) = ωSup (iterateChain (↑f : α →o α) x h)
have a : ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α)) ≤ ωSup (iterateChain (↑f : α →o α) x h)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α)) ≤ ωSup (iterateChain (↑f : α →o α) x h)
⊢ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α)) = ωSup (iterateChain (↑f : α →o α) x h)
have a₁ : ωSup (iterateChain (↑f : α →o α) x h) ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
⊢ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α)) ≤ ωSup (iterateChain (↑f : α →o α) x h)
have a : ∀ (i : ℕ), ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) i ≤ ωSup (iterateChain (↑f : α →o α) x h)
Tactic: apply ωSup_le
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
n : ℕ
⊢ ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) n ≤ ωSup (iterateChain (↑f : α →o α) x h)
have a : (f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) ≤ ωSup (iterateChain (↑f : α →o α) x h)
Tactic: simp only [Chain.coe_map, OrderHomClass.coe_coe, comp_apply]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
n : ℕ
⊢ (f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) ≤ ωSup (iterateChain (↑f : α →o α) x h)
have this : Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
  ((f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) : α)
Tactic: have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
      Function.iterate_succ_apply' ..
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
n : ℕ
this :
  Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
    ((f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) : α)
⊢ (f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) ≤ ωSup (iterateChain (↑f : α →o α) x h)
have a : (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ ≤ ωSup (iterateChain (↑f : α →o α) x h)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
⊢ ωSup (iterateChain (↑f : α →o α) x h) ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
have a : ∀ (i : ℕ), (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) i ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
Tactic: apply ωSup_le
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) 0 ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
have a : (f : (a : α) → α) x ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
Tactic: apply le_trans h
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
⊢ (f : (a : α) → α) x ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
have a : ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) 0 ≤
  ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
Tactic: change ((iterateChain f x h).map f) 0 ≤ ωSup ((iterateChain f x h).map (f : α →o α))
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
n : ℕ
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) (n + 1) ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
have this : Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
  (((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) n : α)
Tactic: have : iterateChain f x h (n.succ) = (iterateChain f x h).map f n :=
        Function.iterate_succ_apply' ..
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
n : ℕ
this :
  Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
    (((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) n : α)
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) (n + 1) ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
have a : ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) n ≤
  ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : (f : (a : α) → α) a ≤ a
h_x_le_a : x ≤ a
⊢ ωSup (iterateChain (↑f : α →o α) x h) ≤ a
have a₁ : ∀ (i : ℕ), (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) i ≤ a
Tactic: apply ωSup_le
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : (f : (a : α) → α) a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n ≤ a
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) (n + 1) ≤ a
have this : Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
  ((f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) : α)
Tactic: have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
      Function.iterate_succ_apply' ..
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : (f : (a : α) → α) a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n ≤ a
this :
  Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
    ((f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) : α)
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) (n + 1) ≤ a
have a₁ : (f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) ≤ a
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : (f : (a : α) → α) a ≤ a
h_x_le_a : x ≤ a
n : ℕ
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n ≤ a
have a₁ : (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) 0 ≤ a
Tactic: induction n with
  | zero => exact h_x_le_a
  | succ n h_ind =>
    have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
      Function.iterate_succ_apply' ..
    rw [this]
    exact le_trans (f.monotone h_ind) h_a
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (goal)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : (f : (a : α) → α) a ≤ a
h_x_le_a : x ≤ a
n : ℕ
a₁ : (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) 0 ≤ a
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n ≤ a
have a₂ : ∀ (n : ℕ) (h_ind : (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n ≤ a),
  (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) (n + 1) ≤ a
Tactic: induction n with
  | zero => exact h_x_le_a
  | succ n h_ind =>
    have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
      Function.iterate_succ_apply' ..
    rw [this]
    exact le_trans (f.monotone h_ind) h_a
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a
h_x_le_a : x ≤ a
⊢ ωSup (iterateChain (↑f : α →o α) x h) ≤ a
have h_a₁ : IsFixedPt (⇑f : (a : α) → α) a
Tactic: rw [mem_fixedPoints] at h_a
Cleared hypotheses: h_a, h_x_le_a
-- Lean 4 proof step from Mathlib.Order.OmegaCompletePartialOrder (hypothesis)
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : IsFixedPt (⇑f : (a : α) → α) a
h_x_le_a : x ≤ a
⊢ ωSup (iterateChain (↑f : α →o α) x h) ≤ a
have h_a₁ : (f : (a : α) → α) a ≤ a
Tactic: obtain h_a := Eq.le h_a