scratch

Author: datokrat

Archive/Imo/Imo2013Q1.lean

@@ -26,6 +26,7 @@ We prove a slightly more general version where k does not need to be strictly po
 
 
 namespace Imo2013Q1
+
 theorem arith_lemma (k n : ℕ) : 0 < 2 * n + 2 ^ k.succ := by positivity
 
 theorem prod_lemma (m : ℕ → ℕ+) (k : ℕ) (nm : ℕ+) :

Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean

@@ -617,8 +617,7 @@ protected noncomputable def unit' : 𝟭 (ModuleCat S) ⟶ restrictScalars f ⋙
   naturality Y Y' g :=
     hom_ext <| LinearMap.ext fun y : Y => CoextendScalars.ext <| LinearMap.ext fun s : S => by
       -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): previously simp [CoextendScalars.map_apply]
-      simp only [Functor.id_map, Functor.id_obj,
-        Functor.comp_map]
+      simp only [Functor.id_map, Functor.id_obj, Functor.comp_map]
       change s • (g y) = g (s • y)
       rw [map_smul]