cases/exists

Stream: new members

[Iocta]

Documentation says cases x works on an instance x of an inductive type. What is the inductive type in cases h ((u n - l)/2) in this solution?

[Jalex Stark]

it's something like \exists N, hN

[Anatole Dedecker]

The full thing we apply cases to is h ((u n - l)/2) (by linarith). If you want to see its type, you can just insert a line have := h ((u n - l)/2) (by linarith), and see the type of this in the tactic state

[Iocta]

this : ∃ (N : ℕ), ∀ (n_1 : ℕ), n_1 ≥ N → |u n_1 - l| ≤ (u n - l) / 2

[Jalex Stark]

that looks right; are you still confused about something?

[Iocta]

What is inductive about it?

[Jalex Stark]

\exists is an inductive constructor

[Jalex Stark]

so are \and and \or

[Patrick Massot]

https://leanprover-community.github.io/mathlib_docs/core/init/logic.html#Exists

[Bryan Gin-ge Chen]

Relevant TPiL section

[Iocta]

thanks, will review that