Ring tactic fix (#39)

* aligned tactic names to mathport

* added byContra tactic

* added guardExprEq guardTarget guardHyp

* added introv

* Update Mathlib/Tactic/Basic.lean

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

* Update Mathlib/Tactic/Basic.lean

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

* added exacts

* use of elab and examples

* matchTarget

* byContra all cases

* sorry & iterate

* fix : get to build

* fix : get to build

* fix : get to build 3

* fix : alpha eq in guardHyp but consuming mdata

* feat : repeat' tactic

* feat : anyGoals tactic

* feat(Algebra/Group/Defs): Monoid lemmas

* feat(Tactic/Ring): starting ring

* fix: fixed normNum

* fix : compatibility Numeric.ofNat with One.one and Zero.zero

* fix : removed print

* fix: fixed normNum

* feat: ring with only additions and one variable

* feat: ring tactic furnctional for addition and multiplication

* feat(Algebra) : more lemmas

* feat (Tactic/NormNum) : normNum exponentiation

* feat (Tactic/Ring) : exponentiation for ring

* fix : updated with new version of mkNatLit

* fix : import ring

* chore : update to newer lean version

* doc (Tactic/Ring) : add author

* fix(Algebra/Group/Defs) : Monoid.npow

* chore(Tactic/Ring) : updated to new lean version

* fix(Tactic/Ring) : fixed issue with constant multiplication

Co-authored-by: Aurélien SAUE <aurelien.saue@polytechnique.edu>
Co-authored-by: Gabriel Ebner <gebner@gebner.org>

Mathlib/Tactic/Ring.lean

@@ -243,8 +243,7 @@ by simp [h₂.symm, h₁.symm, horner, add_mul, @mul_right_comm α _]
 /-- Evaluate `k * a` where `k` is a rational numeral and `a` is in normal form. -/
 def evalConstMul (k : Expr × ℕ) : HornerExpr → RingM (HornerExpr × Expr)
 | (const e coeff) => do
-  let e' ← mkRawNatLit (k.2 * coeff)
-  let p ← mkEqRefl e'
+  let (e', p) ← NormNum.eval $ ← mkMul k.1 e
   return (const e' (k.2 * coeff), p)
 | (xadd e a x n b) => do
   let (a', h₁) ← evalConstMul k a