mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasCoproduct A
inst✝ : Limits.HasCoproduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X Y : C
p : X ⟶ Y
⊢ T p → HasLiftingProperty (Limits.Sigma.map f) p

Tactic:
hp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasCoproduct A
inst✝ : Limits.HasCoproduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X Y : C
p : X ⟶ Y
hp : T p
⊢ HasLiftingProperty (Limits.Sigma.map f) p
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasProduct A
inst✝ : Limits.HasProduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X Y : C
p : X ⟶ Y
⊢ T p → HasLiftingProperty p (Limits.Pi.map f)

Tactic:
hp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasProduct A
inst✝ : Limits.HasProduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X Y : C
p : X ⟶ Y
hp : T p
⊢ HasLiftingProperty p (Limits.Pi.map f)
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
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
h₁ : cofibrations C f₁
h₂ : cofibrations C f₂
inst✝¹ : HasBinaryCoproduct X₁ X₂
inst✝ : HasBinaryCoproduct Y₁ Y₂
⊢ (cofibrations C).functorCategory (Discrete WalkingPair) (mapPair f₁ f₂)

Tactic:
rintro (_ | _)

Goal state after:
case left
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
h₁ : cofibrations C f₁
h₂ : cofibrations C f₂
inst✝¹ : HasBinaryCoproduct X₁ X₂
inst✝ : HasBinaryCoproduct Y₁ Y₂
⊢ cofibrations C ((mapPair f₁ f₂).app { as := WalkingPair.left })

case right
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
h₁ : cofibrations C f₁
h₂ : cofibrations C f₂
inst✝¹ : HasBinaryCoproduct X₁ X₂
inst✝ : HasBinaryCoproduct Y₁ Y₂
⊢ cofibrations C ((mapPair f₁ f₂).app { as := WalkingPair.right })
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
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : HasBinaryProduct Y₁ Y₂
⊢ (fibrations C).functorCategory (Discrete WalkingPair) (mapPair f₁ f₂)

Tactic:
rintro (_ | _)

Goal state after:
case left
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : HasBinaryProduct Y₁ Y₂
⊢ fibrations C ((mapPair f₁ f₂).app { as := WalkingPair.left })

case right
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : CategoryWithFibrations C
X₁ X₂ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
inst✝² : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
h₁ : fibrations C f₁
h₂ : fibrations C f₂
inst✝¹ : HasBinaryProduct X₁ X₂
inst✝ : HasBinaryProduct Y₁ Y₂
⊢ fibrations C ((mapPair f₁ f₂).app { as := WalkingPair.right })
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

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✝⁷ : Preadditive D
A : Type u_3
inst✝⁶ : Category.{v_3, u_3} A
inst✝⁵ : Abelian A
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : HasZeroObject C
inst✝² : HasBinaryBiproducts C
inst✝¹ : HasZeroObject D
inst✝ : HasBinaryBiproducts D
⊢ F.mapHomotopyCategoryPlus.IsTriangulated

Tactic:
dsimp only [mapHomotopyCategoryPlus]
  infer_instance

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

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D₁
inst✝¹ : Category.{v_4, u_4} D₂
A B : ObjectProperty C
inst✝ : A.IsVerdierRightLocalizing B
X✝ Y✝ : Cᵒᵖ
f : X✝ ⟶ Y✝
hX : A.op X✝
hY : B.op Y✝
⊢ ∃ Z a b, A.op Z ∧ B.op Z ∧ a ≫ b = f

Tactic:
obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac f.unop hY hX
    exact ⟨_, b.op, a.op, h₁, h₂, Quiver.Hom.unop_inj fac⟩

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

Goal state before:
pp: C : Type u_1
D : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
inst✝² : Category.{v_3, u_3} D₁
inst✝¹ : Category.{v_4, u_4} D₂
A B : ObjectProperty Cᵒᵖ
inst✝ : A.IsVerdierRightLocalizing B
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hX : A.unop X✝
hY : B.unop Y✝
⊢ ∃ Z a b, A.unop Z ∧ B.unop Z ∧ a ≫ b = f

Tactic:
by
    obtain ⟨Z, a, b, h₁, h₂, fac⟩ := IsVerdierRightLocalizing.fac f.op hY hX
    exact ⟨_, b.unop, a.unop, h₁, h₂, Quiver.Hom.op_inj fac⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹² : Category.{v_1, u_1} C
inst✝¹¹ : Preadditive C
inst✝¹⁰ : HasZeroObject C
inst✝⁹ : HasShift C ℤ
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
P✝ : ObjectProperty C
t✝ : TStructure C
inst✝⁶ : P✝.IsTriangulated
h : P✝.HasInducedTStructure t✝
P P' : ObjectProperty C
inst✝⁵ : P.IsTriangulated
inst✝⁴ : P'.IsTriangulated
t : TStructure C
inst✝³ : P.HasInducedTStructure t
inst✝² : P'.HasInducedTStructure t
inst✝¹ : P.IsClosedUnderIsomorphisms
inst✝ : P'.IsClosedUnderIsomorphisms
⊢ ∀ (X : C), (P ⊓ P') X → ∀ (n : ℤ), (P ⊓ P') ((t.truncLE n).obj X) ∧ (P ⊓ P') ((t.truncGE n).obj X)

Tactic:
rintro X ⟨hX, hX'⟩ n
    exact
      ⟨⟨(P.mem_of_hasInductedTStructure t _ (t.triangleLEGE_distinguished n _ rfl X) n _ rfl
          (by dsimp; infer_instance) hX (by dsimp; infer_instance)).1,
        (P'.mem_of_hasInductedTStructure t _ (t.triangleLEGE_distinguished n _ rfl X) n _ rfl
          (by dsimp; infer_instance) hX' (by dsimp; infer_instance)).1⟩,
          ⟨(P.mem_of_hasInductedTStructure t _ (t.triangleLEGE_distinguished (n - 1) n (by lia) X)
          (n - 1) n (by lia) (by dsimp; infer_instance) hX (by dsimp; infer_instance)).2,
        (P'.mem_of_hasInductedTStructure t _ (t.triangleLEGE_distinguished (n - 1) n (by lia) X)
          (n - 1) n (by lia) (by dsimp; infer_instance) hX' (by dsimp; infer_instance)).2⟩⟩

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✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ (t.truncGE n).map (x✝¹ + x✝) = (t.truncGE n).map x✝¹ + (t.truncGE n).map x✝

Tactic:
dsimp only [truncGE, Functor.comp_map]

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✝³ x✝² : C
x✝¹ x✝ : x✝³ ⟶ x✝²
⊢ Triangle.π₃.map ((TruncAux.triangleFunctor t n).map (x✝¹ + x✝)) =
    Triangle.π₃.map ((TruncAux.triangleFunctor t n).map x✝¹) + Triangle.π₃.map ((TruncAux.triangleFunctor t n).map x✝)
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝² : IsCofibrant X
inst✝¹ : IsFibrant Y
h : RightHomotopyRel f g
P : PathObject Y
inst✝ : P.IsGood
⊢ LeftHomotopyRel f g

Tactic:
leftHomotopyRel_iff_rightHomotopyRel

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

Goal state before:
pp: case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi✝ : i ≤ n₀
hi : i < n₀
⊢ QuasiIsoAt (π K L n₁) i

Tactic:
rw [quasiIsoAt_iff' _ (i - 1) i (i + 1) (by simp) (by simp)]

Goal state after:
case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
inst✝ : EnoughInjectives C
n₀ n₁ : ℤ
hn₁ : n₀ + 1 = n₁
i : ℤ
hi✝ : i ≤ n₀
hi : i < n₀
⊢ ShortComplex.QuasiIso ((shortComplexFunctor' C (ComplexShape.up ℤ) (i - 1) i (i + 1)).map (π K L n₁))
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : FibrantObject C
f : X ⟶ Y
⊢ weakEquivalences (HoCat C) (toHoCat.map f) ↔ weakEquivalences (FibrantObject C) f

Tactic:
apply MorphismProperty.quotient_iff

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
n : ℤ
hf : ∀ i < n, QuasiIsoAt f i
inst✝¹ : Mono f
inst✝ : Mono (homologyMap f n)
hq : n ≤ n
this✝¹ : Mono (homologyMap (π f n) n)
this✝ : Mono (homologyMap (mappingCocone.triangle (α f n)).mor₁ n)
h₁ : IsLimit (KernelFork.ofι (homologyShortComplex f n).f ⋯)
h₂ :
  IsLimit
    (KernelFork.ofι
      { X₁ := homology (mappingCocone.triangle (α f n)).obj₁ n, X₂ := homology (mappingCocone.triangle (α f n)).obj₂ n,
          X₃ := homology (mappingCocone.triangle (α f n)).obj₃ n,
          f := homologyMap (mappingCocone.triangle (α f n)).mor₁ n,
          g := homologyMap (mappingCocone.triangle (α f n)).mor₂ n, zero := ⋯ }.f
      ⋯)
this : homologyMap (ι f n) n = (h₁.conePointUniqueUpToIso h₂).hom
⊢ QuasiIsoAt (ι f n) n

Tactic:
quasiIsoAt_iff_isIso_homologyMap,

Goal state after:
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
this✝¹ : Mono (homologyMap (π f n) n)
this✝ : Mono (homologyMap (mappingCocone.triangle (α f n)).mor₁ n)
h₁ : IsLimit (KernelFork.ofι (homologyShortComplex f n).f ⋯)
h₂ :
  IsLimit
    (KernelFork.ofι
      { X₁ := homology (mappingCocone.triangle (α f n)).obj₁ n, X₂ := homology (mappingCocone.triangle (α f n)).obj₂ n,
          X₃ := homology (mappingCocone.triangle (α f n)).obj₃ n,
          f := homologyMap (mappingCocone.triangle (α f n)).mor₁ n,
          g := homologyMap (mappingCocone.triangle (α f n)).mor₂ n, zero := ⋯ }.f
      ⋯)
this : homologyMap (ι f n) n = (h₁.conePointUniqueUpToIso h₂).hom
⊢ IsIso (homologyMap (ι f n) n)
Module: Mathlib.CategoryTheory.GuitartExact.Quotient

Goal state before:
pp: C₀ : Type u_1
C : Type u_2
H₀ : Type u_3
H✝ : Type u_4
inst✝⁶ : Category.{v_1, u_1} C₀
inst✝⁵ : Category.{v_2, u_2} C
inst✝⁴ : Category.{v_3, u_3} H₀
inst✝³ : Category.{v_4, u_4} H✝
T : C₀ ⥤ H₀
L : C₀ ⥤ C
R : H₀ ⥤ H✝
B : C ⥤ H✝
inst✝² : T.EssSurj
inst✝¹ : T.Full
inst✝ : B.Full
e : T ⋙ R ≅ L ⋙ B
he :
  ∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁)
Y₀ : H₀
X : C
g : R.obj Y₀ ⟶ B.obj X
X₀ : C₀ := T.objPreimage Y₀
e₀ : T.obj X₀ ≅ Y₀ := T.objObjPreimageIso Y₀
S : Type (max 0 v_2) := { f // B.map f = e.inv.app X₀ ≫ R.map e₀.hom ≫ g }
Z : S → CostructuredArrowDownwards e.hom g := fun s ↦ CostructuredArrowDownwards.mk e.hom g X₀ e₀.inv ↑s ⋯
this : Nonempty (CostructuredArrowDownwards e.hom g)
A₀ A₁ : CostructuredArrowDownwards e.hom g
H : ∀ (A : CostructuredArrowDownwards e.hom g), ∃ s, Nonempty (Z s ⟶ A)
s₀ : S
f₀ : Z s₀ ⟶ A₀
s₁ : S
f₁ : Z s₁ ⟶ A₁
⊢ B.map ↑s₀ = B.map ↑s₁

Tactic:
by simp [s₀.property, s₁.property]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝¹⁰ : Category.{v₁, u₁} C₁
inst✝⁹ : Category.{v₂, u₂} C₂
inst✝⁸ : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₄, u₄} D₁
inst✝⁶ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
F : C₂ ⥤ H
F₁ : D₁ ⥤ H
α₁ : Φ.functor ⋙ F ⟶ L₁ ⋙ F₁
F₂ : D₂ ⥤ H
α₂ : F ⟶ L₂ ⋙ F₂
inst✝³ : F₁.IsRightDerivedFunctor α₁ W₁
inst✝² : Φ.IsRightDerivabilityStructure
inst✝¹ : (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst✝ : F₂.IsRightDerivedFunctor α₂ W₂
this : F.HasPointwiseRightDerivedFunctor W₂
⊢ IsIso
    (F₁.rightDerivedDesc α₁ W₁ (Φ.localizedFunctor L₁ L₂ ⋙ F₂)
      (Φ.functor.whiskerLeft α₂ ≫
        (Φ.functor.associator L₂ F₂).inv ≫
          whiskerRight (CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom F₂ ≫
            (L₁.associator (Φ.localizedFunctor L₁ L₂) F₂).hom))

Tactic:
← isRightDerivedFunctor_iff_isIso_rightDerivedDesc,

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
H : Type u₃
inst✝¹⁰ : Category.{v₁, u₁} C₁
inst✝⁹ : Category.{v₂, u₂} C₂
inst✝⁸ : Category.{v₃, u₃} H
D₁ : Type u₄
D₂ : Type u₅
inst✝⁷ : Category.{v₄, u₄} D₁
inst✝⁶ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
inst✝⁵ : L₁.IsLocalization W₁
inst✝⁴ : L₂.IsLocalization W₂
F : C₂ ⥤ H
F₁ : D₁ ⥤ H
α₁ : Φ.functor ⋙ F ⟶ L₁ ⋙ F₁
F₂ : D₂ ⥤ H
α₂ : F ⟶ L₂ ⋙ F₂
inst✝³ : F₁.IsRightDerivedFunctor α₁ W₁
inst✝² : Φ.IsRightDerivabilityStructure
inst✝¹ : (Φ.functor ⋙ F).HasPointwiseRightDerivedFunctor W₁
inst✝ : F₂.IsRightDerivedFunctor α₂ W₂
this : F.HasPointwiseRightDerivedFunctor W₂
⊢ (Φ.localizedFunctor L₁ L₂ ⋙ F₂).IsRightDerivedFunctor
    (Φ.functor.whiskerLeft α₂ ≫
      (Φ.functor.associator L₂ F₂).inv ≫
        whiskerRight (CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom F₂ ≫
          (L₁.associator (Φ.localizedFunctor L₁ L₂) F₂).hom)
    W₁
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
X Y : DifferentialObject S C
f : X ≅ Y
⊢ f.inv.f ≫ f.hom.f = 𝟙 Y.obj

Tactic:
by rw [← comp_f, Iso.inv_hom_id, id_f]

Goal state after:
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: case a.a
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 ≫ (shiftFunctor C 1).map X.d)

pp: case a.a
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
| η.app ((shiftFunctor C 1).obj X.obj)

pp: case a
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
| (shiftFunctor D 1).map (η.app X.obj)

Tactic:
X.d_squared,

Goal state after:
case a.a
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 0

case a.a
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
| η.app ((shiftFunctor C 1).obj X.obj)

case a
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
| (shiftFunctor D 1).map (η.app X.obj)
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ (CategoryTheory.shiftFunctor C n).map (X.d ≫ (CategoryTheory.shiftFunctor C 1).map X.d) ≫
      (shiftComm ((CategoryTheory.shiftFunctor C 1).obj X.obj) 1 n).hom ≫
        (CategoryTheory.shiftFunctor C 1).map (shiftComm X.obj 1 n).hom =
    0

Tactic:
X.d_squared,

Goal state after:
S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
n : S
X : DifferentialObject S C
⊢ (CategoryTheory.shiftFunctor C n).map 0 ≫
      (shiftComm ((CategoryTheory.shiftFunctor C 1).obj X.obj) 1 n).hom ≫
        (CategoryTheory.shiftFunctor C 1).map (shiftComm X.obj 1 n).hom =
    0
Module: Mathlib.CategoryTheory.DifferentialObject

Goal state before:
pp: S : Type u_1
inst✝³ : AddCommGroupWithOne S
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasShift C S
⊢ shiftFunctor C 0 ≅ 𝟭 (DifferentialObject S C)

Tactic:
refine NatIso.ofComponents (fun X => mkIso ((shiftFunctorZero C S).app X.obj) ?_) (fun f => ?_)
  · erw [← NatTrans.naturality]
    dsimp
    simp only [shiftFunctorZero_hom_app_shift, Category.assoc]
  · cat_disch

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.app P.complex ≫
      (F.mapHomotopyCategory (ComplexShape.down ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) ≫
        (F.mapHomotopyCategory (ComplexShape.down ℕ)).map Q.iso.inv =
    (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) ≫
      (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.app Q.complex ≫
        (F.mapHomotopyCategory (ComplexShape.down ℕ)).map Q.iso.inv

Tactic:
erw [(F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.naturality_assoc]

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u_1
inst✝⁴ : Category.{v_1, u_1} D
inst✝³ : Abelian C
inst✝² : HasProjectiveResolutions C
inst✝¹ : Abelian D
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
φ : P.complex ⟶ Q.complex
comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
F : C ⥤ D
inst✝ : F.Additive
⊢ (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.app P.complex ≫
      (F.mapHomotopyCategory (ComplexShape.down ℕ)).map ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ) ≫
        (F.mapHomotopyCategory (ComplexShape.down ℕ)).map Q.iso.inv =
    (F.mapHomotopyCategoryFactors (ComplexShape.down ℕ)).inv.app P.complex ≫
      (HomotopyCategory.quotient C (ComplexShape.down ℕ) ⋙ F.mapHomotopyCategory (ComplexShape.down ℕ)).map φ ≫
        (F.mapHomotopyCategory (ComplexShape.down ℕ)).map Q.iso.inv
Module: Mathlib.CategoryTheory.Abelian.LeftDerived

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u_1
inst✝⁵ : Category.{v_1, u_1} D
inst✝⁴ : Abelian C
inst✝³ : HasProjectiveResolutions C
inst✝² : Abelian D
F : C ⥤ D
inst✝¹ : F.Additive
inst✝ : PreservesFiniteColimits F
X : C
⊢ IsIso (F.fromLeftDerivedZero.app X)

Tactic:
by
  dsimp [Functor.fromLeftDerivedZero]
  infer_instance

Goal state after:
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
K : HomologicalComplex C c
inst✝¹ : DecidableEq I
inst✝ : ∀ (X₂ : C), PreservesColimit (Functor.empty C) ((curriedTensor C).flip.obj X₂)
i : I
⊢ K.leftUnitor'.inv i =
    (λ_ (K.X i)).inv ≫ (singleObjXSelf c 0 (𝟙_ C)).inv ▷ K.X i ≫ (tensorUnit C c).ιTensorObj K 0 i i ⋯

Tactic:
dsimp [leftUnitor']
  rw [GradedObject.Monoidal.leftUnitor_inv_apply, assoc, assoc, Iso.cancel_iso_inv_left,
    GradedObject.Monoidal.ι_tensorHom]
  dsimp
  rw [tensorHom_id, ← comp_whiskerRight_assoc]
  congr 2
  rw [← cancel_epi (GradedObject.Monoidal.tensorUnit₀ (I := I)).hom, Iso.hom_inv_id_assoc]
  dsimp [tensorUnitIso]
  rw [dif_pos rfl]
  rfl

Goal state after:
Module: Mathlib.Algebra.Homology.SpectralObject.EpiMono

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ IsIso (X.map f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ hn₂ hn₃)

Tactic:
apply ShortComplex.isIso_homologyMap_of_epi_of_isIso_of_mono'

Goal state after:
case h₁
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Epi (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯).τ₁

case h₂
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ IsIso (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯).τ₂

case h₃
C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} ι
X : SpectralObject C ι
i₀ i₁ i₂ i₃ i₄ : ι
f₁ : i₀ ⟶ i₁
f₂ : i₁ ⟶ i₂
f₃ : i₂ ⟶ i₃
f₄ : i₃ ⟶ i₄
f₃₄ : i₂ ⟶ i₄
h₃₄ : f₃ ≫ f₄ = f₃₄
n₁ n₂ n₃ : ℤ
h : (X.H n₁).map (twoδ₁Toδ₀ f₃ f₄ f₃₄ h₃₄) = 0
hn₂ : n₁ + 1 = n₂
hn₃ : n₂ + 1 = n₃
⊢ Mono (X.shortComplexMap f₁ f₂ f₃ f₁ f₂ f₃₄ (fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄) n₁ n₂ n₃ ⋯ ⋯).τ₃