mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
⊢ w.GuitartExact

Tactic:
let : CatCommSq H₂ eL.functor eR.functor H₃ := ⟨w'⟩

Goal state after:
case mp
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
⊢ w.GuitartExact
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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
q : ℤ
hq : q ≤ n
⊢ QuasiIsoAt (ι f n) q

Tactic:
obtain hq | rfl := hq.lt_or_eq'

Goal state after:
case inl
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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
q : ℤ
hq✝ : q ≤ n
hq : q < n
⊢ QuasiIsoAt (ι f n) q

case inr
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 : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
⊢ QuasiIsoAt (ι f n) n
Module: Mathlib.CategoryTheory.GuitartExact.VerticalComposition

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
D₁ : Type u_4
D₂ : Type u_5
D₃ : Type u_6
inst✝⁵ : Category.{v_1, u_1} C₁
inst✝⁴ : Category.{v_2, u_2} C₂
inst✝³ : Category.{v_3, u_3} C₃
inst✝² : Category.{v_4, u_4} D₁
inst✝¹ : Category.{v_5, u_5} D₂
inst✝ : Category.{v_6, u_6} D₃
H₁ : C₁ ⥤ D₁
L₁ : C₁ ⥤ C₂
R₁ : D₁ ⥤ D₂
H₂ : C₂ ⥤ D₂
w : TwoSquare H₁ L₁ R₁ H₂
H₃ : C₃ ⥤ D₃
eL : C₂ ≌ C₃
eR : D₂ ≌ D₃
w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃
hww' : (w ≫ᵥ w'.hom).GuitartExact
this✝ : CatCommSq H₂ eL.functor eR.functor H₃ := { iso := w' }
hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w'
this : CatCommSq H₃ eL.inverse eR.inverse H₂ := (CatCommSq.vInvEquiv H₂ eL eR H₃) inferInstance
w'' : H₃ ⋙ eR.inverse ≅ eL.inverse ⋙ H₂ := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
  L₁.associator eL.functor eL.inverse ≪≫ L₁.isoWhiskerLeft eL.unitIso.symm ≪≫ L₁.rightUnitor
β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
  R₁.associator eR.functor eR.inverse ≪≫ R₁.isoWhiskerLeft eR.unitIso.symm ≪≫ R₁.rightUnitor
X₁ : C₁
⊢ w.natTrans.app X₁ =
    w.natTrans.app X₁ ≫
      eR.unit.app (H₂.obj (L₁.obj X₁)) ≫
        eR.inverse.map
            ((H₂ ⋙ eR.functor).map (eL.unit.app (L₁.obj X₁)) ≫
              (natTrans w'.hom).app ((eL.functor ⋙ eL.inverse).obj (L₁.obj X₁)) ≫
                w'.inv.app (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
          eR.unitIso.inv.app (H₂.obj (eL.inverse.obj (eL.functor.obj (L₁.obj X₁)))) ≫
            H₂.map (eL.unitIso.inv.app (L₁.obj X₁))

Tactic:
simp [← H₂.map_comp]

Goal state after:
Module: Mathlib.Algebra.Homology.Factorizations.CM5a

Goal state before:
pp: case inr
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
inst✝³ : EnoughInjectives C
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
q₁ q₂ : ℕ
hq : q₁ ≤ q₂
i : ℤ
hi : i ≤ n₀ + ↑q₁
this : ∀ {q₁ q₂ : ℕ} (hq : q₁ ≤ q₂), i ≤ n₀ + ↑q₁ → q₁ + 1 = q₂ → IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)
k : ℕ
hk : q₁ + k = q₂
⊢ IsIso (((functor f n₀).map (homOfLE hq).op).hom.h.f i)

Tactic:
induction k generalizing q₁ q₂ with

Goal state after:
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
inst✝² : Mono f
n₀ : ℤ
inst✝¹ : K.IsStrictlyGE (n₀ + 1)
inst✝ : L.IsStrictlyGE (n₀ + 1)
⊢ (mid f n₀).IsStrictlyGE (n₀ + 1)

Tactic:
rw [isStrictlyGE_iff]
  intro i hi
  have := isIso_midπ_f f n₀ 0 i
  exact (L.isZero_of_isStrictlyGE (n₀ + 1) i).of_iso (asIso ((midπ f n₀ 0).f i))

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

Goal state before:

Tactic:
Zigzag A₀ (Z s₀) := .of_inv f₀
    Zigzag (Z s₀) Z' := .of_hom <|
      CostructuredArrow.homMk (StructuredArrow.homMk P.i₀) (by simp [Z, Z', dsimp% h.h₀])
    Zigzag Z' (Z s₁) := .of_inv <|
      CostructuredArrow.homMk (StructuredArrow.homMk P.i₁) (by simp [Z, Z', dsimp% h.h₁])
    Zigzag (Z s₁) A₁ := .of_hom f₁

Goal state after:
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 : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
n : ℤ
inst✝ : K.IsStrictlyGE n
this : HasDerivedCategory C
L : CochainComplex C ℤ
i : K ⟶ L
w✝¹ : Mono i
w✝ : QuasiIso i
hL : ∀ (n : ℤ), Injective (L.X n)
h✝ : L.IsStrictlyGE (n - 1)
hK : (DerivedCategory.Q.obj K).IsGE n
⊢ (DerivedCategory.Q.obj L).IsGE n

Tactic:
exact DerivedCategory.TStructure.t.isGE_of_iso (asIso (DerivedCategory.Q.map i)) n

Goal state after:
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : F.HasPointwiseRightDerivedFunctor W
inst✝ : L.IsLocalization W
Y : D
this : L.EssSurj
⊢ L.HasPointwiseLeftKanExtensionAt F Y

Tactic:
← hasPointwiseLeftKanExtensionAt_iff_of_iso _ F (L.objObjPreimageIso Y),

Goal state after:
C : Type u₁
D : Type u₂
H : Type u₃
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₂, u₂} D
inst✝² : Category.{v₃, u₃} H
F : C ⥤ H
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : F.HasPointwiseRightDerivedFunctor W
inst✝ : L.IsLocalization W
Y : D
this : L.EssSurj
⊢ L.HasPointwiseLeftKanExtensionAt F (L.obj (L.objPreimage Y))
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

Goal state before:
pp: case mp
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
hF : F.HasPointwiseRightDerivedFunctor W₂
X₁ : C₁
⊢ (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctorAt W₁ X₁

Tactic:
rw [hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure]

Goal state after:
case mp
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} H
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
F : C₂ ⥤ H
inst✝ : Φ.IsRightDerivabilityStructure
hF : F.HasPointwiseRightDerivedFunctor W₂
X₁ : C₁
⊢ F.HasPointwiseRightDerivedFunctorAt W₂ (Φ.functor.obj X₁)
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
inst✝⁴ : HasDerivedCategory C
inst✝³ : HasDerivedCategory D
S : ShortComplex C
hS : S.ShortExact
F : C ⥤ D
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ (F.mapDerivedCategorySingleFunctor 0).inv.app S.X₃ ≫
      ShiftedHom.map hS.singleδ F.mapDerivedCategory ≫
        (shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁) =
    ⋯.singleδ

Tactic:
dsimp [ShiftedHom.map, ShortComplex.ShortExact.singleδ]

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
inst✝⁴ : HasDerivedCategory C
inst✝³ : HasDerivedCategory D
S : ShortComplex C
hS : S.ShortExact
F : C ⥤ D
inst✝² : F.Additive
inst✝¹ : PreservesFiniteLimits F
inst✝ : PreservesFiniteColimits F
⊢ (F.mapDerivedCategorySingleFunctor 0).inv.app S.X₃ ≫
      (F.mapDerivedCategory.map
            (((singleFunctorsPostcompQIso C).hom.hom 0).app S.X₃ ≫
              triangleOfSESδ ⋯ ≫
                (shiftFunctor (DerivedCategory C) 1).map (((singleFunctorsPostcompQIso C).inv.hom 0).app S.X₁)) ≫
          (Functor.commShiftIso F.mapDerivedCategory 1).hom.app ((singleFunctor C 0).obj S.X₁)) ≫
        (shiftFunctor (DerivedCategory D) 1).map ((F.mapDerivedCategorySingleFunctor 0).hom.app S.X₁) =
    ((singleFunctorsPostcompQIso D).hom.hom 0).app (F.obj S.X₃) ≫
      triangleOfSESδ ⋯ ≫
        (shiftFunctor (DerivedCategory D) 1).map (((singleFunctorsPostcompQIso D).inv.hom 0).app (F.obj S.X₁))
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : Abelian C
D : Type u'
inst✝⁶ : Category.{v', u'} D
inst✝⁵ : Abelian D
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
f : X ⟶ Y
⊢ ((F.mapCochainComplexSingleFunctor 0).app X).inv ≫
      (F.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism (ComplexShape.up ℤ)).functor.map
          ((CochainComplex.singleFunctor C 0).map f) ≫
        ((F.mapCochainComplexSingleFunctor 0).app Y).hom =
    (CochainComplex.singleFunctor D 0).map (F.map f)

Tactic:
simpa only [Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor,
    Functor.mapCochainComplexSingleFunctor, Iso.app_inv, Iso.app_hom] using! NatIso.naturality_1 _ f

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
⊢ (F.map X.d ≫ η.app X.obj) ≫ (shiftFunctor D 1).map (F.map X.d) ≫ (shiftFunctor D 1).map (η.app X.obj) = 0

Tactic:
← Functor.comp_map F (shiftFunctor D (1 : S))

Goal state after:
S : Type u_1
inst✝⁶ : AddMonoidWithOne S
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
inst✝³ : HasShift C S
D : Type u'
inst✝² : Category.{v', u'} D
inst✝¹ : HasZeroMorphisms D
inst✝ : HasShift D S
F : C ⥤ D
η : shiftFunctor C 1 ⋙ F ⟶ F ⋙ shiftFunctor D 1
hF : ∀ (c c' : C), F.map 0 = 0
X : DifferentialObject S C
⊢ (F.map X.d ≫ η.app X.obj) ≫ (F ⋙ shiftFunctor D 1).map X.d ≫ (shiftFunctor D 1).map (η.app X.obj) = 0
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
⊢ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫ K.d (n + 1) n =
    ((restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫
        h.d (Int.negSucc (n + 1)) (Int.negSucc n) ≫
          (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).inv) ≫
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom

Tactic:
d_negSucc

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K K' K'' : ChainComplex C ℕ
L L' L'' : CochainComplex C ℕ
h : ConnectData K L
h' : ConnectData K' L'
h'' : ConnectData K'' L''
n : ℕ
⊢ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫ K.d (n + 1) n =
    ((restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom ≫
        K.d (n + 1) n ≫ (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).inv) ≫
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasZeroObject C
X : C
K : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ X
n : ℤ
h : p + n = q
⊢ (toSingleEquiv h) (toSingleMk f h) = f

Tactic:
by
  simp [toSingleEquiv]

Goal state after:
Module: Mathlib.CategoryTheory.Preadditive.Projective.Resolution

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
P : ProjectiveResolution Z
⊢ ((pOpcycles P.complex 0 ≫
          P.complex.isoHomologyι₀.inv ≫ homologyMap P.π 0 ≫ (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z).hom) ≫
        (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z).inv) ≫
      ((single C (ComplexShape.down ℕ) 0).obj Z).homologyι 0 =
    (P.π.f 0 ≫ (singleObjHomologySelfIso (ComplexShape.down ℕ) 0 Z).inv) ≫
      ((single C (ComplexShape.down ℕ) 0).obj Z).homologyι 0

Tactic:
simp only [isoHomologyι₀_inv_naturality_assoc, p_opcyclesMap_assoc, single₀_obj_zero, assoc,
    Iso.hom_inv_id, comp_id, isoHomologyι_inv_hom_id, singleObjHomologySelfIso_inv_homologyι,
    singleObjOpcyclesSelfIso_hom, single₀ObjXSelf, Iso.refl_inv, id_comp]

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

Goal state before:
pp: case e'_3
C : Type u_1
ι : Type u_2
inst✝¹³ : Category.{v_1, u_1} C
inst✝¹² : Category.{v_2, u_2} ι
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
D : Type u_3
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : HasZeroObject D
inst✝⁴ : HasShift D ℤ
inst✝³ : Preadditive D
inst✝² : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝¹ : Pretriangulated D
X : SpectralObject C ι
ι' : Type u_4
inst✝ : Category.{?u.64, u_4} ι'
F : ι' ⥤ ι
D₁ D₂ : ComposableArrows ι' 2
f : D₁ ⟶ D₂
this :
  X.ω₁.map ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫ homMk₁ (F.map (f.app 1)) (F.map (f.app 2)) ⋯) ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₂) =
    X.ω₁.map (F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).hom ≫
      X.δ'.app ((F.mapComposableArrows 2).obj D₁) ≫
        (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))
⊢ (shiftFunctor C 1).map
      (X.ω₁.map
        ((F.mapComposableArrowsObjMk₁Iso (D₁.map (homOfLE ⋯))).inv ≫
          (F.mapComposableArrows 1).map (homMk₁ (f.app 0) (f.app 1) ⋯) ≫
            (F.mapComposableArrowsObjMk₁Iso (D₂.map (homOfLE ⋯))).hom)) =
    (shiftFunctor C 1).map (X.ω₁.map (homMk₁ (F.map (f.app 0)) (F.map (f.app 1)) ⋯))

Tactic:
congr 2; cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.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
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
a : R
⊢ cyclesMap' (a • φ) h₁ h₂ = a • cyclesMap' φ h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default
  simp only [(γ.smul a).cyclesMap'_eq, LeftHomologyMapData.smul_φK, γ.cyclesMap'_eq]

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.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
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ a • φ₁.τ₁ = S₁.f ≫ (a • h.h₁) + a • h.h₀ + a • φ₂.τ₁

Tactic:
rw [h.comm₁]

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
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
a : R
⊢ a • (S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁) = S₁.f ≫ (a • h.h₁) + a • h.h₀ + a • φ₂.τ₁
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ K₂ L₂ : HomologicalComplex C c
g : K₂ ⟶ L₂
⊢ (K₁ ◁ g).f = 𝟙 (K₁.X ⊗ K₂.X) ≫ K₁.X ◁ g.f

Tactic:
erw [id_comp]

Goal state after:
C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ K₂ L₂ : HomologicalComplex C c
g : K₂ ⟶ L₂
⊢ (K₁ ◁ g).f = K₁.X ◁ g.f
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ L₁ : HomologicalComplex C c
f : K₁ ⟶ L₁
K₂ : HomologicalComplex C c
⊢ (f ▷ K₂).f = 𝟙 (K₁.X ⊗ K₂.X) ≫ f.f ▷ K₂.X

Tactic:
erw [id_comp]

Goal state after:
C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ L₁ : HomologicalComplex C c
f : K₁ ⟶ L₁
K₂ : HomologicalComplex C c
⊢ (f ▷ K₂).f = f.f ▷ K₂.X
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ L₁ K₂ L₂ : HomologicalComplex C c
f : K₁ ⟶ L₁
g : K₂ ⟶ L₂
⊢ (f ⊗ₘ g).f = 𝟙 (K₁.X ⊗ K₂.X) ≫ (f.f ⊗ₘ g.f)

Tactic:
erw [id_comp]

Goal state after:
C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ L₁ K₂ L₂ : HomologicalComplex C c
f : K₁ ⟶ L₁
g : K₂ ⟶ L₂
⊢ (f ⊗ₘ g).f = f.f ⊗ₘ g.f
Module: Mathlib.Algebra.Homology.Monoidal

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ K₂ K₃ : HomologicalComplex C c
⊢ (α_ K₁ K₂ K₃).hom.f = 𝟙 ((K₁ ⊗ K₂).X ⊗ K₃.X) ≫ (α_ K₁.X K₂.X K₃.X).hom

Tactic:
erw [id_comp]

Goal state after:
C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : MonoidalCategory C
inst✝¹² : Preadditive C
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : (curriedTensor C).Additive
inst✝⁹ : ∀ (X₁ : C), ((curriedTensor C).obj X₁).Additive
I : Type u_2
inst✝⁸ : AddMonoid I
c : ComplexShape I
inst✝⁷ : c.TensorSigns
inst✝⁶ : ∀ (X₁ X₂ : GradedObject I C), X₁.HasTensor X₂
inst✝⁵ : ∀ (X₁ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).obj X₁)
inst✝⁴ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
inst✝³ : ∀ (X₁ X₂ X₃ X₄ : GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄
inst✝² : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝¹ : ∀ (X₁ X₂ X₃ : GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝ : DecidableEq I
K₁ K₂ K₃ : HomologicalComplex C c
⊢ (α_ K₁ K₂ K₃).hom.f = (α_ K₁.X K₂.X K₃.X).hom