[pre-commit.ci lite] apply automatic fixes

Author: pre-commit-ci-lite[bot]

Mathlib/xclip

@@ -3,25 +3,25 @@ index f256701817..21cb5732e6 100644
 --- a/Mathlib/CategoryTheory/Closed/PowerObjects.lean
 +++ b/Mathlib/CategoryTheory/Closed/PowerObjects.lean
 @@ -25,35 +25,43 @@ variable {ℰ : Type u} [Category.{v} ℰ]
- 
+
  namespace LeftRepresentable
- 
+
 -variable {F : ℰᵒᵖ × ℰᵒᵖ ⥤ Type (max u v)}
 +variable (F : (ℰ × ℰ)ᵒᵖ ⥤ Type (max u v))
- 
+
 -variable {B PB : ℰ} (hPB : ((curryObj F).obj (op B)).RepresentableBy PB)
 -  {C PC : ℰ} (hPC : ((curryObj F).obj (op C)).RepresentableBy PC)
 +def curryObj' : ℰᵒᵖ ⥤ ℰᵒᵖ ⥤ Type (max u v) := curryObj ((prodOpEquiv ℰ).inverse ⋙ F)
 +
 +variable {F} {B PB : ℰ} (hPB : ((curryObj' F).obj (op B)).RepresentableBy PB)
 +  {C PC : ℰ} (hPC : ((curryObj' F).obj (op C)).RepresentableBy PC)
- 
+
  /-- The morphism induced by a morphism between the base objects. -/
 -def map (h : B ⟶ C) : PC ⟶ PB :=
 -  hPB.homEquiv.symm (F.map (h.op ×ₘ 𝟙 (op PC)) (hPC.homEquiv (𝟙 PC)))
 +def Pmap (h : B ⟶ C) : PC ⟶ PB :=
 +  hPB.homEquiv.symm (F.map (h ×ₘ 𝟙 PC).op (hPC.homEquiv (𝟙 PC)))
- 
+
  lemma map_universal (h : B ⟶ C) :
 -  F.map (𝟙 (op B) ×ₘ (map hPB hPC h).op) (hPB.homEquiv (𝟙 PB))
 -    = F.map (h.op ×ₘ 𝟙 (op PC)) (hPC.homEquiv (𝟙 PC)) := by
@@ -36,12 +36,12 @@ index f256701817..21cb5732e6 100644
 +      rw [← hPB.homEquiv_eq, Pmap, hPB.homEquiv.apply_symm_apply]
 +
 +variable {D PD : ℰ} (hPD : ((curryObj' F).obj (op D)).RepresentableBy PD)
- 
+
 -variable {D PD : ℰ} (hPD : ((curryObj F).obj (op D)).RepresentableBy PD)
 +lemma comm {PB PC : ℰ} (f : B ⟶ C) (Pf : PC ⟶ PB) :
 +    (f ×ₘ 𝟙 PB).op ≫ (𝟙 B ×ₘ Pf).op = (𝟙 C ×ₘ Pf).op ≫ (f ×ₘ 𝟙 PC).op :=
 +  congrArg Quiver.Hom.op (by simp)
- 
+
  lemma compose (h : B ⟶ C) (h' : C ⟶ D) :
 -    map hPB hPD (h ≫ h') = map hPC hPD h' ≫ map hPB hPC h := by
 -  let Ph := map hPB hPC h