mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
⊢ (liftCochain φ α β h).comp (↑(fst φ)) h = α

Tactic:
by
  simp [liftCochain]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
K : CochainComplex C ℤ
n m : ℤ
α : Cochain K F m
β : Cochain K G n
h : n + 1 = m
⊢ (liftCochain φ α β h).comp (snd φ) ⋯ = β

Tactic:
by
  simp [liftCochain]

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : K.HasCylinder
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
⊢ inrX K j ≫ (nullHomotopicMap K).f j = inrX K j ≫ (π K ≫ ι₀ K - 𝟙 K.cylinder).f j

Tactic:
have : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr :=
    biprod.hom_ext _ _ (by simp) (by simp)
  obtain ⟨i, hij⟩ := hc j
  dsimp [nullHomotopicMap]
  by_cases hj : ∃ (k : ι), c.Rel j k
  · obtain ⟨k, hjk⟩ := hj
    simp only [Homotopy.nullHomotopicMap'_f hij hjk, homotopyCofiber_d, assoc, comp_add,
      homotopyCofiber.inrX_d_assoc, homotopyCofiber.inrX_sndX_assoc, comp_sub,
      inrX_π_assoc, comp_id, ← Hom.comm_assoc, homotopyCofiber.inlX_d _ _ _ _ _ hjk,
      comp_neg, add_neg_cancel_left]
    rw [← cancel_epi (biprodXIso K K j).inv]
    ext
    · simp [ι₀]
    · simp only [inr_biprodXIso_inv_assoc, biprod_inr_snd_f_assoc, comp_sub,
        biprod_inr_desc_f_assoc, id_f, id_comp, ι₀, comp_f, this,
        sub_f_apply, sub_comp, homotopyCofiber.inr_f]
  · simp only [not_exists] at hj
    simp only [assoc, Homotopy.nullHomotopicMap'_f_of_not_rel_left hij hj,
      homotopyCofiber_d, homotopyCofiber.inlX_d' _ _ _ _ (hj _), homotopyCofiber.inrX_sndX_assoc,
      comp_sub, inrX_π_assoc, comp_id, ι₀, comp_f, homotopyCofiber.inr_f]
    rw [← cancel_epi (biprodXIso K K j).inv]
    ext
    · simp
    · simp [this]

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

Goal state before:
pp: ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C : HomologicalComplex V c
⊢ IsZero ((quotient V c).obj C) ↔ Nonempty (Homotopy (𝟙 C) 0)

Tactic:
by
  rw [IsZero.iff_id_eq_zero]
  constructor
  · intro h
    exact ⟨(homotopyOfEq _ _ (by simp [h]))⟩
  · rintro ⟨h⟩
    simpa using (eq_of_homotopy _ _ h)

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      𝟙 (F.obj X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (shiftFunctorZero D A).inv.app (F.obj X)

Tactic:
id_comp

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (shiftFunctorZero D A).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (shiftFunctorZero D A).inv.app (F.obj X)
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
a b : ℤ
x✝ : HomologicalComplex C (ComplexShape.up ℤ)
i✝ : ℤ
⊢ 𝟙 (F.obj (x✝.X (i✝ + (a + b)))) =
    F.map (((shiftFunctorAdd (HomologicalComplex C (ComplexShape.up ℤ)) a b).hom.app x✝).f i✝) ≫
      𝟙 (F.obj (x✝.X (i✝ + b + a))) ≫
        ((shiftFunctorAdd (HomologicalComplex D (ComplexShape.up ℤ)) a b).inv.app
              ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj x✝)).f
          i✝

Tactic:
id_comp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : Preadditive C
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
a b : ℤ
x✝ : HomologicalComplex C (ComplexShape.up ℤ)
i✝ : ℤ
⊢ 𝟙 (F.obj (x✝.X (i✝ + (a + b)))) =
    F.map (((shiftFunctorAdd (HomologicalComplex C (ComplexShape.up ℤ)) a b).hom.app x✝).f i✝) ≫
      ((shiftFunctorAdd (HomologicalComplex D (ComplexShape.up ℤ)) a b).inv.app
            ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj x✝)).f
        i✝
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
D : Type u'
inst✝³ : Category.{v', u'} D
inst✝² : Preadditive D
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
n : ℤ
⊢ ∀ {X Y : HomotopyCategory C (ComplexShape.up ℤ)} (f : X ⟶ Y) (r : R),
    (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map (r • f) =
      r • (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) n).map f

Tactic:
rintro ⟨X⟩ ⟨Y⟩ f r
    obtain ⟨f, rfl⟩ := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map_surjective f
    have h₁ := NatIso.naturality_1 ((HomotopyCategory.quotient _ _).commShiftIso n) f
    have h₂ := NatIso.naturality_1 ((HomotopyCategory.quotient _ _).commShiftIso n) (r • f)
    dsimp at h₁ h₂
    rw [← Functor.map_smul, ← h₁, ← h₂]
    simp

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

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
F : C ⥤ D
G : D ⥤ E
A : Type u_4
B : Type u_5
inst✝⁸ : AddMonoid A
inst✝⁷ : AddCommMonoid B
inst✝⁶ : HasShift C A
inst✝⁵ : HasShift D A
inst✝⁴ : HasShift E A
inst✝³ : HasShift C B
inst✝² : HasShift D B
inst✝¹ : F.CommShift A
inst✝ : G.CommShift A
a b : A
⊢ ((shiftFunctor C (a + b)).associator F G).symm ≪≫
      isoWhiskerRight (commShiftIso F (a + b)) G ≪≫
        F.associator (shiftFunctor D (a + b)) G ≪≫
          F.isoWhiskerLeft (commShiftIso G (a + b)) ≪≫ (F.associator G (shiftFunctor E (a + b))).symm =
    isoAdd
      (((shiftFunctor C a).associator F G).symm ≪≫
        isoWhiskerRight (commShiftIso F a) G ≪≫
          F.associator (shiftFunctor D a) G ≪≫
            F.isoWhiskerLeft (commShiftIso G a) ≪≫ (F.associator G (shiftFunctor E a)).symm)
      (((shiftFunctor C b).associator F G).symm ≪≫
        isoWhiskerRight (commShiftIso F b) G ≪≫
          F.associator (shiftFunctor D b) G ≪≫
            F.isoWhiskerLeft (commShiftIso G b) ≪≫ (F.associator G (shiftFunctor E b)).symm)

Tactic:
ext X
    dsimp
    simp only [commShiftIso_add, isoAdd_hom_app]
    dsimp
    simp only [comp_id, id_comp, assoc, ← Functor.map_comp_assoc, Iso.inv_hom_id_app, comp_obj]
    simp only [map_comp, assoc, commShiftIso_hom_naturality_assoc]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
n : ℕ
f : T₁ ⟶ T₂
⊢ ↑n.succ • f = ↑n • f + f

Tactic:
ext <;> apply SubNegMonoid.zsmul_succ'

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
γ' : Cochain L M 0
⊢ (γ.comp γ' ⋯).leftShift a n' hn' = (γ.leftShift a n' hn').comp γ' ⋯

Tactic:
leftShift_comp γ a n' hn' γ' (add_zero _) hn',

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L M : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' : ℤ
hn' : n + a = n'
γ' : Cochain L M 0
⊢ (a * 0).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯ = (γ.leftShift a n' hn').comp γ' ⋯
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case mp
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.mor₁ = 0 ∧ T.mor₃ = 0 → IsIso T.mor₂

Tactic:
intro ⟨h₁, h₃⟩
    have := T.epi₂ hT h₃
    obtain ⟨f, hf⟩ := yoneda_exact₂ T hT (𝟙 _) (by rw [h₁, zero_comp])
    exact ⟨f, hf.symm, by rw [← cancel_epi T.mor₂, comp_id, ← reassoc_of% hf]⟩

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
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝¹ : IsIso φ'.hom₁
this✝ : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
j : J
this : g ≫ 𝟙 T'.obj₂ ≫ (productTriangle T).mor₂ ≫ Pi.π (fun j ↦ (T j).obj₃) j = 0
⊢ (g ≫ Pi.π (fun j ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0

Tactic:
id_comp

Goal state after:
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
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝¹ : IsIso φ'.hom₁
this✝ : IsIso φ'.hom₂
A✝ A : C
f : A ⟶ T'.obj₃
hf : f ≫ φ'.hom₃ = 0
hf' : f ≫ T'.mor₃ = 0
g : A ⟶ T'.obj₂
hg : f = g ≫ T'.mor₂
j : J
this : g ≫ (productTriangle T).mor₂ ≫ Pi.π (fun j ↦ (T j).obj₃) j = 0
⊢ (g ≫ Pi.π (fun j ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: case refine_2
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
G : C ⥤ D
inst✝ : G.Additive
⊢ inr ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ) =
    𝟙 ((G.mapHomologicalComplex (ComplexShape.up ℤ)).obj L) ≫ inr ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)

Tactic:
id_comp

Goal state after:
case refine_2
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
G : C ⥤ D
inst✝ : G.Additive
⊢ inr ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ) = inr ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
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
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
j : J
⊢ a ≫ (productTriangle T).mor₃ ≫ (shiftFunctor C 1).map (productTriangle.π T j).hom₁ =
    a ≫
      (productTriangle T).mor₃ ≫
        𝟙 ((shiftFunctor C 1).obj T'.obj₁) ≫ (shiftFunctor C 1).map (productTriangle.π T j).hom₁

Tactic:
id_comp

Goal state after:
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
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
φ' : T' ⟶ productTriangle T := productTriangle.lift T φ
h₁ : φ'.hom₁ = 𝟙 T'.obj₁
h₂ : φ'.hom₂ = 𝟙 T'.obj₂
this✝ : IsIso φ'.hom₁
this : IsIso φ'.hom₂
A : C
a : A ⟶ (productTriangle T).obj₃
a' : A ⟶ Z
ha' : a' ≫ T'.mor₃ = a ≫ (productTriangle T).mor₃
j : J
⊢ a ≫ (productTriangle T).mor₃ ≫ (shiftFunctor C 1).map (productTriangle.π T j).hom₁ =
    a ≫ (productTriangle T).mor₃ ≫ (shiftFunctor C 1).map (productTriangle.π T j).hom₁
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
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X =
    𝟙 ((F.shift a).obj ((shiftFunctor C m ⋙ shiftFunctor C n).obj X)) ≫
      (F.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X

Tactic:
id_comp

Goal state after:
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
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X =
    (F.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj X) ≫ (F.shiftIso m a' a'' ha'').hom.app X
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
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ τ.app (L.obj (W.Q.obj x✝).as.obj) =
    𝟙 (X✝.obj (L.obj (W.Q.obj x✝).as.obj)) ≫ ((whiskeringLeftFunctor L W E).map τ).hom.app x✝

Tactic:
id_comp

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
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
X✝ Y✝ : D ⥤ E
τ : X✝ ⟶ Y✝
x✝ : C
⊢ τ.app (L.obj (W.Q.obj x✝).as.obj) = ((whiskeringLeftFunctor L W E).map τ).hom.app x✝
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
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
P : MorphismProperty D
inst✝¹ : P.RespectsIso
inst✝ : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ e.hom.app Y = 𝟙 ((uniq W.Q L W).functor.obj (W.Q.obj Y)) ≫ e.hom.app Y

Tactic:
id_comp

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
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
P : MorphismProperty D
inst✝¹ : P.RespectsIso
inst✝ : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ e.hom.app Y = e.hom.app Y
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₁, u₁} C₁
inst✝⁶ : Category.{v₂, u₂} C₂
inst✝⁵ : Category.{v₃, u₃} C₃
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝ : Φ.IsLocalizedFullyFaithful
⊢ Φ.op.IsLocalizedFullyFaithful

Tactic:
by
  let G := Φ.localizedFunctor W₁.Q W₂.Q
  let : CatCommSq Φ.op.functor W₁.Q.op W₂.Q.op G.op :=
    ⟨NatIso.op (CatCommSq.iso Φ.functor W₁.Q W₂.Q G).symm⟩
  exact IsLocalizedFullyFaithful.mk' Φ.op W₁.Q.op W₂.Q.op G.op
    (Φ.fullyFaithful W₁.Q W₂.Q G).op

Goal state after:
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: case inl
X : Type u_1
P₁ P₂ : X → Prop
κ : Cardinal.{u_2}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT (Subtype P₁) κ
h₂ : HasCardinalLT (Subtype P₂) κ
this : HasCardinalLT (Subtype P₁ ⊕ Subtype P₂) κ
x : X
hx : P₁ x
⊢ ∃ a, Sum.elim (fun x ↦ ⟨↑x, ⋯⟩) (fun x ↦ ⟨↑x, ⋯⟩) a = ⟨x, ⋯⟩

Tactic:
exact ⟨Sum.inl ⟨x, hx⟩, rfl⟩

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
⊢ (P ⊔ Q).shift a = P.shift a ⊔ Q.shift a

Tactic:
ext
  simp [prop_shift_iff]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
ι : Sort u_4
P : ι → ObjectProperty C
a : A
⊢ (⨆ i, P i).shift a = ⨆ i, (P i).shift a

Tactic:
ext
  simp [prop_shift_iff]

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₂.obj ((Q W).obj Y)) ≫ eqToHom ⋯

Tactic:
id_comp

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 ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x✝³ x✝² x✝¹ x✝ : C
f : x✝³ ⟶ x✝²
g : x✝¹ ⟶ x✝
h : RetractArrow f g
hg : Epi g
Z✝ : C
α β : x✝² ⟶ Z✝
w : f ≫ α = f ≫ β
⊢ α = β

Tactic:
rw [← cancel_epi h.r.right, ← cancel_epi g, ← Category.assoc, ← Category.assoc, ← h.r_w,
      Category.assoc, Category.assoc, w]

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 : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
⊢ P.trW g ↔ ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P X

Tactic:
rw [P.trW_iff]

Goal state after:
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 : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
Y Z : C
g : Y ⟶ Z
⊢ (∃ Z_1 g_1 h, ∃ (_ : Triangle.mk g g_1 h ∈ distinguishedTriangles), P Z_1) ↔
    ∃ X f h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), P X
Module: Mathlib.Algebra.Homology.Localization

Goal state before:
pp: case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
K' L' : HomologicalComplex C c
g : K' ⟶ L'
h : HomologicalComplex.quasiIso C c g
e : Arrow.mk ((quotient C c).map g) ≅ Arrow.mk ((quotient C c).map f)
⊢ quasiIso C c ((quotient C c).map f)

Tactic:
← quotient_map_mem_quasiIso_iff

Goal state after:
case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
ι : Type u_2
c : ComplexShape ι
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
K L : HomologicalComplex C c
f : K ⟶ L
K' L' : HomologicalComplex C c
g : K' ⟶ L'
h : quasiIso C c ((quotient C c).map g)
e : Arrow.mk ((quotient C c).map g) ≅ Arrow.mk ((quotient C c).map f)
⊢ quasiIso C c ((quotient C c).map f)
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 : ObjectProperty C
inst✝ : P.IsClosedUnderIsomorphisms
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ P.trW T.mor₁ ↔ P T.obj₃

Tactic:
by
  constructor
  · rintro ⟨Z, g, h, hT', mem⟩
    obtain ⟨e, _⟩ := exists_iso_of_arrow_iso _ _ hT' hT (Iso.refl _)
    exact P.prop_of_iso (Triangle.π₃.mapIso e) mem
  · intro h
    exact ⟨_, _, _, hT, h⟩

Goal state after: