From 03ab8168618c1486a4d45a80fee1d9e1d4aab78b Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 14 Jun 2023 07:27:14 +0000 Subject: [PATCH] chore: clean up porting notes about op_induction (#5035) Closes #4551. Essentially `op_induction` is not necessary, now that `Opposite.rec'` is labelled with `@[eliminator]`. It would be nice if we could use this from inside `aesop`, see https://github.com/JLimperg/aesop/issues/59. Co-authored-by: Scott Morrison --- Mathlib/AlgebraicGeometry/PresheafedSpace.lean | 3 ++- Mathlib/AlgebraicGeometry/SheafedSpace.lean | 3 ++- Mathlib/AlgebraicGeometry/Stalks.lean | 2 +- Mathlib/Mathport/Syntax.lean | 2 -- Mathlib/Topology/Sheaves/Presheaf.lean | 11 ++++++++--- Mathlib/Topology/Sheaves/Stalks.lean | 10 +++------- 6 files changed, 16 insertions(+), 15 deletions(-) diff --git a/Mathlib/AlgebraicGeometry/PresheafedSpace.lean b/Mathlib/AlgebraicGeometry/PresheafedSpace.lean index b4466dc81013a1..26c9138280b597 100644 --- a/Mathlib/AlgebraicGeometry/PresheafedSpace.lean +++ b/Mathlib/AlgebraicGeometry/PresheafedSpace.lean @@ -36,7 +36,8 @@ variable (C : Type _) [Category C] -- local attribute [tidy] tactic.op_induction' -- A possible replacement would be: -- attribute [local aesop safe cases (rule_sets [CategoryTheory])] Opposite --- but it doesn't seem necessary here. +-- but this would probably require https://github.com/JLimperg/aesop/issues/59 +-- In any case, it doesn't seem necessary here. namespace AlgebraicGeometry diff --git a/Mathlib/AlgebraicGeometry/SheafedSpace.lean b/Mathlib/AlgebraicGeometry/SheafedSpace.lean index 590ddd96a0702a..3a095bb07e0aef 100644 --- a/Mathlib/AlgebraicGeometry/SheafedSpace.lean +++ b/Mathlib/AlgebraicGeometry/SheafedSpace.lean @@ -33,7 +33,8 @@ variable (C : Type u) [Category.{v} C] -- local attribute [tidy] tactic.op_induction' -- as it isn't needed here. If it is useful elsewhere -- attribute [local aesop safe cases (rule_sets [CategoryTheory])] Opposite --- should suffice. +-- should suffice, but may need +-- https://github.com/JLimperg/aesop/issues/59 namespace AlgebraicGeometry diff --git a/Mathlib/AlgebraicGeometry/Stalks.lean b/Mathlib/AlgebraicGeometry/Stalks.lean index 3eb1aa3311e4bf..29861c6482362c 100644 --- a/Mathlib/AlgebraicGeometry/Stalks.lean +++ b/Mathlib/AlgebraicGeometry/Stalks.lean @@ -31,7 +31,7 @@ open Opposite CategoryTheory CategoryTheory.Category CategoryTheory.Functor Cate variable {C : Type u} [Category.{v} C] [HasColimits C] -- Porting note : no tidy tactic --- attribute [local tidy] tactic.op_induction' tactic.auto_cases_opens +-- attribute [local tidy] tactic.auto_cases_opens -- this could be replaced by -- attribute [local aesop safe cases (rule_sets [CategoryTheory])] Opens -- but it doesn't appear to be needed here. diff --git a/Mathlib/Mathport/Syntax.lean b/Mathlib/Mathport/Syntax.lean index 19cfa792641003..7f6f6d21ac15c8 100644 --- a/Mathlib/Mathport/Syntax.lean +++ b/Mathlib/Mathport/Syntax.lean @@ -260,8 +260,6 @@ syntax termList := " [" term,* "]" /- E -/ syntax (name := isBounded_default) "isBounded_default" : tactic -/- N -/ syntax (name := opInduction) "op_induction" (ppSpace colGt term)? : tactic - /- S -/ syntax (name := mvBisim) "mv_bisim" (ppSpace colGt term)? (" with" (ppSpace binderIdent)+)? : tactic diff --git a/Mathlib/Topology/Sheaves/Presheaf.lean b/Mathlib/Topology/Sheaves/Presheaf.lean index 8b316b9acf68aa..3dc54b57058e2e 100644 --- a/Mathlib/Topology/Sheaves/Presheaf.lean +++ b/Mathlib/Topology/Sheaves/Presheaf.lean @@ -223,12 +223,17 @@ theorem id_hom_app' (U) (p) : (id ℱ).hom.app (op ⟨U, p⟩) = ℱ.map (𝟙 ( set_option linter.uppercaseLean3 false in #align Top.presheaf.pushforward.id_hom_app' TopCat.Presheaf.Pushforward.id_hom_app' --- porting note: TODO: attribute [local tidy] tactic.op_induction' +-- Porting note: +-- the proof below could be `by aesop_cat` if +-- https://github.com/JLimperg/aesop/issues/59 +-- can be resolved, and we add: +attribute [local aesop safe cases (rule_sets [CategoryTheory])] Opposite +attribute [local aesop safe cases (rule_sets [CategoryTheory])] Opens @[simp] theorem id_hom_app (U) : (id ℱ).hom.app U = ℱ.map (eqToHom (Opens.op_map_id_obj U)) := by - -- was `tidy` - induction' U with U + -- was `tidy`, see porting note above. + induction U apply id_hom_app' set_option linter.uppercaseLean3 false in #align Top.presheaf.pushforward.id_hom_app TopCat.Presheaf.Pushforward.id_hom_app diff --git a/Mathlib/Topology/Sheaves/Stalks.lean b/Mathlib/Topology/Sheaves/Stalks.lean index c99e2e7b3908d8..535ed2d6c24b6c 100644 --- a/Mathlib/Topology/Sheaves/Stalks.lean +++ b/Mathlib/Topology/Sheaves/Stalks.lean @@ -172,9 +172,8 @@ set_option linter.uppercaseLean3 false in -- (colim.map (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) ℱ) : -- colim.obj ((OpenNhds.inclusion (f x) ⋙ Opens.map f).op ⋙ ℱ) ⟶ _) ≫ -- colimit.pre ((OpenNhds.inclusion x).op ⋙ ℱ) (OpenNhds.map f x).op -namespace stalkPushforward --- Porting note: TODO: attribute [local tidy] tactic.op_induction' +namespace stalkPushforward @[simp] theorem id (ℱ : X.Presheaf C) (x : X) : @@ -182,13 +181,10 @@ theorem id (ℱ : X.Presheaf C) (x : X) : -- Porting note: We need to this to help ext tactic. change (_ : colimit _ ⟶ _) = (_ : colimit _ ⟶ _) ext1 j - induction' j using Opposite.rec with j - -- Porting note: unsupported non-interactive tactic tactic.op_induction' - -- run_tac - -- tactic.op_induction' + induction' j with j rcases j with ⟨⟨_, _⟩, _⟩ erw [colimit.ι_map_assoc] - simpa [stalkFunctor, stalkPushforward] using by rfl + simp [stalkFunctor, stalkPushforward] set_option linter.uppercaseLean3 false in #align Top.presheaf.stalk_pushforward.id TopCat.Presheaf.stalkPushforward.id