-- Mathlib/Control/LawfulFix.lean
theorem fix_eq_of_ωScottContinuous (hc : ωScottContinuous g) :
    Part.fix g = g (Part.fix g)

Proof state:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
⊢ (approxChain { toFun := g, monotone' := ⋯ }) i ≤
    ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) i

Tactic:
intro x

Result:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
x : α
⊢ (approxChain { toFun := g, monotone' := ⋯ }) i x ≤
    ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) i x

Proof state:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
⊢ ∃ j,
    ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) i ≤
      (approxChain { toFun := g, monotone' := ⋯ }) j

Tactic:
exists i.succ

Result:
no goals

Proof state:
case a
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup (approxChain { toFun := g, monotone' := ⋯ }) ≤
    ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ })

Tactic:
apply ωSup_le_ωSup_of_le _

Result:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ approxChain { toFun := g, monotone' := ⋯ } ≤
    (approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }

Proof state:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ approxChain { toFun := g, monotone' := ⋯ } ≤
    (approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }

Tactic:
intro i

Result:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
⊢ ∃ j,
    (approxChain { toFun := g, monotone' := ⋯ }) i ≤
      ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) j

Proof state:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ (approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ } ≤
    approxChain { toFun := g, monotone' := ⋯ }

Tactic:
intro i

Result:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
⊢ ∃ j,
    ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) i ≤
      (approxChain { toFun := g, monotone' := ⋯ }) j

Proof state:
case a
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) ≤
    ωSup (approxChain { toFun := g, monotone' := ⋯ })

Tactic:
apply ωSup_le_ωSup_of_le _

Result:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ (approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ } ≤
    approxChain { toFun := g, monotone' := ⋯ }

Proof state:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
⊢ ∃ j,
    (approxChain { toFun := g, monotone' := ⋯ }) i ≤
      ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) j

Tactic:
exists i

Result:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
⊢ (approxChain { toFun := g, monotone' := ⋯ }) i ≤
    ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) i

Proof state:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup (approxChain { toFun := g, monotone' := ⋯ }) =
    ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ })

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup (approxChain { toFun := g, monotone' := ⋯ }) ≤
    ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ })

case a
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) ≤
    ωSup (approxChain { toFun := g, monotone' := ⋯ })

Proof state:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ Part.fix g = g (Part.fix g)

Tactic:
rw [fix_eq_ωSup_of_ωScottContinuous hc, hc.map_ωSup]

Result:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
⊢ ωSup (approxChain { toFun := g, monotone' := ⋯ }) =
    ωSup ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ })

Proof state:
α : Type u_1
β : α → Type u_2
g : ((a : α) → Part (β a)) → (a : α) → Part (β a)
hc : ωScottContinuous g
i : ℕ
x : α
⊢ (approxChain { toFun := g, monotone' := ⋯ }) i x ≤
    ((approxChain { toFun := g, monotone' := ⋯ }).map { toFun := g, monotone' := ⋯ }) i x

Tactic:
apply le_f_of_mem_approx _ ⟨i, rfl⟩

Result:
no goals