mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
⊢ map q ≫ map q' = map fun a ↦ q a ≫ q' a

Tactic:
by
  ext; simp

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
⊢ (map' id fun a ↦ 𝟙 (f a)) = 𝟙 (∐ f)

Tactic:
by
  ext; simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
p' : β → γ
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h (p' b)
⊢ map' p q ≫ map' p' q' = map' (p' ∘ p) fun a ↦ q a ≫ q' (p a)

Tactic:
by
  ext; simp

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h b
⊢ map' p q ≫ map q' = map' p fun a ↦ q a ≫ q' (p a)

Tactic:
by
  ext; simp

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g : α → C
h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h (p a)
⊢ map q ≫ map' p q' = map' p fun a ↦ q a ≫ q' a

Tactic:
by
  ext; simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : WalkingCospan ⥤ C
s t : Cone F
i : s.pt ≅ t.pt
w₁ : s.π.app left = i.hom ≫ t.π.app left
w₂ : s.π.app right = i.hom ≫ t.π.app right
⊢ s ≅ t

Tactic:
apply Cone.ext i _
  rintro (⟨⟩ | ⟨⟨⟩⟩)
  · have h₁ := s.π.naturality WalkingCospan.Hom.inl
    dsimp at h₁
    simp only [Category.id_comp] at h₁
    have h₂ := t.π.naturality WalkingCospan.Hom.inl
    dsimp at h₂
    simp only [Category.id_comp] at h₂
    simp_rw [h₂, ← Category.assoc, ← w₁, ← h₁]
  · exact w₁
  · exact w₂

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
F : D ⥤ T
Y : T
X : D
Y✝ Z✝ : StructuredArrow X (proj Y F)
m : Y✝ ⟶ Z✝
⊢ Y✝.hom ≫ (proj X (proj Y F) ⋙ proj Y F).map m = Z✝.hom

Tactic:
have := m.w

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
Y✝ Z✝ : StructuredArrow X (proj Y F)
m : Y✝ ⟶ Z✝
this : Y✝.hom ≫ (proj Y F).map (Hom.right m) = Z✝.hom
⊢ Y✝.hom ≫ (proj X (proj Y F) ⋙ proj Y F).map m = Z✝.hom
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
F : D ⥤ T
Y : T
X : D
Y✝ Z✝ : StructuredArrow Y (Under.forget X ⋙ F)
m : Y✝ ⟶ Z✝
⊢ Y✝.hom ≫ F.map ((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).map m) = Z✝.hom

Tactic:
have := m.w

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
Y✝ Z✝ : StructuredArrow Y (Under.forget X ⋙ F)
m : Y✝ ⟶ Z✝
this : Y✝.hom ≫ (Under.forget X ⋙ F).map (Hom.right m) = Z✝.hom
⊢ Y✝.hom ≫ F.map ((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).map m) = Z✝.hom
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 × T
Y✝ Z✝ : StructuredArrow X.2 (Under.forget X.1)
m : Y✝ ⟶ Z✝
⊢ (Y✝.right.hom, Y✝.hom) ≫ (Functor.diag T).map ((proj X.2 (Under.forget X.1) ⋙ Under.forget X.1).map m) =
    (Z✝.right.hom, Z✝.hom)

Tactic:
have := m.w

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : StructuredArrow X.2 (Under.forget X.1)
m : Y✝ ⟶ Z✝
this : Y✝.hom ≫ (Under.forget X.1).map (Hom.right m) = Z✝.hom
⊢ (Y✝.right.hom, Y✝.hom) ≫ (Functor.diag T).map ((proj X.2 (Under.forget X.1) ⋙ Under.forget X.1).map m) =
    (Z✝.right.hom, Z✝.hom)
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
F : T ⥤ D
Y : D
X : T
Y✝ Z✝ : CostructuredArrow (proj F Y) X
m : Y✝ ⟶ Z✝
⊢ (proj (proj F Y) X ⋙ proj F Y).map m ≫ Z✝.hom = Y✝.hom

Tactic:
have := m.w

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
Y✝ Z✝ : CostructuredArrow (proj F Y) X
m : Y✝ ⟶ Z✝
this : (proj F Y).map m.left ≫ Z✝.hom = Y✝.hom ≫ (Functor.fromPUnit X).map m.right
⊢ (proj (proj F Y) X ⋙ proj F Y).map m ≫ Z✝.hom = Y✝.hom
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
F : T ⥤ D
Y : D
X : T
Y✝ Z✝ : CostructuredArrow (Over.forget X ⋙ F) Y
m : Y✝ ⟶ Z✝
⊢ F.map ((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).map m) ≫ Z✝.hom = Y✝.hom

Tactic:
have := m.w

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
Y✝ Z✝ : CostructuredArrow (Over.forget X ⋙ F) Y
m : Y✝ ⟶ Z✝
this : (Over.forget X ⋙ F).map m.left ≫ Z✝.hom = Y✝.hom ≫ (Functor.fromPUnit Y).map m.right
⊢ F.map ((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).map m) ≫ Z✝.hom = Y✝.hom
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 × T
Y✝ Z✝ : CostructuredArrow (Over.forget X.1) X.2
m : Y✝ ⟶ Z✝
⊢ (Functor.diag T).map ((proj (Over.forget X.1) X.2 ⋙ Over.forget X.1).map m) ≫ (Z✝.left.hom, Z✝.hom) =
    (Y✝.left.hom, Y✝.hom)

Tactic:
have := m.w

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Over.forget X.1) X.2
m : Y✝ ⟶ Z✝
this : (Over.forget X.1).map m.left ≫ Z✝.hom = Y✝.hom ≫ (Functor.fromPUnit X.2).map m.right
⊢ (Functor.diag T).map ((proj (Over.forget X.1) X.2 ⋙ Over.forget X.1).map m) ≫ (Z✝.left.hom, Z✝.hom) =
    (Y✝.left.hom, Y✝.hom)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝ : Mono i
s✝ : PullbackCone f g
H : IsLimit s✝
s : PullbackCone (f ≫ i) (g ≫ i)
l : s.pt ⟶ s✝.pt
h₁ : l ≫ s✝.fst = s.fst
h₂ : l ≫ s✝.snd = s.snd
⊢ ∀ {m : s.pt ⟶ (mk s✝.fst s✝.snd ⋯).pt},
    m ≫ (mk s✝.fst s✝.snd ⋯).fst = s.fst → m ≫ (mk s✝.fst s✝.snd ⋯).snd = s.snd → m = l

Tactic:
intro m

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝ : Mono i
s✝ : PullbackCone f g
H : IsLimit s✝
s : PullbackCone (f ≫ i) (g ≫ i)
l : s.pt ⟶ s✝.pt
h₁ : l ≫ s✝.fst = s.fst
h₂ : l ≫ s✝.snd = s.snd
m : s.pt ⟶ (mk s✝.fst s✝.snd ⋯).pt
⊢ m ≫ (mk s✝.fst s✝.snd ⋯).fst = s.fst → m ≫ (mk s✝.fst s✝.snd ⋯).snd = s.snd → m = l
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
s✝ : PushoutCocone f g
H : IsColimit s✝
s : PushoutCocone (h ≫ f) (h ≫ g)
l : s✝.pt ⟶ s.pt
h₁ : s✝.inl ≫ l = s.inl
h₂ : s✝.inr ≫ l = s.inr
⊢ ∀ {m : (mk s✝.inl s✝.inr ⋯).pt ⟶ s.pt},
    (mk s✝.inl s✝.inr ⋯).inl ≫ m = s.inl → (mk s✝.inl s✝.inr ⋯).inr ≫ m = s.inr → m = l

Tactic:
intro m

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
W X Y Z : C
f✝ : X ⟶ Y
g✝ : X ⟶ Z
f : X ⟶ Y
g : X ⟶ Z
h : W ⟶ X
inst✝ : Epi h
s✝ : PushoutCocone f g
H : IsColimit s✝
s : PushoutCocone (h ≫ f) (h ≫ g)
l : s✝.pt ⟶ s.pt
h₁ : s✝.inl ≫ l = s.inl
h₂ : s✝.inr ≫ l = s.inr
m : (mk s✝.inl s✝.inr ⋯).pt ⟶ s.pt
⊢ (mk s✝.inl s✝.inr ⋯).inl ≫ m = s.inl → (mk s✝.inl s✝.inr ⋯).inr ≫ m = s.inr → m = l
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
⊢ ∀ {X_1 Y_1 Z : WalkingParallelPair} (f_1 : X_1 ⟶ Y_1) (g_1 : Y_1 ⟶ Z),
    parallelPairHom f g (f_1 ≫ g_1) = parallelPairHom f g f_1 ≫ parallelPairHom f g g_1

Tactic:
rintro _ _ _ ⟨⟩ ⟨⟩

Goal state after:
case left.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (left ≫ WalkingParallelPairHom.id one) =
    parallelPairHom f g left ≫ parallelPairHom f g (WalkingParallelPairHom.id one)

case right.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (right ≫ WalkingParallelPairHom.id one) =
    parallelPairHom f g right ≫ parallelPairHom f g (WalkingParallelPairHom.id one)

case id.left
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (WalkingParallelPairHom.id zero ≫ left) =
    parallelPairHom f g (WalkingParallelPairHom.id zero) ≫ parallelPairHom f g left

case id.right
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
⊢ parallelPairHom f g (WalkingParallelPairHom.id zero ≫ right) =
    parallelPairHom f g (WalkingParallelPairHom.id zero) ≫ parallelPairHom f g right

case id.id
C : Type u
X Y : C
inst✝ : Category.{v, u} C
f g : X ⟶ Y
X✝ : WalkingParallelPair
⊢ parallelPairHom f g (WalkingParallelPairHom.id X✝ ≫ WalkingParallelPairHom.id X✝) =
    parallelPairHom f g (WalkingParallelPairHom.id X✝) ≫ parallelPairHom f g (WalkingParallelPairHom.id X✝)
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝¹ : C
app✝¹ :
  (X : J) →
    ((Functor.const J).obj pt✝¹).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝¹).map f ≫ app✝¹ Y =
      app✝¹ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit { pt := pt✝¹, π := { app := app✝¹, naturality := naturality✝¹ } }
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶
      ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C).map f
m :
  { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.pt ⟶
    ((𝟭 C).mapCone { pt := pt✝¹, π := { app := app✝¹, naturality := naturality✝¹ } }).pt
w :
  ∀ (j : J),
    m ≫ ((𝟭 C).mapCone { pt := pt✝¹, π := { app := app✝¹, naturality := naturality✝¹ } }).π.app j =
      { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j
⊢ m =
    h.lift
      { pt := { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.pt,
        π :=
          { app := fun j ↦ { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j, naturality := ⋯ } }

Tactic:
exact h.uniq _ m w

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w
𝒥 : Category.{w', w} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝¹ : C
app✝¹ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝¹).obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝¹ Y =
      app✝¹ X ≫ ((Functor.const J).obj pt✝¹).map f
h : IsColimit { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } }
pt✝ : C
app✝ :
  (X : J) →
    ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C).obj X ⟶
      ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C).map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
m :
  ((𝟭 C).mapCocone { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } }).pt ⟶
    { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt
w :
  ∀ (j : J),
    ((𝟭 C).mapCocone { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } }).ι.app j ≫ m =
      { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j
⊢ m =
    h.desc
      { pt := { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt,
        ι :=
          { app := fun j ↦ { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j, naturality := ⋯ } }

Tactic:
exact h.uniq _ m w

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
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X Y : C
⊢ IsIso 0 ≃ (X ≅ 0) × (Y ≅ 0)

Tactic:
refine (isIsoZeroEquiv X Y).trans ?_
  symm
  fconstructor
  · rintro ⟨eX, eY⟩
    fconstructor
    · exact (idZeroEquivIsoZero X).symm eX
    · exact (idZeroEquivIsoZero Y).symm eY
  · rintro ⟨hX, hY⟩
    fconstructor
    · exact (idZeroEquivIsoZero X) hX
    · exact (idZeroEquivIsoZero Y) hY
  · cat_disch
  · cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝¹ : C
app✝¹ :
  (X : J) →
    ((Functor.const J).obj pt✝¹).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝¹).map f ≫ app✝¹ Y =
      app✝¹ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
h : IsLimit ((𝟭 C).mapCone { pt := pt✝¹, π := { app := app✝¹, naturality := naturality✝¹ } })
pt✝ : C
app✝ :
  (X : J) →
    ((Functor.const J).obj pt✝).obj X ⟶ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((Functor.const J).obj pt✝).map f ≫ app✝ Y =
      app✝ X ≫ { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f
m :
  { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.pt ⟶
    { pt := pt✝¹, π := { app := app✝¹, naturality := naturality✝¹ } }.pt
w :
  ∀ (j : J),
    m ≫ { pt := pt✝¹, π := { app := app✝¹, naturality := naturality✝¹ } }.π.app j =
      { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j
⊢ m =
    h.lift
      { pt := { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.pt,
        π :=
          { app := fun j ↦ { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j, naturality := ⋯ } }

Tactic:
exact h.uniq _ m w

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Basic

Goal state before:
pp: case mk
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J✝ : Type w
inst✝ : Category.{w', w} J✝
K : J✝ ⥤ C
J : Type w'
𝒥 : Category.{w, w'} J
obj✝ : J → C
map✝ : {X Y : J} → (X ⟶ Y) → (obj✝ X ⟶ obj✝ Y)
map_id✝ : ∀ (X : J), map✝ (𝟙 X) = 𝟙 (obj✝ X)
map_comp✝ : ∀ {X Y Z : J} (f : X ⟶ Y) (g : Y ⟶ Z), map✝ (f ≫ g) = map✝ f ≫ map✝ g
pt✝¹ : C
app✝¹ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝¹).obj X
naturality✝¹ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝¹ Y =
      app✝¹ X ≫ ((Functor.const J).obj pt✝¹).map f
h : IsColimit ((𝟭 C).mapCocone { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } })
pt✝ : C
app✝ :
  (X : J) →
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.obj X ⟶ ((Functor.const J).obj pt✝).obj X
naturality✝ :
  ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }.map f ≫ app✝ Y =
      app✝ X ≫ ((Functor.const J).obj pt✝).map f
m :
  { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } }.pt ⟶
    { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt
w :
  ∀ (j : J),
    { pt := pt✝¹, ι := { app := app✝¹, naturality := naturality✝¹ } }.ι.app j ≫ m =
      { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j
⊢ m =
    h.desc
      { pt := { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.pt,
        ι :=
          { app := fun j ↦ { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }.ι.app j, naturality := ⋯ } }

Tactic:
exact h.uniq _ m w

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Z✝ ⟶ X
H : g ≫ (r • f) = g' ≫ (r • f)
⊢ g = g'

Tactic:
rw [comp_smul, comp_smul, ← smul_comp, ← smul_comp, cancel_mono] at H

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
R : Type w
inst✝³ : Semiring R
inst✝² : Linear R C
X Y : C
f : X ⟶ Y
inst✝¹ : Mono f
r : R
inst✝ : Invertible r
Z✝ : C
g g' : Z✝ ⟶ X
H : r • g = r • g'
⊢ g = g'
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✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : -g = -g'
⊢ g = g'

Tactic:
neg_inj

Goal state after:
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✝ : Epi f
Z✝ : C
g g' : Q ⟶ Z✝
H : g = g'
⊢ g = g'
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 = -g'
⊢ g = g'

Tactic:
neg_inj

Goal state after:
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 = g'
⊢ g = g'
Module: Mathlib.CategoryTheory.ObjectProperty.CompleteLattice

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
X : C
⊢ ⊤.map P.ι X → P.isoClosure X

Tactic:
rintro ⟨⟨Y, hY⟩, _, ⟨e⟩⟩
    exact ⟨Y, hY, ⟨e.symm⟩⟩

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✝ : HasKernel f
W : C
h : 0 ≫ f = 0
⊢ lift f 0 h = 0

Tactic:
by
  ext; simp

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
⊢ IsLimit (G.mapCone (Fan.mk P g)) ≃ IsLimit (Fan.mk (G.obj P) fun j ↦ G.map (g j))

Tactic:
refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)

Goal state after:
case refine_1
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
⊢ Discrete.functor f ⋙ G ≅ Discrete.functor fun j ↦ G.obj (f j)

case refine_2
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
⊢ (Cone.postcompose (Iso.hom ?refine_1)).obj (G.mapCone (Fan.mk P g)) ≅ Fan.mk (G.obj P) fun j ↦ G.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
inst✝ : HasCokernel f
W : C
h : f ≫ 0 = 0
⊢ desc f 0 h = 0

Tactic:
by
  ext; 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
inst✝ : HasKernel f
F : MonoFactorisation f
⊢ kernel.ι f ≫ F.e = 0

Tactic:
rw [← cancel_mono F.m, zero_comp, Category.assoc, F.fac, kernel.condition]

Goal state after:
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 : (j : J) → f j ⟶ g j
P : C
k : (j : J) → g j ⟶ P
⊢ map p ≫ desc k = desc fun j ↦ p j ≫ k j

Tactic:
by
  ext; simp

Goal state after:
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 : C
k : (j : J) → P ⟶ f j
p : (j : J) → f j ⟶ g j
⊢ lift k ≫ map p = lift fun j ↦ k j ≫ p j

Tactic:
by
  ext; 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 Q P' Q' : C
b : BinaryBicone P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ IsLimit (b.ofIso eP eQ).toCone

Tactic:
by
    refine (IsLimit.equivOfNatIsoOfIso (mapPairIso eP eQ) _ _ ?_).1 hb.isLimit
    exact BinaryFan.ext (Iso.refl _) (by simp [BinaryFan.fst])
      (by simp [BinaryFan.snd])

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
⊢ ∀ {m : s.pt ⟶ (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯).pt},
    m ≫ Fork.ι (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯) = s.ι → m = s.ι ≫ toSubtype f fun j ↦ j ≠ i

Tactic:
intro m

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
m : s.pt ⟶ (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯).pt
⊢ m ≫ Fork.ι (KernelFork.ofι (fromSubtype f fun j ↦ j ≠ i) ⋯) = s.ι → m = s.ι ≫ toSubtype f fun j ↦ j ≠ i