Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-28 19:38 3f65a930

View on Github →

fix(tactic/restate_axiom): change default naming in restate_axiom (#286)

beginning renaming
modifying names in restate_axiom
removing ematch attributes from category_theory
improving behaviour of restate_axiom, documenting and testing
oops

Estimated changes

Modified category_theory/category.lean

Modified category_theory/functor.lean

added theorem category_theory.functor.map_comp

deleted theorem category_theory.functor.map_comp_lemma

added theorem category_theory.functor.map_id

deleted theorem category_theory.functor.map_id_lemma

Modified category_theory/functor_category.lean

modified theorem category_theory.functor.category.comp_app

modified theorem category_theory.functor.category.id_app

modified theorem category_theory.functor.category.nat_trans.app_naturality

modified theorem category_theory.functor.category.nat_trans.naturality_app

Modified category_theory/natural_transformation.lean

modified theorem category_theory.nat_trans.exchange

added theorem category_theory.nat_trans.naturality

deleted theorem category_theory.nat_trans.naturality_lemma

modified theorem category_theory.nat_trans.vcomp_assoc

Modified category_theory/opposites.lean

Modified category_theory/products.lean

modified theorem category_theory.functor.prod_map

modified theorem category_theory.functor.prod_obj

modified theorem category_theory.nat_trans.prod_app

modified theorem category_theory.prod_comp

modified theorem category_theory.prod_id

Modified category_theory/types.lean

modified theorem category_theory.functor_to_types.map_comp

modified theorem category_theory.functor_to_types.map_id

modified theorem category_theory.functor_to_types.naturality

Modified docs/tactics.md

Modified tactic/restate_axiom.lean

Created tests/restate_axiom.lean

added structure A