Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - chore: classify added lemma porting notes #10791

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: classify added lemma porting notes #10791

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 6 additions & 6 deletions Mathlib/Algebra/Category/GroupCat/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -68,18 +68,18 @@ instance {X Y : GroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
instance instFunLike (X Y : GroupCat) : FunLike (X ⟶ Y) X Y :=
show FunLike (X →* Y) X Y from inferInstance

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_id {X : GroupCat} : (𝟙 X : X → X) = id := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_comp {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

@[to_additive]
lemma comp_def {X Y Z : GroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : f ≫ g = g.comp f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupCat).map f = (f : X → Y) := rfl

@[to_additive (attr := ext)]
Expand Down Expand Up @@ -217,18 +217,18 @@ instance {X Y : CommGroupCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
instance instFunLike (X Y : CommGroupCat) : FunLike (X ⟶ Y) X Y :=
show FunLike (X →* Y) X Y from inferInstance

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_id {X : CommGroupCat} : (𝟙 X : X → X) = id := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_comp {X Y Z : CommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

@[to_additive]
lemma comp_def {X Y Z : CommGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} : f ≫ g = g.comp f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma forget_map {X Y : CommGroupCat} (f : X ⟶ Y) :
(forget CommGroupCat).map f = (f : X → Y) :=
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Category/GroupWithZeroCat.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ instance groupWithZeroConcreteCategory : ConcreteCategory GroupWithZeroCat where
map := fun f => f.toFun }
forget_faithful := ⟨fun h => DFunLike.coe_injective h⟩

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : X ⟶ Y) : (forget GroupWithZeroCat).map f = f := rfl
instance hasForgetToBipointed : HasForget₂ GroupWithZeroCat Bipointed where
forget₂ :=
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Category/ModuleCat/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -227,7 +227,7 @@ theorem comp_def (f : M ⟶ N) (g : N ⟶ U) : f ≫ g = g.comp f :=
rfl
#align Module.comp_def ModuleCat.comp_def

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : M ⟶ N) : (forget (ModuleCat R)).map f = (f : M → N) := rfl

end ModuleCat
Expand Down
12 changes: 6 additions & 6 deletions Mathlib/Algebra/Category/MonCat/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,15 +93,15 @@ instance instFunLike (X Y : MonCat) : FunLike (X ⟶ Y) X Y :=
instance instMonoidHomClass (X Y : MonCat) : MonoidHomClass (X ⟶ Y) X Y :=
inferInstanceAs <| MonoidHomClass (X →* Y) X Y

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_id {X : MonCat} : (𝟙 X : X → X) = id := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_comp {X Y Z : MonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)] lemma forget_map (f : X ⟶ Y) : (forget MonCat).map f = f := rfl

@[to_additive (attr := ext)]
Expand Down Expand Up @@ -215,15 +215,15 @@ instance {X Y : CommMonCat} : CoeFun (X ⟶ Y) fun _ => X → Y where
instance instFunLike (X Y : CommMonCat) : FunLike (X ⟶ Y) X Y :=
show FunLike (X →* Y) X Y by infer_instance

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_id {X : CommMonCat} : (𝟙 X : X → X) = id := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma coe_comp {X Y Z : CommMonCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[to_additive (attr := simp)]
lemma forget_map {X Y : CommMonCat} (f : X ⟶ Y) :
(forget CommMonCat).map f = (f : X → Y) :=
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/Algebra/Category/Ring/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ lemma coe_id {X : SemiRingCat} : (𝟙 X : X → X) = id := rfl
-- Porting note (#10756): added lemma
lemma coe_comp {X Y Z : SemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : X ⟶ Y) : (forget SemiRingCat).map f = (f : X → Y) := rfl

lemma ext {X Y : SemiRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
Expand Down Expand Up @@ -215,7 +215,7 @@ lemma coe_id {X : RingCat} : (𝟙 X : X → X) = id := rfl
-- Porting note (#10756): added lemma
lemma coe_comp {X Y Z : RingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : X ⟶ Y) : (forget RingCat).map f = (f : X → Y) := rfl

lemma ext {X Y : RingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
Expand Down Expand Up @@ -321,7 +321,7 @@ lemma coe_id {X : CommSemiRingCat} : (𝟙 X : X → X) = id := rfl
-- Porting note (#10756): added lemma
lemma coe_comp {X Y Z : CommSemiRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : X ⟶ Y) : (forget CommSemiRingCat).map f = (f : X → Y) := rfl

lemma ext {X Y : CommSemiRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
Expand Down Expand Up @@ -441,7 +441,7 @@ lemma coe_id {X : CommRingCat} : (𝟙 X : X → X) = id := rfl
-- Porting note (#10756): added lemma
lemma coe_comp {X Y Z : CommRingCat} {f : X ⟶ Y} {g : Y ⟶ Z} : (f ≫ g : X → Z) = g ∘ f := rfl

-- porting note: added
-- porting note (#10756): added lemma
@[simp] lemma forget_map (f : X ⟶ Y) : (forget CommRingCat).map f = (f : X → Y) := rfl

lemma ext {X Y : CommRingCat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
Expand Down
Loading