mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ { obj := fun j ↦ (data.factorizationData (X✝.hom.app j)).Z,
            map := fun {X Y} φ ↦ data.mapZ (Arrow.homMk (X✝.left.map φ) (X✝.right.map φ) ⋯), map_id := ⋯,
            map_comp := ⋯ }.map
        x✝ ≫
      data.mapZ (Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    data.mapZ (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯) ≫
      { obj := fun j ↦ (data.factorizationData (Y✝.hom.app j)).Z,
            map := fun {X Y} φ ↦ data.mapZ (Arrow.homMk (Y✝.left.map φ) (Y✝.right.map φ) ⋯), map_id := ⋯,
            map_comp := ⋯ }.map
        x✝

Tactic:
dsimp

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ : Arrow (J ⥤ C)
τ : X✝ ⟶ Y✝
x✝² x✝¹ : J
x✝ : x✝² ⟶ x✝¹
⊢ data.mapZ (Arrow.homMk (X✝.left.map x✝) (X✝.right.map x✝) ⋯) ≫
      data.mapZ (Arrow.homMk ((Arrow.Hom.left τ).app x✝¹) ((Arrow.Hom.right τ).app x✝¹) ⋯) =
    data.mapZ (Arrow.homMk ((Arrow.Hom.left τ).app x✝²) ((Arrow.Hom.right τ).app x✝²) ⋯) ≫
      data.mapZ (Arrow.homMk (Y✝.left.map x✝) (Y✝.right.map x✝) ⋯)
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
j : J
⊢ { app := fun j ↦ data.mapZ (Arrow.homMk ((Arrow.Hom.left (𝟙 f)).app j) ((Arrow.Hom.right (𝟙 f)).app j) ⋯),
          naturality := ⋯ }.app
      j =
    (𝟙
          { obj := fun j ↦ (data.factorizationData (f.hom.app j)).Z,
            map := fun {X Y} φ ↦ data.mapZ (Arrow.homMk (f.left.map φ) (f.right.map φ) ⋯), map_id := ⋯,
            map_comp := ⋯ }).app
      j

Tactic:
dsimp

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
f : Arrow (J ⥤ C)
j : J
⊢ data.mapZ (Arrow.homMk (𝟙 (f.left.obj j)) (𝟙 (f.right.obj j)) ⋯) = 𝟙 (data.factorizationData (f.hom.app j)).Z
Module: Mathlib.CategoryTheory.MorphismProperty.Factorization

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ Z✝ : Arrow (J ⥤ C)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
j : J
⊢ { app := fun j ↦ data.mapZ (Arrow.homMk ((Arrow.Hom.left (f ≫ g)).app j) ((Arrow.Hom.right (f ≫ g)).app j) ⋯),
          naturality := ⋯ }.app
      j =
    ({ app := fun j ↦ data.mapZ (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯),
            naturality := ⋯ } ≫
          { app := fun j ↦ data.mapZ (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯),
            naturality := ⋯ }).app
      j

Tactic:
dsimp

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
W₁ W₂ : MorphismProperty C
data : W₁.FunctorialFactorizationData W₂
J : Type u_3
inst✝ : Category.{v_3, u_3} J
X✝ Y✝ Z✝ : Arrow (J ⥤ C)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
j : J
⊢ data.mapZ
      (Arrow.homMk ((Arrow.Hom.left f).app j ≫ (Arrow.Hom.left g).app j)
        ((Arrow.Hom.right f).app j ≫ (Arrow.Hom.right g).app j) ⋯) =
    data.mapZ (Arrow.homMk ((Arrow.Hom.left f).app j) ((Arrow.Hom.right f).app j) ⋯) ≫
      data.mapZ (Arrow.homMk ((Arrow.Hom.left g).app j) ((Arrow.Hom.right g).app j) ⋯)
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X : C
x : d ⟶ F.obj X
Y : C
y : d ⟶ F.obj Y
f : op (StructuredArrow.mk x) ⟶ op (StructuredArrow.mk y)
⊢ StructuredArrow.Hom.right
      ((𝟭 (StructuredArrow d F)ᵒᵖ).map f ≫
          (StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk y))).right) ⋯).op.hom).unop =
    StructuredArrow.Hom.right
      ((StructuredArrow.isoMk (Iso.refl (unop (op (StructuredArrow.mk x))).right) ⋯).op.hom ≫
          (StructuredArrow.toCostructuredArrow F d ⋙ (CostructuredArrow.toStructuredArrow' F d).rightOp).map f).unop

Tactic:
apply Quiver.Hom.op_inj (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
d : D
X : C
x : F.obj X ⟶ d
Y : C
y : F.obj Y ⟶ d
f : op (CostructuredArrow.mk x) ⟶ op (CostructuredArrow.mk y)
⊢ ((𝟭 (CostructuredArrow F d)ᵒᵖ).map f ≫
          (CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk y))).left) ⋯).op.hom).unop.left =
    ((CostructuredArrow.isoMk (Iso.refl (unop (op (CostructuredArrow.mk x))).left) ⋯).op.hom ≫
          (CostructuredArrow.toStructuredArrow F d ⋙ (StructuredArrow.toCostructuredArrow' F d).rightOp).map
            f).unop.left

Tactic:
apply Quiver.Hom.op_inj (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Fork f g
⊢ s.π.app one = s.ι ≫ f

Tactic:
← s.app_zero_eq_ι,

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Fork f g
⊢ s.π.app one = s.π.app zero ≫ f
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Fork f g
⊢ s.π.app one = s.ι ≫ g

Tactic:
← s.app_zero_eq_ι,

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
s : Fork f g
⊢ s.π.app one = s.π.app zero ≫ g
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
b : B
X✝ Y✝ : CostructuredArrow (snd L R) b
f : X✝ ⟶ Y✝
⊢ L.map f.left.left ≫ (CostructuredArrow.mk (Y✝.left.hom ≫ R.map Y✝.hom)).hom =
    (CostructuredArrow.mk (X✝.left.hom ≫ R.map X✝.hom)).hom

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
b : B
X✝ Y✝ : CostructuredArrow (snd L R) b
f : X✝ ⟶ Y✝
⊢ L.map f.left.left ≫ Y✝.left.hom ≫ R.map Y✝.hom = X✝.left.hom ≫ R.map X✝.hom
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : IsIso f
inst✝ : HasImage g
F' : MonoFactorisation (f ≫ g)
⊢ image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m = ((Image.monoFactorisation g).isoComp f).m

Tactic:
dsimp

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : IsIso f
inst✝ : HasImage g
F' : MonoFactorisation (f ≫ g)
⊢ image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m = image.ι g
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
H : C ⥤ D
X : C
⊢ (η ≫ 0).app X = NatTrans.app 0 X

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
X✝ Y✝ : C ⥤ D
η : X✝ ⟶ Y✝
H : C ⥤ D
X : C
⊢ η.app X ≫ NatTrans.app 0 X = NatTrans.app 0 X
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
F G H : C ⥤ D
η : G ⟶ H
X : C
⊢ (0 ≫ η).app X = NatTrans.app 0 X

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroMorphisms D
F G H : C ⥤ D
η : G ⟶ H
X : C
⊢ NatTrans.app 0 X ≫ η.app X = NatTrans.app 0 X
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : f = 0
⊢ IsZero Y

Tactic:
by
  subst h
  apply of_epi_zero X Y

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y✝ : C
inst✝² : Category.{v, u} C
f✝ g : X✝ ⟶ Y✝
inst✝¹ : IsSplitMono f✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
s : Fork (𝟙 Y) (retraction f ≫ f)
⊢ (s.ι ≫ retraction f) ≫ (coneOfIsSplitMono f).ι = s.ι

Tactic:
dsimp

Goal state after:
C : Type u
X✝ Y✝ : C
inst✝² : Category.{v, u} C
f✝ g : X✝ ⟶ Y✝
inst✝¹ : IsSplitMono f✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitMono f
s : Fork (𝟙 Y) (retraction f ≫ f)
⊢ (s.ι ≫ retraction f) ≫ f = s.ι
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ inl X Y ≫ fst = 𝟙 X

Tactic:
by
  simp [prod.inl]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : HasBinaryProduct X Y
⊢ inl X Y ≫ snd = 0

Tactic:
by
  simp [prod.inl]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X✝ Y✝ : C
inst✝² : Category.{v, u} C
f✝ g : X✝ ⟶ Y✝
inst✝¹ : IsSplitEpi f✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
s : Cofork (𝟙 X) (f ≫ section_ f)
⊢ (coconeOfIsSplitEpi f).π ≫ section_ f ≫ s.π = s.π

Tactic:
dsimp

Goal state after:
C : Type u
X✝ Y✝ : C
inst✝² : Category.{v, u} C
f✝ g : X✝ ⟶ Y✝
inst✝¹ : IsSplitEpi f✝
X Y : C
f : X ⟶ Y
inst✝ : IsSplitEpi f
s : Cofork (𝟙 X) (f ≫ section_ f)
⊢ f ≫ section_ f ≫ s.π = s.π
Module: Mathlib.CategoryTheory.Limits.Preserves.Finite

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesColimitsOfShape J F

Tactic:
exact preservesColimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
⊢ Injective (@toMonoid M)

Tactic:
rintro @⟨@⟨⟩⟩ @⟨@⟨⟩⟩ h

Goal state after:
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
toNPow✝¹ : NPow M
npow_zero✝¹ : ∀ (x : M), x ^ 0 = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsLeftCancelMul✝¹ : IsLeftCancelMul M
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
toNPow✝ : NPow M
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsLeftCancelMul✝ : IsLeftCancelMul M
h :
  { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
        npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsLeftCancelMul := toIsLeftCancelMul✝¹ }.toMonoid =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsLeftCancelMul := toIsLeftCancelMul✝ }.toMonoid
⊢ { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
      npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsLeftCancelMul := toIsLeftCancelMul✝¹ } =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
      npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsLeftCancelMul := toIsLeftCancelMul✝ }
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: M : Type u
⊢ Injective (@toMonoid M)

Tactic:
rintro @⟨@⟨⟩⟩ @⟨@⟨⟩⟩ h

Goal state after:
M : Type u
toSemigroup✝¹ : Semigroup M
toOne✝¹ : One M
one_mul✝¹ : ∀ (a : M), 1 * a = a
mul_one✝¹ : ∀ (a : M), a * 1 = a
toNPow✝¹ : NPow M
npow_zero✝¹ : ∀ (x : M), x ^ 0 = 1
npow_succ✝¹ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝¹ : IsRightCancelMul M
toSemigroup✝ : Semigroup M
toOne✝ : One M
one_mul✝ : ∀ (a : M), 1 * a = a
mul_one✝ : ∀ (a : M), a * 1 = a
toNPow✝ : NPow M
npow_zero✝ : ∀ (x : M), x ^ 0 = 1
npow_succ✝ : ∀ (n : ℕ) (x : M), x ^ (n + 1) = x ^ n * x
toIsRightCancelMul✝ : IsRightCancelMul M
h :
  { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
        npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsRightCancelMul := toIsRightCancelMul✝¹ }.toMonoid =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
        npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsRightCancelMul := toIsRightCancelMul✝ }.toMonoid
⊢ { toSemigroup := toSemigroup✝¹, toOne := toOne✝¹, one_mul := one_mul✝¹, mul_one := mul_one✝¹, toNPow := toNPow✝¹,
      npow_zero := npow_zero✝¹, npow_succ := npow_succ✝¹, toIsRightCancelMul := toIsRightCancelMul✝¹ } =
    { toSemigroup := toSemigroup✝, toOne := toOne✝, one_mul := one_mul✝, mul_one := mul_one✝, toNPow := toNPow✝,
      npow_zero := npow_zero✝, npow_succ := npow_succ✝, toIsRightCancelMul := toIsRightCancelMul✝ }
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: G : Type u_1
⊢ Injective (@toDivInvMonoid G)

Tactic:
by
  rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl

Goal state after:
Module: Mathlib.Algebra.Group.Ext

Goal state before:
pp: G : Type u_1
⊢ Injective (@toGroup G)

Tactic:
by
  rintro ⟨⟩ ⟨⟩ ⟨⟩; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ₗ D
G : D ⥤ₗ E
⊢ leftExactFunctor C E ((forget D E ⋙ (Functor.whiskeringLeft C D E).obj F.obj).obj G)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ₗ D
G : D ⥤ₗ E
⊢ leftExactFunctor C E (F.obj ⋙ G.obj)
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : D ⥤ₗ E
G : C ⥤ₗ D
⊢ leftExactFunctor C E ((forget C D ⋙ (Functor.whiskeringRight C D E).obj F.obj).obj G)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : D ⥤ₗ E
G : C ⥤ₗ D
⊢ leftExactFunctor C E (G.obj ⋙ F.obj)
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ᵣ D
G : D ⥤ᵣ E
⊢ rightExactFunctor C E ((forget D E ⋙ (Functor.whiskeringLeft C D E).obj F.obj).obj G)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ᵣ D
G : D ⥤ᵣ E
⊢ rightExactFunctor C E (F.obj ⋙ G.obj)
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : D ⥤ᵣ E
G : C ⥤ᵣ D
⊢ rightExactFunctor C E ((forget C D ⋙ (Functor.whiskeringRight C D E).obj F.obj).obj G)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : D ⥤ᵣ E
G : C ⥤ᵣ D
⊢ rightExactFunctor C E (G.obj ⋙ F.obj)
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ₑ D
G : D ⥤ₑ E
⊢ leftExactFunctor C E ((forget D E ⋙ (Functor.whiskeringLeft C D E).obj F.obj).obj G)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ₑ D
G : D ⥤ₑ E
⊢ leftExactFunctor C E (F.obj ⋙ G.obj)
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ₑ D
G : D ⥤ₑ E
⊢ rightExactFunctor C E ((forget D E ⋙ (Functor.whiskeringLeft C D E).obj F.obj).obj G)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : C ⥤ₑ D
G : D ⥤ₑ E
⊢ rightExactFunctor C E (F.obj ⋙ G.obj)
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : D ⥤ₑ E
G : C ⥤ₑ D
⊢ leftExactFunctor C E ((forget C D ⋙ (Functor.whiskeringRight C D E).obj F.obj).obj G)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : D ⥤ₑ E
G : C ⥤ₑ D
⊢ leftExactFunctor C E (G.obj ⋙ F.obj)
Module: Mathlib.CategoryTheory.Limits.ExactFunctor

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : D ⥤ₑ E
G : C ⥤ₑ D
⊢ rightExactFunctor C E ((forget C D ⋙ (Functor.whiskeringRight C D E).obj F.obj).obj G)

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F : D ⥤ₑ E
G : C ⥤ₑ D
⊢ rightExactFunctor C E (G.obj ⋙ F.obj)
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: case pos
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : F.PreservesZeroMorphisms
J : Type w₁
f : J → C
b : Bicone f
j : J
⊢ 𝟙 (F.obj (f j)) = 𝟙 ((F.obj ∘ f) j)

Tactic:
dsimp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
j : Discrete J
⊢ ((Cone.postcompose (Discrete.natIso fun j ↦ Iso.refl (G.obj (f j.as))).hom).obj (G.mapCone (Fan.mk P g))).π.app j =
    (Iso.refl
          ((Cone.postcompose (Discrete.natIso fun j ↦ Iso.refl (G.obj (f j.as))).hom).obj
              (G.mapCone (Fan.mk P g))).pt).hom ≫
      (Fan.mk (G.obj P) fun j ↦ G.map (g j)).π.app j

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → P ⟶ f j
j : Discrete J
⊢ G.map (g j.as) ≫ 𝟙 (G.obj (f j.as)) = 𝟙 (G.obj P) ≫ G.map (g j.as)
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app one = i.symm.hom ≫ (KernelFork.ofι l ⋯).π.app one

Tactic:
dsimp

Goal state after:
case one
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ X
s : KernelFork f
hs : IsLimit s
i : Z ≅ s.pt
h : i.hom ≫ Fork.ι s = l
⊢ s.π.app one = i.inv ≫ l ≫ f
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
j : Discrete J
⊢ ((Cocone.precompose (Discrete.natIso fun j ↦ Iso.refl (G.obj (f j.as))).hom).obj (G.mapCocone (Cofan.mk P g))).ι.app
        j ≫
      (Iso.refl
          ((Cocone.precompose (Discrete.natIso fun j ↦ Iso.refl (G.obj (f j.as))).hom).obj
              (G.mapCocone (Cofan.mk P g))).pt).hom =
    (Cofan.mk (G.obj P) fun j ↦ G.map (g j)).ι.app j

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
f : J → C
P : C
g : (j : J) → f j ⟶ P
j : Discrete J
⊢ (𝟙 (G.obj (f j.as)) ≫ G.map (g j.as)) ≫ 𝟙 (G.obj P) = G.map (g j.as)
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
⊢ s.ι.app zero ≫ i.hom = (CokernelCofork.ofπ l ⋯).ι.app zero

Tactic:
dsimp

Goal state after:
case zero
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Y ⟶ Z
s : CokernelCofork f
hs : IsColimit s
i : s.pt ≅ Z
h : Cofork.π s ≫ i.hom = l
⊢ s.ι.app zero ≫ i.hom = f ≫ l
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
⊢ (bicone f).toCocone.ι.app { as := j✝ } ≫ (bicone f).toCone.π.app { as := j✝¹ } ≫ p j✝¹ =
    p j✝ ≫ (bicone g).toCocone.ι.app { as := j✝ } ≫ (bicone g).toCone.π.app { as := j✝¹ }

Tactic:
dsimp

Goal state after:
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f g : J → C
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct g
p : (b : J) → f b ⟶ g b
j✝¹ j✝ : J
⊢ ι f j✝ ≫ π f j✝¹ ≫ p j✝¹ = p j✝ ≫ ι g j✝ ≫ π g j✝¹
Module: Mathlib.CategoryTheory.Preadditive.AdditiveFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (F.map f' + F.map g') = (F ⋙ G).map (f' + g')

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} E
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
inst✝⁴ : Preadditive E
F : C ⥤ D
inst✝³ : F.Additive
inst✝² : F.Full
inst✝¹ : F.EssSurj
G : D ⥤ E
inst✝ : (F ⋙ G).Additive
X Y : D
f g : X ⟶ Y
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = (F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv
g' : F.objPreimage X ⟶ F.objPreimage Y
hg' : F.map g' = (F.objObjPreimageIso X).hom ≫ g ≫ (F.objObjPreimageIso Y).inv
⊢ G.map (F.map f' + F.map g') = G.map (F.map (f' + g'))