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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
J : Type u_1
T : J → Triangle C
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₁
inst✝ : HasZeroMorphisms C
h : ∀ (j : J), (T j).mor₃ ≫ (shiftFunctor C 1).map (T j).mor₁ = 0
this : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₂
⊢ ((Limits.Pi.map fun j ↦ (T j).mor₃) ≫
      inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) ≫
        (shiftFunctor C 1).map (Pi.lift fun j ↦ Pi.π (fun j ↦ (T j).obj₁) j ≫ (T j).mor₁) ≫
          piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₂) =
    0

Tactic:
ext j

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasShift C ℤ
J : Type u_1
T : J → Triangle C
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₁
inst✝ : HasZeroMorphisms C
h : ∀ (j : J), (T j).mor₃ ≫ (shiftFunctor C 1).map (T j).mor₁ = 0
this : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₂
j : J
⊢ ((Limits.Pi.map fun j ↦ (T j).mor₃) ≫
        inv (piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₁) ≫
          (shiftFunctor C 1).map (Pi.lift fun j ↦ Pi.π (fun j ↦ (T j).obj₁) j ≫ (T j).mor₁) ≫
            piComparison (shiftFunctor C 1) fun j ↦ (T j).obj₂) ≫
      Pi.π (fun b ↦ (shiftFunctor C 1).obj (T b).obj₂) j =
    0 ≫ Pi.π (fun b ↦ (shiftFunctor C 1).obj (T b).obj₂) j
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₁) =
    (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₁)

Tactic:
Int.negOnePow_add,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a.negOnePow * b.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₁) =
    (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₁ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₁)
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a + b).negOnePow •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₂) =
    (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₂)

Tactic:
Int.negOnePow_add,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
a b : ℤ
T : Triangle C
⊢ (a.negOnePow * b.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₂) =
    (b.negOnePow * a.negOnePow) •
      (CategoryTheory.shiftFunctorAdd' C a b (a + b) ⋯).hom.app T.obj₂ ≫
        (CategoryTheory.shiftFunctor C b).map ((CategoryTheory.shiftFunctor C a).map T.mor₂)
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
⊢ (a * n + a * (a - 1) / 2).negOnePow • γ.shift a =
    (a.negOnePow * (a * a + a * n + a * (a - 1) / 2).negOnePow) • γ.shift a

Tactic:
Int.negOnePow_add,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
⊢ ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a * a + a * n + a * (a - 1) / 2).negOnePow) • γ.shift a
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
⊢ ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * (a * a + a * n + a * (a - 1) / 2).negOnePow) • γ.shift a

Tactic:
Int.negOnePow_add,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
⊢ ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * ((a * a + a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
⊢ ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * ((a * a + a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a

Tactic:
Int.negOnePow_add,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a n' n'' : ℤ
hn' : n' + a = n
hn'' : n + a = n''
⊢ ((a * n).negOnePow * (a * (a - 1) / 2).negOnePow) • γ.shift a =
    (a.negOnePow * ((a * a).negOnePow * (a * n).negOnePow * (a * (a - 1) / 2).negOnePow)) • γ.shift a
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
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
⊢ g ≫ T.mor₁ = 0

Tactic:
obtain ⟨h, hh⟩ := Triangle.coyoneda_exact₂ T'.invRotate (inv_rot_of_distTriang _ hT')
      (g ≫ φ.hom₁) (by dsimp; rw [assoc, ← φ.comm₁, hf])

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
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₃ : IsIso φ.hom₃
A : C
g : A ⟶ T.obj₁
hf : g ≫ T.mor₁ ≫ φ.hom₂ = 0
h : A ⟶ T'.invRotate.obj₁
hh : g ≫ φ.hom₁ = h ≫ T'.invRotate.mor₁
⊢ g ≫ T.mor₁ = 0
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
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ inr φ ≫ (triangle φ).mor₃ = 0

Tactic:
by ext; simp

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
K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
φ₂ : K₂ ⟶ L₂
φ₃ : K₃ ⟶ L₃
a : K₁ ⟶ K₂
b : L₁ ⟶ L₂
comm : φ₁ ≫ b = a ≫ φ₂
a' : K₂ ⟶ K₃
b' : L₂ ⟶ L₃
⊢ (triangle φ₁).mor₂ ≫ map φ₁ φ₂ a b comm = b ≫ (triangle φ₂).mor₂

Tactic:
by
    dsimp
    rw [map_eq_mapOfHomotopy, triangleMapOfHomotopy_comm₂]

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₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun j ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ g_1, g ≫ Pi.π (fun j ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
α : (j : J) → A ⟶ (T j).obj₁ := fun j ↦ ⋯.choose
hα : ∀ (j : J), g ≫ Pi.π (fun j ↦ (T j).obj₂) j = α j ≫ (T j).mor₁
⊢ g = Pi.lift α ≫ Limits.Pi.map fun j ↦ (T j).mor₁

Tactic:
ext j

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₂
hg' : ∀ (j : J), (g ≫ Pi.π (fun j ↦ (T j).obj₂) j) ≫ (T j).mor₂ = 0
hg'' : ∀ (j : J), ∃ g_1, g ≫ Pi.π (fun j ↦ (T j).obj₂) j = g_1 ≫ (T j).mor₁
α : (j : J) → A ⟶ (T j).obj₁ := fun j ↦ ⋯.choose
hα : ∀ (j : J), g ≫ Pi.π (fun j ↦ (T j).obj₂) j = α j ≫ (T j).mor₁
j : J
⊢ g ≫ Pi.π (fun j ↦ (T j).obj₂) j = (Pi.lift α ≫ Limits.Pi.map fun j ↦ (T j).mor₁) ≫ Pi.π (fun j ↦ (T j).obj₂) j
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₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ : T₁.mor₂ ≫ γ.hom₃ = γ.hom₂ ≫ T₂.mor₂
⊢ ∃ c,
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃

Tactic:
have comm₃ := γ.comm₃

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ : T₁.mor₂ ≫ γ.hom₃ = γ.hom₂ ≫ T₂.mor₂
comm₃ : T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map γ.hom₁ = γ.hom₃ ≫ T₂.mor₃
⊢ ∃ c,
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃
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₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ : T₁.mor₂ ≫ γ.hom₃ = γ.hom₂ ≫ T₂.mor₂
comm₃ : T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map γ.hom₁ = γ.hom₃ ≫ T₂.mor₃
⊢ ∃ c,
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃

Tactic:
dsimp [γ] at comm₂ comm₃

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
H : Homotopy (φ₁ ≫ b'') (a'' ≫ φ₂)
γ : T₁ ⟶ T₂ := e₁.hom ≫ trianglehMapOfHomotopy H ≫ e₂.inv
comm₂ :
  T₁.mor₂ ≫ e₁.hom.hom₃ ≫ (quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) ≫ e₂.inv.hom₃ =
    (e₁.hom.hom₂ ≫ (quotient C (ComplexShape.up ℤ)).map b'' ≫ e₂.inv.hom₂) ≫ T₂.mor₂
comm₃ :
  T₁.mor₃ ≫
      (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (e₁.hom.hom₁ ≫ (quotient C (ComplexShape.up ℤ)).map a'' ≫ e₂.inv.hom₁) =
    (e₁.hom.hom₃ ≫ (quotient C (ComplexShape.up ℤ)).map (mapOfHomotopy H) ≫ e₂.inv.hom₃) ≫ T₂.mor₃
⊢ ∃ c,
    T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map a = c ≫ T₂.mor₃
Module: Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (triangle φ).rotate.mor₃ ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map (Iso.refl (triangle φ).rotate.obj₁).hom =
    (Iso.refl (triangle φ).rotate.obj₃).hom ≫
      (triangleOfDegreewiseSplit (triangleRotateShortComplex φ) (triangleRotateShortComplexSplitting φ)).mor₃

Tactic:
by ext; simp

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✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C :=
  { X₁ := K.homology i, X₂ := K.opcycles i, X₃ := K.cycles j, f := K.homologyι i, g := K.opcyclesToCycles i j,
    zero := ⋯ }
S' : ShortComplex C :=
  { X₁ := K.homology i, X₂ := K.opcycles i, X₃ := K.X j, f := K.homologyι i, g := K.fromOpcycles i j, zero := ⋯ }
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex C :=
  { X₁ := K.opcycles i, X₂ := K.cycles j, X₃ := K.homology j, f := K.opcyclesToCycles i j, g := K.homologyπ j,
    zero := ⋯ }
T' : ShortComplex C :=
  { X₁ := K.X i, X₂ := K.cycles j, X₃ := K.homology j, f := K.toCycles i j, g := K.homologyπ j, zero := ⋯ }
⊢ (composableArrows₃ K i j).Exact

Tactic:
let π : T' ⟶ T :=
    { τ₁ := K.pOpcycles i
      τ₂ := 𝟙 _
      τ₃ := 𝟙 _ }

Goal state after:
C : Type u_1
ι✝ : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι✝
K : HomologicalComplex C c
i j : ι✝
hij : c.Rel i j
inst✝ : CategoryWithHomology C
S : ShortComplex C :=
  { X₁ := K.homology i, X₂ := K.opcycles i, X₃ := K.cycles j, f := K.homologyι i, g := K.opcyclesToCycles i j,
    zero := ⋯ }
S' : ShortComplex C :=
  { X₁ := K.homology i, X₂ := K.opcycles i, X₃ := K.X j, f := K.homologyι i, g := K.fromOpcycles i j, zero := ⋯ }
ι : S ⟶ S' := { τ₁ := 𝟙 S.X₁, τ₂ := 𝟙 S.X₂, τ₃ := K.iCycles j, comm₁₂ := ⋯, comm₂₃ := ⋯ }
hS : S.Exact
T : ShortComplex C :=
  { X₁ := K.opcycles i, X₂ := K.cycles j, X₃ := K.homology j, f := K.opcyclesToCycles i j, g := K.homologyπ j,
    zero := ⋯ }
T' : ShortComplex C :=
  { X₁ := K.X i, X₂ := K.cycles j, X₃ := K.homology j, f := K.toCycles i j, g := K.homologyπ j, zero := ⋯ }
π : T' ⟶ T := { τ₁ := K.pOpcycles i, τ₂ := 𝟙 T'.X₂, τ₃ := 𝟙 T'.X₃, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ (composableArrows₃ K i j).Exact
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 j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ x₁ ≫ S.X₁.d j k = 0

Tactic:
by
        have := hS.mono_f
        rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁,
          d_comp_d, comp_zero, zero_comp]

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 : C
f₁ f₂ : L.obj X ⟶ L.obj Y
φ : W.LeftFraction₂ X Y
hφ₁ : f₁ = φ.fst.map L ⋯
hφ₂ : f₂ = φ.snd.map L ⋯
⊢ add' W f₁ f₂ = φ.add.map L ⋯

Tactic:
obtain ⟨φ₀, rfl, rfl, hφ₀⟩ : ∃ (φ₀ : W.LeftFraction₂ X Y)
    (_ : f₁ = φ₀.fst.map L (inverts L W))
    (_ : f₂ = φ₀.snd.map L (inverts L W)),
    add' W f₁ f₂ = φ₀.add.map L (inverts L W) :=
    ⟨(exists_leftFraction₂ L W f₁ f₂).choose,
      (exists_leftFraction₂ L W f₁ f₂).choose_spec.1,
      (exists_leftFraction₂ L W f₁ f₂).choose_spec.2, rfl⟩
  obtain ⟨Z, t₁, t₂, hst, hft, hft', ht⟩ := (LeftFraction₂.map_eq_iff L W φ₀ φ).1 ⟨hφ₁, hφ₂⟩
  have := inverts L W _ ht
  rw [hφ₀, ← cancel_mono (L.map (φ₀.s ≫ t₁))]
  nth_rw 2 [hst]
  rw [L.map_comp, L.map_comp, LeftFraction.map_comp_map_s_assoc,
    LeftFraction.map_comp_map_s_assoc, ← L.map_comp, ← L.map_comp,
    add_comp, add_comp, hft, hft']

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j ↦ transfiniteIterate φ j i₀
i : I
⊢ i ≤ φ i

Tactic:
by_cases hi : i = ⊤

Goal state after:
case pos
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j ↦ transfiniteIterate φ j i₀
i : I
hi : i = ⊤
⊢ i ≤ φ i

case neg
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j ↦ transfiniteIterate φ j i₀
i : I
hi : ¬i = ⊤
⊢ i ≤ φ i
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
⊢ ∃ j₁ j₂, ∃ (_ : j₁ < j₂), transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀

Tactic:
grind [Function.Injective]

Goal state after:
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective fun j ↦ transfiniteIterate φ j i₀
⊢ ∃ j, transfiniteIterate φ j i₀ = ⊤

Tactic:
have hφ (i : I) : i ≤ φ i := by
    by_cases hi : i = ⊤
    · subst hi
      rw [φtop]
    · exact (hφ' i hi).le
  obtain ⟨j₁, j₂, hj, eq⟩ : ∃ (j₁ j₂ : J) (hj : j₁ < j₂),
      transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀ := by
    grind [Function.Injective]
  by_contra!
  suffices transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀ by
    simp only [eq, lt_self_iff_false] at this
  have hj₁ : ¬ IsMax j₁ := by
    simp only [not_isMax_iff]
    exact ⟨_, hj⟩
  refine lt_of_lt_of_le (hφ' _ (this j₁)) ?_
  rw [← transfiniteIterate_succ φ i₀ j₁ hj₁]
  exact monotone_transfiniteIterate _ _ hφ (Order.succ_le_of_lt hj)

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasTerminal C
P Q : ObjectProperty C
inst✝¹ : Q.IsClosedUnderBinaryProducts
inst✝ : Q.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
⊢ P.binaryProductsClosure ≤ Q ↔ P ≤ Q

Tactic:
refine ⟨fun h ↦ (P.le_limitsClosure _).trans h, fun h ↦ ?_⟩
  let : Q.IsClosedUnderIsomorphisms := IsClosedUnderBinaryProducts.closedUnderIsomorphisms Q
  exact limitsClosure_le h

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

Goal state before:
pp: case mpr
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
inst✝ : W.HasRightCalculusOfFractions
Y Z : C
f₁ f₂ : Y ⟶ Z
⊢ (∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂) → L.map f₁ = L.map f₂

Tactic:
rintro ⟨Z, s, hs, fac⟩
    simp only [← cancel_epi (Localization.isoOfHom L W s hs).hom,
      Localization.isoOfHom_hom, ← L.map_comp, fac]

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.Retract

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝² w✝¹ : C
w✝ : w✝² ⟶ w✝¹
hg : RetractArrow f✝ w✝
hg' : a✝ w✝
⊢ b✝.retracts f✝

Tactic:
exact ⟨_, _, _, hg, h _ hg'⟩

Goal state after: