Some fixes

leanprover-community · Aug 16, 2024 · 54a6616 · 54a6616
1 parent 9c41f64
commit 54a6616
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 11 deletions.
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Normalized.lean b/Mathlib/AlgebraicTopology/DoldKan/Normalized.lean
@@ -124,10 +124,13 @@ def N₁_iso_normalizedMooreComplex_comp_toKaroubi : N₁ ≅ normalizedMooreCom
           comm := by erw [inclusionOfMooreComplexMap_comp_PInfty, id_comp] }
       naturality := fun X Y f => by
         ext
-        simp only [Functor.comp_map, normalizedMooreComplex_map, Karoubi.comp_f, toKaroubi_map_f,
-          HomologicalComplex.comp_f, NormalizedMooreComplex.map_f,
-          inclusionOfMooreComplexMap_f, factorThru_arrow, N₁_map_f,
-          inclusionOfMooreComplexMap_comp_PInfty_assoc, AlternatingFaceMapComplex.map_f] }
+        simp only [Functor.comp_obj, normalizedMooreComplex_obj, toKaroubi_obj_X,
+          NormalizedMooreComplex.obj_X, N₁_obj_X, AlternatingFaceMapComplex.obj_X, Functor.comp_map,
+          normalizedMooreComplex_map, Karoubi.comp_f, toKaroubi_map_f, HomologicalComplex.comp_f,
+          NormalizedMooreComplex.map_f, inclusionOfMooreComplexMap_f, NormalizedMooreComplex.objX,
+          factorThru_arrow, N₁_map_f, inclusionOfMooreComplexMap_comp_PInfty_assoc,
+          AlternatingFaceMapComplex.map_f]
+         }
   hom_inv_id := by
     ext X : 3
     simp only [PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap,

diff --git a/Mathlib/Data/PFunctor/Univariate/M.lean b/Mathlib/Data/PFunctor/Univariate/M.lean
@@ -281,9 +281,7 @@ theorem mk_dest (x : M F) : M.mk (dest x) = x := by
   cases' h : x.approx (succ n) with _ hd ch
   have h' : hd = head' (x.approx 1) := by
     rw [← head_succ' n, h, head']
-    · split
-      injections
-    · apply x.consistent
+    apply x.consistent
   revert ch
   rw [h']
   intros ch h

diff --git a/Mathlib/RingTheory/Binomial.lean b/Mathlib/RingTheory/Binomial.lean
@@ -241,7 +241,7 @@ instance Int.instBinomialRing : BinomialRing ℤ where
   nsmul_right_injective n hn r s hrs := Int.eq_of_mul_eq_mul_left (Int.ofNat_ne_zero.mpr hn) hrs
   multichoose := Int.multichoose
   factorial_nsmul_multichoose r k := by
-    rw [Int.multichoose, nsmul_eq_mul]
+    rw [Int.multichoose.eq_def, nsmul_eq_mul]
     cases r with
     | ofNat n =>
       simp only [multichoose, nsmul_eq_mul, Int.ofNat_eq_coe, Int.ofNat_mul_out]

diff --git a/Mathlib/Topology/UniformSpace/CompactConvergence.lean b/Mathlib/Topology/UniformSpace/CompactConvergence.lean
@@ -330,7 +330,7 @@ theorem uniformSpace_eq_inf_precomp_of_cover {δ₁ δ₂ : Type*} [TopologicalS
   have h_preimage₂ : MapsTo (φ₂ ⁻¹' ·) 𝔖 𝔗₂ := fun K ↦ h_proper₂.isCompact_preimage
   have h_cover' : ∀ S ∈ 𝔖, S ⊆ range φ₁ ∪ range φ₂ := fun S _ ↦ h_cover ▸ subset_univ _
   -- ... and we just pull it back.
-  simp_rw [compactConvergenceUniformSpace, replaceTopology_eq, inferInstanceAs, inferInstance,
+  simp_rw [compactConvergenceUniformSpace, replaceTopology_eq,
     UniformOnFun.uniformSpace_eq_inf_precomp_of_cover _ _ _ _ _
       h_image₁ h_image₂ h_preimage₁ h_preimage₂ h_cover',
     UniformSpace.comap_inf, ← UniformSpace.comap_comap]
@@ -351,7 +351,7 @@ theorem uniformSpace_eq_iInf_precomp_of_cover {δ : ι → Type*} [∀ i, Topolo
       inter_eq_right.mp ?_⟩
     simp_rw [iUnion₂_inter, mem_setOf, iUnion_nonempty_self, ← iUnion_inter, h_cover, univ_inter]
   -- ... and we just pull it back.
-  simp_rw [compactConvergenceUniformSpace, replaceTopology_eq, inferInstanceAs, inferInstance,
+  simp_rw [compactConvergenceUniformSpace, replaceTopology_eq,
     UniformOnFun.uniformSpace_eq_iInf_precomp_of_cover _ _ _ h_image h_preimage h_cover',
     UniformSpace.comap_iInf, ← UniformSpace.comap_comap]
   rfl

diff --git a/Mathlib/Topology/VectorBundle/Basic.lean b/Mathlib/Topology/VectorBundle/Basic.lean
@@ -559,7 +559,7 @@ instance moduleFiber (x : B) : Module R (Z.Fiber x) :=
   inferInstanceAs (Module R F)
 
 /-- The projection from the total space of a fiber bundle core, on its base. -/
-@[reducible, simp, mfld_simps]
+@[reducible]
 protected def proj : TotalSpace F Z.Fiber → B :=
   TotalSpace.proj