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 leanprover-community/aesop#59. Co-authored-by: Scott Morrison <[email protected]>
leanprover-community · Jun 14, 2023 · 9558b65 · 9558b65
1 parent 6054b3d
commit 9558b65
Show file tree

Hide file tree

Showing 6 changed files with 16 additions and 15 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -172,23 +172,19 @@ 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) :
     ℱ.stalkPushforward C (𝟙 X) x = (stalkFunctor C x).map (Pushforward.id ℱ).hom := by
   -- 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