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

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type v₁
f : Y ⟶ Z
g : ((coyoneda.rightOp ⋙ coyoneda).obj X).obj Y
⊢ (ConcreteCategory.hom
          (((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
      g =
    (ConcreteCategory.hom
          ((coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
            ((evaluation C (Type v₁) ⋙
                      (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
                  X).map
              f)).toFun
      g

Tactic:
rw [← ULift.down_inj]

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type v₁
f : Y ⟶ Z
g : ((coyoneda.rightOp ⋙ coyoneda).obj X).obj Y
⊢ ((ConcreteCategory.hom
            (((coyoneda.rightOp ⋙ coyoneda).obj X).map f ≫ (coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
        g).down =
    ((ConcreteCategory.hom
            ((coyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
              ((evaluation C (Type v₁) ⋙
                        (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).obj
                    X).map
                f)).toFun
        g).down
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type v₁
g : ((coyoneda.rightOp ⋙ coyoneda).obj Y).obj F
⊢ (ConcreteCategory.hom
          (((coyoneda.rightOp ⋙ coyoneda).map f ≫
                (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
            F)).toFun
      g =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                (evaluation C (Type v₁) ⋙
                      (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
                  f).app
            F)).toFun
      g

Tactic:
rw [← ULift.down_inj]

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type v₁
g : ((coyoneda.rightOp ⋙ coyoneda).obj Y).obj F
⊢ ((ConcreteCategory.hom
            (((coyoneda.rightOp ⋙ coyoneda).map f ≫
                  (NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
              F)).toFun
        g).down =
    ((ConcreteCategory.hom
            (((NatIso.ofComponents (fun x ↦ (coyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                  (evaluation C (Type v₁) ⋙
                        (whiskeringRight (C ⥤ Type v₁) (Type v₁) (Type (max u₁ v₁))).obj uliftFunctor.{u₁, v₁}).map
                    f).app
              F)).toFun
        g).down
Module: Mathlib.CategoryTheory.EssentiallySmall

Goal state before:
pp: case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
e : C ≌ D
⊢ EssentiallySmall.{w, v, u} C → EssentiallySmall.{w, v', u'} D

Tactic:
rintro ⟨S, 𝒮, ⟨f⟩⟩
    exact EssentiallySmall.mk' (e.symm.trans f)

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type (max w v₁)
f : Y ⟶ Z
g : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).obj Y
⊢ (ConcreteCategory.hom
          (((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).map f ≫
            (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
      g =
    (ConcreteCategory.hom
          ((uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
            ((evaluation C (Type (max v₁ w)) ⋙
                      (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                        uliftFunctor.{u₁, max v₁ w}).obj
                  X).map
              f)).toFun
      g

Tactic:
rw [← ULift.down_inj]

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
Y Z : C ⥤ Type (max w v₁)
f : Y ⟶ Z
g : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).obj Y
⊢ ((ConcreteCategory.hom
            (((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj X).map f ≫
              (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom)).toFun
        g).down =
    ((ConcreteCategory.hom
            ((uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫
              ((evaluation C (Type (max v₁ w)) ⋙
                        (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                          uliftFunctor.{u₁, max v₁ w}).obj
                    X).map
                f)).toFun
        g).down
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type (max w v₁)
g : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj Y).obj F
⊢ (ConcreteCategory.hom
          (((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).map f ≫
                (NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
            F)).toFun
      g =
    (ConcreteCategory.hom
          (((NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                (evaluation C (Type (max v₁ w)) ⋙
                      (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                        uliftFunctor.{u₁, max v₁ w}).map
                  f).app
            F)).toFun
      g

Tactic:
rw [← ULift.down_inj]

Goal state after:
C✝ : Type u₁
inst✝¹ : Category.{v₁, u₁} C✝
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Y Z : C
f : Y ⟶ Z
F : C ⥤ Type (max w v₁)
g : ((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).obj Y).obj F
⊢ ((ConcreteCategory.hom
            (((uliftCoyoneda.{w, v₁, u₁}.rightOp ⋙ coyoneda).map f ≫
                  (NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom).app
              F)).toFun
        g).down =
    ((ConcreteCategory.hom
            (((NatIso.ofComponents (fun x ↦ (uliftCoyonedaEquiv.trans Equiv.ulift.symm).toIso) ⋯).hom ≫
                  (evaluation C (Type (max v₁ w)) ⋙
                        (whiskeringRight (C ⥤ Type (max v₁ w)) (Type (max v₁ w)) (Type (max (max w u₁) v₁))).obj
                          uliftFunctor.{u₁, max v₁ w}).map
                    f).app
              F)).toFun
        g).down
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right }))
    (m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    m ≫ c.fst ≫ f = s.fst → m ≫ c.snd = s.snd → m = IsLimit.lift h (s.fst ≫ inv f) s.snd

Tactic:
· intro s m e₁ e₂
    apply BinaryFan.IsLimit.hom_ext h
    · simpa
    · simpa

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

Goal state before:
pp: case left
⊢ (match one with
    | zero => one
    | one => zero) ⟶
    match zero with
    | zero => one
    | one => zero

pp: case right
⊢ (match one with
    | zero => one
    | one => zero) ⟶
    match zero with
    | zero => one
    | one => zero

pp: case id
X✝ : WalkingParallelPair
⊢ (match X✝ with
    | zero => one
    | one => zero) ⟶
    match X✝ with
    | zero => one
    | one => zero

Tactic:
exacts [left, right, WalkingParallelPairHom.id _]

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

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : T ⥤ D
G : D ⥤ E
X✝ Y✝ : Under X
f : X✝ ⟶ Y✝
⊢ Hom.right ((post (F ⋙ G)).map f ≫ (Iso.refl ((post (F ⋙ G)).obj Y✝)).hom) =
    Hom.right ((Iso.refl ((post (F ⋙ G)).obj X✝)).hom ≫ (post F ⋙ post G).map f)

Tactic:
dsimp only [Iso.refl_hom, Under.comp_right, Under.id_right]

Goal state after:
T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
E : Type u_1
inst✝ : Category.{v_1, u_1} E
F : T ⥤ D
G : D ⥤ E
X✝ Y✝ : Under X
f : X✝ ⟶ Y✝
⊢ Hom.right ((post (F ⋙ G)).map f) ≫ 𝟙 ((post (F ⋙ G)).obj Y✝).right =
    𝟙 ((post (F ⋙ G)).obj X✝).right ≫ Hom.right ((post F ⋙ post G).map f)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ t.snd = k ≫ t.snd
⊢ h ≫ t.fst ≫ f = k ≫ t.fst ≫ f

Tactic:
condition

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
t : PullbackCone f g
ht : IsLimit t
inst✝ : Mono f
W : C
h k : W ⟶ t.pt
i : h ≫ t.snd = k ≫ t.snd
⊢ h ≫ t.snd ≫ g = k ≫ t.snd ≫ g
Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers

Goal state before:
pp: C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
p : F.obj zero ⟶ G.obj zero
q : F.obj one ⟶ G.obj one
hl : F.map left ≫ q = p ≫ G.map left
hr : F.map right ≫ q = p ≫ G.map right
⊢ ∀ ⦃X Y : WalkingParallelPair⦄ (f : X ⟶ Y),
    F.map f ≫ WalkingParallelPair.casesOn Y p q = WalkingParallelPair.casesOn X p q ≫ G.map f

Tactic:
by rintro _ _ (_ | _); all_goals cat_disch

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 : WalkingParallelPair ⥤ C
p : F.obj zero ≅ G.obj zero
q : F.obj one ≅ G.obj one
hl : F.map left ≫ q.hom = p.hom ≫ G.map left
hr : F.map right ≫ q.hom = p.hom ≫ G.map right
⊢ ∀ {X Y : WalkingParallelPair} (f : X ⟶ Y),
    F.map f ≫ (WalkingParallelPair.casesOn Y p q).hom = (WalkingParallelPair.casesOn X p q).hom ≫ G.map f

Tactic:
by rintro _ _ (_ | _); all_goals cat_disch

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

Goal state before:
pp: case zero
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero

pp: case one
C : Type u
X Y : C
inst✝ : Category.{v, u} C
F G : WalkingParallelPair ⥤ C
zero : F.obj WalkingParallelPair.zero ≅ G.obj WalkingParallelPair.zero
one : F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one
left : F.map WalkingParallelPairHom.left ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.left
right : F.map WalkingParallelPairHom.right ≫ one.hom = zero.hom ≫ G.map WalkingParallelPairHom.right
⊢ F.obj WalkingParallelPair.one ≅ G.obj WalkingParallelPair.one

Tactic:
exacts [zero, one]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : HasZeroObject C
f : 0 ⟶ 0
⊢ IsIso f

Tactic:
convert! show IsIso (𝟙 (0 : C)) by infer_instance
  subsingleton

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 : Cofork f g
⊢ s.ι.app zero = g ≫ s.π

Tactic:
rw [← s.app_one_eq_π, ← s.w right, parallelPair_map_right]

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✝¹ : HasCoequalizer f g
X' Y' Z : C
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
h : Y' ⟶ Z
wh : f' ≫ h = g' ≫ h
⊢ (parallelPairHom f g f' g' p q wf wg).app one ≫ colimit.ι (parallelPair f' g') one ≫ desc h wh = q ≫ h

Tactic:
parallelPairHom_app_one,

Goal state after:
C : Type u
X Y : C
inst✝² : Category.{v, u} C
f g : X ⟶ Y
inst✝¹ : HasCoequalizer f g
X' Y' Z : C
f' g' : X' ⟶ Y'
inst✝ : HasCoequalizer f' g'
p : X ⟶ X'
q : Y ⟶ Y'
wf : f ≫ q = p ≫ f'
wg : g ≫ q = p ≫ g'
h : Y' ⟶ Z
wh : f' ≫ h = g' ≫ h
⊢ q ≫ colimit.ι (parallelPair f' g') one ≫ desc h wh = q ≫ h
Module: Mathlib.CategoryTheory.Linear.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
⊢ ∀ (x y : X ⟶ Y), leftComp S Z (x + y) = leftComp S Z x + leftComp S Z y

Tactic:
by
    intros
    ext
    simp

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
S : Type w
inst✝¹ : CommSemiring S
inst✝ : Linear S C
X Y Z : C
⊢ ∀ (m : S) (x : X ⟶ Y), leftComp S Z (m • x) = (RingHom.id S) m • leftComp S Z x

Tactic:
by
    intros
    ext
    simp

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
P✝ Q✝ R : C
f✝ f' : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R
P Q : C
f : P ⟶ Q
inst✝ : Mono f
Z✝ : C
g g' : Z✝ ⟶ P
H : g ≫ (-f) = g' ≫ (-f)
⊢ g = g'

Tactic:
by rwa [comp_neg, comp_neg, ← neg_comp, ← neg_comp, cancel_mono, neg_inj] at H

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : KernelFork (f - g)
i : IsLimit c
s : Fork f g
m✝ : s.pt ⟶ (forkOfKernelFork c).pt
h : m✝ ≫ (forkOfKernelFork c).ι = s.ι
⊢ m✝ = i.lift (kernelForkOfFork s)

Tactic:
apply Fork.IsLimit.hom_ext i; cat_disch

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
s : Fork (f - g) 0
m✝ : s.pt ⟶ (kernelForkOfFork c).pt
h : m✝ ≫ Fork.ι (kernelForkOfFork c) = s.ι
⊢ m✝ = i.lift (forkOfKernelFork s)

Tactic:
apply Fork.IsLimit.hom_ext i; cat_disch

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

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : WidePullbackShape J
⊢ Finset (j ⟶ none)

Tactic:
obtain - | j := j

Goal state after:
case none.none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
⊢ Finset (none ⟶ none)

case none.some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j : J
⊢ Finset (some j ⟶ none)
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : Type v
j j' : WidePushoutShape J
⊢ Finset (j ⟶ j')

Tactic:
obtain - | j := j

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
⊢ Finset (none ⟶ j')

case some
C : Type u
inst✝ : Category.{v, u} C
J : Type v
j' : WidePushoutShape J
j : J
⊢ Finset (some j ⟶ j')
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ (iso G X Y).inv ≫ G.map prod.fst = prod.fst

Tactic:
← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y),

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ (iso G X Y).hom ≫ (iso G X Y).inv ≫ G.map prod.fst = (iso G X Y).hom ≫ prod.fst
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ (iso G X Y).inv ≫ G.map prod.snd = prod.snd

Tactic:
← Iso.cancel_iso_hom_left (PreservesLimitPair.iso G X Y),

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y : C
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ (iso G X Y).hom ≫ (iso G X Y).inv ≫ G.map prod.snd = (iso G X Y).hom ≫ prod.snd
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: 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
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
j : J
⊢ (F.map (lift g) ≫ (F.mapBiproduct f).hom) ≫ π (F.obj ∘ f) j = (lift fun j ↦ F.map (g j)) ≫ π (F.obj ∘ f) j

Tactic:
dsimp only [Function.comp_def]

Goal state after:
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
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → W ⟶ f j
j : J
⊢ (F.map (lift g) ≫ (F.mapBiproduct f).hom) ≫ π (fun x ↦ F.obj (f x)) j =
    (lift fun j ↦ F.map (g j)) ≫ π (fun x ↦ F.obj (f x)) j
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts

Goal state before:
pp: 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
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
⊢ ι (F.obj ∘ f) j ≫ (F.mapBiproduct f).inv ≫ F.map (desc g) = ι (F.obj ∘ f) j ≫ desc fun j ↦ F.map (g j)

Tactic:
dsimp only [Function.comp_def]

Goal state after:
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
inst✝¹ : HasBiproduct f
inst✝ : PreservesBiproduct f F
W : C
g : (j : J) → f j ⟶ W
j : J
⊢ ι (fun x ↦ F.obj (f x)) j ≫ (F.mapBiproduct f).inv ≫ F.map (desc g) =
    ι (fun x ↦ F.obj (f x)) j ≫ desc fun j ↦ F.map (g j)
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : X ⟶ Z
i : Z ≅ Y
h : l ≫ i.hom = f
s✝ : KernelFork f
hs : IsLimit s✝
s : Fork l 0
⊢ s.ι ≫ f = 0

Tactic:
simp [← h]

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

Goal state before:
pp: 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
⊢ l ≫ f = 0

Tactic:
simp [← h]

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
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct fun j ↦ G.obj (f j)
inst✝ : PreservesColimit (Discrete.functor f) G
⊢ IsIso (sigmaComparison G f)

Tactic:
rw [← PreservesCoproduct.inv_hom]

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
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct fun j ↦ G.obj (f j)
inst✝ : PreservesColimit (Discrete.functor f) G
⊢ IsIso (PreservesCoproduct.iso G f).inv
Module: Mathlib.CategoryTheory.Limits.Shapes.Kernels

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
Z : C
l : Z ⟶ X
i : Z ≅ kernel f
h : i.hom ≫ ι f = l
⊢ l ≫ f = 0

Tactic:
simp [← h]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝¹ : HasCokernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasCokernel f'
p : X ⟶ X'
q : Y ⟶ Y'
w : f ≫ q = p ≫ f'
⊢ (f ≫ q) ≫ π f' = (p ≫ f') ≫ π f'

Tactic:
apply congrArg (· ≫ π f') w

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
Z : C
l : Z ⟶ Y
i : X ≅ Z
h : i.hom ≫ l = f
s✝ : CokernelCofork f
hs : IsColimit s✝
s : Cofork l 0
⊢ f ≫ s.π = 0

Tactic:
simp [← h]

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

Goal state before:
pp: 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
⊢ f ≫ l = 0

Tactic:
simp [← h]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasCokernel f
Z : C
l : Y ⟶ Z
i : cokernel f ≅ Z
h : π f ≫ i.hom = l
⊢ f ≫ l = 0

Tactic:
simp [← h]

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

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Fork (π f i) 0
j : J
⊢ s.ι ≫ (map fun j ↦ if j ≠ i then 𝟙 (f j) else 0) ≫ π f j = s.ι ≫ π f j

Tactic:
biproduct.map_π

Goal state after:
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Fork (π f i) 0
j : J
⊢ (s.ι ≫ π f j ≫ if j ≠ i then 𝟙 (f j) else 0) = s.ι ≫ π f j
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Cofork (ι f i) 0
j : J
⊢ ι f j ≫ Cofork.π (CokernelCofork.ofπ (toSubtype f fun j ↦ j ≠ i) ⋯) ≫ (fromSubtype f fun j ↦ j ≠ i) ≫ s.π =
    ι f j ≫ s.π

Tactic:
CokernelCofork.π_ofπ,

Goal state after:
J✝ : Type w
C✝ : Type uC
inst✝⁷ : Category.{uC', uC} C✝
inst✝⁶ : HasZeroMorphisms C✝
D : Type uD
inst✝⁵ : Category.{uD', uD} D
inst✝⁴ : HasZeroMorphisms D
F : J✝ → C✝
J : Type w
K : Type u_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
f : J → C
i : J
inst✝¹ : HasBiproduct f
inst✝ : HasBiproduct (Subtype.restrict (fun j ↦ j ≠ i) f)
s : Cofork (ι f i) 0
j : J
⊢ ι f j ≫ (toSubtype f fun j ↦ j ≠ i) ≫ (fromSubtype f fun j ↦ j ≠ i) ≫ s.π = ι f j ≫ s.π