no goals
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
⊢ approx (↑f) i ≤ approx (↑f) (Nat.succ i)
induction i with
| zero => dsimp [approx]; apply @bot_le _ _ _ (f ⊥)
| succ _ i_ih => intro ; apply f.monotone; apply i_ih
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ⊥ ≤ ↑f ⊥
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ approx (↑f) Nat.zero ≤ approx (↑f) (Nat.succ Nat.zero)
dsimp [approx]
no goals
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
⊢ ⊥ ≤ ↑f ⊥
apply @bot_le _ _ _ (f ⊥)
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
i✝ : α
⊢ approx (↑f) (Nat.succ n✝) i✝ ≤ approx (↑f) (Nat.succ (Nat.succ n✝)) i✝
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
⊢ approx (↑f) (Nat.succ n✝) ≤ approx (↑f) (Nat.succ (Nat.succ n✝))
intro
case succ.a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
i✝ : α
⊢ approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
i✝ : α
⊢ approx (↑f) (Nat.succ n✝) i✝ ≤ approx (↑f) (Nat.succ (Nat.succ n✝)) i✝
apply f.monotone
no goals
case succ.a
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
n✝ : ℕ
i_ih : approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
i✝ : α
⊢ approx (↑f) n✝ ≤ approx (↑f) (Nat.succ n✝)
apply i_ih