mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Closed.Ideal

Goal state before:
pp: case comm1.refine_2
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
i : D ⥤ C
inst✝⁴ : CartesianMonoidalCategory C
inst✝³ : Reflective i
inst✝² : MonoidalClosed C
inst✝¹ : CartesianMonoidalCategory D
inst✝ : ExponentialIdeal i
l : i.EssImageSubcategory ⥤ D
φ : l ⋙ i ≅ i.essImage.ι
B X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ i.map (B ◁ f) ≫ prodComparison i B Y✝ = prodComparison i B X✝ ≫ i.obj B ◁ i.map f

Tactic:
rw [prodComparison_natural_whiskerLeft]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution.Closed

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
inst✝ : MonoidalClosed V
F G H : C ⥤ V
ℌ : DayConvolutionInternalHom F G H
G' H' : C ⥤ V
f✝ : G ⟶ G'
ℌ' : DayConvolutionInternalHom F G' H'
c c' : C
f : c ⟶ c'
⊢ H.map f ≫
      Wedge.IsLimit.lift (ℌ'.isLimitWedge c')
        (fun j ↦ ℌ.π c' j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c').app (op j)).app j) ⋯ =
    Wedge.IsLimit.lift (ℌ'.isLimitWedge c)
        (fun j ↦ ℌ.π c j ≫ ((((dayConvolutionInternalHomDiagramFunctor F).map f✝).app c).app (op j)).app j) ⋯ ≫
      H'.map f

Tactic:
by
    apply Wedge.IsLimit.hom_ext (ℌ'.isLimitWedge c')
    intro j
    dsimp
    simp only [Category.assoc, map_comp_π]
    rw [← Wedge.mk_ι
        (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c')
        (H'.obj c') (ℌ'.π c') (ℌ'.hπ c'),
      ← Wedge.mk_ι
        (F := dayConvolutionInternalHomDiagramFunctor F |>.obj _ |>.obj c)
        (H'.obj c) (ℌ'.π c) (ℌ'.hπ c),
      Wedge.IsLimit.lift_ι (ℌ'.isLimitWedge c'),
      Wedge.IsLimit.lift_ι_assoc (ℌ'.isLimitWedge c)]
    simp [← Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| R.X ◁
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
        ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft) ≫
    TensorBimod.actLeft (P.tensorBimod Q) L

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| coequalizer.desc
    ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫
      coequalizer.desc
        ((α_ P.X Q.X L.X).hom ≫
          P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
            coequalizer.π (P.actRight ▷ TensorBimod.X Q L)
              ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L))
        ⋯)
    ⋯

Tactic:
rw [TensorBimod.whiskerLeft_π_actLeft]

Goal state after:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| (α_ R.X (P.tensorBimod Q).X L.X).inv ≫
    (P.tensorBimod Q).actLeft ▷ L.X ≫
      coequalizer.π ((P.tensorBimod Q).actRight ▷ L.X)
        ((α_ (P.tensorBimod Q).X T.X L.X).hom ≫ (P.tensorBimod Q).X ◁ L.actLeft)

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
R S T U : Mon C
P : Bimod R S
Q : Bimod S T
L : Bimod T U
| coequalizer.desc
    ((PreservesCoequalizer.iso (tensorRight L.X) (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)).inv ≫
      coequalizer.desc
        ((α_ P.X Q.X L.X).hom ≫
          P.X ◁ coequalizer.π (Q.actRight ▷ L.X) ((α_ Q.X T.X L.X).hom ≫ Q.X ◁ L.actLeft) ≫
            coequalizer.π (P.actRight ▷ TensorBimod.X Q L)
              ((α_ P.X S.X (TensorBimod.X Q L)).hom ≫ P.X ◁ TensorBimod.actLeft Q L))
        ⋯)
    ⋯
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫ 𝒮 ▷ A ≫ Δ ▷ A ≫ (α_ A A A).hom ≫ A ◁ A ◁ Δ ≫ (α_ A A (A ⊗ A)).inv ≫ tensorμ A A A A ≫ (μ ⊗ₘ μ) =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
simp only [tensorμ]

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      𝒮 ▷ A ≫
        Δ ▷ A ≫
          (α_ A A A).hom ≫
            A ◁ A ◁ Δ ≫
              (α_ A A (A ⊗ A)).inv ≫
                ((α_ A A (A ⊗ A)).hom ≫
                    A ◁ (α_ A A A).inv ≫ A ◁ (β_ A A).hom ▷ A ≫ A ◁ (α_ A A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫
                  (μ ⊗ₘ μ) =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      Δ ▷ A ≫
        (α_ A A A).hom ≫
          A ◁ A ◁ Δ ≫ A ◁ A ◁ (β_ A A).hom ≫ A ◁ A ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ A A (A ⊗ A)).inv ≫ tensorμ A A A A ≫ (μ ⊗ₘ μ) =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)

Tactic:
simp only [tensorμ]

Goal state after:
case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ Δ ≫
      Δ ▷ A ≫
        (α_ A A A).hom ≫
          A ◁ A ◁ Δ ≫
            A ◁ A ◁ (β_ A A).hom ≫
              A ◁ A ◁ (𝒮 ⊗ₘ 𝒮) ≫
                (α_ A A (A ⊗ A)).inv ≫
                  ((α_ A A (A ⊗ A)).hom ≫
                      A ◁ (α_ A A A).inv ≫ A ◁ (β_ A A).hom ▷ A ≫ A ◁ (α_ A A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫
                    (μ ⊗ₘ μ) =
    ε ≫ (λ_ (𝟙_ C)).inv ≫ (η ⊗ₘ η)
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫ tensorμ A A A A ≫ (α_ (A ⊗ A) A A).inv ≫ μ ▷ A ▷ A ≫ 𝒮 ▷ A ▷ A ≫ (α_ A A A).hom ≫ A ◁ μ ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
simp only [tensorμ]

Goal state after:
case hba
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      ((α_ A A (A ⊗ A)).hom ≫ A ◁ (α_ A A A).inv ≫ A ◁ (β_ A A).hom ▷ A ≫ A ◁ (α_ A A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫
        (α_ (A ⊗ A) A A).inv ≫ μ ▷ A ▷ A ≫ 𝒮 ▷ A ▷ A ≫ (α_ A A A).hom ≫ A ◁ μ ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      tensorμ A A A A ≫
        (α_ (A ⊗ A) A A).inv ≫ μ ▷ A ▷ A ≫ (α_ A A A).hom ≫ A ◁ (β_ A A).hom ≫ A ◁ (𝒮 ⊗ₘ 𝒮) ≫ A ◁ μ ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
simp only [tensorμ]

Goal state after:
case hac
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ⊗ₘ Δ) ≫
      ((α_ A A (A ⊗ A)).hom ≫ A ◁ (α_ A A A).inv ≫ A ◁ (β_ A A).hom ▷ A ≫ A ◁ (α_ A A A).hom ≫ (α_ A A (A ⊗ A)).inv) ≫
        (α_ (A ⊗ A) A A).inv ≫ μ ▷ A ▷ A ≫ (α_ A A A).hom ≫ A ◁ (β_ A A).hom ≫ A ◁ (𝒮 ⊗ₘ 𝒮) ≫ A ◁ μ ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
V : Type u₂
inst✝³ : Category.{v₂, u₂} V
inst✝² : MonoidalCategory C
inst✝¹ : MonoidalCategory V
F G : C ⥤ V
inst✝ : DayConvolution F G
⊢ ∀ {Y Y' : C ⥤ V} (g : Y ⟶ Y') (f : F ⊛ G ⟶ Y),
    ((F ⊛ G).homEquivOfIsLeftKanExtension (unit F G) Y') (f ≫ g) =
      (ConcreteCategory.hom
          (((Functor.whiskeringLeft (C × C) C V).obj (tensor C) ⋙ coyoneda.obj (Opposite.op (F ⊠ G))).map g))
        (((F ⊛ G).homEquivOfIsLeftKanExtension (unit F G) Y) f)

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
F G : C ⥤ V
inst✝⁵ : DayConvolution F G
H : C ⥤ V
inst✝⁴ : DayConvolution G H
inst✝³ : DayConvolution F (G ⊛ H)
inst✝² : DayConvolution (F ⊛ G) H
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
⊢ ∀ {Y Y' : C ⥤ V} (g : Y ⟶ Y') (f : F ⊛ G ⊛ H ⟶ Y),
    ((corepresentableBy F (G ⊛ H)).homEquiv.trans
          ((F ⊠ G ⊛ H).homEquivOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F)
            (((whiskeringLeft (C × C) C V).obj (tensor C)).obj Y')))
        (f ≫ g) =
      (ConcreteCategory.hom
          (((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                (whiskeringLeft (C × C × C) (C × C) V).obj ((𝟭 C).prod (tensor C)) ⋙
                  coyoneda.obj (Opposite.op (F ⊠ G ⊠ H))).map
            g))
        (((corepresentableBy F (G ⊛ H)).homEquiv.trans
            ((F ⊠ G ⊛ H).homEquivOfIsLeftKanExtension (extensionUnitRight (G ⊛ H) (unit G H) F)
              (((whiskeringLeft (C × C) C V).obj (tensor C)).obj Y)))
          f)

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
F G : C ⥤ V
inst✝⁵ : DayConvolution F G
H : C ⥤ V
inst✝⁴ : DayConvolution G H
inst✝³ : DayConvolution F (G ⊛ H)
inst✝² : DayConvolution (F ⊛ G) H
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
⊢ ∀ {Y Y' : C ⥤ V} (g : Y ⟶ Y') (f : (F ⊛ G) ⊛ H ⟶ Y),
    ((corepresentableBy (F ⊛ G) H).homEquiv.trans
          (((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
            (((whiskeringLeft (C × C) C V).obj (tensor C)).obj Y')))
        (f ≫ g) =
      (ConcreteCategory.hom
          (((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                (whiskeringLeft ((C × C) × C) (C × C) V).obj ((tensor C).prod (𝟭 C)) ⋙
                  coyoneda.obj (Opposite.op ((F ⊠ G) ⊠ H))).map
            g))
        (((corepresentableBy (F ⊛ G) H).homEquiv.trans
            (((F ⊛ G) ⊠ H).homEquivOfIsLeftKanExtension (extensionUnitLeft (F ⊛ G) (unit F G) H)
              (((whiskeringLeft (C × C) C V).obj (tensor C)).obj Y)))
          f)

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalCategory V
U : C ⥤ V
inst✝³ : DayConvolutionUnit U
F : C ⥤ V
inst✝² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution U F
⊢ ∀ {Y Y' : C ⥤ V} (g : Y ⟶ Y') (f : U ⊛ F ⟶ Y),
    (((U ⊛ F).homEquivOfIsLeftKanExtension (DayConvolution.unit U F) Y').trans
          ((U ⊠ F).homEquivOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ Y')))
        (f ≫ g) =
      (ConcreteCategory.hom
          (((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                (whiskeringLeft (Discrete PUnit.{1} × C) (C × C) V).obj ((fromPUnit (𝟙_ C)).prod (𝟭 C)) ⋙
                  coyoneda.obj (Opposite.op (fromPUnit (𝟙_ V) ⊠ F))).map
            g))
        ((((U ⊛ F).homEquivOfIsLeftKanExtension (DayConvolution.unit U F) Y).trans
            ((U ⊠ F).homEquivOfIsLeftKanExtension (extensionUnitLeft U (φ U) F) (tensor C ⋙ Y)))
          f)

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C : Type u₁
inst✝⁷ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁶ : Category.{v₂, u₂} V
inst✝⁵ : MonoidalCategory C
inst✝⁴ : MonoidalCategory V
U : C ⥤ V
inst✝³ : DayConvolutionUnit U
F : C ⥤ V
inst✝² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorLeft v)
inst✝¹ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ : DayConvolution F U
⊢ ∀ {Y Y' : C ⥤ V} (g : Y ⟶ Y') (f : F ⊛ U ⟶ Y),
    (((F ⊛ U).homEquivOfIsLeftKanExtension (DayConvolution.unit F U) Y').trans
          ((F ⊠ U).homEquivOfIsLeftKanExtension (extensionUnitRight U (φ U) F) (tensor C ⋙ Y')))
        (f ≫ g) =
      (ConcreteCategory.hom
          (((whiskeringLeft (C × C) C V).obj (tensor C) ⋙
                (whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V).obj ((𝟭 C).prod (fromPUnit (𝟙_ C))) ⋙
                  coyoneda.obj (Opposite.op (F ⊠ fromPUnit (𝟙_ V)))).map
            g))
        ((((F ⊛ U).homEquivOfIsLeftKanExtension (DayConvolution.unit F U) Y).trans
            ((F ⊠ U).homEquivOfIsLeftKanExtension (extensionUnitRight U (φ U) F) (tensor C ⋙ Y)))
          f)

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : MonObj A
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := A.map (f ≫ g), isMonHom_hom := ⋯ } =
    { hom := A.map f, isMonHom_hom := ⋯ } ≫ { hom := A.map g, isMonHom_hom := ⋯ }

Tactic:
ext; dsimp; rw [Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : MonoidalCategory D
A : C ⥤ D
inst✝ : ComonObj A
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { hom := A.map (f ≫ g), isComonHom_hom := ⋯ } =
    { hom := A.map f, isComonHom_hom := ⋯ } ≫ { hom := A.map g, isComonHom_hom := ⋯ }

Tactic:
ext; dsimp; rw [Functor.map_comp]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Ind

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : P.RespectsIso
X Y Z : C
i : Y ⟶ Z
hi : IsIso i
f : X ⟶ Y
x✝ : P.ind f
J : Type u_1
w✝¹ : SmallCategory J
w✝ : IsFiltered J
D : J ⥤ C
t : (Functor.const J).obj X ⟶ D
s : D ⟶ (Functor.const J).obj Y
hs : IsColimit { pt := Y, ι := s }
hst : ∀ (j : J), P (t.app j) ∧ t.app j ≫ s.app j = f
⊢ P.ind (f ≫ i)

Tactic:
refine ⟨J, ‹_›, ‹_›, D, t, s ≫ (Functor.const J).map i, ?_, fun j ↦ ⟨(hst j).1, ?_⟩⟩
    · exact (IsColimit.equivIsoColimit (Cocone.ext (asIso i))) hs
    · simp [reassoc_of% (hst j).2]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.DayConvolution

Goal state before:
pp: C✝ : Type u₁
inst✝¹³ : Category.{v₁, u₁} C✝
V✝ : Type u₂
inst✝¹² : Category.{v₂, u₂} V✝
inst✝¹¹ : MonoidalCategory C✝
inst✝¹⁰ : MonoidalCategory V✝
C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
V : Type u₂
inst✝⁸ : Category.{v₂, u₂} V
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalCategory V
D : Type u₃
inst✝⁵ : Category.{v₃, u₃} D
inst✝⁴ : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D
inst✝³ : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)
inst✝² : ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)
inst✝¹ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorRight v)
inst✝ :
  ∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (𝟙_ C)) d) (tensorLeft v)
this : MonoidalCategoryStruct D := mkMonoidalCategoryStruct C V D
x✝¹ : D
x✝ : C
⊢ DayConvolutionUnit.can ▷ ((ι C V D).obj x✝¹).obj x✝ ≫
      (DayConvolution.unit ((ι C V D).obj (𝟙_ D)) ((ι C V D).obj x✝¹)).app (𝟙_ C, x✝) ≫
        ((ι C V D).map (λ_ x✝¹).hom).app (𝟙_ C ⊗ x✝) =
    (λ_ (((ι C V D).obj x✝¹).obj x✝)).hom ≫ ((ι C V D).obj x✝¹).map (λ_ x✝).inv

Tactic:
by
      simp only [Functor.comp_obj, tensor_obj, leftUnitor,
        Functor.FullyFaithful.preimageIso_hom, Functor.FullyFaithful.map_preimage]
      apply DayConvolutionUnit.leftUnitor_hom_unit_app

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.SiteLocal

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
K : Precoverage C
inst✝ : P.IsClosedUnderIsomorphisms
H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)
X : C
R : Presieve X
hR : R ∈ K.coverings X
Y : C
f : Y ⟶ X
hf : R f
hX : P X
⊢ P Y

Tactic:
by
    rw [CategoryTheory.Precoverage.mem_iff_exists_zeroHypercover] at hR
    obtain ⟨𝒰, rfl⟩ := hR
    rw [H 𝒰] at hX
    obtain ⟨i⟩ := hf
    exact hX i

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := (x✝¹ + 1) • x✝.left, right := (x✝¹ + 1) • x✝.right, w := ⋯ } =
    { left := x✝¹ • x✝.left, right := x✝¹ • x✝.right, w := ⋯ } + x✝

Tactic:
ext <;> dsimp

Goal state after:
case h₁
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ (x✝¹ + 1) • x✝.left = x✝¹ • x✝.left + x✝.left

case h₂
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ (x✝¹ + 1) • x✝.right = x✝¹ • x✝.right + x✝.right
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := ↑x✝¹.succ • x✝.left, right := ↑x✝¹.succ • x✝.right, w := ⋯ } =
    { left := ↑x✝¹ • x✝.left, right := ↑x✝¹ • x✝.right, w := ⋯ } + x✝

Tactic:
ext <;> dsimp

Goal state after:
case h₁
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ (↑x✝¹ + 1) • x✝.left = ↑x✝¹ • x✝.left + x✝.left

case h₂
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ (↑x✝¹ + 1) • x✝.right = ↑x✝¹ • x✝.right + x✝.right
Module: Mathlib.CategoryTheory.Preadditive.Comma

Goal state before:
pp: A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ { left := Int.negSucc x✝¹ • x✝.left, right := Int.negSucc x✝¹ • x✝.right, w := ⋯ } =
    -{ left := ↑x✝¹.succ • x✝.left, right := ↑x✝¹.succ • x✝.right, w := ⋯ }

Tactic:
ext <;> dsimp

Goal state after:
case h₁
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ Int.negSucc x✝¹ • x✝.left = -((↑x✝¹ + 1) • x✝.left)

case h₂
A : Type u₁
inst✝⁷ : Category.{v₁, u₁} A
inst✝⁶ : Preadditive A
B : Type u₂
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Preadditive B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
inst✝² : Preadditive T
L : A ⥤ T
inst✝¹ : L.Additive
R : B ⥤ T
inst✝ : R.Additive
u v : Comma L R
x✝¹ : ℕ
x✝ : u ⟶ v
⊢ Int.negSucc x✝¹ • x✝.right = -((↑x✝¹ + 1) • x✝.right)
Module: Mathlib.CategoryTheory.Preadditive.OfBiproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
X Y : C
h₂ : ∀ (f : X ⟶ Y), biprod.desc 0 f = biprod.snd ≫ f
h₁ : ∀ (f : X ⟶ Y), biprod.desc f 0 = biprod.fst ≫ f
f : X ⟶ Y
⊢ rightAdd X Y 0 f = f

Tactic:
simp [h₂ f, rightAdd, biprod.lift_snd_assoc, Category.id_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Schur

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : IsAlgClosed 𝕜
inst✝ : Linear 𝕜 C
X : C
isIso_iff_nonzero : ∀ (f : X ⟶ X), IsIso f ↔ f ≠ 0
I : FiniteDimensional 𝕜 (X ⟶ X)
⊢ finrank 𝕜 (X ⟶ X) = 1

Tactic:
by
  have id_nonzero := (isIso_iff_nonzero (𝟙 X)).mp (by infer_instance)
  refine finrank_eq_one (𝟙 X) id_nonzero ?_
  intro f
  have : Nontrivial (End X) := nontrivial_of_ne _ _ id_nonzero
  have : FiniteDimensional 𝕜 (End X) := I
  obtain ⟨c, nu⟩ := spectrum.nonempty_of_isAlgClosed_of_finiteDimensional 𝕜 (End.of f)
  use c
  rw [spectrum.mem_iff, IsUnit.sub_iff, isUnit_iff_isIso, isIso_iff_nonzero, Ne,
    Classical.not_not, sub_eq_zero, Algebra.algebraMap_eq_smul_one] at nu
  exact nu.symm

Goal state after: