fix(tactic/norm_cast): assumption_mod_cast should only work on one go…

…al (#8649)

fixes #8438 



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>

src/tactic/norm_cast.lean

@@ -583,7 +583,7 @@ decorate_error "assumption_mod_cast failed:" $ do
   },
   replace_at derive [] tt,
   ctx ← local_context,
-  try_lst $ ctx.map (λ h, aux_mod_cast h ff >>= tactic.exact)
+  ctx.mfirst (λ h, aux_mod_cast h ff >>= tactic.exact)
 
 end tactic
 

test/norm_cast.lean

@@ -126,3 +126,10 @@ begin
 end
 
 end ennreal
+
+lemma b (h g : true) : true ∧ true :=
+begin
+ split,
+ assumption_mod_cast,
+ assumption_mod_cast,
+end