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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ (homologyMap φ).op = S₂.homologyOpIso.inv ≫ homologyMap (opMap φ) ≫ S₁.homologyOpIso.hom

Tactic:
dsimp only [homologyMap, homologyOpIso]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝¹ : S₁.HasHomology
inst✝ : S₂.HasHomology
⊢ (homologyMap' φ S₁.homologyData S₂.homologyData).op =
    (S₂.op.leftHomologyIso.symm ≪≫ S₂.leftHomologyOpIso ≪≫ S₂.rightHomologyIso.symm.op).inv ≫
      homologyMap' (opMap φ) S₂.op.homologyData S₁.op.homologyData ≫
        (S₁.op.leftHomologyIso.symm ≪≫ S₁.leftHomologyOpIso ≪≫ S₁.rightHomologyIso.symm.op).hom
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ φ₁.τ₁ = S₁.f ≫ (h₁₂.h₁ + h₂₃.h₁) + (h₁₂.h₀ + h₂₃.h₀) + φ₃.τ₁

Tactic:
rw [h₁₂.comm₁, h₂₃.comm₁, comp_add]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h₁₂ : Homotopy φ₁ φ₂
h₂₃ : Homotopy φ₂ φ₃
⊢ S₁.f ≫ h₁₂.h₁ + h₁₂.h₀ + (S₁.f ≫ h₂₃.h₁ + h₂₃.h₀ + φ₃.τ₁) = S₁.f ≫ h₁₂.h₁ + S₁.f ≫ h₂₃.h₁ + (h₁₂.h₀ + h₂₃.h₀) + φ₃.τ₁
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
h' : Homotopy φ₃ φ₄
⊢ (φ₁ - φ₃).τ₂ = S₁.g ≫ (h.h₂ - h'.h₂) + (h.h₁ - h'.h₁) ≫ S₂.f + (φ₂ - φ₄).τ₂

Tactic:
rw [sub_τ₂, sub_τ₂, h.comm₂, h'.comm₂, comp_sub, sub_comp]; abel

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁

Tactic:
h.comm₁

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ S₃ : ShortComplex C
φ₁ φ₂ φ₃ φ₄ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁✝ S₂✝ S₃ : ShortComplex C
φ₁✝ φ₂✝ φ₃ φ₄ : S₁✝ ⟶ S₂✝
S₁ S₂ : ShortComplex Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁

Tactic:
h.comm₁

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁✝ S₂✝ S₃ : ShortComplex C
φ₁✝ φ₂✝ φ₃ φ₄ : S₁✝ ⟶ S₂✝
S₁ S₂ : ShortComplex Cᵒᵖ
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = h.h₀ + S₁.f ≫ h.h₁ + φ₂.τ₁
Module: Mathlib.Algebra.Homology.ShortComplex.Preadditive

Goal state before:
pp: case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)

Tactic:
h.comm₁

Goal state after:
case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)
Module: Mathlib.Algebra.Homology.ShortComplex.ShortExact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : S.ShortExact
⊢ Epi S.op.g

Tactic:
have := h.mono_f
    dsimp
    infer_instance

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex Cᵒᵖ
h : S.ShortExact
⊢ Epi S.unop.g

Tactic:
have := h.mono_f
    dsimp
    infer_instance

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

Goal state before:
pp: S : ShortComplex Ab
⊢ (AddCommGrpCat.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f ⋯) ≫
      AddCommGrpCat.ofHom (QuotientAddGroup.mk' S.abToCycles.range) =
    0

Tactic:
ext (x : S.X₁)

Goal state after:
S : ShortComplex Ab
x : ↑S.X₁
⊢ (AddCommGrpCat.Hom.hom
        ((AddCommGrpCat.kernelIsLimit S.g).lift (Limits.KernelFork.ofι S.f ⋯) ≫
          AddCommGrpCat.ofHom (QuotientAddGroup.mk' S.abToCycles.range)))
      x =
    (AddCommGrpCat.Hom.hom 0) x
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
inst✝ : HasZeroObject C
hf : S.f = 0
⊢ S.Exact → Mono S.g

Tactic:
intro h
    have := h.hasHomology
    simp only [exact_iff_isZero_homology] at h
    have := S.isIso_pOpcycles hf
    have := mono_of_isZero_kernel' _ S.homologyIsKernel h
    rw [← S.p_fromOpcycles]
    apply mono_comp

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

Goal state before:
pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ kernel.lift g.unop (kernel.ι f.unop) ⋯ ≫ kernel.ι g.unop = kernel.ι f.unop

Tactic:
exact Quiver.Hom.op_inj (by simp)

Goal state after:
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
⊢ ∀ {X Y : Subobject B}, X.Factors f ∧ Y.Factors f → (X ⊓ Y).Factors f

Tactic:
apply Quotient.ind₂'

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
⊢ ∀ (a₁ a₂ : MonoOver B),
    Factors (Quotient.mk'' a₁) f ∧ Factors (Quotient.mk'' a₂) f → (Quotient.mk'' a₁ ⊓ Quotient.mk'' a₂).Factors f
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case insert
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
m : i✝ ∈ insert a✝¹ s✝
⊢ (P i✝).Factors (P a✝¹ ⊓ s✝.inf P).arrow

Tactic:
simp only [Finset.mem_insert] at m

Goal state after:
case insert
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : ∀ i ∈ s✝, (P i).Factors (s✝.inf P).arrow
i✝ : I
m : i✝ = a✝¹ ∨ i✝ ∈ s✝
⊢ (P i✝).Factors (P a✝¹ ⊓ s✝.inf P).arrow
Module: Mathlib.CategoryTheory.Limits.Filtered

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

Tactic:
IsFiltered.iff_cocone_nonempty.{v}

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
⊢ (∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), Nonempty (Cocone F)) ↔
    ∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : J ⥤ C), ∃ X, Nonempty (limit (F.op ⋙ yoneda.obj X))
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case insert
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : (∃ i ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
j : I
m : j ∈ insert a✝¹ s✝
h : (P j).Factors f
⊢ (P a✝¹ ⊔ s✝.sup P).Factors f

Tactic:
simp only [Finset.mem_insert] at m

Goal state after:
case insert
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasImages C
inst✝² : HasBinaryCoproducts C
inst✝¹ : HasInitial C
inst✝ : InitialMonoClass C
I : Type u_1
A B : C
P : I → Subobject B
f : A ⟶ B
a✝¹ : I
s✝ : Finset I
a✝ : a✝¹ ∉ s✝
ih : (∃ i ∈ s✝, (P i).Factors f) → (s✝.sup P).Factors f
j : I
h : (P j).Factors f
m : j = a✝¹ ∨ j ∈ s✝
⊢ (P a✝¹ ⊔ s✝.sup P).Factors f
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
p : YonedaCollection F X
⊢ op (CostructuredArrow.mk p.fst) = op (CostructuredArrow.mk (map₁ η p).fst)

Tactic:
by rw [YonedaCollection.map₁_fst]

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

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : F ⟶ L' ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk (G ⋙ F') (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)) := ⋯
⊢ F'.IsLeftKanExtension α → (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)

pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : F ⟶ L' ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk (G ⋙ F') (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)) := ⋯
⊢ (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom) → F'.IsLeftKanExtension α

Tactic:
· exact fun _ => ⟨⟨eq (isUniversalOfIsLeftKanExtension _ _)⟩⟩

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
D' : Type u_5
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} H
inst✝² : Category.{v_4, u_4} D
inst✝¹ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : C ⥤ D'
G : D ⥤ D'
inst✝ : G.IsEquivalence
e : L ⋙ G ≅ L'
F : C ⥤ H
F' : D' ⥤ H
α : F ⟶ L' ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk (G ⋙ F') (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom)) := ⋯
⊢ (G ⋙ F').IsLeftKanExtension (α ≫ whiskerRight e.inv F' ≫ (L.associator G F').hom) → F'.IsLeftKanExtension α
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : F ⟶ L ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk F' (G.whiskerLeft α ≫ (G.associator L F').inv)) := ⋯
⊢ F'.IsLeftKanExtension α → F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv)

pp: case mpr
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : F ⟶ L ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk F' (G.whiskerLeft α ≫ (G.associator L F').inv)) := ⋯
⊢ F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv) → F'.IsLeftKanExtension α

Tactic:
· exact fun _ => ⟨⟨eq (isUniversalOfIsLeftKanExtension _ _)⟩⟩

Goal state after:
case mpr
C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} C'
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
L : C ⥤ D
F : C ⥤ H
F' : D ⥤ H
G : C' ⥤ C
inst✝ : G.IsEquivalence
α : F ⟶ L ⋙ F'
eq : StructuredArrow.IsUniversal (LeftExtension.mk F' α) ≃
  StructuredArrow.IsUniversal (LeftExtension.mk F' (G.whiskerLeft α ≫ (G.associator L F').inv)) := ⋯
⊢ F'.IsLeftKanExtension (G.whiskerLeft α ≫ (G.associator L F').inv) → F'.IsLeftKanExtension α
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_2.refine_3
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ monoLift f (kernel.ι (cokernel.π f)) ⋯ ≫ kernel.lift (cokernel.π f) f ⋯ = 𝟙 (kernel (cokernel.π f))

pp: case refine_2.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel.lift (cokernel.π f) f ⋯ ≫ monoLift f (kernel.ι (cokernel.π f)) ⋯ = 𝟙 A

pp: case refine_2.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ { hom := monoLift f (kernel.ι (cokernel.π f)) ⋯, inv := kernel.lift (cokernel.π f) f ⋯,
          hom_inv_id := ?refine_2.refine_3, inv_hom_id := ?refine_2.refine_4 }.hom ≫
      f =
    kernel.ι (cokernel.π f)

Tactic:
· simp only [← cancel_mono (kernel.ι (cokernel.π f)), Category.assoc, image.fac, monoLift_comp,
        Category.id_comp]

Goal state after:
case refine_2.refine_4
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ kernel.lift (cokernel.π f) f ⋯ ≫ monoLift f (kernel.ι (cokernel.π f)) ⋯ = 𝟙 A

case refine_2.refine_5
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
f : A ⟶ X
hf : Mono f
⊢ { hom := monoLift f (kernel.ι (cokernel.π f)) ⋯, inv := kernel.lift (cokernel.π f) f ⋯, hom_inv_id := ⋯,
          inv_hom_id := ?refine_2.refine_4 }.hom ≫
      f =
    kernel.ι (cokernel.π f)
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝¹ : Category.{v₂, u₂} ℰ
A : C ⥤ ℰ
inst✝ : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
L : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ ℰ
α : A ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ L
left✝ : IsIso α
right✝ :
  PreservesColimitsOfSize.{v₁, max w u₁ v₁ v₂, max (max (max u₁ v₁) v₂) w, v₂,
      max (max (max u₁ (v₁ + 1)) (v₂ + 1)) (w + 1), u₂}
    L
P : Cᵒᵖ ⥤ Type (max (max w v₂) v₁)
e : (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor ⋙
    CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ A ≅
  functorToRepresentables P ⋙ L :=
  (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.isoWhiskerLeft
      ((CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P).isoWhiskerLeft (asIso α)) ≪≫
    (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.isoWhiskerLeft
        ((CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P).associator uliftYoneda.{max w v₂, v₁, u₁} L).symm ≪≫
      ((CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor.associator
            (CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ uliftYoneda.{max w v₂, v₁, u₁}) L).symm ≪≫
        Functor.isoWhiskerRight
          (Iso.refl
            ((CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor ⋙
              CostructuredArrow.proj uliftYoneda.{max w v₂, v₁, u₁} P ⋙ uliftYoneda.{max w v₂, v₁, u₁}))
          L
⊢ IsColimit
    ((Cocone.precompose e.symm.hom).obj
      (Cocone.whisker (CategoryOfElements.costructuredArrowULiftYonedaEquivalence P).functor
        ((Functor.LeftExtension.mk L α).coconeAt P)))

Tactic:
exact IsColimit.ofIsoColimit (isColimitOfPreserves L (colimitOfRepresentable.{max w v₂} P))
      (Cocone.ext (Iso.refl _))

Goal state after:
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₁ l₂ : A ⟶ X
h₁ : l₁ ≫ f = g
h₂ : l₂ ≫ f = g
⊢ l₁ ≫ f = l₂ ≫ f

Tactic:
h₁,

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
h₁ : l₁ ≫ f = g
h₂ : l₂ ≫ f = g
⊢ g = l₂ ≫ f
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₁ l₂ : Y ⟶ A
h₁ : f ≫ l₁ = g
h₂ : f ≫ l₂ = g
⊢ f ≫ l₁ = f ≫ l₂

Tactic:
h₁,

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
h₁ : f ≫ l₁ = g
h₂ : f ≫ l₂ = g
⊢ g = f ≫ l₂
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : C ⥤ D
T : D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits S
A : CostructuredArrow S T
P : { P // ∃ q, S.map P.arrow.unop ≫ q = A.hom }
⊢ ↑((fun P ↦ ⟨projectQuotient P, ⋯⟩) ((fun P ↦ liftQuotient ↑P ⋯) P)) = ↑P

Tactic:
simp only [liftQuotient, Quiver.Hom.unop_op, homMk_left,
      Quiver.Hom.op_unop, projectQuotient_mk, Subobject.mk_arrow]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCoseparating
X : C
inst✝ : HasProduct (P.productToFamily X)
Z✝ : C
u v : Z✝ ⟶ X
huv : u ≫ P.productTo X = v ≫ P.productTo X
G : C
hG : P G
h : X ⟶ G
⊢ u ≫ h = v ≫ h

Tactic:
simpa using huv =≫ P.πProductTo h hG

Goal state after:
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS : S.Exact
⊢ (S.map colim).Exact

Tactic:
by
    replace hS := fun j => hS.map ((evaluation _ _).obj j)
    simp only [ShortComplex.ab_exact_iff_ker_le_range] at hS ⊢
    intro x (hx : _ = _)
    dsimp at hx
    rcases Concrete.colimit_exists_rep S.X₂ x with ⟨j, y, rfl⟩
    rw [← ConcreteCategory.comp_apply, colimMap_eq, colimit.ι_map, ConcreteCategory.comp_apply,
      ← map_zero (colimit.ι S.X₃ j).hom] at hx
    rcases Concrete.colimit_exists_of_rep_eq.{u, u, u} S.X₃ _ _ hx with ⟨k, e₁, e₂, hk⟩
    rw [map_zero, ← ConcreteCategory.comp_apply, ← NatTrans.naturality, ConcreteCategory.comp_apply]
      at hk
    rcases hS k hk with ⟨t, ht⟩
    use colimit.ι S.X₁ k t
    erw [← ConcreteCategory.comp_apply, colimit.ι_map, ConcreteCategory.comp_apply, ht]
    exact colimit.w_apply S.X₂ e₁ y

Goal state after:
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
⊢ HasExactLimitsOfShape (Discrete J) AddCommGrpCat

Tactic:
by
  apply +allowSynthFailures hasExactLimitsOfShape_of_preservesEpi
  exact {
    preserves {X Y} f hf := by
      let iX : limit X ≅ AddCommGrpCat.of ((i : J) → X.obj ⟨i⟩) := (Pi.isoLimit X).symm ≪≫
        (limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit
      let iY : limit Y ≅ AddCommGrpCat.of ((i : J) → Y.obj ⟨i⟩) := (Pi.isoLimit Y).symm ≪≫
        (limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit
      have : Pi.map (fun i ↦ f.app ⟨i⟩) = iX.inv ≫ lim.map f ≫ iY.hom := by
        simp only [Discrete.functor_obj_eq_as, Discrete.mk_as, Pi.isoLimit,
          IsLimit.conePointUniqueUpToIso, limit.cone, AddCommGrpCat.HasLimit.productLimitCone,
          Iso.trans_inv, Functor.mapIso_inv, IsLimit.uniqueUpToIso_inv, Cone.forget_map,
          IsLimit.liftConeMorphism_hom, limit.isLimit_lift, Iso.symm_inv, Functor.mapIso_hom,
          IsLimit.uniqueUpToIso_hom, lim_map, Iso.trans_hom, Iso.symm_hom,
          AddCommGrpCat.HasLimit.lift, Category.assoc, limit.lift_map_assoc, iX, iY]
        ext g j
        change _ = (_ ≫ limit.π (Discrete.functor fun j ↦ Y.obj { as := j }) ⟨j⟩) _
        simp only [Discrete.functor_obj_eq_as, productIsProduct', limit.lift_π,
          Fan.mk_π_app, Pi.map_apply]
        change _ = (_ ≫ _ ≫ limit.π Y ⟨j⟩) _
        simp
      suffices Epi (iX.hom ≫ (iX.inv ≫ lim.map f ≫ iY.hom) ≫ iY.inv) by simpa using this
      suffices Epi (iX.inv ≫ lim.map f ≫ iY.hom) from inferInstance
      rw [AddCommGrpCat.epi_iff_surjective, ← this]
      simp_rw [CategoryTheory.NatTrans.epi_iff_epi_app, AddCommGrpCat.epi_iff_surjective] at hf
      refine fun b ↦ ⟨fun i ↦ (hf ⟨i⟩ (b i)).choose, ?_⟩
      funext i
      exact (hf ⟨i⟩ (b i)).choose_spec }

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

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
this :
  ∀ (u : G.ColimitType) (x : F.obj X),
    G.descColimitType c u = x → G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ColimitType
hu :
  ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₁ =
    ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₂
x : c.pt
hx₁ : G.descColimitType c u₁ = x
hx₂ : G.descColimitType c u₂ = x
⊢ G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u₂

Tactic:
← this _ _ hx₂

Goal state after:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
G : F.Elementsᵒᵖ ⥤ Type w := (CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X
c : G.CoconeTypes := G.coconeTypesEquiv.symm (coconeπOpCompShrinkYonedaObj F X)
this :
  ∀ (u : G.ColimitType) (x : F.obj X),
    G.descColimitType c u = x → G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) = u
u₁ u₂ : ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).ColimitType
hu :
  ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₁ =
    ((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).descColimitType
      (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
        (coconeπOpCompShrinkYonedaObj F X))
      u₂
x : c.pt
hx₁ : G.descColimitType c u₁ = x
hx₂ : G.descColimitType c u₂ = x
⊢ G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X)) =
    G.ιColimitType (op (F.elementsMk X x)) (shrinkYonedaObjObjEquiv.symm (𝟙 X))
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

Goal state before:
pp: G H : AddCommGrpCat
p : ↑G
q : ↑H
⊢ (hom (Functor.LaxMonoidal.μ (forget AddCommGrpCat) G H)) (p, q) = (p, q)

Tactic:
apply Prod.ext
  · exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_fst (forget AddCommGrpCat.{u}) G H) (p, q)
  · exact congr_hom (CC := fun X ↦ X) (Functor.Monoidal.μ_snd (forget AddCommGrpCat.{u}) G H) (p, q)

Goal state after:
Module: Mathlib.Data.ZMod.IntUnitsPower

Goal state before:
pp: z₁ z₂ : ZMod 2
au : Additive ℤˣ
⊢ Additive.toMul au ^ (z₁ * z₂).val = (Additive.toMul au ^ z₂.val) ^ z₁.val

Tactic:
rw [← pow_mul, ZMod.val_mul, ← Int.units_pow_eq_pow_mod_two, mul_comm]

Goal state after: