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

Porting note: removed @[ext] #11182

Open
pitmonticone opened this issue Mar 5, 2024 · 0 comments
Open

Porting note: removed @[ext] #11182

pitmonticone opened this issue Mar 5, 2024 · 0 comments
Labels
porting-notes Mathlib3 to Mathlib4 porting notes.

Comments

@pitmonticone
Copy link
Collaborator

pitmonticone commented Mar 5, 2024 •
edited

Classifies porting notes claiming:

removed @[ext]

Examples

mathlib4/Mathlib/CategoryTheory/Subobject/Basic.lean

Lines 288 to 310 in 2a65c8d

-- Porting note: removed @[ext]
/-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
the arrows. -/
theorem eq_mk_of_comm {B A : C} {X : Subobject B} (f : A ⟶ B) [Mono f] (i : (X : C) ≅ A)
(w : i.hom ≫ f = X.arrow) : X = mk f :=
eq_of_comm (i.trans (underlyingIso f).symm) <| by simp [w]
#align category_theory.subobject.eq_mk_of_comm CategoryTheory.Subobject.eq_mk_of_comm
-- Porting note: removed @[ext]
/-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
the arrows. -/
theorem mk_eq_of_comm {B A : C} {X : Subobject B} (f : A ⟶ B) [Mono f] (i : A ≅ (X : C))
(w : i.hom ≫ X.arrow = f) : mk f = X :=
Eq.symm <| eq_mk_of_comm _ i.symm <| by rw [Iso.symm_hom, Iso.inv_comp_eq, w]
#align category_theory.subobject.mk_eq_of_comm CategoryTheory.Subobject.mk_eq_of_comm
-- Porting note: removed @[ext]
/-- To show that two subobjects are equal, it suffices to exhibit an isomorphism commuting with
the arrows. -/
theorem mk_eq_mk_of_comm {B A₁ A₂ : C} (f : A₁ ⟶ B) (g : A₂ ⟶ B) [Mono f] [Mono g] (i : A₁ ≅ A₂)
(w : i.hom ≫ g = f) : mk f = mk g :=
eq_mk_of_comm _ ((underlyingIso f).trans i) <| by simp [w]
#align category_theory.subobject.mk_eq_mk_of_comm CategoryTheory.Subobject.mk_eq_mk_of_comm

@pitmonticone pitmonticone added the porting-notes Mathlib3 to Mathlib4 porting notes. label Mar 5, 2024
@pitmonticone pitmonticone mentioned this issue Mar 5, 2024
Closed
mathlib-bors bot pushed a commit that referenced this issue Mar 5, 2024
@pitmonticone
chore: classify removed @[ext] porting notes (#11183)
15d4635 
Classifies by adding issue number #11182 to porting notes claiming: 

> removed `@[ext]`
kbuzzard pushed a commit that referenced this issue Mar 12, 2024
@pitmonticone @kbuzzard
chore: classify removed @[ext] porting notes (#11183)
92a7892 
Classifies by adding issue number #11182 to porting notes claiming: 

> removed `@[ext]`
@casavaca casavaca mentioned this issue Mar 19, 2024
Closed
dagurtomas pushed a commit that referenced this issue Mar 22, 2024
@pitmonticone @dagurtomas
chore: classify removed @[ext] porting notes (#11183)
09f8936 
Classifies by adding issue number #11182 to porting notes claiming: 

> removed `@[ext]`
mathlib-bors bot pushed a commit that referenced this issue Mar 23, 2024
@casavaca
chore: fix some @[ext] attribute (#11494)
fe6230c 
This PR contains 2 changes:

1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes.
2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159).
3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1.

Partially addresses #11182
mathlib-bors bot pushed a commit that referenced this issue Mar 23, 2024
@casavaca
chore: fix some @[ext] attribute (#11494)
76e46f2 
This PR contains 2 changes:

1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes.
2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159).
3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1.

Partially addresses #11182
utensil pushed a commit that referenced this issue Mar 26, 2024
@pitmonticone @utensil
chore: classify removed @[ext] porting notes (#11183)
d9df14e 
Classifies by adding issue number #11182 to porting notes claiming: 

> removed `@[ext]`
utensil pushed a commit that referenced this issue Mar 26, 2024
@casavaca @utensil
chore: fix some @[ext] attribute (#11494)
4d94ee4 
This PR contains 2 changes:

1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes.
2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159).
3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1.

Partially addresses #11182
Louddy pushed a commit that referenced this issue Apr 15, 2024
@pitmonticone @Louddy
chore: classify removed @[ext] porting notes (#11183)
2d38218 
Classifies by adding issue number #11182 to porting notes claiming: 

> removed `@[ext]`
Louddy pushed a commit that referenced this issue Apr 15, 2024
@casavaca @Louddy
chore: fix some @[ext] attribute (#11494)
f996ab7 
This PR contains 2 changes:

1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes.
2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159).
3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1.

Partially addresses #11182
atarnoam pushed a commit that referenced this issue Apr 16, 2024
@casavaca @atarnoam
chore: fix some @[ext] attribute (#11494)
30b27a3 
This PR contains 2 changes:

1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes.
2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159).
3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1.

Partially addresses #11182
uniwuni pushed a commit that referenced this issue Apr 19, 2024
@casavaca @uniwuni
chore: fix some @[ext] attribute (#11494)
0ae9bff 
This PR contains 2 changes:

1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes.
2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159).
3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1.

Partially addresses #11182
callesonne pushed a commit that referenced this issue Apr 22, 2024
@pitmonticone @callesonne
chore: classify removed @[ext] porting notes (#11183)
1a7de62 
Classifies by adding issue number #11182 to porting notes claiming: 

> removed `@[ext]`
callesonne pushed a commit that referenced this issue Apr 22, 2024
@casavaca @callesonne
chore: fix some @[ext] attribute (#11494)
db31ce7 
This PR contains 2 changes:

1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes.
2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159).
3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1.

Partially addresses #11182
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
porting-notes Mathlib3 to Mathlib4 porting notes.
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@pitmonticone