mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
n : ℤ
⊢ (Q.obj K).IsGE n ↔ K.IsGE n

Tactic:
by
  have eq := fun i ↦ ((homologyFunctorFactors C i).app K).isZero_iff
  simp only [Functor.comp_obj, HomologicalComplex.homologyFunctor_obj] at eq
  simp only [isGE_iff, CochainComplex.isGE_iff,
    HomologicalComplex.exactAt_iff_isZero_homology, eq]

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

Goal state before:
pp: case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ (coproducts.{w, v, u} T).rlp

Tactic:
· rw [← le_llp_iff_le_rlp]
    exact T.coproducts_le_llp_rlp

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
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_5, u_3} C₁₂
inst✝²⁸ : Category.{v_6, u_4} C₂₃
inst✝²⁷ : HasZeroMorphisms C₁
inst✝²⁶ : HasZeroMorphisms C₂
inst✝²⁵ : HasZeroMorphisms C₃
inst✝²⁴ : Preadditive C₁₂
inst✝²³ : Preadditive C₂₃
inst✝²² : Preadditive C₄
F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
F : C₁ ⥤ C₂₃ ⥤ C₄
G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
inst✝²¹ : F₁₂.PreservesZeroMorphisms
inst✝²⁰ : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms
inst✝¹⁹ : G.Additive
inst✝¹⁸ : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms
inst✝¹⁷ : G₂₃.PreservesZeroMorphisms
inst✝¹⁶ : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms
inst✝¹⁵ : F.PreservesZeroMorphisms
inst✝¹⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
ι₁ : 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₂ F₁₂ c₁₂
inst✝⁷ : K₂.HasMapBifunctor K₃ G₂₃ c₂₃
inst✝⁶ : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄
inst✝⁵ : DecidableEq ι₁₂
inst✝⁴ : DecidableEq ι₂₃
inst✝³ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
inst✝² : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄
inst✝¹ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
⊢ mapBifunctor₁₂.ιOrZero F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j ≫
      (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ j).hom =
    ((associator.hom.app (K₁.X i₁)).app (K₂.X i₂)).app (K₃.X i₃) ≫
      mapBifunctor₂₃.ιOrZero F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j

Tactic:
by_cases h : ComplexShape.r c₁ c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
  · rw [mapBifunctor₁₂.ιOrZero_eq _ _ _ _ _ _ _ _ _ _ _ h,
      mapBifunctor₂₃.ιOrZero_eq _ _ _ _ _ _ _ _ _ _ _ _ h,
      ι_mapBifunctorAssociatorX_hom]
  · rw [mapBifunctor₁₂.ιOrZero_eq_zero _ _ _ _ _ _ _ _ _ _ _ h,
      mapBifunctor₂₃.ιOrZero_eq_zero _ _ _ _ _ _ _ _ _ _ _ _ h,
      zero_comp, comp_zero]

Goal state after:
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
K : HomologicalComplex C (ComplexShape.up ℤ)
hX : HomotopyCategory.plus C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
⊢ HomotopyCategory.plus D
    ((HomotopyCategory.quotient D (ComplexShape.up ℤ)).obj
      ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K).as))

Tactic:
simp only [HomotopyCategory.plus_quotient_obj_iff] at hX ⊢

Goal state after:
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
K : HomologicalComplex C (ComplexShape.up ℤ)
hX : CochainComplex.plus C K
⊢ CochainComplex.plus D
    ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K).as)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

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
t : TStructure C
a : ℤ
⊢ t.truncGEπ (a + 1) ≫ 𝟙 (t.truncGT a) = t.truncGEπ (a + 1)

Tactic:
Category.comp_id

Goal state after:
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
t : TStructure C
a : ℤ
⊢ t.truncGEπ (a + 1) = t.truncGEπ (a + 1)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

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
t : TStructure C
a : ℤ
⊢ t.truncGEπ (a + 1) ≫ 𝟙 (t.truncGE (a + 1)) = t.truncGEπ (a + 1)

Tactic:
Category.comp_id

Goal state after:
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
t : TStructure C
a : ℤ
⊢ t.truncGEπ (a + 1) = t.truncGEπ (a + 1)
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
I : C
w✝ : Injective I
f : I ⟶ X
w : f ≫ g = 0
σ : { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.Splitting
this : IsSplitEpi g
e : I ≅ kernel g :=
  ⋯.fIsKernel.conePointUniqueUpToIso
    (limit.isLimit (parallelPair { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.g 0))
⊢ epiWithInjectiveKernel g

Tactic:
exact ⟨inferInstance, Injective.of_iso e inferInstance⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
⊢ ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W} (h : RetractArrow f g), epiWithInjectiveKernel g → epiWithInjectiveKernel f

Tactic:
rintro X' Y' X Y f' f r ⟨_, hf⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X' Y' X Y : C
f' : X' ⟶ Y'
f : X ⟶ Y
r : RetractArrow f' f
left✝ : Epi f
hf : Injective (kernel f)
⊢ epiWithInjectiveKernel f'
Module: Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor

Goal state before:
pp: case refine_2
C₁ : Type u_1
C₂ : Type u_2
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
inst✝⁴ : ∀ (X₂ : C₂), IsConnected (Φ.RightResolution X₂)
inst✝³ : Φ.arrow.HasRightResolutions
inst✝² : W₂.ContainsIdentities
D : Type u_3
inst✝¹ : Category.{v_3, u_3} D
L : C₂ ⥤ D
inst✝ : L.IsLocalization W₂
X₂ : C₂
X₃ : D
y : L.obj X₂ ⟶ X₃
w : TwoSquare Φ.functor (Φ.functor ⋙ L) L (𝟭 D) :=
  TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv
this✝ : Nonempty (w.CostructuredArrowDownwards y)
c : C₁
g : X₂ ⟶ Φ.functor.obj c
x : L.obj (Φ.functor.obj c) ⟶ X₃
fac✝ : L.map g ≫ 𝟙 (L.obj (Φ.functor.obj c)) ≫ x = y
fac : L.map g ≫ x = y
ρ : Φ.arrow.RightResolution (Arrow.mk g) := Classical.arbitrary (Φ.arrow.RightResolution (Arrow.mk g))
this :
  Zigzag
    ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      { X₁ := c, w := 𝟙 (Φ.functor.obj c), hw := ⋯ })
    ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      { X₁ := ρ.X₁.right, w := Arrow.Hom.right ρ.w, hw := ⋯ })
⊢ Zigzag
    ((fromRightResolution Φ L x ⋙ w.costructuredArrowDownwardsPrecomp x y g fac).obj
      { X₁ := ρ.X₁.right, w := Arrow.Hom.right ρ.w, hw := ⋯ })
    ((fromRightResolution Φ L y).obj { X₁ := ρ.X₁.left, w := Arrow.Hom.left ρ.w, hw := ⋯ })

Tactic:
apply Zigzag.of_inv
    refine CostructuredArrow.homMk (StructuredArrow.homMk ρ.X₁.hom (by simp)) ?_
    ext
    simp [← cancel_epi (isoOfHom L W₂ ρ.w.left ρ.hw.1).hom, ← L.map_comp_assoc, fac]

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)
q : ℕ
i : ℤ
⊢ (midπ f n₀ q).f i ≫ ((functor f n₀).obj (op q)).obj.π.f i = (π f n₀).f i

Tactic:
rw [← midπ_π f n₀ q]
  dsimp

Goal state after:
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₁ : X ⟶ L.obj Y₀),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.p₀ = T.map P.p₁ ∧ Nonempty ((P.map L).RightHomotopy f₀ f₁)
⊢ (op e.inv).GuitartExact

Tactic:
let e' : T.op ⋙ R.op ≅ L.op ⋙ B.op := NatIso.op e.symm

Goal state after:
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₁ : X ⟶ L.obj Y₀),
    B.map f₀ = B.map f₁ → ∃ P, T.map P.p₀ = T.map P.p₁ ∧ Nonempty ((P.map L).RightHomotopy f₀ f₁)
e' : T.op ⋙ R.op ≅ L.op ⋙ B.op := NatIso.op e.symm
⊢ (op e.inv).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 : CochainComplex C ℤ
inst✝¹ : EnoughInjectives C
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst✝ : K.IsStrictlyGE n₁
this : K.IsStrictlyGE (n₀ + 1)
L : CochainComplex C ℤ
hL : L.IsStrictlyGE n₀
i : K ⟶ L
p : L ⟶ 0
hi : Mono i
hi' : QuasiIso i
hp : degreewiseEpiWithInjectiveKernel p
right✝ : i ≫ p = 0
⊢ ∃ L i, ∃ (_ : Mono i) (_ : QuasiIso i) (_ : ∀ (n : ℤ), Injective (L.X n)), L.IsStrictlyGE n₀

Tactic:
exact ⟨L, i, hi, hi', (degreewiseEpiWithInjectiveKernel_iff_of_isZero p
    (Limits.isZero_zero _)).1 hp, hL⟩

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₂
X : C₁
⊢ IsIso (α₂.app (Φ.functor.obj X) ≫ F₂.map ((CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom.app X)) ↔
    IsIso (α₂.app (Φ.functor.obj X))

Tactic:
isIso_comp_right_iff

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₂
X : C₁
⊢ IsIso (α₂.app (Φ.functor.obj X)) ↔ IsIso (α₂.app (Φ.functor.obj X))
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived

Goal state before:
pp: case refine_2
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' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  e.hom.app X₁ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) = s.ι.app (CostructuredArrow.mk φ)
this : IsIso (F.map w)
eq :
  F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)) = s.ι.app (CostructuredArrow.mk φ)
⊢ e.hom.app X₁ ≫
      G.map (L.map w) ≫
        G.map (Localization.isoOfHom L W w hw).inv ≫
          G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    e.hom.app X₁ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))

Tactic:
← G.map_comp_assoc

Goal state after:
case refine_2
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' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ F'
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : L.IsLocalization W
Y : C
s : Cocone (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  e.hom.app X₁ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) = s.ι.app (CostructuredArrow.mk φ)
this : IsIso (F.map w)
eq :
  F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)) = s.ι.app (CostructuredArrow.mk φ)
⊢ e.hom.app X₁ ≫
      G.map (L.map w ≫ (Localization.isoOfHom L W w hw).inv) ≫
        G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))) =
    e.hom.app X₁ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
⊢ ∀ ⦃X : CochainComplex.Plus C⦄ ⦃Y₀ : CochainComplex.Plus (InjectiveObject C)⦄
    (f₀ f₁ : X ⟶ (CochainComplex.Plus.localizerMorphism C).functor.obj Y₀),
    (R C).functor.map f₀ = (R C).functor.map f₁ →
      ∃ P,
        (L C).functor.map P.p₀ = (L C).functor.map P.p₁ ∧
          Nonempty ((P.map (CochainComplex.Plus.localizerMorphism C).functor).RightHomotopy f₀ f₁)

Tactic:
rintro ⟨K₁, n₁, hn₁⟩ ⟨K₂, n₂, hn₂⟩ f₀ f₁ hf

Goal state after:
C : Type u_1
H : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : Category.{v_2, u_2} H
K₁ : CochainComplex C ℤ
n₁ : ℤ
hn₁ : K₁.IsStrictlyGE n₁
K₂ : CochainComplex (InjectiveObject C) ℤ
n₂ : ℤ
hn₂ : K₂.IsStrictlyGE n₂
f₀ f₁ :
  { obj := K₁, property := ⋯ } ⟶ (CochainComplex.Plus.localizerMorphism C).functor.obj { obj := K₂, property := ⋯ }
hf : (R C).functor.map f₀ = (R C).functor.map f₁
⊢ ∃ P,
    (L C).functor.map P.p₀ = (L C).functor.map P.p₁ ∧
      Nonempty ((P.map (CochainComplex.Plus.localizerMorphism C).functor).RightHomotopy f₀ f₁)
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✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map
      (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategoryFactors.hom.app (CochainComplex.mappingCone S.f) ≫
      Q.map
          ((CochainComplex.mappingCone.mapHomologicalComplexIso S.f F).hom ≫
            (CochainComplex.mappingCone.triangle ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map S.f)).mor₃) ≫
        (Functor.commShiftIso Q 1).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj S.X₁) ≫
          (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
            (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)

Tactic:
← CochainComplex.mappingCone.map_δ,

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
F : C ⥤ D
inst✝⁴ : F.Additive
inst✝³ : PreservesFiniteLimits F
inst✝² : PreservesFiniteColimits F
inst✝¹ : HasDerivedCategory C
inst✝ : HasDerivedCategory D
S : ShortComplex (CochainComplex C ℤ)
hS : S.ShortExact
this : QuasiIso (CochainComplex.mappingCone.descShortComplex S)
⊢ F.mapDerivedCategory.map
      (Q.map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫ (Functor.commShiftIso Q 1).hom.app S.X₁) =
    F.mapDerivedCategoryFactors.hom.app (CochainComplex.mappingCone S.f) ≫
      Q.map
          ((F.mapHomologicalComplex (ComplexShape.up ℤ)).map (CochainComplex.mappingCone.triangle S.f).mor₃ ≫
            (Functor.commShiftIso (F.mapHomologicalComplex (ComplexShape.up ℤ)) 1).hom.app S.X₁) ≫
        (Functor.commShiftIso Q 1).hom.app ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj S.X₁) ≫
          (shiftFunctor (DerivedCategory D) 1).map (F.mapDerivedCategoryFactors.inv.app S.X₁) ≫
            (Functor.commShiftIso F.mapDerivedCategory 1).inv.app (Q.obj S.X₁)
Module: Mathlib.Algebra.Homology.Embedding.StupidTrunc

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✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝ : e.IsRelIff
i : ι
i' : ι'
hi' : e.f i = i'
⊢ (K.restriction e).X i = K.X i'

Tactic:
subst hi'; rfl

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

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

Tactic:
simp at hnm

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

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

Tactic:
simp at hnm

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

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

Tactic:
by_cases hmp : m + 1 = p

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

case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
K : ChainComplex C ℕ
L : CochainComplex C ℕ
h : ConnectData K L
n m p : ℤ
hnm : n + 1 = m
hmp : ¬m + 1 = p
⊢ h.d n m ≫ h.d m p = 0
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 : C ⥤ D ⥤ D
X : C
e : F.obj X ≅ 𝟭 D
inst✝¹ : ∀ (Y : D), PreservesColimit (Functor.empty C) (F.flip.obj Y)
p : I × J → J
hp : ∀ (j : J), p (0, j) = j
Y : GradedObject J D
inst✝ : (((mapBifunctor F I J).obj ((single₀ I).obj X)).obj Y).HasMap p
j : J
⊢ ιMapBifunctorMapObj F p ((single₀ I).obj X) Y 0 j j ⋯ ≫ (mapBifunctorLeftUnitor F X e p hp Y).hom j =
    (F.map (singleObjApplyIso 0 X).hom).app (Y j) ≫ e.hom.app (Y j)

Tactic:
by
  dsimp [mapBifunctorLeftUnitor]
  erw [CofanMapObjFun.ιMapObj_iso_inv]
  rw [mapBifunctorLeftUnitorCofan_inj]

Goal state after:
Module: Mathlib.CategoryTheory.GradedObject.Unitor

Goal state before:
pp: case neg
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)
j' : J
i : I
h : (j', i) ∈ p ⁻¹' {j}
hi : ¬i = 0
⊢ IsInitial ((((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).mapObjFun p j ⟨(j', i), h⟩)

Tactic:
exact mapBifunctorObjObjSingle₀IsInitial _ _ _ _ hi

Goal state after:
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'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
j : J
⊢ φ j ≫ (mapBifunctorRightUnitor F Y e p hp X').inv j =
    (mapBifunctorRightUnitor F Y e p hp X).inv j ≫ mapBifunctorMapMap F p φ (𝟙 ((single₀ I).obj Y)) j

Tactic:
mapBifunctorRightUnitor_inv_apply,

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'
inst✝¹ : (((mapBifunctor F J I).obj X).obj ((single₀ I).obj Y)).HasMap p
inst✝ : (((mapBifunctor F J I).obj X').obj ((single₀ I).obj Y)).HasMap p
j : J
⊢ φ j ≫
      e.inv.app (X' j) ≫
        (F.obj (X' j)).map (singleObjApplyIso 0 Y).inv ≫ ιMapBifunctorMapObj F p X' ((single₀ I).obj Y) j 0 j ⋯ =
    (mapBifunctorRightUnitor F Y e p hp X).inv j ≫ mapBifunctorMapMap F p φ (𝟙 ((single₀ I).obj Y)) j