mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithCofibrations C
inst✝ : CategoryWithWeakEquivalences C
⊢ trivialCofibrations C f ↔ Cofibration f ∧ WeakEquivalence f

Tactic:
cofibration_iff,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : CategoryWithCofibrations C
inst✝ : CategoryWithWeakEquivalences C
⊢ trivialCofibrations C f ↔ cofibrations C f ∧ WeakEquivalence f
Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : Cylinder A
inst✝² : IsCofibrant A
P P' : Cylinder A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : P.I ⨿ A ⟶ (P.trans P').I := coprod.desc (pushout.inl P.i₁ P'.i₀) (P'.i₁ ≫ pushout.inr P.i₁ P'.i₀)
⊢ coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr P.i₁ P'.i₀

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : Cylinder A
inst✝² : IsCofibrant A
P P' : Cylinder A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : P.I ⨿ A ⟶ (P.trans P').I := ⋯
⊢ coprod.inl ≫ coprod.map P.i₁ (𝟙 A) ≫ ψ = coprod.inl ≫ P'.i ≫ pushout.inr P.i₁ P'.i₀

case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : Cylinder A
inst✝² : IsCofibrant A
P P' : Cylinder A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : P.I ⨿ A ⟶ (P.trans P').I := ⋯
⊢ coprod.inr ≫ coprod.map P.i₁ (𝟙 A) ≫ ψ = coprod.inr ≫ P'.i ≫ pushout.inr P.i₁ P'.i₀
Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : PathObject A
inst✝² : IsFibrant A
P P' : PathObject A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : (P.trans P').P ⟶ P.P ⨯ A := prod.lift (pullback.fst P.p₁ P'.p₀) (pullback.snd P.p₁ P'.p₀ ≫ P'.p₁)
⊢ ψ ≫ prod.map P.p₁ (𝟙 A) = pullback.snd P.p₁ P'.p₀ ≫ P'.p

Tactic:
ext

Goal state after:
case h₁
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : PathObject A
inst✝² : IsFibrant A
P P' : PathObject A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : (P.trans P').P ⟶ P.P ⨯ A := ⋯
⊢ (ψ ≫ prod.map P.p₁ (𝟙 A)) ≫ prod.fst = (pullback.snd P.p₁ P'.p₀ ≫ P'.p) ≫ prod.fst

case h₂
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ModelCategory C
A : C
P✝ : PathObject A
inst✝² : IsFibrant A
P P' : PathObject A
inst✝¹ : P.IsGood
inst✝ : P'.IsGood
ψ : (P.trans P').P ⟶ P.P ⨯ A := ⋯
⊢ (ψ ≫ prod.map P.p₁ (𝟙 A)) ≫ prod.snd = (pullback.snd P.p₁ P'.p₀ ≫ P'.p) ≫ prod.snd
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ : C
P✝ : Precylinder X✝
Y✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : Precylinder X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ Q.i₀ ≫ ObjectProperty.homMk h.h = f

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ : C
P✝ : Precylinder X✝
Y✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : Precylinder X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ (Q.i₀ ≫ ObjectProperty.homMk h.h).hom = f.hom
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ : C
P✝ : Precylinder X✝
Y✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : Precylinder X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ Q.i₁ ≫ ObjectProperty.homMk h.h = g

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ : C
P✝ : Precylinder X✝
Y✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : Precylinder X
f g : X ⟶ Y
h : (Q.map P.ι).LeftHomotopy f.hom g.hom
⊢ (Q.i₁ ≫ ObjectProperty.homMk h.h).hom = g.hom
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
f g : X ⟶ Y
h : LeftHomotopyRel f g
⊢ ∃ P, P.IsGood ∧ Nonempty (P.LeftHomotopy f g)

Tactic:
by
  obtain ⟨P, ⟨h⟩⟩ := h
  exact h.exists_good_cylinder

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y✝ : C
P✝ : PrepathObject Y✝
X✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : PrepathObject Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ ObjectProperty.homMk h.h ≫ Q.p₀ = f

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
Y✝ : C
P✝ : PrepathObject Y✝
X✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : PrepathObject Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ (ObjectProperty.homMk h.h ≫ Q.p₀).hom = f.hom
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
Y✝ : C
P✝ : PrepathObject Y✝
X✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : PrepathObject Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ ObjectProperty.homMk h.h ≫ Q.p₁ = g

Tactic:
ext

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
Y✝ : C
P✝ : PrepathObject Y✝
X✝ : C
P : ObjectProperty C
X Y : P.FullSubcategory
Q : PrepathObject Y
f g : X ⟶ Y
h : (Q.map P.ι).RightHomotopy f.hom g.hom
⊢ (ObjectProperty.homMk h.h ≫ Q.p₁).hom = g.hom
Module: Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
f g : X ⟶ Y
inst✝ : IsCofibrant X
h : RightHomotopyRel f g
Z : C
p : Y ⟶ Z
⊢ RightHomotopyRel (f ≫ p) (g ≫ p)

Tactic:
obtain ⟨P, _, ⟨h⟩⟩ := h.exists_very_good_pathObject
  obtain ⟨Q, _⟩ := PathObject.exists_very_good Z
  have sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p)) := { }
  exact ⟨Q,
   ⟨{ h := h.h ≫ sq.lift
      h₀ := by
        have := sq.fac_right =≫ prod.fst
        simp only [Category.assoc, prod.lift_fst, Q.p_fst] at this
        simp [this]
      h₁ := by
        have := sq.fac_right =≫ prod.snd
        simp only [Category.assoc, prod.lift_snd, Q.p_snd] at this
        simp [this]
    }⟩⟩

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : Plus C
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L = K.obj
⊢ (quotient C).obj { obj := L, property := ?m.38 } = K

Tactic:
ext

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : Plus C
L : HomologicalComplex C (ComplexShape.up ℤ)
hL : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L = K.obj
⊢ ((quotient C).obj { obj := L, property := ?m.38 }).obj = K.obj
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✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ : HomotopyCategory.Plus C
f : F.mapHomotopyCategoryPlus.obj X✝ ⟶ F.mapHomotopyCategoryPlus.obj Y✝
⊢ F.mapHomotopyCategoryPlus.map (ObjectProperty.homMk ((F.mapHomotopyCategory (ComplexShape.up ℤ)).preimage f.hom)) = f

Tactic:
ext

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
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ : HomotopyCategory.Plus C
f : F.mapHomotopyCategoryPlus.obj X✝ ⟶ F.mapHomotopyCategoryPlus.obj Y✝
⊢ (F.mapHomotopyCategoryPlus.map
        (ObjectProperty.homMk ((F.mapHomotopyCategory (ComplexShape.up ℤ)).preimage f.hom))).hom =
    f.hom
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✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ : HomotopyCategory.Plus C
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F.mapHomotopyCategoryPlus.map a₁✝ = F.mapHomotopyCategoryPlus.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
ext

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
inst✝¹ : F.Full
inst✝ : F.Faithful
X✝ Y✝ : HomotopyCategory.Plus C
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : F.mapHomotopyCategoryPlus.map a₁✝ = F.mapHomotopyCategoryPlus.map a₂✝
⊢ a₁✝.hom = a₂✝.hom
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT

Goal state before:
pp: case refine_3
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 b : ℤ
h : a + 1 = b
⊢ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
      Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C 1) =
    (Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁

Tactic:
ext

Goal state after:
case refine_3
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 b : ℤ
h : a + 1 = b
x✝ : C
⊢ ((t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁ ≫
          Functor.whiskerRight (t.truncLEIsoTruncLT a b h).hom (shiftFunctor C 1)).app
      x✝ =
    ((Iso.refl (t.triangleLEGE a b h ⋙ Triangle.π₃)).hom ≫ (t.triangleLTGE b).whiskerLeft Triangle.π₃Toπ₁).app x✝
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 b : ℤ
h : a + 1 = b
⊢ (t.triangleLEGT a).whiskerLeft Triangle.π₃Toπ₁ ≫
      Functor.whiskerRight (Iso.refl (t.triangleLEGT a ⋙ Triangle.π₁)).hom (shiftFunctor C 1) =
    (t.truncGTIsoTruncGE a b h).hom ≫ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁

Tactic:
ext

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 b : ℤ
h : a + 1 = b
x✝ : C
⊢ ((t.triangleLEGT a).whiskerLeft Triangle.π₃Toπ₁ ≫
          Functor.whiskerRight (Iso.refl (t.triangleLEGT a ⋙ Triangle.π₁)).hom (shiftFunctor C 1)).app
      x✝ =
    ((t.truncGTIsoTruncGE a b h).hom ≫ (t.triangleLEGE a b h).whiskerLeft Triangle.π₃Toπ₁).app x✝
Module: Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
⊢ (∃ Z g h, ∃ (_ : Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles), B.inverseImage A.ι Z) ↔
    ∃ Z g h, ∃ (_ : Triangle.mk f.hom g h ∈ Pretriangulated.distinguishedTriangles), (A ⊓ B) Z

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
⊢ (∃ Z g h, ∃ (_ : Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles), B.inverseImage A.ι Z) →
    ∃ Z g h, ∃ (_ : Triangle.mk f.hom g h ∈ Pretriangulated.distinguishedTriangles), (A ⊓ B) Z

case mpr
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
A B : ObjectProperty C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : A.IsTriangulated
X Y : A.FullSubcategory
f : X ⟶ Y
⊢ (∃ Z g h, ∃ (_ : Triangle.mk f.hom g h ∈ Pretriangulated.distinguishedTriangles), (A ⊓ B) Z) →
    ∃ Z g h, ∃ (_ : Triangle.mk f g h ∈ Pretriangulated.distinguishedTriangles), B.inverseImage A.ι Z
Module: Mathlib.Algebra.Homology.DerivedCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : Plus C
n : ℤ
⊢ (ι.obj X).IsGE n ↔ X.IsGE n

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : Plus C
n : ℤ
⊢ (ι.obj X).IsGE n → X.IsGE n

case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : Plus C
n : ℤ
⊢ X.IsGE n → (ι.obj X).IsGE n
Module: Mathlib.Algebra.Homology.DerivedCategory.Plus

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : Plus C
n : ℤ
⊢ (ι.obj X).IsLE n ↔ X.IsLE n

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : Plus C
n : ℤ
⊢ (ι.obj X).IsLE n → X.IsLE n

case mpr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : Plus C
n : ℤ
⊢ X.IsLE n → (ι.obj X).IsLE n
Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
⊢ Injective I ↔ (MorphismProperty.monomorphisms C).rlp 0

Tactic:
constructor

Goal state after:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
⊢ Injective I → (MorphismProperty.monomorphisms C).rlp 0

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
⊢ (MorphismProperty.monomorphisms C).rlp 0 → Injective I
Module: Mathlib.CategoryTheory.Preadditive.Injective.LiftingProperties

Goal state before:
pp: case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
⊢ Injective I

Tactic:
constructor

Goal state after:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
I Z : C
hZ : IsZero Z
h : (MorphismProperty.monomorphisms C).rlp 0
⊢ ∀ {X Y : C} (g : X ⟶ I) (f : X ⟶ Y) [Mono f], ∃ h, f ≫ h = g
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
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f = 0

Tactic:
ext

Goal state after:
case h₁
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
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₁ = TriangleMorphism.hom₁ 0

case h₂
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
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₂ = TriangleMorphism.hom₂ 0

case h₃
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
T T' : Triangle C
f₁ f₂ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
a b : ℤ
h₀ : t.IsLE T.obj₁ a
h₁ : t.IsGE T'.obj₃ b
H : f₁.hom₂ = f₂.hom₂
hab : a ≤ b
f : T ⟶ T'
hf : f.hom₂ = 0
⊢ f.hom₃ = TriangleMorphism.hom₃ 0
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 : C
g : X ⟶ Y
⊢ epiWithInjectiveKernel g ↔
    ∃ I,
      ∃ (_ : Injective I),
        ∃ f, ∃ (w : f ≫ g = 0), Nonempty { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.Splitting

Tactic:
constructor

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
⊢ epiWithInjectiveKernel g →
    ∃ I,
      ∃ (_ : Injective I),
        ∃ f, ∃ (w : f ≫ g = 0), Nonempty { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.Splitting

case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
g : X ⟶ Y
⊢ (∃ I,
      ∃ (_ : Injective I),
        ∃ f, ∃ (w : f ≫ g = 0), Nonempty { X₁ := I, X₂ := X, X₃ := Y, f := f, g := g, zero := w }.Splitting) →
    epiWithInjectiveKernel g
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✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
this✝² : Preadditive D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this✝¹ : Preadditive D₂ := Localization.preadditive L₂ B.trW
this✝ : L₁.Additive
this : L₂.Additive
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful

Tactic:
let e : A.ι ⋙ L₂ ≅ L₁ ⋙ F :=
    CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F

Goal state after:
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✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
this✝² : Preadditive D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this✝¹ : Preadditive D₂ := Localization.preadditive L₂ B.trW
this✝ : L₁.Additive
this : L₂.Additive
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
⊢ ((A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂).Faithful
Module: Mathlib.CategoryTheory.Abelian.EpiWithInjectiveKernel

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
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
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ (biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ = 0

Tactic:
ext

Goal state after:
case refine_1.h₀
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
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
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ biprod.inl ≫ (biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ = biprod.inl ≫ 0

case h₁
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y Z : C
g₁ : X ⟶ Y
g₂ : Y ⟶ Z
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
I₂ : C
w✝ : Injective I₂
f₂ : I₂ ⟶ Y
w₂ : f₂ ≫ g₂ = 0
σ₂ : { X₁ := I₂, X₂ := Y, X₃ := Z, f := f₂, g := g₂, zero := w₂ }.Splitting
⊢ biprod.inr ≫ (biprod.fst ≫ f₁ + biprod.snd ≫ f₂ ≫ σ₁.s) ≫ g₁ ≫ g₂ = biprod.inr ≫ 0
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 : C
⊢ t.IsGE X n ↔ IsIso ((t.truncGEπ n).app X)

Tactic:
constructor

Goal state after:
case mp
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 : C
⊢ t.IsGE X n → IsIso ((t.truncGEπ n).app X)

case mpr
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 : C
⊢ IsIso ((t.truncGEπ n).app X) → t.IsGE X n
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✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
this✝³ : Preadditive D₁ := Localization.preadditive L₁ (B.inverseImage A.ι).trW
this✝² : Preadditive D₂ := Localization.preadditive L₂ B.trW
this✝¹ : L₁.Additive
this✝ : L₂.Additive
F : D₁ ⥤ D₂ := (A.triangulatedLocalizerMorphism B).localizedFunctor L₁ L₂
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := CatCommSq.iso (A.triangulatedLocalizerMorphism B).functor L₁ L₂ F
X₁ X₂ : A.FullSubcategory
f : X₁ ⟶ X₂
X₃ : C
s : X₂.obj ⟶ X₃
hs : B.trW s
fac : f.hom ≫ s = 0 ≫ s
X₄ : C
t : X₂.obj ⟶ X₄
a : X₃ ⟶ X₄
hX₄ : A X₄
ht : (A ⊓ B).trW t
fac' : s ≫ a = t
t' : X₂ ⟶ { obj := X₄, property := hX₄ } := homMk t
this : IsIso (L₁.map t')
⊢ f ≫ t' = 0

Tactic:
ext

Goal state after:
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✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasShift C ℤ
inst✝⁹ : Preadditive C
inst✝⁸ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁷ : Pretriangulated C
inst✝⁶ : IsTriangulated C
inst✝⁵ : A.IsTriangulated
inst✝⁴ : B.IsTriangulated
inst✝³ : B.IsClosedUnderIsomorphisms
inst✝² : A.IsVerdierRightLocalizing B
L₁ : A.FullSubcategory ⥤ D₁
L₂ : C ⥤ D₂
inst✝¹ : L₁.IsLocalization (B.inverseImage A.ι).trW
inst✝ : L₂.IsLocalization B.trW
this✝³ : Preadditive D₁ := ⋯
this✝² : Preadditive D₂ := ⋯
this✝¹ : L₁.Additive
this✝ : L₂.Additive
F : D₁ ⥤ D₂ := ⋯
e : A.ι ⋙ L₂ ≅ L₁ ⋙ F := ⋯
X₁ X₂ : A.FullSubcategory
f : X₁ ⟶ X₂
X₃ : C
s : X₂.obj ⟶ X₃
hs : B.trW s
fac : f.hom ≫ s = 0 ≫ s
X₄ : C
t : X₂.obj ⟶ X₄
a : X₃ ⟶ X₄
hX₄ : A X₄
ht : (A ⊓ B).trW t
fac' : s ≫ a = t
t' : X₂ ⟶ { obj := X₄, property := hX₄ } := ⋯
this : IsIso (L₁.map t')
⊢ (f ≫ t').hom = InducedCategory.Hom.hom 0