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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
P Q : C
f : P ⟶ Q
I : C := Abelian.coimage f
i : Abelian.coimage f ⟶ Q := Abelian.factorThruCoimage f
p : P ⟶ cokernel (kernel.ι f) := cokernel.π (kernel.ι f)
R : C
g : R ⟶ I
hgi : g ≫ i = 0
u : P ⟶ cokernel g := p ≫ cokernel.π g
hu : NormalEpi u
h : NormalEpi.W u ⟶ P := NormalEpi.g
t : cokernel g ⟶ Q
ht : cokernel.π g ≫ t = i
hf : h ≫ f = 0
l : NormalEpi.W u ⟶ kernel f
hl : l ≫ kernel.ι f = h
⊢ (l ≫ kernel.ι f) ≫ p = l ≫ 0

Tactic:
by rw [Category.assoc, cokernel.condition]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasCokernel f
inst✝⁴ : HasKernel (cokernel.π f)
inst✝³ : PreservesColimit (parallelPair f 0) F
inst✝² : PreservesLimit (parallelPair (cokernel.π f) 0) F
inst✝¹ : HasCokernel (F.map f)
inst✝ : HasKernel (cokernel.π (F.map f))
⊢ Abelian.factorThruImage (F.map f) ≫ (iso F f).inv = F.map (Abelian.factorThruImage f)

Tactic:
by
  simp [Iso.comp_inv_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages

Goal state before:
pp: C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasKernel f
inst✝⁴ : HasCokernel (kernel.ι f)
inst✝³ : PreservesLimit (parallelPair f 0) F
inst✝² : PreservesColimit (parallelPair (kernel.ι f) 0) F
inst✝¹ : HasKernel (F.map f)
inst✝ : HasCokernel (kernel.ι (F.map f))
⊢ coimage.π (F.map f) ≫ (iso F f).inv = F.map (coimage.π f)

Tactic:
by
  simp [Iso.comp_inv_eq]

Goal state after:
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
h : S.RightHomologyData
A : C
hf : S.f = 0
c : KernelFork S.g
hc : IsLimit c
T : C
φ : S.X₂ ⟶ T
⊢ S.f ≫ φ = 0

Tactic:
simp [hf]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
h : S.LeftHomologyData
A K' H' : C
eK : K' ≅ h.K
eH : H' ≅ h.H
⊢ (eK.hom ≫ h.i) ≫ S.g = 0

Tactic:
by rw [assoc, h.wi, comp_zero]

Goal state after:
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₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ opcyclesMap φ = h₁.opcyclesIso.hom ≫ γ.φQ ≫ h₂.opcyclesIso.inv

Tactic:
dsimp [RightHomologyData.opcyclesIso, cyclesMapIso']
  rw [← γ.opcyclesMap'_eq, ← opcyclesMap'_comp, ← opcyclesMap'_comp, id_comp, comp_id]
  rfl

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

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₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
⊢ S₁.LeftHomologyData

Tactic:
have hπ : IsColimit (CokernelCofork.ofπ h.π wπ) := CokernelCofork.IsColimit.ofπ _ _
    (fun x hx => h.descH x (by rw [← cancel_epi φ.τ₁, ← reassoc_of% hf'', hx, comp_zero]))
    (fun x hx => π_descH _ _ _)
    (fun x hx b hx => by rw [← cancel_epi h.π, π_descH, hx])

Goal state after:
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : HasZeroMorphisms C
S S₁ S₂ S₃ : ShortComplex C
φ : S₁ ⟶ S₂
h : S₂.LeftHomologyData
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
i : h.K ⟶ S₁.X₂ := h.i ≫ inv φ.τ₂
wi : i ≫ S₁.g = 0
hi : IsLimit (KernelFork.ofι i wi)
f' : (KernelFork.ofι S₁.f ⋯).pt ⟶ (KernelFork.ofι i wi).pt := hi.lift (KernelFork.ofι S₁.f ⋯)
hf' : f' ≫ i = S₁.f
hf'' : f' = φ.τ₁ ≫ h.f'
wπ : f' ≫ h.π = 0
hπ : IsColimit (CokernelCofork.ofπ h.π wπ)
⊢ S₁.LeftHomologyData
Module: Mathlib.Algebra.Homology.ShortComplex.Limits

Goal state before:
pp: 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
eq₂ : ∀ (j : J), (c.ι.app j).τ₂ ≫ h₂.desc (π₂.mapCocone s) = (s.ι.app j).τ₂
eq₃ : ∀ (j : J), (c.ι.app j).τ₃ ≫ h₃.desc (π₃.mapCocone s) = (s.ι.app j).τ₃
eq₂₃ : ∀ (j : J), (c.ι.app j).τ₂ ≫ c.pt.g = (F.obj j).g ≫ (c.ι.app j).τ₃
eq₂₃' : ∀ (j : J), (s.ι.app j).τ₂ ≫ s.pt.g = (F.obj j).g ≫ (s.ι.app j).τ₃
⊢ (F.obj j).g ≫ (s.ι.app j).τ₃ = (c.ι.app j).τ₂ ≫ c.pt.g ≫ h₃.desc (π₃.mapCocone s)

Tactic:
reassoc_of% eq₂₃,

Goal state after:
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
eq₂ : ∀ (j : J), (c.ι.app j).τ₂ ≫ h₂.desc (π₂.mapCocone s) = (s.ι.app j).τ₂
eq₃ : ∀ (j : J), (c.ι.app j).τ₃ ≫ h₃.desc (π₃.mapCocone s) = (s.ι.app j).τ₃
eq₂₃ : ∀ (j : J), (c.ι.app j).τ₂ ≫ c.pt.g = (F.obj j).g ≫ (c.ι.app j).τ₃
eq₂₃' : ∀ (j : J), (s.ι.app j).τ₂ ≫ s.pt.g = (F.obj j).g ≫ (s.ι.app j).τ₃
⊢ (F.obj j).g ≫ (s.ι.app j).τ₃ = (F.obj j).g ≫ (c.ι.app j).τ₃ ≫ h₃.desc (π₃.mapCocone s)
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₂ : ShortComplex C
φ : S₁ ⟶ S₂
F : C ⥤ D
inst✝⁶ : F.PreservesZeroMorphisms
inst✝⁵ : S₁.HasHomology
inst✝⁴ : S₂.HasHomology
inst✝³ : (S₁.map F).HasHomology
inst✝² : (S₂.map F).HasHomology
inst✝¹ : F.PreservesRightHomologyOf S₁
inst✝ : F.PreservesRightHomologyOf S₂
⊢ homologyMap (F.mapShortComplex.map φ) ≫ (S₂.mapHomologyIso' F).hom =
    (S₁.mapHomologyIso' F).hom ≫ F.map (homologyMap φ)

Tactic:
dsimp only [Iso.trans, Iso.symm, Functor.mapIso, mapHomologyIso']
  simp only [← RightHomologyData.rightHomologyIso_hom_naturality_assoc _
    ((homologyData S₁).right.map F) ((homologyData S₂).right.map F), assoc,
    ← RightHomologyData.map_rightHomologyMap', ← F.map_comp,
    RightHomologyData.rightHomologyIso_inv_naturality _
      (homologyData S₁).right (homologyData S₂).right]

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 φ₁ φ₂
ψ : S₃ ⟶ S₁
⊢ (ψ ≫ φ₁).τ₃ = ψ.τ₃ ≫ h.h₃ + (ψ.τ₃ ≫ h.h₂) ≫ S₂.g + (ψ ≫ φ₂).τ₃

Tactic:
rw [comp_τ₃, comp_τ₃, h.comm₃, comp_add, comp_add, assoc]

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✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasKernel S.g
⊢ S.Exact ↔ Epi (kernel.lift S.g S.f ⋯)

Tactic:
by
  rw [exact_iff_epi_toCycles]
  apply (MorphismProperty.epimorphisms C).arrow_mk_iso_iff
  exact Arrow.isoMk (Iso.refl _) S.cyclesIsoKernel (by cat_disch)

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✝² : Preadditive C
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasCokernel S.f
⊢ S.Exact ↔ Mono (cokernel.desc S.f S.g ⋯)

Tactic:
by
  rw [exact_iff_mono_fromOpcycles]
  refine (MorphismProperty.monomorphisms C).arrow_mk_iso_iff (Iso.symm ?_)
  exact Arrow.isoMk S.opcyclesIsoCokernel.symm (Iso.refl _) (by cat_disch)

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✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
a✝ : Epi S.f
⊢ S.g = 0

Tactic:
rw [← cancel_epi S.f, zero, comp_zero]

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✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
this : Epi S.g
⊢ s.s ≫ s.r = 0

Tactic:
simp only [← cancel_epi S.g, comp_zero, g_s_assoc, sub_comp, id_comp,
    assoc, f_r, comp_id, sub_self]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
⊢ (imageSubobjectIso f).hom ≫ image.ι f = (imageSubobject f).arrow

Tactic:
simp [imageSubobjectIso]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
⊢ (imageSubobjectIso f).inv ≫ (imageSubobject f).arrow = image.ι f

Tactic:
simp [imageSubobjectIso]

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

Goal state before:
pp: case empty
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
I : Type u_1
B : C
P : I → Subobject B
⊢ ∀ i ∈ ∅, (P i).Factors (∅.inf P).arrow

Tactic:
rintro _ ⟨⟩

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

Goal state before:
pp: case insert.inr
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✝ ∈ s✝
⊢ (P i✝).Factors (s✝.inf P).arrow

Tactic:
exact ih _ m

Goal state after:
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:
rw [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.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
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
Φ : StructuredArrow Y L ⥤ StructuredArrow (E.functor.obj Y) (L ⋙ E.functor) := StructuredArrow.post Y L E.functor
⊢ (L ⋙ E.functor).HasPointwiseRightKanExtensionAt F (E.functor.obj Y)

Tactic:
have : HasLimit ((asEquivalence Φ).functor ⋙
    StructuredArrow.proj (E.functor.obj Y) (L ⋙ E.functor) ⋙ F) :=
    (inferInstance : HasPointwiseRightKanExtensionAt L F Y)

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
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
inst✝ : L.HasPointwiseRightKanExtensionAt F Y
Φ : StructuredArrow Y L ⥤ StructuredArrow (E.functor.obj Y) (L ⋙ E.functor) := StructuredArrow.post Y L E.functor
this : HasLimit (Φ.asEquivalence.functor ⋙ StructuredArrow.proj (E.functor.obj Y) (L ⋙ E.functor) ⋙ F)
⊢ (L ⋙ E.functor).HasPointwiseRightKanExtensionAt F (E.functor.obj Y)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
e : CostructuredArrow.proj L Y ⋙ F' ≅ CostructuredArrow.proj L Y ⋙ F :=
  NatIso.ofComponents (fun X ↦ (e₂.app ((CostructuredArrow.proj L Y).obj X)).symm) ⋯
⊢ HasColimit (CostructuredArrow.proj L Y ⋙ F')

Tactic:
hasColimit_iff_of_iso e

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_4, u_4} H
L L' : C ⥤ D
F F' : C ⥤ H
Y : D
inst✝ : L.HasPointwiseLeftKanExtensionAt F Y
e₁ : L ≅ L'
e₂ : F ≅ F'
e : CostructuredArrow.proj L Y ⋙ F' ≅ CostructuredArrow.proj L Y ⋙ F :=
  NatIso.ofComponents (fun X ↦ (e₂.app ((CostructuredArrow.proj L Y).obj X)).symm) ⋯
⊢ HasColimit (CostructuredArrow.proj L Y ⋙ F)
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
⊢ (StructuredArrow.Hom.right f₁).app Y = (StructuredArrow.Hom.right f₂).app Y

Tactic:
apply (h Y).hom_ext

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.LeftExtension F
h : E.IsPointwiseLeftKanExtension
G : L.LeftExtension F
f₁ f₂ : E ⟶ G
Y : D
⊢ ∀ (j : CostructuredArrow L Y),
    (E.coconeAt Y).ι.app j ≫ (StructuredArrow.Hom.right f₁).app Y =
      (E.coconeAt Y).ι.app j ≫ (StructuredArrow.Hom.right f₂).app Y
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
⊢ f₁.left.app Y = f₂.left.app Y

Tactic:
apply (h Y).hom_ext

Goal state after:
C : Type u_1
D : Type u_2
H : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
F : C ⥤ H
E : L.RightExtension F
h : E.IsPointwiseRightKanExtension
G : L.RightExtension F
f₁ f₂ : G ⟶ E
Y : D
⊢ ∀ (j : StructuredArrow Y L), f₁.left.app Y ≫ (E.coneAt Y).π.app j = f₂.left.app Y ≫ (E.coneAt Y).π.app j
Module: Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
D : Type u_2
inst✝⁴ : Category.{v_2, u_2} D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
J : Type u_4
inst✝² : Category.{v_4, u_4} J
inst✝¹ : HasColimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesColimitsOfShape J F
G : J ⥤ C ⥤ D
j : J
⊢ whiskerRight (colimit.ι G j) F ≫ (colimitCompWhiskeringRightIsoColimitComp F G).inv =
    colimit.ι (G ⋙ (whiskeringRight C D E).obj F) j

Tactic:
by
  simp [Iso.comp_inv_eq]

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
X : StructuredArrow S T
⊢ P X.right ↔ ∃ a, P a ∧ ∃ b, mk b = X

Tactic:
exact ⟨fun h ↦ ⟨_, h, _, rfl⟩, by rintro ⟨_, h, _, rfl⟩; exact h⟩

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 : C ⥤ D
T : D
P : ObjectProperty C
inst✝¹ : ObjectProperty.Small.{v₁, v₁, u₁} P
inst✝ : LocallySmall.{v₁, v₂, u₂} D
X : CostructuredArrow S T
⊢ P X.left ↔ ∃ a, P a ∧ ∃ b, mk b = X

Tactic:
exact ⟨fun h ↦ ⟨_, h, _, rfl⟩, by rintro ⟨_, h, _, rfl⟩; exact h⟩

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)
m : (coconeOfRepresentable P).pt ⟶ s.pt
hm : ∀ (j : P.Elementsᵒᵖ), uliftYonedaEquiv.symm (unop j).snd ≫ m = s.ι.app j
X : Cᵒᵖ
x : (coconeOfRepresentable P).pt.obj X
⊢ (hom (m.app X)) x = uliftYonedaEquiv (uliftYonedaEquiv.symm (unop (op (P.elementsMk X x))).snd ≫ m)

Tactic:
uliftYonedaEquiv_comp,

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)
m : (coconeOfRepresentable P).pt ⟶ s.pt
hm : ∀ (j : P.Elementsᵒᵖ), uliftYonedaEquiv.symm (unop j).snd ≫ m = s.ι.app j
X : Cᵒᵖ
x : (coconeOfRepresentable P).pt.obj X
⊢ (hom (m.app X)) x =
    (hom (m.app (op (unop X)))) (uliftYonedaEquiv (uliftYonedaEquiv.symm (unop (op (P.elementsMk X x))).snd))
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : ObjectProperty C
hP : ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, Epi p
⊢ P.IsSeparating

Tactic:
by
  intro X Y f g h
  obtain ⟨ι, s, hs, c, hc, p, _⟩ := hP X
  rw [← cancel_epi p]
  exact Cofan.IsColimit.hom_ext hc _ _
    (fun i ↦ by simpa using h _ (hs i) (c.inj i ≫ p))

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
X : C
p : uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P
⊢ uliftYonedaEquiv ((p ≫ presheafHom φ P) ≫ F.op.whiskerLeft (G.map f)) =
    (hom ((G.map (p ≫ f)).app (op (F.obj X))))
      ((hom ((φ.app X).app (op (F.obj X)))) { down := 𝟙 (unop (op (F.obj X))) })

Tactic:
uliftYonedaEquiv_comp,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : (Cᵒᵖ ⥤ Type (max w v₁ v₂)) ⥤ Dᵒᵖ ⥤ Type (max w v₁ v₂)
φ : F ⋙ uliftYoneda.{max w v₁, v₂, u₂} ⟶ uliftYoneda.{max w v₂, v₁, u₁} ⋙ G
P Q : Cᵒᵖ ⥤ Type (max w v₁ v₂)
f : P ⟶ Q
X : C
p : uliftYoneda.{max w v₂, v₁, u₁}.obj X ⟶ P
⊢ (hom ((F.op.whiskerLeft (G.map f)).app (op X))) (uliftYonedaEquiv (p ≫ presheafHom φ P)) =
    (hom ((G.map (p ≫ f)).app (op (F.obj X))))
      ((hom ((φ.app X).app (op (F.obj X)))) { down := 𝟙 (unop (op (F.obj X))) })
Module: Mathlib.Algebra.Category.Grp.AB

Goal state before:
pp: J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
⊢ (AddCommGrpCat.Hom.hom (S.map colim).g).ker ≤ (AddCommGrpCat.Hom.hom (S.map colim).f).range

Tactic:
intro x (hx : _ = _)

Goal state after:
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsFiltered J
S : ShortComplex (J ⥤ AddCommGrpCat)
hS :
  ∀ (j : J),
    (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).g).ker ≤
      (AddCommGrpCat.Hom.hom (S.map ((evaluation J AddCommGrpCat).obj j)).f).range
x : ↑(S.map colim).X₂
hx : (AddCommGrpCat.Hom.hom (S.map colim).g) x = 0
⊢ x ∈ (AddCommGrpCat.Hom.hom (S.map colim).f).range
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
⊢ StructuredArrow.hom (Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom) ≫
      ((Functor.whiskeringLeft C (Cᵒᵖ ⥤ Type (max (max w v₁) v₂)) (Dᵒᵖ ⥤ Type (max (max w v₁) v₂))).obj
            uliftYoneda.{max w v₂, v₁, u₁}).map
        (natTrans (StructuredArrow.hom Φ)) =
    StructuredArrow.hom Φ

Tactic:
ext X : 2

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
ℰ : Type u₂
inst✝³ : Category.{v₂, u₂} ℰ
A✝ A : C ⥤ ℰ
inst✝² : uliftYoneda.{max w v₂, v₁, u₁}.HasPointwiseLeftKanExtension A
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : ∀ (P : Cᵒᵖ ⥤ Type (max w v₁ v₂)), F.op.HasLeftKanExtension P
Φ : uliftYoneda.{max w v₂, v₁, u₁}.LeftExtension (F ⋙ uliftYoneda.{max w v₁, v₂, u₂})
X : C
⊢ (StructuredArrow.hom (Functor.LeftExtension.mk F.op.lan (compULiftYonedaIsoULiftYonedaCompLan F).hom) ≫
          ((Functor.whiskeringLeft C (Cᵒᵖ ⥤ Type (max (max w v₁) v₂)) (Dᵒᵖ ⥤ Type (max (max w v₁) v₂))).obj
                uliftYoneda.{max w v₂, v₁, u₁}).map
            (natTrans (StructuredArrow.hom Φ))).app
      X =
    (StructuredArrow.hom Φ).app X
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))
this : Epi (iX.hom ≫ (iX.inv ≫ lim.map f ≫ iY.hom) ≫ iY.inv)
⊢ Epi (lim.map f)

Tactic:
simpa using this

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coproducts

Goal state before:
pp: C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
⊢ Function.Bijective (fromSigma F c)

Tactic:
← isColimit_iff_bijective_fromSigma

Goal state after:
C : Type u
F : C → Type v
c : CofanTypes F
hc : Functor.CoconeTypes.IsColimit c
⊢ Functor.CoconeTypes.IsColimit c
Module: Mathlib.Algebra.Category.Grp.CartesianMonoidal

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

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

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

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

pp: case snd
G H : CommGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget CommGrpCat) G H)) (p, q)).2 = (p, q).2

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

Goal state after:
case snd
G H : CommGrpCat
p : ↑G
q : ↑H
⊢ ((hom (Functor.LaxMonoidal.μ (forget CommGrpCat) G H)) (p, q)).2 = (p, q).2
Module: Mathlib.CategoryTheory.Limits.Presheaf

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
u : (shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).Elements
m : ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X (shrinkYonedaObjObjEquiv.symm (𝟙 X))).fst ⟶ u.fst
hm :
  (ConcreteCategory.hom ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).map m))
      ((shrinkYoneda.{w, v₁, u₁}.flip.obj (op X)).elementsMk X (shrinkYonedaObjObjEquiv.symm (𝟙 X))).snd =
    u.snd
⊢ ↑⟨m, hm⟩ = ↑⟨shrinkYonedaObjObjEquiv u.snd, ⋯⟩

Tactic:
simp [← hm, shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm.{w}]

Goal state after: