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

Goal state before:
pp: case h₁
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫
        { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₁ =
    (s.ι.app j).τ₁

pp: case h₂
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫
        { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₂ =
    (s.ι.app j).τ₂

pp: case h₃
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫
        { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₃ =
    (s.ι.app j).τ₃

Tactic:
· apply IsColimit.fac h₁

Goal state after:
case h₂
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫
        { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₂ =
    (s.ι.app j).τ₂

case h₃
J : Type u_1
C : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasZeroMorphisms C
F : J ⥤ ShortComplex C
c : Cocone F
h₁ : IsColimit (π₁.mapCocone c)
h₂ : IsColimit (π₂.mapCocone c)
h₃ : IsColimit (π₃.mapCocone c)
s : Cocone F
j : J
⊢ (c.ι.app j ≫
        { τ₁ := h₁.desc (π₁.mapCocone s), τ₂ := h₂.desc (π₂.mapCocone s), τ₃ := h₃.desc (π₃.mapCocone s), comm₁₂ := ⋯,
          comm₂₃ := ⋯ }).τ₃ =
    (s.ι.app j).τ₃
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
X Y Z : C
ι₁ : X ⟶ Z
ι₂ : Y ⟶ Z
inst✝ : PreservesColimit (parallelPair ι₂ 0) F
i : IsColimit (BinaryCofan.mk ι₁ ι₂)
bc : BinaryBicone X Y := BinaryBicone.ofColimitCocone i
presf : PreservesColimit (parallelPair bc.inr 0) F := inst✝
⊢ IsColimit (F.mapCocone (BinaryCofan.mk ι₁ ι₂))

Tactic:
let hf : IsColimit bc.inrCokernelCofork := BinaryBicone.isColimitInrCokernelCofork i

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
X Y Z : C
ι₁ : X ⟶ Z
ι₂ : Y ⟶ Z
inst✝ : PreservesColimit (parallelPair ι₂ 0) F
i : IsColimit (BinaryCofan.mk ι₁ ι₂)
bc : BinaryBicone X Y := BinaryBicone.ofColimitCocone i
presf : PreservesColimit (parallelPair bc.inr 0) F := inst✝
hf : IsColimit bc.inrCokernelCofork := BinaryBicone.isColimitInrCokernelCofork i
⊢ IsColimit (F.mapCocone (BinaryCofan.mk ι₁ ι₂))
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
S : ShortComplex C
hS : S.Exact
inst✝ : HasZeroObject C
kf : KernelFork S.g
hkf : IsLimit kf
this : S.HasHomology
⊢ Epi ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))

Tactic:
refine ((MorphismProperty.epimorphisms C).arrow_mk_iso_iff ?_).1
      hS.epi_toCycles

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✝² : Preadditive C
inst✝¹ : Preadditive D
S : ShortComplex C
hS : S.Exact
inst✝ : HasZeroObject C
kf : KernelFork S.g
hkf : IsLimit kf
this : S.HasHomology
⊢ Arrow.mk S.toCycles ≅ Arrow.mk ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯))
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
hf : S.f = 0
this✝¹ : S.HasHomology
this✝ : Epi S.toCycles
this : S.iCycles = 0
⊢ ∀ {P : C} (g : P ⟶ S.X₂), g ≫ S.g = 0 → g = 0

Tactic:
intro A

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
this✝¹ : S.HasHomology
this✝ : Epi S.toCycles
this : S.iCycles = 0
A : C
⊢ ∀ (g : A ⟶ S.X₂), g ≫ S.g = 0 → g = 0
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
this : S.pOpcycles = 0
⊢ ∀ {R : C} (g : S.X₂ ⟶ R), S.f ≫ g = 0 → g = 0

Tactic:
intro A

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
this : S.pOpcycles = 0
A : C
⊢ ∀ (g : S.X₂ ⟶ A), S.f ≫ g = 0 → g = 0
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
s : S.Splitting
⊢ Mono S.f

Tactic:
have := s.isSplitMono_f

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
this : IsSplitMono S.f
⊢ Mono S.f
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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
S S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ e.inv.τ₃ ≫ s.s ≫ S₁.g ≫ e.hom.τ₃ = 𝟙 S₂.X₃

Tactic:
s.s_g_assoc,

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✝¹ : Preadditive C
inst✝ : Preadditive D
S S₁ S₂ : ShortComplex C
s : S₁.Splitting
e : S₁ ≅ S₂
⊢ e.inv.τ₃ ≫ e.hom.τ₃ = 𝟙 S₂.X₃
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

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₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
⊢ ∀ (P : C) (g : P ⟶ S₁.X₂), g ≫ φ.τ₂ = 0 → g = 0

Tactic:
intro A

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₁.Exact
inst✝³ : Mono S₁.f
inst✝² : Mono S₂.f
inst✝¹ : Mono φ.τ₁
inst✝ : Mono φ.τ₃
A : C
⊢ ∀ (g : A ⟶ S₁.X₂), g ≫ φ.τ₂ = 0 → g = 0
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✝¹ : Balanced C
inst✝ : S.HasHomology
⊢ S.Exact ∧ Mono S.f ↔ Nonempty (IsLimit (KernelFork.ofι S.f ⋯))

Tactic:
constructor
  · intro ⟨hS, _⟩
    exact ⟨hS.fIsKernel⟩
  · intro ⟨hS⟩
    exact ⟨S.exact_of_f_is_kernel hS, mono_of_isLimit_fork hS⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
⊢ { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ }.unop.Exact ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ Epi φ.τ₂

Tactic:
have : Mono φ.τ₂.op ↔ Epi φ.τ₂ :=
    ⟨fun _ => unop_epi_of_mono φ.τ₂.op, fun _ => op_mono_of_epi _⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
hg₂ : S₂.g = 0
this : Mono φ.τ₂.op ↔ Epi φ.τ₂
⊢ { X₁ := S₂.op.X₂, X₂ := S₁.op.X₂, X₃ := S₁.op.X₃, f := (opMap φ).τ₂, g := S₁.op.g, zero := ⋯ }.unop.Exact ∧
      Mono (opMap φ).τ₂ ↔
    { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ Epi φ.τ₂
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasCokernels C
X : C
⊢ ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g],
    Subobject.mk f ≤ Subobject.mk g →
      Subobject.lift (fun x f x_1 ↦ Subobject.mk (cokernel.π f).op) ⋯ (Subobject.mk f) ≤
        Subobject.lift (fun x f x_1 ↦ Subobject.mk (cokernel.π f).op) ⋯ (Subobject.mk g)

Tactic:
intro A

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasCokernels C
X A : C
⊢ ∀ ⦃B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g],
    Subobject.mk f ≤ Subobject.mk g →
      Subobject.lift (fun x f x_1 ↦ Subobject.mk (cokernel.π f).op) ⋯ (Subobject.mk f) ≤
        Subobject.lift (fun x f x_1 ↦ Subobject.mk (cokernel.π f).op) ⋯ (Subobject.mk g)
Module: Mathlib.CategoryTheory.Subobject.Limits

Goal state before:
pp: 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) [inst : Mono f] [inst_1 : Mono g],
    Subobject.mk f ≤ Subobject.mk g →
      Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk f) ≤
        Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk g)

Tactic:
intro A

Goal state after:
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 : Cᵒᵖ
⊢ ∀ ⦃B : Cᵒᵖ⦄ (f : A ⟶ op X) (g : B ⟶ op X) [inst : Mono f] [inst_1 : Mono g],
    Subobject.mk f ≤ Subobject.mk g →
      Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk f) ≤
        Subobject.lift (fun x f x_1 ↦ Subobject.mk (kernel.ι f.unop)) ⋯ (Subobject.mk g)
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).ShortExact, ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      F.PreservesHomology, PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE

Tactic:
tfae_have 1 → 3
  | hF => by
    refine ⟨fun {X Y} f ↦ ?_, fun {X Y} f ↦ ?_⟩
    · have h := (preservesFiniteLimits_tfae F |>.out 0 2 |>.1 fun S hS ↦
        And.intro (hF S hS).exact (hF S hS).mono_f)
      exact h f
    · have h := (preservesFiniteColimits_tfae F |>.out 0 2 |>.1 fun S hS ↦
        And.intro (hF S hS).exact (hF S hS).epi_g)
      exact h f

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_3 : (∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact) → F.PreservesHomology
⊢ [∀ (S : ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : ShortComplex C), S.Exact → (S.map F).Exact,
      F.PreservesHomology, PreservesFiniteLimits F ∧ PreservesFiniteColimits F].TFAE
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: case mp
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 eL Y Y' e

Goal state after:
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
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ counitForward F (unop s) ((ConcreteCategory.hom (F.map f)) x) = (counitForward F (unop t) x).map₂ f.unop.left ⋯

Tactic:
refine OverArrows.ext <| YonedaCollection.ext (by simp) ?_

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
s t : (CostructuredArrow yoneda A)ᵒᵖ
f : t ⟶ s
x : F.obj t
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯)))
      (YonedaCollection.snd ((counitForward F (unop t) x).map₂ f.unop.left ⋯).val) =
    YonedaCollection.snd (counitForward F (unop s) ((ConcreteCategory.hom (F.map f)) x)).val
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ ∀ ⦃A : Cᵒᵖ⦄ (f : A ⟶ op X) [inst : Mono f],
    ((cokernelOrderHom X).comp (kernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)

Tactic:
intro A

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
A : Cᵒᵖ
⊢ ∀ (f : A ⟶ op X) [inst : Mono f],
    ((cokernelOrderHom X).comp (kernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)
Module: Mathlib.CategoryTheory.Abelian.Subobject

Goal state before:
pp: case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
⊢ ∀ ⦃A : C⦄ (f : A ⟶ X) [inst : Mono f],
    ((kernelOrderHom X).comp (cokernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk f)

Tactic:
intro A

Goal state after:
case refine_2
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X A : C
⊢ ∀ (f : A ⟶ X) [inst : Mono f],
    ((kernelOrderHom X).comp (cokernelOrderHom X)) (Subobject.mk f) = OrderHom.id (Subobject.mk 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
⊢ (fun g ↦ { app := fun y ↦ (uliftYonedaEquiv (y.hom ≫ g)).down, naturality := ⋯ })
      ((fun f ↦
          { app := fun x ↦ ↾fun x_1 ↦ { down := f.app (CostructuredArrow.mk (uliftYonedaEquiv.symm x_1)) },
            naturality := ⋯ })
        f) =
    f

Tactic:
by
    ext X
    let e : CostructuredArrow.mk
      (uliftYonedaEquiv.{max w v₂}.symm (X.hom.app (op X.left) ⟨𝟙 X.left⟩)) ≅ X :=
        CostructuredArrow.isoMk (Iso.refl _) (by
          ext Y x
          dsimp
          simp [← NatTrans.naturality_apply])
    simpa [e] using! f.naturality e.inv

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Transfer

Goal state before:
pp: C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteProducts C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝ : HasKernels C
this : HasCokernels C
X Y : C
f : X ⟶ Y
⊢ IsIso (Abelian.coimageImageComparison f)

Tactic:
let arrowIso : Arrow.mk (G.map (F.map f)) ≅ Arrow.mk f :=
      ((Functor.mapArrowFunctor _ _).mapIso i).app (Arrow.mk f)

Goal state after:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasFiniteProducts C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝¹ : G.PreservesZeroMorphisms
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this✝ : HasKernels C
this : HasCokernels C
X Y : C
f : X ⟶ Y
arrowIso : Arrow.mk (G.map (F.map f)) ≅ Arrow.mk f := ((Functor.mapArrowFunctor C C).mapIso i).app (Arrow.mk f)
⊢ IsIso (Abelian.coimageImageComparison f)
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P₁ P₂ : Cᵒᵖ ⥤ Type (max w v₁)
α : P₁ ⟶ P₂
j : P₁.Elementsᵒᵖ
⊢ (coconeOfRepresentable P₁).ι.app j ≫ α = (coconeOfRepresentable P₂).ι.app ((CategoryOfElements.map α).op.obj j)

Tactic:
ext T f
  simp [uliftYonedaEquiv]

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

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ∀ (T : C), Function.Bijective fun x ↦ x ≫ f
⊢ ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op G)).map f))

Tactic:
intro A

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst✝ : Mono f
h : ∀ (T : C), Function.Bijective fun x ↦ x ≫ f
A : C
⊢ P A → Function.Surjective ⇑(ConcreteCategory.hom ((coyoneda.obj (op A)).map f))
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : ∀ (T : C), Function.Bijective fun x ↦ f ≫ x
⊢ ∀ (G : C), P G → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj G).map f.op))

Tactic:
intro A

Goal state after:
case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst✝ : Epi f
h : ∀ (T : C), Function.Bijective fun x ↦ f ≫ x
A : C
⊢ P A → Function.Surjective ⇑(ConcreteCategory.hom ((yoneda.obj A).map f.op))
Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
⊢ SolutionSetCondition G

Tactic:
intro A

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
G : D ⥤ C
inst✝ : G.IsRightAdjoint
A : C
⊢ ∃ ι B f, ∀ (X : D) (h : A ⟶ G.obj X), ∃ i g, f i ≫ G.map g = h
Module: Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
hG : SolutionSetCondition G
⊢ ∀ (A : C), HasInitial (StructuredArrow A G)

Tactic:
intro A

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₁
inst✝² : Category.{v₁, u₁} D
G : D ⥤ C
inst✝¹ : HasLimits D
inst✝ : PreservesLimitsOfSize.{v₁, v₁, v₁, v, u₁, u} G
hG : SolutionSetCondition G
A : C
⊢ HasInitial (StructuredArrow A G)
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case refine_2
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 Q : (CostructuredArrow S T)ᵒᵖ
f : P ⟶ op A
g : Q ⟶ op A
hf : Mono f
hg : Mono g
h :
  { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk f) ≤
    { toFun := fun P ↦ ⟨projectQuotient P, ⋯⟩, invFun := fun P ↦ liftQuotient ↑P ⋯, left_inv := ⋯, right_inv := ⋯ }
      (Subobject.mk g)
⊢ (homMk (Subobject.ofMkLEMk (MonoOver.mk f).arrow.unop.left.op (MonoOver.mk g).arrow.unop.left.op h).unop ⋯).op ≫ g = f

Tactic:
apply Quiver.Hom.unop_inj
      ext
      exact unop_left_comp_ofMkLEMk_unop _

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

Goal state before:
pp: case e'_2.mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
X : C
⊢ G = X ∨ H = X → ∃ i, WalkingPair.rec G H i = X

Tactic:
rintro (rfl | rfl); exacts [⟨.left, rfl⟩, ⟨.right, rfl⟩]

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

Goal state before:
pp: case e'_2.mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
X : C
⊢ G = X ∨ H = X → ∃ i, WalkingPair.rec G H i = X

Tactic:
rintro (rfl | rfl); exacts [⟨.left, rfl⟩, ⟨.right, rfl⟩]

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

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
⊢ Epi (iX.inv ≫ lim.map f ≫ iY.hom)

Tactic:
rw [AddCommGrpCat.epi_iff_surjective, ← this]

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
hf : Epi f
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
⊢ Function.Surjective (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i })))
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
hf : ∀ (k : Discrete J), Function.Surjective ⇑(ConcreteCategory.hom (f.app k))
b : ↑(AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })))
⊢ (Pi.map (fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) fun i ↦ ⋯.choose) = b

Tactic:
funext i

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
X Y : Discrete J ⥤ AddCommGrpCat
f : X ⟶ Y
iX : limit X ≅ AddCommGrpCat.of ((i : J) → ↑(X.obj { as := i })) :=
  (Pi.isoLimit X).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ X.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ X.obj { as := j }).isLimit
iY : limit Y ≅ AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })) :=
  (Pi.isoLimit Y).symm ≪≫
    (limit.isLimit (Discrete.functor fun j ↦ Y.obj { as := j })).conePointUniqueUpToIso
      (AddCommGrpCat.HasLimit.productLimitCone fun j ↦ Y.obj { as := j }).isLimit
this :
  (Pi.map fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) = ⇑(ConcreteCategory.hom (iX.inv ≫ lim.map f ≫ iY.hom))
hf : ∀ (k : Discrete J), Function.Surjective ⇑(ConcreteCategory.hom (f.app k))
b : ↑(AddCommGrpCat.of ((i : J) → ↑(Y.obj { as := i })))
i : J
⊢ Pi.map (fun i ↦ ⇑(ConcreteCategory.hom (f.app { as := i }))) (fun i ↦ ⋯.choose) i = b i