assumption?

library/init/meta/interactive.lean

@@ -244,10 +244,13 @@ meta def refine (q : parse texpr) : tactic unit :=
 tactic.refine q
 
 /--
-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 :=

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/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,3 @@
+-{"msgs":[{"caption":"trace output","file_name":"assumption.lean","pos_col":2,"pos_line":3,"severity":"information","text":"Try this: h1\n"}],"response":"all_messages"}
+-{"msgs":[{"caption":"trace output","file_name":"assumption.lean","pos_col":2,"pos_line":3,"severity":"information","text":""Try this: @h1\n"},"response":"all_messages"]
+-{"message":"file invalidated","response":"ok","seq_num":0}