linter.fugue.byAssumption

f (by assumption) opens a tactic block to do what a term already says, and hides which hypothesis is meant. Write ‹_›, or ‹T› when the type reads.