mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

Goal state before:
pp: A : Type u₁
B : Type u₂
C : Type u₃
inst✝³ : Category.{v₁, u₁} A
inst✝² : Category.{v₂, u₂} B
inst✝¹ : Category.{v₃, u₃} C
F : A ⥤ B
G : C ⥤ B
X : Type u₄
inst✝ : Category.{v₄, u₄} X
x✝ : CatCommSqOver F G X
⊢ ∀ {X_1 Y : X} (f : X_1 ⟶ Y),
    ((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.map f ≫
        (Iso.refl
            (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.obj Y)).hom =
      (Iso.refl
            (((CatCommSqOver.toFunctorToCategoricalPullback F G X ⋙ toCatCommSqOver F G X).obj x✝).snd.obj X_1)).hom ≫
        ((𝟭 (CatCommSqOver F G X)).obj x✝).snd.map f

Tactic:
intros; simp

Goal state after:
Module: Mathlib.CategoryTheory.MarkovCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MarkovCategory C
X : C
f : X ⟶ 𝟙_ C
⊢ f ≫ 𝟙 (𝟙_ C) = ε

Tactic:
← discard_unit,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MarkovCategory C
X : C
f : X ⟶ 𝟙_ C
⊢ f ≫ ε = ε
Module: Mathlib.CategoryTheory.Monad.Monadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ F.map A.a = 𝟙 (F.obj ((𝟭 C).obj A.A))

pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj ((𝟭 C).obj A.A))

Tactic:
· rw [← F.map_comp, ← F.map_id]
    exact congr_arg F.map A.unit

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₁, u₂} D
G : D ⥤ C
F : C ⥤ D
adj : F ⊣ G
A : adj.toMonad.Algebra
⊢ F.map (adj.unit.app A.A) ≫ adj.counit.app (F.obj A.A) = 𝟙 (F.obj ((𝟭 C).obj A.A))
Module: Mathlib.CategoryTheory.Monoidal.Braided.Reflection

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : SymmetricCategory D
inst✝⁴ : MonoidalClosed D
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
d d' : D
this :
  δ L ((𝟭 D).obj d) ((𝟭 D).obj d') ≫
      (L.map (adj.unit.app d) ⊗ₘ L.map (adj.unit.app d')) ≫ μ L ((L ⋙ R).obj d) ((L ⋙ R).obj d') =
    δ L ((𝟭 D).obj d) ((𝟭 D).obj d') ≫ μ L ((𝟭 D).obj d) ((𝟭 D).obj d') ≫ L.map (adj.unit.app d ⊗ₘ adj.unit.app d')
⊢ IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))

Tactic:
δ_μ_assoc

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : MonoidalCategory D
inst✝⁵ : SymmetricCategory D
inst✝⁴ : MonoidalClosed D
inst✝³ : MonoidalCategory C
L : D ⥤ C
inst✝² : L.Monoidal
R : C ⥤ D
inst✝¹ : R.Faithful
inst✝ : R.Full
adj : L ⊣ R
d d' : D
this :
  δ L ((𝟭 D).obj d) ((𝟭 D).obj d') ≫
      (L.map (adj.unit.app d) ⊗ₘ L.map (adj.unit.app d')) ≫ μ L ((L ⋙ R).obj d) ((L ⋙ R).obj d') =
    L.map (adj.unit.app d ⊗ₘ adj.unit.app d')
⊢ IsIso (L.map (adj.unit.app d ⊗ₘ adj.unit.app d'))
Module: Mathlib.CategoryTheory.Monoidal.Closed.Enrichment

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X Y₁ Y₂ : C
g : Y₁ ⟶ Y₂
⊢ eHomWhiskerLeft C X g = (ihom X).map g

Tactic:
by
  change (ρ_ _).inv ≫ _ ◁ curry' g ≫ comp X Y₁ Y₂ = _
  rw [whiskerLeft_curry'_comp, Iso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid

Goal state before:
pp: D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (ihom.coev (F.obj Y)).app (G.obj X) ≫ (ihom (F.obj Y)).map (F.obj Y ◁ G.map f) =
    (ihom.coev (F.obj Y)).app (G.obj X) ≫
      (ihom (F.obj Y)).map (CategoryTheory.inv (F.map f) ▷ G.obj X ≫ (F.map f ⊗ₘ G.map f))

Tactic:
tensorHom_def

Goal state after:
D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (ihom.coev (F.obj Y)).app (G.obj X) ≫ (ihom (F.obj Y)).map (F.obj Y ◁ G.map f) =
    (ihom.coev (F.obj Y)).app (G.obj X) ≫
      (ihom (F.obj Y)).map (CategoryTheory.inv (F.map f) ▷ G.obj X ≫ F.map f ▷ G.obj X ≫ F.obj Y ◁ G.map f)
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid

Goal state before:
pp: D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (F.map f ⊗ₘ (ihom (F.obj X)).map (G.map f) ≫ (pre (CategoryTheory.inv (F.map f))).app (G.obj Y)) ≫
      (ihom.ev (F.obj Y)).app (G.obj Y) =
    (ihom.ev (F.obj X)).app (G.obj X) ≫ G.map f

Tactic:
tensorHom_def

Goal state after:
D : Type u
C : Type u_1
inst✝³ : Groupoid D
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
F G : D ⥤ C
X Y : D
f : X ⟶ Y
⊢ (F.map f ▷ (ihom (F.obj X)).obj (G.obj X) ≫
        F.obj Y ◁ ((ihom (F.obj X)).map (G.map f) ≫ (pre (CategoryTheory.inv (F.map f))).app (G.obj Y))) ≫
      (ihom.ev (F.obj Y)).app (G.obj Y) =
    (ihom.ev (F.obj X)).app (G.obj X) ≫ G.map f
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalClosed C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
inst✝ : ∀ (F₁ F₂ : J ⥤ C), HasFunctorEnrichedHom C F₁ F₂
F₁ F₂ F₂' F₃ F₃' : J ⥤ C
f : F₁ ⊗ F₂ ⟶ F₃
j : J
k₁ k₂ : Under j
φ : k₁ ⟶ k₂
⊢ (F₂.map k₁.hom ≫ curry (f.app k₁.right)) ≫
      ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).obj (Opposite.op k₁)).map φ =
    (F₂.map k₂.hom ≫ curry (f.app k₂.right)) ≫ ((diagram C (Under.forget j ⋙ F₁) (Under.forget j ⋙ F₃)).map φ.op).app k₂

Tactic:
dsimp
          simp only [enrichedOrdinaryCategorySelf_eHomWhiskerLeft, Category.assoc,
            enrichedOrdinaryCategorySelf_eHomWhiskerRight]
          rw [← curry_natural_left_assoc, ← curry_natural_left_assoc,
            ← curry_natural_right, curry_pre_app, Category.assoc,
            ← f.naturality φ.right, Monoidal.tensorObj_map, tensorHom_def_assoc,
            ← Under.w φ, Functor.map_comp, MonoidalCategory.whiskerLeft_comp_assoc,
            whisker_exchange_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Subterminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
A T : C
hT : IsTerminal T
inst✝ : Mono (hT.from A)
Z : C
f g : Z ⟶ A
⊢ f ≫ hT.from A = g ≫ hT.from A

Tactic:
apply hT.hom_ext

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : MonoidalClosed C
h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)
B✝ : C
hB : i.essImage B✝
A : C
⊢ i.essImage (A ⟹ B✝)

Tactic:
rcases hB with ⟨B', ⟨iB'⟩⟩

Goal state after:
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
i : D ⥤ C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : MonoidalClosed C
h : ∀ (B : D) (A : C), i.essImage (A ⟹ i.obj B)
B✝ A : C
B' : D
iB' : i.obj B' ≅ B✝
⊢ i.essImage (A ⟹ B✝)
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 H G : C ⥤ V
inst✝ : DayConvolution F H
ℌ : DayConvolutionInternalHom F G H
H' : C ⥤ V
ℌ' : DayConvolutionInternalHom F (F ⊛ H) H'
⊢ ℌ'.coev_app ≫ ℌ'.map ℌ.ev_app ℌ = 𝟙 H

Tactic:
by
  ext c
  apply Wedge.IsLimit.hom_ext <| ℌ.isLimitWedge c
  intro j
  apply MonoidalClosed.uncurry_injective
  simp [MonoidalClosed.uncurry_natural_right]

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

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

Tactic:
tensorHom_def

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ ε ≫ (ρ_ (𝟙_ C)).inv ≫ η ▷ 𝟙_ C ≫ A ◁ η = ε ≫ (λ_ (𝟙_ C)).inv ≫ η ▷ 𝟙_ C ≫ A ◁ η
Module: Mathlib.CategoryTheory.Monoidal.Hopf_

Goal state before:
pp: 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).hom ≫
                  (A ⊗ A) ◁ (β_ A A).hom ≫
                    (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ (A ⊗ A) A A).inv ≫ ((α_ A A A).hom ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
tensorHom_def

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : BraidedCategory C
A : C
inst✝ : HopfObj A
⊢ (Δ ▷ A ≫ (A ⊗ 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).hom ≫
                  (A ⊗ A) ◁ (β_ A A).hom ≫
                    (A ⊗ A) ◁ (𝒮 ⊗ₘ 𝒮) ≫ (α_ (A ⊗ A) A A).inv ≫ ((α_ A A A).hom ▷ A ≫ (A ◁ μ) ▷ A ≫ μ ▷ A) ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η
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).inv ≫ (α_ A A A).inv ▷ A ≫ μ ▷ A ▷ A ≫ 𝒮 ▷ A ▷ A ≫ (α_ A A A).hom ≫ A ◁ μ ≫ μ =
    (ε ⊗ₘ ε) ≫ (λ_ (𝟙_ C)).hom ≫ η

Tactic:
exact mul_antipode₁ A

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
R S : Mon C
P : Bimod R S
inst✝¹ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorRight X)
| μ ▷ P.X ≫ P.actLeft

pp: case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
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.X R.X P.X).inv

Tactic:
rw [left_assoc]

Goal state after:
case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
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.X R.X P.X).hom ≫ R.X ◁ P.actLeft ≫ P.actLeft

case a
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : MonoidalCategory C
inst✝² : HasCoequalizers C
R S : Mon C
P : Bimod R S
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.X R.X P.X).inv
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✝ : DayConvolution F U
x : C
⊢ (rightUnitor U F).inv.app x =
    (ρ_ (F.obj x)).inv ≫ F.obj x ◁ can ≫ (DayConvolution.unit F U).app (x, 𝟙_ C) ≫ (F ⊛ U).map (ρ_ x).hom

Tactic:
by
  dsimp [rightUnitor, Coyoneda.fullyFaithful, corepresentableByRight,
    rightUnitorCorepresentingIso, Functor.CorepresentableBy.ofIso,
    Functor.corepresentableByEquiv, Iso.toEquiv, Equiv.toIso]
  dsimp [prod.rightUnitorEquivalence, Equivalence.congrLeft, Equivalence.fullyFaithfulFunctor,
    Functor.FullyFaithful.homEquiv]
  erw [id_apply] -- TODO: remove this `erw` (introduced in #36613)
  simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X✝ Y✝ Z✝ : C
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
hf : P.localEpi f
hg : P.localEpi g
T : C
hT : P T
x✝¹ x✝ : Z✝ ⟶ T
huv : (fun g_1 ↦ (f ≫ g) ≫ g_1) x✝¹ = (fun g_1 ↦ (f ≫ g) ≫ g_1) x✝
⊢ (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) x✝¹) = (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) x✝)

Tactic:
simpa using huv

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
⊢ ⊤.localEpi = MorphismProperty.epimorphisms C

Tactic:
by
  ext
  simp

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hg : P.isLocal g
hfg : P.localEpi (f ≫ g)
T : C
hT : P T
u v : Z ⟶ T
huv : (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) u) = (fun g ↦ f ≫ g) ((fun g_1 ↦ g ≫ g_1) v)
⊢ (fun g_1 ↦ (f ≫ g) ≫ g_1) ?m.71 = (fun g_1 ↦ (f ≫ g) ≫ g_1) ?m.72

Tactic:
simpa using huv

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasZeroObject C
⊢ isArtinianObject.Is 0

Tactic:
exact isArtinianObject_of_isZero (isZero_zero C)

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.ArtinianObject

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y : C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsArtinianObject X
h : ¬IsZero X
⊢ Mono (simpleSubobjectArrow h)

Tactic:
dsimp only [simpleSubobjectArrow]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y : C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsArtinianObject X
h : ¬IsZero X
⊢ Mono ⋯.choose.arrow
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
F G : T.Algebra
r : ℤ
α : F ⟶ G
⊢ r • F.a ≫ α.f = F.a ≫ (r • α.f)

Tactic:
comp_zsmul

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
T : Monad C
inst✝ : T.Additive
F G : T.Algebra
r : ℤ
α : F ⟶ G
⊢ r • F.a ≫ α.f = r • F.a ≫ α.f
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✝ : HasBinaryBiproducts V
u v : Arrow V
f✝ : u ⟶ v
X✝ Y✝ : RightFreyd V
f : X✝ ⟶ Y✝
⊢ Nonempty (ColimitCocone (parallelPair f 0))

Tactic:
obtain ⟨f, rfl⟩ := (quotient V).map_surjective f
    exact ⟨_, Candidate.isColimitCokernelCofork f⟩

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
n : ℤ
α : u ⟶ v
⊢ L.map (n • α.left) ≫ v.hom = u.hom ≫ R.map (n • α.right)

Tactic:
simp [Functor.map_zsmul, Preadditive.comp_zsmul, Preadditive.zsmul_comp]

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
⊢ EckmannHilton.IsUnital (fun x1 x2 ↦ rightAdd X Y x1 x2) 0

Tactic:
by
  have h₂ : ∀ f : X ⟶ Y, biprod.desc (0 : X ⟶ Y) f = biprod.snd ≫ f := by
    intro f
    ext
    · simp
    · simp only [biprod.inr_desc, BinaryBicone.inr_snd_assoc]
  have h₁ : ∀ f : X ⟶ Y, biprod.desc f (0 : X ⟶ Y) = biprod.fst ≫ f := by
    intro f
    ext
    · simp
    · simp only [biprod.inr_desc, BinaryBicone.inr_fst_assoc, zero_comp]
  exact {
    left_id := fun f => by simp [h₂ f, rightAdd, biprod.lift_snd_assoc, Category.id_comp],
    right_id := fun f => by simp [h₁ f, rightAdd, biprod.lift_fst_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
inst✝¹ : HasKernels C
X : C
inst✝ : Simple X
f : End X
hf : f ≠ 0
⊢ (f * if h : f = 0 then 0 else inv f) = 1

Tactic:
by
    dsimp
    rw [dif_neg hf]
    have := isIso_of_hom_simple hf
    exact IsIso.inv_hom_id f

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

Goal state before:
pp: case pos
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : j' = j
⊢ (if h' : j' = j then eqToHom ⋯ else 0) = if h : j = j' then eqToHom ⋯ else 0

pp: case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : ¬j' = j
⊢ (if h' : j' = j then eqToHom ⋯ else 0) = if h : j = j' then eqToHom ⋯ else 0

Tactic:
· subst h
                simp

Goal state after:
case neg
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Preadditive C
n : ℕ
f : Fin n → Mat_ C
i' : Fin n
j' j : (f i').ι
h : ¬j' = j
⊢ (if h' : j' = j then eqToHom ⋯ else 0) = if h : j = j' then eqToHom ⋯ else 0
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : J ⟶ c.pt
j : ↑J.obj → A
g : (x : ↑J.obj) → (fun X ↦ X) ((F ⋙ forget (CardinalDirectedPoset κ)).obj (j x))
hg :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
      (ConcreteCategory.hom f) x
m : A := IsCardinalFiltered.max j hJ
φ : ↑J.obj → ↑(F.obj m).obj := fun x ↦ (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x)
x : ↑J.obj
⊢ (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
    (ConcreteCategory.hom (c.ι.app m)) ((ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x))

Tactic:
← ConcreteCategory.comp_apply,

Goal state after:
κ : Cardinal.{u}
inst✝¹ : Fact κ.IsRegular
J : CardinalDirectedPoset κ
κ' : Cardinal.{u}
inst✝ : Fact κ'.IsRegular
hJ : HasCardinalLT (↑J.obj) κ'
h : κ ≤ κ'
A : Type u
x✝¹ : SmallCategory A
x✝ : IsCardinalFiltered A κ'
F : A ⥤ CardinalDirectedPoset κ
c : Cocone F
this✝ : IsFiltered A
this : IsCardinalFiltered A κ
hc : IsColimit ((forget (CardinalDirectedPoset κ)).mapCocone c)
f : J ⟶ c.pt
j : ↑J.obj → A
g : (x : ↑J.obj) → (fun X ↦ X) ((F ⋙ forget (CardinalDirectedPoset κ)).obj (j x))
hg :
  ∀ (x : ↑J.obj),
    (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
      (ConcreteCategory.hom f) x
m : A := IsCardinalFiltered.max j hJ
φ : ↑J.obj → ↑(F.obj m).obj := fun x ↦ (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x))) (g x)
x : ↑J.obj
⊢ (ConcreteCategory.hom (((forget (CardinalDirectedPoset κ)).mapCocone c).ι.app (j x))) (g x) =
    (ConcreteCategory.hom (F.map (IsCardinalFiltered.toMax j hJ x) ≫ c.ι.app m)) (g x)
Module: Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset

Goal state before:
pp: κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
X K : Type u
f : K → SetCardinalLT κ X
hK : Cardinal.mk K < κ
⊢ HasCardinalLT K κ

Tactic:
by rwa [hasCardinalLT_iff_cardinal_mk_lt]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Type

Goal state before:
pp: X : Type u
κ : Cardinal.{u}
inst✝ : Fact κ.IsRegular
ι : Type u
A : ι → HasCardinalLT.Set X κ
hι : Cardinal.mk ι < κ
⊢ HasCardinalLT ι κ

Tactic:
by rwa [hasCardinalLT_iff_cardinal_mk_lt]

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Directed

Goal state before:
pp: case refine_3
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
j : J
l₁ l₂ : j ⟶ m
hl₁ : (D₂ D hι u).W l₁
hl₂ : (D₂ D hι u).W l₂
hj : (∃ a, (D a).P j) ∨ m = j
⊢ l₁ = l₂

Tactic:
obtain (⟨i, hj⟩ | rfl) := hj

Goal state after:
case refine_3.inl
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
j : J
l₁ l₂ : j ⟶ m
hl₁ : (D₂ D hι u).W l₁
hl₂ : (D₂ D hι u).W l₂
i : ι
hj : (D i).P j
⊢ l₁ = l₂

case refine_3.inr
J : Type w
inst✝² : SmallCategory J
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalFiltered J κ
hJ : ∀ (e : J), ∃ m x, IsEmpty (m ⟶ e)
ι : Type w
D : ι → DiagramWithUniqueTerminal J κ
hι : HasCardinalLT ι κ
m : J
u : (i : ι) → (D i).top ⟶ m
hm₀ : ∀ (i : ι), IsEmpty (m ⟶ (D i).top)
hm :
  ∀ (i₁ i₂ : ι) (j : J) (hj₁ : (D i₁).P j) (hj₂ : (D i₂).P j),
    (D i₁).isTerminal.lift hj₁ ≫ u i₁ = (D i₂).isTerminal.lift hj₂ ≫ u i₂
φ : (x : (i : ι) × Subtype (D i).P) → ↑x.snd ⟶ m := fun x ↦ (D x.fst).isTerminal.lift ⋯ ≫ u x.fst
hD : ∀ {i : ι}, ¬(D i).P m
H : ∀ {i : ι} {j : J} (hj : (D i).P j) {f : j ⟶ m}, (D₂ D hι u).W f → f = φ ⟨i, ⟨j, hj⟩⟩
l₁ l₂ : m ⟶ m
hl₁ : (D₂ D hι u).W l₁
hl₂ : (D₂ D hι u).W l₂
⊢ l₁ = l₂
Module: Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Precoherent C
X : C
α : Type
inst✝¹ : Finite α
Y : α → C
π : (a : α) → Y a ⟶ X
h : EffectiveEpiFamily Y π
β : α → Type
inst✝ : ∀ (a : α), Finite (β a)
Y_n : (a : α) → β a → C
π_n : (a : α) → (b : β a) → Y_n a b ⟶ Y a
H : ∀ (a : α), EffectiveEpiFamily (Y_n a) (π_n a)
h₂ :
  Sieve.generate
      (Presieve.ofArrows
        (fun x ↦
          match x with
          | ⟨a, b⟩ => Y_n a b)
        fun x ↦
        match x with
        | ⟨a, b⟩ => π_n a b ≫ π a) ∈
    (coherentTopology C) X
⊢ ∀ (W : C),
    Presieve.IsSheafFor (yoneda.obj W)
      (Sieve.generate (Presieve.ofArrows (fun c ↦ Y_n c.fst c.snd) fun c ↦ π_n c.fst c.snd ≫ π c.fst)).arrows

Tactic:
exact fun W => coherentTopology.isSheaf_yoneda_obj W _ h₂

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

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Category.{v_2, u_2} D
F : C ⥤ D
inst✝⁵ : F.PreservesFiniteEffectiveEpiFamilies
inst✝⁴ : F.ReflectsFiniteEffectiveEpiFamilies
inst✝³ : F.Full
inst✝² : F.Faithful
inst✝¹ : F.EffectivelyEnough
inst✝ : Precoherent D
B : D
⊢ EffectiveEpiFamily (fun x ↦ F.effectiveEpiOverObj B) fun x ↦ F.effectiveEpiOver B

Tactic:
rw [← effectiveEpi_iff_effectiveEpiFamily]
    infer_instance

Goal state after: