Commit 2021-08-12 12:16 3ce73ce7

View on Github →

Tactic implementations (#30)

  • aligned tactic names to mathport
  • added byContra tactic
  • added guardExprEq guardTarget guardHyp
  • added introv
  • Update Mathlib/Tactic/Basic.lean
  • Update Mathlib/Tactic/Basic.lean
  • 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

Estimated changes

modified theorem mul_one
added theorem npow_eq_pow
added theorem npow_succ'
added theorem npow_zero'
modified theorem one_mul