α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ωSup (approxChain f) ≤ X
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ Part.fix ↑f ≤ X
rw [fix_eq_ωSup f]
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ∀ (i : ℕ), ↑(approxChain f) i ≤ X
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ωSup (approxChain f) ≤ X
apply ωSup_le _ _ _
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ∀ (i : ℕ), approx (↑f) i ≤ X
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ∀ (i : ℕ), ↑(approxChain f) i ≤ X
simp only [Fix.approxChain, OrderHom.coe_fun_mk]
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
i : ℕ
⊢ approx (↑f) i ≤ X
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ∀ (i : ℕ), approx (↑f) i ≤ X
intro i
no goals
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
i : ℕ
⊢ approx (↑f) i ≤ X
induction i with
| zero => dsimp [Fix.approx]; apply bot_le
| succ _ i_ih => trans f X; apply f.monotone i_ih ; apply hX
case zero
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ⊥ ≤ X
case zero
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ approx (↑f) Nat.zero ≤ X
dsimp [Fix.approx]
no goals
case zero
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
⊢ ⊥ ≤ X
apply bot_le
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ X
⊢ approx (↑f) (Nat.succ n✝) ≤ ↑f X

α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ X
⊢ ↑f X ≤ X
case succ
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ X
⊢ approx (↑f) (Nat.succ n✝) ≤ X
trans f X
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ X
⊢ ↑f X ≤ X
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ X
⊢ approx (↑f) (Nat.succ n✝) ≤ ↑f X

α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ X
⊢ ↑f X ≤ X
apply f.monotone i_ih
no goals
α✝ : Type u_2
β : α✝ → Type u_1
α : Type ?u.12565
f : ((a : α✝) → Part (β a)) →o (a : α✝) → Part (β a)
X : (a : α✝) → Part (β a)
hX : ↑f X ≤ X
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ X
⊢ ↑f X ≤ X
apply hX