Plain local hypotheses for long analytic proofs #
have! h : T := v (or have! h := v) adds the hypothesis h : T proved by v as a plain
local hypothesis. Unlike have, the proof v does not stay in the local context as the value
of h, and unlike obtain h : T := v, nothing is generalized in the goal. Both matter in very
long tactic proofs: every nested by block instantiates the whole local context (including the
values of earlier haves), and obtain traverses the goal at every step.
Equations
- One or more equations did not get rendered due to their size.