diff --git a/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean b/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean index f2aa25b41cad5..5e08c95817557 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/Basic.lean @@ -526,7 +526,7 @@ theorem diagonalTargetAffineLocallyOfOpenCover (P : AffineTargetMorphismProperty let 𝒱 := (Scheme.Pullback.openCoverOfBase 𝒰 f f).bind fun i => Scheme.Pullback.openCoverOfLeftRight.{u} (𝒰' i) (𝒰' i) pullback.snd pullback.snd have i1 : ∀ i, IsAffine (𝒱.obj i) := fun i => by dsimp [𝒱]; infer_instance - refine' (hP.affine_openCover_iff _ _).mpr _ + refine' (hP.affine_openCover_iff _ 𝒱).mpr _ rintro ⟨i, j, k⟩ dsimp [𝒱] convert (affine_cancel_left_isIso hP.1 diff --git a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean index aaafbddb325a4..60f650dce95e3 100644 --- a/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean +++ b/Mathlib/AlgebraicGeometry/Morphisms/QuasiCompact.lean @@ -136,8 +136,8 @@ theorem isCompact_basicOpen (X : Scheme) {U : Opens X.carrier} (hU : IsCompact ( use V.1 ⊓ X.basicOpen f have : V.1.1 ⟶ U := by apply homOfLE; change _ ⊆ (U : Set X.carrier); rw [e] - convert @Set.subset_iUnion₂ _ _ _ - (fun (U : X.affineOpens) (_ : U ∈ s) => ↑U) V V.prop using 1 + convert Set.subset_iUnion₂ (s := fun (U : X.affineOpens) (_ : U ∈ s) => (U : Set X.carrier)) + V V.prop using 1 erw [← X.toLocallyRingedSpace.toRingedSpace.basicOpen_res this.op] exact IsAffineOpen.basicOpenIsAffine V.1.prop _ haveI : Finite s := hs.to_subtype diff --git a/Mathlib/AlgebraicGeometry/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/StructureSheaf.lean index 6d18284ab3da7..a31e098178883 100644 --- a/Mathlib/AlgebraicGeometry/StructureSheaf.lean +++ b/Mathlib/AlgebraicGeometry/StructureSheaf.lean @@ -980,10 +980,7 @@ instance IsLocalization.to_basicOpen (r : R) : #align algebraic_geometry.structure_sheaf.is_localization.to_basic_open AlgebraicGeometry.StructureSheaf.IsLocalization.to_basicOpen instance to_basicOpen_epi (r : R) : Epi (toOpen R (PrimeSpectrum.basicOpen r)) := - ⟨fun {S} f g h => by - refine' IsLocalization.ringHom_ext (R := R) - (S := (structureSheaf R).val.obj (op <| PrimeSpectrum.basicOpen r)) _ _ - exact h⟩ + ⟨fun _ _ h => IsLocalization.ringHom_ext (Submonoid.powers r) h⟩ #align algebraic_geometry.structure_sheaf.to_basic_open_epi AlgebraicGeometry.StructureSheaf.to_basicOpen_epi @[elementwise] diff --git a/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean b/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean index 573533c76baba..89e3789dac386 100644 --- a/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean +++ b/Mathlib/Analysis/BoxIntegral/Partition/Basic.lean @@ -625,7 +625,7 @@ theorem filter_true : (π.filter fun _ => True) = π := theorem iUnion_filter_not (π : Prepartition I) (p : Box ι → Prop) : (π.filter fun J => ¬p J).iUnion = π.iUnion \ (π.filter p).iUnion := by simp only [Prepartition.iUnion] - convert (@Set.biUnion_diff_biUnion_eq _ (Box ι) π.boxes (π.filter p).boxes (↑) _).symm + convert (@Set.biUnion_diff_biUnion_eq (ι → ℝ) (Box ι) π.boxes (π.filter p).boxes (↑) _).symm · simp (config := { contextual := true }) · rw [Set.PairwiseDisjoint] convert π.pairwiseDisjoint diff --git a/Mathlib/Analysis/Convex/Segment.lean b/Mathlib/Analysis/Convex/Segment.lean index d3b4e756dfd9d..7f00d83c55df7 100644 --- a/Mathlib/Analysis/Convex/Segment.lean +++ b/Mathlib/Analysis/Convex/Segment.lean @@ -337,12 +337,12 @@ theorem midpoint_mem_segment [Invertible (2 : 𝕜)] (x y : E) : midpoint 𝕜 x #align midpoint_mem_segment midpoint_mem_segment theorem mem_segment_sub_add [Invertible (2 : 𝕜)] (x y : E) : x ∈ [x - y -[𝕜] x + y] := by - convert @midpoint_mem_segment 𝕜 _ _ _ _ _ _ _ + convert @midpoint_mem_segment 𝕜 _ _ _ _ _ (x - y) (x + y) rw [midpoint_sub_add] #align mem_segment_sub_add mem_segment_sub_add theorem mem_segment_add_sub [Invertible (2 : 𝕜)] (x y : E) : x ∈ [x + y -[𝕜] x - y] := by - convert @midpoint_mem_segment 𝕜 _ _ _ _ _ _ _ + convert @midpoint_mem_segment 𝕜 _ _ _ _ _ (x + y) (x - y) rw [midpoint_add_sub] #align mem_segment_add_sub mem_segment_add_sub diff --git a/Mathlib/Analysis/InnerProductSpace/l2Space.lean b/Mathlib/Analysis/InnerProductSpace/l2Space.lean index 4bc12fcc49983..4d082b19a3c2e 100644 --- a/Mathlib/Analysis/InnerProductSpace/l2Space.lean +++ b/Mathlib/Analysis/InnerProductSpace/l2Space.lean @@ -475,7 +475,7 @@ protected theorem dense_span (b : HilbertBasis ι 𝕜 E) : protected theorem hasSum_inner_mul_inner (b : HilbertBasis ι 𝕜 E) (x y : E) : HasSum (fun i => ⟪x, b i⟫ * ⟪b i, y⟫) ⟪x, y⟫ := by - convert (b.hasSum_repr y).mapL (innerSL _ x) using 1 + convert (b.hasSum_repr y).mapL (innerSL 𝕜 x) using 1 ext i rw [innerSL_apply, b.repr_apply_apply, inner_smul_right, mul_comm] #align hilbert_basis.has_sum_inner_mul_inner HilbertBasis.hasSum_inner_mul_inner diff --git a/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean b/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean index e3ce6ccbadc29..e650e293e0ba2 100644 --- a/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean +++ b/Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean @@ -351,7 +351,7 @@ instance finiteDimensional_vectorSpan_insert (s : AffineSubspace k P) rcases (s : Set P).eq_empty_or_nonempty with (hs | ⟨p₀, hp₀⟩) · rw [coe_eq_bot_iff] at hs rw [hs, bot_coe, span_empty, bot_coe, direction_affineSpan] - convert finiteDimensional_bot _ _ <;> simp + convert finiteDimensional_bot k V <;> simp · rw [affineSpan_coe, direction_affineSpan_insert hp₀] infer_instance #align finite_dimensional_vector_span_insert finiteDimensional_vectorSpan_insert diff --git a/Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean b/Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean index fd46ee41b627d..5ba1b2bd676e1 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean @@ -120,7 +120,7 @@ theorem vanishesTrivially_of_sum_tmul_eq_zero (hm : Submodule.span R (Set.range have exact_ker_subtype : Exact (ker G).subtype G := G.exact_subtype_ker_map -- Tensor the exact sequence with $N$. have exact_rTensor_ker_subtype : Exact (rTensor N (ker G).subtype) (rTensor N G) := - rTensor_exact N exact_ker_subtype G_surjective + rTensor_exact (M := ↥(ker G)) N exact_ker_subtype G_surjective /- We conclude that $\sum_i e_i \otimes n_i$ is in the range of $\ker G \otimes N \to R^\iota \otimes N$. -/ have en_mem_range : en ∈ range (rTensor N (ker G).subtype) := diff --git a/Mathlib/NumberTheory/Padics/PadicVal.lean b/Mathlib/NumberTheory/Padics/PadicVal.lean index 4681b52cbac37..8b52329f22667 100644 --- a/Mathlib/NumberTheory/Padics/PadicVal.lean +++ b/Mathlib/NumberTheory/Padics/PadicVal.lean @@ -768,8 +768,8 @@ digits of `k` plus the sum of the digits of `n - k` minus the sum of digits of ` theorem sub_one_mul_padicValNat_choose_eq_sub_sum_digits {k n : ℕ} [hp : Fact p.Prime] (h : k ≤ n) : (p - 1) * padicValNat p (choose n k) = (p.digits k).sum + (p.digits (n - k)).sum - (p.digits n).sum := by - convert @sub_one_mul_padicValNat_choose_eq_sub_sum_digits' _ _ _ _ - all_goals exact Nat.eq_add_of_sub_eq h rfl + convert @sub_one_mul_padicValNat_choose_eq_sub_sum_digits' _ _ _ ‹_› + all_goals omega end padicValNat diff --git a/Mathlib/RingTheory/Jacobson.lean b/Mathlib/RingTheory/Jacobson.lean index 1a2b74cdf7a1e..7f57b08baea2d 100644 --- a/Mathlib/RingTheory/Jacobson.lean +++ b/Mathlib/RingTheory/Jacobson.lean @@ -491,7 +491,7 @@ theorem isMaximal_comap_C_of_isMaximal [Nontrivial R] (hP' : ∀ x : R, C x ∈ suffices (⊥ : Ideal (Localization M)).IsMaximal by rw [← IsLocalization.comap_map_of_isPrime_disjoint M (Localization M) ⊥ bot_prime (disjoint_iff_inf_le.mpr fun x hx => hM (hx.2 ▸ hx.1))] - refine' ((isMaximal_iff_isMaximal_disjoint (Localization M) _ _).mp (by rwa [map_bot])).1 + refine' ((isMaximal_iff_isMaximal_disjoint (Localization M) a _).mp (by rwa [map_bot])).1 let M' : Submonoid (R[X] ⧸ P) := M.map φ have hM' : (0 : R[X] ⧸ P) ∉ M' := fun ⟨z, hz⟩ => hM (quotientMap_injective (_root_.trans hz.2 φ.map_zero.symm) ▸ hz.1)