mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ (inv (coimageImageComparison f) ≫ cokernel.desc (kernel.ι f) F.e ⋯) ≫ F.m = (imageMonoFactorisation f).m

Tactic:
rw [imageMonoFactorisation_m]

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
inst✝² : HasKernels C
inst✝¹ : HasCokernels C
X Y : C
f : X ⟶ Y
inst✝ : IsIso (coimageImageComparison f)
F : MonoFactorisation f
⊢ (inv (coimageImageComparison f) ≫ cokernel.desc (kernel.ι f) F.e ⋯) ≫ F.m = kernel.ι (cokernel.π f)
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (factorThruImage f ≫ (imageIsoImage f).inv) ≫ equalizer.ι (cokernel.π f) 0 =
    (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) ≫ equalizer.ι (cokernel.π f) 0

Tactic:
rw [IsImage.isoExt_inv, image.isImage_lift, Limits.image.fac_lift,
    imageStrongEpiMonoFactorisation_e, Category.assoc, kernel.lift_ι, equalizer_as_kernel,
    kernel.lift_ι, Limits.image.fac]

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Abelian C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
i : X ⟶ Y
inst✝³ : HasCokernel i
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Mono (F.map i)
inst✝ : PreservesColimit (parallelPair i 0) F
e : parallelPair (cokernel.π (F.map i)) 0 ≅ parallelPair (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext (Iso.refl ((parallelPair (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
hi : IsLimit (KernelFork.ofι (F.map i) ⋯) :=
  monoIsKernelOfCokernel (Cofork.ofπ (cokernel.π (F.map i)) ⋯) (cokernelIsCokernel (F.map i))
⊢ 𝟙 (F.obj X) ≫ F.map i ≫ 𝟙 (F.obj Y) = F.map i

Tactic:
Category.comp_id,

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Abelian C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
i : X ⟶ Y
inst✝³ : HasCokernel i
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Mono (F.map i)
inst✝ : PreservesColimit (parallelPair i 0) F
e : parallelPair (cokernel.π (F.map i)) 0 ≅ parallelPair (cokernel.π i) 0 ⋙ F :=
  parallelPair.ext (Iso.refl ((parallelPair (cokernel.π (F.map i)) 0).obj WalkingParallelPair.zero))
    (asIso (cokernelComparison i F)) ⋯ ⋯
hi : IsLimit (KernelFork.ofι (F.map i) ⋯) :=
  monoIsKernelOfCokernel (Cofork.ofπ (cokernel.π (F.map i)) ⋯) (cokernelIsCokernel (F.map i))
⊢ 𝟙 (F.obj X) ≫ F.map i = F.map i
Module: Mathlib.CategoryTheory.Abelian.Basic

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Abelian C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
p : X ⟶ Y
inst✝³ : HasKernel p
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Epi (F.map p)
inst✝ : PreservesLimit (parallelPair p 0) F
e : parallelPair (kernel.ι p) 0 ⋙ F ≅ parallelPair (kernel.ι (F.map p)) 0 :=
  parallelPair.ext (asIso (kernelComparison p F))
    (Iso.refl ((parallelPair (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) ⋯ ⋯
hp : IsColimit (CokernelCofork.ofπ (F.map p) ⋯) :=
  epiIsCokernelOfKernel (Fork.ofι (kernel.ι (F.map p)) ⋯) (kernelIsKernel (F.map p))
⊢ F.map p ≫ 𝟙 (F.obj Y) = 𝟙 (F.obj X) ≫ F.map p

Tactic:
Category.comp_id,

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
inst✝⁶ : Abelian C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : HasZeroMorphisms D
X Y : D
p : X ⟶ Y
inst✝³ : HasKernel p
F : D ⥤ C
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : Epi (F.map p)
inst✝ : PreservesLimit (parallelPair p 0) F
e : parallelPair (kernel.ι p) 0 ⋙ F ≅ parallelPair (kernel.ι (F.map p)) 0 :=
  parallelPair.ext (asIso (kernelComparison p F))
    (Iso.refl ((parallelPair (kernel.ι p) 0 ⋙ F).obj WalkingParallelPair.one)) ⋯ ⋯
hp : IsColimit (CokernelCofork.ofπ (F.map p) ⋯) :=
  epiIsCokernelOfKernel (Fork.ofι (kernel.ι (F.map p)) ⋯) (kernelIsKernel (F.map p))
⊢ F.map p = 𝟙 (F.obj X) ≫ F.map p
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (fun x ↦ β⁻¹ • x) ((fun x ↦ β • x) x) = x

Tactic:
dsimp only

Goal state after:
A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ β⁻¹ • β • x = x
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (fun x ↦ β • x) ((fun x ↦ β⁻¹ • x) x) = x

Tactic:
dsimp only

Goal state after:
A B : GrpCat
f : A ⟶ B
β : ↑B
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ β • β⁻¹ • x = x
Module: Mathlib.Algebra.Homology.ShortComplex.RightHomology

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ₁ ψ₂ : RightHomologyMapData φ h₁ h₂
hQ : ψ₁.φQ = ψ₂.φQ
⊢ ψ₁.φH = ψ₂.φH

Tactic:
rw [← cancel_mono h₂.ι, commι, commι, hQ]

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

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
ψ : RightHomologyMapData φ h₁ h₂
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : h₁.IsPreservedBy F
inst✝ : h₂.IsPreservedBy F
⊢ F.map ψ.φQ ≫ (h₂.map F).g' = (h₁.map F).g' ≫ (F.mapShortComplex.map φ).τ₃

Tactic:
by simpa only [RightHomologyData.map_g', F.map_comp] using! F.congr_map ψ.commg'

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

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ F.map (hₗ.i ≫ hᵣ.p) = (hₗ.map F).π ≫ leftRightHomologyComparison' (hₗ.map F) (hᵣ.map F) ≫ (hᵣ.map F).ι

Tactic:
ShortComplex.π_leftRightHomologyComparison'_ι

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✝⁴ : HasZeroMorphisms C
inst✝³ : HasZeroMorphisms D
S : ShortComplex C
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
hₗ : S.LeftHomologyData
hᵣ : S.RightHomologyData
inst✝¹ : hₗ.IsPreservedBy F
inst✝ : hᵣ.IsPreservedBy F
⊢ F.map (hₗ.i ≫ hᵣ.p) = (hₗ.map F).i ≫ (hᵣ.map F).p
Module: Mathlib.Algebra.Homology.ShortComplex.Abelian

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
S : ShortComplex C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : HasZeroMorphisms D
kf : KernelFork S.g
cc : CokernelCofork S.f
hkf : IsLimit kf
hcc : IsColimit cc
H : C
π : kf.pt ⟶ H
ι : H ⟶ cc.pt
fac : Fork.ι kf ≫ Cofork.π cc = π ≫ ι
inst✝¹ : Epi π
inst✝ : Mono ι
⊢ Cofork.π
        ((Cocone.precompose
              (parallelPair.ext
                  (Iso.refl
                    ((parallelPair ((hkf.ofIsoLimit (Fork.ext (Iso.refl kf.pt) ⋯)).lift (KernelFork.ofι S.f ⋯)) 0).obj
                      WalkingParallelPair.zero))
                  (S.isoCyclesOfIsLimit hkf) ⋯ ⋯).inv).obj
          (CokernelCofork.ofπ π ⋯)) ≫
      (isoHomology S hkf hcc fac).hom =
    Cofork.π (CokernelCofork.ofπ S.homologyπ ⋯)

Tactic:
simp [Cofork.π]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Basic

Goal state before:
pp: case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ F.map f' ≫ adj.counit.app E✝ ≫ g = f

Tactic:
← Adjunction.counit_naturality,

Goal state after:
case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesEpimorphisms
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = adj.unit.app P ≫ G.map f
⊢ F.map f' ≫ F.map (G.map g) ≫ adj.counit.app X✝ = f
Module: Mathlib.Algebra.Homology.ShortComplex.Exact

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : IsZero S.X₂
⊢ S.Exact

Tactic:
rw [(HomologyData.ofZeros S (IsZero.eq_of_tgt h _ _) (IsZero.eq_of_src h _ _)).exact_iff]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h : IsZero S.X₂
⊢ IsZero (HomologyData.ofZeros S ⋯ ⋯).left.H
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
⊢ S.Exact ↔ ∀ (x₂ : ↑S.X₂), (ConcreteCategory.hom S.g) x₂ = 0 → ∃ x₁, (ConcreteCategory.hom S.f) x₁ = x₂

Tactic:
rw [exact_iff_surjective_abToCycles]
  constructor
  · intro h x₂ hx₂
    obtain ⟨x₁, hx₁⟩ := h ⟨x₂, hx₂⟩
    exact ⟨x₁, by simpa only [Subtype.ext_iff, abToCycles_apply_coe] using hx₁⟩
  · rintro h ⟨x₂, hx₂⟩
    obtain ⟨x₁, rfl⟩ := h x₂ hx₂
    exact ⟨x₁, rfl⟩

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

Goal state before:
pp: S : ShortComplex Ab
⊢ S.Exact ↔ (AddCommGrpCat.Hom.hom S.f).range = (AddCommGrpCat.Hom.hom S.g).ker

Tactic:
rw [ab_exact_iff_ker_le_range]
  constructor
  · intro h
    refine le_antisymm ?_ h
    rintro _ ⟨x₁, rfl⟩
    rw [AddMonoidHom.mem_ker, ← ConcreteCategory.comp_apply, S.zero]
    rfl
  · intro h
    rw [h]

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact ∧ Mono φ.τ₂

Tactic:
refine ⟨?_, this⟩

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
hf₁ : S₁.f = 0
hg₁ : S₁.g = 0
hf₂ : S₂.f = 0
w : φ.τ₂ ≫ S₂.g = 0
h : IsIso (S₂.liftCycles φ.τ₂ ⋯)
this : Mono φ.τ₂
⊢ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact
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 (a.arrow ≫ h) k)
        (PullbackCone.IsLimit.lift t (pullback.fst (a.arrow ≫ h) k ≫ a.arrow) (pullback.snd (a.arrow ≫ h) k) ⋯) ⋯ ≫
      pullback.snd a.obj.hom f ≫ g =
    pullback.snd (a.arrow ≫ h) k

Tactic:
rw [pullback.lift_snd_assoc]

Goal state after:
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
⊢ PullbackCone.IsLimit.lift t (pullback.fst (a.arrow ≫ h) k ≫ a.arrow) (pullback.snd (a.arrow ≫ h) k) ⋯ ≫ g =
    pullback.snd (a.arrow ≫ h) k
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: case mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ IsIso (imageToKernel S.f S.g ⋯) → imageSubobject S.f = kernelSubobject S.g

pp: case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ imageSubobject S.f = kernelSubobject S.g → IsIso (imageToKernel S.f S.g ⋯)

Tactic:
· intro
    exact Subobject.eq_of_comm (asIso (imageToKernel _ _ S.zero)) (by simp)

Goal state after:
case mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ imageSubobject S.f = kernelSubobject S.g → IsIso (imageToKernel S.f S.g ⋯)
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ L.map (Abelian.factorThruImage S.f) ≫ L.map (kernel.ι (cokernel.π S.f)) = L.map S.f ≫ 𝟙 (L.obj S.X₂)

Tactic:
Category.comp_id,

Goal state after:
A : Type u₁
B : Type u₂
inst✝⁶ : Category.{v₁, u₁} A
inst✝⁵ : Category.{v₂, u₂} B
inst✝⁴ : Abelian A
inst✝³ : Abelian B
L : A ⥤ B
inst✝² : L.PreservesZeroMorphisms
inst✝¹ : L.PreservesEpimorphisms
inst✝ : ∀ {X Y : A} (f : X ⟶ Y), PreservesLimit (parallelPair f 0) L
S : ShortComplex A
hS : S.Exact
⊢ L.map (Abelian.factorThruImage S.f) ≫ L.map (kernel.ι (cokernel.π S.f)) = L.map S.f
Module: Mathlib.CategoryTheory.Abelian.FunctorCategory

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (coimageImageComparison α).app X = (coimageObjIso α X).hom ≫ coimageImageComparison (α.app X) ≫ (imageObjIso α X).inv

Tactic:
by
  simp only [coimageImageComparison_app, Iso.hom_inv_id_assoc, Iso.hom_inv_id, Category.assoc,
    Category.comp_id]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteProducts C
inst✝¹ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
inst✝ : HasLimitsOfShape (Discrete α) C
X✝ Y✝ : Discrete α ⥤ C
β : X✝ ⟶ Y✝
⊢ (liftToFinset C α ⋙ lim).map β ≫ (limit.isoLimitCone (liftToFinsetLimitCone Y✝)).symm.hom =
    (limit.isoLimitCone (liftToFinsetLimitCone X✝)).symm.hom ≫ lim.map β

Tactic:
by
      simp only [Functor.comp_obj, lim_obj, Functor.comp_map, lim_map, Iso.symm_hom]
      ext J
      simp [liftToFinset]

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
G : C ⥤ H
inst✝² : L.HasPointwiseLeftKanExtension G
inst✝¹ : HasColimitsOfShape D H
inst✝ : HasColimitsOfShape C H
X : Grothendieck (CostructuredArrow.functor L)
⊢ colimit.ι (CostructuredArrow.grothendieckProj L ⋙ G) X ≫ (L.colimitIsoColimitGrothendieck G).inv =
    colimit.ι G ((CostructuredArrow.proj L X.base).obj X.fiber)

Tactic:
by
  simp [colimitIsoColimitGrothendieck]

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x✝² : YonedaCollection F X
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₁ (η ≫ μ) x✝²).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom (((map₁ μ ∘ map₁ η) x✝²).fst.app x✝¹)).toFun x✝

pp: case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G H : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
μ : G ⟶ H
x✝ : YonedaCollection F X
⊢ (ConcreteCategory.hom (H.map (eqToHom ⋯))) ((map₁ μ ∘ map₁ η) x✝).snd = (map₁ (η ≫ μ) x✝).snd

Tactic:
all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
x✝² : YonedaCollection F X
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₂ F (𝟙 X) x✝²).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom ((id x✝²).fst.app x✝¹)).toFun x✝

pp: case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
x✝ : YonedaCollection F X
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯))) (id x✝).snd = (map₂ F (𝟙 X) x✝).snd

Tactic:
all_goals simp

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₂ : D
f : Y₁ ⟶ Y₂
g₁ g₂ : CostructuredArrow L Y₁
φ : g₁ ⟶ g₂
⊢ (CostructuredArrow.proj L Y₁ ⋙ F).map φ ≫
      colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g₂) =
    colimit.ι (CostructuredArrow.proj L Y₂ ⋙ F) ((CostructuredArrow.map f).obj g₁) ≫
      ((const (CostructuredArrow L Y₁)).obj (colimit (CostructuredArrow.proj L Y₂ ⋙ F))).map φ

Tactic:
simpa using colimit.w (CostructuredArrow.proj L Y₂ ⋙ F)
              ((CostructuredArrow.map f).map φ)

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝² : YonedaCollection F Z
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₂ F (f ≫ g) x✝²).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom (((map₂ F f ∘ map₂ F g) x✝²).fst.app x✝¹)).toFun x✝

pp: case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
x✝ : YonedaCollection F Z
⊢ (ConcreteCategory.hom (F.map (eqToHom ⋯))) ((map₂ F f ∘ map₂ F g) x✝).snd = (map₂ F (f ≫ g) x✝).snd

Tactic:
all_goals simp

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: case h
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
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
x✝¹ : Cᵒᵖ
x✝ : (yoneda.obj X).obj x✝¹
⊢ (ConcreteCategory.hom ((map₂ G f (map₁ η p)).fst.app x✝¹)).toFun x✝ =
    (ConcreteCategory.hom ((map₁ η (map₂ F f p)).fst.app x✝¹)).toFun x✝

pp: case h'
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
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ (ConcreteCategory.hom (G.map (eqToHom ⋯))) (map₁ η (map₂ F f p)).snd = (map₂ G f (map₁ η p)).snd

Tactic:
all_goals simp

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
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ (L ⋙ L.pointwiseRightKanExtension F).map f ≫
      limit.π (StructuredArrow.proj (L.obj X₂) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₂))) =
    limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f

Tactic:
simp only [comp_map,
      pointwiseRightKanExtension_map, limit.lift_π, StructuredArrow.map_mk]

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
X₁ X₂ : C
f : X₁ ⟶ X₂
⊢ limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (L.map f ≫ 𝟙 (L.obj X₂))) =
    limit.π (StructuredArrow.proj (L.obj X₁) L ⋙ F) (StructuredArrow.mk (𝟙 (L.obj X₁))) ≫ F.map f
Module: Mathlib.CategoryTheory.Comma.Presheaf.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
T : Over A
X : CostructuredArrow yoneda A
f : (toOver yoneda A).obj X ⟶ T
⊢ (overEquivPresheafCostructuredArrow A).inverse.map
      ((ConcreteCategory.hom ((toOverCompYoneda A T).hom.app (op X))) f) =
    (toOverCompOverEquivPresheafCostructuredArrow A).isoCompInverse.inv.app X ≫
      f ≫ (overEquivPresheafCostructuredArrow A).unit.app T

Tactic:
by
  simp [CostructuredArrow.toOverCompYoneda]

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
T : Over A
X : CostructuredArrow yoneda A
f : yoneda.obj X ⟶ (overEquivPresheafCostructuredArrow A).functor.obj T
⊢ (overEquivPresheafCostructuredArrow A).functor.map
      ((ConcreteCategory.hom ((toOverCompYoneda A T).inv.app (op X))) f) =
    (toOverCompOverEquivPresheafCostructuredArrow A).hom.app X ≫ f

Tactic:
by
  simp [CostructuredArrow.toOverCompYoneda]

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.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 : F ⊣ G
inst✝⁷ : F.Full
inst✝⁶ : F.Faithful
J : Type u'
inst✝⁵ : Category.{v', u'} J
inst✝⁴ : HasLimitsOfShape J C
inst✝³ : HasLimitsOfShape J D
inst✝² : HasExactLimitsOfShape J D
inst✝¹ : HasFiniteColimits C
inst✝ : PreservesFiniteColimits G
K : Type
x✝¹ : SmallCategory K
x✝ : FinCategory K
H : K ⥤ J ⥤ C
⊢ PreservesColimit H lim

Tactic:
by
    have : PreservesLimitsOfSize.{v', u'} G := adj.rightAdjoint_preservesLimits
    have : PreservesColimitsOfSize.{0, 0} F := adj.leftAdjoint_preservesColimits
    let e : (whiskeringRight J _ _).obj F ⋙ lim ⋙ G ≅ lim :=
      isoWhiskerLeft _ (preservesLimitNatIso G) ≪≫
        (Functor.associator _ _ _).symm ≪≫
        isoWhiskerRight (whiskeringRightObjCompIso F G) _ ≪≫
        isoWhiskerRight ((whiskeringRight J C C).mapIso (asIso adj.unit).symm) _ ≪≫
        isoWhiskerRight whiskeringRightObjIdIso _ ≪≫ lim.leftUnitor
    exact preservesColimit_of_natIso _ e

Goal state after:
Module: Mathlib.CategoryTheory.Comma.StructuredArrow.Small

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
⊢ ObjectProperty.Small.{v₁, v₁, max u₁ v₂} (P.inverseImage (proj S T))

Tactic:
by
  suffices P.inverseImage (proj S T) = .ofObj fun f : Σ (G : Subtype P), S ⟶ T.obj G => mk f.2 by
    rw [this]
    infer_instance
  ext X
  simp only [ObjectProperty.prop_inverseImage_iff, proj_obj, ObjectProperty.ofObj_iff,
    Sigma.exists, Subtype.exists, exists_prop]
  exact ⟨fun h ↦ ⟨_, h, _, rfl⟩, by rintro ⟨_, h, _, rfl⟩; exact h⟩

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
⊢ HasCokernel f

Tactic:
have : PreservesColimits G := adj.leftAdjoint_preservesColimits

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
this : PreservesColimits G
⊢ HasCokernel f