fix?

Author: chrisflav

Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean

@@ -363,27 +363,6 @@ lemma _root_.CategoryTheory.PreOneHypercover.sieve₀_map
     PreOneHypercover.map_toPreZeroHypercover, PreZeroHypercover.presieve₀_map,
     Sieve.generate_map_eq_functorPushforward]
 
-instance {C : Type*} [Category* C] (X : C) (J : GrothendieckTopology C) :
-    Functor.PreservesOneHypercovers.{w} (Over.forget X) (J.over X) J := by
-  intro U E
-  refine ⟨?_, ?_⟩
-  · simpa [CategoryTheory.PreZeroHypercover.sieve₀_map] using E.mem₀
-  · intro i₁ i₂ W p₁ p₂ h
-    let W' : Over X := Over.mk (p₁ ≫ (E.X i₁).hom)
-    let p₁' : W' ⟶ E.X i₁ := Over.homMk p₁ rfl
-    let p₂' : W' ⟶ E.X i₂ := Over.homMk p₂ <| by
-      dsimp at h
-      simp only [Over.forget_obj, Over.mk_left, Over.mk_hom, W']
-      rw [← Over.w (E.f i₂), ← reassoc_of% h]
-      simp
-    have := E.mem₁ _ _ p₁' p₂' (by ext; exact h)
-    rw [J.mem_over_iff] at this
-    refine J.superset_covering ?_ this
-    intro U g hg
-    rw [Sieve.overEquiv_iff] at hg
-    obtain ⟨j, u, h₁, h₂⟩ := hg
-    exact ⟨j, u.left, congr($(h₁).left), congr($(h₂).left)⟩
-
 lemma coverPreserving_of_coverPreserving_comp {C D E : Type*} [Category* C] [Category* D]
     [Category* E] (F : C ⥤ D) (G : D ⥤ E) (J : GrothendieckTopology C) (K : GrothendieckTopology D)
     (T : GrothendieckTopology E) (h : CoverPreserving J T (F ⋙ G)) [G.IsCocontinuous K T]
@@ -408,6 +387,7 @@ instance {C : Type*} [Category* C] {A : Type*} [Category* A]
   · simp [IsIso.hom_inv_id]
   · simp [IsIso.inv_hom_id]
 
+set_option backward.defeqAttrib.useBackward true in
 omit
   [HasSheafify J AddCommGrpCat]
   [J.WEqualsLocallyBijective AddCommGrpCat]

Mathlib/AlgebraicGeometry/Modules/Tilde.lean

@@ -8,10 +8,9 @@ module
 
 public import Mathlib.Algebra.Category.ModuleCat.Localization
 public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
+public import Mathlib.Algebra.Category.ModuleCat.FilteredColimits
 public import Mathlib.AlgebraicGeometry.AffineScheme
 public import Mathlib.AlgebraicGeometry.Modules.Sheaf
-public import Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
-public import Mathlib.Algebra.Category.ModuleCat.FilteredColimits
 public import Mathlib.CategoryTheory.Limits.ConcreteCategory.WithAlgebraicStructures
 public import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over
 public import Mathlib.CategoryTheory.Limits.Preorder
@@ -561,6 +560,7 @@ open CategoryTheory TopologicalSpace
 variable {X : Scheme.{u}} (M : X.Modules) [M.IsQuasicoherent]
 
 open Limits
+set_option backward.defeqAttrib.useBackward true in
 lemma _root_.CategoryTheory.Limits.preservesLimit_walkingParallelPair_of_eq
     {C D : Type*} [Category* C] [Category* D] {K : WalkingParallelPair ⥤ C}
     (heq : K.map .left = K.map .right) (F : C ⥤ D) :
@@ -570,7 +570,7 @@ lemma _root_.CategoryTheory.Limits.preservesLimit_walkingParallelPair_of_eq
     exact preservesLimit_of_iso_diagram _ (diagramIsoParallelPair _).symm
   rintro X Y f g rfl
   refine preservesLimit_of_preserves_limit_cone (isLimitIdFork rfl) ?_
-  exact (isLimitMapConeForkEquiv F _).symm (by simpa using isLimitIdFork rfl)
+  exact (isLimitMapConeForkEquiv F _).symm (by simpa using! isLimitIdFork rfl)
 
 instance {C D : Type*} [Category* C] [Category* D] (F : C ⥤ D) {X Y : C} (f : X ⟶ Y) :
     PreservesLimit (parallelPair f f) F :=
@@ -585,7 +585,7 @@ instance (priority := low) {C D : Type*} [Category* C] [Category* D] [Quiver.IsT
 def _root_.CategoryTheory.Limits.isLimitEquivFanOfIsThin {C : Type*} [Category* C]
     [Quiver.IsThin C] {J : Type*} [Category* J] {K : J ⥤ C} (c : Cone K) :
     IsLimit c ≃ IsLimit (Fan.mk c.pt c.π.app) where
-  toFun hc := Limits.mkFanLimit _ (fun s ↦ hc.lift { pt := s.pt, π.app j := s.proj j })
+  toFun hc := Fan.IsLimit.mk _ (fun s ↦ hc.lift { pt := s.pt, π.app j := s.proj j })
     (by subsingleton) (by subsingleton)
   invFun h := { lift s := Fan.IsLimit.lift h s.π.app }
 

Mathlib/AlgebraicGeometry/OpenImmersion.lean

@@ -225,6 +225,7 @@ theorem appIso_hom' (U) :
     (f.appIso U).hom = f.appLE (f ''ᵁ U) U (preimage_image_eq f U).ge :=
   f.appIso_hom U
 
+set_option backward.defeqAttrib.useBackward true in
 @[reassoc (attr := simp)]
 lemma appIso_hom_naturality {U V : X.Opens} (i : op U ⟶ op V) :
     Y.presheaf.map (f.opensFunctor.op.map i) ≫ (f.appIso V).hom =

Mathlib/CategoryTheory/Sites/CoverPreserving.lean

@@ -210,21 +210,4 @@ lemma Functor.PreservesOneHypercovers.of_coverPreserving [HasPullbacks C]
       (K.pullback_stable (IsPullback.lift (.map _ (.of_hasPullback _ _)) p₁ p₂ h) this)
     simp [PreOneHypercover.pullback_sieve₁]
 
-/-- If `C` has pullbacks and `F : C ⥤ D` preserves pullbacks, any cover preserving
-functor preserves all `1`-hypercovers. -/
-lemma Functor.PreservesOneHypercovers.of_coverPreserving [HasPullbacks C]
-    [PreservesLimitsOfShape WalkingCospan F] (H : CoverPreserving J K F) :
-    Functor.PreservesOneHypercovers.{w} F J K := by
-  refine fun {U} E ↦ ⟨?_, fun i₁ i₂ W p₁ p₂ h ↦ ?_⟩
-  · simp [PreZeroHypercover.sieve₀_map, H.cover_preserve E.mem₀]
-  · let P : C := pullback (E.f i₁) (E.f i₂)
-    have : HasPullback ((E.toPreOneHypercover.map F).f i₁) ((E.toPreOneHypercover.map F).f i₂) :=
-      hasPullback_of_preservesPullback F (E.f i₁) (E.f i₂)
-    have := H.cover_preserve (E.mem₁ i₁ i₂ (pullback.fst (E.f i₁) (E.f i₂)) _ pullback.condition)
-    rw [PreOneHypercover.functorPushforward_sieve₁_of_preservesLimitsOfShape] at this
-    · refine K.superset_covering ?_
-        (K.pullback_stable (IsPullback.lift (.map _ (.of_hasPullback _ _)) p₁ p₂ h) this)
-      simp [PreOneHypercover.pullback_sieve₁]
-    · exact pullback.condition
-
 end CategoryTheory