Skip to content

Commit

Permalink
chore: classify previously simp porting notes (#10789)
Browse files Browse the repository at this point in the history
Classifies by adding issue number (#10745) to porting note claiming anything semantically equivalent to `was simp`. 

Related merged PR: #10746.
  • Loading branch information
pitmonticone committed Feb 21, 2024
1 parent 7a17e9d commit ba55c68
Showing 1 changed file with 4 additions and 4 deletions.
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
Expand Up @@ -500,7 +500,7 @@ protected def unit' : 𝟭 (ModuleCat S) ⟶ restrictScalars f ⋙ coextendScala
app Y := app' f Y
naturality Y Y' g :=
LinearMap.ext fun y : Y => LinearMap.ext fun s : S => by
-- Porting note: previously simp [CoextendScalars.map_apply]
-- Porting note (#10745): previously simp [CoextendScalars.map_apply]
simp only [ModuleCat.coe_comp, Functor.id_map, Functor.id_obj, Functor.comp_obj,
Functor.comp_map]
rw [coe_comp, coe_comp, Function.comp, Function.comp]
Expand Down Expand Up @@ -545,12 +545,12 @@ def restrictCoextendScalarsAdj {R : Type u₁} {S : Type u₂} [Ring R] [Ring S]
{ toFun := RestrictionCoextensionAdj.HomEquiv.fromRestriction.{u₁,u₂,v} f
invFun := RestrictionCoextensionAdj.HomEquiv.toRestriction.{u₁,u₂,v} f
left_inv := fun g => LinearMap.ext fun x : X => by
-- Porting note: once just simp
-- Porting note (#10745): once just simp
rw [RestrictionCoextensionAdj.HomEquiv.toRestriction_apply, AddHom.toFun_eq_coe,
LinearMap.coe_toAddHom, RestrictionCoextensionAdj.HomEquiv.fromRestriction_apply_apply,
one_smul]
right_inv := fun g => LinearMap.ext fun x => LinearMap.ext fun s : S => by
-- Porting note: once just simp
-- Porting note (#10745): once just simp
rw [RestrictionCoextensionAdj.HomEquiv.fromRestriction_apply_apply,
RestrictionCoextensionAdj.HomEquiv.toRestriction_apply, AddHom.toFun_eq_coe,
LinearMap.coe_toAddHom, LinearMap.map_smulₛₗ, RingHom.id_apply,
Expand All @@ -559,7 +559,7 @@ def restrictCoextendScalarsAdj {R : Type u₁} {S : Type u₂} [Ring R] [Ring S]
counit := RestrictionCoextensionAdj.counit'.{u₁,u₂,v} f
homEquiv_unit := LinearMap.ext fun y => rfl
homEquiv_counit := fun {X Y g} => LinearMap.ext <| by
-- Porting note: previously simp [RestrictionCoextensionAdj.counit']
-- Porting note (#10745): previously simp [RestrictionCoextensionAdj.counit']
intro x; dsimp
rw [coe_comp, Function.comp]
change _ = (((restrictScalars f).map g) x).toFun (1 : S)
Expand Down

0 comments on commit ba55c68

Please sign in to comment.