I was playing around with degree 2 polynomials:

```
Lemma deg2_poly_canonical (a b c : R) : a <> 0 ->
let delta := (b² - 4 * a * c) in
forall x, (a * x² + b * x + c = a * ((x + b / (2 * a))² - delta / (4 * a²))).
Proof. intros H delta x; subst delta; unfold Rsqr; field; exact H. Qed.
Lemma deg2_poly_neg_a_evtly_neg (a b c : R) : a < 0 ->
exists alpha, (forall x, x > alpha -> a * x² + b * x + c < 0).
Proof.
intros H; assert (Hn0 : a <> 0) by (now apply Rlt_not_eq).
pose proof (deg2_poly_canonical a b c Hn0) as Eq.
```

Now, the proof state is:

```
a, b, c : R
H : a < 0
Hn0 : a <> 0
Eq : let delta := b² - 4 * a * c in
forall x : R,
a * x² + b * x + c = a * ((x + b / (2 * a))² - delta / (4 * a²))
========================= (1 / 1)
exists alpha : R, forall x : R, x > alpha -> a * x² + b * x + c < 0
```

What I would like to do is `do_something_with Eq`

such that `delta`

appears with its let-in definition in the context so that I don't have to write it manually. In math this would be "let delta be as in Lemma deg2_poly_canonical".

Is there an easy way to do so? Bonus points if it can be done with an intro pattern at the time of `pose proof`

.

Hi. If you know that the `let`

is the top construct of you hypothesis you can write an tactic for this:

```
Require Import Utf8.
Lemma foo: ∀ x y:nat, (let delta := x + y in delta < delta * 2) -> True.
Proof.
intros x y H.
match type of H with
(let xxx := ?c in ?a) =>
pose (xxx := c)
end.
```

sounds similar to https://github.com/coq/coq/issues/17554

Last updated: Jun 18 2024 at 22:01 UTC