term mode equivalent of resetI?

Stream: new members

[Justus Springer]

I'm in a situation similar to this:

import category_theory.isomorphism

open category_theory

variables {C : Type*} [category C]

noncomputable def foo {X Y : C} (f : X ⟶ Y) : Π [h : is_iso f], Y ⟶ X := λ i,
begin
  resetI,
  exact inv f,
end

Only instead of the exact inv f, imagine a more complicated term, using the local instance i in multiple places. I'm a little annoyed that I have to go into tactic mode, just for the resetI. Can I avoid this somehow? The only alternative I see is using @ and passing instances around explicitly, but that seems more complicated than it needs to be...

[Eric Rodriguez]

by exactI is the common hack I think, but it's not a great situation

[Alex J. Best]

Its so common there was even some fancy notation for it for LTE https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/by.20exactI/near/222908190

[Eric Rodriguez]

the notation is actually now a zero-width space, as they use it so much

[Justus Springer]

Thanks, I didn't know about exactI.

[Justus Springer]

The best way to learn a new tactic is by discovering its use case independently :)