mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.Basic

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
n : ℤ
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : t.le n X✝
⊢ t.le n Y✝

Tactic:
simp only [le_iff_isLE] at h ⊢

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
n : ℤ
X✝ Y✝ : C
e : X✝ ≅ Y✝
h : t.IsLE X✝ n
⊢ t.IsLE Y✝ n
Module: Mathlib.Algebra.Homology.HomotopyFiber

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : DecidableRel c.Rel
inst✝ : HasHomotopyFiber φ
i j : α
hij : c.symm.Rel i j
this : HasBinaryBiproduct (G.X j) (F.X i)
⊢ HasBinaryBiproduct (((opFunctor C c).obj (op G)).X j) (((opFunctor C c).obj (op F)).X i)

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : DecidableRel c.Rel
inst✝ : HasHomotopyFiber φ
i j : α
hij : c.symm.Rel i j
this : HasBinaryBiproduct (G.X j) (F.X i)
⊢ HasBinaryBiproduct (op (G.X j)) (op (F.X i))
Module: Mathlib.Algebra.Homology.HomotopyFiber

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : DecidableRel c.Rel
inst✝ : ∀ (i : α), HasBinaryBiproduct (K.X i) (K.X i)
i : α
⊢ HasBinaryBiproduct (K.op.X i) (K.op.X i)

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
α : Type u_2
c : ComplexShape α
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : DecidableRel c.Rel
inst✝ : ∀ (i : α), HasBinaryBiproduct (K.X i) (K.X i)
i : α
⊢ HasBinaryBiproduct (op (K.X i)) (op (K.X i))
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ (triangleOfSES h).mor₁ ≫ e₂.hom =
    (Iso.refl (triangleOfSES h).obj₁).hom ≫
      (Triangle.mk (Q.map (K.ιTruncLE 0) ≫ e₂.hom) (e₂.inv ≫ Q.map (K.πTruncGE 1))
          (inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13)) ≫
            (triangleOfSES h).mor₃)).mor₁

Tactic:
dsimp

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ Q.map (HomologicalComplex.ιTruncLE K (ComplexShape.embeddingUpIntLE 0)) ≫ e₂.hom =
    𝟙 (Q.obj (HomologicalComplex.truncLE K (ComplexShape.embeddingUpIntLE 0))) ≫ Q.map (K.ιTruncLE 0) ≫ e₂.hom
Module: Mathlib.Algebra.Homology.DerivedCategory.TStructure

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ (triangleOfSES h).mor₂ ≫
      (asIso (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13))).hom =
    e₂.hom ≫
      (Triangle.mk (Q.map (K.ιTruncLE 0) ≫ e₂.hom) (e₂.inv ≫ Q.map (K.πTruncGE 1))
          (inv (Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13)) ≫
            (triangleOfSES h).mor₃)).mor₂

Tactic:
dsimp

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X : DerivedCategory C
K : CochainComplex C ℤ
e₂ : Q.obj K ≅ X
h : (K.shortComplexTruncLE 0).ShortExact
⊢ Q.map (K.shortComplexTruncLE 0).g ≫
      Q.map (K.shortComplexTruncLEX₃ToTruncGE 0 1 DerivedCategory.TStructure.t._proof_13) =
    e₂.hom ≫ e₂.inv ≫ Q.map (K.πTruncGE 1)
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 ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : Cochain.ofHom φ = (↑z).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ (Cochain.rightShiftAddEquiv K L n n 0 ⋯) (δ m n (n.negOnePow • f.rightUnshift m ⋯)) =
    (Cochain.rightShiftAddEquiv K L n n 0 ⋯) ↑z

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
z : Cocycle K L n
inst✝ : L.IsKInjective
hK : HomologicalComplex.Acyclic K
m : ℤ
hm : m + 1 = n
φ : K ⟶ (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L
hφ : Cochain.ofHom φ = (↑z).rightShift n 0 ⋯
h : Homotopy φ 0
f : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L) (-1)
hf : Cochain.ofHom φ = δ (-1) 0 f
⊢ (δ m n (n.negOnePow • f.rightUnshift m ⋯)).rightShift n 0 ⋯ = (↑z).rightShift n 0 ⋯
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 : ℤ
eq : ∀ (i : ℤ), IsZero ((homologyFunctor C i).obj (Q.obj K)) ↔ IsZero (HomologicalComplex.homology K i)
⊢ (Q.obj K).IsLE n ↔ K.IsLE n

Tactic:
simp only [isLE_iff, CochainComplex.isLE_iff,
    HomologicalComplex.exactAt_iff_isZero_homology, eq]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
G : C ⥤ D
inst✝ : G.IsEquivalence
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) (G.map p) ↔ HasLiftingProperty i p

Tactic:
#adaptation_note /-- Prior to nightly-2026-05-07, the next three lines were just
  ```
  simp only [dsimp% G.asEquivalence.toAdjunction.hasLiftingProperty_iff,
    ← MorphismProperty.rlp_ofHoms_iff_hasLiftingProperty Unit]
  ```
  This is a temporary repair, and authors/maintainers are encouraged to either find a better repair,
  or identify a minimal example of an underlying problem in Lean.
  -/

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
D : Type u_1
inst✝¹ : Category.{v_1, u_1} D
G : C ⥤ D
inst✝ : G.IsEquivalence
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty (G.map i) (G.map p) ↔ HasLiftingProperty i p
Module: Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithWeakEquivalences C
P : ObjectProperty C
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ WeakEquivalence (P.ι.map f)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
inst✝¹ : CategoryWithWeakEquivalences C
P : ObjectProperty C
X Y : P.FullSubcategory
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ WeakEquivalence f.hom
Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : C
inst✝ : CategoryWithWeakEquivalences C
P : Cylinder A
⊢ WeakEquivalence P.symm.π

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : C
inst✝ : CategoryWithWeakEquivalences C
P : Cylinder A
⊢ WeakEquivalence P.π
Module: Mathlib.AlgebraicTopology.ModelCategory.Cylinder

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
A : C
inst✝⁶ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
inst✝³ : (fibrations C).IsStableUnderComposition
inst✝² : (cofibrations C).RespectsIso
inst✝¹ : HasBinaryCoproducts C
inst✝ : P.IsVeryGood
⊢ Fibration P.symm.π

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
A : C
inst✝⁶ : CategoryWithWeakEquivalences C
P : Cylinder A
inst✝⁵ : CategoryWithCofibrations C
inst✝⁴ : CategoryWithFibrations C
inst✝³ : (fibrations C).IsStableUnderComposition
inst✝² : (cofibrations C).RespectsIso
inst✝¹ : HasBinaryCoproducts C
inst✝ : P.IsVeryGood
⊢ Fibration P.π
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
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (codiag A)
⊢ Fibration (ofFactorizationData h).π

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A : C
P : Cylinder A
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (codiag A)
⊢ Fibration h.p
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
this : WeakEquivalence ((P.i₀ ≫ pushout.inl P.i₁ P'.i₀) ≫ pushout.desc P.π P'.π ⋯)
⊢ WeakEquivalence (P.trans P'.toPrecylinder).π

Tactic:
dsimp

Goal state after:
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
this : WeakEquivalence ((P.i₀ ≫ pushout.inl P.i₁ P'.i₀) ≫ pushout.desc P.π P'.π ⋯)
⊢ WeakEquivalence (pushout.desc P.π P'.π ⋯)
Module: Mathlib.AlgebraicTopology.ModelCategory.PathObject

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : C
inst✝ : CategoryWithWeakEquivalences C
P : PathObject A
⊢ WeakEquivalence P.symm.ι

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
A : C
inst✝ : CategoryWithWeakEquivalences C
P : PathObject A
⊢ WeakEquivalence P.ι
Module: Mathlib.AlgebraicTopology.ModelCategory.Basic

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : CategoryWithFibrations C
inst✝⁶ : CategoryWithCofibrations C
inst✝⁵ : CategoryWithWeakEquivalences C
inst✝⁴ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝³ : (trivialCofibrations C).IsWeakFactorizationSystem (fibrations C)
inst✝² : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
A B X Y : C
f : A ⟶ B
w : X ⟶ Y
inst✝¹ : Fibration f
inst✝ : WeakEquivalence w
h : RetractArrow f w
hw : (trivialCofibrations C).MapFactorizationData (fibrations C) w
this✝¹ : (trivialFibrations C).IsStableUnderRetracts
sq : CommSq (Arrow.Hom.left h.r) hw.i f (hw.p ≫ Arrow.Hom.right h.r)
hf : fibrations C f
this✝ : HasLiftingProperty hw.i f
this : RetractArrow f hw.p
h' : trivialFibrations C hw.p
⊢ WeakEquivalence f

Tactic:
simpa only [weakEquivalence_iff] using (of_retract this h').2

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

Goal state before:
pp: C : Type u
inst✝⁷ : Category.{v, u} C
A : C
inst✝⁶ : CategoryWithWeakEquivalences C
P : PathObject A
inst✝⁵ : CategoryWithFibrations C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : (cofibrations C).IsStableUnderComposition
inst✝² : (fibrations C).RespectsIso
inst✝¹ : HasBinaryProducts C
inst✝ : P.IsVeryGood
⊢ Cofibration P.symm.ι

Tactic:
dsimp

Goal state after:
C : Type u
inst✝⁷ : Category.{v, u} C
A : C
inst✝⁶ : CategoryWithWeakEquivalences C
P : PathObject A
inst✝⁵ : CategoryWithFibrations C
inst✝⁴ : CategoryWithCofibrations C
inst✝³ : (cofibrations C).IsStableUnderComposition
inst✝² : (fibrations C).RespectsIso
inst✝¹ : HasBinaryProducts C
inst✝ : P.IsVeryGood
⊢ Cofibration P.ι
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
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (diag A)
⊢ Cofibration (ofFactorizationData h).ι

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A : C
P : PathObject A
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (diag A)
⊢ Cofibration h.i
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₀)
fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr P.i₁ P'.i₀
⊢ Cofibration (coprod.map P.i₀ (𝟙 A) ≫ ψ)

Tactic:
have sq : IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr _ _) := by
      simpa [ψ] using IsPushout.of_hasPushout P.i₁ P'.i₀

Goal state after:
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₀)
fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr P.i₁ P'.i₀
sq : IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr P.i₁ P'.i₀)
⊢ Cofibration (coprod.map P.i₀ (𝟙 A) ≫ ψ)
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
this : WeakEquivalence (pullback.lift P.ι P'.ι ⋯ ≫ pullback.fst P.p₁ P'.p₀ ≫ P.p₀)
⊢ WeakEquivalence (P.trans P'.toPrepathObject).ι

Tactic:
dsimp

Goal state after:
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
this : WeakEquivalence (pullback.lift P.ι P'.ι ⋯ ≫ pullback.fst P.p₁ P'.p₀ ≫ P.p₀)
⊢ WeakEquivalence (pullback.lift P.ι P'.ι ⋯)
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.LeftHomotopy f g
⊢ (Q.map P.ι).i₀ ≫ h.h.hom = f.hom

Tactic:
dsimp

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.LeftHomotopy f g
⊢ Q.i₀.hom ≫ 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.LeftHomotopy f g
⊢ (Q.map P.ι).i₁ ≫ h.h.hom = g.hom

Tactic:
dsimp

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.LeftHomotopy f g
⊢ Q.i₁.hom ≫ h.h.hom = g.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.RightHomotopy f g
⊢ h.h.hom ≫ (Q.map P.ι).p₀ = f.hom

Tactic:
dsimp

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.RightHomotopy f g
⊢ h.h.hom ≫ 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.RightHomotopy f g
⊢ h.h.hom ≫ (Q.map P.ι).p₁ = g.hom

Tactic:
dsimp

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.RightHomotopy f g
⊢ h.h.hom ≫ 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✝² : CategoryWithWeakEquivalences C
P : PathObject Y
inst✝¹ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝ : (weakEquivalences C).ContainsIdentities
f₀ f₁ : X ⟶ Y
h : P.RightHomotopy f₀ f₁
⊢ WeakEquivalence f₀ ↔ WeakEquivalence f₁

Tactic:
induction h
  grind [weakEquivalence_postcomp_iff]

Goal state after:
Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ G.map ((lift.shiftIso hΦ (m + n) a a'' ⋯).hom.app X) =
    G.map
      (((Φ a'').isoWhiskerLeft (shiftFunctorAdd D m n) ≪≫
              ((Φ a'').associator (shiftFunctor D m) (shiftFunctor D n)).symm ≪≫
                isoWhiskerRight (lift.shiftIso hΦ m a' a'' ha'') (shiftFunctor D n) ≪≫
                  lift.shiftIso hΦ n a a' ha').hom.app
        X)

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝⁸ : Category.{?u.6, u_1} C
inst✝⁷ : Category.{?u.9, u_2} D
inst✝⁶ : Category.{?u.12, u_3} E
A : Type u_4
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift D A
inst✝³ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝² : G.CommShift A
inst✝¹ : G.Full
inst✝ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
n m a a' a'' : A
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ G.map ((lift.shiftIso hΦ (m + n) a a'' ⋯).hom.app X) =
    G.map
      ((shiftFunctorAdd D m n).hom.app ((Φ a'').obj X) ≫
        𝟙 ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((Φ a'').obj X))) ≫
          (shiftFunctor D n).map ((lift.shiftIso hΦ m a' a'' ha'').hom.app X) ≫ (lift.shiftIso hΦ n a a' ha').hom.app X)
Module: Mathlib.CategoryTheory.Shift.SingleFunctorsLift

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹³ : Category.{u_5, u_1} C
inst✝¹² : Category.{u_6, u_2} D
inst✝¹¹ : Category.{u_7, u_3} E
A : Type u_4
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift D A
inst✝⁸ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝⁷ : G.CommShift A
inst✝⁶ : G.Full
inst✝⁵ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : Preadditive E
inst✝¹ : G.Additive
a : A
inst✝ : (F.functor a).Additive
⊢ ((F.lift G Φ hΦ).functor a ⋙ G).Additive

Tactic:
dsimp

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹³ : Category.{u_5, u_1} C
inst✝¹² : Category.{u_6, u_2} D
inst✝¹¹ : Category.{u_7, u_3} E
A : Type u_4
inst✝¹⁰ : AddMonoid A
inst✝⁹ : HasShift D A
inst✝⁸ : HasShift E A
F : SingleFunctors C E A
G : D ⥤ E
inst✝⁷ : G.CommShift A
inst✝⁶ : G.Full
inst✝⁵ : G.Faithful
Φ : A → C ⥤ D
hΦ : (a : A) → Φ a ⋙ G ≅ F.functor a
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
inst✝² : Preadditive E
inst✝¹ : G.Additive
a : A
inst✝ : (F.functor a).Additive
⊢ (Φ a ⋙ G).Additive
Module: Mathlib.Algebra.Homology.HomotopyCategory.Plus

Goal state before:
pp: case refine_1
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
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h✝¹ : CochainComplex.IsStrictlyGE T.obj₁.as n₁
n₂ : ℤ
h✝ : CochainComplex.IsStrictlyGE T.obj₂.as n₂
f : T.obj₁.as ⟶ T.obj₂.as
hf : (quotient C (ComplexShape.up ℤ)).map f = T.mor₁
⊢ plus C (Triangle.π₃.obj (CochainComplex.mappingCone.triangleh f))

Tactic:
dsimp

Goal state after:
case refine_1
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
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T ∈ distinguishedTriangles
h₁ : plus C T.obj₁
h₂ : plus C T.obj₂
n₁ : ℤ
h✝¹ : CochainComplex.IsStrictlyGE T.obj₁.as n₁
n₂ : ℤ
h✝ : CochainComplex.IsStrictlyGE T.obj₂.as n₂
f : T.obj₁.as ⟶ T.obj₂.as
hf : (quotient C (ComplexShape.up ℤ)).map f = T.mor₁
⊢ plus C ((quotient C (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone f))
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.Plus.ι C ⋙ F.mapHomotopyCategory (ComplexShape.up ℤ)).obj
      { obj := (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K, property := hX })

Tactic:
dsimp

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 : 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))
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
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ t.IsGE X n₁ ↔ IsZero ((t.truncLE n₀).obj X)

Tactic:
by
  rw [t.isGE_iff_isIso_truncGEπ_app n₁ X]
  exact (Triangle.isZero₁_iff_isIso₂ _ (t.triangleLEGE_distinguished n₀ n₁ h X)).symm

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
X Y : C
f : X ⟶ Y
n : ℤ
inst✝ : t.IsLE X n
⊢ t.IsGE ((t.triangleLEGT n).obj Y).obj₃ (n + 1)

Tactic:
dsimp

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
X Y : C
f : X ⟶ Y
n : ℤ
inst✝ : t.IsLE X n
⊢ t.IsGE ((t.truncGT n).obj Y) (n + 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
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst✝ : t.IsGE Y n₁
⊢ t.IsLE ((t.triangleLEGT n₀).obj X).obj₁ n₀

Tactic:
dsimp

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
X Y : C
f : X ⟶ Y
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
inst✝ : t.IsGE Y n₁
⊢ t.IsLE ((t.truncLE n₀).obj X) n₀