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

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

Tactic:
dsimp [d₁]

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
P : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : P.IsTriangulated
Y : C
hY : P.rightOrthogonal Y
X₁ X₂ : C
f : X₁ ⟶ X₂
x✝ : P.trW f
X₃ : C
g : X₂ ⟶ X₃
h : X₃ ⟶ (shiftFunctor C 1).obj X₁
hT : Triangle.mk f g h ∈ distinguishedTriangles
hX₃ : P X₃
⊢ Function.Injective fun g ↦ f ≫ g

Tactic:
suffices ∀ (α : X₂ ⟶ Y), f ≫ α = 0 → α = 0 from fun α₁ α₂ hα ↦ by
      simpa [sub_eq_zero] using this (α₁ - α₂) (by simpa [sub_eq_zero] using hα)
    intro α hα
    obtain ⟨β, rfl⟩ := Triangle.yoneda_exact₂ _ hT α hα
    simp [hY β hX₃]

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
hL : L.IsKInjective
n : ℤ
⊢ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L).IsKInjective

Tactic:
rw [isKInjective_iff_rightOrthogonal] at hL ⊢

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
L : CochainComplex C ℤ
hL : (HomotopyCategory.subcategoryAcyclic C).rightOrthogonal ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)
n : ℤ
⊢ (HomotopyCategory.subcategoryAcyclic C).rightOrthogonal
    ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L))
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

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
α : Cochain K L (-1)
n : ℤ
hα : (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) n
hK : HomologicalComplex.ExactAt K (n + 1)
inst✝ : Injective (L.X (n + 1))
u : K.X (n + 1) ⟶ L.X (n + 1) :=
  f.f (n + 1) - α.v (n + 1) n ⋯ ≫ L.d n (n + 1) - K.d (n + 1) (n + 2) ≫ α.v (n + 2) (n + 1) ⋯
⊢ n ≤ n

Tactic:
by rfl

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
⊢ (quasiIso A).RespectsIso

Tactic:
by
  dsimp only [quasiIso]
  infer_instance

Goal state after:
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 : ℤ
⊢ a ≤ a

Tactic:
by rfl

Goal state after:
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 : ℤ
X : C
⊢ a ≤ a

Tactic:
by rfl

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n : ℤ
X Y : C
φ : X ⟶ Y
A : ?m.28
a : ℤ
⊢ a ≤ a

Tactic:
by rfl

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

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
hL : IsZero L
n : ℤ
⊢ epiWithInjectiveKernel (f.f n) ↔ Injective (K.X n)

Tactic:
epiWithInjectiveKernel_iff_of_isZero

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
hL : IsZero L
n : ℤ
⊢ Injective (K.X n) ↔ Injective (K.X n)

case hY
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
K L : CochainComplex C ℤ
f : K ⟶ L
hL : IsZero L
n : ℤ
⊢ IsZero (L.X n)
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
a : ℤ
⊢ a ≤ a

Tactic:
by rfl

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
a : ℤ
X : C
⊢ a ≤ a

Tactic:
by rfl

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
inst✝ : IsTriangulated C
X : C
n : ℤ
⊢ n ≤ n

Tactic:
by rfl

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsCofibrant X
g : Y ⟶ Z
inst✝² : IsFibrant Y
inst✝¹ : IsFibrant Z
inst✝ : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
⊢ ((fun f ↦ f.postcomp h.r) ∘ fun f ↦ f.postcomp h.i) = id

Tactic:
ext φ

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsCofibrant X
g : Y ⟶ Z
inst✝² : IsFibrant Y
inst✝¹ : IsFibrant Z
inst✝ : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
φ : LeftHomotopyClass X Y
⊢ ((fun f ↦ f.postcomp h.r) ∘ fun f ↦ f.postcomp h.i) φ = id φ
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsCofibrant X
g : Y ⟶ Z
inst✝² : IsFibrant Y
inst✝¹ : IsFibrant Z
inst✝ : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
hi : Function.Bijective fun f ↦ f.postcomp h.i
⊢ (fun f ↦ f.postcomp g) = (fun f ↦ f.postcomp h.p) ∘ fun f ↦ f.postcomp h.i

Tactic:
ext φ

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsCofibrant X
g : Y ⟶ Z
inst✝² : IsFibrant Y
inst✝¹ : IsFibrant Z
inst✝ : WeakEquivalence g
h : FibrantBrownFactorization g := Classical.arbitrary (FibrantBrownFactorization g)
hi : Function.Bijective fun f ↦ f.postcomp h.i
φ : LeftHomotopyClass X Y
⊢ φ.postcomp g = ((fun f ↦ f.postcomp h.p) ∘ fun f ↦ f.postcomp h.i) φ
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsFibrant Z
f : X ⟶ Y
inst✝² : IsCofibrant X
inst✝¹ : IsCofibrant Y
inst✝ : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
⊢ ((fun g ↦ g.precomp h.s) ∘ fun g ↦ g.precomp h.p) = id

Tactic:
ext φ

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsFibrant Z
f : X ⟶ Y
inst✝² : IsCofibrant X
inst✝¹ : IsCofibrant Y
inst✝ : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
φ : RightHomotopyClass Y Z
⊢ ((fun g ↦ g.precomp h.s) ∘ fun g ↦ g.precomp h.p) φ = id φ
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsFibrant Z
f : X ⟶ Y
inst✝² : IsCofibrant X
inst✝¹ : IsCofibrant Y
inst✝ : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
hj : Function.Bijective fun g ↦ g.precomp h.p
⊢ (fun g ↦ g.precomp f) = (fun g ↦ g.precomp h.i) ∘ fun g ↦ g.precomp h.p

Tactic:
ext φ

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ModelCategory C
X Y Z : C
inst✝³ : IsFibrant Z
f : X ⟶ Y
inst✝² : IsCofibrant X
inst✝¹ : IsCofibrant Y
inst✝ : WeakEquivalence f
h : CofibrantBrownFactorization f := Classical.arbitrary (CofibrantBrownFactorization f)
hj : Function.Bijective fun g ↦ g.precomp h.p
φ : RightHomotopyClass Y Z
⊢ φ.precomp f = ((fun g ↦ g.precomp h.i) ∘ fun g ↦ g.precomp h.p) φ
Module: Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ weakEquivalences (FibrantObject C) ≤ (weakEquivalences C).inverseImage ι

Tactic:
by rfl

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

Goal state before:
pp: case mp
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_4
D₂ : Type u_5
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_4, u_4} D₁
inst✝ : Category.{v_5, u_5} D₂
T : C₁ ⥤ D₁
L : C₁ ⥤ C₂
R : D₁ ⥤ D₂
B : C₂ ⥤ D₂
w : TwoSquare T L R B
L' : C₁ ⥤ C₂
R' : D₁ ⥤ D₂
α : L ≅ L'
β : R ≅ R'
h : (w.whiskerVertical α.hom β.inv).GuitartExact
this : w = (w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom
⊢ ((w.whiskerVertical α.hom β.inv).whiskerVertical α.inv β.hom).GuitartExact

Tactic:
exact whiskerVertical (w.whiskerVertical α.hom β.inv) α.symm β.symm

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

Goal state before:
pp: 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)
this : ∀ (X : w.CostructuredArrowDownwards y), ∃ Y, Zigzag X ((fromRightResolution Φ L y).obj Y)
X X' : (TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv).CostructuredArrowDownwards y
⊢ Zigzag X X'

Tactic:
obtain ⟨Y, hX⟩ := this X

Goal state after:
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)
this : ∀ (X : w.CostructuredArrowDownwards y), ∃ Y, Zigzag X ((fromRightResolution Φ L y).obj Y)
X X' : (TwoSquare.mk Φ.functor (Φ.functor ⋙ L) L (𝟭 D) (Φ.functor ⋙ L).rightUnitor.inv).CostructuredArrowDownwards y
Y : Φ.RightResolution X₂
hX : Zigzag X ((fromRightResolution Φ L y).obj Y)
⊢ Zigzag X X'
Module: Mathlib.CategoryTheory.GuitartExact.Basic

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
C₄ : Type u₄
inst✝³ : Category.{v₁, u₁} C₁
inst✝² : Category.{v₂, u₂} C₂
inst✝¹ : Category.{v₃, u₃} C₃
inst✝ : Category.{v₄, u₄} C₄
T : C₁ ⥤ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ⥤ C₄
w : TwoSquare T L R B
X₂ : C₂
X₃ : C₃
g : R.obj X₂ ⟶ B.obj X₃
f₁ f₂ : w.CostructuredArrowDownwards g
φ : f₁ ⟶ f₂
⊢ L.map (StructuredArrow.Hom.right φ.left) ≫
      (StructuredArrow.mk (CostructuredArrow.homMk (CostructuredArrow.left f₂).hom ⋯)).right.hom =
    (StructuredArrow.mk (CostructuredArrow.homMk (CostructuredArrow.left f₁).hom ⋯)).right.hom

Tactic:
by dsimp; rw [← CostructuredArrow.w φ]; rfl

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₁)
e' : T.op ⋙ R.op ≅ L.op ⋙ B.op := NatIso.op e.symm
X₀ : C₀ᵒᵖ
Y : Cᵒᵖ
f₀ f₁ : L.op.obj X₀ ⟶ Y
h : B.op.map f₀ = B.op.map f₁
⊢ ∃ P, T.op.map P.i₀ = T.op.map P.i₁ ∧ Nonempty ((P.map L.op).LeftHomotopy f₀ f₁)

Tactic:
obtain ⟨P, hP, ⟨h⟩⟩ := he f₀.unop f₁.unop (Quiver.Hom.op_inj h)

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
X₀ : C₀ᵒᵖ
Y : Cᵒᵖ
f₀ f₁ : L.op.obj X₀ ⟶ Y
h✝ : B.op.map f₀ = B.op.map f₁
P : PrepathObject (unop X₀)
hP : T.map P.p₀ = T.map P.p₁
h : (P.map L).RightHomotopy f₀.unop f₁.unop
⊢ ∃ P, T.op.map P.i₀ = T.op.map P.i₁ ∧ Nonempty ((P.map L.op).LeftHomotopy f₀ 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 : ℤ
q : ℕ
hq : i ≤ n₀ + ↑q
this : IsIso ((midπ f n₀ q).f i)
⊢ epiWithInjectiveKernel ((midπ f n₀ q).f i ≫ ((functor f n₀).obj (op q)).obj.π.f i)

Tactic:
exact MorphismProperty.comp_mem _ _ _
    (epiWithInjectiveKernel_of_iso _)
    ((CofFibFactorizationQuasiIsoLE.sequence f n₀ q).obj.property.2 i)

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

Goal state before:
pp: case cons
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✝
g : b✝ ⟶ c✝
hf : P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map (f.cons g)))

Tactic:
| cons f g hf =>

Goal state after:
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
⊢ (quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus ≤
    (quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus

Tactic:
by rfl

Goal state after:
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
inst✝ : EnoughInjectives C
⊢ (quasiIso C).inverseImage (InjectiveObject.ι C).mapCochainComplexPlus ≤
    (weakEquivalences (FibrantObject (Plus C))).inverseImage (fibrantObjectEquivalence C).functor

Tactic:
by rfl

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives

Goal state before:
pp: case refine_2
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₁ : K₁ ⟶ ((InjectiveObject.ι C).mapHomologicalComplex (ComplexShape.up ℤ)).obj K₂
hf : (R C).functor.map (ObjectProperty.homMk f₀) = (R C).functor.map (ObjectProperty.homMk f₁)
⊢ ((Plus.prepathObject { obj := K₂, property := ⋯ }).map
        (CochainComplex.Plus.localizerMorphism C).functor).RightHomotopy
    (ObjectProperty.homMk f₀) (ObjectProperty.homMk f₁)

Tactic:
· refine PrepathObject.RightHomotopy.fullSubcategoryEquiv.symm
        { h := pathObject.lift f₀ f₁ (homotopyOfEq _ _
          ((HomotopyCategory.Plus.ι C).congr_map hf)) ≫
          (pathObject.mapHomologicalComplexObjIso K₂ (InjectiveObject.ι C)
            (fun n ↦ ⟨n + 1, by simp⟩)).inv
          h₀ := ?_
          h₁ := ?_ }
      all_goals
        dsimp [Functor.mapCochainComplexPlus]
        cat_disch

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.KProjective

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
K L : ChainComplex C ℕ
inst✝¹ : ∀ (n : ℕ), Projective (K.X n)
inst✝ : ∀ (n : ℕ), Projective (L.X n)
f : K ⟶ L
⊢ QuasiIso f ↔ homotopyEquivalences C (ComplexShape.down ℕ) f

Tactic:
by
  rw [← quasiIso_extendMap_iff _ ComplexShape.embeddingDownNat,
    CochainComplex.IsKProjective.quasiIso_iff,
    homotopyEquivalences_extendMap_iff]

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✝ : ℤ
n m : ℕ
hnm : Int.negSucc n + 1 ≠ Int.negSucc m
⊢ h.d (Int.negSucc n) (Int.negSucc m) = 0

Tactic:
by
    simpa only [d_negSucc] using! K.shape n m (by simp at hnm ⊢; lia)

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this✝¹ : HasZeroObject C
this✝ : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
⊢ Cofork.π cc ≫ hS.cokerToKer' k hk cc kf hcc hkf ≫ Fork.ι kf = (S.sc hS (k + 1) ⋯).f

Tactic:
IsComplex.cokerToKer'_fac

Goal state after:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n : ℕ
S : ComposableArrows C (n + 3)
hS : S.IsComplex
k : ℕ
hk : k ≤ n
cc : CokernelCofork (S.map' k (k + 1) ⋯ ⋯)
kf : KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)
hcc : IsColimit cc
hkf : IsLimit kf
hS' : (S.sc hS (k + 1) ⋯).Exact
this✝¹ : HasZeroObject C
this✝ : (S.sc hS (k + 1) ⋯).HasHomology
h : (S.sc hS (k + 1) ⋯).LeftHomologyData := hS'.leftHomologyDataOfIsLimitKernelFork kf hkf
this : Epi h.f'
⊢ S.map' (k + 1) (k + 2) ⋯ ⋯ = (S.sc hS (k + 1) ⋯).f
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 : X ⟶ K.X q
n : ℤ
h : p + n = q
q' : ℤ
hq' : q + 1 = q'
hf : f ≫ K.d q q' = 0
⊢ δ n (n + 1) (Cochain.fromSingleMk f h) = 0

Tactic:
by
    rw [Cochain.δ_fromSingleMk _ _ _ q' (by lia), hf]
    simp

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

Goal state before:
pp: I : Type u
inst✝³ : AddMonoid I
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : MonoidalCategory C
X Y : GradedObject I C
inst✝ : X.HasTensor Y
⊢ tensorHom (𝟙 X) (𝟙 Y) = 𝟙 (tensorObj X Y)

Tactic:
dsimp [tensorHom, mapBifunctorMapMap]
  simp only [Functor.map_id, NatTrans.id_app, comp_id, mapMap_id]
  rfl

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

Goal state before:
pp: I : Type u
inst✝⁶ : AddMonoid I
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ X₄ : GradedObject I C
inst✝³ : X₃.HasTensor X₄
inst✝² : X₂.HasTensor (tensorObj X₃ X₄)
inst✝¹ : X₁.HasTensor (tensorObj X₂ (tensorObj X₃ X₄))
j : I
A : C
f g : tensorObj X₁ (tensorObj X₂ (tensorObj X₃ X₄)) j ⟶ A
inst✝ : X₂.HasGoodTensorTensor₂₃ X₃ X₄
H : X₁.HasTensor₄ObjExt X₂ X₃ X₄
h :
  ∀ (i₁ i₂ i₃ i₄ : I) (h : i₁ + i₂ + i₃ + i₄ = j),
    ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ f = ιTensorObj₄ X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j h ≫ g
⊢ f = g

Tactic:
by
  apply tensorObj_ext
  intro i₁ i₂₃₄ h'
  apply left_tensor_tensorObj₃_ext
  intro i₂ i₃ i₄ h''
  have hj : i₁ + i₂ + i₃ + i₄ = j := by simp only [← h', ← h'', add_assoc]
  simpa only [assoc, ιTensorObj₄_eq X₁ X₂ X₃ X₄ i₁ i₂ i₃ i₄ j hj i₂₃₄ h''] using h i₁ i₂ i₃ i₄ hj

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} ι
inst✝ : Abelian C
X : SpectralObject C ι
i j k : ι
f : i ⟶ j
g : j ⟶ k
n₀ : ℤ
A : C
x : A ⟶ (X.H n₀).obj (mk₁ g)
hx : x ≫ X.δ f g n₀ (n₀ + 1) ⋯ = 0
⊢ x ≫ X.δ f g n₀ (n₀ + 1) ⋯ = 0

Tactic:
exact hx

Goal state after: