Gabriel Ebner

I'd like to reserve the [`letI`](https://github.com/leanprover-community/mathlib4/blob/f6714df2cc806810a95edc901f78d2f2da7dc577/Mathlib/Tactic/HaveI.lean#L21-L22) name for "inline" let, which does not produce a let-binding at all.

> But that's exactly what this is known as, a dependent let! The type of the body can depend on the value of the binding. Do you have a reference...

> was (morally) to hide the defeq `x = v` when typechecking `e` in `let x := v; e` and to introduce a `let dep` with the current behaviour Not...

David Renshaw just reminded me of another reason why hiding hypotheses is confusing: tactics can fail if you have extra hypotheses in the local context. (So you have to call...

See also the discussion at https://leanprover.zulipchat.com/#narrow/stream/147302-lean4-dev/topic/LeanPaths/near/289386295

I thought that was the last discussion on integrating the two, did a miss another one? You're right about the need to show conflicting information though, when `A` has different...

I'm not sure why you expect the goal state to change here. After `have h :=` comes a term, not a tactic. (It would be great though if the expected...

> Do you know why we are not getting the correct expected type here? I'm pretty sure that's because we look for the smallest term node around the cursor, but...

It would also be cool if the output was machine-readable.

Congratulations! You've found an exciting bug in `push_neg`! It was the usual missing `instantiateMVars`. There's still one failing test, I'll let you fix it. BTW, `guard_hyp foo : ty` works,...