feat: last adaptations for v4.31.0 (#229)

Sorry, automated processes fell apart at the last moment.

Author: kim-em

Mathlib/Algebra/Exact/Sequence.lean

@@ -48,8 +48,23 @@ public lemma sum_neg_one_pow_finrank_eq_zero_of_exact {n : ℕ} (V : Fin (n + 2)
   simp_rw [← smul_eq_mul]
   refine Fin.sum_neg_one_pow_eq_zero _ (fun i ↦ finrank k (f i).range) ?_ (fun i ↦ ?_) ?_
   · aesop
-  · grind [(h_exact i).linearMap_ker_eq, (f i.succ).finrank_range_add_finrank_ker]
-  · grind [finrank_top]
+  · #adaptation_note /-- Prior to v4.31.0-rc1, this proof was
+      ```
+      grind [(h_exact i).linearMap_ker_eq, (f i.succ).finrank_range_add_finrank_ker]
+      ```
+      -/
+    have hrn := (f i.succ).finrank_range_add_finrank_ker
+    have hker : finrank k ↥(LinearMap.ker (f i.succ)) =
+        finrank k ↥(LinearMap.range (f i.castSucc)) :=
+      congrArg (fun S : Submodule k (V i.succ.castSucc) => finrank k ↥S)
+        (h_exact i).linearMap_ker_eq
+    omega
+  · #adaptation_note /-- Prior to v4.31.0-rc1, this proof was
+      ```
+      grind [finrank_top]
+      ```
+      -/
+    rw [surj, finrank_top, Fin.succ_last]
 
 /- An unrolled version of `Module.sum_neg_one_pow_finrank_eq_zero_of_exact`. This is an auxiliary
 lemma en route to `Module.sum_neg_one_pow_finrank_eq_zero_of_exact_six`. -/
@@ -78,7 +93,7 @@ private lemma sum_neg_one_pow_finrank_eq_zero_of_exact_six_aux {V₀ V₁ V₂ V
   | 0 => ‹_› | 1 => ‹_› | 2 => ‹_› | 3 => ‹_› | 4 => ‹_› | 5 => ‹_›
   letI fs (i : Fin 5) : Vs i.castSucc →ₗ[k] Vs i.succ := match i with
   | 0 => f₀ | 1 => f₁ | 2 => f₂ | 3 => f₃ | 4 => f₄
-  simpa [Fin.sum_univ_six] using Module.sum_neg_one_pow_finrank_eq_zero_of_exact Vs fs inj
+  simpa [Fin.sum_univ_six] using! Module.sum_neg_one_pow_finrank_eq_zero_of_exact Vs fs inj
     (fun i ↦ by fin_cases i; exacts [exact₁, exact₂, exact₃, exact₄]) surj
 
 /-- This is an unrolled, universe-polymorphic version of

Mathlib/AlgebraicGeometry/Birational/Dominant.lean

@@ -34,6 +34,7 @@ namespace Scheme
 
 namespace PartialMap
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Restricting a dominant partial map to a dense open yields a dominant partial map. -/
 lemma isDominant_restrict_hom (f : X.PartialMap Y) [IsDominant f.hom] (U : X.Opens)
     (hU : Dense (U : Set X)) (hU' : U ≤ f.domain) : IsDominant (f.restrict U hU hU').hom := by
@@ -54,6 +55,7 @@ lemma isDominant_hom_iff_isDominant_restrict_hom (f : X.PartialMap Y) (U : X.Ope
   ⟨fun _ ↦ f.isDominant_restrict_hom U hU hU',
     fun _ ↦ f.isDominant_hom_of_isDominant_restrict_hom U hU hU'⟩
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Dominance of the underlying morphism is invariant under equivalence of partial maps. -/
 lemma isDominant_hom_iff_of_equiv (f g : X.PartialMap Y) (h : f.equiv g) :
     IsDominant f.hom ↔ IsDominant g.hom := by

Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

@@ -101,7 +101,7 @@ theorem d_squared (n : ℕ) : objD X (n + 1) ≫ objD X n = 0 := by
     simp_rw [S, Finset.compl_filter, Finset.mem_filter_univ, not_le] at hij'
     refine ⟨(j'.pred <| ?_, Fin.castSucc i'), ?_, ?_⟩
     · rintro rfl
-      simp only [Fin.val_zero, not_lt_zero'] at hij'
+      simp only [Fin.val_zero, not_lt_zero] at hij'
     · simpa [S] using! Nat.le_sub_one_of_lt hij'
     · simp only [φ, Fin.castLT_castSucc, Fin.succ_pred]
   · -- identification of corresponding terms in both sums

Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean

@@ -160,6 +160,7 @@ lemma hasPointwiseRightKanExtensionAt_iff_of_equivalence
         isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
       (E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)
 
+set_option backward.defeqAttrib.useBackward true in
 lemma HasPointwiseLeftKanExtensionAt.of_natIso {L L' : C ⥤ D} {F F' : C ⥤ H} (Y : D)
     [L.HasPointwiseLeftKanExtensionAt F Y] (e₁ : L ≅ L') (e₂ : F ≅ F') :
     L'.HasPointwiseLeftKanExtensionAt F' Y := by
@@ -176,6 +177,7 @@ lemma hasPointwiseLeftKanExtensionAt_iff_of_natIso {L L' : C ⥤ D} {F F' : C 
     L.HasPointwiseLeftKanExtensionAt F Y ↔ L'.HasPointwiseLeftKanExtensionAt F' Y :=
   ⟨fun _ ↦ .of_natIso Y e₁ e₂, fun _ ↦ .of_natIso Y e₁.symm e₂.symm⟩
 
+set_option backward.defeqAttrib.useBackward true in
 lemma HasPointwiseRightKanExtensionAt.of_natIso {L L' : C ⥤ D} {F F' : C ⥤ H} (Y : D)
     [L.HasPointwiseRightKanExtensionAt F Y] (e₁ : L ≅ L') (e₂ : F ≅ F') :
     L'.HasPointwiseRightKanExtensionAt F' Y := by

Mathlib/CategoryTheory/Monoidal/Free/Coherence.lean

@@ -204,6 +204,7 @@ def normalizeIsoApp' :
 @[simp] theorem normalizeIsoApp'_unit (n : NormalMonoidalObject C) :
     normalizeIsoApp' C (𝟙_ (F C)) n = ρ_ _ := rfl
 
+set_option backward.defeqAttrib.useBackward true in
 theorem normalizeIsoApp_eq :
     ∀ (X : F C) (n : N C), normalizeIsoApp C X n = normalizeIsoApp' C X n.as
   | of _, _ => rfl
@@ -279,6 +280,7 @@ theorem normalize_naturality (n : NormalMonoidalObject C) {X Y : F C} (f : X ⟶
 
 end
 
+set_option backward.defeqAttrib.useBackward true in
 /-- The isomorphism between `n ⊗ X` and `normalize X n` is natural (in both `X` and `n`, but
 naturality in `n` is trivial and was "proved" in `normalizeIsoAux`). This is the real heart
 of our proof of the coherence theorem. -/

Mathlib/CategoryTheory/MorphismProperty/LocalEpi.lean

@@ -47,7 +47,7 @@ def localEpi (P : ObjectProperty C) : MorphismProperty C := fun _ _ f ↦
   ∀ ⦃Z⦄, P Z → Function.Injective fun (g : _ ⟶ Z) ↦ f ≫ g
 
 instance : P.localEpi.IsMultiplicative where
-  id_mem X Z _ := by simpa using Function.injective_id
+  id_mem X Z _ := by simpa using! Function.injective_id
   comp_mem f g hf hg T hT _ _ huv := hg hT (hf hT <| by simpa using huv)
 
 lemma localEpi.of_epi {X Y : C} (f : X ⟶ Y) [Epi f] : P.localEpi f := by
@@ -101,6 +101,7 @@ variable {D : Type*} [Category* D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G)
   [G.Faithful] [G.Full]
 include adj
 
+set_option backward.isDefEq.respectTransparency false in
 lemma localEpi_mem_range_iff_epi {X Y : C} (f : X ⟶ Y) :
     localEpi (· ∈ Set.range G.obj) f ↔ Epi (F.map f) := by
   rw [← dsimp% (localEpi (· ∈ Set.range G.obj)).postcomp_iff _ _ (isLocal_adj_unit_app adj Y),

Mathlib/CategoryTheory/MorphismProperty/OverAdjunction.lean

@@ -58,6 +58,7 @@ def Over.mapCongr [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf :
   NatIso.ofComponents (fun Y ↦ Over.isoMk (Iso.refl _))
 
 set_option backward.defeqAttrib.useBackward true in
+set_option linter.overlappingInstances false in
 /-- `Over.map` preserves identities. -/
 @[simps!]
 def Over.mapId [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := 𝟙 X)
@@ -237,6 +238,7 @@ def Under.mapCongr [Q.RespectsIso] {X Y : T} {f g : X ⟶ Y} (hfg : f = g) (hf :
   NatIso.ofComponents (fun Y ↦ Under.isoMk (Iso.refl _))
 
 set_option backward.defeqAttrib.useBackward true in
+set_option linter.overlappingInstances false in
 /-- `Under.map` preserves identities. -/
 @[simps!]
 def Under.mapId [P.IsMultiplicative] [Q.RespectsIso] (X : T) (f : X ⟶ X := 𝟙 X)

Mathlib/CategoryTheory/Presentable/CardinalDirectedPoset.lean

@@ -76,7 +76,7 @@ instance (J : Type u) [SmallCategory J] [IsCardinalFiltered J κ] :
     simp only [(isCardinalFiltered κ).prop_iff_of_iso
       (p.isColimit.coconePointUniqueUpToIso
         (Limits.isColimitCocone (colimit.isColimit (p.diag ⋙ forget PartOrdEmb)))),
-      isCardinalFiltered_iff, Limits.cocone_pt_coe]
+      isCardinalFiltered_iff]
     exact Limits.CoconePt.isCardinalFiltered_pt _ p.prop_diag_obj
 
 end PartOrdEmb
@@ -138,6 +138,7 @@ variable {J : CardinalFilteredPoset κ} (P : Set J.obj → Prop)
   [IsDirectedOrder (Subtype P)] [Nonempty (Subtype P)]
   [∀ (S : Subtype P), IsCardinalFiltered S.val κ]
 
+set_option backward.defeqAttrib.useBackward true in
 /-- Given a predicate `P : Set J.obj → Prop` on the underlying type
 of `J : CardinalFilteredPoset κ` such that all the subsets satisfying `P`
 are `κ`-filtered, this is the functor `Subtype P ⥤ CardinalFilteredPoset κ`

Mathlib/Data/Finsupp/Single.lean

@@ -162,7 +162,7 @@ lemma apply_surjective (a : α) : Surjective fun f : α →₀ M ↦ f a :=
   RightInverse.surjective fun _ ↦ single_eq_same
 
 theorem support_single_ne_bot (i : α) (h : b ≠ 0) : (single i b).support ≠ ⊥ := by
-  simpa only [support_single_ne_zero _ h] using! singleton_ne_empty _
+  simpa only [support_single _ h] using! singleton_ne_empty _
 
 theorem support_single_disjoint {b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : α} :
     Disjoint (single i b).support (single j b').support ↔ i ≠ j := by

Mathlib/FieldTheory/Galois/IsGaloisGroup.lean

@@ -658,7 +658,7 @@ theorem map_quotientMk' [Finite G] [IsGaloisGroup G K L] (h : E ≤ F) :
     isInvariant := ⟨fun x h ↦ by
       obtain ⟨a, ha⟩ := hE.isInvariant.isInvariant (algebraMap F L x) (by
         rintro ⟨g, hg⟩
-        simpa only [← algebraMap.smul'] using congr_arg (algebraMap F L) <| h ⟨g, ⟨g, hg, rfl⟩⟩)
+        simpa only [← algebraMap.smul'] using! congr_arg (algebraMap F L) <| h ⟨g, ⟨g, hg, rfl⟩⟩)
       exact ⟨a, FaithfulSMul.algebraMap_injective F L
         (by rw [← IsScalarTower.algebraMap_apply, ha])⟩⟩ }