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

Goal state before:
pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ (ρ_ A).hom ≫ μ

pp: case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

pp: case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (A ◁ 𝒮) ▷ A

pp: case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

pp: case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ ε

Tactic:
whiskerLeft_rightUnitor,

Goal state after:
case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| ((α_ A A (𝟙_ C)).inv ≫ (ρ_ (A ⊗ A)).hom) ≫ μ

case a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| Δ ▷ A

case a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (A ◁ 𝒮) ▷ A

case a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| (α_ A A A).hom

case a.a.a.a
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
| A ◁ A ◁ ε
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)).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 ≫ η

Tactic:
simp only [Category.assoc, pentagon_hom_inv_inv_inv_inv_assoc]

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).inv ≫ (α_ A A A).inv ▷ A ≫ μ ▷ 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
⊢ Δ ≫ μ ▷ (A ⊗ A) ≫ A ◁ ((𝒮 ⊗ₘ 𝒮) ≫ (β_ A A).hom ≫ μ) ≫ μ = ε ≫ η

Tactic:
simp only [Comon.tensorObj_comul, whiskerRight_tensor,
      BraidedCategory.braiding_naturality_assoc, whiskerLeft_comp, Category.assoc,
      Comon.tensorObj_counit]

Goal state after:
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 ≫ η
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).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 ≫ η

Tactic:
simp only [Category.assoc, pentagon_hom_inv_inv_inv_inv_assoc]

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).inv ≫
              (α_ A A A).inv ▷ A ≫ μ ▷ A ▷ A ≫ (α_ A A A).hom ≫ A ◁ (β_ A A).hom ≫ A ◁ (𝒮 ⊗ₘ 𝒮) ≫ A ◁ μ ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R ↑A)) (of R ↑A) ≫ ↟(mul' R ↑A)))
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x) =
    (Hom.hom (MonoidalCategoryStruct.leftUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x)

Tactic:
hom_comp,

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)) ∘ₗ Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(Algebra.linearMap R ↑A)) (of R ↑A)))
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x) =
    (Hom.hom (MonoidalCategoryStruct.leftUnitor (of R ↑A)).hom)
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorUnit (ModuleCat R)) ↑(of R ↑A)) 1) x)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ ((((TensorProduct.mk R ↑(of R ↑A) ↑(of R ↑A)).compr₂ₛₗ
            ((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑(of R ↑A)).compr₂ₛₗ
              (Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A) ≫ ↟(mul' R ↑A)))))
          x)
        y)
      z =
    ((((TensorProduct.mk R ↑(of R ↑A) ↑(of R ↑A)).compr₂ₛₗ
            ((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑(of R ↑A)).compr₂ₛₗ
              (Hom.hom
                ((MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom ≫
                  MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A)) ≫ ↟(mul' R ↑A)))))
          x)
        y)
      z

Tactic:
dsimp only [compr₂ₛₗ_apply, TensorProduct.mk_apply]

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A) ≫ ↟(mul' R ↑A)))
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z) =
    (Hom.hom
        ((MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom ≫
          MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A)) ≫ ↟(mul' R ↑A)))
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A) ≫ ↟(mul' R ↑A)))
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z) =
    (Hom.hom
        ((MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom ≫
          MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A)) ≫ ↟(mul' R ↑A)))
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)

Tactic:
hom_comp,

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)) ∘ₗ Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A)))
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z) =
    (Hom.hom
        ((MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom ≫
          MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A)) ≫ ↟(mul' R ↑A)))
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A)))
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)) =
    (Hom.hom
        ((MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom ≫
          MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A)) ≫ ↟(mul' R ↑A)))
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)

Tactic:
hom_comp,

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A)))
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)) =
    (Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A)) ≫ ↟(mul' R ↑A)) ∘ₗ
        Hom.hom (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom)
      (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)
Module: Mathlib.CategoryTheory.Monoidal.Internal.Module

Goal state before:
pp: R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A)))
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)) =
    (Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A)) ≫ ↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom)
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z))

Tactic:
hom_comp,

Goal state after:
R : Type u
inst✝ : CommRing R
A : AlgCat R
x y z : ↑(of R ↑A)
⊢ (Hom.hom (↟(mul' R ↑A)))
      ((Hom.hom (MonoidalCategoryStruct.whiskerRight (↟(mul' R ↑A)) (of R ↑A)))
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z)) =
    (Hom.hom (↟(mul' R ↑A)) ∘ₗ Hom.hom (MonoidalCategoryStruct.whiskerLeft (of R ↑A) (↟(mul' R ↑A))))
      ((Hom.hom (MonoidalCategoryStruct.associator (of R ↑A) (of R ↑A) (of R ↑A)).hom)
        (((TensorProduct.mk R ↑(MonoidalCategoryStruct.tensorObj (of R ↑A) (of R ↑A)) ↑A) (x ⊗ₜ[R] y)) z))
Module: Mathlib.CategoryTheory.Monoidal.Bimod

Goal state before:
pp: 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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫ colimit.ι (parallelPair (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫
      (λ_ (X.X ⊗ N.X)).inv ≫
        (η ▷ (X.X ⊗ N.X) ≫ X.X ◁ N.actLeft) ≫ coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)

Tactic:
slice_rhs 4 4 => rw [← Iso.inv_hom_id_assoc (α_ X.X X.X N.X) (X.X ◁ N.actLeft)]

Goal state after:
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)
X Y : Mon C
M N : Bimod X Y
f : M ⟶ N
⊢ X.X ◁ f.hom ≫ colimit.ι (parallelPair (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)) WalkingParallelPair.one =
    X.X ◁ f.hom ≫
      (λ_ (X.X ⊗ N.X)).inv ≫
        η ▷ (X.X ⊗ N.X) ≫
          ((α_ X.X X.X N.X).inv ≫ (α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft) ≫
            coequalizer.π (μ ▷ N.X) ((α_ X.X X.X N.X).hom ≫ X.X ◁ N.actLeft)
Module: Mathlib.CategoryTheory.Presentable.Dense

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
J : Type u'
inst✝² : Category.{v', u'} J
inst✝¹ : EssentiallySmall.{w, v', u'} J
inst✝ : IsCardinalFiltered J κ
X : C
p : (isCardinalPresentable C κ).ColimitOfShape J X
this : IsFiltered J
f : CostructuredArrow (isCardinalPresentable C κ).ι X
j : J
g₁ g₂ : f ⟶ p.toCostructuredArrow.obj j
k : J
a : j ⟶ k
h : g₁.left.hom ≫ p.diag.map a = g₂.left.hom ≫ p.diag.map a
⊢ g₁ ≫ p.toCostructuredArrow.map a = g₂ ≫ p.toCostructuredArrow.map a

Tactic:
by cat_disch

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
X Y : C
f : X ⟶ Y
x✝ : P.ind f
J : Type w
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.underObj.ind (CategoryTheory.Under.mk f)

Tactic:
refine ⟨J, ‹_›, ‹_›, ⟨Under.lift D t, ?_, ?_⟩, ?_⟩
    · exact { app j := CategoryTheory.Under.homMk (s.app j) (by simp [hst]) }
    · have : Nonempty J := IsFiltered.nonempty
      exact Under.isColimitLiftCocone _ _ _ _ (by simp [hst]) hs
    · simp [underObj, hst]

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

Goal state before:
pp: case of_presieve
C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z : C
f✝ : X ⟶ Z
X✝ Y✝ : C
f : X✝ ⟶ Y✝
R : Presieve X✝
hR : R ∈ K.coverings X✝
h✝ : ∀ (U : C) (g : U ⟶ X✝), R g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    R g →
      ∀ (W : C) (g_1 : Y ⟶ Y✝) (fst : W ⟶ U) (snd : W ⟶ Y), IsPullback fst snd (g ≫ f) g_1 → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ X✝
snd : W ⟶ Y
h : IsPullback fst snd f g
⊢ ∀ (U : C) (g : U ⟶ W), Presieve.pullbackArrows fst R g → sourceLocalClosure K P (g ≫ snd)

Tactic:
intro U v ⟨Z, u, hu⟩

Goal state after:
case of_presieve
C : Type u
inst✝³ : Category.{v, u} C
K : Precoverage C
P Q : MorphismProperty C
X✝¹ Y✝¹ : C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : K.IsStableUnderBaseChange
inst✝ : HasPullbacks C
Y X Z✝ : C
f✝ : X ⟶ Z✝
X✝ Y✝ : C
f : X✝ ⟶ Y✝
R : Presieve X✝
hR : R ∈ K.coverings X✝
h✝ : ∀ (U : C) (g : U ⟶ X✝), R g → sourceLocalClosure K P (g ≫ f)
ih :
  ∀ (U : C) (g : U ⟶ X✝),
    R g →
      ∀ (W : C) (g_1 : Y ⟶ Y✝) (fst : W ⟶ U) (snd : W ⟶ Y), IsPullback fst snd (g ≫ f) g_1 → sourceLocalClosure K P snd
W : C
g : Y ⟶ Y✝
fst : W ⟶ X✝
snd : W ⟶ Y
h : IsPullback fst snd f g
U : C
v : U ⟶ W
Z : C
u : Z ⟶ X✝
hu : R u
⊢ sourceLocalClosure K P (pullback.snd u fst ≫ snd)
Module: Mathlib.CategoryTheory.Preadditive.EilenbergMoore

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : Preadditive C
T : Monad C
inst✝¹ : T.Additive
U : Comonad C
inst✝ : U.Additive
F G : U.Coalgebra
α β : F ⟶ G
⊢ F.a ≫ U.map (α.f + β.f) = (α.f + β.f) ≫ G.a

Tactic:
simp only [Functor.map_add, comp_add, Comonad.Coalgebra.Hom.h, add_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g : u ⟶ v
⊢ Function.LeftInverse (fun h ↦ { hom := h.hom, comm := ⋯ }) fun h ↦ { hom := h.hom, comm := ⋯ }

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.Homotopy

Goal state before:
pp: V : Type u_1
inst✝¹ : Category.{v_1, u_1} V
inst✝ : Preadditive V
u v w : Arrow V
f g : u ⟶ v
⊢ Function.RightInverse (fun h ↦ { hom := h.hom, comm := ⋯ }) fun h ↦ { hom := h.hom, comm := ⋯ }

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u v : Arrow V
f g : u ⟶ v
inst✝ : HasZeroObject V
x✝³ x✝² : V
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ (rightFunctor V).map (x✝¹ + x✝) = (rightFunctor V).map x✝¹ + (rightFunctor V).map x✝

Tactic:
by cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd

Goal state before:
pp: V : Type u_1
inst✝² : Category.{v_1, u_1} V
inst✝¹ : Preadditive V
u✝ v : Arrow V
f g : u✝ ⟶ v
inst✝ : HasZeroObject V
X✝ Y✝ : V
u : (rightFunctor V).obj X✝ ⟶ (rightFunctor V).obj Y✝
⊢ (rightFunctor V).map (Hom.right u) = u

Tactic:
by cat_disch

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✝ : u ⟶ v
⊢ 0 + x✝ = x✝

Tactic:
by cat_disch

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✝ : u ⟶ v
⊢ x✝ + 0 = x✝

Tactic:
by cat_disch

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✝ : u ⟶ v
⊢ -x✝ + x✝ = 0

Tactic:
by cat_disch

Goal state after:
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
hr : ∀ (f : X ⟶ Y), biprod.lift 0 f = f ≫ biprod.inr
hl : ∀ (f : X ⟶ Y), biprod.lift f 0 = f ≫ biprod.inl
f : X ⟶ Y
⊢ leftAdd X Y f 0 = f

Tactic:
by simp [hl f, leftAdd, Category.assoc, Category.comp_id, biprod.inl_desc]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (f j).ι
y : { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.ι
h : y.fst = j
⊢ (fun i j_1 ↦
      (f j).X i ⟶ { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.X j_1)
    x y

Tactic:
refine if h' : @Eq.ndrec _ y.1 (fun j => (f j).ι) y.2 _ h = x then ?_ else 0

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
j : Fin n
x : (f j).ι
y : { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.ι
h : y.fst = j
h' : h ▸ y.snd = x
⊢ (fun i j_1 ↦
      (f j).X i ⟶ { ι := (j : Fin n) × (f j).ι, fintype := Sigma.instFintype, X := fun p ↦ (f p.fst).X p.snd }.X j_1)
    x y
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
x y : CoconePt hc
j : J
x₁ y₁ : ↑(F.obj j)
hx₁ : (ConcreteCategory.hom (c.ι.app j)) x₁ = x
hy₁ : (ConcreteCategory.hom (c.ι.app j)) y₁ = y
h₁ : x₁ ≤ y₁
k : J
y₂ x₂ : ↑(F.obj k)
hy₂ : (ConcreteCategory.hom (c.ι.app k)) y₂ = y
hx₂ : (ConcreteCategory.hom (c.ι.app k)) x₂ = x
h₂ : y₂ ≤ x₂
l₁ : J
a : j ⟶ l₁
b : k ⟶ l₁
h₃ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a)) x₁ = (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b)) x₂
l₂ : J
a' : j ⟶ l₂
b' : k ⟶ l₂
h₄ :
  (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map a')) y₁ =
    (ConcreteCategory.hom ((F ⋙ forget PartOrdEmb).map b')) y₂
l : J
d : l₁ ⟶ l
d' : l₂ ⟶ l
h₅ : a ≫ d = a' ≫ d'
h₆ : b ≫ d = b' ≫ d'
⊢ (ConcreteCategory.hom (F.map (a' ≫ d'))) y₁ = (ConcreteCategory.hom (F.map (b ≫ d))) y₂

Tactic:
simpa [h₆]

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
F : J ⥤ PartOrdEmb
c : Cocone (F ⋙ forget PartOrdEmb)
hc : IsColimit c
⊢ ∀ (a b : CoconePt hc),
    (∃ j x' y',
        ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = a) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = b), x' ≤ y') →
      (∃ j x' y',
          ∃ (_ : (ConcreteCategory.hom (c.ι.app j)) x' = b) (_ : (ConcreteCategory.hom (c.ι.app j)) y' = a), x' ≤ y') →
        a = b

Tactic:
by
    rintro x y ⟨j, x₁, y₁, hx₁, hy₁, h₁⟩ ⟨k, y₂, x₂, hy₂, hx₂, h₂⟩
    obtain ⟨l, a, b, x₃, y₃, h₃, h₄, h₅, h₆⟩ :
        ∃ (l : J) (a : j ⟶ l) (b : k ⟶ l) (x₃ y₃ : _),
        x₃ = F.map a x₁ ∧ x₃ = F.map b x₂ ∧ y₃ = F.map a y₁ ∧ y₃ = F.map b y₂ := by
      obtain ⟨l₁, a, b, h₃⟩ :=
        (Types.FilteredColimit.isColimit_eq_iff _ hc (xi := x₁) (xj := x₂)).1
          (hx₁.trans hx₂.symm)
      obtain ⟨l₂, a', b', h₄⟩ :=
        (Types.FilteredColimit.isColimit_eq_iff _ hc (xi := y₁) (xj := y₂)).1
          (hy₁.trans hy₂.symm)
      obtain ⟨l, d, d', h₅, h₆⟩ := IsFiltered.bowtie a a' b b'
      exact ⟨l, a ≫ d, b ≫ d, F.map (a ≫ d) x₁, F.map (a' ≫ d') y₁, rfl,
        by simpa, by rw [h₅], by simpa [h₆]⟩
    have h₇ : x₃ = y₃ :=
      le_antisymm
        (by simpa only [h₃, h₅] using (F.map a).hom.monotone h₁)
        (by simpa only [h₄, h₆] using (F.map b).hom.monotone h₂)
    exact hx₁.symm.trans ((ConcreteCategory.congr_hom (c.w a) x₁).symm.trans
      ((congr_arg (c.ι.app l) (h₃.symm.trans (h₇.trans h₅))).trans
        ((ConcreteCategory.congr_hom (c.w a) y₁).trans hy₁)))

Goal state after:
Module: Mathlib.Order.Category.PartOrdEmb

Goal state before:
pp: α : PartOrdEmb
P : Set ↑α → Prop
inst✝¹ : IsDirectedOrder (Subtype P)
inst✝ : Nonempty (Subtype P)
hP : ∀ (a : ↑α), ∃ J, P J ∧ a ∈ J
⊢ IsColimit ((forget PartOrdEmb).mapCocone (coconeOfPredicateSet P))

Tactic:
refine Types.FilteredColimit.isColimitOf' _ _ (fun a ↦ ?_)
      (fun J x y h ↦ ⟨J, 𝟙 _, Subtype.ext h⟩)
    obtain ⟨J, hJ, ha⟩ := hP a
    exact ⟨⟨J, hJ⟩, ⟨a, ha⟩, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Coherent.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
β : Type
w✝ : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ B₂
h : EffectiveEpiFamily X₂ π₂
i : β → α
ι : (b : β) → X₂ b ⟶ X₁ (i b)
hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
⊢ ∃ T ∈ {S | ∃ α, ∃ (_ : Finite α), ∃ X π, S = Presieve.ofArrows X π ∧ EffectiveEpiFamily X π},
    T.FactorsThruAlong (Presieve.ofArrows X₁ π₁) f

Tactic:
refine ⟨Presieve.ofArrows X₂ π₂, ⟨β, inferInstance, X₂, π₂, rfl, h⟩, ?_⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Precoherent C
B₁ B₂ : C
f : B₂ ⟶ B₁
α : Type
w✝¹ : Finite α
X₁ : α → C
π₁ : (a : α) → X₁ a ⟶ B₁
hS : EffectiveEpiFamily X₁ π₁
β : Type
w✝ : Finite β
X₂ : β → C
π₂ : (b : β) → X₂ b ⟶ B₂
h : EffectiveEpiFamily X₂ π₂
i : β → α
ι : (b : β) → X₂ b ⟶ X₁ (i b)
hh : ∀ (b : β), ι b ≫ π₁ (i b) = π₂ b ≫ f
⊢ (Presieve.ofArrows X₂ π₂).FactorsThruAlong (Presieve.ofArrows X₁ π₁) f
Module: Mathlib.CategoryTheory.Sites.Adjunction

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
J : GrothendieckTopology C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
E : Type u_1
inst✝² : Category.{v_1, u_1} E
F : D ⥤ E
G : E ⥤ D
inst✝¹ : HasWeakSheafify J D
inst✝ : J.HasSheafCompose F
adj : G ⊣ F
Y : Sheaf J D
⊢ (sheafToPresheaf J D).map
      ((Iso.refl (sheafToPresheaf J E ⋙ (whiskeringRight Cᵒᵖ E D).obj G ⋙ presheafToSheaf J D)).inv.app
          ((sheafCompose J F).obj Y) ≫
        ((whiskeringRight Cᵒᵖ E D).obj G ⋙ presheafToSheaf J D).map
            ((Iso.refl (𝟭 (Sheaf J D) ⋙ sheafToPresheaf J D ⋙ (whiskeringRight Cᵒᵖ D E).obj F)).inv.app Y) ≫
          ((Adjunction.whiskerRight Cᵒᵖ adj).comp (sheafificationAdjunction J D)).counit.app ((𝟭 (Sheaf J D)).obj Y)) =
    sheafifyLift J ((Adjunction.whiskerRight Cᵒᵖ adj).counit.app Y.obj) ⋯

Tactic:
by cat_disch

Goal state after: