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