chore(AlgebraicTopology/SimplicialSet/AnodyneExtensions): removing some set_option

Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/IsUniquelyCodimOneFace.lean

@@ -96,7 +96,6 @@ lemma le : x ≤ y := by
     ← this]
   exact ⟨(SimplexCategory.δ _).op, rfl⟩
 
-set_option backward.defeqAttrib.useBackward true in
 include hxy in
 lemma unique (f : ⦋d⦌ ⟶ ⦋d + 1⦌) [Mono f]
     (hf : X.map f.op (y.cast (by rw [hxy.dim_eq, hd])).simplex = (x.cast hd).simplex) :
@@ -116,7 +115,6 @@ lemma op : (S.opEquiv.symm x).IsUniquelyCodimOneFace (S.opEquiv.symm y) := by
   obtain ⟨i, rfl⟩ := i.rev_surjective
   simpa [← hxy.δ_eq_iff rfl] using hi
 
-set_option backward.defeqAttrib.useBackward true in
 include hxy in
 lemma of_iso {Y : SSet.{u}} (e : X ≅ Y) :
     (S.mk (e.hom.app _ x.simplex)).IsUniquelyCodimOneFace (S.mk (e.hom.app _ y.simplex)) := by

Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Op.lean

@@ -26,7 +26,7 @@ variable {X : SSet.{u}} {A : X.Subcomplex} (P : A.Pairing)
 
 /-- If `P` is a pairing for a subcomplex `A` of a simplicial set `X`,
 this is the corresponding pairing of `A.op`. -/
-@[simps I II]
+@[implicit_reducible, simps I II]
 def op : A.op.Pairing where
   I := Subcomplex.N.opEquiv ⁻¹' P.I
   II := Subcomplex.N.opEquiv ⁻¹' P.II
@@ -35,18 +35,15 @@ def op : A.op.Pairing where
   p := (N.opEquiv.subtypeEquiv (by simp)).trans
     (P.p.trans (N.opEquiv.symm.subtypeEquiv (by simp)))
 
-set_option backward.defeqAttrib.useBackward true in
 @[simp]
 lemma op_p (x : P.II) :
     dsimp% P.op.p ⟨Subcomplex.N.opEquiv.symm x.1, x.2⟩ =
       ⟨Subcomplex.N.opEquiv.symm (P.p x), by simp⟩ := rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma op_ancestralRel_iff (x y : P.II) :
     P.op.AncestralRel ⟨Subcomplex.N.opEquiv.symm x.1, x.2⟩
       ⟨Subcomplex.N.opEquiv.symm y.1, y.2⟩ ↔ P.AncestralRel x y :=
-  and_congr (not_congr (by aesop)) (by simp)
+  and_congr (not_congr (by simp [Subtype.ext_iff])) (by simp)
 
 instance [P.IsProper] : P.op.IsProper where
   isUniquelyCodimOneFace x := (P.isUniquelyCodimOneFace ⟨_, x.2⟩).op

Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Pairing.lean

@@ -146,7 +146,7 @@ variable {Y : SSet.{u}} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom
 
 /-- Given an isomorphism `Y ≅ X` of simplicial sets, a pairing `P` of a subcomplex
 `A` of `X`, this is a pairing for a subcomplex `B` of `Y` if `A.preimage e.hom = B`. -/
-@[simps I II]
+@[implicit_reducible, simps I II]
 def ofIso : B.Pairing where
   I := Subcomplex.N.orderIsoOfIso e hA ⁻¹' P.I
   II := Subcomplex.N.orderIsoOfIso e hA ⁻¹' P.II
@@ -165,7 +165,6 @@ unif_hint {X : SSet.{u}} {A : X.Subcomplex} (P : A.Pairing)
     {Y : SSet.{u}} {B : Y.Subcomplex} (e : Y ≅ X) (hA : A.preimage e.hom = B) where
   ⊢ (P.ofIso e hA).II ≟ (N.orderIsoOfIso e hA) ⁻¹' P.II
 
-set_option backward.defeqAttrib.useBackward true in
 @[simp]
 lemma ofIso_p (x : P.II) :
     dsimp% (P.ofIso e hA).p ⟨(Subcomplex.N.orderIsoOfIso e hA).symm x, by simp⟩ =
@@ -175,16 +174,13 @@ lemma ofIso_p (x : P.II) :
   change e'.symm (P.p ⟨e' (e'.symm x), _⟩) = e'.symm (P.p x)
   simp
 
-set_option backward.isDefEq.respectTransparency.types false in
-set_option backward.defeqAttrib.useBackward true in
 lemma ofIso_ancestralRel_iff (x y : P.II) :
     (P.ofIso e hA).AncestralRel
       ⟨(Subcomplex.N.orderIsoOfIso e hA).symm x, by simp⟩
       ⟨(Subcomplex.N.orderIsoOfIso e hA).symm y, by simp⟩ ↔
     P.AncestralRel x y :=
   and_congr (not_congr (by aesop)) (by simp)
 
-set_option backward.defeqAttrib.useBackward true in
 instance [P.IsProper] : (P.ofIso e hA).IsProper where
   isUniquelyCodimOneFace := by
     rintro ⟨x, hx⟩
@@ -202,8 +198,6 @@ instance [P.IsRegular] : (P.ofIso e hA).IsRegular where
     refine hP.false ⟨fun n ↦ ⟨_, (f n).2⟩, fun n ↦ ?_⟩
     simpa [← P.ofIso_ancestralRel_iff e hA] using hf n
 
-set_option backward.isDefEq.respectTransparency false in
-@[simp]
 lemma ofIso_index (x : P.II) {d : ℕ} (hd : x.1.dim = d) [P.IsProper] :
     ((P.ofIso e hA).isUniquelyCodimOneFace ⟨(N.orderIsoOfIso e hA).symm x, by simp⟩).index hd =
       (isUniquelyCodimOneFace P x).index hd := by

Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/PairingCore.lean

@@ -62,6 +62,7 @@ variable {A}
 
 /-- The `PairingCore` structure induced by a pairing. The opposite construction
 is `PairingCore.pairing`. -/
+@[implicit_reducible]
 noncomputable def Pairing.pairingCore (P : A.Pairing) [P.IsProper] :
     A.PairingCore where
   ι := P.II
@@ -102,12 +103,12 @@ namespace PairingCore
 variable (h : A.PairingCore)
 
 /-- The type (I) simplices of `h : A.PairingCore`, as a family indexed by `h.ι`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def type₁ (s : h.ι) : A.N :=
   Subcomplex.N.mk (h.simplex s) (h.nonDegenerate₁ s) (h.notMem₁ s)
 
 /-- The type (II) simplices of `h : A.PairingCore`, as a family indexed by `h.ι`. -/
-@[simps!]
+@[implicit_reducible, simps!]
 def type₂ (s : h.ι) : A.N :=
   Subcomplex.N.mk (X.δ (h.index s) (h.simplex s)) (h.nonDegenerate₂ s)
     (h.notMem₂ s)
@@ -128,21 +129,21 @@ lemma surjective (x : A.N) :
   · exact ⟨s, Or.inr (by rwa [N.ext_iff, SSet.N.ext_iff])⟩
 
 /-- The type (I) simplices of `h : A.PairingCore`, as a subset of `A.N`. -/
-def I : Set A.N := Set.range h.type₁
+abbrev I : Set A.N := Set.range h.type₁
 
 /-- The type (II) simplices of `h : A.PairingCore`, as a subset of `A.N`. -/
-def II : Set A.N := Set.range h.type₂
+abbrev II : Set A.N := Set.range h.type₂
 
 /-- The bijection `h.ι ≃ h.I` when `h : A.PairingCore`. -/
-@[simps! apply_coe]
+@[implicit_reducible, simps! apply_coe]
 noncomputable def equivI : h.ι ≃ h.I := Equiv.ofInjective _ h.injective_type₁
 
 /-- The bijection `h.ι ≃ h.II` when `h : A.PairingCore`. -/
-@[simps! apply_coe]
+@[implicit_reducible, simps! apply_coe]
 noncomputable def equivII : h.ι ≃ h.II := Equiv.ofInjective _ h.injective_type₂
 
 /-- The pairing induced by `h : A.PairingCore`. -/
-@[simps I II]
+@[implicit_reducible, simps I II]
 noncomputable def pairing : A.Pairing where
   I := h.I
   II := h.II
@@ -169,10 +170,9 @@ lemma pairing_p_symm_equivI (x : h.ι) :
     DFunLike.coe (F := h.I ≃ h.II) h.pairing.p.symm (h.equivI x) = h.equivII x := by
   simp [pairing]
 
-set_option backward.defeqAttrib.useBackward true in
 lemma type₁_pairing (x : h.ι) :
     h.type₁ x = h.pairing.p (h.equivII x) := by
-  simp +instances
+  simp
 
 /-- The condition that `h : A.PairingCore` is proper, i.e. for each `s : h.ι`,
 the type (II) simplex `h.type₂ s` is uniquely a `1`-codimensional
@@ -192,8 +192,6 @@ instance [X.Nonsingular] : h.IsProper where
         (fun _ _ hi hj ↦ Nonsingular.δ_injective _
           (h.nonDegenerate₁ s) _ _ (hi.trans hj.symm)))
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 instance [h.IsProper] : h.pairing.IsProper where
   isUniquelyCodimOneFace x := by
     obtain ⟨s, rfl⟩ := h.equivII.surjective x
@@ -202,16 +200,14 @@ instance [h.IsProper] : h.pairing.IsProper where
 lemma isProper_pairing_iff :
     h.pairing.IsProper ↔ h.IsProper := by
   refine ⟨fun _ ↦ ⟨fun s ↦ ?_⟩, fun _ ↦ inferInstance⟩
-  simpa [type₁_pairing] using h.pairing.isUniquelyCodimOneFace (h.equivII s)
+  simpa using h.pairing.isUniquelyCodimOneFace (h.equivII s)
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma isUniquelyCodimOneFace_index [h.IsProper] (s : h.ι) :
     (h.isUniquelyCodimOneFace s).index rfl = h.index s := by
   symm
   simp [← (h.isUniquelyCodimOneFace s).δ_eq_iff]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma isUniquelyCodimOneFace_index_coe
     [h.IsProper] (s : h.ι) {d : ℕ} (hd : h.dim s = d) :
     ((h.isUniquelyCodimOneFace s).index hd).val = (h.index s).val := by
@@ -239,8 +235,6 @@ instance [h.IsInner] [h.IsProper] : h.pairing.IsInner where
 def AncestralRel (s t : h.ι) : Prop :=
   s ≠ t ∧ h.type₂ s < h.type₁ t
 
-set_option backward.defeqAttrib.useBackward true in
-set_option backward.isDefEq.respectTransparency false in
 lemma ancestralRel_iff (s t : h.ι) :
     h.AncestralRel s t ↔ h.pairing.AncestralRel (h.equivII s) (h.equivII t) := by
   simp [AncestralRel, Pairing.AncestralRel]
@@ -250,7 +244,6 @@ is regular. -/
 class IsRegular (h : A.PairingCore) extends h.IsProper where
   wf (h) : WellFounded h.AncestralRel
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance [h.IsRegular] : h.pairing.IsRegular where
   wf := by
     have := IsRegular.wf h

Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/Rank.lean

@@ -127,7 +127,6 @@ structure WeakRankFunction where
   rank : h.ι → α
   lt {x y : h.ι} : h.AncestralRel x y → h.dim x = h.dim y → rank x < rank y
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Rank functions for `h : A.PairingCore` correspond to
 rank functions for `h.pairing : A.Pairing`. -/
 noncomputable def rankFunctionEquiv :
@@ -147,7 +146,6 @@ noncomputable def rankFunctionEquiv :
   left_inv _ := by simp
   right_inv _ := by simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Weak rank functions for `h : A.PairingCore` correspond to
 weak rank functions for `h.pairing : A.Pairing`. -/
 noncomputable def weakRankFunctionEquiv :

Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/RelativeCellComplex.lean

@@ -25,8 +25,6 @@ cell complex with basic cells given by horn inclusions.
 
 -/
 
-set_option backward.defeqAttrib.useBackward true
-
 @[expose] public section
 
 universe v u
@@ -81,12 +79,10 @@ abbrev map : Δ[c.dim + 1] ⟶ X :=
   yonedaEquiv.symm
     ((P.p c.s).val.cast (P.isUniquelyCodimOneFace c.s).dim_eq).simplex
 
-set_option backward.defeqAttrib.useBackward true in
 @[simp]
 lemma range_map : Subcomplex.range c.map = (P.p c.s).val.subcomplex := by
   rw [range_eq_ofSimplex, Equiv.apply_symm_apply, S.ofSimplex_eq_subcomplex_mk,
     ← S.cast_eq_self _ (P.dim_p c.s)]
-  dsimp [S.subcomplex]
 
 lemma map_app_objEquiv_symm_δ_index :
     c.map.app (op ⦋c.dim⦌) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index)) =
@@ -126,6 +122,7 @@ noncomputable abbrev basicCell (i : ι) (c : f.Cell i) : (c.horn : SSet) ⟶ Δ[
 
 /-- The filtration of a simplicial set given by a rank function
 for a proper pairing of a subcomplex. -/
+@[implicit_reducible]
 def filtration (i : ι) : X.Subcomplex :=
   A ⊔ ⨆ (j : ι) (_ : j < i) (c : f.Cell j), (P.p c.s).val.subcomplex
 
@@ -389,13 +386,12 @@ lemma Cell.ι_t_app {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ) :
     c.ιSigmaHorn.app x ≫ (f.t j).app x = c.mapHorn.app x :=
   NatTrans.congr_app c.ι_t x
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Given a rank `j` cell `c` for a rank function `f` for a proper
 pairing of a subcomplex of a simplicial set, this is
 the nondegenerate simplex in `f.sigmaStdSimplex j`
 not in the image of `f.m j : f.sigmaHorn j ⟶ f.sigmaStdSimplex j`
 which corresponds to `c.ιSigmaStdSimplex`. -/
-@[simps]
+@[implicit_reducible, simps]
 noncomputable def Cell.type₁ {j : ι} (c : f.Cell j) : (Subcomplex.range (f.m j)).N where
   simplex := c.ιSigmaStdSimplex.app _ (stdSimplex.objEquiv.symm (𝟙 _))
   nonDegenerate := by
@@ -409,13 +405,12 @@ noncomputable def Cell.type₁ {j : ι} (c : f.Cell j) : (Subcomplex.range (f.m
     obtain ⟨rfl, rfl⟩ := hy
     exact objEquiv_symm_notMem_horn_of_isIso _ _ hy'
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Given a rank `j` cell `c` for a rank function `f` for a proper
 pairing of a subcomplex of a simplicial set, this is
 the nondegenerate simplex in `f.sigmaStdSimplex j`
 not in the image of `f.m j : f.sigmaHorn j ⟶ f.sigmaStdSimplex j`
 which corresponds to the `c.index`th-face of `c.type₁`. -/
-@[simps]
+@[implicit_reducible, simps]
 noncomputable def Cell.type₂ {j : ι} (c : f.Cell j) : (Subcomplex.range (f.m j)).N where
   simplex := c.ιSigmaStdSimplex.app _
     (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))
@@ -430,7 +425,6 @@ noncomputable def Cell.type₂ {j : ι} (c : f.Cell j) : (Subcomplex.range (f.m
     obtain ⟨rfl, rfl⟩ := hy
     simpa using (objEquiv_symm_δ_mem_horn_iff _ _).mp hy'
 
-set_option backward.isDefEq.respectTransparency false in
 lemma exists_or_of_range_m_N {j : ι} (s : (Subcomplex.range (f.m j)).N) :
     ∃ (c : f.Cell j), s = c.type₁ ∨ s = c.type₂ := by
   obtain ⟨d, s, hs, hs', rfl⟩ := s.mk_surjective
@@ -475,7 +469,6 @@ lemma w (j : ι) :
   ext c : 1
   simp [← cancel_mono (Subcomplex.ι _)]
 
-set_option backward.isDefEq.respectTransparency false in
 lemma isPullback (j : ι) :
     IsPullback (f.t j) (f.m j) (homOfLE (f.filtration_monotone (Order.le_succ j))) (f.b j) where
   w := f.w j
@@ -501,7 +494,6 @@ lemma isPullback (j : ι) :
     · rw [← NatTrans.comp_app_apply]
       simp)⟩
 
-set_option backward.isDefEq.respectTransparency false in
 lemma range_homOfLE_app_union_range_b_app (j : ι) (d : SimplexCategoryᵒᵖ) :
     Set.range ((homOfLE (f.filtration_monotone (Order.le_succ j))).app d) ⊔
       Set.range ((f.b j).app d) = Set.univ := by
@@ -525,7 +517,6 @@ corresponding to an element in `(Subcomplex.range (f.m j)).N`. -/
 noncomputable def mapN {j : ι} (x : (Subcomplex.range (f.m j)).N) : X.S :=
   S.mk ((f.b j).app _ x.simplex).val
 
-set_option backward.isDefEq.respectTransparency.types false in
 @[simp]
 lemma mapN_type₁ {j : ι} (c : f.Cell j) : f.mapN c.type₁ = S.mk (P.p c.s).val.simplex := by
   dsimp only [Cell.type₁, mapN]
@@ -534,7 +525,6 @@ lemma mapN_type₁ {j : ι} (c : f.Cell j) : f.mapN c.type₁ = S.mk (P.p c.s).v
   rw [S.ext_iff, c.ι_b_app_apply]
   apply yonedaEquiv_symm_app_id
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma mapN_type₂ {j : ι} (c : f.Cell j) : f.mapN c.type₂ = S.mk c.s.val.simplex := by
   dsimp [mapN]
@@ -565,7 +555,6 @@ private lemma isPushout_aux₃ {j : ι} :
     Function.Injective fun (x : (Subcomplex.range (f.m j)).N) ↦ S.mk ((f.b j).app _ x.simplex) :=
   fun _ _ h ↦ f.isPushout_aux₂ (congr_arg (S.map (Subcomplex.ι _)) h)
 
-set_option backward.isDefEq.respectTransparency false in
 lemma isPushout (j : ι) :
     IsPushout (f.t j) (f.m j) (homOfLE (f.filtration_monotone (Order.le_succ j))) (f.b j) where
   w := f.w j