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

Goal state before:
pp: I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ (({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
        f' ≫
      fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫ fun i ↦ f' (g (f i))

Tactic:
funext

Goal state after:
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x✝ : K
⊢ (({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
          f' ≫
        fun b ↦ 𝟙 (Y (g (f b))))
      x✝ =
    ((fun b ↦ 𝟙 (X (g (f b)))) ≫ fun i ↦ f' (g (f i))) x✝
Module: Mathlib.CategoryTheory.Pi.Basic

Goal state before:
pp: I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
⊢ ((fun i ↦ f' (g (f i))) ≫ fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫
      ({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
            { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
        f'

Tactic:
funext

Goal state after:
I : Type w₀
J✝ : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
J : Type w₁
K : Type w₂
f : K → J
g : J → I
X Y : (i : I) → C i
f' : X ⟶ Y
x✝ : K
⊢ ((fun i ↦ f' (g (f i))) ≫ fun b ↦ 𝟙 (Y (g (f b)))) x✝ =
    ((fun b ↦ 𝟙 (X (g (f b)))) ≫
        ({ obj := fun f i ↦ f (g i), map := fun {X Y} α i ↦ α (g i), map_id := ⋯, map_comp := ⋯ } ⋙
              { obj := fun f_1 i ↦ f_1 (f i), map := fun {X Y} α i ↦ α (f i), map_id := ⋯, map_comp := ⋯ }).map
          f')
      x✝
Module: Mathlib.CategoryTheory.EpiMono

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z✝ : C
g h : Y ⟶ Z✝
w : f ≫ g = f ≫ h
⊢ g = h

Tactic:
by replace w := se.section_ ≫= w; simpa using w

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.isoClosure = P ↔ P.RespectsIso

Tactic:
refine ⟨(· ▸ P.isoClosure_respectsIso), fun hP ↦ le_antisymm ?_ (P.le_isoClosure)⟩
  intro X Y f ⟨X', Y', f', hf', ⟨e⟩⟩
  exact (P.arrow_mk_iso_iff e).1 hf'

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

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ α.app X.left ≫ F.map (L.map (F₁.preimage φ.left) ≫ Y.hom) ≫ β.app Y.right =
    α.app X.left ≫ F.map (X.hom ≫ R.map (F₂.preimage φ.right)) ≫ β.app Y.right

Tactic:
F.map_comp,

Goal state after:
A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ α.app X.left ≫ (F.map (L.map (F₁.preimage φ.left)) ≫ F.map Y.hom) ≫ β.app Y.right =
    α.app X.left ≫ F.map (X.hom ≫ R.map (F₂.preimage φ.right)) ≫ β.app Y.right
Module: Mathlib.CategoryTheory.Comma.Basic

Goal state before:
pp: A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ α.app X.left ≫ (F.map (L.map (F₁.preimage φ.left)) ≫ F.map Y.hom) ≫ β.app Y.right =
    α.app X.left ≫ F.map (X.hom ≫ R.map (F₂.preimage φ.right)) ≫ β.app Y.right

Tactic:
F.map_comp,

Goal state after:
A : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁹ : Category.{v₂, u₂} B
T : Type u₃
inst✝⁸ : Category.{v₃, u₃} T
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
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
L' : A' ⥤ T'
R' : B' ⥤ T'
F₁ : A ⥤ A'
F₂ : B ⥤ B'
F : T ⥤ T'
α : F₁ ⋙ L' ⟶ L ⋙ F
β : R ⋙ F ⟶ F₂ ⋙ R'
inst✝⁴ : F.Faithful
inst✝³ : F₁.Full
inst✝² : F₂.Full
inst✝¹ : IsIso α
inst✝ : IsIso β
X Y : Comma L R
φ : (map α β).obj X ⟶ (map α β).obj Y
⊢ α.app X.left ≫ (F.map (L.map (F₁.preimage φ.left)) ≫ F.map Y.hom) ≫ β.app Y.right =
    α.app X.left ≫ (F.map X.hom ≫ F.map (R.map (F₂.preimage φ.right))) ≫ β.app Y.right
Module: Mathlib.Algebra.Category.MonCat.Basic

Goal state before:
pp: X✝ Y✝ : Type u
X Y : MonCat
f : X ⟶ Y
x✝ : IsIso ((forget MonCat).map f)
⊢ IsIso f

Tactic:
let i := asIso ((forget MonCat).map f)
    let e : X ≃* Y := { f.hom, i.toEquiv with }
    exact e.toMonCatIso.isIso_hom

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ F.map (adj.unit.app X ≫ G.map f) ≫ adj.counit.app Y = f

Tactic:
F.map_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
X : C
Y : D
f : F.obj X ⟶ Y
⊢ (F.map (adj.unit.app X) ≫ F.map (G.map f)) ≫ adj.counit.app Y = f
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)

Tactic:
← whiskerLeft_comp,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ (η.hom ≫ η.inv) = 𝟙 (f ≫ g)
Module: Mathlib.CategoryTheory.Bicategory.Basic

Goal state before:
pp: B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.inv ≫ f ◁ η.hom = 𝟙 (f ≫ h)

Tactic:
← whiskerLeft_comp,

Goal state after:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ (η.inv ≫ η.hom) = 𝟙 (f ≫ h)
Module: Mathlib.CategoryTheory.LiftingProperties.Adjunction

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
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ adj.unit.app A ≫ F.map (G.map i ≫ v) = i ≫ adj.unit.app B ≫ F.map v

Tactic:
F.map_comp,

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
G : C ⥤ D
F : D ⥤ C
A B : C
X Y : D
i : A ⟶ B
p : X ⟶ Y
u : G.obj A ⟶ X
v : G.obj B ⟶ Y
sq : CommSq u (G.map i) p v
adj : G ⊣ F
⊢ adj.unit.app A ≫ F.map (G.map i) ≫ F.map v = i ≫ adj.unit.app B ≫ F.map v
Module: Mathlib.CategoryTheory.Functor.EpiMono

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
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
inst✝² : F'.PreservesMonomorphisms
inst✝¹ : F.PreservesEpimorphisms
inst✝ : StrongEpi f
X Y : D
Z : X ⟶ Y
⊢ ∀ [Mono Z], HasLiftingProperty (F.map f) Z

Tactic:
by
    intro
    rw [adj.hasLiftingProperty_iff]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.PUnit

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
⊢ Nonempty (C ≌ Discrete PUnit.{w + 1}) → Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))

Tactic:
rintro ⟨h⟩

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
h : C ≌ Discrete PUnit.{w + 1}
⊢ Nonempty C ∧ ∀ (x y : C), Nonempty (Unique (x ⟶ y))
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cocone (Discrete.functor f)
j : Discrete β
⊢ { pt := f default,
              ι :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.ι.app
        j ≫
      s.ι.app default =
    s.ι.app j

Tactic:
by
        obtain rfl := Subsingleton.elim j default
        apply Category.id_comp

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

Goal state before:
pp: β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ⇑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' ⋯) ≫ colimit.ι (Discrete.functor f) { as := ε b } =
    colimit.ι (Discrete.functor f) { as := ε (ε.symm (ε b)) }
⊢ (Discrete.functor (f ∘ ⇑ε)).map ((Discrete.equivalence ε).unit.app { as := b }) ≫
      colimit.ι (Discrete.functor f) { as := ε (ε.symm (ε b)) } =
    ι f (ε b)

Tactic:
← h,

Goal state after:
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ⇑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' ⋯) ≫ colimit.ι (Discrete.functor f) { as := ε b } =
    colimit.ι (Discrete.functor f) { as := ε (ε.symm (ε b)) }
⊢ (Discrete.functor (f ∘ ⇑ε)).map ((Discrete.equivalence ε).unit.app { as := b }) ≫
      (Discrete.functor f).map (Discrete.eqToHom' ⋯) ≫ colimit.ι (Discrete.functor f) { as := ε b } =
    ι f (ε b)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
W : C
k l : t.pt ⟶ W
h₀ : t.inl ≫ k = t.inl ≫ l
h₁ : t.inr ≫ k = t.inr ≫ l
⊢ t.ι.app none ≫ k = t.ι.app none ≫ l

Tactic:
← t.w fst,

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
W : C
k l : t.pt ⟶ W
h₀ : t.inl ≫ k = t.inl ≫ l
h₁ : t.inr ≫ k = t.inr ≫ l
⊢ ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ k = ((span f g).map fst ≫ t.ι.app WalkingSpan.left) ≫ l
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
t : IsColimit (mk (𝟙 Y) (𝟙 Y) ⋯)
Z : C
g h : Y ⟶ Z
eq : f ≫ g = f ≫ h
⊢ g = h

Tactic:
rcases PushoutCocone.IsColimit.desc' t _ _ eq with ⟨_, rfl, rfl⟩
    rfl

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

Goal state before:
pp: i j : WalkingParallelPairᵒᵖ
f : i ⟶ j
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫ (eqToIso ⋯).hom =
    (eqToIso ⋯).hom ≫ (𝟭 WalkingParallelPairᵒᵖ).map f

Tactic:
by
      induction i with | _ i
      induction j with | _ j
      let g := f.unop
      have : f = g.op := rfl
      rw [this]
      cases i <;> cases j <;> cases g <;> rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : MonoFactorisation f
m : F.I ⟶ Y
e : X ⟶ F.I
hm : m = F.m
he : e = F.e
⊢ Mono m

Tactic:
rw [hm]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : MonoFactorisation f
m : F.I ⟶ Y
e : X ⟶ F.I
hm : m = F.m
he : e = F.e
⊢ Mono F.m
Module: Mathlib.CategoryTheory.Limits.Shapes.Images

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : Epi (image.ι f)
inst✝ : Epi (factorThruImage f)
⊢ Epi f

Tactic:
rw [← image.fac f]
  apply epi_comp

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 : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ 0 ≫ f = default

Tactic:
zero_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X : C
h : 𝟙 X = 0
Y : C
f : X ⟶ Y
⊢ 0 = default
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero

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
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.Full
X Y : C
⊢ F.map (0 ≫ F.preimage 0) = 0

Tactic:
F.map_comp,

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
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
inst✝¹ : HasZeroMorphisms E
F : C ⥤ D
inst✝ : F.Full
X Y : C
⊢ F.map 0 ≫ F.map (F.preimage 0) = 0
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
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm✝ : Mono h
s : Fork (f ≫ h) (g ≫ h)
s' : Fork f g := Fork.ofι s.ι ⋯
l : { l // l ≫ c.ι = s'.ι } := Fork.IsLimit.lift' i s'.ι ⋯
m✝ : s.pt ⟶ (Fork.ofι c.ι ⋯).pt
hm : m✝ ≫ c.ι = s.ι
⊢ m✝ ≫ c.ι = ↑l ≫ c.ι

Tactic:
rw [hm]

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
c : Fork f g
i : IsLimit c
Z : C
h : Y ⟶ Z
hm✝ : Mono h
s : Fork (f ≫ h) (g ≫ h)
s' : Fork f g := Fork.ofι s.ι ⋯
l : { l // l ≫ c.ι = s'.ι } := Fork.IsLimit.lift' i s'.ι ⋯
m✝ : s.pt ⟶ (Fork.ofι c.ι ⋯).pt
hm : m✝ ≫ c.ι = s.ι
⊢ s.ι = ↑l ≫ c.ι
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
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm✝ : Epi h
s : Cofork (h ≫ f) (h ≫ g)
s' : Cofork f g := Cofork.ofπ s.π ⋯
l : { l // c.π ≫ l = s'.π } := Cofork.IsColimit.desc' i s'.π ⋯
m✝ : (Cofork.ofπ c.π ⋯).pt ⟶ s.pt
hm : c.π ≫ m✝ = s.π
⊢ c.π ≫ m✝ = c.π ≫ ↑l

Tactic:
rw [hm]

Goal state after:
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
c : Cofork f g
i : IsColimit c
W : C
h : W ⟶ X
hm✝ : Epi h
s : Cofork (h ≫ f) (h ≫ g)
s' : Cofork f g := Cofork.ofπ s.π ⋯
l : { l // c.π ≫ l = s'.π } := Cofork.IsColimit.desc' i s'.π ⋯
m✝ : (Cofork.ofπ c.π ⋯).pt ⟶ s.pt
hm : c.π ≫ m✝ = s.π
⊢ s.π = c.π ≫ ↑l
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)
⊢ Fork.ι c ≫ f = Fork.ι c ≫ g

Tactic:
by rw [← sub_eq_zero, ← comp_sub, c.condition]

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 : Cofork f g
⊢ f ≫ c.π - g ≫ c.π = 0 ≫ c.π

Tactic:
zero_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ f ≫ c.π - g ≫ c.π = 0
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
ι : Type w
inst✝ : Finite ι
⊢ HasLimitsOfShape (Discrete ι) C

Tactic:
rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
⊢ HasLimitsOfShape (Discrete ι) C
Module: Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
ι : Type w
inst✝ : Finite ι
⊢ HasColimitsOfShape (Discrete ι) C

Tactic:
rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteCoproducts C
ι : Type w
inst✝ : Finite ι
n : ℕ
e : ι ≃ Fin n
⊢ HasColimitsOfShape (Discrete ι) C
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
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
⊢ ∀ (j : Discrete WalkingPair),
    ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).π.app j =
      (Iso.refl ((Cone.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).pt).hom ≫
        (BinaryFan.mk (G.map f) (G.map g)).π.app j

Tactic:
rintro (_ | _) <;> simp

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
P : C
ι ι' : P ⟶ X
w : ι ≫ f = 0
h : ι = ι'
⊢ ι' ≫ f = 0

Tactic:
← h,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
P : C
ι ι' : P ⟶ X
w : ι ≫ f = 0
h : ι = ι'
⊢ ι ≫ f = 0
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
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
⊢ ∀ (j : Discrete WalkingPair),
    ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).ι.app j ≫
        (Iso.refl
            ((Cocone.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj
                (G.mapCocone (BinaryCofan.mk f g))).pt).hom =
      (BinaryCofan.mk (G.map f) (G.map g)).ι.app j

Tactic:
rintro (_ | _) <;> simp

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
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m✝ : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m✝ ≫ Fork.ι c = s.ι
⊢ m✝ ≫ Fork.ι c = ↑l ≫ Fork.ι c

Tactic:
rw [hm]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : Fork h 0
s' : KernelFork f := Fork.ofι s.ι ⋯
l : { l // l ≫ Fork.ι c = Fork.ι s' } := KernelFork.IsLimit.lift' i (Fork.ι s') ⋯
m✝ : s.pt ⟶ (KernelFork.ofι (Fork.ι c) ⋯).pt
hm : m✝ ≫ Fork.ι c = s.ι
⊢ s.ι = ↑l ≫ Fork.ι c
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
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
⊢ Fork.ι s ≫ f ≫ g = (Fork.ι s ≫ 0) ≫ g

Tactic:
← hh

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
i : IsLimit c
Z : C
g : Y ⟶ Z
hg : Mono g
h : X ⟶ Z
hh : h = f ≫ g
s : KernelFork h
⊢ Fork.ι s ≫ h = (Fork.ι s ≫ 0) ≫ g
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✝
X Y : C
f : X ⟶ Y
c : KernelFork f
hf : Mono f
h : IsZero c.pt
s : KernelFork f
⊢ 0 ≫ Fork.ι c = Fork.ι s

Tactic:
zero_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
c : KernelFork f
hf : Mono f
h : IsZero c.pt
s : KernelFork f
⊢ 0 = Fork.ι s
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✝
X Y : C
f : X ⟶ Y
c : KernelFork f
hf : Mono f
h : IsZero c.pt
s : KernelFork f
⊢ 0 ≫ f = Fork.ι s ≫ f

Tactic:
zero_comp,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
c : KernelFork f
hf : Mono f
h : IsZero c.pt
s : KernelFork f
⊢ 0 = Fork.ι s ≫ 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
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]
  infer_instance

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
P : C
π π' : Y ⟶ P
w : f ≫ π = 0
h : π = π'
⊢ f ≫ π' = 0

Tactic:
← h,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
P : C
π π' : Y ⟶ P
w : f ≫ π = 0
h : π = π'
⊢ f ≫ π = 0
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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m✝ : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π c ≫ m✝ = s.π
⊢ Cofork.π c ≫ m✝ = Cofork.π c ≫ ↑l

Tactic:
rw [hm]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : Cofork h 0
s' : CokernelCofork f := Cofork.ofπ s.π ⋯
l : { l // Cofork.π c ≫ l = Cofork.π s' } := CokernelCofork.IsColimit.desc' i (Cofork.π s') ⋯
m✝ : (CokernelCofork.ofπ (Cofork.π c) ⋯).pt ⟶ s.pt
hm : Cofork.π c ≫ m✝ = s.π
⊢ s.π = Cofork.π c ≫ ↑l
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
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ (g ≫ f) ≫ Cofork.π s = g ≫ 0 ≫ Cofork.π s

Tactic:
← hh

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
i : IsColimit c
W : C
g : W ⟶ X
hg : Epi g
h : W ⟶ Y
hh : h = g ≫ f
s : CokernelCofork h
⊢ h ≫ Cofork.π s = g ≫ 0 ≫ Cofork.π s
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
F : MonoFactorisation f
⊢ (kernel.ι f ≫ F.e) ≫ F.m = 0 ≫ F.m

Tactic:
zero_comp,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
inst✝ : HasKernel f
F : MonoFactorisation f
⊢ (kernel.ι f ≫ F.e) ≫ F.m = 0
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 g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Mono (p j)
⊢ Mono (map p)

Tactic:
show Sigma.map p = (biproduct.isoCoproduct _).inv ≫ biproduct.map p ≫
    (biproduct.isoCoproduct _).hom by aesop

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 g : J → C
inst✝² : HasBiproduct f
inst✝¹ : HasBiproduct g
p : (j : J) → f j ⟶ g j
inst✝ : ∀ (j : J), Mono (p j)
⊢ Mono ((biproduct.isoCoproduct f).inv ≫ biproduct.map p ≫ (biproduct.isoCoproduct g).hom)