Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-10-31 23:37 df916232

View on Github →

chore(category_theory/whiskering): clean up (#1613)

chore(category_theory/whiskering): clean up
ugh, the stalks proofs are so fragile
fixes
minor
fix
fix

Estimated changes

Modified src/algebraic_geometry/stalks.lean

Modified src/category_theory/monad/limits.lean

Modified src/category_theory/opposites.lean

deleted theorem category_theory.nat_trans.op_app

added theorem category_theory.nat_trans.op_id

deleted theorem category_theory.nat_trans.unop_app

added theorem category_theory.nat_trans.unop_id

Modified src/category_theory/whiskering.lean

deleted theorem category_theory.whisker_left.app

modified def category_theory.whisker_left

deleted theorem category_theory.whisker_right.app

modified def category_theory.whisker_right

modified def category_theory.whiskering_left

deleted theorem category_theory.whiskering_left_map_app_app

deleted theorem category_theory.whiskering_left_obj_map

deleted theorem category_theory.whiskering_left_obj_obj

modified def category_theory.whiskering_right

deleted theorem category_theory.whiskering_right_map_app_app

deleted theorem category_theory.whiskering_right_obj_map

deleted theorem category_theory.whiskering_right_obj_obj

Modified src/topology/sheaves/stalks.lean