case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij✝ : i ≤ j
hij : i ≤ Nat.zero
⊢ approx (↑f) i ≤ approx (↑f) Nat.zero

case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j✝ : ℕ
hij✝ : i ≤ j✝
j : ℕ
ih : i ≤ j → approx (↑f) i ≤ approx (↑f) j
hij : i ≤ Nat.succ j
⊢ approx (↑f) i ≤ approx (↑f) (Nat.succ j)
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij : i ≤ j
⊢ approx (↑f) i ≤ approx (↑f) j
induction' j with j ih
case succ.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j✝ j : ℕ
hij : Nat.succ j ≤ j✝
ih : Nat.succ j ≤ j → approx (↑f) (Nat.succ j) ≤ approx (↑f) j
⊢ approx (↑f) (Nat.succ j) ≤ approx (↑f) (Nat.succ j)

case succ.step
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j✝ : ℕ
hij : i ≤ j✝
j : ℕ
ih : i ≤ j → approx (↑f) i ≤ approx (↑f) j
a✝ : Nat.le i j
⊢ approx (↑f) i ≤ approx (↑f) (Nat.succ j)
case succ
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j✝ : ℕ
hij✝ : i ≤ j✝
j : ℕ
ih : i ≤ j → approx (↑f) i ≤ approx (↑f) j
hij : i ≤ Nat.succ j
⊢ approx (↑f) i ≤ approx (↑f) (Nat.succ j)
cases hij
no goals
case succ.step
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j✝ : ℕ
hij : i ≤ j✝
j : ℕ
ih : i ≤ j → approx (↑f) i ≤ approx (↑f) j
a✝ : Nat.le i j
⊢ approx (↑f) i ≤ approx (↑f) (Nat.succ j)
exact le_trans (ih ‹_›) (approx_mono' f)
case zero.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j : ℕ
hij : Nat.zero ≤ j
⊢ approx (↑f) Nat.zero ≤ approx (↑f) Nat.zero
case zero
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i j : ℕ
hij✝ : i ≤ j
hij : i ≤ Nat.zero
⊢ approx (↑f) i ≤ approx (↑f) Nat.zero
cases hij
no goals
case zero.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j : ℕ
hij : Nat.zero ≤ j
⊢ approx (↑f) Nat.zero ≤ approx (↑f) Nat.zero
exact le_rfl
no goals
case succ.refl
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
j✝ j : ℕ
hij : Nat.succ j ≤ j✝
ih : Nat.succ j ≤ j → approx (↑f) (Nat.succ j) ≤ approx (↑f) j
⊢ approx (↑f) (Nat.succ j) ≤ approx (↑f) (Nat.succ j)
exact le_rfl