Merge master into nightly-testing

Author: mathlib-nightly-testing[bot]

Mathlib.lean

@@ -3452,6 +3452,7 @@ public import Mathlib.Combinatorics.Enumerative.Stirling
 public import Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
 public import Mathlib.Combinatorics.Graph.Basic
 public import Mathlib.Combinatorics.Graph.Delete
+public import Mathlib.Combinatorics.Graph.Lattice
 public import Mathlib.Combinatorics.Graph.Subgraph
 public import Mathlib.Combinatorics.HalesJewett
 public import Mathlib.Combinatorics.Hall.Basic

Mathlib/Algebra/Category/Grp/AB.lean

@@ -15,7 +15,7 @@ public import Mathlib.CategoryTheory.Limits.FunctorCategory.EpiMono
 # AB axioms for the category of abelian groups
 
 This file proves that the category of abelian groups satisfies Grothendieck's axioms AB5, AB4, and
-AB4*.
+AB4\*.
 -/
 
 @[expose] public section

Mathlib/Algebra/Category/ModuleCat/AB.lean

@@ -14,7 +14,7 @@ public import Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
 # AB axioms in module categories
 
 This file proves that the category of modules over a ring satisfies Grothendieck's axioms AB5, AB4,
-and AB4*. Further, it proves that `R` is a separator in the category of modules over `R`, and
+and AB4\*. Further, it proves that `R` is a separator in the category of modules over `R`, and
 concludes that this category is Grothendieck abelian.
 -/
 

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -82,7 +82,6 @@ def freeHomEquiv {X : Type u} {M : ModuleCat.{u} R} :
 
 variable (R)
 
-set_option backward.isDefEq.respectTransparency false in
 /-- The free-forgetful adjunction for R-modules.
 -/
 def adj : free R ⊣ forget (ModuleCat.{u} R) :=

Mathlib/Algebra/Category/ModuleCat/EpiMono.lean

@@ -61,13 +61,11 @@ instance mono_as_hom'_subtype (U : Submodule R X) : Mono (ModuleCat.ofHom U.subt
 instance epi_as_hom''_mkQ (U : Submodule R X) : Epi (ModuleCat.ofHom U.mkQ) :=
   (epi_iff_range_eq_top _).mpr <| Submodule.range_mkQ _
 
-set_option backward.isDefEq.respectTransparency false in
 instance forget_preservesEpimorphisms : (forget (ModuleCat.{v} R)).PreservesEpimorphisms where
     preserves f hf := by
       rw [CategoryTheory.ofHom_epi_iff_surjective, ← epi_iff_surjective]
       exact hf
 
-set_option backward.isDefEq.respectTransparency false in
 instance forget_preservesMonomorphisms : (forget (ModuleCat.{v} R)).PreservesMonomorphisms where
     preserves f hf := by
       rw [CategoryTheory.ofHom_mono_iff_injective, ← mono_iff_injective]

Mathlib/Algebra/Category/ModuleCat/Presheaf/Generator.lean

@@ -167,7 +167,6 @@ lemma ι_fromFreeYonedaCoproduct_apply (m : M.Elements) (X : Cᵒᵖ) (x : m.fre
   ConcreteCategory.congr_hom
     ((evaluation R X ⋙ forget _).congr_map (M.ι_fromFreeYonedaCoproduct m)) x
 
-set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma fromFreeYonedaCoproduct_app_mk (m : M.Elements) :
     M.fromFreeYonedaCoproduct.app _ (M.freeYonedaCoproductMk m) = m.2 := by

Mathlib/Algebra/Category/Ring/FinitePresentation.lean

@@ -137,7 +137,6 @@ lemma RingHom.EssFiniteType.exists_eq_comp_ι_app_of_isColimit (hf : f.hom.Finit
     rw [c.w, hg']
     rfl
 
-set_option backward.isDefEq.respectTransparency false in
 /-- If `S` is a finitely presented `R`-algebra, then `Hom_R(S, -)` preserves filtered colimits. -/
 lemma CommRingCat.preservesColimit_coyoneda_of_finitePresentation
     (S : Under R) (hS : S.hom.hom.FinitePresentation) (F : J ⥤ Under R)

Mathlib/Algebra/Category/Ring/Under/Basic.lean

@@ -34,7 +34,6 @@ instance : CoeSort (Under R) (Type u) where
 
 instance (A : Under R) : Algebra R A := RingHom.toAlgebra A.hom.hom
 
-set_option backward.isDefEq.respectTransparency false in
 /-- Turn a morphism in `Under R` into an algebra homomorphism. -/
 def toAlgHom {A B : Under R} (f : A ⟶ B) : A →ₐ[R] B where
   __ := f.right.hom

Mathlib/Algebra/DualNumber.lean

@@ -223,7 +223,7 @@ theorem range_lift
     AlgHom.map_adjoin, ← AlgHom.range_comp, Set.image_singleton, lift_apply_eps, lift_comp_inlHom,
     Algebra.map_top]
 
-/-- Show DualNumber with values x and y as an "x + y*ε" string -/
+/-- Show DualNumber with values x and y as an `"x + y*ε"` string -/
 instance instRepr [Repr R] : Repr (DualNumber R) where
   reprPrec f p :=
     (if p > 65 then (Std.Format.bracket "(" · ")") else (·)) <|

Mathlib/Algebra/FiniteSupport/Basic.lean

@@ -13,7 +13,7 @@ public import Mathlib.Data.Set.Finite.Lattice
 import Mathlib.Algebra.Group.Support
 
 /-!
-# Make fun_prop work for finite (multiplicative) support
+# Make `fun_prop` work for finite (multiplicative) support
 
 We provide API lemmas for the predicate `HasFiniteMulSupport` (and its additivized version
 `HasFiniteSupport`) on functions so that `fun_prop` can prove it for functions that are