feat(apply_fun): handle implicit arguments (#6091)

I've modified the way `apply_fun` handles inequalities, by building an intermediate expression before calling `mono` to discharge the `monotone f` subgoal. This has the effect of sometimes filling in implicit arguments successfully, so that `mono` works.

In `tests/apply_fun.lean` I've added an example showing this in action 


Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/tactic/apply_fun.lean

@@ -22,14 +22,20 @@ do {
       to_expr ``(congr_arg (%%e : %%ltp → %%mv) %%hyp)
   | `(%%l ≤ %%r) := do
        Hmono ← match mono_lem with
-               | some mono_lem :=
-                 tactic.i_to_expr mono_lem
-               | none := do
-                 n ← get_unused_name `mono,
-                 to_expr ``(monotone %%e) >>= assert n,
-                 do { intro_lst [`x, `y, `h], `[dsimp, mono], skip } <|> swap,
-                 get_local n
-               end,
+        | some mono_lem :=
+          tactic.i_to_expr mono_lem
+        | none := do
+          n ← get_unused_name `mono,
+          to_expr ``(monotone %%e) >>= assert n,
+          -- In order to resolve implicit arguments in `%%e`,
+          -- we build (and discard) the expression `%%n %%hyp` before calling the `mono` tactic.
+          swap,
+          n ← get_local n,
+          to_expr ``(%%n %%hyp),
+          swap,
+          do { intro_lst [`x, `y, `h], `[try { dsimp }, mono] } <|> swap,
+          return n
+        end,
        to_expr ``(%%Hmono %%hyp)
   | _ := fail ("failed to apply " ++ to_string e ++ " at " ++ to_string hyp.local_pp_name)
   end,

src/tactic/monotonicity/lemmas.lean

@@ -71,7 +71,7 @@ open set
 attribute [mono] inter_subset_inter union_subset_union
                  sUnion_mono bUnion_mono sInter_subset_sInter bInter_mono
                  image_subset preimage_mono prod_mono monotone_prod seq_mono
-                 image2_subset
+                 image2_subset order_embedding.monotone
 attribute [mono] upper_bounds_mono_set lower_bounds_mono_set
                  upper_bounds_mono_mem  lower_bounds_mono_mem
                  upper_bounds_mono  lower_bounds_mono

test/apply_fun.lean

@@ -47,3 +47,10 @@ begin
   guard_hyp' h : f (A * B) = f 0,
   exact h,
 end
+
+-- Verify that `apply_fun` works with `fin.cast_succ`, even though it has an implicit argument.
+example (n : ℕ) (a b : fin n) (H : a ≤ b) : a.cast_succ ≤ b.cast_succ :=
+begin
+  apply_fun fin.cast_succ at H,
+  exact H,
+end