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

Goal state before:
pp: case succ.succ.succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k : ℕ
hjk : (ComplexShape.up ℕ).Rel (0 + 1) (k + 1 + 1)
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) (0 + 1)
⊢ ((match n✝ + 1, 0 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match 0 + 1, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

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

Goal state before:
pp: case succ.succ.succ.succ.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k j : ℕ
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) (k + 1 + 1)
hij : (ComplexShape.up ℕ).Rel 0 (j + 1 + 1)
⊢ ((match 0, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

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

Goal state before:
pp: case succ.succ.succ.succ.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
this : ∀ (k : ℕ), f ≫ C.d 0 (k + 1) = 0
k j : ℕ
hjk : (ComplexShape.up ℕ).Rel (j + 1 + 1) (k + 1 + 1)
n✝ : ℕ
hij : (ComplexShape.up ℕ).Rel (n✝ + 1) (j + 1 + 1)
⊢ ((match n✝ + 1, j + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) ≫
      match j + 1 + 1, k + 1 + 1 with
      | 0, 1 => f
      | i.succ, j.succ => C.d i j
      | x, x_1 => 0) =
    0

Tactic:
simp [this]

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c✝ : ComplexShape J
inst✝² : TotalComplexShape c₁ c₂ c₁₂
I : Type u_7
inst✝¹ : AddMonoid I
c : ComplexShape I
inst✝ : c.TensorSigns
i₁✝ i₁'✝ i₂✝ i₂'✝ : I
h : c.Rel i₁✝ i₁'✝
x✝ : c.Rel i₂✝ i₂'✝
⊢ c.ε i₁✝ * 1 = -1 * c.ε i₁'✝

Tactic:
rw [neg_mul, one_mul, mul_one, c.ε_succ h, neg_neg]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
C₁₂ : Type u_5
C₂₃ : Type u_6
inst✝⁶ : Category.{v_1, u_1} C₁
inst✝⁵ : Category.{v_2, u_2} C₂
inst✝⁴ : Category.{v_3, u_3} C₃
inst✝³ : Category.{v_4, u_4} C₄
inst✝² : Category.{v_5, u_5} C₁₂
inst✝¹ : Category.{v_6, u_6} C₂₃
F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
p : I₁ × I₂ × I₃ → J
X₁ : GradedObject I₁ C₁
inst✝ :
  ∀ (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃), ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).HasMap p
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
⊢ mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) (𝟙 X₃) = 𝟙 (mapTrifunctorMapObj F p X₁ X₂ X₃)

Tactic:
by
        ext j i₁ i₂ i₃ h
        simp only [ι_mapTrifunctorMapMap, categoryOfGradedObjects_id, Functor.map_id,
          NatTrans.id_app, id_comp, comp_id]

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

Goal state before:
pp: C₁ : Type u_1
C₁' : Type u_2
C₂ : Type u_3
C₂' : Type u_4
D : Type u_5
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₁'
inst✝⁹ : Category.{v_3, u_3} C₂
inst✝⁸ : Category.{v_4, u_4} C₂'
inst✝⁷ : Category.{v_5, u_5} D
M : Type u_6
inst✝⁶ : AddCommMonoid M
inst✝⁵ : HasShift C₁ M
inst✝⁴ : HasShift C₁' M
inst✝³ : HasShift C₂ M
inst✝² : HasShift D M
F : C₁' ⥤ C₁
inst✝¹ : F.CommShift M
G : C₁ ⥤ C₂ ⥤ D
h : CommShift₂Setup D M
inst✝ : G.CommShift₂ h
X₁' : C₁'
X₂ : C₂
m n : M
this :
  (commShiftIso (G.obj ((shiftFunctor C₁ m).obj (F.obj X₁'))) n).hom.app X₂ ≫
      (shiftFunctor D n).map ((commShiftIso (G.flip.obj X₂) m).hom.app (F.obj X₁')) =
    (commShiftIso (G.flip.obj ((shiftFunctor C₂ n).obj X₂)) m).hom.app (F.obj X₁') ≫
      (shiftFunctor D m).map ((commShiftIso (G.obj (F.obj X₁')) n).hom.app X₂) ≫
        (shiftFunctorComm D m n).inv.app ((G.obj (F.obj X₁')).obj X₂) ≫
          (↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.obj (F.obj X₁')).obj X₂)))
⊢ (commShiftIso (G.obj (F.obj ((shiftFunctor C₁' m).obj X₁'))) n).hom.app X₂ ≫
      ((commShiftIso (G.obj ((shiftFunctor C₁' m ⋙ F).obj X₁')) n).inv.app X₂ ≫
          (G.map ((commShiftIso F m).hom.app X₁')).app ((shiftFunctor C₂ n).obj X₂) ≫
            (commShiftIso (G.obj ((F ⋙ shiftFunctor C₁ m).obj X₁')) n).hom.app X₂) ≫
        (shiftFunctor D n).map ((commShiftIso (G.flip.obj X₂) m).hom.app (F.obj X₁')) =
    (G.map ((commShiftIso F m).hom.app X₁')).app ((shiftFunctor C₂ n).obj X₂) ≫
      (commShiftIso (G.flip.obj ((shiftFunctor C₂ n).obj X₂)) m).hom.app (F.obj X₁') ≫
        (shiftFunctor D m).map ((commShiftIso (G.obj (F.obj X₁')) n).hom.app X₂) ≫
          (shiftFunctorComm D m n).inv.app ((G.obj (F.obj X₁')).obj X₂) ≫
            (↑(h.ε m n)).app ((shiftFunctor D n).obj ((shiftFunctor D m).obj ((G.obj (F.obj X₁')).obj X₂)))

Tactic:
simp [this]

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

Goal state before:
pp: case pos.e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
K : HomologicalComplex₂ C (up ℤ) (up ℤ)
y : ℤ
inst✝ : K.HasTotal (up ℤ)
n₀ n₁ n₀' n₁' : ℤ
h₀ : n₀ + y = n₀'
h₁ : n₁ + y = n₁'
h : n₀ + 1 = n₁
p q : ℤ
hpq : p + q = n₀
⊢ (p + 1) * y = y + p * y

Tactic:
linarith

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
n : ℤ
hK : HomologicalComplex.ExactAt K n
m : ℤ
hm : n + m = 0
⊢ HomologicalComplex.ExactAt ((opEquivalence C).functor.obj (op K)) m

Tactic:
obtain rfl : n = -m := by lia

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
m : ℤ
hK : HomologicalComplex.ExactAt K (-m)
hm : -m + m = 0
⊢ HomologicalComplex.ExactAt ((opEquivalence C).functor.obj (op K)) m
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m p : ℤ
hm : n + 1 = m
hp : m + 1 = p
⊢ (Cocycle.isKernel K L m p hp).lift (KernelFork.ofι (HomologicalComplex.sc' (K.HomComplex L) n m p).f ⋯) ≫
      AddCommGrpCat.ofHom (CohomologyClass.mkAddMonoidHom K L m) =
    0

Tactic:
by
    ext x
    dsimp
    rw [CohomologyClass.mk_eq_zero_iff]
    exact ⟨n, hm, x, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.Orthogonal

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
D : Type u'
inst✝⁴ : Category.{v', u'} D
P : ObjectProperty C
M : Type u_1
inst✝³ : AddGroup M
inst✝² : HasShift C M
inst✝¹ : HasZeroMorphisms C
inst✝ : P.IsStableUnderShift M
n : M
Y : C
hY : P.rightOrthogonal Y
X : C
f : X ⟶ (shiftFunctor C n).obj Y
hX : P X
⊢ f = 0

Tactic:
obtain ⟨g, rfl⟩ := ((shiftEquiv C n).symm.toAdjunction.homEquiv _ _).surjective f
    simp [hY g (P.le_shift (-n) _ hX), Adjunction.homEquiv_unit]

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : 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
j' : ι'
i : ι
hij' : ¬c'.Rel j' (e.f i)
hj' : ¬∃ j, e.f j = j'
⊢ ∀ (j : ι), e.f j ≠ j'

Tactic:
tauto

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : 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 j' i'
hi' : ¬∃ i, e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
tauto

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : 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 j' i'
⊢ extend.hom e h.hom i' j' = 0

Tactic:
by
    by_cases hi' : ∃ i, e.f i = i'
    · obtain ⟨i, rfl⟩ := hi'
      by_cases hj' : ∃ j, e.f j = j'
      · obtain ⟨j, rfl⟩ := hj'
        rw [extend.hom_eq _ _ rfl rfl, h.zero _ _ (by rwa [← e.rel_iff]),
          zero_comp, comp_zero]
      · exact extend.hom_eq_zero₂ _ _ _ _ (by tauto)
    · exact extend.hom_eq_zero₁ _ _ _ _ (by tauto)

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

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : 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' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
tauto

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

Goal state before:
pp: case inl
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.sc' K n (n + 1) (n + 2)).Exact
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) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p : ℤ
hp✝ : p ≤ n + 1
hpq : p + 0 = p
hp : p < n + 1
⊢ (Cochain.ofHom f).v p p ⋯ + (δ (-1) 0 (Cochain.single β (-1))).v p p hpq = (Cochain.ofHom f).v p p hpq

Tactic:
add_eq_left,

Goal state after:
case inl
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.sc' K n (n + 1) (n + 2)).Exact
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) ⋯
hu : K.d n (n + 1) ≫ u = 0
β : K.X (n + 2) ⟶ L.X (n + 1)
hβ : K.d (n + 1) (n + 2) ≫ β = u
p : ℤ
hp✝ : p ≤ n + 1
hpq : p + 0 = p
hp : p < n + 1
⊢ (δ (-1) 0 (Cochain.single β (-1))).v p p hpq = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
j' : ι'
i : ι
hj' : ¬∃ j, e.f j = j'
⊢ ∀ (i : ι), e.f i ≠ j'

Tactic:
tauto

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 ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
k : ℕ
x : ↑(X k)
p q : ℤ
hpq : p + -1 = q
hp : p ≤ d + ↑k
⊢ (↑x).v p q hpq + (Cochain.single ⋯.choose (-1)).v p q hpq = (↑x).v p q hpq

Tactic:
add_eq_left,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Abelian C
L : CochainComplex C ℤ
d : ℤ
inst✝¹ : L.IsStrictlyGE d
inst✝ : ∀ (n : ℤ), Injective (L.X n)
K : CochainComplex C ℤ
f : K ⟶ L
hK : HomologicalComplex.Acyclic K
X : ℕ → Set (Cochain K L (-1)) := fun n ↦ {α | (δ (-1) 0 α).EqUpTo (Cochain.ofHom f) (↑n + d - 1)}
x₀ : ↑(X 0) := ⟨0, ⋯⟩
φ : (n : ℕ) → ↑(X n) → ↑(X (n + 1)) := fun n α ↦ ⟨↑α + Cochain.single ⋯.choose (-1), ⋯⟩
k : ℕ
x : ↑(X k)
p q : ℤ
hpq : p + -1 = q
hp : p ≤ d + ↑k
⊢ (Cochain.single ⋯.choose (-1)).v p q hpq = 0
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomotopy

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroObject C
inst✝¹ : Preadditive C
K L : HomologicalComplex C c
f g : K ⟶ L
e : c.Embedding c'
inst✝ : e.IsRelIff
h : Homotopy (extendMap f e) (extendMap g e)
i' j' : ι'
hi' : ¬∃ i, e.f i = i'
⊢ ∀ (i : ι), e.f i ≠ i'

Tactic:
tauto

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝¹ : W₁.HasFactorization W₂
inst✝ : W₁.IsStableUnderRetracts
h₁ : W₁ ≤ W₂.llp
A B : C
i : A ⟶ B
hi : W₂.llp i
⊢ W₁ i

Tactic:
by
    have h := factorizationData W₁ W₂ i
    have := hi _ h.hp
    simpa using of_retract (RetractArrow.ofLeftLiftingProperty h.fac) h.hi

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : Cofibration i
hp : Fibration p ∧ WeakEquivalence p
⊢ HasLiftingProperty i p

Tactic:
have := hp.1

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
hi : Cofibration i
hp : Fibration p ∧ WeakEquivalence p
this : Fibration p
⊢ HasLiftingProperty i p
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
P : PathObject Y
left✝ : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject Z
h✝ : Q.IsVeryGood
sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
this : sq.lift ≫ Q.p₀ = P.p₀ ≫ p
⊢ (h.h ≫ sq.lift) ≫ Q.p₀ = f ≫ p

Tactic:
simp [this]

Goal state after:
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
P : PathObject Y
left✝ : P.IsVeryGood
h : P.RightHomotopy f g
Q : PathObject Z
h✝ : Q.IsVeryGood
sq : CommSq (p ≫ Q.ι) P.ι Q.p (prod.lift (P.p₀ ≫ p) (P.p₁ ≫ p))
this : sq.lift ≫ Q.p₁ = P.p₁ ≫ p
⊢ (h.h ≫ sq.lift) ≫ Q.p₁ = g ≫ p

Tactic:
simp [this]

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
n : ℤ
⊢ (t.truncGT n).Additive

Tactic:
by
  dsimp only [truncGT]
  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 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✝

Tactic:
dsimp [truncGTδLE]

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.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✝
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 : ℤ
X : C
⊢ t.IsLE X n ↔ IsZero ((t.truncGT n).obj X)

Tactic:
rw [t.isLE_iff_isIso_truncLEι_app n X]
  exact (Triangle.isZero₃_iff_isIso₁ _ (t.triangleLEGT_distinguished n X)).symm

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
X Y : C
f : X ⟶ Y
n : ℤ
x✝ : ∃ Z g h, ∃ (_ : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles), t.IsGE Z n
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj ((t.truncLT n).obj X)
mem : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ∈ distinguishedTriangles
h✝ : t.IsGE Z n
e : Triangle.mk ((t.truncLTι n).app X ≫ f) g h ≅ (t.triangleLTGE n).obj Y
he : e.hom.hom₂ = (Iso.refl (Triangle.mk ((t.truncLTι n).app X ≫ f) g h).obj₂).hom
this : (t.truncLT n).map f = e.hom.hom₁
⊢ IsIso ((t.truncLT n).map f)

Tactic:
rw [this]; infer_instance

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
Y Z : C
g : Y ⟶ Z
n₀ n₁ : ℤ
hn : n₀ + 1 = n₁
x✝ : ∃ X f h, ∃ (_ : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles), t.IsLE X n₀
X : C
f : X ⟶ Y
h : (t.truncGE n₁).obj Z ⟶ (shiftFunctor C 1).obj X
mem : Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h ∈ distinguishedTriangles
h✝ : t.IsLE X n₀
e : (t.triangleLTGE n₁).obj Y ≅ Triangle.mk f (g ≫ (t.truncGEπ n₁).app Z) h
he : e.hom.hom₂ = (Iso.refl ((t.triangleLTGE n₁).obj Y).obj₂).hom
this : (t.truncGE n₁).map g = e.hom.hom₃
⊢ IsIso ((t.truncGE n₁).map g)

Tactic:
rw [this]; infer_instance

Goal state after:
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this✝¹ : Epi π
this✝ : Mono ι
n : ℤ
this :
  (↑(cocycle₁' sq hsq)).v n (n + 1) ⋯ ≫ X.d (n + 1) (n + 2) +
      1 • B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq)).v (n + 1) (n + 2) ⋯ =
    0
⊢ (cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) +
      1 • Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯ =
    0

Tactic:
one_smul

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
this✝¹ : Epi π
this✝ : Mono ι
n : ℤ
this :
  (↑(cocycle₁' sq hsq)).v n (n + 1) ⋯ ≫ X.d (n + 1) (n + 2) +
      B.d n (n + 1) ≫ (↑(cocycle₁' sq hsq)).v (n + 1) (n + 2) ⋯ =
    0
⊢ (cochain₁ sq hsq hQ hK).v n (n + 1) ⋯ ≫ K.d (n + 1) (n + 2) +
      Q.d n (n + 1) ≫ (cochain₁ sq hsq hQ hK).v (n + 1) (n + 2) ⋯ =
    0
Module: Mathlib.Algebra.Homology.ModelCategory.Lifting

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
A B X Y : CochainComplex C ℤ
t : A ⟶ X
i : A ⟶ B
p : X ⟶ Y
b : B ⟶ Y
sq : CommSq t i p b
hsq : (n : ℤ) → ⋯.LiftStruct
Q : CochainComplex C ℤ
π : B ⟶ Q
hπ : i ≫ π = 0
hQ : IsColimit (CokernelCofork.ofπ π hπ)
K : CochainComplex C ℤ
ι : K ⟶ X
hι : ι ≫ p = 0
hK : IsLimit (KernelFork.ofι ι hι)
α : Cochain Q K 0
hα : (Cochain.ofHom π).comp ((δ 0 1 α).comp (Cochain.ofHom ι) ⋯) ⋯ = ↑(cocycle₁' sq hsq)
l : Cocycle B X 0 := Cocycle.mk (cochain₀ sq hsq - (Cochain.ofHom π).comp (α.comp (Cochain.ofHom ι) ⋯) ⋯) 1 ⋯ ⋯
n : ℤ
h₁ : i.f n ≫ π.f n = 0
h₂ : i.f n ≫ (hsq n).l = t.f n
⊢ (i ≫ l.homOf).f n = t.f n

Tactic:
simp [l, reassoc_of% h₁, h₂]

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

Goal state before:
pp: case pos
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
a b : ℤ
X : C
h : a ≤ b
u₁₂ : (t.truncLT a).obj X ⟶ (t.truncLT b).obj X := (t.natTransTruncLTOfLE a b h).app X
u₂₃ : (t.truncLT b).obj X ⟶ X := (t.truncLTι b).app X
u₁₃ : (t.truncLT a).obj X ⟶ X := (t.truncLTι a).app X
eq : u₁₂ ≫ u₂₃ = u₁₃
H : Octahedron eq ⋯ ⋯ ⋯
m₁ : (t.truncGELT a b).obj X ⟶ (t.truncGE a).obj X := H.m₁
this : IsIso ((t.truncLT b).map H.m₁)
eq' : t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncGELTToLTGE a b).app X
fac : (t.truncLTι b).app ((t.truncGE a).obj ((t.truncLT b).obj X)) ≫ t.liftTruncLT m₁ (b - 1) b ⋯ = (t.truncLT b).map m₁
⊢ IsIso (t.liftTruncLT m₁ (b - 1) b ⋯)

Tactic:
exact IsIso.of_isIso_fac_left fac

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
f g : X ⟶ Y
inst✝¹ : IsCofibrant X
h✝ : LeftHomotopyRel f g
Q : PathObject Y
inst✝ : Q.IsGood
P : Cylinder X := ⋯.choose
h : ⋯.choose.LeftHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (f ≫ Q.ι) P.i₀ Q.p (prod.lift (P.π ≫ f) h.h)
this : sq.lift ≫ Q.p₀ = P.π ≫ f
⊢ (P.i₁ ≫ sq.lift) ≫ Q.p₀ = f

Tactic:
simp [this]

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
f g : X ⟶ Y
inst✝¹ : IsCofibrant X
h✝ : LeftHomotopyRel f g
Q : PathObject Y
inst✝ : Q.IsGood
P : Cylinder X := ⋯.choose
h : ⋯.choose.LeftHomotopy f g
h' : ⋯.choose.IsGood
sq : CommSq (f ≫ Q.ι) P.i₀ Q.p (prod.lift (P.π ≫ f) h.h)
this : sq.lift ≫ Q.p₁ = h.h
⊢ (P.i₁ ≫ sq.lift) ≫ Q.p₁ = g

Tactic:
simp [this]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
W : MorphismProperty C
homRel : HomRel C
inst✝² : HomRel.IsStableUnderPrecomp homRel
inst✝¹ : HomRel.IsStableUnderPostcomp homRel
inst✝ : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
⊢ W.quotient homRel ((Quotient.functor homRel).map f) ↔ W f

Tactic:
refine ⟨fun ⟨f', hf', h⟩ ↦ ?_, fun hf ↦ ⟨f, hf, rfl⟩⟩

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
W : MorphismProperty C
homRel : HomRel C
inst✝² : HomRel.IsStableUnderPrecomp homRel
inst✝¹ : HomRel.IsStableUnderPostcomp homRel
inst✝ : W.HasQuotient homRel
X Y : C
f : X ⟶ Y
x✝ : W.quotient homRel ((Quotient.functor homRel).map f)
f' : ((Quotient.functor homRel).1 X).as ⟶ ((Quotient.functor homRel).1 Y).as
hf' : W f'
h : (Quotient.functor homRel).map f = (Quotient.functor homRel).map f'
⊢ W f
Module: Mathlib.CategoryTheory.MorphismProperty.Quotient

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
W : MorphismProperty C
homRel : HomRel C
inst✝² : HomRel.IsStableUnderPrecomp homRel
inst✝¹ : HomRel.IsStableUnderPostcomp homRel
inst✝ : W.HasQuotient homRel
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
⊢ W f✝ ↔ (W.quotient homRel).inverseImage (Quotient.functor homRel) f✝

Tactic:
exact (quotient_iff _ _ _).symm

Goal state after: