mathlib-initiative/mathlib-tactics huggingface dataset:
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₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
hX : ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0
⊢ IsZero ((t.truncLT n₁).obj X)

Tactic:
IsZero.iff_id_eq_zero

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₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
hX : ∀ (Y : C) (f : Y ⟶ X), t.IsLE Y n₀ → f = 0
⊢ 𝟙 ((t.truncLT n₁).obj X) = 0
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
b : { obj := B, property := hB } ⟶ { obj := Y, property := hY }
i : { obj := A, property := hA }.obj ⟶ { obj := B, property := hB }.obj
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono (ObjectProperty.homMk i).hom
p : { obj := X, property := hX }.obj ⟶ { obj := Y, property := hY }.obj
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel (ObjectProperty.homMk p).hom
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : { obj := A, property := hA }.obj ⟶ { obj := X, property := hX }.obj
sq : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) b
⊢ sq.HasLift

Tactic:
obtain ⟨b, rfl⟩ := ObjectProperty.homMk_surjective b

Goal state after:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Abelian C
A : CochainComplex C ℤ
hA : CochainComplex.plus C A
B : CochainComplex C ℤ
hB : CochainComplex.plus C B
X : CochainComplex C ℤ
hX : CochainComplex.plus C X
Y : CochainComplex C ℤ
hY : CochainComplex.plus C Y
i : { obj := A, property := hA }.obj ⟶ { obj := B, property := hB }.obj
inst✝¹ : Mono (ObjectProperty.homMk i)
hi : Mono (ObjectProperty.homMk i).hom
p : { obj := X, property := hX }.obj ⟶ { obj := Y, property := hY }.obj
inst✝ : Fibration (ObjectProperty.homMk p)
hp : degreewiseEpiWithInjectiveKernel (ObjectProperty.homMk p).hom
hip : WeakEquivalence (ObjectProperty.homMk i) ∨ WeakEquivalence (ObjectProperty.homMk p)
t : { obj := A, property := hA }.obj ⟶ { obj := X, property := hX }.obj
b : { obj := B, property := hB }.obj ⟶ { obj := Y, property := hY }.obj
sq : CommSq (ObjectProperty.homMk t) (ObjectProperty.homMk i) (ObjectProperty.homMk p) (ObjectProperty.homMk b)
⊢ sq.HasLift
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
⊢ ∀ {X Y : Plus C} (f : X ⟶ Y), Nonempty ((trivialCofibrations (Plus C)).MapFactorizationData (fibrations (Plus C)) f)

Tactic:
intro ⟨K, n, hn⟩

Goal state after:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ ∀ {Y : Plus C} (f : { obj := K, property := ⋯ } ⟶ Y),
    Nonempty ((trivialCofibrations (Plus C)).MapFactorizationData (fibrations (Plus C)) f)
Module: Mathlib.Algebra.Homology.ModelCategory.Injective

Goal state before:
pp: C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
⊢ ∀ {X Y : Plus C} (f : X ⟶ Y), Nonempty ((cofibrations (Plus C)).MapFactorizationData (trivialFibrations (Plus C)) f)

Tactic:
intro ⟨K, n, hn⟩

Goal state after:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Abelian C
inst✝ : EnoughInjectives C
K : CochainComplex C ℤ
n : ℤ
hn : K.IsStrictlyGE n
⊢ ∀ {Y : Plus C} (f : { obj := K, property := ⋯ } ⟶ Y),
    Nonempty ((cofibrations (Plus C)).MapFactorizationData (trivialFibrations (Plus C)) f)
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)
i : ℤ
hi : autoParam (i < n₀ + 1) isStrictlyGE_iff._auto_1
this : IsIso ((midπ f n₀ 0).f i)
⊢ IsZero ((mid f n₀).X i)

Tactic:
exact (L.isZero_of_isStrictlyGE (n₀ + 1) i).of_iso (asIso ((midπ f n₀ 0).f i))

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

Goal state before:
pp: case cons.inr
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := { obj := X }
Y₀ b✝ c✝ : Paths (LocQuiver W)
f : Quiver.Path X₀ b✝
hf : P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
w : c✝.obj ⟶ b✝.obj
hw : W w
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map (f.cons (Sum.inr ⟨w, hw⟩))))

Tactic:
simpa only [← Construction.wInv_eq_isoOfHom_inv w hw] using! hP₂ w hw _ hf

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Map

Goal state before:
pp: case e_g
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✝³ : HasDerivedCategory C
inst✝² : HasDerivedCategory D
inst✝¹ : HasExt C
inst✝ : HasExt D
X Y : C
n : ℕ
e : Ext X Y n
this :
  (mapExactFunctor F e).hom =
    (ShiftedHom.mk₀ 0 ⋯
          (DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).app X).inv ≫
            F.mapDerivedCategoryFactors.symm.hom.app ((CochainComplex.singleFunctor C 0).obj X))).comp
      ((((SmallShiftedHom.equiv (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) DerivedCategory.Q) e).map
            F.mapDerivedCategory).comp
        (ShiftedHom.mk₀ 0 ⋯
          (F.mapDerivedCategoryFactors.symm.inv.app ((CochainComplex.singleFunctor C 0).obj Y) ≫
            DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).app Y).hom))
        ⋯)
      ⋯
⊢ ShiftedHom.mk₀ 0 ⋯
      (F.mapDerivedCategoryFactors.symm.inv.app ((CochainComplex.singleFunctor C 0).obj Y) ≫
        DerivedCategory.Q.map ((F.mapCochainComplexSingleFunctor 0).app Y).hom) =
    ShiftedHom.mk₀ 0 ⋯ ((F.mapDerivedCategorySingleFunctor 0).hom.app Y)

Tactic:
· simp [CochainComplex.singleFunctor, CochainComplex.singleFunctors,
      ← Functor.mapDerivedCategoryFactors_inv_app_mapDerivedCategorySingleFunctor_hom_app]

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
X Y : DifferentialObject S C
f : X ≅ Y
⊢ (f.inv ≫ f.hom).f = 𝟙 Y.obj

Tactic:
Iso.inv_hom_id,

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
X Y : DifferentialObject S C
f : X ≅ Y
⊢ (𝟙 Y).f = 𝟙 Y.obj
Module: Mathlib.Algebra.Homology.Embedding.Connect

Goal state before:
pp: case pos.negSucc.succ.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
p : ℤ
n : ℕ
hmp : Int.negSucc (n + 1) + 1 = p
hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)
⊢ h.d (Int.negSucc (n + 1 + 1)) (Int.negSucc (n + 1)) ≫ h.d (Int.negSucc (n + 1)) p = 0

Tactic:
obtain rfl : p = .negSucc n := by lia

Goal state after:
case pos.negSucc.succ.succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n : ℕ
hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)
hmp : Int.negSucc (n + 1) + 1 = Int.negSucc n
⊢ h.d (Int.negSucc (n + 1 + 1)) (Int.negSucc (n + 1)) ≫ h.d (Int.negSucc (n + 1)) (Int.negSucc n) = 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 =
    (restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1))).d (n + 1) n ≫
      (restrictionXIso h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ⋯).hom

Tactic:
rw [restriction_d_eq (e := (ComplexShape.embeddingUpIntLE (-1))) _
      (i' := Int.negSucc (n + 1)) (j' := Int.negSucc n) (by dsimp; lia) (by dsimp; lia),
      cochainComplex_d, 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.CategoryTheory.Idempotents.FunctorExtension

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
inst✝ : Category.{v_3, u_3} E
F : C ⥤ Karoubi D
⊢ (functorExtension₁ C D).map ((functorExtension₁CompWhiskeringLeftToKaroubiIso C D).symm.hom.app F) ≫
      (KaroubiUniversal₁.counitIso C D).hom.app ((functorExtension₁ C D).obj F) =
    𝟙 ((functorExtension₁ C D).obj F)

Tactic:
by
    ext P
    dsimp
    rw [comp_p, ← comp_f, ← F.map_comp, P.idem]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P Q : ProjectiveResolution X
⊢ Homotopy (lift (𝟙 X ≫ 𝟙 X) P P) (𝟙 P.complex)

Tactic:
simpa [id_comp] using liftIdHomotopy _ _

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P Q : ProjectiveResolution X
⊢ Homotopy (lift (𝟙 X ≫ 𝟙 X) Q Q) (𝟙 Q.complex)

Tactic:
simpa [id_comp] using liftIdHomotopy _ _

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
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
⊢ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ ≫ Q.iso.inv ≫ Q.iso.hom =
    (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ

Tactic:
Iso.inv_hom_id,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasProjectiveResolutions C
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
⊢ (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ ≫
      𝟙 ((HomotopyCategory.quotient C (ComplexShape.down ℕ)).obj Q.complex) =
    (HomotopyCategory.quotient C (ComplexShape.down ℕ)).map φ
Module: Mathlib.CategoryTheory.Abelian.Ext

Goal state before:
pp: R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ IsZero (HomologicalComplex.sc ((ProjectiveResolution.self X).complex.linearYonedaObj R Y) (n + 1)).X₂

Tactic:
IsZero.iff_id_eq_zero

Goal state after:
R : Type u_1
inst✝⁵ : Ring R
C : Type u_2
inst✝⁴ : Category.{v_1, u_2} C
inst✝³ : Abelian C
inst✝² : Linear R C
inst✝¹ : EnoughProjectives C
X Y : C
inst✝ : Projective X
n : ℕ
⊢ 𝟙 (HomologicalComplex.sc ((ProjectiveResolution.self X).complex.linearYonedaObj R Y) (n + 1)).X₂ = 0
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
⊢ (P.isoLeftDerivedToHomotopyCategoryObj F).inv ≫ F.leftDerivedToHomotopyCategory.map f =
    (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map φ ≫
      (Q.isoLeftDerivedToHomotopyCategoryObj F).inv

Tactic:
dsimp [Functor.leftDerivedToHomotopyCategory, isoLeftDerivedToHomotopyCategoryObj]

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 P.iso.inv) ≫
      (F.mapHomotopyCategory (ComplexShape.down ℕ)).map ((projectiveResolutions C).map f) =
    (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
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
⊢ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) ≫
      (Q.isoLeftDerivedToHomotopyCategoryObj F).inv ≫ (Q.isoLeftDerivedToHomotopyCategoryObj F).hom =
    (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)

Tactic:
Iso.inv_hom_id,

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
⊢ (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) ≫
      𝟙
        ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
          ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex)) =
    (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)
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
n : ℕ
⊢ (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map φ =
    (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
        φ ≫
      (Q.isoLeftDerivedObj F n).inv ≫ (Q.isoLeftDerivedObj F n).hom

Tactic:
Iso.inv_hom_id,

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
n : ℕ
⊢ (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map φ =
    (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
        φ ≫
      𝟙
        ((F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙
              HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj
          Q.complex)
Module: Mathlib.Algebra.Homology.LocalCohomology

Goal state before:
pp: case h.inl
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : unop j1.left ≤ unop j2.left
⊢ Nonempty (j2 ⟶ j1)

Tactic:
exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩

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

Goal state before:
pp: case h.inr
R : Type u
inst✝ : CommRing R
I J K : Ideal R
hR : IsNoetherian R R
J' : SelfLERadical J
j1 j2 : CostructuredArrow (idealPowersToSelfLERadical J) J'
h : unop j2.left ≤ unop j1.left
⊢ Nonempty (j1 ⟶ j2)

Tactic:
exact ⟨CostructuredArrow.homMk (homOfLE h).op rfl⟩

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
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (P.isoLeftDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
        g =
    (P.isoLeftDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
          g ≫
        (Q.isoLeftDerivedObj F n).inv ≫ (Q.isoLeftDerivedObj F n).hom

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
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ g.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f

Tactic:
Iso.inv_hom_id,

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
F : C ⥤ D
inst✝ : F.Additive
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ (P.isoLeftDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
        g =
    (P.isoLeftDerivedObj F n).hom ≫
      (F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map
          g ≫
        𝟙
          ((F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙
                HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj
            Q.complex)

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
n : ℕ
X Y : C
f : X ⟶ Y
P : ProjectiveResolution X
Q : ProjectiveResolution Y
g : P.complex ⟶ Q.complex
w : g ≫ Q.π = P.π ≫ (ChainComplex.single₀ C).map f
⊢ g.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f
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 G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
⊢ (NatTrans.leftDerivedToHomotopyCategory α).app X ≫ (P.isoLeftDerivedToHomotopyCategoryObj G).hom =
    (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) ≫
        (P.isoLeftDerivedToHomotopyCategoryObj G).inv ≫ (P.isoLeftDerivedToHomotopyCategoryObj G).hom

Tactic:
Iso.inv_hom_id,

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
F G : C ⥤ D
inst✝¹ : F.Additive
inst✝ : G.Additive
α : F ⟶ G
X : C
P : ProjectiveResolution X
⊢ (NatTrans.leftDerivedToHomotopyCategory α).app X ≫ (P.isoLeftDerivedToHomotopyCategoryObj G).hom =
    (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫
      (HomotopyCategory.quotient D (ComplexShape.down ℕ)).map
          ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) ≫
        𝟙
          ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj
            ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex))
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
m : (mapBifunctorRightUnitorCofan F Y e p hp X j).pt ⟶ s.pt
hm : ∀ (j_1 : ↑(p ⁻¹' {j})), Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) j_1 ≫ m = s.inj j_1
⊢ m =
    e.inv.app (X j) ≫
      (F.obj (X j)).map ((singleObjApplyIso 0 Y).inv ≫ (singleObjApplyIso 0 Y).hom) ≫ e.hom.app (X j) ≫ m

Tactic:
Iso.inv_hom_id,

Goal state after:
C : Type u_1
D : Type u_2
I : Type u_3
J : Type u_4
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Category.{v_2, u_2} D
inst✝³ : Zero I
inst✝² : DecidableEq I
inst✝¹ : HasInitial C
F : D ⥤ C ⥤ D
Y : C
e : F.flip.obj Y ≅ 𝟭 D
inst✝ : ∀ (X : D), PreservesColimit (Functor.empty C) (F.obj X)
p : J × I → J
hp : ∀ (j : J), p (j, 0) = j
X X' : GradedObject J D
φ : X ⟶ X'
j : J
s : Cofan ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j)
m : (mapBifunctorRightUnitorCofan F Y e p hp X j).pt ⟶ s.pt
hm : ∀ (j_1 : ↑(p ⁻¹' {j})), Cofan.inj (mapBifunctorRightUnitorCofan F Y e p hp X j) j_1 ≫ m = s.inj j_1
⊢ m = e.inv.app (X j) ≫ (F.obj (X j)).map (𝟙 Y) ≫ e.hom.app (X j) ≫ m