mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a : R
g : (functor r).obj X ⟶ (functor r).obj Y
f : X ⟶ Y
⊢ a • ((functor r).map f + g) = a • (functor r).map f + a • g

Tactic:
obtain ⟨g, rfl⟩ := (functor r).map_surjective g

Goal state after:
R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a : R
f g : X ⟶ Y
⊢ a • ((functor r).map f + (functor r).map g) = a • (functor r).map f + a • (functor r).map g
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
g : { as := Y } ⟶ { as := Z }
f : X ⟶ Y
⊢ (a • (functor r).map f) ≫ g = a • (functor r).map f ≫ g

Tactic:
obtain ⟨g, rfl⟩ := (functor r).map_surjective g

Goal state after:
R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (a • (functor r).map f) ≫ (functor r).map g = a • (functor r).map f ≫ (functor r).map g
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
g : { as := Y } ⟶ { as := Z }
f : X ⟶ Y
⊢ (functor r).map f ≫ (a • g) = a • (functor r).map f ≫ g

Tactic:
obtain ⟨g, rfl⟩ := (functor r).map_surjective g

Goal state after:
R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
X Y Z : C
a : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (functor r).map f ≫ (a • (functor r).map g) = a • (functor r).map f ≫ (functor r).map g
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: case mk.mk.mk
C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
P✝ Q✝ R✝ : Quotient r
f✝ : P✝ ⟶ Q✝
a✝² : P✝.as ⟶ Q✝.as
g✝ : Q✝ ⟶ R✝
a✝¹ : Q✝.as ⟶ R✝.as
g'✝ : Q✝ ⟶ R✝
a✝ : Q✝.as ⟶ R✝.as
⊢ Quot.mk (HomRel.CompClosure r) a✝² ≫ (Quot.mk (HomRel.CompClosure r) a✝¹ + Quot.mk (HomRel.CompClosure r) a✝) =
    Quot.mk (HomRel.CompClosure r) a✝² ≫ Quot.mk (HomRel.CompClosure r) a✝¹ +
      Quot.mk (HomRel.CompClosure r) a✝² ≫ Quot.mk (HomRel.CompClosure r) a✝

Tactic:
exact congr_arg (functor r).map (by apply Preadditive.comp_add)

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
Y Z : C
g : Y ⟶ Z
⊢ ∃ X f h, Triangle.mk f g h ∈ distinguishedTriangles

Tactic:
obtain ⟨X', f', g', mem⟩ := distinguished_cocone_triangle g
  exact ⟨_, _, _, inv_rot_of_distTriang _ mem⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
this : Mono φ.hom₂
A : C
f₁ f₂ : A ⟶ T.obj₂
h : (fun x ↦ x ≫ φ.hom₂) f₁ = (fun x ↦ x ≫ φ.hom₂) f₂
⊢ f₁ = f₂

Tactic:
simpa only [← cancel_mono φ.hom₂] using h

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X₁ X₃ X₂ : C
inl : X₁ ⟶ X₂
snd : X₂ ⟶ X₃
mem : Triangle.mk inl snd 0 ∈ distinguishedTriangles
inr : X₃ ⟶ X₂
inr_snd : 𝟙 X₃ = inr ≫ snd
⊢ (𝟙 X₂ - snd ≫ inr) ≫ (Triangle.mk inl snd 0).mor₂ = 0

Tactic:
dsimp
      simp only [sub_comp, assoc, id_comp, ← inr_snd, comp_id, sub_self]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ lift (inr φ) (-(Cocycle.ofHom φ).leftShift 1 1 ⋯) (-(inl φ).leftShift 1 0 ⋯) ⋯ ≫ desc (inr φ) 0 (triangle φ).mor₃ ⋯ =
    𝟙 ((CategoryTheory.shiftFunctor (HomologicalComplex C (ComplexShape.up ℤ)) 1).obj K)

Tactic:
ext n
    -- the following list of lemmas has been obtained by doing
    -- simp? [lift_desc_f _ _ _ _ _ _ _ _ _ rfl,
    --   (inl φ).leftShift_v 1 0 _ _ n _ (n + 1) (by simp only [add_neg_cancel_right])]
    simp only [shiftFunctor_obj_X', Int.reduceNeg, HomologicalComplex.comp_f,
      lift_desc_f _ _ _ _ _ _ _ _ _ rfl, Cocycle.coe_neg, Cocycle.leftShift_coe,
      Cocycle.ofHom_coe, Cochain.neg_v, Cochain.zero_v,
      comp_zero, (inl φ).leftShift_v 1 0 _ _ n _ (n + 1) (by simp only [add_neg_cancel_right]),
      shiftFunctor_obj_X, mul_zero, sub_self, Int.zero_ediv, add_zero, Int.negOnePow_zero,
      shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl, Iso.refl_hom, id_comp, one_smul,
      Preadditive.neg_comp, inl_v_triangle_mor₃_f, Iso.refl_inv, neg_neg, zero_add,
      HomologicalComplex.id_f]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles C
⊢ T.rotate ∈ distinguishedTriangles C

Tactic:
obtain ⟨K, L, φ, ⟨e⟩⟩ := hT
  exact ⟨_, _, _, ⟨(rotate _).mapIso e ≪≫ CochainComplex.mappingCone.rotateTrianglehIso φ⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} D
inst✝¹¹ : Category.{v_3, u_3} E
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : HasShift D ℤ
inst✝⁸ : HasShift E ℤ
F : C ⥤ D
inst✝⁷ : F.CommShift ℤ
G : D ⥤ E
inst✝⁶ : G.CommShift ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : Preadditive D
inst✝³ : F.Additive
F₁ F₂ : C ⥤ D
e : F₁ ≅ F₂
inst✝² : F₁.CommShift ℤ
inst✝¹ : F₂.CommShift ℤ
inst✝ : NatTrans.CommShift e.hom ℤ
T : Triangle C
⊢ (F₁.mapTriangle.obj T).mor₃ ≫ (shiftFunctor D 1).map (e.app T.obj₁).hom =
    (e.app T.obj₃).hom ≫ (F₂.mapTriangle.obj T).mor₃

Tactic:
by
      dsimp
      simp only [assoc, NatTrans.shift_app_comm e.hom (1 : ℤ) T.obj₁,
        NatTrans.naturality_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Functor

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝²⁴ : Category.{v_1, u_1} C
inst✝²³ : Category.{v_2, u_2} D
inst✝²² : Category.{v_3, u_3} E
inst✝²¹ : HasShift C ℤ
inst✝²⁰ : HasShift D ℤ
inst✝¹⁹ : HasShift E ℤ
inst✝¹⁸ : HasZeroObject C
inst✝¹⁷ : HasZeroObject D
inst✝¹⁶ : HasZeroObject E
inst✝¹⁵ : Preadditive C
inst✝¹⁴ : Preadditive D
inst✝¹³ : Preadditive E
inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝⁹ : Pretriangulated C
inst✝⁸ : Pretriangulated D
inst✝⁷ : Pretriangulated E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁶ : F.CommShift ℤ
inst✝⁵ : G.CommShift ℤ
inst✝⁴ : H.CommShift ℤ
inst✝³ : NatTrans.CommShift e.hom ℤ
inst✝² : G.IsTriangulated
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ F.IsTriangulated ↔ H.IsTriangulated

Tactic:
rw [← isTriangulated_iff_of_iso e]

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝²⁴ : Category.{v_1, u_1} C
inst✝²³ : Category.{v_2, u_2} D
inst✝²² : Category.{v_3, u_3} E
inst✝²¹ : HasShift C ℤ
inst✝²⁰ : HasShift D ℤ
inst✝¹⁹ : HasShift E ℤ
inst✝¹⁸ : HasZeroObject C
inst✝¹⁷ : HasZeroObject D
inst✝¹⁶ : HasZeroObject E
inst✝¹⁵ : Preadditive C
inst✝¹⁴ : Preadditive D
inst✝¹³ : Preadditive E
inst✝¹² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝⁹ : Pretriangulated C
inst✝⁸ : Pretriangulated D
inst✝⁷ : Pretriangulated E
F : C ⥤ D
G : D ⥤ E
H : C ⥤ E
e : F ⋙ G ≅ H
inst✝⁶ : F.CommShift ℤ
inst✝⁵ : G.CommShift ℤ
inst✝⁴ : H.CommShift ℤ
inst✝³ : NatTrans.CommShift e.hom ℤ
inst✝² : G.IsTriangulated
inst✝¹ : G.Full
inst✝ : G.Faithful
⊢ F.IsTriangulated ↔ (F ⋙ G).IsTriangulated
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} A
F : C ⥤ A
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
X Y Z : C
n : M
f : X ⟶ (shiftFunctor C n).obj Y
g : Y ⟶ Z
a a' : M
ha' : n + a = a'
⊢ F.shiftMap (f ≫ (shiftFunctor C n).map g) a a' ha' = F.shiftMap f a a' ha' ≫ (F.shift a').map g

Tactic:
simp [shiftMap]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_3, u_3} A
F : C ⥤ A
M : Type u_4
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
X Y Z : C
n : M
f : X ⟶ Y
g : Y ⟶ (shiftFunctor C n).obj Z
a a' : M
ha' : n + a = a'
⊢ F.shiftMap (f ≫ g) a a' ha' = (F.shift a).map f ≫ F.shiftMap g a a' ha'

Tactic:
simp [shiftMap]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_3, u_3} A
F : C ⥤ A
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : F.ShiftSequence M
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms A
inst✝¹ : F.PreservesZeroMorphisms
inst✝ : ∀ (n : M), (shiftFunctor C n).PreservesZeroMorphisms
X Y : C
n a a' : M
ha' : n + a = a'
⊢ F.shiftMap 0 a a' ha' = 0

Tactic:
simp [shiftMap]

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
⊢ { X₁ := S.X₁.homology i, X₂ := S.X₂.homology i, X₃ := S.X₃.homology i, f := HomologicalComplex.homologyMap S.f i,
      g := HomologicalComplex.homologyMap S.g i, zero := ⋯ }.Exact

Tactic:
by
  by_cases h : c.Rel i (c.next i)
  · exact (snakeInput hS i _ h).L₀_exact
  · have := hS.epi_g
    have : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i) :=
      fun K => ShortComplex.isIso_homologyι (K.sc i) (K.shape _ _ h)
    have e : S.map (HomologicalComplex.homologyFunctor C c i) ≅
        S.map (HomologicalComplex.opcyclesFunctor C c i) :=
      ShortComplex.isoMk (asIso (S.X₁.homologyι i))
        (asIso (S.X₂.homologyι i)) (asIso (S.X₃.homologyι i)) (by simp) (by simp)
    exact ShortComplex.exact_of_iso e.symm (opcycles_right_exact S hS.exact i)

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
F₁ F₂ : D ⥤ E
τ τ' : F₁ ⟶ F₂
h : ∀ (X : C), τ.app (L.obj X) = τ'.app (L.obj X)
⊢ τ = τ'

Tactic:
by
  have := essSurj L W
  ext Y
  rw [← cancel_epi (F₁.map (L.objObjPreimageIso Y).hom), τ.naturality, τ'.naturality, h]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.Predicate

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
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
⊢ L₂.IsLocalization W

Tactic:
have h := Localization.inverts L₁ W
  rw [MorphismProperty.IsInvertedBy.iff_of_iso W e] at h
  let F₁ := Localization.Construction.lift L₁ (Localization.inverts L₁ W)
  let F₂ := Localization.Construction.lift L₂ h
  exact
    { inverts := h
      isEquivalence := Functor.isEquivalence_of_iso (liftNatIso W.Q W L₁ L₂ F₁ F₂ e) }

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction₂ X Y
Z : C
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
w✝ : z₁.f ≫ t₁ = z₂.f ≫ t₂
hft' : z₁.f' ≫ t₁ = z₂.f' ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ LeftFractionRel z₁.snd z₂.snd

Tactic:
exact ⟨Z, t₁, t₂, hst, hft', ht⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : L.obj X ⟶ L.obj Y
g₁ g₂ : L.obj Y ⟶ L.obj Z
α : W.LeftFraction X Y
hα : f = α.map L ⋯
β : W.LeftFraction₂ Y Z
hβ₁ : g₁ = β.fst.map L ⋯
hβ₂ : g₂ = β.snd.map L ⋯
γ : W.LeftFraction₂ α.Y' β.Y'
hγ₁ : β.f ≫ γ.s = α.s ≫ γ.f
hγ₂ : β.f' ≫ γ.s = α.s ≫ γ.f'
⊢ f ≫ g₁ = { Y' := γ.Y', f := α.f ≫ γ.f, f' := α.f ≫ γ.f', s := β.s ≫ γ.s, hs := ⋯ }.fst.map L ⋯

Tactic:
simpa only [hα, hβ₁] using! LeftFraction.map_comp_map_eq_map α β.fst γ.fst hγ₁ L

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.ContainsZero
inst✝ : P.IsClosedUnderIsomorphisms
X : C
p : P.ColimitOfShape (Discrete PEmpty.{1}) X
Z : C
hZ : IsZero Z
hZ₂ : P Z
hX : IsInitial X
⊢ P X

Tactic:
exact P.prop_of_isZero (IsZero.of_iso hZ
      (IsColimit.coconePointUniqueUpToIso hX (IsZero.isInitial hZ)))

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ F₂.map ((Q W).map f.s) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = F₂.map ((Q W).map f.s) ≫ F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯

Tactic:
← F₂.map_comp_assoc,

Goal state after:
case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ F₂.map ((Q W).map f.s) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = F₂.map ((Q W).map f.s ≫ Qinv f.s ⋯) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝¹⁷ : Category.{v_1, u_1} C
inst✝¹⁶ : HasShift C ℤ
inst✝¹⁵ : Category.{v_2, u_2} D
inst✝¹⁴ : HasZeroObject D
inst✝¹³ : HasShift D ℤ
inst✝¹² : Preadditive D
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁰ : Pretriangulated D
inst✝⁹ : Category.{v_3, u_3} A
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Abelian A
L : C ⥤ D
inst✝³ : L.CommShift ℤ
inst✝² : L.IsTriangulated
inst✝¹ : L.mapArrow.EssSurj
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
inst✝ : G.IsHomological
⊢ F.IsHomological

Tactic:
have : F.PreservesZeroMorphisms := preservesZeroMorphisms_of_map_zero_object
    (F.mapIso L.mapZeroObject.symm ≪≫ e.app _ ≪≫ G.mapZeroObject)

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝¹⁷ : Category.{v_1, u_1} C
inst✝¹⁶ : HasShift C ℤ
inst✝¹⁵ : Category.{v_2, u_2} D
inst✝¹⁴ : HasZeroObject D
inst✝¹³ : HasShift D ℤ
inst✝¹² : Preadditive D
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹⁰ : Pretriangulated D
inst✝⁹ : Category.{v_3, u_3} A
inst✝⁸ : HasZeroObject C
inst✝⁷ : Preadditive C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Abelian A
L : C ⥤ D
inst✝³ : L.CommShift ℤ
inst✝² : L.IsTriangulated
inst✝¹ : L.mapArrow.EssSurj
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
inst✝ : G.IsHomological
this : F.PreservesZeroMorphisms
⊢ F.IsHomological
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
W : MorphismProperty C
inst✝ : L.IsLocalization W
h : W.HasLeftCalculusOfFractions
X Y : Cᵒᵖ
φ : W.op.LeftFraction X Y
ψ : W.LeftFraction (Opposite.unop Y) (Opposite.unop X)
eq : φ.unop.f ≫ ψ.s = φ.unop.s ≫ ψ.f
⊢ ∃ ψ, ψ.s ≫ φ.f = ψ.f ≫ φ.s

Tactic:
exact ⟨ψ.op, Quiver.Hom.unop_inj eq⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
W : MorphismProperty C
inst✝ : L.IsLocalization W
h : W.HasRightCalculusOfFractions
X Y : Cᵒᵖ
φ : W.op.RightFraction X Y
ψ : W.RightFraction (Opposite.unop Y) (Opposite.unop X)
eq : ψ.s ≫ φ.unop.f = ψ.f ≫ φ.unop.s
⊢ ∃ ψ, φ.f ≫ ψ.s = φ.s ≫ ψ.f

Tactic:
exact ⟨ψ.op, Quiver.Hom.unop_inj eq⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P Q P' : ObjectProperty C
h : P ≤ P'
X Y Z : C
f : Y ⟶ X
g : X ⟶ Z
k : Z ⟶ (shiftFunctor C 1).obj Y
hT : Triangle.mk f g k ∈ distinguishedTriangles
hP : P Y
hQ : Q Z
⊢ P'.extensionProduct Q X

Tactic:
exact ⟨Y, Z, f, g, k, hT, h Y hP, hQ⟩

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ X₃ : CochainComplex C ℤ
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ Cochain.ofHom (inv f g ≫ hom f g) =
    δ (-1) 0
        (-(snd (mappingConeCompTriangle f g).mor₁).comp
            ((↑(fst (f ≫ g))).comp ((inl f).comp (inl (mappingConeCompTriangle f g).mor₁) homotopyInvHomId._proof_1) ⋯)
            ⋯) +
      Cochain.ofHom (𝟙 (mappingCone (mappingConeCompTriangle f g).mor₁))

Tactic:
rw [δ_neg, δ_zero_cochain_comp _ _ _ (neg_add_cancel 1),
        Int.negOnePow_neg, Int.negOnePow_one, Units.neg_smul, one_smul,
        δ_comp _ _ (show 1 + (-2) = -1 by decide) 2 (-1) 0 (by decide)
          (by decide) (by decide),
        δ_comp _ _ (show (-1) + (-1) = -2 by decide) 0 0 (-1) (by decide)
          (by decide) (by decide), Int.negOnePow_neg, Int.negOnePow_neg,
        Int.negOnePow_even 2 ⟨1, by decide⟩, Int.negOnePow_one, Units.neg_smul,
        one_smul, one_smul, δ_inl, δ_inl, δ_snd, Cocycle.δ_eq_zero, Cochain.zero_comp, add_zero,
        Cochain.neg_comp, neg_neg]
      ext n
      rw [ext_from_iff _ (n + 1) n rfl, ext_from_iff _ (n + 1) n rfl,
        ext_from_iff _ (n + 2) (n + 1) (by lia)]
      dsimp [hom, inv]
      simp [ext_to_iff _ n (n + 1) rfl, map, Cochain.comp_v _ _
          (add_neg_cancel 1) n (n + 1) n (by lia) (by lia),
        Cochain.comp_v _ _ (show 1 + -2 = -1 by decide) (n + 1) (n + 2) n
          (by lia) (by lia),
        Cochain.comp_v _ _ (show (-1) + -1 = -2 by decide) (n + 2) (n + 1) n
          (by lia) (by lia)]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁✝ X₂✝ X₃✝ : CochainComplex C ℤ
f : X₁✝ ⟶ X₂✝
g : X₂✝ ⟶ X₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj (mappingCone.triangle u₁₂)).mor₃ ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((quotient C (ComplexShape.up ℤ)).mapTriangle.map α).hom₁ =
    (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₃ ≫
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone.triangle u₁₂).obj₁

Tactic:
by dsimp [α]; simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
i j : ι
i' j' : ι'
hj' : e.f j = j'
hi : c.prev j = i
hi' : c'.prev j' = i'
W : C
φ : K.X j ⟶ W
hij : c.Rel i j
⊢ K.d i j ≫ φ = 0 ↔ (K.extend e).d i' j' ≫ (K.extendXIso e hj').hom ≫ φ = 0

Tactic:
have hi' : e.f i = i' := by rw [← hi', ← hj', c'.prev_eq' (e.rel hij)]
    rw [K.extend_d_eq e hi' hj', assoc, assoc, Iso.inv_hom_id_assoc,
      ← cancel_epi (K.extendXIso e hi').hom, comp_zero]

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: case neg
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : HasZeroMorphisms C
e : c.Embedding c'
K : HomologicalComplex C c
inst✝ : ∀ (i : ι), Injective (K.X i)
i' : ι'
hi' : ∀ (i : ι), e.f i ≠ i'
⊢ Injective ((K.extend e).X i')

Tactic:
exact (isZero_extend_X K e i' hi').injective

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.TruncLEHomology

Goal state before:
pp: case pos.hf
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : Abelian C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝ : e.IsTruncLE
i : ι
j' : ι'
hj' : c'.Rel (e.f i) j'
⊢ { X₁ := (K.shortComplexTruncLE e).X₂.homology (e.f i), X₂ := (K.shortComplexTruncLE e).X₃.homology (e.f i),
        X₃ := (K.shortComplexTruncLE e).X₁.homology j', f := homologyMap (K.shortComplexTruncLE e).g (e.f i),
        g := ⋯.δ (e.f i) j' hj', zero := ⋯ }.f =
    0

Tactic:
rw [← cancel_epi (homologyMap (K.ιTruncLE e) (e.f i)), comp_zero]
        dsimp [shortComplexTruncLE]
        rw [← homologyMap_comp, cokernel.condition, homologyMap_zero]

Goal state after: