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

Goal state before:
pp: case snd
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n}
⊢ (↑((fun x_1 ↦
            match x_1 with
            | ⟨(a, b), h⟩ => ⟨(a - x, b), ⋯⟩)
          ((fun x_1 ↦
              match x_1 with
              | ⟨(a, b), h⟩ => ⟨(a + x, b), ⋯⟩)
            ⟨(a, b), h⟩))).2 =
    (↑⟨(a, b), h⟩).2

Tactic:
· rfl

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

Goal state before:
pp: case snd
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K L : HomologicalComplex₂ C (up ℤ) (up ℤ)
f : K ⟶ L
x y : ℤ
inst✝ : K.HasTotal (up ℤ)
n a b : ℤ
h : (a, b) ∈ (up ℤ).π (up ℤ) (up ℤ) ⁻¹' {n + x}
⊢ (↑((fun x_1 ↦
            match x_1 with
            | ⟨(a, b), h⟩ => ⟨(a + x, b), ⋯⟩)
          ((fun x_1 ↦
              match x_1 with
              | ⟨(a, b), h⟩ => ⟨(a - x, b), ⋯⟩)
            ⟨(a, b), h⟩))).2 =
    (↑⟨(a, b), h⟩).2

Tactic:
· rfl

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
x : ℤ
inst✝ : K.HasTotal (up ℤ)
a b n : ℤ
h : a + b = n
a' : ℤ
ha' : a' = a + x
n' : ℤ
hn' : n' = n + x
⊢ ((shiftFunctor₁ C x).obj K).ιTotal (up ℤ) a b n h ≫ (K.totalShift₁Iso x).hom.f n =
    (K.shiftFunctor₁XXIso a x a' ha' b).hom ≫
      K.ιTotal (up ℤ) a' b n' ⋯ ≫ (CochainComplex.shiftFunctorObjXIso (K.total (up ℤ)) x n n' hn').inv

Tactic:
subst ha' hn'
  dsimp [totalShift₁Iso, totalShift₁XIso]
  simp only [ι_totalDesc, comp_id, id_comp]

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_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✝¹⁴ : HasZeroMorphisms C₁
inst✝¹³ : HasZeroMorphisms C₂
inst✝¹² : HasZeroMorphisms C₃
inst✝¹¹ : Preadditive C₁₂
inst✝¹⁰ : Preadditive 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
ι₁ : Type u_7
ι₂ : Type u_8
ι₃ : Type u_9
ι₁₂ : Type u_10
ι₄ : 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 ι₄
inst✝⁴ : TotalComplexShape c₁ c₂ c₁₂
inst✝³ : TotalComplexShape c₁₂ c₃ c₄
inst✝² : K₁.HasMapBifunctor K₂ F₁₂ c₁₂
inst✝¹ : DecidableEq ι₁₂
inst✝ : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
j : ι₄
h : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ d₁ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j = 0

Tactic:
by
  dsimp [d₁]
  rw [shape _ _ _ h, Functor.map_zero, zero_app, Functor.map_zero, zero_app, zero_comp, smul_zero]

Goal state after:
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₄
inst✝ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄
j : ι₄
A : C₄
f :
  (i₁ : ι₁) →
    (i₂ : ι₂) →
      (i₃ : ι₃) → c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j → ((F.obj (K₁.X i₁)).obj ((G₂₃.obj (K₂.X i₂)).obj (K₃.X i₃)) ⟶ A)
i₁ : ι₁
i₂ : ι₂
i₃ : ι₃
h : c₁.r c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j
⊢ ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h ≫ mapBifunctor₂₃Desc c₁₂ f = f i₁ i₂ i₃ h

Tactic:
apply GradedObject.ι_mapBifunctorBifunctor₂₃Desc

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

Goal state before:
pp: case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij' : ¬c'.Rel (e.f j) (e.f i)
⊢ (K.extendXIso e ⋯).hom ≫ h.hom i j ≫ (L.extendXIso e ⋯).inv = 0

Tactic:
h.zero _ _ (by rwa [← e.rel_iff]),

Goal state after:
case pos
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
h : Homotopy f g
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hij' : ¬c'.Rel (e.f j) (e.f i)
⊢ (K.extendXIso e ⋯).hom ≫ 0 ≫ (L.extendXIso e ⋯).inv = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝³ : e.IsRelIff
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomologicalComplex C c
φ : K.extend e ⟶ L.extend e
⊢ ∃ a, (e.extendHomotopyFunctor C).map a = (HomotopyCategory.quotient C c').map φ

Tactic:
obtain ⟨φ, rfl⟩ := (e.extendFunctor C).map_surjective φ

Goal state after:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝³ : e.IsRelIff
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : Preadditive C
K L : HomologicalComplex C c
φ : K ⟶ L
⊢ ∃ a, (e.extendHomotopyFunctor C).map a = (HomotopyCategory.quotient C c').map ((e.extendFunctor C).map φ)
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
X : C
n₀ n₁ : ℤ
h : n₀ < n₁
inst✝¹ : t.IsLE X n₀
inst✝ : t.IsGE X n₁
⊢ IsZero X

Tactic:
by
  rw [IsZero.iff_id_eq_zero]
  exact t.zero _ n₀ n₁ h

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasCoproduct A
inst✝ : Limits.HasCoproduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X : C
⊢ ∀ ⦃Y : C⦄ (g : X ⟶ Y), T g → HasLiftingProperty (Limits.Sigma.map f) g

Tactic:
Y

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasCoproduct A
inst✝ : Limits.HasCoproduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.llp (f j)
X Y : C
⊢ ∀ (g : X ⟶ Y), T g → HasLiftingProperty (Limits.Sigma.map f) g
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasProduct A
inst✝ : Limits.HasProduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X : C
⊢ ∀ ⦃Y : C⦄ (g : X ⟶ Y), T g → HasLiftingProperty g (Limits.Pi.map f)

Tactic:
Y

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
T : MorphismProperty C
J : Type u_1
A B : J → C
inst✝¹ : Limits.HasProduct A
inst✝ : Limits.HasProduct B
f : (j : J) → A j ⟶ B j
hf : ∀ (j : J), T.rlp (f j)
X Y : C
⊢ ∀ (g : X ⟶ Y), T g → HasLiftingProperty g (Limits.Pi.map f)
Module: Mathlib.CategoryTheory.MorphismProperty.LiftingProperty

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
inst✝ : Nonempty ι
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i p → (ofHoms fun x ↦ i).rlp p

Tactic:
rintro _ _ _ _ ⟨⟩; assumption

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
ι : Type u_1
inst✝ : Nonempty ι
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
⊢ HasLiftingProperty i p → (ofHoms fun x ↦ p).llp i

Tactic:
rintro _ _ _ _ ⟨⟩; assumption

Goal state after:
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
⊢ Cofibration (P.trans P').i

Tactic:
by
    let ψ : P.I ⨿ A ⟶ (P.trans P').I := coprod.desc (pushout.inl _ _) (P'.i₁ ≫ pushout.inr _ _)
    rw [show (P.trans P').i = coprod.map P.i₀ (𝟙 A) ≫ ψ by simp [Precylinder.i, ψ]]
    have fac : coprod.map P.i₁ (𝟙 A) ≫ ψ = P'.i ≫ pushout.inr _ _ := by
      ext
      · simp [ψ, pushout.condition]
      · simp [ψ]
    have sq : IsPushout P.i₁ (coprod.inl ≫ P'.i) (coprod.inl ≫ ψ) (pushout.inr _ _) := by
      simpa [ψ] using IsPushout.of_hasPushout P.i₁ P'.i₀
    have : Cofibration ψ := by
      rw [cofibration_iff]
      exact (cofibrations C).of_isPushout
        (IsPushout.of_top sq fac (IsPushout.of_coprod_inl_with_id P.i₁ A).flip)
        (by rw [← cofibration_iff]; infer_instance)
    infer_instance

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : ModelCategory C
P : Cylinder X
f g : X ⟶ Y
h : P.LeftHomotopy f g
d : (cofibrations C).MapFactorizationData (trivialFibrations C) P.i :=
  (cofibrations C).factorizationData (trivialFibrations C) P.i
⊢ Cofibration
    { I := d.Z, i₀ := coprod.inl ≫ d.i, i₁ := coprod.inr ≫ d.i, π := d.p ≫ P.π, i₀_π := ⋯, i₁_π := ⋯,
        weakEquivalence_π := ⋯ }.i

Tactic:
by
        rw [cofibration_iff]
        convert! d.hi
        aesop

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
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
n : ℤ
X : C
⊢ plus C ((singleFunctor C n).obj X)

Tactic:
rw [← quotient_obj_singleFunctors_obj, plus_quotient_obj_iff]

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
inst✝¹ : HasZeroObject C
inst✝ : HasBinaryBiproducts C
n : ℤ
X : C
⊢ CochainComplex.plus C ((CochainComplex.singleFunctor C n).obj 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.truncLEIsoTruncLT a b h).hom ≫ t.truncLTι b = t.truncLEι a

Tactic:
subst 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
a : ℤ
⊢ (t.truncLEIsoTruncLT a (a + 1) ⋯).hom ≫ t.truncLTι (a + 1) = t.truncLEι a
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.truncLEIsoTruncLT a b h).inv ≫ t.truncLEι a = t.truncLTι b

Tactic:
subst 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
a : ℤ
⊢ (t.truncLEIsoTruncLT a (a + 1) ⋯).inv ≫ t.truncLEι a = t.truncLTι (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 b : ℤ
h : a + 1 = b
⊢ t.truncGTπ a ≫ (t.truncGTIsoTruncGE a b h).hom = t.truncGEπ b

Tactic:
subst 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
a : ℤ
⊢ t.truncGTπ a ≫ (t.truncGTIsoTruncGE a (a + 1) ⋯).hom = 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 b : ℤ
h : a + 1 = b
⊢ t.truncGEπ b ≫ (t.truncGTIsoTruncGE a b h).inv = t.truncGTπ a

Tactic:
subst 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
a : ℤ
⊢ t.truncGEπ (a + 1) ≫ (t.truncGTIsoTruncGE a (a + 1) ⋯).inv = t.truncGTπ a
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
x✝ : C
⊢ ((t.truncGTIsoTruncGE a (a + 1) ⋯).hom.app x✝ ≫ (t.truncGEδLE a (a + 1) ⋯).app x✝) ≫
      (shiftFunctor C 1).map (𝟙 ((t.truncLE a).obj x✝)) =
    (t.truncGTIsoTruncGE a b h).hom.app x✝ ≫ (t.truncGEδLE a b h).app x✝

Tactic:
subst 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
a : ℤ
x✝ : C
⊢ ((t.truncGTIsoTruncGE a (a + 1) ⋯).hom.app x✝ ≫ (t.truncGEδLE a (a + 1) ⋯).app x✝) ≫
      (shiftFunctor C 1).map (𝟙 ((t.truncLE a).obj x✝)) =
    (t.truncGTIsoTruncGE a (a + 1) ⋯).hom.app x✝ ≫ (t.truncGEδLE a (a + 1) ⋯).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
X Y : C
f : X ⟶ Y
a b : ℤ
h : a + 1 = b
⊢ IsIso ((t.truncLE a).map f) ↔
    ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLEι a).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z b

Tactic:
subst 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
X Y : C
f : X ⟶ Y
a : ℤ
⊢ IsIso ((t.truncLE a).map f) ↔
    ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLEι a).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z (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
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₃ : t.IsGE T.obj₃ n₁
⊢ IsIso ((t.truncLE n₀).map T.mor₁)

Tactic:
subst 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
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ : ℤ
h₃ : t.IsGE T.obj₃ (n₀ + 1)
⊢ IsIso ((t.truncLE n₀).map T.mor₁)
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
K : CochainComplex C ℤ
hK : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
L : CochainComplex C ℤ
φ : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L
hL : CochainComplex.plus C L
⊢ ∃ Z a b, HomotopyCategory.plus C Z ∧ HomotopyCategory.subcategoryAcyclic C Z ∧ a ≫ b = φ

Tactic:
obtain ⟨n, hn⟩ := hL

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
K : CochainComplex C ℤ
hK : HomotopyCategory.subcategoryAcyclic C ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K)
L : CochainComplex C ℤ
φ : (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K ⟶ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L
n : ℤ
hn : L.IsStrictlyGE n
⊢ ∃ Z a b, HomotopyCategory.plus C Z ∧ HomotopyCategory.subcategoryAcyclic C Z ∧ a ≫ b = φ
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
⊢ ∀ (Y : Plus C), Qh.essImage Y

Tactic:
by
    intro ⟨X, n, K, e, h⟩
    refine ⟨⟨(HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K, ?_⟩,
      ⟨Plus.ι.preimageIso ((quotientCompQhIso C).app _ ≪≫ e.symm)⟩⟩
    simp only [HomotopyCategory.plus_quotient_obj_iff]
    exact ⟨n, h⟩

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₀ n₁ : ℤ
h : n₀ + 1 = n₁
X : C
⊢ t.IsLE X n₀ ↔ IsIso ((t.truncLTι n₁).app X)

Tactic:
subst h

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
n₀ : ℤ
X : C
⊢ t.IsLE X n₀ ↔ IsIso ((t.truncLTι (n₀ + 1)).app X)
Module: Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE

Goal state before:
pp: 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

Tactic:
· intro
    exact t.isGE_of_iso (asIso ((truncGEπ t n).app X)).symm n

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ (IsZero (Injective.under (K.X (i + 1))) ∧ IsZero (Injective.under (K.X i))) ∧ IsZero (L.X i)

Tactic:
refine ⟨⟨?_, ?_⟩, L.isZero_of_isStrictlyGE n i hi⟩

Goal state after:
case refine_1
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero (Injective.under (K.X (i + 1)))

case refine_2
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Abelian C
inst✝² : EnoughInjectives C
K L : CochainComplex C ℤ
f : K ⟶ L
n : ℤ
inst✝¹ : K.IsStrictlyGE (n + 1)
inst✝ : L.IsStrictlyGE n
i : ℤ
hi : autoParam (i < n) isStrictlyGE_iff._auto_1
⊢ IsZero (Injective.under (K.X i))
Module: Mathlib.CategoryTheory.Functor.OfSequence

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i j : ℕ
h : i = j
⊢ f i = eqToHom ⋯ ≫ f j ≫ eqToHom ⋯

Tactic:
subst h

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : ℕ → C
f : (n : ℕ) → X n ⟶ X (n + 1)
i : ℕ
⊢ f i = eqToHom ⋯ ≫ f i ≫ eqToHom ⋯
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
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
h₁ : t.IsLE T.obj₁ n₀
X : C
f : X ⟶ T.obj₂
k : (t.truncGE n₁).obj T.obj₃ ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f (T.mor₂ ≫ (t.truncGEπ n₁).app T.obj₃) k ∈ distinguishedTriangles
⊢ t.IsLE X n₀

Tactic:
subst h

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
n₀ : ℤ
h₁ : t.IsLE T.obj₁ n₀
X : C
f : X ⟶ T.obj₂
k : (t.truncGE (n₀ + 1)).obj T.obj₃ ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f (T.mor₂ ≫ (t.truncGEπ (n₀ + 1)).app T.obj₃) k ∈ distinguishedTriangles
⊢ t.IsLE X n₀
Module: Mathlib.AlgebraicTopology.ModelCategory.Homotopy

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ModelCategory C
X Y Z : C
f g : X ⟶ Y
inst✝¹ : IsFibrant Y
h✝ : RightHomotopyRel f g
Q : Cylinder X
inst✝ : Q.IsGood
P : PathObject Y := ⋯.choose
h : ⋯.choose.RightHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (coprod.desc (f ≫ P.ι) h.h) Q.i P.p₀ (Q.π ≫ f)
this : Q.i₁ ≫ sq.lift = h.h
⊢ Q.i₁ ≫ sq.lift ≫ P.p₁ = g

Tactic:
simp [reassoc_of% this, P]

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✝³ : 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
⊢ Function.Bijective fun g ↦ g.precomp f

Tactic:
convert! (precomp_bijective_of_cofibration_of_weakEquivalence Z h.i).comp hj using 1

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
⊢ (fun g ↦ g.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
X Y : FibrantObject C
f g : X ⟶ Y
P : Cylinder X.obj
h : P.LeftHomotopy f.hom g.hom
⊢ WeakEquivalence f.hom ↔ WeakEquivalence g.hom

Tactic:
apply h.weakEquivalence_iff

Goal state after: