feat(tactic/tidy): lower the priority of ext in tidy (#1178)

* feat(category_theory/adjunction): additional simp lemmas

* experimenting with deferring ext in tidy

* abbreviate some proofs

* refactoring CommRing/adjunctions

* renaming

Author: kim-em

src/algebra/CommRing/adjunctions.lean

@@ -10,6 +10,8 @@ import algebra.CommRing.basic
 import category_theory.adjunction.basic
 import data.mv_polynomial
 
+noncomputable theory
+
 universe u
 
 open mv_polynomial
@@ -19,23 +21,27 @@ namespace CommRing
 
 local attribute [instance, priority 0] classical.prop_decidable
 
-noncomputable def polynomial_ring : Type u ⥤ CommRing.{u} :=
-{ obj := λ α, ⟨mv_polynomial α ℤ⟩,
-  map := λ α β f, ⟨rename f, by apply_instance⟩ }
+private def free_obj (α : Type u) : CommRing.{u} := ⟨mv_polynomial α ℤ⟩
+
+def free : Type u ⥤ CommRing.{u} :=
+{ obj := free_obj,
+  map := λ α β f, ⟨rename f, by apply_instance⟩, }
+
+@[simp] lemma free_obj_α {α : Type u} :
+  (free.obj α).α = mv_polynomial α ℤ := rfl
 
-@[simp] lemma polynomial_ring_obj_α {α : Type u} :
-  (polynomial_ring.obj α).α = mv_polynomial α ℤ := rfl
+@[simp] lemma free_map_val {α β : Type u} {f : α → β} :
+  (free.map f).val = rename f := rfl
 
-@[simp] lemma polynomial_ring_map_val {α β : Type u} {f : α → β} :
-  (polynomial_ring.map f).val = rename f := rfl
+def hom_equiv (α : Type u) (R : CommRing.{u}) : (free.obj α ⟶ R) ≃ (α ⟶ forget.obj R) :=
+{ to_fun    := λ f, f ∘ X,
+  inv_fun   := λ f, ⟨eval₂ (λ n : ℤ, (n : R)) f, by { unfold_coes, apply_instance }⟩,
+  left_inv  := λ f, bundled.hom_ext (@eval₂_hom_X _ _ _ _ _ _ f.val _),
+  right_inv := λ x, by { ext1, unfold_coes, simp only [function.comp_app, eval₂_X] } }
 
-noncomputable def adj : polynomial_ring ⊣ (forget : CommRing ⥤ Type u) :=
+def adj : free ⊣ (forget : CommRing ⥤ Type u) :=
 adjunction.mk_of_hom_equiv
-{ hom_equiv := λ α R,
-  { to_fun    := λ f, f ∘ X,
-    inv_fun   := λ f, ⟨eval₂ (λ n : ℤ, (n : R)) f, by { unfold_coes, apply_instance }⟩,
-    left_inv  := λ f, bundled.hom_ext (@eval₂_hom_X _ _ _ _ _ _ f.val _),
-    right_inv := λ x, by { ext1, unfold_coes, simp only [function.comp_app, eval₂_X] } },
+{ hom_equiv := hom_equiv,
   hom_equiv_naturality_left_symm' :=
   λ X X' Y f g, by { ext1, dsimp, apply eval₂_cast_comp } }.
 

src/category_theory/adjunction/limits.lean

@@ -29,24 +29,8 @@ def functoriality_is_left_adjoint :
 { right := (cocones.functoriality G) ⋙ (cocones.precompose
     (K.right_unitor.inv ≫ (whisker_left K adj.unit) ≫ (associator _ _ _).inv)),
   adj := mk_of_unit_counit
-  { unit :=
-    { app := λ c,
-      { hom := adj.unit.app c.X,
-        w' := λ j, by have := adj.unit.naturality (c.ι.app j); tidy },
-      naturality' := λ _ _ f, by have := adj.unit.naturality (f.hom); tidy },
-    counit :=
-    { app := λ c,
-      { hom := adj.counit.app c.X,
-        w' :=
-        begin
-          intro j,
-          dsimp,
-          erw [category.comp_id, category.id_comp, F.map_comp, category.assoc,
-            adj.counit.naturality (c.ι.app j), ← category.assoc,
-            adj.left_triangle_components, category.id_comp],
-          refl,
-        end },
-      naturality' := λ _ _ f, by have := adj.counit.naturality (f.hom); tidy } } }
+  { unit := { app := λ c, { hom := adj.unit.app c.X } },
+    counit := { app := λ c, { hom := adj.counit.app c.X } } } }
 
 /-- A left adjoint preserves colimits. -/
 def left_adjoint_preserves_colimits : preserves_colimits F :=
@@ -67,24 +51,8 @@ def functoriality_is_right_adjoint :
 { left := (cones.functoriality F) ⋙ (cones.postcompose
     ((associator _ _ _).hom ≫ (whisker_left K adj.counit) ≫ K.right_unitor.hom)),
   adj := mk_of_unit_counit
-  { unit :=
-    { app := λ c,
-      { hom := adj.unit.app c.X,
-        w' :=
-        begin
-          intro j,
-          dsimp,
-          erw [category.comp_id, category.id_comp, G.map_comp, ← category.assoc,
-            ← adj.unit.naturality (c.π.app j), category.assoc,
-            adj.right_triangle_components, category.comp_id],
-          refl,
-        end },
-      naturality' := λ _ _ f, by have := adj.unit.naturality (f.hom); tidy },
-    counit :=
-    { app := λ c,
-      { hom := adj.counit.app c.X,
-        w' := λ j, by have := adj.counit.naturality (c.π.app j); tidy },
-      naturality' := λ _ _ f, by have := adj.counit.naturality (f.hom); tidy } } }
+  { unit := { app := λ c, { hom := adj.unit.app c.X, } },
+    counit := { app := λ c, { hom := adj.counit.app c.X, } } } }
 
 /-- A right adjoint preserves limits. -/
 def right_adjoint_preserves_limits : preserves_limits G :=
@@ -110,12 +78,7 @@ nat_iso.of_components (λ Y,
         erw [← adj.hom_equiv_naturality_left_symm, ← adj.hom_equiv_naturality_right_symm, t.naturality],
         dsimp, simp
       end } } )
-begin
-  intros Y₁ Y₂ f,
-  ext1 t,
-  ext1 j,
-  apply adj.hom_equiv_naturality_right
-end
+(by tidy)
 
 -- Note: this is natural in K, but we do not yet have the tools to formulate that.
 def cones_iso {J : Type v} [small_category J] {K : J ⥤ D} :

src/tactic/tidy.lean

@@ -44,12 +44,12 @@ meta def default_tactics : list (tactic string) :=
 [ reflexivity                                 >> pure "refl",
   `[exact dec_trivial]                        >> pure "exact dec_trivial",
   propositional_goal >> assumption            >> pure "assumption",
-  ext1_wrapper,
   intros1                                     >>= λ ns, pure ("intros " ++ (" ".intercalate (ns.map (λ e, e.to_string)))),
   auto_cases,
   `[apply_auto_param]                         >> pure "apply_auto_param",
   `[dsimp at *]                               >> pure "dsimp at *",
   `[simp at *]                                >> pure "simp at *",
+  ext1_wrapper,
   fsplit                                      >> pure "fsplit",
   injections_and_clear                        >> pure "injections_and_clear",
   propositional_goal >> (`[solve_by_elim])    >> pure "solve_by_elim",