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

[Merged by Bors] - chore: fix outdated ext porting notes #17810

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - chore: fix outdated ext porting notes #17810

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
9 changes: 3 additions & 6 deletions Mathlib/Algebra/Polynomial/Monomial.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,12 +56,9 @@ theorem ringHom_ext {S} [Semiring S] {f g : R[X] →+* S} (h₁ : ∀ a, f (C a)
set f' := f.comp (toFinsuppIso R).symm.toRingHom with hf'
set g' := g.comp (toFinsuppIso R).symm.toRingHom with hg'
have A : f' = g' := by
-- Porting note: Was `ext; simp [..]; simpa [..] using h₂`.
ext : 1
· ext
simp [f', g', h₁, RingEquiv.toRingHom_eq_coe]
· refine MonoidHom.ext_mnat ?_
simpa [RingEquiv.toRingHom_eq_coe] using h₂
ext
simp [f', g', h₁, RingEquiv.toRingHom_eq_coe]
simpa using h₂
have B : f = f'.comp (toFinsuppIso R) := by
rw [hf', RingHom.comp_assoc]
ext x
Expand Down
1 change: 0 additions & 1 deletion Mathlib/AlgebraicGeometry/Limits.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,6 @@ def Scheme.emptyTo (X : Scheme.{u}) : ∅ ⟶ X :=

@[ext]
theorem Scheme.empty_ext {X : Scheme.{u}} (f g : ∅ ⟶ X) : f = g :=
-- Porting note (#11041): `ext` regression
Scheme.Hom.ext' (Subsingleton.elim (α := ∅ ⟶ _) _ _)

theorem Scheme.eq_emptyTo {X : Scheme.{u}} (f : ∅ ⟶ X) : f = Scheme.emptyTo X :=
Expand Down
2 changes: 0 additions & 2 deletions Mathlib/CategoryTheory/EpiMono.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -38,7 +38,6 @@ such that `f ≫ retraction f = 𝟙 X`.
Every split monomorphism is a monomorphism.
-/
/- Porting note(#5171): removed @[nolint has_nonempty_instance] -/
/- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule -/
@[ext, aesop apply safe (rule_sets := [CategoryTheory])]
structure SplitMono {X Y : C} (f : X ⟶ Y) where
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should the aesop tag be removed accordingly? What does it even do, when applied to a structure?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

So I went as far as checking the aesop source code and as far as I can tell, no idea what it's supposed to mean 🤷. Looks like removing the attribute doesn't break anything either.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the digging! @JLimperg, maybe there should be a check in aesop that one is not tagging a structure?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The rule takes the structure and register it as a rule with conclusion Type _, naturally. 🙂 But yes, Aesop should warn about this. leanprover-community/aesop#172

/-- The map splitting `f` -/
Expand All @@ -64,7 +63,6 @@ such that `section_ f ≫ f = 𝟙 Y`.
Every split epimorphism is an epimorphism.
-/
/- Porting note(#5171): removed @[nolint has_nonempty_instance] -/
/- Porting note: `@[ext]` used to accept lemmas like this. Now we add an aesop rule -/
@[ext, aesop apply safe (rule_sets := [CategoryTheory])]
structure SplitEpi {X Y : C} (f : X ⟶ Y) where
/-- The map splitting `f` -/
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Data/Set/Image.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -950,7 +950,7 @@ theorem range_inclusion (h : s ⊆ t) : range (inclusion h) = { x : t | (x : α)
-- When `f` is injective, see also `Equiv.ofInjective`.
theorem leftInverse_rangeSplitting (f : α → β) :
LeftInverse (rangeFactorization f) (rangeSplitting f) := fun x => by
apply Subtype.ext -- Porting note: why doesn't `ext` find this lemma?
ext
simp only [rangeFactorization_coe]
apply apply_rangeSplitting

Expand Down
6 changes: 2 additions & 4 deletions Mathlib/LinearAlgebra/Finsupp.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1331,8 +1331,7 @@ def splittingOfFinsuppSurjective (f : M →ₗ[R] α →₀ R) (s : Surjective f

theorem splittingOfFinsuppSurjective_splits (f : M →ₗ[R] α →₀ R) (s : Surjective f) :
f.comp (splittingOfFinsuppSurjective f s) = LinearMap.id := by
-- Porting note: `ext` can't find appropriate theorems.
refine lhom_ext' fun x => ext_ring <| Finsupp.ext fun y => ?_
ext x
dsimp [splittingOfFinsuppSurjective]
congr
rw [sum_single_index, one_smul]
Expand All @@ -1357,8 +1356,7 @@ def splittingOfFunOnFintypeSurjective [Finite α] (f : M →ₗ[R] α → R) (s
theorem splittingOfFunOnFintypeSurjective_splits [Finite α] (f : M →ₗ[R] α → R)
(s : Surjective f) : f.comp (splittingOfFunOnFintypeSurjective f s) = LinearMap.id := by
classical
-- Porting note: `ext` can't find appropriate theorems.
refine pi_ext' fun x => ext_ring <| funext fun y => ?_
ext x y
dsimp [splittingOfFunOnFintypeSurjective]
rw [linearEquivFunOnFinite_symm_single, Finsupp.sum_single_index, one_smul,
(s (Finsupp.single x 1)).choose_spec, Finsupp.single_eq_pi_single]
Expand Down
3 changes: 1 addition & 2 deletions Mathlib/LinearAlgebra/Matrix/Adjugate.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -114,8 +114,7 @@ theorem cramer_row_self (i : n) (h : ∀ j, b j = A j i) : A.cramer b = Pi.singl

@[simp]
theorem cramer_one : cramer (1 : Matrix n n α) = 1 := by
-- Porting note: was `ext i j`
refine LinearMap.pi_ext' (fun (i : n) => LinearMap.ext_ring (funext (fun (j : n) => ?_)))
ext i j
convert congr_fun (cramer_row_self (1 : Matrix n n α) (Pi.single i 1) i _) j
· simp
· intro j
Expand Down
3 changes: 1 addition & 2 deletions Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -93,8 +93,7 @@ theorem Matrix.represents_iff' {A : Matrix ι ι R} {f : Module.End R M} :
have := LinearMap.congr_fun h (Pi.single i 1)
rwa [PiToModule.fromEnd_apply_single_one, PiToModule.fromMatrix_apply_single_one] at this
· intro h
-- Porting note: was `ext`
refine LinearMap.pi_ext' (fun i => LinearMap.ext_ring ?_)
ext
simp_rw [LinearMap.comp_apply, LinearMap.coe_single, PiToModule.fromEnd_apply_single_one,
PiToModule.fromMatrix_apply_single_one]
apply h
Expand Down
3 changes: 1 addition & 2 deletions Mathlib/NumberTheory/Zsqrtd/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -931,8 +931,7 @@ def lift {d : ℤ} : { r : R // r * r = ↑d } ≃ (ℤ√d →+* R) where
ext
simp
right_inv f := by
-- Porting note: was `ext`
refine hom_ext _ _ ?_
ext
simp

/-- `lift r` is injective if `d` is non-square, and R has characteristic zero (that is, the map from
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/RepresentationTheory/Invariants.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ def invariantsEquivRepHom (X Y : Rep k G) : (linHom X.ρ Y.ρ).invariants ≃ₗ
map_add' _ _ := rfl
map_smul' _ _ := rfl
invFun f := ⟨f.hom, fun g => (mem_invariants_iff_comm _ g).2 (f.comm g)⟩
left_inv _ := by apply Subtype.ext; ext; rfl -- Porting note: Added `apply Subtype.ext`
left_inv _ := by ext; rfl
right_inv _ := by ext; rfl

end Rep
Expand Down
Loading