mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Colimit.DirectLimit

Goal state before:
pp: R : Type u_1
ι : Type u_2
inst✝¹¹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝¹⁰ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁹ : (i : ι) → FunLike (H i) (G i) C
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (G i)
inst✝⁴ : (i : ι) → Algebra R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : Semiring P
inst✝ : Algebra R P
g : (i : ι) → G i →ₐ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
r : R
i : ι := Classical.arbitrary ι
⊢ DirectLimit.lift f (fun x1 x2 ↦ (g x1) x2) ⋯ ⟦⟨i, (algebraMap R (G i)) r⟩⟧ = (algebraMap R P) r

Tactic:
lift_def,

Goal state after:
R : Type u_1
ι : Type u_2
inst✝¹¹ : Preorder ι
G : ι → Type u_3
H : ι → Type u_4
C : Type u_5
T : ⦃i j : ι⦄ → i ≤ j → Type u_6
f : (x x_1 : ι) → (h : x ≤ x_1) → T h
inst✝¹⁰ : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)
inst✝⁹ : (i : ι) → FunLike (H i) (G i) C
inst✝⁸ : DirectedSystem G fun x1 x2 x3 ↦ ⇑(f x1 x2 x3)
inst✝⁷ : IsDirectedOrder ι
inst✝⁶ : CommSemiring R
inst✝⁵ : (i : ι) → Semiring (G i)
inst✝⁴ : (i : ι) → Algebra R (G i)
inst✝³ : ∀ (i j : ι) (h : i ≤ j), AlgHomClass (T h) R (G i) (G j)
inst✝² : Nonempty ι
P : Type u_7
inst✝¹ : Semiring P
inst✝ : Algebra R P
g : (i : ι) → G i →ₐ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
r : R
i : ι := Classical.arbitrary ι
⊢ (g ⟨i, (algebraMap R (G i)) r⟩.fst) ⟨i, (algebraMap R (G i)) r⟩.snd = (algebraMap R P) r
Module: Mathlib.Data.List.Sym

Goal state before:
pp: case mp
α : Type u_1
xs : List α
a b : α
h : s(a, b) ∈ xs.sym2
⊢ a ∈ xs ∧ b ∈ xs

Tactic:
exact ⟨left_mem_of_mk_mem_sym2 h, right_mem_of_mk_mem_sym2 h⟩

Goal state after:
Module: Mathlib.Data.Finset.Sym

Goal state before:
pp: α : Type u_1
β : Type u_2
s t : Finset α
a b : α
inst✝ : DecidableEq α
n : ℕ
h : a ∉ s
m : ↥((insert a s).sym n)
⊢ s = (insert a s).erase a

Tactic:
rw [erase_insert h]

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
z : Sym2 α
h : z.IsDiag
⊢ diag (z.diagElem h) = z

Tactic:
cases z; cases h; rfl

Goal state after:
Module: Mathlib.Data.Sym.Sym2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
z✝ : Sym2 α
f : α → β
inst✝ : DecidableEq α
a : α
z : Sym2 α
h : a ∈ z
⊢ ∀ (a_1 b c d : α) (h : Rel α (a_1, b) (c, d)),
    Eq.ndrec (motive := fun x ↦ a ∈ x → α) (fun x ↦ if a = a_1 then b else a_1) ⋯ = fun x ↦ if a = c then d else c

Tactic:
by
    clear h z
    intro b c d e h
    ext hy
    have {f g h} : @Eq.ndrec (Sym2 α) s(b, c)
      (fun x => a ∈ x → α) (fun _ => if a = b then c else b) f g h =
        if a = b then c else b := by subst g; rfl
    aesop

Goal state after:
Module: Mathlib.Logic.Lemmas

Goal state before:
pp: f : Prop → Prop
x✝ : ∃ p, f p
p : Prop
h : f p
⊢ f True ∨ f False

Tactic:
refine (em p).imp ?_ ?_ <;> intro H <;> convert! h <;> simp [H]

Goal state after:
Module: Mathlib.CategoryTheory.Opposites

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X✝ Y✝ : C
X Y : Cᵒᵖ
f : X ≅ Y
⊢ f.hom.unop ≫ f.inv.unop = 𝟙 (Opposite.unop Y)

Tactic:
simp only [← unop_comp, f.inv_hom_id, unop_id]

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

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ Hom.left (e.inv ≫ e.hom) = 𝟙 g.left

Tactic:
e.inv_hom_id,

Goal state after:
T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
e : f ≅ g
⊢ Hom.left (𝟙 g) = 𝟙 g.left
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'
X Y : Comma L R
φ : X ⟶ Y
⊢ α.app X.left ≫ (L ⋙ F).map φ.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ β.app X.right ≫ (F₂ ⋙ R').map φ.right

Tactic:
← β.naturality

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'
X Y : Comma L R
φ : X ⟶ Y
⊢ α.app X.left ≫ (L ⋙ F).map φ.left ≫ F.map Y.hom ≫ β.app Y.right =
    α.app X.left ≫ F.map X.hom ≫ (R ⋙ F).map φ.right ≫ β.app Y.right
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ∀ {X Y : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)} (f : X ⟶ Y),
    (yonedaPairing C).map f ≫ (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom =
      (yonedaEquiv.trans Equiv.ulift.symm).toIso.hom ≫ (yonedaEvaluation C).map f

Tactic:
by intro (X, F) (Y, G) f
        ext (a : yoneda.obj X.unop ⟶ F)
        apply ULift.ext
        dsimp [yonedaEvaluation, yonedaEquiv]
        simp [← NatTrans.naturality_apply]

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
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✝ F : J ⥤ C
⊢ ((↾fun c ↦ ⟨op c.pt, c.π⟩) ≫ ↾fun c ↦ { pt := unop c.fst, π := c.snd }) = 𝟙 (Cone F)

Tactic:
ext X
    cases X
    rfl

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

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
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✝ F : J ⥤ C
⊢ ((↾fun c ↦ ⟨c.pt, c.ι⟩) ≫ ↾fun c ↦ { pt := c.fst, ι := c.snd }) = 𝟙 (Cocone F)

Tactic:
ext X
    cases X
    rfl

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

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasColimitsOfSize.{v₁, u₁, v, u} C
J : Type u₂
inst✝² : Category.{v₂, u₂} J
inst✝¹ : Small.{u₁, u₂} J
inst✝ : LocallySmall.{v₁, v₂, u₂} J
⊢ HasColimitsOfShape J C

Tactic:
have := HasColimitsOfSize.has_colimits_of_shape (C := C) (ShrinkHoms (Shrink.{u₁} J))
  exact hasColimitsOfShape_of_equivalence
    ((ShrinkHoms.equivalence _).symm.trans (Shrink.equivalence _).symm)

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ c.fst = 𝟙 X
⊢ (c.fst ≫ l) ≫ c.fst = 𝟙 (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }) ≫ c.fst

Tactic:
by simpa [hl, -Category.comp_id] using Category.comp_id _

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
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
A : Type u₃
inst✝¹ : Category.{v₃, u₃} A
B : Type u₄
inst✝ : Category.{v₄, u₄} B
L : D
R : C ⥤ D
L' : B
R' : A ⥤ B
F : C ⥤ A
G : D ⥤ B
α : L' ⟶ G.obj L
β : R ⋙ G ⟶ F ⋙ R'
F' : C ⥤ A
G' : D ⥤ B
e₁ : F ≅ F'
e₂ : G ≅ G'
α' : L' ⟶ G'.obj L
β' : R ⋙ G' ⟶ F' ⋙ R'
hα : α = α' ≫ e₂.inv.app L
hβ : β ≫ Functor.whiskerRight e₁.hom R' = R.whiskerLeft e₂.hom ≫ β'
X : StructuredArrow L R
⊢ ((map₂ α β).obj X).hom ≫ R'.map (e₁.app X.right).hom = ((map₂ α' β').obj X).hom

Tactic:
subst hα
    simp [dsimp% congr($(hβ).app X.right)]

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✝ : Over X
φ : f✝ ⟶ g✝
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
⊢ l ≫ f.hom = m ≫ f.hom

Tactic:
rw [← Over.w k, ← Category.assoc, congrArg (· ≫ g.hom) a, Category.assoc]

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 : Over X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : D ⟶ (Functor.const J).obj X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
⊢ hc.lift ((forget X).mapCone t) ≫ (liftCone D s c p hp).pt.hom = t.pt.hom

Tactic:
by
    let j : J := Classical.arbitrary _
    simp [← hp j, dsimp% (t.π.app j).w, dsimp% hc.fac_assoc ((forget X).mapCone t) j]

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
T : D
S : C ⥤ D
X Y : CostructuredArrow S T
h : X = Y
⊢ (eqToHom h).left = eqToHom ⋯

Tactic:
subst h
  simp only [eqToHom_refl, id_left]

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
T T' T'' : D
Y Y' Y'' : C
S S' : C ⥤ D
f f' : CostructuredArrow S T
g : f.left ≅ f'.left
w : S.map g.hom ≫ f'.hom = f.hom
⊢ S.map g.hom ≫ f'.hom = f.hom ≫ (Functor.fromPUnit T).map (eqToIso ⋯).hom

Tactic:
by simpa using w

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
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
⊢ IsZero F

Tactic:
constructor <;> intro G

Goal state after:
case unique_to
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ Nonempty (Unique (F ⟶ G))

case unique_from
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F : C ⥤ D
hF : ∀ (X : C), IsZero (F.obj X)
G : C ⥤ D
⊢ Nonempty (Unique (G ⟶ F))
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 : Y ⟶ X
⊢ f ≫ 0 = default

Tactic:
comp_zero,

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
inst✝¹ : HasInitial C
inst✝ : HasInitial D
f : ⊥_ D ⟶ G.obj (⊥_ C)
i : IsIso f
⊢ PreservesColimit (Functor.empty C) G

Tactic:
by
  rw [Subsingleton.elim f (initialComparison G)] at i
  exact PreservesInitial.of_iso_comparison G

Goal state after:
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
β : Type u'
inst✝¹ : HasZeroMorphisms C
f : β → C
inst✝ : HasLimit (Discrete.functor f)
b : β
⊢ IsSplitEpi (Pi.π f b)

Tactic:
by
  classical exact IsSplitEpi.mk' { section_ := Pi.lift <| Pi.single b (𝟙 _) }

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

Tactic:
comp_zero,

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
J✝ : Type v
J : Type
inst✝¹ : Finite J
inst✝ : HasFiniteWidePullbacks C
⊢ HasLimitsOfShape (WidePullbackShape J) C

Tactic:
by
  have := @HasFiniteWidePullbacks.out C _ _ J
  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
c : KernelFork f
hc : IsLimit c
inst✝ : Mono f
this : Mono (Fork.ι c)
⊢ 𝟙 c.pt ≫ 0 = 0 ≫ 0

Tactic:
comp_zero,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : KernelFork f
hc : IsLimit c
inst✝ : Mono f
this : Mono (Fork.ι c)
⊢ 0 = 0 ≫ 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 : CokernelCofork h
⊢ f ≫ Cofork.π s = 0 ≫ Cofork.π s

Tactic:
rw [← cancel_epi g, ← Category.assoc, ← 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✝
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hf : Epi f
h : IsZero c.pt
s : CokernelCofork f
⊢ Cofork.π c ≫ 0 = Cofork.π s

Tactic:
comp_zero,

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 : CokernelCofork f
hf : Epi f
h : IsZero c.pt
s : CokernelCofork f
⊢ 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✝
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hf : Epi f
h : IsZero c.pt
s : CokernelCofork f
⊢ f ≫ 0 = f ≫ Cofork.π s

Tactic:
comp_zero,

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 : CokernelCofork f
hf : Epi f
h : IsZero c.pt
s : CokernelCofork f
⊢ 0 = f ≫ 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
c : CokernelCofork f
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ 0 ≫ 𝟙 c.pt = f ≫ Cofork.π c ≫ 0

Tactic:
comp_zero,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ 0 ≫ 𝟙 c.pt = 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
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ 0 ≫ 𝟙 c.pt = f ≫ 0

Tactic:
comp_zero,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
inst✝ : Epi f
this : Epi (Cofork.π c)
⊢ 0 ≫ 𝟙 c.pt = 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
f : J → C
t : Bicone f
ht : IsLimit t.toCone
j : J
j' : Discrete J
⊢ t.ι j ≫ t.toCone.π.app j' = ht.lift (Fan.mk (f j) fun j' ↦ if h : j = j' then eqToHom ⋯ else 0) ≫ t.toCone.π.app j'

Tactic:
rw [ht.fac]
    simp [t.ι_π]

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
f : J → C
t : Bicone f
ht : IsColimit t.toCocone
j : J
j' : Discrete J
⊢ t.toCocone.ι.app j' ≫ t.π j =
    t.toCocone.ι.app j' ≫ ht.desc (Cofan.mk (f j) fun j' ↦ if h : j' = j then eqToHom ⋯ else 0)

Tactic:
rw [ht.fac]
    simp [t.ι_π]

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
m : (CokernelCofork.ofπ (Cofork.π s✝) ⋯).pt ⟶ s.pt
h : Cofork.π (CokernelCofork.ofπ (Cofork.π s✝) ⋯) ≫ m = s.π
⊢ m = hs.desc (CokernelCofork.ofπ s.π ⋯)

Tactic:
by
      apply Cofork.IsColimit.hom_ext hs
      simpa using h

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

Goal state before:
pp: case pos
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
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasBiproduct (g i)
inst✝ : HasBiproduct fun i ↦ ⨁ g i
x✝¹ x✝ : (i : ι) × f i
j : ι
x : f j
j' : ι
y : f j'
h : ⟨j, x⟩ = ⟨j', y⟩
⊢ (biproduct.ι (g ⟨j, x⟩.fst) ⟨j, x⟩.snd ≫ biproduct.ι (fun i ↦ ⨁ g i) ⟨j, x⟩.fst) ≫
      biproduct.π (fun i ↦ ⨁ g i) ⟨j', y⟩.fst ≫ biproduct.π (g ⟨j', y⟩.fst) ⟨j', y⟩.snd =
    eqToHom ⋯

Tactic:
obtain ⟨rfl, rfl⟩ := h

Goal state after:
case pos
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
ι : Type u_3
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasBiproduct (g i)
inst✝ : HasBiproduct fun i ↦ ⨁ g i
x✝¹ x✝ : (i : ι) × f i
j : ι
x : f j
⊢ (biproduct.ι (g ⟨j, x⟩.fst) ⟨j, x⟩.snd ≫ biproduct.ι (fun i ↦ ⨁ g i) ⟨j, x⟩.fst) ≫
      biproduct.π (fun i ↦ ⨁ g i) ⟨j, x⟩.fst ≫ biproduct.π (g ⟨j, x⟩.fst) ⟨j, x⟩.snd =
    eqToHom ⋯
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : ¬p j
⊢ (if h : ↑i = j then eqToHom ⋯ else 0) = ι (Subtype.restrict p f) i ≫ 0

Tactic:
dif_neg (show (i : J) ≠ j from fun h₂ => h (h₂ ▸ i.2)),

Goal state after:
case neg
J : Type w
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
f : J → C
inst✝² : HasBiproduct f
p : J → Prop
inst✝¹ : HasBiproduct (Subtype.restrict p f)
inst✝ : DecidablePred p
j : J
i : Subtype p
h : ¬p j
⊢ 0 = ι (Subtype.restrict p f) i ≫ 0
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

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
P P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
as : WalkingPair
⊢ b.toBicone.toCone.π.app { as := as } = (Iso.refl b.toBicone.toCone.pt).hom ≫ b.toCone.π.app { as := as }

Tactic:
by cases as <;> simp

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

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
P P' Q Q' X Y : C
b : BinaryBicone X Y
x✝ : Discrete WalkingPair
as : WalkingPair
⊢ b.toBicone.toCocone.ι.app { as := as } ≫ (Iso.refl b.toBicone.toCocone.pt).hom = b.toCocone.ι.app { as := as }

Tactic:
by cases as <;> simp

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

Goal state before:
pp: case inl
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
⊢ s.ι ≫ π f i ≫ 0 = s.ι ≫ π f i

Tactic:
comp_zero,

Goal state after:
case inl
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
⊢ s.ι ≫ 0 = s.ι ≫ π f i
Module: Mathlib.CategoryTheory.Limits.Shapes.Biproducts

Goal state before:
pp: case inl
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
⊢ s.ι ≫ 0 = s.ι ≫ π f i

Tactic:
comp_zero,

Goal state after:
case inl
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
⊢ 0 = s.ι ≫ π f i
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

Goal state before:
pp: case h₀.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ fst = (inl ≫ map' f g) ≫ fst

pp: case h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ snd = (inl ≫ map' f g) ≫ snd

pp: case h₁.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ fst = (inr ≫ map' f g) ≫ fst

pp: case h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ snd = (inr ≫ map' f g) ≫ snd

Tactic:
· simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π,
      Category.assoc, ← BinaryBicone.toCone_π_app_left, ←
      BinaryBicone.toCocone_ι_app_left]
    simp

Goal state after:
case h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inl ≫ map f g) ≫ snd = (inl ≫ map' f g) ≫ snd

case h₁.h₀
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ fst = (inr ≫ map' f g) ≫ fst

case h₁
C : Type uC
inst✝³ : Category.{uC', uC} C
inst✝² : HasZeroMorphisms C
W X Y Z : C
inst✝¹ : HasBinaryBiproduct W X
inst✝ : HasBinaryBiproduct Y Z
f : W ⟶ Y
g : X ⟶ Z
⊢ (inr ≫ map f g) ≫ snd = (inr ≫ map' f g) ≫ snd
Module: Mathlib.CategoryTheory.Preadditive.Biproducts

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ X
hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)
⊢ (q ≫ 𝟙 X) ≫ b.inl = 0

Tactic:
← b.inl_fst,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
X✝ Y✝ : C
inst✝ : HasBinaryBiproduct X✝ Y✝
X Y : C
b : BinaryBicone X Y
hb : IsLimit b.sndKernelFork
T : C
f : T ⟶ X
g : T ⟶ Y
m : T ⟶ b.pt
h₁ : m ≫ BinaryFan.fst b.toCone = f
h₂ : m ≫ BinaryFan.snd b.toCone = g
h₁' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.fst = 0
h₂' : (m - (f ≫ b.inl + g ≫ b.inr)) ≫ b.snd = 0
q : T ⟶ X
hq : q ≫ b.inl = m - (f ≫ b.inl + g ≫ b.inr)
⊢ (q ≫ b.inl ≫ b.fst) ≫ b.inl = 0