From 1243cdbe575665908419428a40bc8c86cc57d289 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 1 Oct 2024 02:24:24 +0000 Subject: [PATCH] chore: adaptations for nightly-2024-09-30 (#17296) Co-authored-by: leanprover-community-mathlib4-bot Co-authored-by: Kim Morrison --- .../ContinuedFractions/ConvergentsEquiv.lean | 3 -- Mathlib/Algebra/Free.lean | 1 - .../Algebra/Group/Submonoid/Operations.lean | 2 +- .../Group/Subsemigroup/Operations.lean | 2 +- .../GroupWithZero/NonZeroDivisors.lean | 2 +- .../Homology/HomologicalBicomplex.lean | 2 +- Mathlib/Algebra/Homology/TotalComplex.lean | 4 +- .../Algebra/Homology/TotalComplexShift.lean | 4 +- Mathlib/Algebra/Module/Submodule/Lattice.lean | 2 +- Mathlib/Algebra/Order/Group/Abs.lean | 4 +- Mathlib/Algebra/Order/Group/Defs.lean | 6 +-- Mathlib/Algebra/Star/Free.lean | 2 +- .../Morphisms/QuasiCompact.lean | 10 ++++- Mathlib/AlgebraicGeometry/OpenImmersion.lean | 8 ++-- .../ProjectiveSpectrum/Scheme.lean | 2 +- Mathlib/AlgebraicGeometry/Pullbacks.lean | 2 +- .../Instances.lean | 22 +++++----- .../NonUnital.lean | 2 +- .../ContinuousFunctionalCalculus/Unital.lean | 4 +- Mathlib/CategoryTheory/Extensive.lean | 4 +- .../Functor/KanExtension/Adjunction.lean | 2 +- .../CategoryTheory/GradedObject/Monoidal.lean | 2 +- .../Limits/Shapes/Pullback/CommSq.lean | 16 +++---- .../MorphismProperty/Basic.lean | 16 +++---- .../CategoryTheory/Triangulated/Functor.lean | 2 +- Mathlib/Combinatorics/SimpleGraph/Path.lean | 2 +- Mathlib/Data/Array/ExtractLemmas.lean | 8 ++-- Mathlib/Data/List/Basic.lean | 13 ------ Mathlib/Data/List/Cycle.lean | 4 +- Mathlib/Data/List/Indexes.lean | 2 +- Mathlib/Data/List/Lemmas.lean | 2 + Mathlib/Data/List/MinMax.lean | 22 ++++++---- Mathlib/Data/List/Perm.lean | 22 +--------- Mathlib/Data/Nat/Defs.lean | 7 +-- Mathlib/Data/Option/Defs.lean | 4 -- Mathlib/Data/Ordmap/Ordset.lean | 2 +- Mathlib/Data/Setoid/Basic.lean | 2 +- Mathlib/Data/ZMod/Defs.lean | 2 +- .../IsAlgClosed/AlgebraicClosure.lean | 2 +- Mathlib/FieldTheory/PurelyInseparable.lean | 2 +- Mathlib/FieldTheory/Separable.lean | 2 +- Mathlib/FieldTheory/SeparableDegree.lean | 2 +- .../Geometry/RingedSpace/OpenImmersion.lean | 44 +++++++++---------- .../RingedSpace/PresheafedSpace/Gluing.lean | 31 +++++++------ Mathlib/GroupTheory/OrderOfElement.lean | 2 +- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean | 2 +- .../LinearAlgebra/Alternating/DomCoprod.lean | 2 +- .../CliffordAlgebra/Grading.lean | 6 +-- Mathlib/LinearAlgebra/Dual.lean | 2 +- .../LinearAlgebra/FiniteDimensional/Defs.lean | 2 +- Mathlib/LinearAlgebra/Semisimple.lean | 2 +- .../NumberField/Units/DirichletTheorem.lean | 2 +- Mathlib/Order/Directed.lean | 2 +- Mathlib/Order/Filter/Bases.lean | 4 +- Mathlib/RingTheory/AdjoinRoot.lean | 4 +- .../IsIntegralClosure/Basic.lean | 6 +-- Mathlib/RingTheory/LocalRing/Module.lean | 26 ++++++----- .../RingTheory/Localization/FractionRing.lean | 2 +- Mathlib/RingTheory/RingHomProperties.lean | 6 ++- Mathlib/RingTheory/SimpleRing/Basic.lean | 2 +- Mathlib/RingTheory/Smooth/StandardSmooth.lean | 4 +- Mathlib/Tactic/Ring/Basic.lean | 2 +- .../Topology/Algebra/Valued/NormedValued.lean | 2 +- .../Category/LightProfinite/Extend.lean | 4 +- .../Topology/Category/Profinite/Extend.lean | 4 +- Mathlib/Util/CountHeartbeats.lean | 4 +- lake-manifest.json | 4 +- lean-toolchain | 2 +- test/aesop_cat.lean | 2 + test/says.lean | 3 +- 70 files changed, 190 insertions(+), 214 deletions(-) diff --git a/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean b/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean index 2adf582909701..99e76fa64a5f5 100644 --- a/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean +++ b/Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean @@ -166,9 +166,6 @@ theorem succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq : gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2) by simpa only [convs'Aux, s_head_eq] - have : convs'Aux s.tail (m + 2) = convs'Aux (squashSeq s.tail m) (m + 1) := by - refine IH gp_succ_n ?_ - simpa [Stream'.Seq.get?_tail] using s_succ_nth_eq have : (squashSeq s (m + 1)).head = some gp_head := (squashSeq_nth_of_lt m.succ_pos).trans s_head_eq simp_all [convs'Aux, squashSeq_succ_n_tail_eq_squashSeq_tail_n] diff --git a/Mathlib/Algebra/Free.lean b/Mathlib/Algebra/Free.lean index 1b0f927525cca..134a4e81ed9ff 100644 --- a/Mathlib/Algebra/Free.lean +++ b/Mathlib/Algebra/Free.lean @@ -6,7 +6,6 @@ Authors: Kenny Lau import Mathlib.Algebra.Group.Equiv.Basic import Mathlib.Control.Applicative import Mathlib.Control.Traversable.Basic -import Mathlib.Data.List.Basic import Mathlib.Logic.Equiv.Defs import Mathlib.Tactic.AdaptationNote diff --git a/Mathlib/Algebra/Group/Submonoid/Operations.lean b/Mathlib/Algebra/Group/Submonoid/Operations.lean index 1bf4b67f90258..f84160423a5b5 100644 --- a/Mathlib/Algebra/Group/Submonoid/Operations.lean +++ b/Mathlib/Algebra/Group/Submonoid/Operations.lean @@ -591,7 +591,7 @@ theorem closure_closure_coe_preimage {s : Set M} : closure (((↑) : closure s Subtype.recOn x fun x hx _ => by refine closure_induction' (p := fun y hy ↦ (⟨y, hy⟩ : closure s) ∈ closure (((↑) : closure s → M) ⁻¹' s)) - (fun g hg => subset_closure hg) ?_ (fun g₁ g₂ hg₁ hg₂ => ?_) hx + _ (fun g hg => subset_closure hg) ?_ (fun g₁ g₂ hg₁ hg₂ => ?_) hx · exact Submonoid.one_mem _ · exact Submonoid.mul_mem _ diff --git a/Mathlib/Algebra/Group/Subsemigroup/Operations.lean b/Mathlib/Algebra/Group/Subsemigroup/Operations.lean index 05de353785319..85f523619d7ca 100644 --- a/Mathlib/Algebra/Group/Subsemigroup/Operations.lean +++ b/Mathlib/Algebra/Group/Subsemigroup/Operations.lean @@ -501,7 +501,7 @@ theorem closure_closure_coe_preimage {s : Set M} : eq_top_iff.2 fun x => Subtype.recOn x fun _ hx' _ => closure_induction' (p := fun y hy ↦ (⟨y, hy⟩ : closure s) ∈ closure (((↑) : closure s → M) ⁻¹' s)) - (fun _ hg => subset_closure hg) (fun _ _ _ _ => Subsemigroup.mul_mem _) hx' + _ (fun _ hg => subset_closure hg) (fun _ _ _ _ => Subsemigroup.mul_mem _) hx' /-- Given `Subsemigroup`s `s`, `t` of semigroups `M`, `N` respectively, `s × t` as a subsemigroup of `M × N`. -/ diff --git a/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean b/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean index 3c09328f414ca..2c4e1832cb5a3 100644 --- a/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean +++ b/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean @@ -304,7 +304,7 @@ theorem mk_mem_nonZeroDivisors_associates : Associates.mk a ∈ (Associates M₀ /-- The non-zero divisors of associates of a monoid with zero `M₀` are isomorphic to the associates of the non-zero divisors of `M₀` under the map `⟨⟦a⟧, _⟩ ↦ ⟦⟨a, _⟩⟧`. -/ def associatesNonZeroDivisorsEquiv : (Associates M₀)⁰ ≃* Associates M₀⁰ where - toEquiv := .subtypeQuotientEquivQuotientSubtype (s₂ := Associated.setoid _) + toEquiv := .subtypeQuotientEquivQuotientSubtype _ (s₂ := Associated.setoid _) (· ∈ nonZeroDivisors _) (by simp [mem_nonZeroDivisors_iff, Quotient.forall, Associates.mk_mul_mk]) (by simp [Associated.setoid]) diff --git a/Mathlib/Algebra/Homology/HomologicalBicomplex.lean b/Mathlib/Algebra/Homology/HomologicalBicomplex.lean index b02aad6a648b8..dbd85f9d8e710 100644 --- a/Mathlib/Algebra/Homology/HomologicalBicomplex.lean +++ b/Mathlib/Algebra/Homology/HomologicalBicomplex.lean @@ -205,7 +205,7 @@ def XXIsoOfEq {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : @[simp] lemma XXIsoOfEq_rfl (i₁ : I₁) (i₂ : I₂) : - K.XXIsoOfEq (rfl : i₁ = i₁) (rfl : i₂ = i₂) = Iso.refl _ := rfl + K.XXIsoOfEq _ _ _ (rfl : i₁ = i₁) (rfl : i₂ = i₂) = Iso.refl _ := rfl end HomologicalComplex₂ diff --git a/Mathlib/Algebra/Homology/TotalComplex.lean b/Mathlib/Algebra/Homology/TotalComplex.lean index 73fb3959181c0..645d747de064f 100644 --- a/Mathlib/Algebra/Homology/TotalComplex.lean +++ b/Mathlib/Algebra/Homology/TotalComplex.lean @@ -260,7 +260,7 @@ noncomputable def ιTotal (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂) @[reassoc (attr := simp)] lemma XXIsoOfEq_hom_ιTotal {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂) (i₁₂ : I₁₂) (h : ComplexShape.π c₁ c₂ c₁₂ (y₁, y₂) = i₁₂) : - (K.XXIsoOfEq h₁ h₂).hom ≫ K.ιTotal c₁₂ y₁ y₂ i₁₂ h = + (K.XXIsoOfEq _ _ _ h₁ h₂).hom ≫ K.ιTotal c₁₂ y₁ y₂ i₁₂ h = K.ιTotal c₁₂ x₁ x₂ i₁₂ (by rw [h₁, h₂, h]) := by subst h₁ h₂ simp @@ -268,7 +268,7 @@ lemma XXIsoOfEq_hom_ιTotal {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : @[reassoc (attr := simp)] lemma XXIsoOfEq_inv_ιTotal {x₁ y₁ : I₁} (h₁ : x₁ = y₁) {x₂ y₂ : I₂} (h₂ : x₂ = y₂) (i₁₂ : I₁₂) (h : ComplexShape.π c₁ c₂ c₁₂ (x₁, x₂) = i₁₂) : - (K.XXIsoOfEq h₁ h₂).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h = + (K.XXIsoOfEq _ _ _ h₁ h₂).inv ≫ K.ιTotal c₁₂ x₁ x₂ i₁₂ h = K.ιTotal c₁₂ y₁ y₂ i₁₂ (by rw [← h, h₁, h₂]) := by subst h₁ h₂ simp diff --git a/Mathlib/Algebra/Homology/TotalComplexShift.lean b/Mathlib/Algebra/Homology/TotalComplexShift.lean index 8d32945310df2..345677aa57934 100644 --- a/Mathlib/Algebra/Homology/TotalComplexShift.lean +++ b/Mathlib/Algebra/Homology/TotalComplexShift.lean @@ -129,7 +129,7 @@ noncomputable def totalShift₁XIso (n n' : ℤ) (h : n + x = n') : (((shiftFunctor₁ C x).obj K).total (up ℤ)).X n ≅ (K.total (up ℤ)).X n' where hom := totalDesc _ (fun p q hpq => K.ιTotal (up ℤ) (p + x) q n' (by dsimp at hpq ⊢; omega)) inv := totalDesc _ (fun p q hpq => - (K.XXIsoOfEq (Int.sub_add_cancel p x) rfl).inv ≫ + (K.XXIsoOfEq _ _ _ (Int.sub_add_cancel p x) rfl).inv ≫ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) (p - x) q n (by dsimp at hpq ⊢; omega)) hom_inv_id := by @@ -235,7 +235,7 @@ noncomputable def totalShift₂XIso (n n' : ℤ) (h : n + y = n') : hom := totalDesc _ (fun p q hpq => (p * y).negOnePow • K.ιTotal (up ℤ) p (q + y) n' (by dsimp at hpq ⊢; omega)) inv := totalDesc _ (fun p q hpq => (p * y).negOnePow • - (K.XXIsoOfEq rfl (Int.sub_add_cancel q y)).inv ≫ + (K.XXIsoOfEq _ _ _ rfl (Int.sub_add_cancel q y)).inv ≫ ((shiftFunctor₂ C y).obj K).ιTotal (up ℤ) p (q - y) n (by dsimp at hpq ⊢; omega)) hom_inv_id := by ext p q h diff --git a/Mathlib/Algebra/Module/Submodule/Lattice.lean b/Mathlib/Algebra/Module/Submodule/Lattice.lean index 1b9c97d71bbe6..7b582582da3ac 100644 --- a/Mathlib/Algebra/Module/Submodule/Lattice.lean +++ b/Mathlib/Algebra/Module/Submodule/Lattice.lean @@ -287,7 +287,7 @@ theorem toAddSubmonoid_sSup (s : Set (Submodule R M)) : { toAddSubmonoid := sSup (toAddSubmonoid '' s) smul_mem' := fun t {m} h ↦ by simp_rw [AddSubsemigroup.mem_carrier, AddSubmonoid.mem_toSubsemigroup, sSup_eq_iSup'] at h ⊢ - refine AddSubmonoid.iSup_induction' + refine AddSubmonoid.iSup_induction' _ (C := fun x _ ↦ t • x ∈ ⨆ p : toAddSubmonoid '' s, (p : AddSubmonoid M)) ?_ ?_ (fun x y _ _ ↦ ?_) h · rintro ⟨-, ⟨p : Submodule R M, hp : p ∈ s, rfl⟩⟩ x (hx : x ∈ p) diff --git a/Mathlib/Algebra/Order/Group/Abs.lean b/Mathlib/Algebra/Order/Group/Abs.lean index 3d6763c037cfa..9693c189cfb6c 100644 --- a/Mathlib/Algebra/Order/Group/Abs.lean +++ b/Mathlib/Algebra/Order/Group/Abs.lean @@ -94,7 +94,7 @@ theorem apply_abs_le_mul_of_one_le {β : Type*} [MulOneClass β] [Preorder β] theorem abs_add (a b : α) : |a + b| ≤ |a| + |b| := abs_le.2 ⟨(neg_add |a| |b|).symm ▸ - add_le_add ((@neg_le α ..).2 <| neg_le_abs _) ((@neg_le α ..).2 <| neg_le_abs _), + add_le_add (neg_le.2 <| neg_le_abs _) (neg_le.2 <| neg_le_abs _), add_le_add (le_abs_self _) (le_abs_self _)⟩ theorem abs_add' (a b : α) : |a| ≤ |b| + |b + a| := by simpa using abs_add (-b) (b + a) @@ -122,7 +122,7 @@ theorem sub_lt_of_abs_sub_lt_right (h : |a - b| < c) : a - c < b := sub_lt_of_abs_sub_lt_left (abs_sub_comm a b ▸ h) theorem abs_sub_abs_le_abs_sub (a b : α) : |a| - |b| ≤ |a - b| := - (@sub_le_iff_le_add α ..).2 <| + sub_le_iff_le_add.2 <| calc |a| = |a - b + b| := by rw [sub_add_cancel] _ ≤ |a - b| + |b| := abs_add _ _ diff --git a/Mathlib/Algebra/Order/Group/Defs.lean b/Mathlib/Algebra/Order/Group/Defs.lean index 15946e02be003..53b53337c45d3 100644 --- a/Mathlib/Algebra/Order/Group/Defs.lean +++ b/Mathlib/Algebra/Order/Group/Defs.lean @@ -175,13 +175,11 @@ variable [OrderedCommGroup α] {a b : α} @[to_additive (attr := gcongr) neg_le_neg] theorem inv_le_inv' : a ≤ b → b⁻¹ ≤ a⁻¹ := - -- Porting note: explicit type annotation was not needed before. - (@inv_le_inv_iff α ..).mpr + inv_le_inv_iff.mpr @[to_additive (attr := gcongr) neg_lt_neg] theorem inv_lt_inv' : a < b → b⁻¹ < a⁻¹ := - -- Porting note: explicit type annotation was not needed before. - (@inv_lt_inv_iff α ..).mpr + inv_lt_inv_iff.mpr -- The additive version is also a `linarith` lemma. @[to_additive] diff --git a/Mathlib/Algebra/Star/Free.lean b/Mathlib/Algebra/Star/Free.lean index eefbd4ba0c208..b29ed2137d81e 100644 --- a/Mathlib/Algebra/Star/Free.lean +++ b/Mathlib/Algebra/Star/Free.lean @@ -48,7 +48,7 @@ instance : StarRing (FreeAlgebra R X) where unfold Star.star simp only [Function.comp_apply] let y := lift R (X := X) (MulOpposite.op ∘ ι R) - apply induction (C := fun x ↦ (y (y x).unop).unop = x) _ _ _ _ x + refine induction (C := fun x ↦ (y (y x).unop).unop = x) _ _ ?_ ?_ ?_ ?_ x · intros simp only [AlgHom.commutes, MulOpposite.algebraMap_apply, MulOpposite.unop_op] · intros diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean index c85901ed45bc9..cf3a6124cc51f 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean @@ -198,7 +198,15 @@ theorem exists_pow_mul_eq_zero_of_res_basicOpen_eq_zero_of_isAffineOpen (X : Sch {U : X.Opens} (hU : IsAffineOpen U) (x f : Γ(X, U)) (H : x |_ X.basicOpen f = 0) : ∃ n : ℕ, f ^ n * x = 0 := by rw [← map_zero (X.presheaf.map (homOfLE <| X.basicOpen_le f : X.basicOpen f ⟶ U).op)] at H - obtain ⟨n, e⟩ := (hU.isLocalization_basicOpen f).exists_of_eq H + #adaptation_note + /-- + Prior to nightly-2024-09-29, we could use dot notation here: + `(hU.isLocalization_basicOpen f).exists_of_eq H` + This is no longer possible; + likely changing the signature of `IsLocalization.Away.exists_of_eq` is in order. + -/ + obtain ⟨n, e⟩ := + @IsLocalization.Away.exists_of_eq _ _ _ _ _ _ (hU.isLocalization_basicOpen f) _ _ H exact ⟨n, by simpa [mul_comm x] using e⟩ /-- If `x : Γ(X, U)` is zero on `D(f)` for some `f : Γ(X, U)`, and `U` is quasi-compact, then diff --git a/Mathlib/AlgebraicGeometry/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/OpenImmersion.lean index c65f7aa086fbc..5ace362109bfb 100644 --- a/Mathlib/AlgebraicGeometry/OpenImmersion.lean +++ b/Mathlib/AlgebraicGeometry/OpenImmersion.lean @@ -431,7 +431,7 @@ instance pullback_fst_of_right : IsOpenImmersion (pullback.fst g f) := by rw [← pullbackSymmetry_hom_comp_snd] -- Porting note: was just `infer_instance`, it is a bit weird that no explicit class instance is -- provided but still class inference fail to find this - exact LocallyRingedSpace.IsOpenImmersion.comp (H := inferInstance) _ + exact LocallyRingedSpace.IsOpenImmersion.comp (H := inferInstance) _ _ instance pullback_to_base [IsOpenImmersion g] : IsOpenImmersion (limit.π (cospan f g) WalkingCospan.one) := by @@ -439,14 +439,14 @@ instance pullback_to_base [IsOpenImmersion g] : change IsOpenImmersion (_ ≫ f) -- Porting note: was just `infer_instance`, it is a bit weird that no explicit class instance is -- provided but still class inference fail to find this - exact LocallyRingedSpace.IsOpenImmersion.comp (H := inferInstance) _ + exact LocallyRingedSpace.IsOpenImmersion.comp (H := inferInstance) _ _ instance forgetToTopPreservesOfLeft : PreservesLimit (cospan f g) Scheme.forgetToTop := by delta Scheme.forgetToTop - apply @Limits.compPreservesLimit (K := cospan f g) (F := forget) + refine @Limits.compPreservesLimit _ _ _ _ _ _ (K := cospan f g) _ _ (F := forget) (G := LocallyRingedSpace.forgetToTop) ?_ ?_ · infer_instance - apply @preservesLimitOfIsoDiagram (F := _) _ _ _ _ _ _ (diagramIsoCospan.{u} _).symm ?_ + refine @preservesLimitOfIsoDiagram _ _ _ _ _ _ _ _ _ (diagramIsoCospan.{u} _).symm ?_ dsimp [LocallyRingedSpace.forgetToTop] infer_instance diff --git a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean index 26f2fbd7457aa..938d2b0845645 100644 --- a/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean +++ b/Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean @@ -811,7 +811,7 @@ If `f ∈ A` is a homogeneous element of positive degree, then the projective sp -/ def projIsoSpec (f) {m} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) : (Proj| pbo f) ≅ (Spec (A⁰_ f)) := - @asIso (f := toSpec 𝒜 f) (isIso_toSpec 𝒜 f f_deg hm) + @asIso _ _ _ _ (f := toSpec 𝒜 f) (isIso_toSpec 𝒜 f f_deg hm) /-- This is the scheme `Proj(A)` for any `ℕ`-graded ring `A`. diff --git a/Mathlib/AlgebraicGeometry/Pullbacks.lean b/Mathlib/AlgebraicGeometry/Pullbacks.lean index 3727fd53e485a..4ceafda2c4dd6 100644 --- a/Mathlib/AlgebraicGeometry/Pullbacks.lean +++ b/Mathlib/AlgebraicGeometry/Pullbacks.lean @@ -507,7 +507,7 @@ def openCoverOfBase' (𝒰 : OpenCover Z) (f : X ⟶ Z) (g : Y ⟶ Z) : OpenCove pasteVertIsPullback rfl (pullbackIsPullback g (𝒰.map i)) (pullbackIsPullback (pullback.snd g (𝒰.map i)) (pullback.snd f (𝒰.map i))) refine - @openCoverOfIsIso + @openCoverOfIsIso _ _ (f := (pullbackSymmetry _ _).hom ≫ (limit.isoLimitCone ⟨_, this⟩).inv ≫ pullback.map _ _ _ _ (𝟙 _) (𝟙 _) (𝟙 _) ?_ ?_) inferInstance · simp [← pullback.condition] diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean index d1e7e6f1539c8..b1b31df7543ab 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean @@ -605,7 +605,7 @@ variable {A : Type*} [TopologicalSpace A] [Ring A] [StarRing A] [Algebra ℂ A] lemma cfcHom_real_eq_restrict {a : A} (ha : IsSelfAdjoint a) : cfcHom ha = ha.spectrumRestricts.starAlgHom (cfcHom ha.isStarNormal) (f := Complex.reCLM) := - ha.spectrumRestricts.cfcHom_eq_restrict Complex.isometry_ofReal.uniformEmbedding + ha.spectrumRestricts.cfcHom_eq_restrict _ Complex.isometry_ofReal.uniformEmbedding ha ha.isStarNormal lemma cfc_real_eq_complex {a : A} (f : ℝ → ℝ) (ha : IsSelfAdjoint a := by cfc_tac) : @@ -626,7 +626,7 @@ variable {A : Type*} [TopologicalSpace A] [NonUnitalRing A] [StarRing A] [Module lemma cfcₙHom_real_eq_restrict {a : A} (ha : IsSelfAdjoint a) : cfcₙHom ha = (ha.quasispectrumRestricts.2).nonUnitalStarAlgHom (cfcₙHom ha.isStarNormal) (f := Complex.reCLM) := - ha.quasispectrumRestricts.2.cfcₙHom_eq_restrict Complex.isometry_ofReal.uniformEmbedding + ha.quasispectrumRestricts.2.cfcₙHom_eq_restrict _ Complex.isometry_ofReal.uniformEmbedding ha ha.isStarNormal lemma cfcₙ_real_eq_complex {a : A} (f : ℝ → ℝ) (ha : IsSelfAdjoint a := by cfc_tac) : @@ -649,14 +649,14 @@ variable {A : Type*} [TopologicalSpace A] [Ring A] [PartialOrder A] [StarRing A] lemma cfcHom_nnreal_eq_restrict {a : A} (ha : 0 ≤ a) : cfcHom ha = (SpectrumRestricts.nnreal_of_nonneg ha).starAlgHom - (cfcHom (IsSelfAdjoint.of_nonneg ha)) := by - apply (SpectrumRestricts.nnreal_of_nonneg ha).cfcHom_eq_restrict uniformEmbedding_subtype_val + (cfcHom (IsSelfAdjoint.of_nonneg ha)) := + (SpectrumRestricts.nnreal_of_nonneg ha).cfcHom_eq_restrict _ uniformEmbedding_subtype_val _ _ lemma cfc_nnreal_eq_real {a : A} (f : ℝ≥0 → ℝ≥0) (ha : 0 ≤ a := by cfc_tac) : cfc f a = cfc (fun x ↦ f x.toNNReal : ℝ → ℝ) a := by replace ha : 0 ≤ a := ha -- hack to avoid issues caused by autoParam - apply (SpectrumRestricts.nnreal_of_nonneg ha).cfc_eq_restrict - uniformEmbedding_subtype_val ha (.of_nonneg ha) + exact (SpectrumRestricts.nnreal_of_nonneg ha).cfc_eq_restrict _ + uniformEmbedding_subtype_val ha (.of_nonneg ha) _ end NNRealEqReal @@ -673,15 +673,15 @@ variable {A : Type*} [TopologicalSpace A] [NonUnitalRing A] [PartialOrder A] [St lemma cfcₙHom_nnreal_eq_restrict {a : A} (ha : 0 ≤ a) : cfcₙHom ha = (QuasispectrumRestricts.nnreal_of_nonneg ha).nonUnitalStarAlgHom - (cfcₙHom (IsSelfAdjoint.of_nonneg ha)) := by - apply (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙHom_eq_restrict - uniformEmbedding_subtype_val + (cfcₙHom (IsSelfAdjoint.of_nonneg ha)) := + (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙHom_eq_restrict _ + uniformEmbedding_subtype_val _ _ lemma cfcₙ_nnreal_eq_real {a : A} (f : ℝ≥0 → ℝ≥0) (ha : 0 ≤ a := by cfc_tac) : cfcₙ f a = cfcₙ (fun x ↦ f x.toNNReal : ℝ → ℝ) a := by replace ha : 0 ≤ a := ha -- hack to avoid issues caused by autoParam - apply (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙ_eq_restrict - uniformEmbedding_subtype_val ha (.of_nonneg ha) + exact (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙ_eq_restrict _ + uniformEmbedding_subtype_val ha (.of_nonneg ha) _ end NNRealEqRealNonUnital diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean index 3ebb272f0dee6..d9e3fec765654 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean @@ -421,7 +421,7 @@ lemma cfcₙ_comp (g f : R → R) (a : A) ext simp rw [cfcₙ_apply .., cfcₙ_apply f a, - cfcₙ_apply _ (by convert hg) (ha := cfcₙHom_predicate (show p a from ha) _) , + cfcₙ_apply _ _ (by convert hg) (ha := cfcₙHom_predicate (show p a from ha) _), ← cfcₙHom_comp _ _] swap · exact ⟨.mk _ <| hf.restrict.codRestrict fun x ↦ by rw [sp_eq]; use x.1; simp, Subtype.ext hf0⟩ diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean index 89017072beb7c..8b6473cba0de3 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean @@ -723,7 +723,7 @@ noncomputable def cfcUnits (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) lemma cfcUnits_pow (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (n : ℕ) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac) (ha : p a := by cfc_tac) : (cfcUnits f a hf') ^ n = - cfcUnits (forall₂_imp (fun _ _ ↦ pow_ne_zero n) hf') (hf := hf.pow n) := by + cfcUnits _ _ (forall₂_imp (fun _ _ ↦ pow_ne_zero n) hf') (hf := hf.pow n) := by ext cases n with | zero => simp [cfc_const_one R a] @@ -778,7 +778,7 @@ lemma cfcUnits_zpow (hf' : ∀ x ∈ spectrum R a, f x ≠ 0) (n : ℤ) | negSucc n => simp only [zpow_negSucc, ← inv_pow] ext - exact cfc_pow (hf := hf.inv₀ hf') _ |>.symm + exact cfc_pow (hf := hf.inv₀ hf') .. |>.symm lemma cfc_zpow (a : Aˣ) (n : ℤ) (ha : p a := by cfc_tac) : cfc (fun x : R ↦ x ^ n) (a : A) = ↑(a ^ n) := by diff --git a/Mathlib/CategoryTheory/Extensive.lean b/Mathlib/CategoryTheory/Extensive.lean index 887e41f0debb8..94619f08a21bb 100644 --- a/Mathlib/CategoryTheory/Extensive.lean +++ b/Mathlib/CategoryTheory/Extensive.lean @@ -527,7 +527,7 @@ instance FinitaryPreExtensive.hasPullbacks_of_inclusions [FinitaryPreExtensive C {α : Type*} (f : X ⟶ Z) {Y : (a : α) → C} (i : (a : α) → Y a ⟶ Z) [Finite α] [hi : IsIso (Sigma.desc i)] (a : α) : HasPullback f (i a) := by apply FinitaryPreExtensive.hasPullbacks_of_is_coproduct (c := Cofan.mk Z i) - exact @IsColimit.ofPointIso (t := Cofan.mk Z i) (P := _) hi + exact @IsColimit.ofPointIso (t := Cofan.mk Z i) (P := _) (i := hi) lemma FinitaryPreExtensive.sigma_desc_iso [FinitaryPreExtensive C] {α : Type} [Finite α] {X : C} {Z : α → C} (π : (a : α) → Z a ⟶ X) {Y : C} (f : Y ⟶ X) (hπ : IsIso (Sigma.desc π)) : @@ -536,7 +536,7 @@ lemma FinitaryPreExtensive.sigma_desc_iso [FinitaryPreExtensive C] {α : Type} [ change IsIso (this.coconePointUniqueUpToIso (getColimitCocone _).2).inv infer_instance let this : IsColimit (Cofan.mk X π) := by - refine @IsColimit.ofPointIso (t := Cofan.mk X π) (P := coproductIsCoproduct Z) ?_ + refine @IsColimit.ofPointIso (t := Cofan.mk X π) (P := coproductIsCoproduct Z) (i := ?_) convert hπ simp [coproductIsCoproduct] refine (FinitaryPreExtensive.isUniversal_finiteCoproducts this diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean index 57c9c1c9353e0..fe8433c905fb7 100644 --- a/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean +++ b/Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean @@ -168,7 +168,7 @@ precomposition by `L`. -/ noncomputable def ranAdjunction : (whiskeringLeft C D H).obj L ⊣ L.ran := Adjunction.mkOfHomEquiv { homEquiv := fun F G => - (homEquivOfIsRightKanExtension (α := L.ranCounit.app G) F).symm + (homEquivOfIsRightKanExtension (α := L.ranCounit.app G) _ F).symm homEquiv_naturality_right := fun {F G₁ G₂} β f ↦ hom_ext_of_isRightKanExtension _ (L.ranCounit.app G₂) _ _ (by ext X diff --git a/Mathlib/CategoryTheory/GradedObject/Monoidal.lean b/Mathlib/CategoryTheory/GradedObject/Monoidal.lean index 917484d456465..b005a034c6b49 100644 --- a/Mathlib/CategoryTheory/GradedObject/Monoidal.lean +++ b/Mathlib/CategoryTheory/GradedObject/Monoidal.lean @@ -325,7 +325,7 @@ lemma left_tensor_tensorObj₃_ext {j : I} {A : C} (Z : C) (_ ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ≫ f = (_ ◁ ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) ≫ g) : f = g := by refine (@isColimitOfPreserves C _ C _ _ _ _ ((curriedTensor C).obj Z) _ - (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj (H := H) j) hZ).hom_ext ?_ + (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj (H := H) (j := j)) hZ).hom_ext ?_ intro ⟨⟨i₁, i₂, i₃⟩, hi⟩ exact h _ _ _ hi diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean index e22ae9d2d8bed..423fed53f4080 100644 --- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean +++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean @@ -280,22 +280,22 @@ noncomputable def isoIsPullback (h : IsPullback fst snd f g) (h' : IsPullback fs @[reassoc (attr := simp)] theorem isoIsPullback_hom_fst (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) : - (h.isoIsPullback h').hom ≫ fst' = fst := + (h.isoIsPullback _ _ h').hom ≫ fst' = fst := IsLimit.conePointUniqueUpToIso_hom_comp h.isLimit h'.isLimit WalkingCospan.left @[reassoc (attr := simp)] theorem isoIsPullback_hom_snd (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) : - (h.isoIsPullback h').hom ≫ snd' = snd := + (h.isoIsPullback _ _ h').hom ≫ snd' = snd := IsLimit.conePointUniqueUpToIso_hom_comp h.isLimit h'.isLimit WalkingCospan.right @[reassoc (attr := simp)] theorem isoIsPullback_inv_fst (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) : - (h.isoIsPullback h').inv ≫ fst = fst' := by + (h.isoIsPullback _ _ h').inv ≫ fst = fst' := by simp only [Iso.inv_comp_eq, isoIsPullback_hom_fst] @[reassoc (attr := simp)] theorem isoIsPullback_inv_snd (h : IsPullback fst snd f g) (h' : IsPullback fst' snd' f g) : - (h.isoIsPullback h').inv ≫ snd = snd' := by + (h.isoIsPullback _ _ h').inv ≫ snd = snd' := by simp only [Iso.inv_comp_eq, isoIsPullback_hom_snd] end @@ -468,22 +468,22 @@ noncomputable def isoIsPushout (h : IsPushout f g inl inr) (h' : IsPushout f g i @[reassoc (attr := simp)] theorem inl_isoIsPushout_hom (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') : - inl ≫ (h.isoIsPushout h').hom = inl' := + inl ≫ (h.isoIsPushout _ _ h').hom = inl' := IsColimit.comp_coconePointUniqueUpToIso_hom h.isColimit h'.isColimit WalkingSpan.left @[reassoc (attr := simp)] theorem inr_isoIsPushout_hom (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') : - inr ≫ (h.isoIsPushout h').hom = inr' := + inr ≫ (h.isoIsPushout _ _ h').hom = inr' := IsColimit.comp_coconePointUniqueUpToIso_hom h.isColimit h'.isColimit WalkingSpan.right @[reassoc (attr := simp)] theorem inl_isoIsPushout_inv (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') : - inl' ≫ (h.isoIsPushout h').inv = inl := by + inl' ≫ (h.isoIsPushout _ _ h').inv = inl := by simp only [Iso.comp_inv_eq, inl_isoIsPushout_hom] @[reassoc (attr := simp)] theorem inr_isoIsPushout_inv (h : IsPushout f g inl inr) (h' : IsPushout f g inl' inr') : - inr' ≫ (h.isoIsPushout h').inv = inr := by + inr' ≫ (h.isoIsPushout _ _ h').inv = inr := by simp only [Iso.comp_inv_eq, inr_isoIsPushout_hom] end diff --git a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean index e9d8b8fb9c0ff..0a3a382da8016 100644 --- a/Mathlib/CategoryTheory/MorphismProperty/Basic.lean +++ b/Mathlib/CategoryTheory/MorphismProperty/Basic.lean @@ -162,13 +162,13 @@ lemma RespectsIso.postcomp (P : MorphismProperty C) [P.RespectsIso] {X Y Z : C} [IsIso e] (f : X ⟶ Y) (hf : P f) : P (f ≫ e) := RespectsRight.postcomp (Q := isomorphisms C) e ‹IsIso e› f hf -instance RespectsIso.op (P : MorphismProperty C) [h : RespectsIso P] : RespectsIso P.op where - precomp e (_ : IsIso e) f hf := h.postcomp e.unop f.unop hf - postcomp e (_ : IsIso e) f hf := h.precomp e.unop f.unop hf +instance RespectsIso.op (P : MorphismProperty C) [RespectsIso P] : RespectsIso P.op where + precomp e (_ : IsIso e) f hf := postcomp P e.unop f.unop hf + postcomp e (_ : IsIso e) f hf := precomp P e.unop f.unop hf -instance RespectsIso.unop (P : MorphismProperty Cᵒᵖ) [h : RespectsIso P] : RespectsIso P.unop where - precomp e (_ : IsIso e) f hf := h.postcomp e.op f.op hf - postcomp e (_ : IsIso e) f hf := h.precomp e.op f.op hf +instance RespectsIso.unop (P : MorphismProperty Cᵒᵖ) [RespectsIso P] : RespectsIso P.unop where + precomp e (_ : IsIso e) f hf := postcomp P e.op f.op hf + postcomp e (_ : IsIso e) f hf := precomp P e.op f.op hf /-- The closure by isomorphisms of a `MorphismProperty` -/ def isoClosure (P : MorphismProperty C) : MorphismProperty C := @@ -190,11 +190,11 @@ lemma monotone_isoClosure : Monotone (isoClosure (C := C)) := by theorem cancel_left_of_respectsIso (P : MorphismProperty C) [hP : RespectsIso P] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] : P (f ≫ g) ↔ P g := - ⟨fun h => by simpa using hP.precomp (inv f) (f ≫ g) h, hP.precomp f g⟩ + ⟨fun h => by simpa using RespectsIso.precomp P (inv f) (f ≫ g) h, RespectsIso.precomp P f g⟩ theorem cancel_right_of_respectsIso (P : MorphismProperty C) [hP : RespectsIso P] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso g] : P (f ≫ g) ↔ P f := - ⟨fun h => by simpa using hP.postcomp (inv g) (f ≫ g) h, hP.postcomp g f⟩ + ⟨fun h => by simpa using RespectsIso.postcomp P (inv g) (f ≫ g) h, RespectsIso.postcomp P g f⟩ theorem arrow_iso_iff (P : MorphismProperty C) [RespectsIso P] {f g : Arrow C} (e : f ≅ g) : P f.hom ↔ P g.hom := by diff --git a/Mathlib/CategoryTheory/Triangulated/Functor.lean b/Mathlib/CategoryTheory/Triangulated/Functor.lean index d78ec3c589a8f..9507a7937e954 100644 --- a/Mathlib/CategoryTheory/Triangulated/Functor.lean +++ b/Mathlib/CategoryTheory/Triangulated/Functor.lean @@ -310,6 +310,6 @@ lemma isTriangulated_of_essSurj_mapComposableArrows_two exact ⟨Octahedron.ofIso (e₁ := (e.app 0).symm) (e₂ := (e.app 1).symm) (e₃ := (e.app 2).symm) (comm₁₂ := ComposableArrows.naturality' e.inv 0 1) (comm₂₃ := ComposableArrows.naturality' e.inv 1 2) - (H := (someOctahedron rfl h₁₂' h₂₃' h₁₃').map F) _ _ _ _ _⟩ + (H := (someOctahedron rfl h₁₂' h₂₃' h₁₃').map F) ..⟩ end CategoryTheory diff --git a/Mathlib/Combinatorics/SimpleGraph/Path.lean b/Mathlib/Combinatorics/SimpleGraph/Path.lean index 9a5f20e639064..f40c73152000a 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Path.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Path.lean @@ -590,7 +590,7 @@ end Path namespace Walk variable {G} {p} {u v : V} {H : SimpleGraph V} -variable (p : G.Walk u v) +variable {p : G.Walk u v} protected theorem IsPath.transfer (hp) (pp : p.IsPath) : (p.transfer H hp).IsPath := by diff --git a/Mathlib/Data/Array/ExtractLemmas.lean b/Mathlib/Data/Array/ExtractLemmas.lean index bc66fc0660fbc..b27b5245af41d 100644 --- a/Mathlib/Data/Array/ExtractLemmas.lean +++ b/Mathlib/Data/Array/ExtractLemmas.lean @@ -27,7 +27,7 @@ theorem extract_append_left {a b : Array α} {i j : Nat} (h : j ≤ a.size) : · simp only [size_extract, size_append] omega · intro h1 h2 h3 - rw [get_extract, get_append_left, get_extract] + rw [getElem_extract, getElem_append_left, getElem_extract] theorem extract_append_right {a b : Array α} {i j : Nat} (h : a.size ≤ i) : (a ++ b).extract i j = b.extract (i - a.size) (j - a.size) := by @@ -35,8 +35,8 @@ theorem extract_append_right {a b : Array α} {i j : Nat} (h : a.size ≤ i) : · rw [size_extract, size_extract, size_append] omega · intro k hi h2 - rw [get_extract, get_extract, - get_append_right (show size a ≤ i + k by omega)] + rw [getElem_extract, getElem_extract, + getElem_append_right (show size a ≤ i + k by omega)] congr omega @@ -50,6 +50,6 @@ theorem extract_extract {s1 e2 e1 s2 : Nat} {a : Array α} (h : s1 + e2 ≤ e1) · simp only [size_extract] omega · intro i h1 h2 - simp only [get_extract, Nat.add_assoc] + simp only [getElem_extract, Nat.add_assoc] end Array diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean index 13f3ef89c67d3..87990322c4065 100644 --- a/Mathlib/Data/List/Basic.lean +++ b/Mathlib/Data/List/Basic.lean @@ -1331,25 +1331,12 @@ local notation a " ⋆ " b => op a b /-- Notation for `foldl op a l`. -/ local notation l " <*> " a => foldl op a l -theorem foldl_assoc : ∀ {l : List α} {a₁ a₂}, (l <*> a₁ ⋆ a₂) = a₁ ⋆ l <*> a₂ - | [], a₁, a₂ => rfl - | a :: l, a₁, a₂ => - calc - ((a :: l) <*> a₁ ⋆ a₂) = l <*> a₁ ⋆ a₂ ⋆ a := by simp only [foldl_cons, ha.assoc] - _ = a₁ ⋆ (a :: l) <*> a₂ := by rw [foldl_assoc, foldl_cons] - theorem foldl_op_eq_op_foldr_assoc : ∀ {l : List α} {a₁ a₂}, ((l <*> a₁) ⋆ a₂) = a₁ ⋆ l.foldr (· ⋆ ·) a₂ | [], a₁, a₂ => rfl | a :: l, a₁, a₂ => by simp only [foldl_cons, foldr_cons, foldl_assoc, ha.assoc]; rw [foldl_op_eq_op_foldr_assoc] -theorem foldr_assoc : ∀ {l : List α} {a₁ a₂}, l.foldr op (op a₁ a₂) = op (l.foldr op a₁) a₂ - | [], a₁, a₂ => rfl - | a :: l, a₁, a₂ => by - simp only [foldr_cons, ha.assoc] - rw [foldr_assoc] - variable [hc : Std.Commutative op] theorem foldl_assoc_comm_cons {l : List α} {a₁ a₂} : ((a₁ :: l) <*> a₂) = a₁ ⋆ l <*> a₂ := by diff --git a/Mathlib/Data/List/Cycle.lean b/Mathlib/Data/List/Cycle.lean index 5f038e2ae1e94..9c8cbaa143209 100644 --- a/Mathlib/Data/List/Cycle.lean +++ b/Mathlib/Data/List/Cycle.lean @@ -334,7 +334,7 @@ theorem prev_next (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) : obtain ⟨⟨n, hn⟩, rfl⟩ := get_of_mem hx simp only [next_get, prev_get, h, Nat.mod_add_mod] cases' l with hd tl - · simp at hx + · simp at hn · have : (n + 1 + length tl) % (length tl + 1) = n := by rw [length_cons] at hn rw [add_assoc, add_comm 1, Nat.add_mod_right, Nat.mod_eq_of_lt hn] @@ -345,7 +345,7 @@ theorem next_prev (l : List α) (h : Nodup l) (x : α) (hx : x ∈ l) : obtain ⟨⟨n, hn⟩, rfl⟩ := get_of_mem hx simp only [next_get, prev_get, h, Nat.mod_add_mod] cases' l with hd tl - · simp at hx + · simp at hn · have : (n + length tl + 1) % (length tl + 1) = n := by rw [length_cons] at hn rw [add_assoc, Nat.add_mod_right, Nat.mod_eq_of_lt hn] diff --git a/Mathlib/Data/List/Indexes.lean b/Mathlib/Data/List/Indexes.lean index 48d9dfcdd8b78..7e53018e89d4b 100644 --- a/Mathlib/Data/List/Indexes.lean +++ b/Mathlib/Data/List/Indexes.lean @@ -119,7 +119,7 @@ theorem getElem?_mapIdx_go (f : ℕ → α → β) : ∀ (l : List α) (arr : Ar (mapIdx.go f l arr)[i]? = if h : i < arr.size then some arr[i] else Option.map (f i) l[i - arr.size]? | [], arr, i => by - simp only [mapIdx.go, Array.toListImpl_eq, getElem?_eq, Array.toList_length, + simp only [mapIdx.go, Array.toListImpl_eq, getElem?_eq, Array.length_toList, Array.getElem_eq_getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none'] | a :: l, arr, i => by rw [mapIdx.go, getElem?_mapIdx_go] diff --git a/Mathlib/Data/List/Lemmas.lean b/Mathlib/Data/List/Lemmas.lean index b10612e1fefde..b055f1b187222 100644 --- a/Mathlib/Data/List/Lemmas.lean +++ b/Mathlib/Data/List/Lemmas.lean @@ -30,6 +30,8 @@ theorem tail_reverse_eq_reverse_dropLast (l : List α) : · rw [getElem?_eq_none, getElem?_eq_none] all_goals (simp; omega) +@[deprecated (since := "2024-08-19")] alias nthLe_tail := getElem_tail + theorem injOn_insertNth_index_of_not_mem (l : List α) (x : α) (hx : x ∉ l) : Set.InjOn (fun k => insertNth k x l) { n | n ≤ l.length } := by induction' l with hd tl IH diff --git a/Mathlib/Data/List/MinMax.lean b/Mathlib/Data/List/MinMax.lean index c20935506c371..52a8f59fb7167 100644 --- a/Mathlib/Data/List/MinMax.lean +++ b/Mathlib/Data/List/MinMax.lean @@ -433,25 +433,31 @@ theorem minimum_of_length_pos_le_getElem {i : ℕ} (w : i < l.length) (h := (Nat l.minimum_of_length_pos h ≤ l[i] := getElem_le_maximum_of_length_pos (α := αᵒᵈ) w -lemma getD_maximum?_eq_unbot'_maximum (l : List α) (d : α) : - l.maximum?.getD d = l.maximum.unbot' d := by +lemma getD_max?_eq_unbot'_maximum (l : List α) (d : α) : + l.max?.getD d = l.maximum.unbot' d := by cases hy : l.maximum with | bot => simp [List.maximum_eq_bot.mp hy] | coe y => rw [List.maximum_eq_coe_iff] at hy simp only [WithBot.unbot'_coe] - cases hz : l.maximum? with - | none => simp [List.maximum?_eq_none_iff.mp hz] at hy + cases hz : l.max? with + | none => simp [List.max?_eq_none_iff.mp hz] at hy | some z => have : Antisymm (α := α) (· ≤ ·) := ⟨_root_.le_antisymm⟩ - rw [List.maximum?_eq_some_iff] at hz + rw [List.max?_eq_some_iff] at hz · rw [Option.getD_some] exact _root_.le_antisymm (hy.right _ hz.left) (hz.right _ hy.left) all_goals simp [le_total] -lemma getD_minimum?_eq_untop'_minimum (l : List α) (d : α) : - l.minimum?.getD d = l.minimum.untop' d := - getD_maximum?_eq_unbot'_maximum (α := αᵒᵈ) _ _ +@[deprecated (since := "2024-09-29")] +alias getD_maximum?_eq_unbot'_maximum := getD_max?_eq_unbot'_maximum + +lemma getD_min?_eq_untop'_minimum (l : List α) (d : α) : + l.min?.getD d = l.minimum.untop' d := + getD_max?_eq_unbot'_maximum (α := αᵒᵈ) _ _ + +@[deprecated (since := "2024-09-29")] +alias getD_minimum?_eq_untop'_minimum := getD_min?_eq_untop'_minimum end LinearOrder diff --git a/Mathlib/Data/List/Perm.lean b/Mathlib/Data/List/Perm.lean index e680168c0687b..96d90a6a53cdb 100644 --- a/Mathlib/Data/List/Perm.lean +++ b/Mathlib/Data/List/Perm.lean @@ -51,25 +51,6 @@ theorem Perm.subset_congr_left {l₁ l₂ l₃ : List α} (h : l₁ ~ l₂) : l theorem Perm.subset_congr_right {l₁ l₂ l₃ : List α} (h : l₁ ~ l₂) : l₃ ⊆ l₁ ↔ l₃ ⊆ l₂ := ⟨fun h' => h'.trans h.subset, fun h' => h'.trans h.symm.subset⟩ -/-- Variant of `Perm.foldr_eq` with explicit commutativity argument. -/ -theorem Perm.foldr_eq' {f : α → β → β} {l₁ l₂ : List α} (p : l₁ ~ l₂) - (comm : ∀ x ∈ l₁, ∀ y ∈ l₁, ∀ z, f y (f x z) = f x (f y z)) - (init : β) : foldr f init l₁ = foldr f init l₂ := by - induction p using recOnSwap' generalizing init with - | nil => simp - | cons x _p IH => - simp only [foldr] - congr 1 - apply IH; intros; apply comm <;> exact .tail _ ‹_› - | swap' x y _p IH => - simp only [foldr] - rw [comm x (.tail _ <| .head _) y (.head _)] - congr 2 - apply IH; intros; apply comm <;> exact .tail _ (.tail _ ‹_›) - | trans p₁ _p₂ IH₁ IH₂ => - refine (IH₁ comm init).trans (IH₂ ?_ _) - intros; apply comm <;> apply p₁.symm.subset <;> assumption - section Rel open Relator @@ -200,7 +181,8 @@ theorem perm_option_to_list {o₁ o₂ : Option α} : o₁.toList ~ o₂.toList cases' o₁ with a <;> cases' o₂ with b; · rfl · cases p.length_eq · cases p.length_eq - · exact Option.mem_toList.1 (p.symm.subset <| by simp) + · #adaptation_note /-- Fixing explicitness of Option.mem_toList in nightly-2024-10-01. -/ + exact (Option.mem_toList _ _).1 (p.symm.subset <| by simp) alias ⟨subperm.of_cons, subperm.cons⟩ := subperm_cons diff --git a/Mathlib/Data/Nat/Defs.lean b/Mathlib/Data/Nat/Defs.lean index 3bef76181d8dc..c434db7783277 100644 --- a/Mathlib/Data/Nat/Defs.lean +++ b/Mathlib/Data/Nat/Defs.lean @@ -137,8 +137,6 @@ lemma one_lt_iff_ne_zero_and_ne_one : ∀ {n : ℕ}, 1 < n ↔ n ≠ 0 ∧ n ≠ lemma le_one_iff_eq_zero_or_eq_one : ∀ {n : ℕ}, n ≤ 1 ↔ n = 0 ∨ n = 1 := by simp [le_succ_iff] -@[simp] lemma lt_one_iff : n < 1 ↔ n = 0 := Nat.lt_succ_iff.trans <| by rw [le_zero_eq] - lemma one_le_of_lt (h : a < b) : 1 ≤ b := Nat.lt_of_le_of_lt (Nat.zero_le _) h @[simp] lemma min_eq_zero_iff : min m n = 0 ↔ m = 0 ∨ n = 0 := by omega @@ -827,7 +825,7 @@ This is an alias of `Nat.leRec`, specialized to `Prop`. -/ @[elab_as_elim] lemma le_induction {m : ℕ} {P : ∀ n, m ≤ n → Prop} (base : P m m.le_refl) (succ : ∀ n hmn, P n hmn → P (n + 1) (le_succ_of_le hmn)) : ∀ n hmn, P n hmn := - @Nat.leRec (motive := P) base succ + @Nat.leRec (motive := P) _ base succ /-- Induction principle deriving the next case from the two previous ones. -/ def twoStepInduction {P : ℕ → Sort*} (zero : P 0) (one : P 1) @@ -1011,9 +1009,6 @@ lemma div_ne_zero_iff_of_dvd (hba : b ∣ a) : a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ @[simp] lemma mul_mod_mod (a b c : ℕ) : (a * (b % c)) % c = a * b % c := by rw [mul_mod, mod_mod, ← mul_mod] -@[simp] lemma mod_mul_mod (a b c : ℕ) : (a % c * b) % c = a * b % c := by - rw [mul_mod, mod_mod, ← mul_mod] - lemma pow_mod (a b n : ℕ) : a ^ b % n = (a % n) ^ b % n := by induction b with | zero => rfl diff --git a/Mathlib/Data/Option/Defs.lean b/Mathlib/Data/Option/Defs.lean index e140c43e996c9..c15bedf853135 100644 --- a/Mathlib/Data/Option/Defs.lean +++ b/Mathlib/Data/Option/Defs.lean @@ -75,10 +75,6 @@ abbrev iget [Inhabited α] : Option α → α theorem iget_some [Inhabited α] {a : α} : (some a).iget = a := rfl -@[simp] -theorem mem_toList {a : α} {o : Option α} : a ∈ toList o ↔ a ∈ o := by - cases o <;> simp [toList, eq_comm] - instance liftOrGet_isCommutative (f : α → α → α) [Std.Commutative f] : Std.Commutative (liftOrGet f) := ⟨fun a b ↦ by cases a <;> cases b <;> simp [liftOrGet, Std.Commutative.comm]⟩ diff --git a/Mathlib/Data/Ordmap/Ordset.lean b/Mathlib/Data/Ordmap/Ordset.lean index 20e17e175fa23..06b25c58fc953 100644 --- a/Mathlib/Data/Ordmap/Ordset.lean +++ b/Mathlib/Data/Ordmap/Ordset.lean @@ -1258,7 +1258,7 @@ theorem Valid'.glue_aux {l r o₁ o₂} (hl : Valid' o₁ l o₂) (hr : Valid' o suffices H : _ by refine ⟨Valid'.balanceL (hl.of_lt ?_ ?_) v H, ?_⟩ · refine @findMin'_all (P := fun a : α => Bounded nil o₁ (a : WithBot α)) - rl rx (sep.2.1.1.imp ?_) hr.1.1.to_nil + _ rl rx (sep.2.1.1.imp ?_) hr.1.1.to_nil exact fun y h => hl.1.1.to_nil.mono_right (le_of_lt h) · exact @findMin'_all _ (fun a => All (· < a) (.node ls ll lx lr)) rl rx diff --git a/Mathlib/Data/Setoid/Basic.lean b/Mathlib/Data/Setoid/Basic.lean index ca1d0ac665068..4f812be71f3cd 100644 --- a/Mathlib/Data/Setoid/Basic.lean +++ b/Mathlib/Data/Setoid/Basic.lean @@ -420,7 +420,7 @@ def sigmaQuotientEquivOfLe {r s : Setoid α} (hle : r ≤ s) : (Σ q : Quotient s, Quotient (r.comap (Subtype.val : Quotient.mk s ⁻¹' {q} → α))) ≃ Quotient r := .trans (.symm <| .sigmaCongrRight fun _ ↦ .subtypeQuotientEquivQuotientSubtype - (s₁ := r) (s₂ := r.comap Subtype.val) _ (fun _ ↦ Iff.rfl) fun _ _ ↦ Iff.rfl) + (s₁ := r) (s₂ := r.comap Subtype.val) _ _ (fun _ ↦ Iff.rfl) fun _ _ ↦ Iff.rfl) (.sigmaFiberEquiv fun a ↦ a.lift (Quotient.mk s) fun _ _ h ↦ Quotient.sound <| hle h) end Setoid diff --git a/Mathlib/Data/ZMod/Defs.lean b/Mathlib/Data/ZMod/Defs.lean index 324dec3252219..3999e96138180 100644 --- a/Mathlib/Data/ZMod/Defs.lean +++ b/Mathlib/Data/ZMod/Defs.lean @@ -103,7 +103,7 @@ namespace ZMod instance instUnique : Unique (ZMod 1) := Fin.uniqueFinOne instance fintype : ∀ (n : ℕ) [NeZero n], Fintype (ZMod n) - | 0, h => (h.ne rfl).elim + | 0, h => (h.ne _ rfl).elim | n + 1, _ => Fin.fintype (n + 1) instance infinite : Infinite (ZMod 0) := diff --git a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean index 21d9418e249a5..787429c5e3827 100644 --- a/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean +++ b/Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean @@ -79,7 +79,7 @@ theorem spanEval_ne_top : spanEval k ≠ ⊤ := by rw [map_one, Finsupp.linearCombination_apply, Finsupp.sum, map_sum, Finset.sum_eq_zero] at hv · exact zero_ne_one hv intro j hj - rw [smul_eq_mul, map_mul, toSplittingField_evalXSelf (s := v.support) hj, + rw [smul_eq_mul, map_mul, toSplittingField_evalXSelf _ (s := v.support) hj, mul_zero] /-- A random maximal ideal that contains `spanEval k` -/ diff --git a/Mathlib/FieldTheory/PurelyInseparable.lean b/Mathlib/FieldTheory/PurelyInseparable.lean index f8b347c9bf68a..8c9b58230a71e 100644 --- a/Mathlib/FieldTheory/PurelyInseparable.lean +++ b/Mathlib/FieldTheory/PurelyInseparable.lean @@ -166,7 +166,7 @@ variable {F K} theorem isPurelyInseparable_iff : IsPurelyInseparable F E ↔ ∀ x : E, IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range) := - ⟨fun h x ↦ ⟨h.isIntegral' x, h.inseparable' x⟩, fun h ↦ ⟨⟨fun x ↦ (h x).1⟩, fun x ↦ (h x).2⟩⟩ + ⟨fun h x ↦ ⟨h.isIntegral' _ x, h.inseparable' x⟩, fun h ↦ ⟨⟨fun x ↦ (h x).1⟩, fun x ↦ (h x).2⟩⟩ /-- Transfer `IsPurelyInseparable` across an `AlgEquiv`. -/ theorem AlgEquiv.isPurelyInseparable (e : K ≃ₐ[F] E) [IsPurelyInseparable F K] : diff --git a/Mathlib/FieldTheory/Separable.lean b/Mathlib/FieldTheory/Separable.lean index c6a87d0dbf1fb..fd852c7cdf7d7 100644 --- a/Mathlib/FieldTheory/Separable.lean +++ b/Mathlib/FieldTheory/Separable.lean @@ -652,7 +652,7 @@ theorem IsSeparable.tower_bot {x : K} (h : IsSeparable F (algebraMap K E x)) : I variable (K E) in theorem Algebra.isSeparable_tower_bot_of_isSeparable [h : Algebra.IsSeparable F E] : Algebra.IsSeparable F K := - ⟨fun _ ↦ IsSeparable.tower_bot (h.isSeparable _)⟩ + ⟨fun _ ↦ IsSeparable.tower_bot (h.isSeparable _ _)⟩ end IsScalarTower diff --git a/Mathlib/FieldTheory/SeparableDegree.lean b/Mathlib/FieldTheory/SeparableDegree.lean index 3bac952cdb9f8..a1c65838ff7d2 100644 --- a/Mathlib/FieldTheory/SeparableDegree.lean +++ b/Mathlib/FieldTheory/SeparableDegree.lean @@ -208,7 +208,7 @@ def embEquivOfAdjoinSplits {S : Set E} (hS : adjoin F S = ⊤) (hS ▸ isAlgebraic_adjoin (S := S) fun x hx ↦ (hK x hx).1) have halg := (topEquiv (F := F) (E := E)).isAlgebraic Classical.choice <| Function.Embedding.antisymm - (halg.algHomEmbeddingOfSplits (fun _ ↦ splits_of_mem_adjoin F (S := S) hK (hS ▸ mem_top)) _) + (halg.algHomEmbeddingOfSplits (fun _ ↦ splits_of_mem_adjoin F E (S := S) hK (hS ▸ mem_top)) _) (halg.algHomEmbeddingOfSplits (fun _ ↦ IsAlgClosed.splits_codomain _) _) /-- The `Field.finSepDegree F E` is equal to the cardinality of `E →ₐ[F] K` diff --git a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean index 5c5349f4adc95..a966c23b3b918 100644 --- a/Mathlib/Geometry/RingedSpace/OpenImmersion.lean +++ b/Mathlib/Geometry/RingedSpace/OpenImmersion.lean @@ -167,7 +167,7 @@ noncomputable def invApp (U : Opens X) : @[simp, reassoc] theorem inv_naturality {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) : - X.presheaf.map i ≫ H.invApp (unop V) = + X.presheaf.map i ≫ H.invApp _ (unop V) = invApp f (unop U) ≫ Y.presheaf.map (opensFunctor f |>.op.map i) := by simp only [invApp, ← Category.assoc] rw [IsIso.comp_inv_eq] @@ -179,11 +179,11 @@ theorem inv_naturality {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) : instance (U : Opens X) : IsIso (invApp f U) := by delta invApp; infer_instance theorem inv_invApp (U : Opens X) : - inv (H.invApp U) = + inv (H.invApp _ U) = f.c.app (op (opensFunctor f |>.obj U)) ≫ X.presheaf.map (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.inj])) := by - rw [← cancel_epi (H.invApp U), IsIso.hom_inv_id] + rw [← cancel_epi (H.invApp _ U), IsIso.hom_inv_id] delta invApp simp [← Functor.map_comp] @@ -195,7 +195,7 @@ theorem invApp_app (U : Opens X) : @[simp, reassoc] theorem app_invApp (U : Opens Y) : - f.c.app (op U) ≫ H.invApp ((Opens.map f.base).obj U) = + f.c.app (op U) ≫ H.invApp _ ((Opens.map f.base).obj U) = Y.presheaf.map ((homOfLE (Set.image_preimage_subset f.base U.1)).op : op U ⟶ op (opensFunctor f |>.obj ((Opens.map f.base).obj U))) := by @@ -244,7 +244,7 @@ instance ofRestrict {X : TopCat} (Y : PresheafedSpace C) {f : X ⟶ Y.carrier} @[elementwise, simp] theorem ofRestrict_invApp {C : Type*} [Category C] (X : PresheafedSpace C) {Y : TopCat} {f : Y ⟶ TopCat.of X.carrier} (h : OpenEmbedding f) (U : Opens (X.restrict h).carrier) : - (PresheafedSpace.IsOpenImmersion.ofRestrict X h).invApp U = 𝟙 _ := by + (PresheafedSpace.IsOpenImmersion.ofRestrict X h).invApp _ U = 𝟙 _ := by delta invApp rw [IsIso.comp_inv_eq, Category.id_comp] change X.presheaf.map _ = X.presheaf.map _ @@ -290,7 +290,7 @@ def pullbackConeOfLeftFst : base := pullback.fst _ _ c := { app := fun U => - hf.invApp (unop U) ≫ + hf.invApp _ (unop U) ≫ g.c.app (op (hf.base_open.isOpenMap.functor.obj (unop U))) ≫ Y.presheaf.map (eqToHom @@ -772,21 +772,21 @@ noncomputable def invApp (U : Opens X) : @[reassoc (attr := simp)] theorem inv_naturality {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) : - X.presheaf.map i ≫ H.invApp (unop V) = - H.invApp (unop U) ≫ Y.presheaf.map (opensFunctor f |>.op.map i) := + X.presheaf.map i ≫ H.invApp _ (unop V) = + H.invApp _ (unop U) ≫ Y.presheaf.map (opensFunctor f |>.op.map i) := PresheafedSpace.IsOpenImmersion.inv_naturality f i -instance (U : Opens X) : IsIso (H.invApp U) := by delta invApp; infer_instance +instance (U : Opens X) : IsIso (H.invApp _ U) := by delta invApp; infer_instance theorem inv_invApp (U : Opens X) : - inv (H.invApp U) = + inv (H.invApp _ U) = f.c.app (op (opensFunctor f |>.obj U)) ≫ X.presheaf.map (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.inj])) := PresheafedSpace.IsOpenImmersion.inv_invApp f U @[reassoc (attr := simp)] theorem invApp_app (U : Opens X) : - H.invApp U ≫ f.c.app (op (opensFunctor f |>.obj U)) = + H.invApp _ U ≫ f.c.app (op (opensFunctor f |>.obj U)) = X.presheaf.map (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.inj])) := PresheafedSpace.IsOpenImmersion.invApp_app f U @@ -794,7 +794,7 @@ attribute [elementwise] invApp_app @[reassoc (attr := simp)] theorem app_invApp (U : Opens Y) : - f.c.app (op U) ≫ H.invApp ((Opens.map f.base).obj U) = + f.c.app (op U) ≫ H.invApp _ ((Opens.map f.base).obj U) = Y.presheaf.map ((homOfLE (Set.image_preimage_subset f.base U.1)).op : op U ⟶ op (opensFunctor f |>.obj ((Opens.map f.base).obj U))) := @@ -818,7 +818,7 @@ instance ofRestrict {X : TopCat} (Y : SheafedSpace C) {f : X ⟶ Y.carrier} @[elementwise, simp] theorem ofRestrict_invApp {C : Type*} [Category C] (X : SheafedSpace C) {Y : TopCat} {f : Y ⟶ TopCat.of X.carrier} (h : OpenEmbedding f) (U : Opens (X.restrict h).carrier) : - (SheafedSpace.IsOpenImmersion.ofRestrict X h).invApp U = 𝟙 _ := + (SheafedSpace.IsOpenImmersion.ofRestrict X h).invApp _ U = 𝟙 _ := PresheafedSpace.IsOpenImmersion.ofRestrict_invApp _ h U /-- An open immersion is an iso if the underlying continuous map is epi. -/ @@ -1154,7 +1154,7 @@ is an open immersion iff every stalk map is an iso. theorem of_stalk_iso {X Y : LocallyRingedSpace} (f : X ⟶ Y) (hf : OpenEmbedding f.1.base) [stalk_iso : ∀ x : X.1, IsIso (f.stalkMap x)] : LocallyRingedSpace.IsOpenImmersion f := - SheafedSpace.IsOpenImmersion.of_stalk_iso hf (H := stalk_iso) + SheafedSpace.IsOpenImmersion.of_stalk_iso _ hf (H := stalk_iso) end OfStalkIso @@ -1180,21 +1180,21 @@ noncomputable def invApp (U : Opens X) : @[reassoc (attr := simp)] theorem inv_naturality {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) : - X.presheaf.map i ≫ H.invApp (unop V) = - H.invApp (unop U) ≫ Y.presheaf.map (opensFunctor f |>.op.map i) := + X.presheaf.map i ≫ H.invApp _ (unop V) = + H.invApp _ (unop U) ≫ Y.presheaf.map (opensFunctor f |>.op.map i) := PresheafedSpace.IsOpenImmersion.inv_naturality f.1 i -instance (U : Opens X) : IsIso (H.invApp U) := by delta invApp; infer_instance +instance (U : Opens X) : IsIso (H.invApp _ U) := by delta invApp; infer_instance theorem inv_invApp (U : Opens X) : - inv (H.invApp U) = + inv (H.invApp _ U) = f.1.c.app (op (opensFunctor f |>.obj U)) ≫ X.presheaf.map (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.inj])) := PresheafedSpace.IsOpenImmersion.inv_invApp f.1 U @[reassoc (attr := simp)] theorem invApp_app (U : Opens X) : - H.invApp U ≫ f.1.c.app (op (opensFunctor f |>.obj U)) = + H.invApp _ U ≫ f.1.c.app (op (opensFunctor f |>.obj U)) = X.presheaf.map (eqToHom (by simp [Opens.map, Set.preimage_image_eq _ H.base_open.inj])) := PresheafedSpace.IsOpenImmersion.invApp_app f.1 U @@ -1202,7 +1202,7 @@ attribute [elementwise] invApp_app @[reassoc (attr := simp)] theorem app_invApp (U : Opens Y) : - f.1.c.app (op U) ≫ H.invApp ((Opens.map f.1.base).obj U) = + f.1.c.app (op U) ≫ H.invApp _ ((Opens.map f.1.base).obj U) = Y.presheaf.map ((homOfLE (Set.image_preimage_subset f.1.base U.1)).op : op U ⟶ op (opensFunctor f |>.obj ((Opens.map f.1.base).obj U))) := @@ -1211,7 +1211,7 @@ theorem app_invApp (U : Opens Y) : /-- A variant of `app_inv_app` that gives an `eqToHom` instead of `homOfLe`. -/ @[reassoc] theorem app_inv_app' (U : Opens Y) (hU : (U : Set Y) ⊆ Set.range f.1.base) : - f.1.c.app (op U) ≫ H.invApp ((Opens.map f.1.base).obj U) = + f.1.c.app (op U) ≫ H.invApp _ ((Opens.map f.1.base).obj U) = Y.presheaf.map (eqToHom <| le_antisymm (Set.image_preimage_subset f.1.base U.1) <| @@ -1226,7 +1226,7 @@ instance ofRestrict {X : TopCat} (Y : LocallyRingedSpace) {f : X ⟶ Y.carrier} @[elementwise, simp] theorem ofRestrict_invApp (X : LocallyRingedSpace) {Y : TopCat} {f : Y ⟶ TopCat.of X.carrier} (h : OpenEmbedding f) (U : Opens (X.restrict h).carrier) : - (LocallyRingedSpace.IsOpenImmersion.ofRestrict X h).invApp U = 𝟙 _ := + (LocallyRingedSpace.IsOpenImmersion.ofRestrict X h).invApp _ U = 𝟙 _ := PresheafedSpace.IsOpenImmersion.ofRestrict_invApp _ h U instance stalk_iso (x : X) : IsIso (f.stalkMap x) := diff --git a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean index b5ac976467db8..4d9076090a048 100644 --- a/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean +++ b/Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean @@ -149,7 +149,7 @@ theorem pullback_base (i j k : D.J) (S : Set (D.V (i, j)).carrier) : /-- The red and the blue arrows in ![this diagram](https://i.imgur.com/0GiBUh6.png) commute. -/ @[simp, reassoc] theorem f_invApp_f_app (i j k : D.J) (U : Opens (D.V (i, j)).carrier) : - (D.f_open i j).invApp U ≫ (D.f i k).c.app _ = + (D.f_open i j).invApp _ U ≫ (D.f i k).c.app _ = (π₁ i, j, k).c.app (op U) ≫ (π₂⁻¹ i, j, k) (unop _) ≫ (D.V _).presheaf.map @@ -161,7 +161,7 @@ theorem f_invApp_f_app (i j k : D.J) (U : Opens (D.V (i, j)).carrier) : apply pullback_base)) := by have := PresheafedSpace.congr_app (@pullback.condition _ _ _ _ _ (D.f i j) (D.f i k) _) dsimp only [comp_c_app] at this - rw [← cancel_epi (inv ((D.f_open i j).invApp U)), IsIso.inv_hom_id_assoc, + rw [← cancel_epi (inv ((D.f_open i j).invApp _ U)), IsIso.inv_hom_id_assoc, IsOpenImmersion.inv_invApp] simp_rw [Category.assoc] erw [(π₁ i, j, k).c.naturality_assoc, reassoc_of% this, ← Functor.map_comp_assoc, @@ -271,7 +271,7 @@ def opensImagePreimageMap (i j : D.J) (U : Opens (D.U i).carrier) : (Opens.map (𝖣.ι j).base).obj ((D.ι_openEmbedding i).isOpenMap.functor.obj U)) := (D.f i j).c.app (op U) ≫ (D.t j i).c.app _ ≫ - (D.f_open j i).invApp (unop _) ≫ + (D.f_open j i).invApp _ (unop _) ≫ (𝖣.U j).presheaf.map (eqToHom (D.ι_image_preimage_eq i j U)).op theorem opensImagePreimageMap_app' (i j k : D.J) (U : Opens (D.U i).carrier) : @@ -436,19 +436,9 @@ abbrev ιInvAppπEqMap {i : D.J} (U : Opens (D.U i).carrier) := theorem π_ιInvApp_π (i j : D.J) (U : Opens (D.U i).carrier) : D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j = D.diagramOverOpenπ U j := by - -- Porting note: originally, the proof of monotonicity was left a blank and proved in the end - -- but Lean 4 doesn't like this any more, so the proof is restructured - rw [← @cancel_mono (f := (componentwiseDiagram 𝖣.diagram.multispan _).map - (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫ 𝟙 _) _ _ (by - rw [Category.comp_id] - apply (config := { allowSynthFailures := true }) mono_comp - change Mono ((_ ≫ D.f j i).c.app _) - rw [comp_c_app] - apply (config := { allowSynthFailures := true }) mono_comp - · erw [D.ι_image_preimage_eq i j U] - infer_instance - · have : IsIso (D.t i j).c := by apply c_isIso_of_iso - infer_instance)] + rw [← @cancel_mono + (f := (componentwiseDiagram 𝖣.diagram.multispan _).map + (Quiver.Hom.op (WalkingMultispan.Hom.snd (i, j))) ≫ 𝟙 _) ..] simp_rw [Category.assoc] rw [limit.w_assoc] erw [limit.lift_π_assoc] @@ -466,6 +456,15 @@ theorem π_ιInvApp_π (i j : D.J) (U : Opens (D.U i).carrier) : convert limit.w (componentwiseDiagram 𝖣.diagram.multispan _) (Quiver.Hom.op (WalkingMultispan.Hom.fst (i, j))) + · rw [Category.comp_id] + apply (config := { allowSynthFailures := true }) mono_comp + change Mono ((_ ≫ D.f j i).c.app _) + rw [comp_c_app] + apply (config := { allowSynthFailures := true }) mono_comp + · erw [D.ι_image_preimage_eq i j U] + infer_instance + · have : IsIso (D.t i j).c := by apply c_isIso_of_iso + infer_instance /-- `ιInvApp` is the inverse of `D.ι i` on `U`. -/ theorem π_ιInvApp_eq_id (i : D.J) (U : Opens (D.U i).carrier) : diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean index 462873bca532e..3b1fa878251d9 100644 --- a/Mathlib/GroupTheory/OrderOfElement.lean +++ b/Mathlib/GroupTheory/OrderOfElement.lean @@ -717,7 +717,7 @@ automatic in the case of a finite cancellative monoid. -/ `addOrderOf_nsmul` but with one assumption less which is automatic in the case of a finite cancellative additive monoid."] theorem orderOf_pow (x : G) : orderOf (x ^ n) = orderOf x / gcd (orderOf x) n := - (isOfFinOrder_of_finite _).orderOf_pow _ + (isOfFinOrder_of_finite _).orderOf_pow .. @[to_additive] theorem mem_powers_iff_mem_range_orderOf [DecidableEq G] : diff --git a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean index 57afc2d245faf..c16d73ee548bd 100644 --- a/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean +++ b/Mathlib/GroupTheory/Perm/Cycle/Concrete.lean @@ -316,7 +316,7 @@ theorem toList_formPerm_nontrivial (l : List α) (hl : 2 ≤ l.length) (hn : Nod · refine ext_getElem (by simp) fun k hk hk' => ?_ simp only [get_eq_getElem, formPerm_pow_apply_getElem _ hn, zero_add, getElem_map, getElem_range, Nat.mod_eq_of_lt hk'] - · simpa [hs] using get_mem _ _ _ + · simp [hs] theorem toList_formPerm_isRotated_self (l : List α) (hl : 2 ≤ l.length) (hn : Nodup l) (x : α) (hx : x ∈ l) : toList (formPerm l) x ~r l := by diff --git a/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean b/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean index 7ae6931a6aa29..9f90f39e9ee1f 100644 --- a/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean +++ b/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean @@ -226,7 +226,7 @@ theorem MultilinearMap.domCoprod_alternization [DecidableEq ιa] [DecidableEq ι -- unfold the quotient mess left by `Finset.sum_partition` -- Porting note: Was `conv in .. => ..`. erw - [@Finset.filter_congr _ _ (fun a => @Quotient.decidableEq _ _ + [@Finset.filter_congr _ _ _ (fun a => @Quotient.decidableEq _ _ (QuotientGroup.leftRelDecidable (MonoidHom.range (Perm.sumCongrHom ιa ιb))) (Quotient.mk (QuotientGroup.leftRel (MonoidHom.range (Perm.sumCongrHom ιa ιb))) a) (Quotient.mk'' σ)) _ (s := Finset.univ) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean index 4359ba5b328d0..e5f6c2be85383 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean @@ -154,7 +154,7 @@ theorem evenOdd_induction (n : ZMod 2) {motive : ∀ x, x ∈ evenOdd Q n → Pr motive (ι Q m₁ * ι Q m₂ * x) (zero_add n ▸ SetLike.mul_mem_graded (ι_mul_ι_mem_evenOdd_zero Q m₁ m₂) hx)) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q n) : motive x hx := by - apply Submodule.iSup_induction' (C := motive) _ (range_ι_pow 0 (Submodule.zero_mem _)) add + apply Submodule.iSup_induction' (C := motive) _ _ (range_ι_pow 0 (Submodule.zero_mem _)) add refine Subtype.rec ?_ simp_rw [ZMod.natCast_eq_iff, add_comm n.val] rintro n' ⟨k, rfl⟩ xv @@ -197,7 +197,7 @@ theorem even_induction {motive : ∀ x, x ∈ evenOdd Q 0 → Prop} motive (ι Q m₁ * ι Q m₂ * x) (zero_add (0 : ZMod 2) ▸ SetLike.mul_mem_graded (ι_mul_ι_mem_evenOdd_zero Q m₁ m₂) hx)) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 0) : motive x hx := by - refine evenOdd_induction (motive := motive) (fun rx => ?_) add ι_mul_ι_mul x hx + refine evenOdd_induction _ _ (motive := motive) (fun rx => ?_) add ι_mul_ι_mul x hx rintro ⟨r, rfl⟩ exact algebraMap r @@ -213,7 +213,7 @@ theorem odd_induction {P : ∀ x, x ∈ evenOdd Q 1 → Prop} P (CliffordAlgebra.ι Q m₁ * CliffordAlgebra.ι Q m₂ * x) (zero_add (1 : ZMod 2) ▸ SetLike.mul_mem_graded (ι_mul_ι_mem_evenOdd_zero Q m₁ m₂) hx)) (x : CliffordAlgebra Q) (hx : x ∈ evenOdd Q 1) : P x hx := by - refine evenOdd_induction (motive := P) (fun ιv => ?_) add ι_mul_ι_mul x hx + refine evenOdd_induction _ _ (motive := P) (fun ιv => ?_) add ι_mul_ι_mul x hx -- Porting note: was `simp_rw [ZMod.val_one, pow_one]`, lean4#1926 intro h; rw [ZMod.val_one, pow_one] at h; revert h rintro ⟨v, rfl⟩ diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index b4d2e69e8d184..e3f4f179d9928 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -181,7 +181,7 @@ def LinearMap.dualMap (f : M₁ →ₗ[R] M₂) : Dual R M₂ →ₗ[R] Dual R M -- Porting note: with reducible def need to specify some parameters to transpose explicitly Module.Dual.transpose (R := R) f -lemma LinearMap.dualMap_eq_lcomp (f : M₁ →ₗ[R] M₂) : f.dualMap = f.lcomp R := rfl +lemma LinearMap.dualMap_eq_lcomp (f : M₁ →ₗ[R] M₂) : f.dualMap = f.lcomp R R := rfl -- Porting note: with reducible def need to specify some parameters to transpose explicitly theorem LinearMap.dualMap_def (f : M₁ →ₗ[R] M₂) : f.dualMap = Module.Dual.transpose (R := R) f := diff --git a/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean b/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean index 9b95709365e77..5cb5ec5a23786 100644 --- a/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean +++ b/Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean @@ -679,7 +679,7 @@ noncomputable def divisionRingOfFiniteDimensional (F K : Type*) [Field F] [Ring inv x := letI := Classical.decEq K if H : x = 0 then 0 else Classical.choose <| FiniteDimensional.exists_mul_eq_one F H - mul_inv_cancel x hx := show x * dite _ (h := _) _ = _ by + mul_inv_cancel x hx := show x * dite _ (h := _) _ _ = _ by rw [dif_neg hx] exact (Classical.choose_spec (FiniteDimensional.exists_mul_eq_one F hx):) inv_zero := dif_pos rfl diff --git a/Mathlib/LinearAlgebra/Semisimple.lean b/Mathlib/LinearAlgebra/Semisimple.lean index ea02d0bd4374e..0e6a2d2d2beb3 100644 --- a/Mathlib/LinearAlgebra/Semisimple.lean +++ b/Mathlib/LinearAlgebra/Semisimple.lean @@ -80,7 +80,7 @@ lemma eq_zero_of_isNilpotent_isSemisimple (hn : IsNilpotent f) (hs : f.IsSemisim have ⟨n, h0⟩ := hn rw [← aeval_X (R := R) f]; rw [← aeval_X_pow (R := R) f] at h0 rw [← RingHom.mem_ker, ← AEval.annihilator_eq_ker_aeval (M := M)] at h0 ⊢ - exact hs.annihilator_isRadical ⟨n, h0⟩ + exact hs.annihilator_isRadical _ _ ⟨n, h0⟩ @[simp] lemma isSemisimple_sub_algebraMap_iff {μ : R} : diff --git a/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean b/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean index 2f8a1d3a28cd8..c03fe0b8cbd59 100644 --- a/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean +++ b/Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean @@ -217,7 +217,7 @@ theorem seq_next {x : 𝓞 K} (hx : x ≠ 0) : fun w => ⟨(w x) / 2, div_nonneg (AbsoluteValue.nonneg _ _) (by norm_num)⟩ suffices ∀ w, w ≠ w₁ → f w ≠ 0 by obtain ⟨g, h_geqf, h_gprod⟩ := adjust_f K B this - obtain ⟨y, h_ynz, h_yle⟩ := exists_ne_zero_mem_ringOfIntegers_lt (f := g) + obtain ⟨y, h_ynz, h_yle⟩ := exists_ne_zero_mem_ringOfIntegers_lt K (f := g) (by rw [convexBodyLT_volume]; convert hB; exact congr_arg ((↑) : NNReal → ENNReal) h_gprod) refine ⟨y, h_ynz, fun w hw => (h_geqf w hw ▸ h_yle w).trans ?_, ?_⟩ · rw [← Rat.cast_le (K := ℝ), Rat.cast_natCast] diff --git a/Mathlib/Order/Directed.lean b/Mathlib/Order/Directed.lean index 39d27f9b220b1..29285fca18124 100644 --- a/Mathlib/Order/Directed.lean +++ b/Mathlib/Order/Directed.lean @@ -167,7 +167,7 @@ instance OrderDual.isDirected_le [LE α] [IsDirected α (· ≥ ·)] : IsDirecte /-- A monotone function on an upwards-directed type is directed. -/ theorem directed_of_isDirected_le [LE α] [IsDirected α (· ≤ ·)] {f : α → β} {r : β → β → Prop} (H : ∀ ⦃i j⦄, i ≤ j → r (f i) (f j)) : Directed r f := - directed_id.mono_comp H + directed_id.mono_comp _ H theorem Monotone.directed_le [Preorder α] [IsDirected α (· ≤ ·)] [Preorder β] {f : α → β} : Monotone f → Directed (· ≤ ·) f := diff --git a/Mathlib/Order/Filter/Bases.lean b/Mathlib/Order/Filter/Bases.lean index dfe2683487ad8..66d78953d6538 100644 --- a/Mathlib/Order/Filter/Bases.lean +++ b/Mathlib/Order/Filter/Bases.lean @@ -668,7 +668,7 @@ theorem HasBasis.eq_iInf (h : l.HasBasis (fun _ => True) s) : l = ⨅ i, 𝓟 (s theorem hasBasis_iInf_principal {s : ι → Set α} (h : Directed (· ≥ ·) s) [Nonempty ι] : (⨅ i, 𝓟 (s i)).HasBasis (fun _ => True) s := ⟨fun t => by - simpa only [true_and] using mem_iInf_of_directed (h.mono_comp monotone_principal.dual) t⟩ + simpa only [true_and] using mem_iInf_of_directed (h.mono_comp _ monotone_principal.dual) t⟩ /-- If `s : ι → Set α` is an indexed family of sets, then finite intersections of `s i` form a basis of `⨅ i, 𝓟 (s i)`. -/ @@ -683,7 +683,7 @@ theorem hasBasis_biInf_principal {s : β → Set α} {S : Set β} (h : DirectedO ⟨fun t => by refine mem_biInf_of_directed ?_ ne rw [directedOn_iff_directed, ← directed_comp] at h ⊢ - refine h.mono_comp ?_ + refine h.mono_comp _ ?_ exact fun _ _ => principal_mono.2⟩ theorem hasBasis_biInf_principal' {ι : Type*} {p : ι → Prop} {s : ι → Set α} diff --git a/Mathlib/RingTheory/AdjoinRoot.lean b/Mathlib/RingTheory/AdjoinRoot.lean index 7532a1f66cbdf..bba7f1e3e7457 100644 --- a/Mathlib/RingTheory/AdjoinRoot.lean +++ b/Mathlib/RingTheory/AdjoinRoot.lean @@ -353,11 +353,11 @@ noncomputable instance instField [Fact (Irreducible f)] : Field (AdjoinRoot f) w ratCast_def q := by rw [← map_natCast (of f), ← map_intCast (of f), ← map_div₀, ← Rat.cast_def]; rfl nnqsmul_def q x := - AdjoinRoot.induction_on (C := fun y ↦ q • y = (of f) q * y) x fun p ↦ by + AdjoinRoot.induction_on f (C := fun y ↦ q • y = (of f) q * y) x fun p ↦ by simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.nnqsmul_eq_C_mul] qsmul_def q x := -- Porting note: I gave the explicit motive and changed `rw` to `simp`. - AdjoinRoot.induction_on (C := fun y ↦ q • y = (of f) q * y) x fun p ↦ by + AdjoinRoot.induction_on f (C := fun y ↦ q • y = (of f) q * y) x fun p ↦ by simp only [smul_mk, of, RingHom.comp_apply, ← (mk f).map_mul, Polynomial.qsmul_eq_C_mul] theorem coe_injective (h : degree f ≠ 0) : Function.Injective ((↑) : K → AdjoinRoot f) := diff --git a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean index 0a9301168ce1c..146fc3d8f12a9 100644 --- a/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean +++ b/Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean @@ -395,14 +395,14 @@ variable [Algebra R A] [Algebra R A'] [IsScalarTower R A B] [IsScalarTower R A' /-- Integral closures are all isomorphic to each other. -/ noncomputable def equiv : A ≃ₐ[R] A' := AlgEquiv.ofAlgHom - (lift _ B (isIntegral := isIntegral_algebra R B)) - (lift _ B (isIntegral := isIntegral_algebra R B)) + (lift R A' B (isIntegral := isIntegral_algebra R B)) + (lift R A B (isIntegral := isIntegral_algebra R B)) (by ext x; apply algebraMap_injective A' R B; simp) (by ext x; apply algebraMap_injective A R B; simp) @[simp] theorem algebraMap_equiv (x : A) : algebraMap A' B (equiv R A B A' x) = algebraMap A B x := - algebraMap_lift A' B (isIntegral := isIntegral_algebra R B) x + algebraMap_lift R A' B (isIntegral := isIntegral_algebra R B) x end Equiv diff --git a/Mathlib/RingTheory/LocalRing/Module.lean b/Mathlib/RingTheory/LocalRing/Module.lean index 06103c98b607e..6def761f3d59e 100644 --- a/Mathlib/RingTheory/LocalRing/Module.lean +++ b/Mathlib/RingTheory/LocalRing/Module.lean @@ -178,19 +178,21 @@ theorem free_of_maximalIdeal_rTensor_injective [Module.FinitePresentation R M] FiniteDimensional.finrank_finsupp_self, one_mul, add_zero] rw [FiniteDimensional.finrank_eq_card_chooseBasisIndex] -- On the other hand, `m ⊗ M → M` injective => `Tor₁(k, M) = 0` => `k ⊗ ker(i) → kᴵ` injective. - have := @lTensor_injective_of_exact_of_exact_of_rTensor_injective - (N₁ := LinearMap.ker i) (N₂ := I →₀ R) (N₃ := M) - (f₁ := (𝔪).subtype) (f₂ := Submodule.mkQ 𝔪) inferInstance inferInstance inferInstance - inferInstance inferInstance inferInstance intro x - apply @this (LinearMap.ker i).subtype i (LinearMap.exact_subtype_mkQ 𝔪) - (Submodule.mkQ_surjective _) (LinearMap.exact_subtype_ker_map i) hi H - (Module.Flat.lTensor_preserves_injective_linearMap _ Subtype.val_injective) - apply hi'.injective - rw [LinearMap.baseChange_eq_ltensor] - erw [← LinearMap.comp_apply (i.lTensor k), ← LinearMap.lTensor_comp] - rw [(LinearMap.exact_subtype_ker_map i).linearMap_comp_eq_zero] - simp only [LinearMap.lTensor_zero, LinearMap.zero_apply, map_zero] + refine lTensor_injective_of_exact_of_exact_of_rTensor_injective + (N₁ := LinearMap.ker i) (N₂ := I →₀ R) (N₃ := M) + (f₁ := (𝔪).subtype) (f₂ := Submodule.mkQ 𝔪) + (g₁ := (LinearMap.ker i).subtype) (g₂ := i) (LinearMap.exact_subtype_mkQ 𝔪) + (Submodule.mkQ_surjective _) (LinearMap.exact_subtype_ker_map i) hi H ?_ ?_ + · apply Module.Flat.lTensor_preserves_injective_linearMap + (N := LinearMap.ker i) (N' := I →₀ R) + (L := (LinearMap.ker i).subtype) + exact Subtype.val_injective + · apply hi'.injective + rw [LinearMap.baseChange_eq_ltensor] + erw [← LinearMap.comp_apply (i.lTensor k), ← LinearMap.lTensor_comp] + rw [(LinearMap.exact_subtype_ker_map i).linearMap_comp_eq_zero] + simp only [LinearMap.lTensor_zero, LinearMap.zero_apply, map_zero] -- TODO: Generalise this to finite free modules. theorem free_of_flat_of_localRing [Module.FinitePresentation R P] [Module.Flat R P] : diff --git a/Mathlib/RingTheory/Localization/FractionRing.lean b/Mathlib/RingTheory/Localization/FractionRing.lean index 1960bbcd7e01d..f4b231a725789 100644 --- a/Mathlib/RingTheory/Localization/FractionRing.lean +++ b/Mathlib/RingTheory/Localization/FractionRing.lean @@ -132,7 +132,7 @@ noncomputable abbrev toField : Field K where lemma surjective_iff_isField [IsDomain R] : Function.Surjective (algebraMap R K) ↔ IsField R where mp h := (RingEquiv.ofBijective (algebraMap R K) - ⟨IsFractionRing.injective R K, h⟩).toMulEquiv.isField (IsFractionRing.toField R).toIsField + ⟨IsFractionRing.injective R K, h⟩).toMulEquiv.isField _ (IsFractionRing.toField R).toIsField mpr h := letI := h.toField (IsLocalization.atUnits R _ (S := K) diff --git a/Mathlib/RingTheory/RingHomProperties.lean b/Mathlib/RingTheory/RingHomProperties.lean index 1b12d138c4092..7008cd0ef9a74 100644 --- a/Mathlib/RingTheory/RingHomProperties.lean +++ b/Mathlib/RingTheory/RingHomProperties.lean @@ -185,9 +185,11 @@ lemma toMorphismProperty_respectsIso_iff : · intro X Y Z e f hf exact h.left f e.commRingCatIsoToRingEquiv hf · intro X Y Z _ _ _ f e hf - exact h.postcomp e.toCommRingCatIso.hom (CommRingCat.ofHom f) hf + exact MorphismProperty.RespectsIso.postcomp (toMorphismProperty P) + e.toCommRingCatIso.hom (CommRingCat.ofHom f) hf · intro X Y Z _ _ _ f e - exact h.precomp e.toCommRingCatIso.hom (CommRingCat.ofHom f) + exact MorphismProperty.RespectsIso.precomp (toMorphismProperty P) + e.toCommRingCatIso.hom (CommRingCat.ofHom f) end ToMorphismProperty diff --git a/Mathlib/RingTheory/SimpleRing/Basic.lean b/Mathlib/RingTheory/SimpleRing/Basic.lean index c9f5a875cc0b8..3f9711cafff02 100644 --- a/Mathlib/RingTheory/SimpleRing/Basic.lean +++ b/Mathlib/RingTheory/SimpleRing/Basic.lean @@ -82,6 +82,6 @@ lemma isField_center (A : Type*) [Ring A] [IsSimpleRing A] : IsField (Subring.ce end IsSimpleRing lemma isSimpleRing_iff_isField (A : Type*) [CommRing A] : IsSimpleRing A ↔ IsField A := - ⟨fun _ ↦ Subring.topEquiv.symm.toMulEquiv.isField <| by + ⟨fun _ ↦ Subring.topEquiv.symm.toMulEquiv.isField _ <| by rw [← Subring.center_eq_top A]; exact IsSimpleRing.isField_center A, fun h ↦ letI := h.toField; inferInstance⟩ diff --git a/Mathlib/RingTheory/Smooth/StandardSmooth.lean b/Mathlib/RingTheory/Smooth/StandardSmooth.lean index d8064eb6a7e8c..27f9f744151d9 100644 --- a/Mathlib/RingTheory/Smooth/StandardSmooth.lean +++ b/Mathlib/RingTheory/Smooth/StandardSmooth.lean @@ -324,14 +324,14 @@ instance IsStandardSmooth.baseChange [IsStandardSmooth.{t, w} R S] : IsStandardSmooth.{t, w} T (T ⊗[R] S) where out := by obtain ⟨⟨P⟩⟩ := ‹IsStandardSmooth R S› - exact ⟨P.baseChange T⟩ + exact ⟨P.baseChange R S T⟩ instance IsStandardSmoothOfRelativeDimension.baseChange [IsStandardSmoothOfRelativeDimension.{t, w} n R S] : IsStandardSmoothOfRelativeDimension.{t, w} n T (T ⊗[R] S) where out := by obtain ⟨P, hP⟩ := ‹IsStandardSmoothOfRelativeDimension n R S› - exact ⟨P.baseChange T, hP⟩ + exact ⟨P.baseChange R S T, hP⟩ end BaseChange diff --git a/Mathlib/Tactic/Ring/Basic.lean b/Mathlib/Tactic/Ring/Basic.lean index 498f20124180d..dcd4f4ddf5f6f 100644 --- a/Mathlib/Tactic/Ring/Basic.lean +++ b/Mathlib/Tactic/Ring/Basic.lean @@ -1014,7 +1014,7 @@ def ExSum.evalInv {a : Q($α)} (czα : Option Q(CharZero $α)) (va : ExSum sα a match va with | ExSum.zero => pure ⟨_, .zero, (q(inv_zero (R := $α)) : Expr)⟩ | ExSum.add va ExSum.zero => do - let ⟨_, vb, pb⟩ ← va.evalInv dα czα + let ⟨_, vb, pb⟩ ← va.evalInv sα dα czα pure ⟨_, vb.toSum, (q(inv_single $pb) : Expr)⟩ | va => do let ⟨_, vb, pb⟩ ← evalInvAtom sα dα a diff --git a/Mathlib/Topology/Algebra/Valued/NormedValued.lean b/Mathlib/Topology/Algebra/Valued/NormedValued.lean index dbe91b1484df4..2c9ce7c08f2c8 100644 --- a/Mathlib/Topology/Algebra/Valued/NormedValued.lean +++ b/Mathlib/Topology/Algebra/Valued/NormedValued.lean @@ -102,7 +102,7 @@ def toNormedField : NormedField L := · set δ : ℝ≥0 := hv.hom ε with hδ have hδ_pos : 0 < δ := by rw [hδ, ← _root_.map_zero hv.hom] - exact hv.strictMono (Units.zero_lt ε) + exact hv.strictMono _ (Units.zero_lt ε) use δ, hδ_pos apply subset_trans _ hε intro x hx diff --git a/Mathlib/Topology/Category/LightProfinite/Extend.lean b/Mathlib/Topology/Category/LightProfinite/Extend.lean index bed0658153636..4f7e5eb315b90 100644 --- a/Mathlib/Topology/Category/LightProfinite/Extend.lean +++ b/Mathlib/Topology/Category/LightProfinite/Extend.lean @@ -118,7 +118,7 @@ then `cone G c.pt` is a limit cone. -/ noncomputable def isLimitCone (hc : IsLimit c) [∀ i, Epi (c.π.app i)] (hc' : IsLimit <| G.mapCone c) : - IsLimit (cone G c.pt) := (functor_initial c hc).isLimitWhiskerEquiv _ hc' + IsLimit (cone G c.pt) := (functor_initial c hc).isLimitWhiskerEquiv _ _ hc' end Limit @@ -158,7 +158,7 @@ noncomputable def isColimitCocone (hc : IsLimit c) [∀ i, Epi (c.π.app i)] (hc' : IsColimit <| G.mapCocone c.op) : IsColimit (cocone G c.pt) := haveI := functorOp_final c hc - (Functor.final_comp (opOpEquivalence ℕ).functor (functorOp c)).isColimitWhiskerEquiv _ hc' + (Functor.final_comp (opOpEquivalence ℕ).functor (functorOp c)).isColimitWhiskerEquiv _ _ hc' end Colimit diff --git a/Mathlib/Topology/Category/Profinite/Extend.lean b/Mathlib/Topology/Category/Profinite/Extend.lean index 8db0cc4dd84e9..2c00a5e5808e0 100644 --- a/Mathlib/Topology/Category/Profinite/Extend.lean +++ b/Mathlib/Topology/Category/Profinite/Extend.lean @@ -141,7 +141,7 @@ then `cone G c.pt` is a limit cone. -/ noncomputable def isLimitCone (hc : IsLimit c) [∀ i, Epi (c.π.app i)] (hc' : IsLimit <| G.mapCone c) : - IsLimit (cone G c.pt) := (functor_initial c hc).isLimitWhiskerEquiv _ hc' + IsLimit (cone G c.pt) := (functor_initial c hc).isLimitWhiskerEquiv _ _ hc' end Limit @@ -177,7 +177,7 @@ are epimorphic, then `cocone G c.pt` is a colimit cone. -/ noncomputable def isColimitCocone (hc : IsLimit c) [∀ i, Epi (c.π.app i)] (hc' : IsColimit <| G.mapCocone c.op) : - IsColimit (cocone G c.pt) := (functorOp_final c hc).isColimitWhiskerEquiv _ hc' + IsColimit (cocone G c.pt) := (functorOp_final c hc).isColimitWhiskerEquiv _ _ hc' end Colimit diff --git a/Mathlib/Util/CountHeartbeats.lean b/Mathlib/Util/CountHeartbeats.lean index 3b30d85e1aa29..bbc00430ba743 100644 --- a/Mathlib/Util/CountHeartbeats.lean +++ b/Mathlib/Util/CountHeartbeats.lean @@ -43,8 +43,8 @@ def runTacForHeartbeats (tac : TSyntax `Lean.Parser.Tactic.tacticSeq) (revert : Given a `List Nat`, return the minimum, maximum, and standard deviation. -/ def variation (counts : List Nat) : List Nat := - let min := counts.minimum?.getD 0 - let max := counts.maximum?.getD 0 + let min := counts.min?.getD 0 + let max := counts.max?.getD 0 let toFloat (n : Nat) := n.toUInt64.toFloat let toNat (f : Float) := f.toUInt64.toNat let counts' := counts.map toFloat diff --git a/lake-manifest.json b/lake-manifest.json index 588da02296eac..8aede30b089cc 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2c9497c893a4f81411023b56c51f2473c7c3c452", + "rev": "5f08456bdf87fffa721603c8988b565ae0e31f4d", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "nightly-testing", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a895713f7701e295a015b1087f3113fd3d615272", + "rev": "50aaaf78b7db5bd635c19c660d59ed31b9bc9b5a", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", diff --git a/lean-toolchain b/lean-toolchain index cbe615647f9be..21c9a36ee0c70 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-09-26 +leanprover/lean4:nightly-2024-09-30 diff --git a/test/aesop_cat.lean b/test/aesop_cat.lean index 7790b9c1b983c..549cd69b92adb 100644 --- a/test/aesop_cat.lean +++ b/test/aesop_cat.lean @@ -10,6 +10,8 @@ example : Foo where x := sorry /-- +error: could not synthesize default value for field 'w' of 'Foo' using tactics +--- error: tactic 'aesop' failed, failed to prove the goal after exhaustive search. Initial goal: ⊢ 35 = 37 diff --git a/test/says.lean b/test/says.lean index e2f9a3f834662..4315e51cb870d 100644 --- a/test/says.lean +++ b/test/says.lean @@ -101,7 +101,8 @@ def very_long_lemma_name_aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa : Q → P := fun _ @[simp] def very_long_lemma_name_bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb : Q := trivial /-- -info: Try this: aesop? says simp_all only [very_long_lemma_name_bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb, +info: Try this: aesop? says + simp_all only [very_long_lemma_name_bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb, very_long_lemma_name_aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa] -/ #guard_msgs in