assume e introduces a new (unnamed) hypothesis of type e.
It is equivalent to intro (_ : e).
The argument e is required to be a proposition, definitionally equal to the hypothesis
(or domain of a dependent function) in the goal. The introduced hypothesis will have
the exact form the user wrote.
Example:
example {α} (f : α → α) (h : Function.Injective f) : ∀ x y, f x = f y → x = y := by
intro x y
assume f x = f y
apply h
assumption
Equations
- One or more equations did not get rendered due to their size.