mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
⊢ IsIso S.f ↔ IsZero S.X₃

Tactic:
have := hS.exact.hasZeroObject

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this : HasZeroObject C
⊢ IsIso S.f ↔ IsZero S.X₃
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
⊢ IsIso S.g ↔ IsZero S.X₁

Tactic:
have := hS.exact.hasZeroObject

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : S.ShortExact
inst✝ : Balanced C
this : HasZeroObject C
⊢ IsIso S.g ↔ IsZero S.X₁
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
⊢ IsIso φ.τ₂

Tactic:
have := h₁.mono_f

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
inst✝² : Balanced C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.ShortExact
h₂ : S₂.ShortExact
inst✝¹ : IsIso φ.τ₁
inst✝ : IsIso φ.τ₃
this : Mono S₁.f
⊢ IsIso φ.τ₂
Module: Mathlib.CategoryTheory.Preadditive.LeftExact

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := ⋯
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) ⋯) := ⋯
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) ⋯) := ⋯
⊢ IsLimit (Fork.ofι (F.map (Fork.ι c)) ⋯)

Tactic:
let p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 :=
    parallelPair.eqOfHomEq F.map_sub rfl

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) F
X Y : C
f g : X ⟶ Y
this✝ : PreservesBinaryBiproducts F := preservesBinaryBiproducts_of_preservesBinaryProducts F
this : F.Additive
c : Cone (parallelPair f g)
i : IsLimit c
c' : IsLimit (KernelFork.ofι (Fork.ι c) ⋯) := isLimitKernelForkOfFork (i.ofIsoLimit (Fork.isoForkOfι c))
iFc : IsLimit (KernelFork.ofι (F.map (Fork.ι c)) ⋯) := isLimitForkMapOfIsLimit' F ⋯ c'
p : parallelPair (F.map (f - g)) 0 ≅ parallelPair (F.map f - F.map g) 0 := parallelPair.eqOfHomEq ⋯ ⋯
⊢ IsLimit (Fork.ofι (F.map (Fork.ι c)) ⋯)
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasCokernel S.f
⊢ S.Exact ↔ Mono (cokernel.desc S.f S.g ⋯)

Tactic:
exact_iff_mono_fromOpcycles

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasCokernel S.f
⊢ Mono S.fromOpcycles ↔ Mono (cokernel.desc S.f S.g ⋯)
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ S.Exact

Tactic:
exact_iff_mono_fromOpcycles

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ Mono S.fromOpcycles
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝ : S.HasHomology
this : Mono S.fromOpcycles
⊢ S.pOpcycles ≫ S.fromOpcycles = 0

Tactic:
p_fromOpcycles,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hg : S.g = 0
this✝ : S.HasHomology
this : Mono S.fromOpcycles
⊢ S.g = 0
Module: Mathlib.CategoryTheory.Subobject.Basic

Goal state before:
pp: case g.refine_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : HasPullbacks C
X Y Z W : C
f : X ⟶ Y
g : X ⟶ Z
h : Y ⟶ W
k : Z ⟶ W
inst✝¹ : Mono h
inst✝ : Mono g
comm : f ≫ h = g ≫ k
t : IsLimit (PullbackCone.mk f g comm)
a : MonoOver Y
⊢ pullback.lift (pullback.fst ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k)
        (PullbackCone.IsLimit.lift t (pullback.fst ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k ≫ a.arrow)
          (pullback.snd ((MonoOver.forget W).obj ((MonoOver.map h).obj a)).hom k) ⋯)
        ⋯ ≫
      ((MonoOver.map g).obj ((MonoOver.pullback f).obj a)).arrow =
    ((MonoOver.pullback k).obj ((MonoOver.map h).obj a)).arrow

Tactic:
dsimp
      rw [pullback.lift_snd_assoc]
      apply PullbackCone.IsLimit.lift_snd

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

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
inst✝⁶ : Preadditive C
inst✝⁵ : Preadditive D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : F.PreservesHomology
inst✝² : HasZeroObject C
inst✝¹ : HasFiniteProducts C
inst✝ : HasKernels C
⊢ PreservesFiniteLimits F

Tactic:
have := fun {X Y : C} (f : X ⟶ Y) ↦ PreservesHomology.preservesKernel F f
  have : HasBinaryBiproducts C := HasBinaryBiproducts.of_hasBinaryProducts
  have : HasEqualizers C := Preadditive.hasEqualizers_of_hasKernels
  have : HasZeroObject D :=
    ⟨F.obj 0, by rw [IsZero.iff_id_eq_zero, ← F.map_id, id_zero, F.map_zero]⟩
  exact preservesFiniteLimits_of_preservesKernels F

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.ExactFunctor

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
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g),
      ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g),
      ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F, PreservesFiniteColimits F].TFAE

Tactic:
tfae_have 1 → 2
  | hF, S, ⟨hS, hf⟩ => by
    have := preservesEpimorphisms_of_preserves_shortExact_right F hF
    refine ⟨?_, inferInstance⟩
    let T := ShortComplex.mk (Abelian.image.ι S.f) S.g (Abelian.image_ι_comp_eq_zero S.zero)
    let φ : S.map F ⟶ T.map F :=
      { τ₁ := F.map <| Abelian.factorThruImage S.f
        τ₂ := 𝟙 _
        τ₃ := 𝟙 _
        comm₁₂ := show _ ≫ F.map (kernel.ι _) = F.map _ ≫ 𝟙 _ by
          rw [← F.map_comp, Abelian.image.fac, Category.comp_id] }
    exact (exact_iff_of_epi_of_isIso_of_mono φ).2 (hF T ⟨(S.exact_iff_exact_image_ι).1 hS⟩).1

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
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g)
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Epi (F.map S.g),
      ∀ (S : ShortComplex C), S.Exact ∧ Epi S.g → (S.map F).Exact ∧ Epi (F.map S.g),
      ∀ ⦃X Y : C⦄ (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F, PreservesFiniteColimits F].TFAE
Module: Mathlib.CategoryTheory.Limits.Filtered

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))

Tactic:
obtain ⟨c⟩ := h F

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
c : Cocone F
⊢ ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))
Module: Mathlib.CategoryTheory.Limits.Filtered

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
⊢ ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))

Tactic:
obtain ⟨c⟩ := h F

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
h : ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cone F)
J : Type v
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ C
c : Cone F
⊢ ∃ X, Nonempty (limit (F ⋙ coyoneda.obj (op X)))
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
⊢ (Sigma.desc π).op ≫ (opCoproductIsoProduct Z).hom = Pi.lift fun a ↦ (π a).op

Tactic:
convert!
    desc_op_comp_opCoproductIsoProduct'_hom (coproductIsCoproduct Z) (productIsProduct (op <| Z ·))
      (Cofan.mk _ π)
  · simp [Sigma.desc, coproductIsCoproduct]
  · simp [productIsProduct]

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F : C ⥤ H
⊢ (L.lan.obj F).IsLeftKanExtension (L.lanUnit.app F)

Tactic:
dsimp [lan, lanUnit]

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
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{v_3, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F : C ⥤ H
⊢ (L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit F)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L'.HasPointwiseRightKanExtensionAt F Y' → L.HasPointwiseRightKanExtensionAt F Y

Tactic:
intro
    exact hasPointwiseRightKanExtensionAt_of_equivalence L' L F E.symm
      (isoWhiskerRight eL.symm _ ≪≫ Functor.associator _ _ _ ≪≫
        isoWhiskerLeft L E.unitIso.symm ≪≫ L.rightUnitor) Y' Y
      (E.inverse.mapIso e.symm ≪≫ E.unitIso.symm.app Y)

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
Y₁ Y₂ Y₃ : D
f : Y₁ ⟶ Y₂
f' : Y₂ ⟶ Y₃
j : CostructuredArrow L Y₁
⊢ colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
        { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
          ι :=
            { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map (f ≫ f')).obj g),
              naturality := ⋯ } } =
    colimit.ι (CostructuredArrow.proj L Y₁ ⋙ F) j ≫
      colimit.desc (CostructuredArrow.proj L Y₁ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₂ ⋙ F),
            ι :=
              { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g),
                naturality := ⋯ } } ≫
        colimit.desc (CostructuredArrow.proj L Y₂ ⋙ F)
          { pt := colimit (CostructuredArrow.proj L Y₃ ⋙ F),
            ι :=
              { app := fun g ↦ colimit.ι (CostructuredArrow.proj L Y₃ ⋙ F) ((CostructuredArrow.map f').obj g),
                naturality := ⋯ } }

Tactic:
dsimp
    simp only [colimit.ι_desc, colimit.ι_desc_assoc, comp_obj, CostructuredArrow.proj_obj]
    congr 1
    apply CostructuredArrow.map_comp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
Y : D
j : StructuredArrow Y L
⊢ limit.lift (StructuredArrow.proj Y L ⋙ F)
        { pt := limit (StructuredArrow.proj Y L ⋙ F),
          π :=
            { app := fun g ↦ limit.π (StructuredArrow.proj Y L ⋙ F) ((StructuredArrow.map (𝟙 Y)).obj g),
              naturality := ⋯ } } ≫
      limit.π (StructuredArrow.proj Y L ⋙ F) j =
    𝟙 (limit (StructuredArrow.proj Y L ⋙ F)) ≫ limit.π (StructuredArrow.proj Y L ⋙ F) j

Tactic:
simp only [limit.lift_π, id_comp]

Goal state after:
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D'
inst✝¹ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
inst✝ : L.HasPointwiseRightKanExtension F
Y : D
j : StructuredArrow Y L
⊢ limit.π (StructuredArrow.proj Y L ⋙ F) ((StructuredArrow.map (𝟙 Y)).obj j) = limit.π (StructuredArrow.proj Y L ⋙ F) j
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) := ⋯
⊢ (X : C ⥤ D) →
    (prod.functor.obj F ⋙ (evaluation C D).obj k).obj X ≅ ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).obj X

Tactic:
intro G

Goal state after:
C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
G : C ⥤ D
⊢ (prod.functor.obj F ⋙ (evaluation C D).obj k).obj G ≅ ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).obj G
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) := ⋯
⊢ ∀ {X Y : C ⥤ D} (f : X ⟶ Y),
    (prod.functor.obj F ⋙ (evaluation C D).obj k).map f ≫ (asIso (prodComparison ((evaluation C D).obj k) F Y)).hom =
      (asIso (prodComparison ((evaluation C D).obj k) F X)).hom ≫
        ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).map f

Tactic:
intro G

Goal state after:
C : Type u
inst✝⁵ : Category.{v₁, u} C
D : Type u₂
inst✝⁴ : Category.{u, u₂} D
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : ∀ (X : D), PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
G : C ⥤ D
⊢ ∀ {Y : C ⥤ D} (f : G ⟶ Y),
    (prod.functor.obj F ⋙ (evaluation C D).obj k).map f ≫ (asIso (prodComparison ((evaluation C D).obj k) F Y)).hom =
      (asIso (prodComparison ((evaluation C D).obj k) F G)).hom ≫
        ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).map f
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁ v₂)
E : ℰ
f :
  CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ⟶
    (Functor.const (CostructuredArrow uliftYoneda.{max w v₂, v₁, u₁} P)).obj E
x✝¹ x✝ : Cᵒᵖ
g : x✝¹ ⟶ x✝
⊢ (P.map g ≫ ↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) }) =
    (↾fun x ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x)) }) ≫
      ((restrictedULiftYoneda A).obj E).map g

Tactic:
ext x
        let φ : CostructuredArrow.mk (uliftYonedaEquiv.{max w v₂}.symm (P.map g x)) ⟶
          CostructuredArrow.mk (uliftYonedaEquiv.symm x) :=
            CostructuredArrow.homMk g.unop (by
              dsimp
              rw [uliftYonedaEquiv_symm_map])
        dsimp
        congr 1
        simpa using! (f.naturality φ).symm

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  uliftYoneda.{w, v₁, u₁}.map f.unop ≫ s.ι.app (op (P.elementsMk X x)) =
    s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))
⊢ uliftYonedaEquiv (s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))) =
    (hom (s.pt.map f)) (uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))))

Tactic:
← this,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
X Y : Cᵒᵖ
f : X ⟶ Y
x : P.obj X
this :
  uliftYoneda.{w, v₁, u₁}.map f.unop ≫ s.ι.app (op (P.elementsMk X x)) =
    s.ι.app (op (P.elementsMk Y ((hom (P.map f)) x)))
⊢ uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map f.unop ≫ s.ι.app (op (P.elementsMk X x))) =
    (hom (s.pt.map f)) (uliftYonedaEquiv (s.ι.app (op (P.elementsMk X x))))
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
j : P.Elementsᵒᵖ
X : Cᵒᵖ
x : ULift.{w, v₁} (unop X ⟶ unop (unop j).fst)
φ : unop j ⟶ P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x) := ⟨Quiver.Hom.op x.down, ⋯⟩
this :
  uliftYoneda.{w, v₁, u₁}.map x.down ≫ s.ι.app j =
    s.ι.app (op (P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x)))
⊢ uliftYonedaEquiv (s.ι.app (op (P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x)))) =
    (hom ((s.ι.app j).app X)) x

Tactic:
← this,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
P : Cᵒᵖ ⥤ Type (max w v₁)
s : Cocone (functorToRepresentables P)
j : P.Elementsᵒᵖ
X : Cᵒᵖ
x : ULift.{w, v₁} (unop X ⟶ unop (unop j).fst)
φ : unop j ⟶ P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x) := ⟨Quiver.Hom.op x.down, ⋯⟩
this :
  uliftYoneda.{w, v₁, u₁}.map x.down ≫ s.ι.app j =
    s.ι.app (op (P.elementsMk X ((hom ((uliftYonedaEquiv.symm (unop j).snd).app X)) x)))
⊢ uliftYonedaEquiv (uliftYoneda.{w, v₁, u₁}.map x.down ≫ s.ι.app j) = (hom ((s.ι.app j).app X)) x
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))
A : C
hA : P A
g : A ⟶ Y
l₁ : A ⟶ X
⊢ ∀ (y₂ : A ⟶ X), l₁ ≫ f = g → y₂ ≫ f = g → l₁ = y₂

Tactic:
l₂

Goal state after:
case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))
A : C
hA : P A
g : A ⟶ Y
l₁ l₂ : A ⟶ X
⊢ l₁ ≫ f = g → l₂ ≫ f = g → l₁ = l₂
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f✝ : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f✝ j₁ = ι ≫ f✝ j₂
i j : WalkingParallelFamily J
f : i ⟶ j
⊢ ((Functor.const (WalkingParallelFamily J)).obj P).map f ≫
      WalkingParallelFamily.casesOn j ι (ι ≫ f✝ (Classical.arbitrary J)) =
    WalkingParallelFamily.casesOn i ι (ι ≫ f✝ (Classical.arbitrary J)) ≫ (parallelFamily f✝).map f

Tactic:
obtain - | k := f

Goal state after:
case id
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f j₁ = ι ≫ f j₂
i : WalkingParallelFamily J
⊢ ((Functor.const (WalkingParallelFamily J)).obj P).map (Hom.id i) ≫
      WalkingParallelFamily.casesOn i ι (ι ≫ f (Classical.arbitrary J)) =
    WalkingParallelFamily.casesOn i ι (ι ≫ f (Classical.arbitrary J)) ≫ (parallelFamily f).map (Hom.id i)

case line
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
ι : P ⟶ X
w : ∀ (j₁ j₂ : J), ι ≫ f j₁ = ι ≫ f j₂
k : J
⊢ ((Functor.const (WalkingParallelFamily J)).obj P).map (line k) ≫
      WalkingParallelFamily.casesOn one ι (ι ≫ f (Classical.arbitrary J)) =
    WalkingParallelFamily.casesOn zero ι (ι ≫ f (Classical.arbitrary J)) ≫ (parallelFamily f).map (line k)
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))
A : C
hA : P A
g : X ⟶ A
l₁ : Y ⟶ A
⊢ ∀ (y₂ : Y ⟶ A), f ≫ l₁ = g → f ≫ y₂ = g → l₁ = y₂

Tactic:
l₂

Goal state after:
case mpr.refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
hf : ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))
A : C
hA : P A
g : X ⟶ A
l₁ l₂ : Y ⟶ A
⊢ f ≫ l₁ = g → f ≫ l₂ = g → l₁ = l₂
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f✝ : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f✝ j₁ ≫ π = f✝ j₂ ≫ π
i j : WalkingParallelFamily J
f : i ⟶ j
⊢ (parallelFamily f✝).map f ≫ WalkingParallelFamily.casesOn j (f✝ (Classical.arbitrary J) ≫ π) π =
    WalkingParallelFamily.casesOn i (f✝ (Classical.arbitrary J) ≫ π) π ≫
      ((Functor.const (WalkingParallelFamily J)).obj P).map f

Tactic:
obtain - | k := f

Goal state after:
case id
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f j₁ ≫ π = f j₂ ≫ π
i : WalkingParallelFamily J
⊢ (parallelFamily f).map (Hom.id i) ≫ WalkingParallelFamily.casesOn i (f (Classical.arbitrary J) ≫ π) π =
    WalkingParallelFamily.casesOn i (f (Classical.arbitrary J) ≫ π) π ≫
      ((Functor.const (WalkingParallelFamily J)).obj P).map (Hom.id i)

case line
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
P : C
π : Y ⟶ P
w : ∀ (j₁ j₂ : J), f j₁ ≫ π = f j₂ ≫ π
k : J
⊢ (parallelFamily f).map (line k) ≫ WalkingParallelFamily.casesOn one (f (Classical.arbitrary J) ≫ π) π =
    WalkingParallelFamily.casesOn zero (f (Classical.arbitrary J) ≫ π) π ≫
      ((Functor.const (WalkingParallelFamily J)).obj P).map (line k)
Module: Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers

Goal state before:
pp: J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
inst✝ : Nonempty J
s t : Cotrident f
i : s.pt ≅ t.pt
w : s.π ≫ i.hom = t.π
⊢ t.π ≫ i.inv = s.π

Tactic:
rw [Iso.comp_inv_eq, w]

Goal state after: