fixes for leanprover/lean4#6558

leanprover-community · Jan 8, 2025 · c2cc119 · c2cc119
1 parent 3a56ccf
commit c2cc119
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 7 deletions.
diff --git a/Mathlib/CategoryTheory/Bicategory/Coherence.lean b/Mathlib/CategoryTheory/Bicategory/Coherence.lean
@@ -129,7 +129,7 @@ def normalizeIso {a : B} :
     ∀ {b c : B} (p : Path a b) (f : Hom b c),
       (preinclusion B).map ⟨p⟩ ≫ f ≅ (preinclusion B).map ⟨normalizeAux p f⟩
   | _, _, _, Hom.of _ => Iso.refl _
-  | _, _, _, Hom.id b => ρ_ _
+  | _, _, _, Hom.id _ => ρ_ _
   | _, _, p, Hom.comp f g =>
     (α_ _ _ _).symm ≪≫ whiskerRightIso (normalizeIso p f) g ≪≫ normalizeIso (normalizeAux p f) g
 

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean b/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
@@ -67,7 +67,7 @@ instance {a : WalkingMulticospan fst snd} : Inhabited (Hom a a) :=
 
 /-- Composition of morphisms for `WalkingMulticospan`. -/
 def Hom.comp : ∀ {A B C : WalkingMulticospan fst snd} (_ : Hom A B) (_ : Hom B C), Hom A C
-  | _, _, _, Hom.id X, f => f
+  | _, _, _, Hom.id _, f => f
   | _, _, _, Hom.fst b, Hom.id _ => Hom.fst b
   | _, _, _, Hom.snd b, Hom.id _ => Hom.snd b
 
@@ -114,7 +114,7 @@ instance {a : WalkingMultispan fst snd} : Inhabited (Hom a a) :=
 
 /-- Composition of morphisms for `WalkingMultispan`. -/
 def Hom.comp : ∀ {A B C : WalkingMultispan fst snd} (_ : Hom A B) (_ : Hom B C), Hom A C
-  | _, _, _, Hom.id X, f => f
+  | _, _, _, Hom.id _, f => f
   | _, _, _, Hom.fst a, Hom.id _ => Hom.fst a
   | _, _, _, Hom.snd a, Hom.id _ => Hom.snd a
 

diff --git a/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean b/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
@@ -421,7 +421,7 @@ variable (J)
 def widePullbackShapeOpMap :
     ∀ X Y : WidePullbackShape J,
       (X ⟶ Y) → ((op X : (WidePushoutShape J)ᵒᵖ) ⟶ (op Y : (WidePushoutShape J)ᵒᵖ))
-  | _, _, WidePullbackShape.Hom.id X => Quiver.Hom.op (WidePushoutShape.Hom.id _)
+  | _, _, WidePullbackShape.Hom.id _ => Quiver.Hom.op (WidePushoutShape.Hom.id _)
   | _, _, WidePullbackShape.Hom.term _ => Quiver.Hom.op (WidePushoutShape.Hom.init _)
 
 /-- The obvious functor `WidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ` -/
@@ -435,7 +435,7 @@ def widePullbackShapeOp : WidePullbackShape J ⥤ (WidePushoutShape J)ᵒᵖ whe
 def widePushoutShapeOpMap :
     ∀ X Y : WidePushoutShape J,
       (X ⟶ Y) → ((op X : (WidePullbackShape J)ᵒᵖ) ⟶ (op Y : (WidePullbackShape J)ᵒᵖ))
-  | _, _, WidePushoutShape.Hom.id X => Quiver.Hom.op (WidePullbackShape.Hom.id _)
+  | _, _, WidePushoutShape.Hom.id _ => Quiver.Hom.op (WidePullbackShape.Hom.id _)
   | _, _, WidePushoutShape.Hom.init _ => Quiver.Hom.op (WidePullbackShape.Hom.term _)
 
 /-- The obvious functor `WidePushoutShape J ⥤ (WidePullbackShape J)ᵒᵖ` -/

diff --git a/Mathlib/Data/List/Basic.lean b/Mathlib/Data/List/Basic.lean
@@ -644,8 +644,8 @@ instance decidableSublist [DecidableEq α] : ∀ l₁ l₂ : List α, Decidable
       @decidable_of_decidable_of_iff _ _ (decidableSublist (a :: l₁) l₂)
         ⟨sublist_cons_of_sublist _, fun s =>
           match a, l₁, s, h with
-          | _, _, Sublist.cons _ s', h => s'
-          | _, _, Sublist.cons₂ t _, h => absurd rfl h⟩
+          | _, _, Sublist.cons _ s', _ => s'
+          | _, _, Sublist.cons₂ _ _, h => absurd rfl h⟩
 
 /-- If the first element of two lists are different, then a sublist relation can be reduced. -/
 theorem Sublist.of_cons_of_ne {a b} (h₁ : a ≠ b) (h₂ : a :: l₁ <+ b :: l₂) : a :: l₁ <+ l₂ :=