fix(tactic/norm_cast): make push_cast discharger match the others (#1…

…0021)

closes #9822



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

src/tactic/norm_cast.lean

@@ -321,7 +321,7 @@ end
 ```
 -/
 meta def push_cast (hs : parse tactic.simp_arg_list) (l : parse location) : tactic unit :=
-tactic.interactive.simp none none tt hs [`push_cast] l
+tactic.interactive.simp none none tt hs [`push_cast] l {discharger := tactic.assumption}
 
 
 end tactic.interactive
@@ -533,7 +533,8 @@ A small variant of `push_cast` suited for non-interactive use.
 -/
 meta def derive_push_cast (extra_lems : list simp_arg_type) (e : expr) : tactic (expr × expr) :=
 do (s, _) ← mk_simp_set tt [`push_cast] extra_lems,
-   (e, prf, _) ← simplify (s.erase [`int.coe_nat_succ]) [] e {fail_if_unchanged := ff},
+   (e, prf, _) ← simplify (s.erase [`int.coe_nat_succ]) [] e
+                  {fail_if_unchanged := ff} `eq tactic.assumption,
    return (e, prf)
 
 end norm_cast

test/linarith.lean

@@ -1,5 +1,4 @@
 import tactic.linarith
-import algebra.field_power
 
 example {α : Type} (_inst : Π (a : Prop), decidable a)
   [linear_ordered_field α]
@@ -395,3 +394,9 @@ example (x y : ℚ) (h₁ : 0 ≤ y) (h₂ : y ≤ x) : y * x ≤ x ^ 2 := by nl
 
 axiom foo {x : int} : 1 ≤ x → 1 ≤ x*x
 lemma bar (x y: int)(h : 0 ≤ y ∧ 1 ≤ x) : 1 ≤ y + x*x := by linarith [foo h.2]
+
+-- issue #9822
+lemma mytest (j : ℕ) (h : 0 < j) : j-1 < j:=
+begin
+  linarith,
+end