Try #281:

library/init/meta/interactive.lean

@@ -243,16 +243,25 @@ Note that some holes may be implicit. The type of each hole must either be synth
 meta def refine (q : parse texpr) : tactic unit :=
 tactic.refine q
 
+precedence `?`:max
 /--
-This tactic looks in the local context for a hypothesis whose type is equal to the goal target. If it finds one, it uses it to prove the goal, and otherwise it fails.
+This tactic looks in the local context for a hypothesis whose type is equal to the goal target.
+If it finds one, it uses it to prove the goal, and otherwise it fails.
+`assumption?` will print the name of the goal that it found.
 -/
-meta def assumption : tactic unit :=
-tactic.assumption
+meta def assumption (trace_result : parse $ optional (tk "?")) :=
+tactic.assumption trace_result.is_some
+
 
 /-- Try to apply `assumption` to all goals. -/
 meta def assumption' : tactic unit :=
 tactic.any_goals' tactic.assumption
 
+
+/-- Try to apply `assumption` to all goals. -/
+meta def assumption'' : tactic unit :=
+tactic.assumption
+
 private meta def change_core (e : expr) : option expr → tactic unit
 | none     := tactic.change e
 | (some h) :=
@@ -411,7 +420,7 @@ propagate_tags (rw_core q l cfg)
 `rewrite` followed by `assumption`.
 -/
 meta def rwa (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {}) : tactic unit :=
-rewrite q l cfg >> try assumption
+rewrite q l cfg >> try tactic.assumption
 
 /--
 A variant of `rewrite` that uses the unifier more aggressively, unfolding semireducible definitions.
@@ -1045,13 +1054,13 @@ If `q` is a proof of a statement of conclusion `t₁ = t₂`, then injection app
 Given `h : a::b = c::d`, the tactic `injection h` adds two new hypothesis with types `a = c` and `b = d` to the main goal. The tactic `injection h with h₁ h₂` uses the names `h₁` and `h₂` to name the new hypotheses.
 -/
 meta def injection (q : parse texpr) (hs : parse with_ident_list) : tactic unit :=
-do e ← i_to_expr q, tactic.injection_with e hs, try assumption
+do e ← i_to_expr q, tactic.injection_with e hs, try tactic.assumption
 
 /--
 `injections with h₁ ... hₙ` iteratively applies `injection` to hypotheses using the names `h₁ ... hₙ`.
 -/
 meta def injections (hs : parse with_ident_list) : tactic unit :=
-do tactic.injections_with hs, try assumption
+do tactic.injections_with hs, try tactic.assumption
 
 end interactive
 

library/init/meta/tactic.lean

@@ -948,10 +948,21 @@ meta def find_same_type : expr → list expr → tactic expr
 meta def find_assumption (e : expr) : tactic expr :=
 do ctx ← local_context, find_same_type e ctx
 
-meta def assumption : tactic unit :=
+meta def is_implicit : expr → bool
+| (expr.pi _ binder_info.implicit _ _) := tt
+| _ := ff
+
+/-- Find a hypothesis matching the goal. `assumption tt` will print the goal that it found.
+    If the goal type starts with an implicit binder, prints an "@" in front. -/
+meta def assumption (trace_result : bool := ff) : tactic unit :=
 do { ctx ← local_context,
      t   ← target,
      H   ← find_same_type t ctx,
+     when trace_result $
+       do { pp_H ← pp H,
+         H_type ← tactic.infer_type H,
+         let H_format := if is_implicit H_type then ↑"@" ++ pp_H else pp_H,
+         trace ( ("Try this: exact " : format) ++ H_format) },
      exact H }
 <|> fail "assumption tactic failed"
 

tests/lean/apply_tac.lean

@@ -51,15 +51,15 @@ rfl
 
 open tactic
 
-lemma foo {a b c : nat} (h₁ : a = b) (h₂ : b = c . assumption) : a = c :=
+lemma foo {a b c : nat} (h₁ : a = b) (h₂ : b = c . assumption'') : a = c :=
 eq.trans h₁ h₂
 
 example (a b c : nat) (h₁ : a = b) (h₂ : b = c) : a = c :=
 begin
   apply @foo a b c h₁ -- uses auto_param for solving goal
 end
 
-lemma my_div_self (a : nat) (h : a ≠ 0 . assumption) : a / a = 1 :=
+lemma my_div_self (a : nat) (h : a ≠ 0 . assumption'') : a / a = 1 :=
 sorry
 
 example (a : nat) (h : a ≠ 0) : a / a = 1 :=

tests/lean/assumption.lean

@@ -0,0 +1,9 @@
+example (p : Prop) (h1 : p) : p :=
+begin
+  assumption?,
+end
+
+example (p : Prop) (h2 : ∀ {x : ℕ}, p) : ∀ x : ℕ, p :=
+begin
+  assumption?,
+end

tests/lean/assumption.lean.expected.out

@@ -0,0 +1,2 @@
+Try this: exact h1
+Try this: exact @h2

tests/lean/run/rw1.lean

@@ -62,7 +62,7 @@ open tactic
 constant f : nat → nat
 constant p : nat → Prop
 /- The following lemma has an "auto_param", i.e., if `h` is not provided we
-   try to synthesize it using the `assumption` tactic -/
+   try to synthesize it using the `assumption''` tactic -/
 lemma f_lemma (a : nat) (h : p a . assumption) : f a = a :=
 sorry