refactor(data/opposite): Remove the op_induction tactic (#9660)

The `induction` tactic is already powerful enough for this; we don't have `order_dual_induction` or `nat_induction` as tactics. The bulk of this change is replacing `op_induction x` with `induction x using opposite.rec`. This leaves behind the non-interactive `op_induction'` which is still needed as a `tidy` hook. This also renames the def `opposite.op_induction` to `opposite.rec` to match `order_dual.rec` etc.
leanprover-community · Oct 12, 2021 · 2e72f35 · 2e72f35
1 parent ad4040d
commit 2e72f35
Show file tree

Hide file tree

Showing 11 changed files with 44 additions and 58 deletions.
diff --git a/src/algebra/algebra/basic.lean b/src/algebra/algebra/basic.lean
@@ -384,7 +384,7 @@ instance : algebra R Aᵒᵖ :=
 { to_ring_hom := (algebra_map R A).to_opposite $ λ x y, algebra.commutes _ _,
   smul_def' := λ c x, unop_injective $
     by { dsimp, simp only [op_mul, algebra.smul_def, algebra.commutes, op_unop] },
-  commutes' := λ r, op_induction $ λ x, by dsimp; simp only [← op_mul, algebra.commutes],
+  commutes' := λ r, opposite.rec $ λ x, by dsimp; simp only [← op_mul, algebra.commutes],
   ..opposite.has_scalar A R }
 
 @[simp] lemma algebra_map_apply (c : R) : algebra_map R Aᵒᵖ c = op (algebra_map R A c) := rfl

diff --git a/src/algebra/opposites.lean b/src/algebra/opposites.lean
@@ -323,7 +323,7 @@ instance _root_.is_scalar_tower.opposite_mid {M N} [monoid N] [has_scalar M N]
 instance _root_.smul_comm_class.opposite_mid {M N} [monoid N] [has_scalar M N]
   [is_scalar_tower M N N] :
   smul_comm_class M Nᵒᵖ N :=
-⟨λ x y z, by { induction y using opposite.op_induction, simp [smul_mul_assoc] }⟩
+⟨λ x y z, by { induction y using opposite.rec, simp [smul_mul_assoc] }⟩
 
 -- The above instance does not create an unwanted diamond, the two paths to
 -- `mul_action (opposite α) (opposite α)` are defeq.
@@ -442,7 +442,7 @@ def ring_hom.to_opposite {R S : Type*} [semiring R] [semiring S] (f : R →+* S)
 /-- The units of the opposites are equivalent to the opposites of the units. -/
 def units.op_equiv {R} [monoid R] : units Rᵒᵖ ≃* (units R)ᵒᵖ :=
 { to_fun := λ u, op ⟨unop u, unop ↑(u⁻¹), op_injective u.4, op_injective u.3⟩,
-  inv_fun := op_induction $ λ u, ⟨op ↑(u), op ↑(u⁻¹), unop_injective $ u.4, unop_injective u.3⟩,
+  inv_fun := opposite.rec $ λ u, ⟨op ↑(u), op ↑(u⁻¹), unop_injective $ u.4, unop_injective u.3⟩,
   map_mul' := λ x y, unop_injective $ units.ext $ rfl,
   left_inv := λ x, units.ext $ rfl,
   right_inv := λ x, unop_injective $ units.ext $ rfl }

diff --git a/src/algebra/quandle.lean b/src/algebra/quandle.lean
@@ -172,16 +172,16 @@ The opposite rack, swapping the roles of `◃` and `◃⁻¹`.
 instance opposite_rack : rack Rᵒᵖ :=
 { act := λ x y, op (inv_act (unop x) (unop y)),
   self_distrib := λ (x y z : Rᵒᵖ), begin
-    op_induction x, op_induction y, op_induction z,
+    induction x using opposite.rec, induction y using opposite.rec, induction z using opposite.rec,
     simp only [unop_op, op_inj_iff],
     exact self_distrib_inv,
   end,
   inv_act := λ x y, op (shelf.act (unop x) (unop y)),
   left_inv := λ x y, begin
-    op_induction x, op_induction y, simp,
+    induction x using opposite.rec, induction y using opposite.rec, simp,
   end,
   right_inv := λ x y, begin
-    op_induction x, op_induction y, simp,
+    induction x using opposite.rec, induction y using opposite.rec, simp,
   end }
 
 @[simp] lemma op_act_op_eq {x y : R} : (op x) ◃ (op y) = op (x ◃⁻¹ y) := rfl
@@ -298,7 +298,7 @@ lemma fix_inv {x : Q} : x ◃⁻¹ x = x :=
 by { rw ←left_cancel x, simp }
 
 instance opposite_quandle : quandle Qᵒᵖ :=
-{ fix := λ x, by { op_induction x, simp } }
+{ fix := λ x, by { induction x using opposite.rec, simp } }
 
 /--
 The conjugation quandle of a group.  Each element of the group acts by

diff --git a/src/algebraic_geometry/presheafed_space.lean b/src/algebraic_geometry/presheafed_space.lean
@@ -105,7 +105,7 @@ instance category_of_PresheafedSpaces : category (PresheafedSpace C) :=
   begin
     ext1, swap,
     { dsimp, simp only [id_comp] },  -- See note [dsimp, simp].
-    { ext U, op_induction, cases U,
+    { ext U, induction U using opposite.rec, cases U,
       dsimp,
       simp only [presheaf.pushforward.comp_inv_app, opens.map_iso_inv_app],
       dsimp,
@@ -115,7 +115,7 @@ instance category_of_PresheafedSpaces : category (PresheafedSpace C) :=
   begin
     ext1, swap,
     { dsimp, simp only [comp_id] },
-    { ext U, op_induction, cases U,
+    { ext U, induction U using opposite.rec, cases U,
       dsimp,
       simp only [presheaf.pushforward.comp_inv_app, opens.map_iso_inv_app],
       dsimp,
@@ -125,7 +125,7 @@ instance category_of_PresheafedSpaces : category (PresheafedSpace C) :=
   begin
      ext1, swap,
      refl,
-     { ext U, op_induction, cases U,
+     { ext U, induction U using opposite.rec, cases U,
        dsimp,
        simp only [assoc, presheaf.pushforward.comp_inv_app, opens.map_iso_inv_app],
        dsimp,
@@ -144,8 +144,8 @@ lemma id_c (X : PresheafedSpace C) :
   (functor.left_unitor _).inv ≫ whisker_right (nat_trans.op (opens.map_id X.carrier).hom) _ := rfl
 
 @[simp] lemma id_c_app (X : PresheafedSpace C) (U) :
-  ((𝟙 X) : X ⟶ X).c.app U = eq_to_hom (by { op_induction U, cases U, refl }) :=
-by { op_induction U, cases U, simp only [id_c], dsimp, simp, }
+  ((𝟙 X) : X ⟶ X).c.app U = eq_to_hom (by { induction U using opposite.rec, cases U, refl }) :=
+by { induction U using opposite.rec, cases U, simp only [id_c], dsimp, simp, }
 
 @[simp] lemma comp_base {X Y Z : PresheafedSpace C} (f : X ⟶ Y) (g : Y ⟶ Z) :
   (f ≫ g).base = f.base ≫ g.base := rfl
@@ -214,13 +214,14 @@ def restrict_top_iso (X : PresheafedSpace C) :
 { hom := X.of_restrict _ _,
   inv := X.to_restrict_top,
   hom_inv_id' := ext _ _ (concrete_category.hom_ext _ _ $ λ ⟨x, _⟩, rfl) $
-    nat_trans.ext _ _ $ funext $ λ U, by { op_induction U,
+    nat_trans.ext _ _ $ funext $ λ U, by { induction U using opposite.rec,
       dsimp only [nat_trans.comp_app, comp_c_app, to_restrict_top, of_restrict,
           whisker_right_app, comp_base, nat_trans.op_app, opens.map_iso_inv_app],
       erw [presheaf.pushforward.comp_inv_app, comp_id, ← X.presheaf.map_comp,
           ← X.presheaf.map_comp, id_c_app],
       exact X.presheaf.map_id _ },
-  inv_hom_id' := ext _ _ rfl $ nat_trans.ext _ _ $ funext $ λ U, by { op_induction U,
+  inv_hom_id' := ext _ _ rfl $ nat_trans.ext _ _ $ funext $ λ U, by {
+    induction U using opposite.rec,
     dsimp only [nat_trans.comp_app, comp_c_app, of_restrict, to_restrict_top,
         whisker_right_app, comp_base, nat_trans.op_app, opens.map_iso_inv_app],
     erw [← X.presheaf.map_comp, ← X.presheaf.map_comp, ← X.presheaf.map_comp, id_c_app],
@@ -235,7 +236,7 @@ def Γ : (PresheafedSpace C)ᵒᵖ ⥤ C :=
 { obj := λ X, (unop X).presheaf.obj (op ⊤),
   map := λ X Y f, f.unop.c.app (op ⊤) ≫ (unop Y).presheaf.map (opens.le_map_top _ _).op,
   map_id' := λ X, begin
-    op_induction X,
+    induction X using opposite.rec,
     erw [unop_id_op, id_c_app, eq_to_hom_refl, id_comp],
     exact X.presheaf.map_id _
   end,

diff --git a/src/algebraic_geometry/presheafed_space/has_colimits.lean b/src/algebraic_geometry/presheafed_space/has_colimits.lean
@@ -96,7 +96,7 @@ def pushforward_diagram_to_colimit (F : J ⥤ PresheafedSpace C) :
   begin
     apply (op_equiv _ _).injective,
     ext U,
-    op_induction U,
+    induction U using opposite.rec,
     cases U,
     dsimp, simp, dsimp, simp,
   end,
@@ -153,7 +153,7 @@ def colimit_cocone (F : J ⥤ PresheafedSpace C) : cocone F :=
       { ext x,
         exact colimit.w_apply (F ⋙ PresheafedSpace.forget C) f x, },
       { ext U,
-        op_induction U,
+        induction U using opposite.rec,
         cases U,
         dsimp,
         simp only [PresheafedSpace.id_c_app, eq_to_hom_op, eq_to_hom_map, assoc,

diff --git a/src/algebraic_geometry/sheafed_space.lean b/src/algebraic_geometry/sheafed_space.lean
@@ -83,8 +83,8 @@ lemma id_c (X : SheafedSpace C) :
   (whisker_right (nat_trans.op (opens.map_id (X.carrier)).hom) _)) := rfl
 
 @[simp] lemma id_c_app (X : SheafedSpace C) (U) :
-  ((𝟙 X) : X ⟶ X).c.app U = eq_to_hom (by { op_induction U, cases U, refl }) :=
-by { op_induction U, cases U, simp only [id_c], dsimp, simp, }
+  ((𝟙 X) : X ⟶ X).c.app U = eq_to_hom (by { induction U using opposite.rec, cases U, refl }) :=
+by { induction U using opposite.rec, cases U, simp only [id_c], dsimp, simp, }
 
 @[simp] lemma comp_base {X Y Z : SheafedSpace C} (f : X ⟶ Y) (g : Y ⟶ Z) :
   (f ≫ g).base = f.base ≫ g.base := rfl

diff --git a/src/algebraic_geometry/stalks.lean b/src/algebraic_geometry/stalks.lean
@@ -104,7 +104,7 @@ end
 begin
   dsimp [stalk_map, stalk_functor, stalk_pushforward],
   ext U,
-  op_induction U,
+  induction U using opposite.rec,
   cases U,
   simp only [colimit.ι_map_assoc, colimit.ι_pre_assoc, colimit.ι_pre,
     whisker_left_app, whisker_right_app,

diff --git a/src/category_theory/limits/cones.lean b/src/category_theory/limits/cones.lean
@@ -692,7 +692,8 @@ def cocone_equivalence_op_cone_op : cocone F ≌ (cone F.op)ᵒᵖ :=
       w' := λ j, by { apply quiver.hom.op_inj, dsimp, simp, }, } },
   unit_iso := nat_iso.of_components (λ c, cocones.ext (iso.refl _) (by tidy)) (by tidy),
   counit_iso := nat_iso.of_components (λ c,
-    by { op_induction c, dsimp, apply iso.op, exact cones.ext (iso.refl _) (by tidy), })
+    by { induction c using opposite.rec,
+         dsimp, apply iso.op, exact cones.ext (iso.refl _) (by tidy), })
     begin
       intros,
       have hX : X = op (unop X) := rfl,

diff --git a/src/data/opposite.lean b/src/data/opposite.lean
@@ -91,17 +91,16 @@ equiv_to_opposite.symm.apply_eq_iff_eq_symm_apply
 
 instance [inhabited α] : inhabited αᵒᵖ := ⟨op (default _)⟩
 
+/-- A recursor for `opposite`. Use as `induction x using opposite.rec`. -/
 @[simp]
-def op_induction {F : Π (X : αᵒᵖ), Sort v} (h : Π X, F (op X)) : Π X, F X :=
+protected def rec {F : Π (X : αᵒᵖ), Sort v} (h : Π X, F (op X)) : Π X, F X :=
 λ X, h (unop X)
 
 end opposite
 
 namespace tactic
 
 open opposite
-open interactive interactive.types lean.parser tactic
-local postfix `?`:9001 := optional
 
 namespace op_induction
 
@@ -122,23 +121,12 @@ end op_induction
 
 open op_induction
 
-meta def op_induction (h : option name) : tactic unit :=
-do h ← match h with
-   | (some h) := pure h
-   | none     := find_opposite_hyp
-   end,
+/-- A version of `induction x using opposite.rec` which finds the appropriate hypothesis
+automatically, for use with `local attribute [tidy] op_induction'`. This is necessary because
+`induction x` is not able to deduce that `opposite.rec` should be used. -/
+meta def op_induction' : tactic unit :=
+do h ← find_opposite_hyp,
    h' ← tactic.get_local h,
-   revert_lst [h'],
-   applyc `opposite.op_induction,
-   tactic.intro h,
-   skip
-
--- For use with `local attribute [tidy] op_induction`
-meta def op_induction' := op_induction none
-
-namespace interactive
-meta def op_induction (h : parse ident?) : tactic unit :=
-tactic.op_induction h
-end interactive
+   tactic.induction' h' [] `opposite.rec
 
 end tactic
diff --git a/src/topology/sheaves/sheaf_condition/pairwise_intersections.lean b/src/topology/sheaves/sheaf_condition/pairwise_intersections.lean
@@ -150,26 +150,21 @@ def cone_equiv_inverse_obj (F : presheaf C X)
   { app :=
     begin
       intro x,
-      op_induction x,
+      induction x using opposite.rec,
       rcases x with (⟨i⟩|⟨i,j⟩),
       { exact c.π.app (walking_parallel_pair.zero) ≫ pi.π _ i, },
       { exact c.π.app (walking_parallel_pair.one) ≫ pi.π _ (i, j), }
     end,
     naturality' :=
     begin
-      -- Unfortunately `op_induction` isn't up to the task here, and we need to use `generalize`.
       intros x y f,
-      have ex : x = op (unop x) := rfl,
-      have ey : y = op (unop y) := rfl,
-      revert ex ey,
-      generalize : unop x = x',
-      generalize : unop y = y',
-      rintro rfl rfl,
+      induction x using opposite.rec,
+      induction y using opposite.rec,
       have ef : f = f.unop.op := rfl,
       revert ef,
       generalize : f.unop = f',
       rintro rfl,
-      rcases x' with ⟨i⟩|⟨⟩; rcases y' with ⟨⟩|⟨j,j⟩; rcases f' with ⟨⟩,
+      rcases x with ⟨i⟩|⟨⟩; rcases y with ⟨⟩|⟨j,j⟩; rcases f' with ⟨⟩,
       { dsimp, erw [F.map_id], simp, },
       { dsimp, simp only [category.id_comp, category.assoc],
         have h := c.π.naturality (walking_parallel_pair_hom.left),
@@ -202,7 +197,7 @@ def cone_equiv_inverse (F : presheaf C X)
     w' :=
     begin
       intro x,
-      op_induction x,
+      induction x using opposite.rec,
       rcases x with (⟨i⟩|⟨i,j⟩),
       { dsimp,
         rw [←(f.w walking_parallel_pair.zero), category.assoc], },
@@ -219,12 +214,13 @@ def cone_equiv_unit_iso_app (F : presheaf C X) ⦃ι : Type v⦄ (U : ι → ope
 { hom :=
   { hom := 𝟙 _,
     w' := λ j, begin
-      op_induction j, rcases j;
+      induction j using opposite.rec, rcases j;
       { dsimp, simp only [limits.fan.mk_π_app, category.id_comp, limits.limit.lift_π], }
     end, },
   inv :=
   { hom := 𝟙 _,
-    w' := λ j, begin op_induction j, rcases j;
+    w' := λ j, begin
+      induction j using opposite.rec, rcases j;
       { dsimp, simp only [limits.fan.mk_π_app, category.id_comp, limits.limit.lift_π], }
     end },
   hom_inv_id' := begin
@@ -298,7 +294,7 @@ is_limit.of_iso_limit ((is_limit.of_cone_equiv (cone_equiv F U).symm).symm P)
     w' :=
     begin
       intro x,
-      op_induction x,
+      induction x using opposite.rec,
       rcases x with ⟨⟩,
       { dsimp, simp, refl, },
       { dsimp,
@@ -312,7 +308,7 @@ is_limit.of_iso_limit ((is_limit.of_cone_equiv (cone_equiv F U).symm).symm P)
     w' :=
     begin
       intro x,
-      op_induction x,
+      induction x using opposite.rec,
       rcases x with ⟨⟩,
       { dsimp, simp, refl, },
       { dsimp,

diff --git a/src/topology/sheaves/stalks.lean b/src/topology/sheaves/stalks.lean
@@ -98,7 +98,7 @@ composition with the `germ` morphisms.
 -/
 lemma stalk_hom_ext (F : X.presheaf C) {x} {Y : C} {f₁ f₂ : F.stalk x ⟶ Y}
   (ih : ∀ (U : opens X) (hxU : x ∈ U), F.germ ⟨x, hxU⟩ ≫ f₁ = F.germ ⟨x, hxU⟩ ≫ f₂) : f₁ = f₂ :=
-colimit.hom_ext $ λ U, by { op_induction U, cases U with U hxU, exact ih U hxU }
+colimit.hom_ext $ λ U, by { induction U using opposite.rec, cases U with U hxU, exact ih U hxU }
 
 @[simp, reassoc, elementwise]
 lemma stalk_functor_map_germ {F G : X.presheaf C} (U : opens X) (x : U)
@@ -171,7 +171,7 @@ end
 begin
   dsimp [stalk_pushforward, stalk_functor],
   ext U,
-  op_induction U,
+  induction U using opposite.rec,
   cases U,
   cases U_val,
   simp only [colimit.ι_map_assoc, colimit.ι_pre_assoc,
@@ -365,7 +365,7 @@ begin
   -- We show that all components of `f` are isomorphisms.
   suffices : ∀ U : (opens X)ᵒᵖ, is_iso (f.app U),
   { exact @nat_iso.is_iso_of_is_iso_app _ _ _ _ F.1 G.1 f this, },
-  intro U, op_induction U,
+  intro U, induction U using opposite.rec,
   -- Since the forgetful functor of `C` reflects isomorphisms, it suffices to see that the
   -- underlying map between types is an isomorphism, i.e. bijective.
   suffices : is_iso ((forget C).map (f.app (op U))),