case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ Part.fix ↑f ≤ ωSup (approxChain f)

case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ↑f
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ Part.fix ↑f = ωSup (approxChain f)
apply le_antisymm
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
⊢ Part.fix (↑f) x ≤ ωSup (approxChain f) x
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ Part.fix ↑f ≤ ωSup (approxChain f)
intro x
case a.intro
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part.fix (↑f) x ≤ ωSup (approxChain f) x
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
⊢ Part.fix (↑f) x ≤ ωSup (approxChain f) x
cases' exists_fix_le_approx f x with i hx
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part.fix (↑f) x ≤ approx (↑f) (Nat.succ i) x

α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ approx (↑f) (Nat.succ i) x ≤ ωSup (approxChain f) x
case a.intro
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part.fix (↑f) x ≤ ωSup (approxChain f) x
trans approx f i.succ x
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ approx (↑f) (Nat.succ i) x ≤ ↑(Chain.map (approxChain f) (Pi.evalOrderHom x)) (Nat.succ i)
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ approx (↑f) (Nat.succ i) x ≤ ωSup (approxChain f) x
apply le_ωSup_of_le i.succ
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ ↑f (approx (↑f) i) x ≤ ↑(approxChain f) (Nat.succ i) x
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ approx (↑f) (Nat.succ i) x ≤ ↑(Chain.map (approxChain f) (Pi.evalOrderHom x)) (Nat.succ i)
dsimp [approx]
no goals
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ ↑f (approx (↑f) i) x ≤ ↑(approxChain f) (Nat.succ i) x
rfl
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part.fix (↑f) x ≤ ?m.11030

α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ ?m.11030 ≤ approx (↑f) (Nat.succ i) x

α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part (β x)
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part.fix (↑f) x ≤ approx (↑f) (Nat.succ i) x
trans
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ approx (↑f) i x ≤ approx (↑f) (Nat.succ i) x
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part.fix (↑f) x ≤ ?m.11030

α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ ?m.11030 ≤ approx (↑f) (Nat.succ i) x

α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ Part (β x)
apply hx
no goals
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
x : α✝
i : ℕ
hx : Part.fix (↑f) x ≤ approx (↑f) i x
⊢ approx (↑f) i x ≤ approx (↑f) (Nat.succ i) x
apply approx_mono' f
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ ∀ (i : ℕ), ↑(approxChain f) i ≤ Part.fix ↑f
case a
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ ωSup (approxChain f) ≤ Part.fix ↑f
apply ωSup_le _ _ _
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ ∀ (i : ℕ), approx (↑f) i ≤ Part.fix ↑f
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ ∀ (i : ℕ), ↑(approxChain f) i ≤ Part.fix ↑f
simp only [Fix.approxChain, OrderHom.coe_fun_mk]
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
y : ℕ
x : α✝
⊢ approx (↑f) y x ≤ Part.fix (↑f) x
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
⊢ ∀ (i : ℕ), approx (↑f) i ≤ Part.fix ↑f
intro y x
no goals
α✝ : Type u_1
β : α✝ → Type u_2
α : Type ?u.10198
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
y : ℕ
x : α✝
⊢ approx (↑f) y x ≤ Part.fix (↑f) x
apply approx_le_fix f