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
⊢ ((comap C g ⋙ comap (C ∘ g) f).map f' ≫ fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫ (comap C (g ∘ f)).map f'

Tactic:
simp only [comap, Function.comp]; funext; simp

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

Goal state before:
pp: α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
f : X ⟶ Y
⊢ F X.as ⟶ F Y.as

Tactic:
rcases f with ⟨⟨h⟩⟩

Goal state after:
α : Type u₁
C : Type u₂
inst✝ : Category.{v₂, u₂} C
I : Type u₁
F : I → C
X Y : Discrete I
h : X.as = Y.as
⊢ F X.as ⟶ F Y.as
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
⊢ ((comap C (g ∘ f)).map f' ≫ fun b ↦ 𝟙 (Y (g (f b)))) =
    (fun b ↦ 𝟙 (X (g (f b)))) ≫ (comap C g ⋙ comap (C ∘ g) f).map f'

Tactic:
simp only [comap, Function.comp]; funext; simp

Goal state after:
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)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ f.hom i ≫ f.inv i = 𝟙 (X i)

Tactic:
← comp_apply,

Goal state after:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ (f.hom ≫ f.inv) i = 𝟙 (X i)
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)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ f.inv i ≫ f.hom i = 𝟙 (Y i)

Tactic:
← comp_apply,

Goal state after:
I : Type w₀
J : Type w₁
C : I → Type u₁
inst✝ : (i : I) → Category.{v₁, u₁} (C i)
X Y : (i : I) → C i
f : X ≅ Y
i : I
⊢ (f.inv ≫ f.hom) i = 𝟙 (Y i)
Module: Mathlib.CategoryTheory.Comma.Arrow

Goal state before:
pp: T : Type u
inst✝ : Category.{v, u} T
f g : Arrow T
φ₁ φ₂ : f ⟶ g
h : φ₁ = φ₂
⊢ Hom.left φ₁ = Hom.left φ₂

Tactic:
by
  rw [h]

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

Goal state before:
pp: X Y : Type u
f : X ⟶ Y
x x' : X
h : x = x'
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom f) x'

Tactic:
by
  rw [h]

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

Goal state before:
pp: X✝ Y✝ : Type u
f : X✝ ⟶ Y✝
hf : Epi f
⊢ ↾Function.surjInv ⋯ ≫ f = 𝟙 Y✝

Tactic:
ext x
          exact (Function.rightInverse_surjInv <| (epi_iff_surjective f).1 hf) x

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 adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) = adj.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)

Tactic:
Adjunction.right_triangle_components,

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 adj' : F ⊣ G
h : adj.unit = adj'.unit
X : D
⊢ 𝟙 (G.obj X) = adj.unit.app (G.obj X) ≫ G.map (adj'.counit.app X)
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : Cᵒᵖ ⥤ Type v
Y : C
e : F.RepresentableBy Y
X X' : C
x : F.obj (op X')
f : X ⟶ X'
⊢ e.homEquiv (f ≫ e.homEquiv.symm x) = e.homEquiv (e.homEquiv.symm ((ConcreteCategory.hom (F.map f.op)) x))

Tactic:
by simp [homEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F : C ⥤ Type v
X : C
e : F.CorepresentableBy X
Y Y' : C
y : F.obj Y
g : Y ⟶ Y'
⊢ e.homEquiv (e.homEquiv.symm y ≫ g) = e.homEquiv (e.homEquiv.symm ((ConcreteCategory.hom (F.map g)) y))

Tactic:
by simp [homEquiv_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Preorder

Goal state before:
pp: X : Type u
inst✝ : PartialOrder X
a b : X
f : a ⟶ b
⊢ IsIso f ↔ a = b

Tactic:
constructor
  · intro _
    exact (asIso f).to_eq
  · rintro rfl
    rw [Subsingleton.elim f (𝟙 _)]
    infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Yoneda

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : Cᵒᵖ
F : Cᵒᵖ ⥤ Type (max w v₁)
f : uliftYoneda.{w, v₁, u₁}.obj (unop X) ⟶ F
g : X ⟶ Y
⊢ (ConcreteCategory.hom (F.map g)) (uliftYonedaEquiv f) = uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map g.unop ≫ f)

Tactic:
by
  simp [uliftYonedaEquiv, uliftYoneda, ← f.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✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : F.ReflectsIsomorphisms
K : J ⥤ C
A B : Cone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
⊢ IsIso f

Tactic:
have : IsIso (F.map f.hom) :=
    (forget (K ⋙ F)).map_isIso ((functoriality K F).map f)

Goal state after:
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✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : F.ReflectsIsomorphisms
K : J ⥤ C
A B : Cone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
this : IsIso (F.map f.hom)
⊢ IsIso f
Module: Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map (tX.to j') = F.map (tX.to j ≫ k)

Tactic:
tX.hom_ext (tX.to j ≫ k) (tX.to j')

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
J : Type u
inst✝ : Category.{v, u} J
X : J
tX : IsInitial X
F : J ⥤ C
j j' : J
k : j ⟶ j'
⊢ F.map (tX.to j') = F.map (tX.to j')
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ G.map (lift F c) ≫ post F G ≫ π (F ⋙ G) j✝ = lift (F ⋙ G) (G.mapCone c) ≫ π (F ⋙ G) j✝

Tactic:
limit.post_π,

Goal state after:
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : J ⥤ C
inst✝¹ : HasLimit F
G : C ⥤ D
inst✝ : HasLimit (F ⋙ G)
c : Cone F
j✝ : J
⊢ G.map (lift F c) ≫ G.map (π F j✝) = lift (F ⋙ G) (G.mapCone c) ≫ π (F ⋙ G) j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ H.map (post F G) ≫ post (F ⋙ G) H ≫ π ((F ⋙ G) ⋙ H) j✝ = post F (G ⋙ H) ≫ π ((F ⋙ G) ⋙ H) j✝

Tactic:
limit.post_π,

Goal state after:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ H.map (post F G) ≫ H.map (π (F ⋙ G) j✝) = post F (G ⋙ H) ≫ π ((F ⋙ G) ⋙ H) j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ H.map (post F G ≫ π (F ⋙ G) j✝) = post F (G ⋙ H) ≫ π ((F ⋙ G) ⋙ H) j✝

Tactic:
limit.post_π,

Goal state after:
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : J ⥤ C
inst✝² : HasLimit F
G : C ⥤ D
inst✝¹ : HasLimit (F ⋙ G)
E : Type u''
inst✝ : Category.{v'', u''} E
H : D ⥤ E
h : HasLimit ((F ⋙ G) ⋙ H)
this : HasLimit (F ⋙ G ⋙ H)
j✝ : J
⊢ H.map (G.map (π F j✝)) = post F (G ⋙ H) ≫ π ((F ⋙ G) ⋙ H) j✝
Module: Mathlib.CategoryTheory.Limits.HasLimits

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 : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j✝ : K
⊢ G.map (pre F E) ≫ post (E ⋙ F) G ≫ π ((E ⋙ F) ⋙ G) j✝ = (post F G ≫ pre (F ⋙ G) E) ≫ π ((E ⋙ F) ⋙ G) j✝

Tactic:
limit.post_π,

Goal state after:
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 : K ⥤ J
F : J ⥤ C
G : C ⥤ D
inst✝² : HasLimit F
inst✝¹ : HasLimit (E ⋙ F)
inst✝ : HasLimit (F ⋙ G)
h : HasLimit ((E ⋙ F) ⋙ G)
this : HasLimit (E ⋙ F ⋙ G)
j✝ : K
⊢ G.map (pre F E) ≫ G.map (π (E ⋙ F) j✝) = (post F G ≫ pre (F ⋙ G) E) ≫ π ((E ⋙ F) ⋙ G) j✝
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
H : IsLimit c
⊢ IsIso c.fst

Tactic:
obtain ⟨l, hl, -⟩ := BinaryFan.IsLimit.lift' H (𝟙 X) (h.from X)

Goal state after:
case mp
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
⊢ IsIso c.fst
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α

Goal state after:
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
β : 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β : β ≫ Functor.whiskerRight e₁.hom R' = R.whiskerLeft e₂.hom ≫ β'
X : StructuredArrow L R
⊢ ((map₂ (α' ≫ e₂.inv.app L) β).obj X).hom ≫ R'.map (e₁.app X.right).hom = ((map₂ α' β').obj X).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
⊢ IsLimit (mk s.fst s.snd ⋯)

Tactic:
apply PullbackCone.isLimitAux'

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_1 : PullbackCone (f ≫ i) (g ≫ i)) →
    { l //
      l ≫ (mk s.fst s.snd ⋯).fst = s_1.fst ∧
        l ≫ (mk s.fst s.snd ⋯).snd = s_1.snd ∧
          ∀ {m : s_1.pt ⟶ (mk s.fst s.snd ⋯).pt},
            m ≫ (mk s.fst s.snd ⋯).fst = s_1.fst → m ≫ (mk s.fst s.snd ⋯).snd = s_1.snd → m = l }
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
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := { I := equalizer g h, m := q ≫ ι f, m_mono := ⋯, e := e', fac := ⋯ }
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ v ≫ q ≫ h = 𝟙 (image f) ≫ h

Tactic:
by rw [← Category.assoc, t]

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
inst✝ : HasImage f
E : Epi (factorThruImage f ≫ image.ι f)
⊢ Epi (image.ι f)

Tactic:
exact epi_of_epi (factorThruImage f) (image.ι f)

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 : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi F'.e

Tactic:
rw [← IsImage.e_isoExt_hom F.toMonoIsImage hF']

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi (F.e ≫ (F.toMonoIsImage.isoExt hF').hom)
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✝ } }
s : Cone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C)
m : s.pt ⟶ ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }).pt
w : ∀ (j : J), m ≫ ((𝟭 C).mapCone { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }).π.app j = s.π.app j
⊢ m = h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } }

Tactic:
rcases s with ⟨_, _, _⟩

Goal state after:
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 := ⋯ } }
Module: Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
Z : C
g h : Z ⟶ X
x✝ : g ≫ f = h ≫ f
⊢ g = h

Tactic:
zero_of_target_iso_zero g i,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
i : X ≅ 0
Z : C
g h : Z ⟶ X
x✝ : g ≫ f = h ≫ f
⊢ 0 = h
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✝ } }
s : Cocone ({ obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ } ⋙ 𝟭 C)
m : ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }).pt ⟶ s.pt
w : ∀ (j : J), ((𝟭 C).mapCocone { pt := pt✝, ι := { app := app✝, naturality := naturality✝ } }).ι.app j ≫ m = s.ι.app j
⊢ m = h.desc { pt := s.pt, ι := { app := fun j ↦ s.ι.app j, naturality := ⋯ } }

Tactic:
rcases s with ⟨_, _, _⟩

Goal state after:
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 := ⋯ } }
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
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
hG : ∀ (X : C), IsZero (G.obj X)
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c✝ : Cocone K
x✝ : IsColimit c✝
⊢ IsColimit (G.mapCocone c✝)

Tactic:
exact IsColimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)

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✝ } })
s : Cone { obj := obj✝, map := map✝, map_id := map_id✝, map_comp := map_comp✝ }
m : s.pt ⟶ { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.pt
w : ∀ (j : J), m ≫ { pt := pt✝, π := { app := app✝, naturality := naturality✝ } }.π.app j = s.π.app j
⊢ m = h.lift { pt := s.pt, π := { app := fun j ↦ s.π.app j, naturality := ⋯ } }

Tactic:
rcases s with ⟨_, _, _⟩

Goal state after:
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 := ⋯ } }