mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Twist

Goal state before:
pp: case e_a
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
i j k : A
h : i + j = k
X : t.Category
this : (shiftFunctorAdd' t.Category i j k h).hom.app X = ↑(t.z i j) • (shiftFunctorAdd' C i j k h).hom.app X
⊢ (shiftFunctorAdd' C i j k h).hom.app X =
    (t.shiftIso k).hom.app X ≫
      (shiftFunctorAdd' C i j k h).hom.app X ≫
        (shiftFunctor C j).map ((t.shiftIso i).inv.app X) ≫ (t.shiftIso j).inv.app ((shiftFunctor t.Category i).obj X)

Tactic:
change _ = 𝟙 _ ≫ _ ≫ (shiftFunctor C j).map (𝟙 _) ≫ 𝟙 _

Goal state after:
case e_a
C : Type u
inst✝² : Category.{v, u} C
A : Type w
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
t : TwistShiftData C A
i j k : A
h : i + j = k
X : t.Category
this : (shiftFunctorAdd' t.Category i j k h).hom.app X = ↑(t.z i j) • (shiftFunctorAdd' C i j k h).hom.app X
⊢ (shiftFunctorAdd' C i j k h).hom.app X =
    𝟙 ((shiftFunctor C k).obj X) ≫
      (shiftFunctorAdd' C i j k h).hom.app X ≫
        (shiftFunctor C j).map (𝟙 ((shiftFunctor C i).obj X)) ≫ 𝟙 ((shiftFunctor C j).obj ((shiftFunctor C i).obj X))
Module: Mathlib.Algebra.Homology.BifunctorHomotopy

Goal state before:
pp: case a
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ : K₂ ⟶ L₂
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
j : J
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c (i₁, i₂) = j
this : ∀ {X Y : D} (a b c d e f : X ⟶ Y), a = c → b = e → f = -d → a + b = c + d + (e + f)
⊢ (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
      (F.map (L₁.d (c₁.prev i₁) i₁)).app (K₂.X i₂) ≫
        (F.obj (L₁.X i₁)).map (f₂.f i₂) ≫ L₁.ιMapBifunctor L₂ F c i₁ i₂ j h =
    K₁.ιMapBifunctor K₂ F c i₁ i₂ j h ≫
      hom₁ h₁ f₂ F c j (c.prev j) ≫ (((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).D₁ c (c.prev j) j

Tactic:
rw [ιMapBifunctor_hom₁_assoc _ _ _ _ _ _ _ _ _ _ rfl]
    by_cases h₃ : c₁.Rel (c₁.prev i₁) i₁
    · rw [ιMapBifunctorOrZero_eq _ _ _ _ _ _ _ (by rw [← ComplexShape.prev_π₁ c₂ c h₃, h]),
        Linear.units_smul_comp, assoc, assoc, HomologicalComplex₂.ι_D₁,
        HomologicalComplex₂.d₁_eq _ _ h₃ _ _ h, Linear.comp_units_smul,
        Linear.comp_units_smul, smul_smul, Int.units_mul_self, one_smul,
        Functor.mapBifunctorHomologicalComplex_obj_obj_d_f, NatTrans.naturality_assoc]
    · rw [h₁.zero _ _ h₃, Functor.map_zero, zero_app, zero_comp, zero_comp, smul_zero, zero_comp]

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

Goal state before:
pp: case e_a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
f g : K ⟶ L
h : Homotopy ((opEquivalence C).functor.map f.op) ((opEquivalence C).functor.map g.op)
H :
  ∀ (p q p' q' : ℤ) (hp : p = p') (hq : q = q'),
    h.hom p q = (HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom p' q' ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op
n : ℤ
this : (f.f (-n)).op = (dNext n) h.hom + (prevD n) h.hom + (g.f (-n)).op
⊢ (L.d (-(n + 1)) (-n)).op ≫ h.hom (n + 1) n =
    (L.d (-(n + 1)) (-n)).op ≫
      ((HomologicalComplex.XIsoOfEq L ⋯).hom.op ≫ h.hom (- -(n + 1)) (- -n)) ≫ (HomologicalComplex.XIsoOfEq K ⋯).hom.op

Tactic:
simp [H (- -(n + 1)) (- -n) (n + 1) n (by simp) (by simp), ← op_comp_assoc, ← op_comp]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
h : IsPushout f g inl inr
⊢ ∀ (R : C) (g_1 : ⋯.shortComplex.X₃ ⟶ R), ⋯.shortComplex.g ≫ g_1 = 0 → g_1 = 0

Tactic:
intro _ b hb

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
f : X₁ ⟶ X₂
g : X₁ ⟶ X₃
inl : X₂ ⟶ X₄
inr : X₃ ⟶ X₄
h : IsPushout f g inl inr
R✝ : C
b : ⋯.shortComplex.X₃ ⟶ R✝
hb : ⋯.shortComplex.g ≫ b = 0
⊢ b = 0
Module: Mathlib.Algebra.Homology.CommSq

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
⊢ ∀ (P : C) (g_1 : P ⟶ ⋯.shortComplex'.X₁), g_1 ≫ ⋯.shortComplex'.f = 0 → g_1 = 0

Tactic:
intro _ b hb

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
X₁ X₂ X₃ X₄ : C
inst✝ : HasBinaryBiproduct X₂ X₃
fst : X₁ ⟶ X₂
snd : X₁ ⟶ X₃
f : X₂ ⟶ X₄
g : X₃ ⟶ X₄
h : IsPullback fst snd f g
P✝ : C
b : P✝ ⟶ ⋯.shortComplex'.X₁
hb : b ≫ ⋯.shortComplex'.f = 0
⊢ b = 0
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
hm : n + 1 = m
hp : m + 1 = p
s : Cofork ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯)) 0
l : (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt ⟶ s.pt
hl : Cofork.π (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯) ≫ l = s.π
x : ↑(CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt
⊢ (AddCommGrpCat.Hom.hom l) x =
    (AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (CohomologyClass.descAddMonoidHom (AddCommGrpCat.Hom.hom s.π) ⋯))) x

Tactic:
obtain ⟨y, rfl⟩ := x.mk_surjective

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
hm : n + 1 = m
hp : m + 1 = p
s : Cofork ((Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯)) 0
l : (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯).pt ⟶ s.pt
hl : Cofork.π (CokernelCofork.ofπ (AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m)) ⋯) ≫ l = s.π
y : Cocycle K L m
⊢ (AddCommGrpCat.Hom.hom l) (CohomologyClass.mk y) =
    (AddCommGrpCat.Hom.hom (AddCommGrpCat.ofHom (CohomologyClass.descAddMonoidHom (AddCommGrpCat.Hom.hom s.π) ⋯)))
      (CohomologyClass.mk y)
Module: Mathlib.Algebra.Homology.BifunctorAssociator

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₂₃ : Type u_4
C₃ : Type u_5
C₄ : Type u_6
inst✝²² : Category.{v_1, u_1} C₁
inst✝²¹ : Category.{v_2, u_2} C₂
inst✝²⁰ : Category.{v_3, u_5} C₃
inst✝¹⁹ : Category.{v_4, u_6} C₄
inst✝¹⁸ : Category.{v_6, u_4} C₂₃
inst✝¹⁷ : HasZeroMorphisms C₁
inst✝¹⁶ : HasZeroMorphisms C₂
inst✝¹⁵ : HasZeroMorphisms C₃
inst✝¹⁴ : Preadditive C₂₃
inst✝¹³ : Preadditive C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝¹² : G₂₃.PreservesZeroMorphisms
inst✝¹¹ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁰ : F.PreservesZeroMorphisms
inst✝⁹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₂₃ : Type u_11
ι₄ : Type u_12
inst✝⁸ : DecidableEq ι₄
c₁ : ComplexShape ι₁
c₂ : ComplexShape ι₂
c₃ : ComplexShape ι₃
K₁ : HomologicalComplex C₁ c₁
K₂ : HomologicalComplex C₂ c₂
K₃ : HomologicalComplex C₃ c₃
c₁₂ : ComplexShape ι₁₂
c₂₃ : ComplexShape ι₂₃
c₄ : ComplexShape ι₄
inst✝⁷ : TotalComplexShape c₁ c₂ c₁₂
inst✝⁶ : TotalComplexShape c₁₂ c₃ c₄
inst✝⁵ : TotalComplexShape c₂ c₃ c₂₃
inst✝⁴ : TotalComplexShape c₁ c₂₃ c₄
inst✝³ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝² : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝¹ : DecidableEq ι₂₃
inst✝ : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : ¬c₂.Rel i₂ (c₂.next i₂)
⊢ (c₁.ε₂ c₂₃ c₄ (i₁, c₂.π c₃ c₂₃ (i₂, i₃)) * c₂.ε₁ c₃ c₂₃ (i₂, i₃)) •
      (F.obj (K₁.X i₁)).map ((G₂₃.map (K₂.d i₂ (c₂.next i₂))).app (K₃.X i₃)) ≫
        ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ (c₂.next i₂) i₃ j =
    0

Tactic:
rw [shape _ _ _ h, Functor.map_zero, zero_app, Functor.map_zero, zero_comp, smul_zero]

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

Goal state before:
pp: ι : 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✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i' j' : ι'
hij' : ¬c'.Rel j' i'
⊢ extend.hom e h.hom i' j' = 0

Tactic:
by_cases hi' : ∃ i, e.f i = i'
    · obtain ⟨i, rfl⟩ := hi'
      by_cases hj' : ∃ j, e.f j = j'
      · obtain ⟨j, rfl⟩ := hj'
        rw [extend.hom_eq _ _ rfl rfl, h.zero _ _ (by rwa [← e.rel_iff]),
          zero_comp, comp_zero]
      · exact extend.hom_eq_zero₂ _ _ _ _ (by tauto)
    · exact extend.hom_eq_zero₁ _ _ _ _ (by tauto)

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

Goal state before:
pp: case refine_1
C : Type u
inst✝⁹ : Category.{v, u} C
D : Type u'
inst✝⁸ : Category.{v', u'} D
P : ObjectProperty C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : P.IsTriangulated
inst✝¹ : IsTriangulated C
X : C
hX : P.trW.isColocal X
L : C ⥤ D
inst✝ : L.IsLocalization P.trW
Y : C
f₁ f₂ : X ⟶ Y
hf : L.map f₁ = L.map f₂
⊢ f₁ = f₂

Tactic:
rw [MorphismProperty.map_eq_iff_postcomp L P.trW] at hf
    obtain ⟨Z, s, hs, eq⟩ := hf
    exact (hX _ hs).1 eq

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (trivialCofibrations C).IsStableUnderCobaseChange

Tactic:
← fibrations_llp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (fibrations C).llp.IsStableUnderCobaseChange
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (trivialCofibrations C).IsMultiplicative

Tactic:
← fibrations_llp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
⊢ (fibrations C).llp.IsMultiplicative
Module: Mathlib.AlgebraicTopology.ModelCategory.Instances

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
J : Type w
⊢ (trivialCofibrations C).IsStableUnderCoproductsOfShape J

Tactic:
← fibrations_llp

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : CategoryWithWeakEquivalences C
inst✝² : CategoryWithCofibrations C
inst✝¹ : CategoryWithFibrations C
inst✝ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
J : Type w
⊢ (fibrations C).llp.IsStableUnderCoproductsOfShape J
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : CategoryWithWeakEquivalences C
P : Cylinder X
inst✝¹ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝ : (weakEquivalences C).ContainsIdentities
f₀ f₁ : X ⟶ Y
h : P.LeftHomotopy f₀ f₁
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁

Tactic:
induction h
  grind [weakEquivalence_precomp_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X Y : C
φ : X ⟶ Y
H : ∃ f, f.hom₂ = φ
⊢ (triangle t n X).mor₁ ≫ φ = (triangle t n X).mor₁ ≫ H.choose.hom₂

Tactic:
H.choose_spec

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X Y : C
φ : X ⟶ Y
H : ∃ f, f.hom₂ = φ
⊢ (triangle t n X).mor₁ ≫ φ = (triangle t n X).mor₁ ≫ φ
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X Y : C
φ : X ⟶ Y
H : ∃ f, f.hom₂ = φ
⊢ H.choose.hom₂ ≫ (triangle t n Y).mor₂ = φ ≫ (triangle t n Y).mor₂

Tactic:
H.choose_spec

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X Y : C
φ : X ⟶ Y
H : ∃ f, f.hom₂ = φ
⊢ φ ≫ (triangle t n Y).mor₂ = φ ≫ (triangle t n Y).mor₂
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
a b : ℤ
h : a ≤ b
H : ∃ f, f.hom₂ = 𝟙 (triangle t a A).obj₂
⊢ (triangle t a A).mor₁ ≫ 𝟙 (triangle t a A).obj₂ = (triangle t a A).mor₁ ≫ H.choose.hom₂

Tactic:
H.choose_spec

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
a b : ℤ
h : a ≤ b
H : ∃ f, f.hom₂ = 𝟙 (triangle t a A).obj₂
⊢ (triangle t a A).mor₁ ≫ 𝟙 (triangle t a A).obj₂ = (triangle t a A).mor₁ ≫ 𝟙 (triangle t a A).obj₂
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
a b : ℤ
h : a ≤ b
H : ∃ f, f.hom₂ = 𝟙 (triangle t a A).obj₂
⊢ H.choose.hom₂ ≫ (triangle t b A).mor₂ = 𝟙 (triangle t a A).obj₂ ≫ (triangle t b A).mor₂

Tactic:
H.choose_spec

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X Y : C
φ : X ⟶ Y
A : C
a b : ℤ
h : a ≤ b
H : ∃ f, f.hom₂ = 𝟙 (triangle t a A).obj₂
⊢ 𝟙 (triangle t a A).obj₂ ≫ (triangle t b A).mor₂ = 𝟙 (triangle t a A).obj₂ ≫ (triangle t b A).mor₂
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
x✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ (t.truncLT n).map (x✝¹ + x✝) = (t.truncLT n).map x✝¹ + (t.truncLT n).map x✝

Tactic:
by
    dsimp only [truncLT, Functor.comp_map]
    rw [Functor.map_add]
    dsimp

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: case mp
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X : C
h : t.IsGE X n
e : (contractibleTriangle X).invRotate ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = 𝟙 X
⊢ IsIso ((t.truncGEπ n).app X)

Tactic:
have : (truncGEπ t n).app X = e.hom.hom₃ := by
      have := e.hom.comm₂
      dsimp at this
      rw [← cancel_epi e.hom.hom₂, ← this, he]

Goal state after:
case mp
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X : C
h : t.IsGE X n
e : (contractibleTriangle X).invRotate ≅ (t.triangleLTGE n).obj X
he : e.hom.hom₂ = 𝟙 X
this : (t.truncGEπ n).app X = e.hom.hom₃
⊢ IsIso ((t.truncGEπ n).app X)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsLE T.obj₁ n
h₃ : t.IsLE T.obj₃ n
⊢ ∀ (Y : C) (f : T.obj₂ ⟶ Y), t.IsGE Y (n + 1) → f = 0

Tactic:
intro Y

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsLE T.obj₁ n
h₃ : t.IsLE T.obj₃ n
Y : C
⊢ ∀ (f : T.obj₂ ⟶ Y), t.IsGE Y (n + 1) → f = 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsGE T.obj₁ n
h₃ : t.IsGE T.obj₃ n
⊢ ∀ (Y : C) (f : Y ⟶ T.obj₂), t.IsLE Y (n - 1) → f = 0

Tactic:
intro Y

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
T : Triangle C
hT : T ∈ distinguishedTriangles
n : ℤ
h₁ : t.IsGE T.obj₁ n
h₃ : t.IsGE T.obj₃ n
Y : C
⊢ ∀ (f : Y ⟶ T.obj₂), t.IsLE Y (n - 1) → f = 0
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
⊢ IsIso ((t.truncGE n₁).map g) ↔
    ∃ X f h, ∃ (_ : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles), t.IsLE X n₀

Tactic:
refine ⟨fun hf ↦ ?_, fun ⟨X, f, h, mem, _⟩ ↦ ?_⟩
  · refine ⟨_, (t.truncLTι n₁).app Y, inv ((t.truncGE n₁).map g) ≫ (t.truncGEδLT n₁).app Y,
      isomorphic_distinguished _ (t.triangleLTGE_distinguished n₁ Y) _ ?_,
      by subst hn; infer_instance⟩
    exact Iso.symm (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
      (asIso ((t.truncGE n₁).map g)) (by simp) (by simp) (by simp))
  · obtain ⟨e, he⟩ :=
      t.triangle_iso_exists (t.triangleLTGE_distinguished n₁ Y) mem (Iso.refl _) n₀ n₁
        (by dsimp; rw [← hn]; infer_instance) (by dsimp; infer_instance)
        (by dsimp; infer_instance) (by dsimp; infer_instance)
    suffices ((t.truncGE n₁).map g) = e.hom.hom₃ by rw [this]; infer_instance
    exact t.from_truncGE_obj_ext (Eq.trans (by cat_disch) e.hom.comm₂.symm)

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
n m : ℤ
hnm : n + 1 = m
⊢ i.f n ≫ (↑(cocycle₁' sq hsq)).v n m hnm = 0

Tactic:
have fac_left (k : ℤ) := (hsq k).fac_left
  dsimp at fac_left
  simp [cocycle₁', fac_left, reassoc_of% fac_left]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
x✝¹ x✝ : X ⟶ Y
h : LeftHomotopyRel x✝¹ x✝
⊢ RightHomotopyClass.mk x✝¹ = RightHomotopyClass.mk x✝

Tactic:
RightHomotopyClass.mk_eq_mk_iff

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
inst✝¹ : IsCofibrant X
inst✝ : IsFibrant Y
x✝¹ x✝ : X ⟶ Y
h : LeftHomotopyRel x✝¹ x✝
⊢ RightHomotopyRel x✝¹ x✝
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n : ℤ
⊢ homologyMap f n ≫ homologyMap (α f n) n = 0

Tactic:
← homologyMap_comp,

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝ : EnoughInjectives C
n : ℤ
⊢ homologyMap (f ≫ α f n) n = 0
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : Mono f
⊢ homologyMap f n ≫ homologyMap (cokernel.π f) n = 0

Tactic:
← homologyMap_comp,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : Mono f
⊢ homologyMap (f ≫ cokernel.π f) n = 0
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : Mono f
T : ShortComplex C :=
  { X₁ := homology K n, X₂ := homology L n, X₃ := homology (cokernel f) n, f := homologyMap f n,
    g := homologyMap (cokernel.π f) n, zero := ⋯ }
⊢ homologyMap (α f n) n = T.g ≫ homologyMap ((cokernel f).πTruncGE n ≫ p f n) n

Tactic:
← homologyMap_comp,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : Mono f
T : ShortComplex C :=
  { X₁ := homology K n, X₂ := homology L n, X₃ := homology (cokernel f) n, f := homologyMap f n,
    g := homologyMap (cokernel.π f) n, zero := ⋯ }
⊢ homologyMap (α f n) n = homologyMap (cokernel.π f ≫ (cokernel f).πTruncGE n ≫ p f n) n
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: case mp
C₁ : Type u_1
C₂ : Type u_2
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_4, u_4} D₁
inst✝ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
⊢ w.GuitartExact

Tactic:
have : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom := by
      ext X₁
      simp only [Functor.comp_obj, whiskerVertical_app, assoc, Iso.hom_inv_id_app_assoc,
        ← B.map_comp, Iso.hom_inv_id_app, B.map_id, comp_id]

Goal state after:
case mp
C₁ : Type u_1
C₂ : Type u_2
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_4, u_4} D₁
inst✝ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
this : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom
⊢ w.GuitartExact