chore: adaptations to lean 4.8.0 (#12583)

Mainly this adds names to instances, which are presumably necessary for some unspecified reason.

Mathlib/Analysis/Complex/Basic.lean

@@ -60,7 +60,7 @@ theorem norm_exp_ofReal_mul_I (t : ℝ) : ‖exp (t * I)‖ = 1 := by
 set_option linter.uppercaseLean3 false in
 #align complex.norm_exp_of_real_mul_I Complex.norm_exp_ofReal_mul_I
 
-instance : NormedAddCommGroup ℂ :=
+instance instNormedAddCommGroup : NormedAddCommGroup ℂ :=
   AddGroupNorm.toNormedAddCommGroup
     { abs with
       map_zero' := map_zero abs

Mathlib/Analysis/NormedSpace/AffineIsometry.lean

@@ -589,7 +589,7 @@ theorem trans_assoc (ePP₂ : P ≃ᵃⁱ[𝕜] P₂) (eP₂G : P₂ ≃ᵃⁱ[
 #align affine_isometry_equiv.trans_assoc AffineIsometryEquiv.trans_assoc
 
 /-- The group of affine isometries of a `NormedAddTorsor`, `P`. -/
-instance : Group (P ≃ᵃⁱ[𝕜] P) where
+instance instGroup : Group (P ≃ᵃⁱ[𝕜] P) where
   mul e₁ e₂ := e₂.trans e₁
   one := refl _ _
   inv := symm

Mathlib/Data/Complex/Module.lean

@@ -95,7 +95,7 @@ instance (priority := 100) instModule [Semiring R] [Module R ℝ] : Module R ℂ
   zero_smul r := by ext <;> simp [smul_re, smul_im, zero_smul]
 
 -- priority manually adjusted in #11980
-instance (priority := 95) [CommSemiring R] [Algebra R ℝ] : Algebra R ℂ :=
+instance (priority := 95) instAlgebraOfReal [CommSemiring R] [Algebra R ℝ] : Algebra R ℂ :=
   { Complex.ofReal.comp (algebraMap R ℝ) with
     smul := (· • ·)
     smul_def' := fun r x => by ext <;> simp [smul_re, smul_im, Algebra.smul_def]

Mathlib/Data/Finsupp/Notation.lean

@@ -63,7 +63,7 @@ def updateUnexpander : Lean.PrettyPrinter.Unexpander
   | _ => throw ()
 
 /-- Display `Finsupp` using `fun₀` notation. -/
-unsafe instance {α β} [Repr α] [Repr β] [Zero β] : Repr (α →₀ β) where
+unsafe instance instRepr {α β} [Repr α] [Repr β] [Zero β] : Repr (α →₀ β) where
   reprPrec f p :=
     if f.support.card = 0 then
       "0"

Mathlib/Data/Rat/Order.lean

@@ -183,7 +183,7 @@ instance : LT ℚ := by infer_instance
 
 instance : DistribLattice ℚ := by infer_instance
 
-instance : Lattice ℚ := by infer_instance
+instance instLattice : Lattice ℚ := by infer_instance
 
 instance : SemilatticeInf ℚ := by infer_instance
 

Mathlib/Data/ZMod/Basic.lean

@@ -1246,7 +1246,7 @@ private theorem mul_inv_cancel_aux (a : ZMod p) (h : a ≠ 0) : a * a⁻¹ = 1 :
   rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]
 
 /-- Field structure on `ZMod p` if `p` is prime. -/
-instance : Field (ZMod p) where
+instance instField : Field (ZMod p) where
   mul_inv_cancel := mul_inv_cancel_aux p
   inv_zero := inv_zero p
   nnqsmul := _

Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean

@@ -319,7 +319,7 @@ theorem _root_.tendsto_riemannZeta_sub_one_div :
     refine hC.comp (tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ ?_ ?_)
     · exact (Complex.continuous_ofReal.tendsto 1).mono_left (nhdsWithin_le_nhds ..)
     · filter_upwards [self_mem_nhdsWithin] with a ha
-      rw [mem_compl_singleton_iff, ← Complex.ofReal_one, Ne.def, Complex.ofReal_inj]
+      rw [mem_compl_singleton_iff, ← Complex.ofReal_one, Ne, Complex.ofReal_inj]
       exact ne_of_gt ha
   refine ⟨_, Complex.tendsto_limUnder_of_differentiable_on_punctured_nhds_of_isLittleO ?_ ?_⟩
   · filter_upwards [self_mem_nhdsWithin] with s hs

Mathlib/NumberTheory/ZetaFunction.lean

@@ -767,7 +767,7 @@ theorem riemannZeta_neg_nat_eq_bernoulli (k : ℕ) :
           push_cast; ring_nf]
     -- substitute in what we know about zeta values at positive integers
     have step1 := congr_arg ((↑) : ℝ → ℂ) (hasSum_zeta_nat (by norm_num : m + 1 ≠ 0)).tsum_eq
-    have step2 := zeta_nat_eq_tsum_of_gt_one (by rw [mul_add]; norm_num : 1 < 2 * (m + 1))
+    have step2 := zeta_nat_eq_tsum_of_gt_one (by rw [mul_add]; omega : 1 < 2 * (m + 1))
     simp_rw [ofReal_tsum, ofReal_div, ofReal_one, ofReal_pow, ofReal_natCast] at step1
     rw [step1, (by norm_cast : (↑(2 * (m + 1)) : ℂ) = 2 * ↑m + 2)] at step2
     rw [step2, mul_div]

Mathlib/Order/Booleanisation.lean

@@ -39,7 +39,8 @@ def Booleanisation (α : Type*) := α ⊕ α
 
 namespace Booleanisation
 
-instance instDecidableEq [DecidableEq α] : DecidableEq (Booleanisation α) := Sum.instDecidableEqSum
+instance instDecidableEq [DecidableEq α] : DecidableEq (Booleanisation α) :=
+  inferInstanceAs <| DecidableEq (α ⊕ α)
 
 variable [GeneralizedBooleanAlgebra α] {x y : Booleanisation α} {a b : α}
 

Mathlib/RingTheory/Ideal/Colon.lean

@@ -29,7 +29,7 @@ def colon (N P : Submodule R M) : Ideal R :=
 theorem mem_colon {r} : r ∈ N.colon P ↔ ∀ p ∈ P, r • p ∈ N :=
   mem_annihilator.trans
      ⟨fun H p hp => (Quotient.mk_eq_zero N).1 (H (Quotient.mk p) (mem_map_of_mem hp)),
-       fun H _ ⟨p, hp, hpm⟩ => hpm ▸ (N.mkQ.map_smul r p ▸ (Quotient.mk_eq_zero N).2 <| H p hp)⟩
+       fun H _ ⟨p, hp, hpm⟩ => hpm ▸ ((Quotient.mk_eq_zero N).2 <| H p hp)⟩
 #align submodule.mem_colon Submodule.mem_colon
 
 theorem mem_colon' {r} : r ∈ N.colon P ↔ P ≤ comap (r • (LinearMap.id : M →ₗ[R] M)) N :=

Mathlib/RingTheory/Ideal/Quotient.lean

@@ -45,7 +45,7 @@ This definition is marked `reducible` so that typeclass instances can be shared
 `Ideal.Quotient I` and `Submodule.Quotient I`.
 -/
 @[reducible]
-instance : HasQuotient R (Ideal R) :=
+instance instHasQuotient : HasQuotient R (Ideal R) :=
   Submodule.hasQuotient
 
 namespace Quotient

Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean

@@ -115,13 +115,13 @@ theorem cyclotomic_pos {n : ℕ} (hn : 2 < n) {R} [LinearOrderedCommRing R] (x :
 
 theorem cyclotomic_pos_and_nonneg (n : ℕ) {R} [LinearOrderedCommRing R] (x : R) :
     (1 < x → 0 < eval x (cyclotomic n R)) ∧ (1 ≤ x → 0 ≤ eval x (cyclotomic n R)) := by
-  rcases n with (_ | _ | _ | n) <;>
-    simp [cyclotomic_zero, cyclotomic_one, cyclotomic_two, succ_eq_add_one, eval_X, eval_one,
-      eval_add, eval_sub, sub_nonneg, sub_pos, zero_lt_one, zero_le_one, imp_true_iff, imp_self,
-      and_self_iff]
-  · constructor <;> intro <;> linarith
-  · have : 2 < n + 3 := by linarith
-    constructor <;> intro <;> [skip; apply le_of_lt] <;> apply cyclotomic_pos this
+  rcases n with (_ | _ | _ | n)
+  · simp only [cyclotomic_zero, eval_one, zero_lt_one, implies_true, zero_le_one, and_self]
+  · simp only [zero_add, cyclotomic_one, eval_sub, eval_X, eval_one, sub_pos, imp_self, sub_nonneg,
+      and_self]
+  · simp only [zero_add, reduceAdd, cyclotomic_two, eval_add, eval_X, eval_one]
+    constructor <;> intro <;> linarith
+  · constructor <;> intro <;> [skip; apply le_of_lt] <;> apply cyclotomic_pos (by omega)
 #align polynomial.cyclotomic_pos_and_nonneg Polynomial.cyclotomic_pos_and_nonneg
 
 /-- Cyclotomic polynomials are always positive on inputs larger than one.

Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

@@ -271,16 +271,14 @@ theorem mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt {B : PowerBasis
   · intro _
     exact dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt hp hBint hQ hzint hei
   · intro hj
-    convert hp.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd _ hndiv
-    · exact n
+    convert hp.dvd_of_pow_dvd_pow_mul_pow_of_square_not_dvd (n := n) _ hndiv
     -- Two technical results we will need about `P.natDegree` and `Q.natDegree`.
     have H := degree_modByMonic_lt Q₁ (minpoly.monic hBint)
     rw [← hQ₁, ← hP] at H
     replace H := Nat.lt_iff_add_one_le.1
       (lt_of_lt_of_le
         (lt_of_le_of_lt (Nat.lt_iff_add_one_le.1 (Nat.lt_of_succ_lt_succ (mem_range.1 hj)))
           (lt_succ_self _)) (Nat.lt_iff_add_one_le.1 ((natDegree_lt_natDegree_iff hQzero).2 H)))
-    rw [add_assoc] at H
     have Hj : Q.natDegree + 1 = j + 1 + (Q.natDegree - j) := by
       rw [← add_comm 1, ← add_comm 1, add_assoc, add_right_inj,
         ← Nat.add_sub_assoc (Nat.lt_of_succ_lt_succ (mem_range.1 hj)).le, add_comm,
@@ -306,7 +304,7 @@ theorem mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt {B : PowerBasis
         Q.coeff (j + 1 + k) • B.gen ^ (j + 1 + k) * B.gen ^ (P.natDegree - (j + 2)) =
         (algebraMap R L) p * Q.coeff (j + 1 + k) • f (k + P.natDegree - 1) := by
       intro k hk
-      rw [smul_mul_assoc, ← pow_add, ← Nat.add_sub_assoc H, ← add_assoc j 1 1, add_comm (j + 1) 1,
+      rw [smul_mul_assoc, ← pow_add, ← Nat.add_sub_assoc H, add_comm (j + 1) 1,
         add_assoc (j + 1), add_comm _ (k + P.natDegree), Nat.add_sub_add_right,
         ← (hf (k + P.natDegree - 1) _).2, mul_smul_comm]
       rw [(minpoly.monic hBint).natDegree_map, add_comm, Nat.add_sub_assoc, le_add_iff_nonneg_right]
@@ -321,7 +319,7 @@ theorem mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAt {B : PowerBasis
         p ^ n.succ ∣ Q.coeff (succ j) ^ n.succ *
           (minpoly R B.gen).coeff 0 ^ (succ j + (P.natDegree - (j + 2))) by
       convert this
-      rw [Nat.succ_eq_add_one, add_assoc, ← Nat.add_sub_assoc H, ← add_assoc, add_comm (j + 1),
+      rw [Nat.succ_eq_add_one, add_assoc, ← Nat.add_sub_assoc H, add_comm (j + 1),
         Nat.add_sub_add_left, ← Nat.add_sub_assoc, Nat.add_sub_add_left, hP, ←
         (minpoly.monic hBint).natDegree_map (algebraMap R K), ←
         minpoly.isIntegrallyClosed_eq_field_fractions' K hBint, natDegree_minpoly, hn, Nat.sub_one,

Mathlib/RingTheory/PowerSeries/Basic.lean

@@ -680,9 +680,9 @@ theorem not_isField : ¬IsField A⟦X⟧ := by
     rw [Ring.not_isField_iff_exists_ideal_bot_lt_and_lt_top]
     use Ideal.span {X}
     constructor
-    · rw [bot_lt_iff_ne_bot, Ne.def, Ideal.span_singleton_eq_bot]
+    · rw [bot_lt_iff_ne_bot, Ne, Ideal.span_singleton_eq_bot]
       exact X_ne_zero
-    · rw [lt_top_iff_ne_top, Ne.def, Ideal.eq_top_iff_one, Ideal.mem_span_singleton,
+    · rw [lt_top_iff_ne_top, Ne, Ideal.eq_top_iff_one, Ideal.mem_span_singleton,
         X_dvd_iff, constantCoeff_one]
       exact one_ne_zero
 

Mathlib/RingTheory/PowerSeries/Order.lean

@@ -360,8 +360,8 @@ theorem order_mul (φ ψ : R⟦X⟧) : order (φ * ψ) = order φ + order ψ :=
 @[simp]
 theorem divided_by_X_pow_order_of_X_eq_one : divided_by_X_pow_order X_ne_zero = (1 : R⟦X⟧) := by
   rw [← mul_eq_left₀ X_ne_zero]
-  simpa only [order_X, X_ne_zero, PartENat.get_one, pow_one, Ne.def,
-    not_false_iff] using self_eq_X_pow_order_mul_divided_by_X_pow_order (@X_ne_zero R _ _)
+  simpa only [order_X, X_ne_zero, PartENat.get_one, pow_one, Ne, not_false_iff] using
+    self_eq_X_pow_order_mul_divided_by_X_pow_order (@X_ne_zero R _ _)
 
 -- Dividing a power series by the maximal power of `X` dividing it, respects multiplication.
 theorem divided_by_X_pow_orderMul {f g : R⟦X⟧} (hf : f ≠ 0) (hg : g ≠ 0) :

Mathlib/RingTheory/Valuation/RankOne.lean

@@ -65,7 +65,7 @@ def unit : Γ₀ˣ :=
 
 /-- A proof that `RankOne.unit v ≠ 1`. -/
 theorem unit_ne_one : unit v ≠ 1 := by
-  rw [Ne.def, ← Units.eq_iff, Units.val_one]
+  rw [Ne, ← Units.eq_iff, Units.val_one]
   exact ((nontrivial v).choose_spec ).2
 
 end RankOne

Mathlib/Topology/Algebra/GroupCompletion.lean

@@ -201,7 +201,7 @@ section UniformAddCommGroup
 
 variable [UniformSpace α] [AddCommGroup α] [UniformAddGroup α]
 
-instance : AddCommGroup (Completion α) :=
+instance instAddCommGroup : AddCommGroup (Completion α) :=
   { (inferInstance : AddGroup <| Completion α) with
     add_comm := fun a b ↦
       Completion.induction_on₂ a b

Mathlib/Topology/Algebra/Module/Basic.lean

@@ -1639,7 +1639,7 @@ theorem comp_smulₛₗ [SMulCommClass R₂ R₂ M₂] [SMulCommClass R₃ R₃
 
 instance distribMulAction [ContinuousAdd M₂] : DistribMulAction S₃ (M →SL[σ₁₂] M₂) where
   smul_add a f g := ext fun x => smul_add a (f x) (g x)
-  smul_zero _a := ext fun _x => smul_zero _
+  smul_zero a := ext fun _ => smul_zero a
 #align continuous_linear_map.distrib_mul_action ContinuousLinearMap.distribMulAction
 
 end SMulMonoid
@@ -1682,7 +1682,7 @@ theorem prod_ext {f g : M × N₂ →L[R] N₃} (hl : f.comp (inl _ _ _) = g.com
 variable [ContinuousAdd M₂] [ContinuousAdd M₃] [ContinuousAdd N₂]
 
 instance module : Module S₃ (M →SL[σ₁₃] M₃) where
-  zero_smul _ := ext fun _ => zero_smul _ _
+  zero_smul _ := ext fun _ => zero_smul S₃ _
   add_smul _ _ _ := ext fun _ => add_smul _ _ _
 #align continuous_linear_map.module ContinuousLinearMap.module
 
@@ -1738,7 +1738,7 @@ def smulRightₗ (c : M →L[R] S) : M₂ →ₗ[T] M →L[R] M₂ where
   toFun := c.smulRight
   map_add' x y := by
     ext e
-    apply smul_add
+    apply smul_add (c e)
   map_smul' a x := by
     ext e
     dsimp

Mathlib/Topology/Algebra/Ring/Basic.lean

@@ -152,6 +152,12 @@ instance [NonUnitalNonAssocRing α] [NonUnitalNonAssocRing β] [TopologicalRing
 
 end
 
+-- Adaptation note: nightly-2024-04-08, needed to help `Pi.instTopologicalSemiring`
+instance {β : Type*} {C : β → Type*} [∀ b, TopologicalSpace (C b)]
+    [∀ b, NonUnitalNonAssocSemiring (C b)] [∀ b, TopologicalSemiring (C b)] :
+    ContinuousAdd ((b : β) → C b) :=
+  inferInstance
+
 instance Pi.instTopologicalSemiring {β : Type*} {C : β → Type*} [∀ b, TopologicalSpace (C b)]
     [∀ b, NonUnitalNonAssocSemiring (C b)] [∀ b, TopologicalSemiring (C b)] :
     TopologicalSemiring (∀ b, C b) where

Mathlib/Topology/Category/Stonean/Basic.lean

@@ -219,7 +219,7 @@ instance {X Y : Stonean} (f : X ⟶ Y) [@Epi CompHaus _ _ _ f] : Epi f := by
   rwa [CompHaus.epi_iff_surjective] at *
 
 /-- Every Stonean space is projective in `CompHaus` -/
-instance (X : Stonean) : Projective X.compHaus where
+instance instProjectiveCompHausCompHaus (X : Stonean) : Projective X.compHaus where
   factors := by
     intro B C φ f _
     haveI : ExtremallyDisconnected X.compHaus.toTop := X.extrDisc
@@ -313,7 +313,7 @@ lemma Gleason (X : CompHaus.{u}) :
   · intro h
     let X' : Stonean := ⟨X⟩
     show Projective X'.compHaus
-    apply Stonean.instProjectiveCompHausCategoryCompHaus
+    apply Stonean.instProjectiveCompHausCompHaus
 
 end CompHaus
 

Mathlib/Topology/ContinuousFunction/Bounded.lean

@@ -1394,7 +1394,7 @@ instance instSMul' : SMul (α →ᵇ 𝕜) (α →ᵇ β) where
 
 instance instModule' : Module (α →ᵇ 𝕜) (α →ᵇ β) :=
   Module.ofMinimalAxioms
-      (fun _ _ _ => ext fun _ => smul_add _ _ _)
+      (fun c _ _ => ext fun a => smul_add (c a) _ _)
       (fun _ _ _ => ext fun _ => add_smul _ _ _)
       (fun _ _ _ => ext fun _ => mul_smul _ _ _)
       (fun f => ext fun x => one_smul 𝕜 (f x))

Mathlib/Topology/Instances/Real.lean

@@ -138,7 +138,7 @@ protected theorem Real.continuous_mul : Continuous fun p : ℝ × ℝ => p.1 * p
 
 -- Porting note: moved `TopologicalRing` instance up
 
-instance : CompleteSpace ℝ := by
+instance Real.instCompleteSpace : CompleteSpace ℝ := by
   apply complete_of_cauchySeq_tendsto
   intro u hu
   let c : CauSeq ℝ abs := ⟨u, Metric.cauchySeq_iff'.1 hu⟩

Mathlib/Topology/Order/ScottTopology.lean

@@ -239,7 +239,7 @@ lemma isLowerSet_of_isClosed : IsClosed s → IsLowerSet s := fun h ↦
 lemma lowerClosure_subset_closure : ↑(lowerClosure s) ⊆ closure s := by
   convert closure.mono (@upperSet_le_scott α _)
   · rw [@IsUpperSet.closure_eq_lowerClosure α _ (upperSet α) ?_ s]
-    exact instIsUpperSetUpperSet
+    infer_instance
   · exact topology_eq α
 
 lemma isClosed_Iic : IsClosed (Iic a) :=

Mathlib/Topology/Sheaves/Skyscraper.lean

@@ -228,7 +228,9 @@ theorem skyscraperPresheaf_isSheaf : (skyscraperPresheaf p₀ A).IsSheaf := by
           dsimp [skyscraperPresheaf]
           rw [if_neg]
           · exact terminalIsTerminal
-          · exact Set.not_mem_empty PUnit.unit)))
+          · -- Adaptation note: 2024-03-24
+            -- Previously the universe annotation was not needed here.
+            exact Set.not_mem_empty PUnit.unit.{u+1})))
 #align skyscraper_presheaf_is_sheaf skyscraperPresheaf_isSheaf
 
 /--

Mathlib/Topology/UniformSpace/Matrix.lean

@@ -29,8 +29,8 @@ instance instUniformAddGroup [AddGroup 𝕜] [UniformAddGroup 𝕜] :
 
 theorem uniformity :
     𝓤 (Matrix m n 𝕜) = ⨅ (i : m) (j : n), (𝓤 𝕜).comap fun a => (a.1 i j, a.2 i j) := by
-  erw [Pi.uniformity, Pi.uniformity]
-  simp_rw [Filter.comap_iInf, Filter.comap_comap]
+  erw [Pi.uniformity]
+  simp_rw [Pi.uniformity, Filter.comap_iInf, Filter.comap_comap]
   rfl
 #align matrix.uniformity Matrix.uniformity
 

docs/overview.yaml

@@ -60,7 +60,7 @@ General algebra:
 
   Ideals and quotients:
     ideal of a commutative ring: 'Ideal'
-    quotient ring: 'Ideal.instHasQuotientIdealToSemiringToCommSemiring'
+    quotient ring: 'Ideal.instHasQuotient'
     prime ideal: 'Ideal.IsPrime'
     maximal ideal: 'Ideal.IsMaximal'
     Chinese remainder theorem: 'Ideal.quotientInfRingEquivPiQuotient'
@@ -234,7 +234,7 @@ Topology:
     extreme value theorem: 'IsCompact.exists_forall_le'
     limit infimum and supremum: 'order/liminf_limsup.html'
     topological group: 'TopologicalGroup'
-    completion of an abelian topological group: 'UniformSpace.Completion.instAddCommGroupCompletion'
+    completion of an abelian topological group: 'UniformSpace.Completion.instAddCommGroup'
     infinite sum: 'HasSum'
     topological ring: 'TopologicalRing'
     completion of a topological ring: 'UniformSpace.Completion.ring'

docs/undergrad.yaml

@@ -130,7 +130,7 @@ Ring Theory:
     product of rings: 'Pi.ring'
   Ideals and Quotients:
     ideal of a commutative ring: 'Ideal'
-    quotient rings: 'Ideal.instHasQuotientIdealToSemiringToCommSemiring'
+    quotient rings: 'Ideal.instHasQuotient'
     prime ideals: 'Ideal.IsPrime'
     maximal ideals: 'Ideal.IsMaximal'
     Chinese remainder theorem: 'Ideal.quotientInfRingEquivPiQuotient'
@@ -256,7 +256,7 @@ Affine and Euclidean Geometry:
     extreme point: 'Set.extremePoints'
   Euclidean affine spaces:
     isometries of a Euclidean affine space: 'AffineIsometryEquiv'
-    group of isometries of a Euclidean affine space: 'AffineIsometryEquiv.instGroupAffineIsometryEquiv'
+    group of isometries of a Euclidean affine space: 'AffineIsometryEquiv.instGroup'
     isometries that do and do not preserve orientation: ''
     direct and opposite similarities of the plane: ''
     classification of isometries in two and three dimensions: ''
@@ -287,7 +287,7 @@ Single Variable Real Analysis:
     Cauchy sequences: 'CauchySeq'
   Topology of R:
     metric structure: 'Real.metricSpace'
-    completeness of R: 'instCompleteSpaceRealToUniformSpacePseudoMetricSpace'
+    completeness of R: 'Real.instCompleteSpace'
     Bolzano-Weierstrass theorem: 'tendsto_subseq_of_bounded'
     compact subsets of $\R$: 'Metric.isCompact_iff_isClosed_bounded'
     connected subsets of $\R$: 'setOf_isPreconnected_eq_of_ordered'

test/Simps.lean

@@ -893,7 +893,7 @@ example (x : Bool) {z} (h : id x = z) : myRingHom x = z := by
 -- set_option trace.simps.debug true
 
 @[to_additive (attr := simps) instAddProd]
-instance {M N} [Mul M] [Mul N] : Mul (M × N) := ⟨fun p q ↦ ⟨p.1 * q.1, p.2 * q.2⟩⟩
+instance instMulProd {M N} [Mul M] [Mul N] : Mul (M × N) := ⟨fun p q ↦ ⟨p.1 * q.1, p.2 * q.2⟩⟩
 
 run_cmd liftTermElabM <| do
   let env ← getEnv

test/ValuedCSP.lean

@@ -26,7 +26,7 @@ def ValuedCSP.binaryTerm {D C : Type} [OrderedAddCommMonoid C]
 -- ## Example: minimize `|x| + |y|` where `x` and `y` are rational numbers
 
 private def absRat : (Fin 1 → ℚ) → ℚ :=
-  Function.OfArity.uncurry (@abs ℚ Rat.instLatticeRat Rat.addGroup)
+  Function.OfArity.uncurry (@abs ℚ Rat.instLattice Rat.addGroup)
 
 private def exampleAbs : Σ (n : ℕ), (Fin n → ℚ) → ℚ := ⟨1, absRat⟩
 

test/byContra.lean

@@ -26,12 +26,12 @@ example : 1 < 2 := by
   guard_hyp this : 2 ≤ 1
   contradiction
 
-example (p : Prop) (bar : False) : ¬ ¬ ¬ ¬ ¬ ¬ P := by
+example (_p : Prop) (bar : False) : ¬ ¬ ¬ ¬ ¬ ¬ P := by
   by_contra! foo : ¬ ¬ ¬ P -- normalises to ¬ P, as does ¬ (goal).
   guard_hyp foo : ¬ ¬ ¬ P
   exact bar
 
-example (p : Prop) (bar : False) : ¬ ¬ ¬ ¬ ¬ ¬ P := by
+example (_p : Prop) (bar : False) : ¬ ¬ ¬ ¬ ¬ ¬ P := by
   by_contra! : ¬ ¬ ¬ P
   guard_hyp this : ¬ ¬ ¬ P
   exact bar