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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
W X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : Epi g
R : C
e : X ⟶ R
h : pullback.fst f g ≫ e = 0
u : X ⊞ Y ⟶ R := biprod.desc e 0
hu : PullbackToBiproductIsKernel.pullbackToBiproduct f g ≫ u = 0
this : IsColimit (CokernelCofork.ofπ (biprod.desc f (-g)) ⋯)
d : Z ⟶ R
hd : biprod.desc f (-g) ≫ d = biprod.desc e 0
⊢ (biprod.inr ≫ biprod.desc f (-g)) ≫ d = biprod.inr ≫ u

Tactic:
by rw [Category.assoc, hd]

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

Goal state before:
pp: case pos
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ (Hom.hom f).range
⊢ (h ((ConcreteCategory.hom f) a)) (fromCoset ⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩) =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩

Tactic:
rw [h_apply_fromCoset' _ _ _ m, fromCoset_eq_of_mem_range _ m]

Goal state after:
case pos
A B : GrpCat
f : A ⟶ B
a : ↑A
y : ↑B
m : y ∈ (Hom.hom f).range
⊢ fromCoset ⟨↑(Hom.hom f).range, ⋯⟩ =
    fromCoset ⟨(ConcreteCategory.hom f) a • ↑⟨(fun x ↦ x • ↑(Hom.hom f).range) y, ⋯⟩, ⋯⟩
Module: Mathlib.Algebra.Category.Grp.EpiMono

Goal state before:
pp: A B : AddGrpCat
f : A ⟶ B
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)

Tactic:
have i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f) := by
    refine ⟨?_, groupAddGroupEquivalence.inverse.epi_of_epi_map⟩
    apply groupAddGroupEquivalence.inverse.map_epi

Goal state after:
A B : AddGrpCat
f : A ⟶ B
i1 : Epi f ↔ Epi (groupAddGroupEquivalence.inverse.map f)
⊢ Epi f ↔ Function.Surjective ⇑(ConcreteCategory.hom f)
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
inst✝² : Epi φ.τ₁
inst✝¹ : IsIso φ.τ₂
inst✝ : Mono φ.τ₃
⊢ (ofEpiOfIsIsoOfMono' φ h).p = φ.τ₂ ≫ h.p

Tactic:
simp [ofEpiOfIsIsoOfMono', opMap]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
hf : S.f = 0
inst✝ : S.HasHomology
⊢ IsIso S.homologyπ

Tactic:
by
  have := S.isIso_leftHomologyπ hf
  dsimp only [homologyπ]
  infer_instance

Goal state after:
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), (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) = (π₂.mapCocone s).ι.app j
⊢ (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) ≫ s.pt.g =
    (π₂.mapCocone c).ι.app j ≫ c.pt.g ≫ h₃.desc (π₃.mapCocone s)

Tactic:
have eq₃ := h₃.fac (π₃.mapCocone s)

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), (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) = (π₂.mapCocone s).ι.app j
eq₃ : ∀ (j : J), (π₃.mapCocone c).ι.app j ≫ h₃.desc (π₃.mapCocone s) = (π₃.mapCocone s).ι.app j
⊢ (π₂.mapCocone c).ι.app j ≫ h₂.desc (π₂.mapCocone s) ≫ s.pt.g =
    (π₂.mapCocone c).ι.app j ≫ c.pt.g ≫ h₃.desc (π₃.mapCocone s)
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₁.g ≫ (-h.h₂) + (-h.h₁) ≫ S₂.f + (-φ₂).τ₂

Tactic:
rw [neg_τ₂, neg_τ₂, h.comm₂, neg_add_rev, comp_neg, neg_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' : Homotopy φ₃ φ₄
⊢ (φ₁ - φ₃).τ₃ = h.h₃ - h'.h₃ + (h.h₂ - h'.h₂) ≫ S₂.g + (φ₂ - φ₄).τ₃

Tactic:
by rw [sub_τ₃, sub_τ₃, h.comm₃, h'.comm₃, sub_comp]; abel

Goal state after:
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 φ₁ φ₂
⊢ φ₁.τ₁ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₁

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 φ₁ φ₂
⊢ φ₁.τ₂ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₂

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 φ₁ φ₂
⊢ φ₁.τ₃ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₃

Tactic:
· dsimp; rw [h.comm₁]; abel

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₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₂

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₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₃
Module: Mathlib.Algebra.Homology.ShortComplex.Ab

Goal state before:
pp: S : ShortComplex Ab
x : ↥(AddCommGrpCat.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom S.iCycles) ((ConcreteCategory.hom S.abLeftHomologyData.cyclesIso.inv) x) = ↑x

Tactic:
rw [← ConcreteCategory.comp_apply, S.abLeftHomologyData.cyclesIso_inv_comp_iCycles]

Goal state after:
S : ShortComplex Ab
x : ↥(AddCommGrpCat.Hom.hom S.g).ker
⊢ (ConcreteCategory.hom S.abLeftHomologyData.i) x = ↑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
S : ShortComplex C
inst✝¹ : S.HasHomology
inst✝ : HasCokernel S.f
⊢ S.Exact ↔ Mono (cokernel.desc S.f S.g ⋯)

Tactic:
rw [exact_iff_mono_fromOpcycles]

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

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

Tactic:
rw [exact_iff_mono_fromOpcycles]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
s : S.Splitting
⊢ S.g ≫ s.s = 𝟙 S.X₂ - s.r ≫ S.f

Tactic:
rw [← s.id, add_sub_cancel_left]

Goal state after:
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 ≫ e.hom.τ₂ ≫ S₂.g = 𝟙 S₂.X₃

Tactic:
e.hom.comm₂₃,

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.τ₃ ≫ s.s ≫ S₁.g ≫ e.hom.τ₃ = 𝟙 S₂.X₃
Module: Mathlib.CategoryTheory.Subobject.MonoOver

Goal state before:
pp: case of
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type u₃
inst✝ : Category.{v₃, u₃} J
X : C
F : Over X
x✝ : (Over.isMono X).limitsOfShape J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z✝ : C
g h : Z✝ ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : J
this : Over.isMono X (p.diag.obj j)
⊢ g ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j) =
    h ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)

Tactic:
← cancel_mono ((p.diag.obj j).hom)

Goal state after:
case of
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
J : Type u₃
inst✝ : Category.{v₃, u₃} J
X : C
F : Over X
x✝ : (Over.isMono X).limitsOfShape J F
p : LimitPresentation J F
hp : ∀ (j : J), Over.isMono X (p.diag.obj j)
Z✝ : C
g h : Z✝ ⟶ F.left
e : g ≫ F.hom = h ≫ F.hom
j : J
this : Over.isMono X (p.diag.obj j)
⊢ (g ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)) ≫ (p.diag.obj j).hom =
    (h ≫ (WithTerminal.coneEquiv.functor.obj { pt := F, π := p.π }).π.app (WithTerminal.of j)) ≫ (p.diag.obj j).hom
Module: Mathlib.CategoryTheory.Abelian.Exact

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
⊢ S.Exact ↔ imageSubobject S.f = kernelSubobject S.g

Tactic:
exact_iff_isIso_imageToKernel

Goal state after:
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
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y : C
⊢ IsIso ⊤.arrow

Tactic:
by rw [isIso_arrow_iff_eq_top]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Abelian C
inst✝¹ : Abelian D
F : C ⥤ D
inst✝ : F.Additive
tfae_1_to_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
hF : ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
X Y : C
f : X ⟶ Y
⊢ PreservesLimit (parallelPair f 0) F

Tactic:
refine preservesLimit_of_preserves_limit_cone (kernelIsKernel 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_2 :
  (∀ (S : ShortComplex C), S.ShortExact → (S.map F).Exact ∧ Mono (F.map S.f)) →
    ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
hF : ∀ (S : ShortComplex C), S.Exact ∧ Mono S.f → (S.map F).Exact ∧ Mono (F.map S.f)
X Y : C
f : X ⟶ Y
⊢ IsLimit (F.mapCone (Fork.ofι (kernel.ι f) ⋯))
Module: Mathlib.CategoryTheory.Subobject.Lattice

Goal state before:
pp: case refine_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasPullbacks C
A : C
f g : Subobject A
s : PullbackCone f.arrow g.arrow
⊢ ((f ⊓ g).factorThru (s.fst ≫ f.arrow) ⋯ ≫ (f ⊓ g).ofLE g ⋯) ≫ g.arrow = s.snd ≫ g.arrow

Tactic:
simp [s.condition]

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

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Abelian C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : F.Faithful
S : ShortComplex C
hS : kernel.ι (F.map S.g) ≫ cokernel.π (F.map S.f) = 0
k : F.obj (Limits.kernel S.g) ⟶ Limits.kernel (F.map S.g)
hk : k ≫ kernel.ι (F.map S.g) = F.map (kernel.ι S.g)
⊢ F.map S.f ≫ F.map (cokernel.π S.f) = 0

Tactic:
by simp only [← F.map_comp, cokernel.condition, CategoryTheory.Functor.map_zero]

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

Goal state before:
pp: case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : LocallySmall.{w, v₁, u₁} C
inst✝¹ : WellPowered.{w, v₁, u₁} C
inst✝ : HasWidePullbacks C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ ((underlyingIso (widePullbackι s)).hom ≫
        limit.π (wideCospan s) (some ⟨(equivShrink (Subobject A)) f, ⋯⟩) ≫ eqToHom ⋯) ≫
      f.arrow =
    (sInf s).arrow

Tactic:
dsimp [sInf]
    simp only [Category.assoc, ← underlyingIso_hom_comp_eq_mk,
      Iso.cancel_iso_hom_left]
    convert! limit.w (wideCospan s) (WidePullbackShape.Hom.term _)
    simp

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

Goal state before:
pp: case f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj f ⟶ underlying.obj (sSup s)

Tactic:
refine eqToHom ?_ ≫ Sigma.ι _ ⟨equivShrink (Subobject A) f, by simpa [Set.mem_image] using hf⟩
      ≫ factorThruImage _ ≫ (underlyingIso _).inv

Goal state after:
case f
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasCoproducts C
inst✝ : HasImages C
A : C
s : Set (Subobject A)
f : Subobject A
hf : f ∈ s
⊢ underlying.obj f = underlying.obj ((equivShrink (Subobject A)).symm ↑⟨(equivShrink (Subobject A)) 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:
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:
simp [CostructuredArrow.toOverCompYoneda]

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

Goal state before:
pp: C : Type u_1
C' : Type u_2
H : Type u_3
D : Type u_4
D' : Type u_5
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
inst✝ : Category.{v_5, u_5} D'
L : C ⥤ D
L' : D ⥤ D'
F₀ : C ⥤ H
F₁ : D ⥤ H
F₂ : D' ⥤ H
α : F₀ ⟶ L ⋙ F₁
hα : StructuredArrow.IsUniversal (mk F₁ α)
b : L'.LeftExtension F₁
hb : StructuredArrow.IsUniversal b
⊢ StructuredArrow.IsUniversal ((precomp₂ L' α).obj b)

Tactic:
by
  letI (y : (L ⋙ L').LeftExtension F₀) :
      Unique ((precomp₂ L' α).obj b ⟶ y) := by
    let u : L'.LeftExtension F₁ :=
      mk y.right <|
        hα.desc <| LeftExtension.mk _ <|
          y.hom ≫ (L.associator L' y.right).hom
    refine
      ⟨⟨StructuredArrow.homMk (hb.desc u) <| by
          ext x
          have hb_fac_app := congr_app (hb.fac u) (L.obj x)
          have hα_fac_app :=
            congr_app (hα.fac <| LeftExtension.mk _ <|
              y.hom ≫ (L.associator L' y.right).hom) x
          dsimp at hα_fac_app hb_fac_app
          simp [hb_fac_app, u, hα_fac_app]⟩, fun a => ?_⟩
    dsimp
    ext1
    apply hb.hom_ext
    apply hα.hom_ext
    ext t
    dsimp
    have a_w_t := congr_app a.w t
    have hb_fac_app := congr_app (hb.fac u) (L.obj t)
    have hα_fac_app :=
      congr_app
        (hα.fac <| LeftExtension.mk _ <|
          y.hom ≫ (L.associator L' y.right).hom) t
    dsimp at hb_fac_app hα_fac_app
    simp only [whiskeringLeft_obj_obj, comp_obj,
      precomp₂_obj_right, whiskeringLeft_obj_map, NatTrans.comp_app,
      precomp₂_obj_hom_app, whiskerLeft_app, assoc] at a_w_t
    simp [← a_w_t, hb_fac_app, u, hα_fac_app]
  apply IsInitial.ofUnique

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
⊢ Abelian C

Tactic:
haveI := hasCokernels F G i adj

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
⊢ Abelian C
Module: Mathlib.CategoryTheory.Limits.Constructions.WeaklyInitial

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
⊢ a = default

Tactic:
have : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 _ := by
      rw [Category.assoc, Category.assoc]
      apply wideEqualizer.condition (id : endos → endos) (h ≫ e ≫ i)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasWideEqualizers C
T : C
hT : ∀ (X : C), Nonempty (T ⟶ X)
endos : Type v := T ⟶ T
i : wideEqualizer id ⟶ T := wideEqualizer.ι id
this✝ : Nonempty endos
X : C
a : wideEqualizer id ⟶ X
E : C := equalizer a (i ≫ Classical.choice ⋯)
e : E ⟶ wideEqualizer id := equalizer.ι a (i ≫ Classical.choice ⋯)
h : T ⟶ E := Classical.choice ⋯
this : ((i ≫ h) ≫ e) ≫ i = i ≫ 𝟙 T
⊢ a = default
Module: Mathlib.CategoryTheory.Subobject.Comma

Goal state before:
pp: case w
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
S : D
T : C ⥤ D
inst✝¹ : HasFiniteLimits C
inst✝ : PreservesFiniteLimits T
A P : StructuredArrow S T
f : P ⟶ A
hf : Mono f
q : S ⟶ T.obj (Subobject.underlying.obj (projectSubobject (Subobject.mk f)))
hq : q ≫ T.map (projectSubobject (Subobject.mk f)).arrow = A.hom
⊢ autoParam ((mk q).hom ≫ T.map (Subobject.underlyingIso (Hom.right (MonoOver.mk f).arrow)).hom = P.hom) isoMk._auto_1

Tactic:
exact (cancel_mono (T.map f.right)).1 (by dsimp; simpa [← T.map_comp] using hq)

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

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝³ : HasFiniteLimits C
this✝² : HasProductsOfShape (Subtype P) C
this✝¹ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this✝ : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
this : ∀ (X : C) [inst : HasProduct (P.productToFamily X)], Mono (P.productTo X)
⊢ (A : C) → Unique (Subobject.underlying.obj ⊥ ⟶ A)

Tactic:
refine fun A => ⟨⟨?_⟩, fun f => ?_⟩

Goal state after:
case refine_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝³ : HasFiniteLimits C
this✝² : HasProductsOfShape (Subtype P) C
this✝¹ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this✝ : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
this : ∀ (X : C) [inst : HasProduct (P.productToFamily X)], Mono (P.productTo X)
A : C
⊢ Subobject.underlying.obj ⊥ ⟶ A

case refine_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : LocallySmall.{w, v₁, u₁} C
inst✝² : WellPowered.{w, v₁, u₁} C
inst✝¹ : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this✝³ : HasFiniteLimits C
this✝² : HasProductsOfShape (Subtype P) C
this✝¹ : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this✝ : CompleteLattice (Subobject (∏ᶜ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ᶜ Subtype.val))
this : ∀ (X : C) [inst : HasProduct (P.productToFamily X)], Mono (P.productTo X)
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
⊢ f = default
Module: Mathlib.CategoryTheory.Generator.Basic

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
G : C
⊢ IsSeparator (op G) ↔ IsCoseparator G

Tactic:
by
  rw [IsSeparator, IsCoseparator, ← isSeparating_op_iff, op_singleton]

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
⊢ Epi (lim.map f)

Tactic:
let iX : limit X ≅ AddCommGrpCat.of ((i : J) → X.obj ⟨i⟩) := (Pi.isoLimit X).symm ≪≫
        (limit.isLimit _).conePointUniqueUpToIso (AddCommGrpCat.HasLimit.productLimitCone _).isLimit

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
⊢ Epi (lim.map f)
Module: Mathlib.Algebra.Category.Grp.Adjunctions

Goal state before:
pp: ⊢ ∀ {X' X : Type u} {Y : AddCommGrpCat} (f : X' ⟶ X) (g : X ⟶ (forget AddCommGrpCat).obj Y),
    (ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm (f ≫ g) =
      free.map f ≫ (ConcreteCategory.homEquiv.trans (FreeAbelianGroup.lift.symm.trans TypeCat.homEquiv.symm)).symm g

Tactic:
intros
        ext
        dsimp [ConcreteCategory.homEquiv]
        rw [← FreeAbelianGroup.lift_comp]
        rfl

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

Goal state before:
pp: case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : LocallySmall.{w, v₁, u₁} C
F : C ⥤ Type w
X : C
x :
  (((CategoryOfElements.π F).op ⋙ shrinkYoneda.{w, v₁, u₁}.obj X).coconeTypesEquiv.symm
      (coconeπOpCompShrinkYonedaObj F X)).pt
⊢ ∃ a,
    ((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))
        a =
      x

Tactic:
· exact ⟨Functor.ιColimitType _ (op (elementsMk _ _ x))
      (shrinkYonedaObjObjEquiv.symm (𝟙 X)), by simp⟩

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

Goal state before:
pp: X'✝ X✝ : GrpCat
Y✝ : CommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGrpCat GrpCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ (CommGrpCat.Hom.hom
        (abelianize.map f✝ ≫
          ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g✝))
      x✝ =
    (CommGrpCat.Hom.hom
        (((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm
          (f✝ ≫ g✝)))
      x✝

Tactic:
apply Abelianization.lift_unique

Goal state after:
X'✝ X✝ : GrpCat
Y✝ : CommGrpCat
f✝ : X'✝ ⟶ X✝
g✝ : X✝ ⟶ (forget₂ CommGrpCat GrpCat).obj Y✝
x✝ : ↑(abelianize.obj X'✝)
⊢ ∀ (x : ↑X'✝),
    (CommGrpCat.Hom.hom
          (abelianize.map f✝ ≫
            ((ConcreteCategory.homEquiv.trans Abelianization.lift.symm).trans ConcreteCategory.homEquiv.symm).symm g✝))
        (Abelianization.of x) =
      (ConcreteCategory.homEquiv.symm.symm (f✝ ≫ g✝)) x
Module: Mathlib.Algebra.Ring.NegOnePow

Goal state before:
pp: n : ℤ
⊢ |n|.negOnePow = n.negOnePow

Tactic:
obtain h | h := abs_choice n

Goal state after:
case inl
n : ℤ
h : |n| = n
⊢ |n|.negOnePow = n.negOnePow

case inr
n : ℤ
h : |n| = -n
⊢ |n|.negOnePow = n.negOnePow
Module: Mathlib.Algebra.Order.Interval.Set.Group

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : PartialOrder α
inst✝ : IsOrderedAddMonoid α
a b : α
⊢ b - a ∈ Ico 0 b ↔ a ∈ Ioc 0 b

Tactic:
simp only [sub_mem_Ico_iff_right, sub_self, sub_zero]

Goal state after: