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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p

pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p

Tactic:
· intro h X p hp
    have : HasEqualizer (𝟙 X) (𝟙 X - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
    convert! hasKernel_of_hasEqualizer (𝟙 X) (𝟙 X - p)
    rw [sub_sub_cancel]

Goal state after:
case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ (∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p) → ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasEqualizer (𝟙 X) p
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
⊢ IsIdempotentComplete D

Tactic:
by
  refine ⟨?_⟩
  intro X' p hp
  let φ := ε.counitIso.symm.app X'
  simp only [Functor.id_obj] at φ
  rw [split_iff_of_iso φ p (φ.inv ≫ p ≫ φ.hom)
      (by
        slice_rhs 1 2 => rw [φ.hom_inv_id]
        rw [id_comp])]
  rcases IsIdempotentComplete.idempotents_split (ε.inverse.obj X') (ε.inverse.map p)
      (by rw [← ε.inverse.map_comp, hp]) with
    ⟨Y, i, e, ⟨h₁, h₂⟩⟩
  use ε.functor.obj Y, ε.functor.map i, ε.functor.map e
  constructor
  · rw [← ε.functor.map_comp, h₁, ε.functor.map_id]
  · simp only [← ε.functor.map_comp, h₂, Equivalence.fun_inv_map]
    rfl

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

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ δ (i.castLT ⋯) ≫ δ j.succ = δ j ≫ δ i

Tactic:
rw [δ_comp_δ]

Goal state after:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ δ j ≫ δ (i.castLT ⋯).castSucc = δ j ≫ δ i

n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : i ≤ j.castSucc
⊢ i.castLT ⋯ ≤ j
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X : J ⥤ C
⊢ autoParam
    (∀ (X_1 Y : J) (f : X_1 ⟶ Y),
      ((toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).obj X).map f =
        eqToHom ⋯ ≫ (((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).obj X).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
intro j j' φ
      ext
      simp

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ δ i.succ ≫ σ i = 𝟙 ⦋n⦌

Tactic:
ext j
  rcases i with ⟨i, _⟩
  rcases j with ⟨j, _⟩
  dsimp [δ, σ, Fin.succAbove, Fin.predAbove]
  split_ifs <;> simp <;> simp at * <;> lia

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h_obj
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ ∀ (X : SimplicialObject C),
    (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).obj X =
      ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).obj X

Tactic:
intro X
    apply HomologicalComplex.ext
    · rintro i j (rfl : j + 1 = i)
      dsimp only [Functor.comp_obj]
      simp only [Functor.mapHomologicalComplex_obj_d, alternatingFaceMapComplex_obj_d,
        eqToHom_refl, id_comp, comp_id, AlternatingFaceMapComplex.objD, Functor.map_sum,
        Functor.map_zsmul]
      rfl
    · ext n
      rfl

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

Goal state before:
pp: case pos
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' :
  ¬(ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
      (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂
⊢ y₂ ≤ y₁

Tactic:
convert! f.toOrderHom.monotone (le_of_not_ge h'')

Goal state after:
case e'_3
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' :
  ¬(ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
      (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂
⊢ y₂ = (Hom.toOrderHom f) ((ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂)

case e'_4
A✝ B✝ : SimplexCategory
f : A✝ ⟶ B✝
hf : IsIso ((forget SimplexCategory).map f)
y₁ y₂ : Fin (B✝.len + 1)
h : y₁ ≤ y₂
h' : y₁ < y₂
h'' :
  ¬(ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁ ≤
      (ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₂
⊢ y₁ = (Hom.toOrderHom f) ((ConcreteCategory.hom (inv ((forget SimplexCategory).map f))) y₁)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: Δ Δ' Δ'' : SimplexCategory
φ : Δ ⟶ Δ''
e : Δ ⟶ Δ'
inst✝¹ : Epi e
i : Δ' ⟶ Δ''
inst✝ : Mono i
fac : e ≫ i = φ
⊢ image φ = Δ'

Tactic:
by
  have := strongEpi_of_epi e
  let e := image.isoStrongEpiMono e i fac
  ext
  exact le_antisymm (len_le_of_epi e.hom) (len_le_of_mono e.hom)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nerve

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
h₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) = ComposableArrows.mk₁ f₁₂
h₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
h'₀ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 1 2 δ₂_two._proof_3 δ₂_zero._proof_1) =
    ComposableArrows.mk₁ f₁₂
h'₂ :
  ComposableArrows.mk₁ (ComposableArrows.map' h'.simplex 0 1 δ₂_two._proof_1 δ₂_two._proof_3) = ComposableArrows.mk₁ f₀₁
⊢ ComposableArrows.arrowEquiv.symm (Arrow.mk (ComposableArrows.map' h'.simplex 1 2 _proof_246✝ _proof_247✝)) =
    ComposableArrows.arrowEquiv.symm (Arrow.mk (ComposableArrows.map' h.simplex 1 2 _proof_246✝ _proof_247✝))

Tactic:
by simp [-Edge.CompStruct.d₀, h'₀, ← h₀]

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ C.d (i + 2) 0 = 0

Tactic:
rw [C.shape]

Goal state after:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
i : ℕ
⊢ ¬(ComplexShape.down ℕ).Rel (i + 2) 0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ C.d 0 (i + 2) = 0

Tactic:
rw [C.shape]

Goal state after:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
i : ℕ
⊢ ¬(ComplexShape.up ℕ).Rel 0 (i + 2)
Module: Mathlib.Algebra.Homology.HomologicalBicomplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
f : K.toGradedObject ⟶ L.toGradedObject
comm₁ : ∀ (i₁ i₁' : I₁) (i₂ : I₂), c₁.Rel i₁ i₁' → f (i₁, i₂) ≫ (L.d i₁ i₁').f i₂ = (K.d i₁ i₁').f i₂ ≫ f (i₁', i₂)
comm₂ : ∀ (i₁ : I₁) (i₂ i₂' : I₂), c₂.Rel i₂ i₂' → f (i₁, i₂) ≫ (L.X i₁).d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ f (i₁, i₂')
i₁ i₁' : I₁
h₁ : c₁.Rel i₁ i₁'
⊢ { f := fun i₂ ↦ f (i₁, i₂), comm' := ⋯ } ≫ L.d i₁ i₁' = K.d i₁ i₁' ≫ { f := fun i₂ ↦ f (i₁', i₂), comm' := ⋯ }

Tactic:
ext i₂
    exact comm₁ i₁ i₁' i₂ h₁

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₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
⊢ IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)

Tactic:
let c₁₂ := fun i₁₂ => (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂

Goal state after:
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₁₂
G : C₁₂ ⥤ C₃ ⥤ C₄
I₁ : Type u_7
I₂ : Type u_8
I₃ : Type u_9
J : Type u_10
r : I₁ × I₂ × I₃ → J
ρ₁₂ : BifunctorComp₁₂IndexData r
X₁ : GradedObject I₁ C₁
X₂ : GradedObject I₂ C₂
X₃ : GradedObject I₃ C₃
inst✝¹ : (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).HasMap ρ₁₂.p
inst✝ : (((mapBifunctor G ρ₁₂.I₁₂ I₃).obj (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂)).obj X₃).HasMap ρ₁₂.q
H : HasGoodTrifunctor₁₂Obj F₁₂ G ρ₁₂ X₁ X₂ X₃
j : J
c₁₂ : (i₁₂ : ρ₁₂.I₁₂) → (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).CofanMapObjFun ρ₁₂.p i₁₂ :=
  fun i₁₂ ↦ (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂).cofanMapObj ρ₁₂.p i₁₂
⊢ IsColimit (cofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K L : HomologicalComplex₂ C c₁ c₂
φ : K ⟶ L
c₁₂ : ComplexShape I₁₂
inst✝³ : TotalComplexShape c₁ c₂ c₁₂
inst✝² : DecidableEq I₁₂
inst✝¹ : K.HasTotal c₁₂
inst✝ : L.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
⊢ K.ιTotalOrZero c₁₂ i₁ i₂ i₁₂ ≫ (total.map φ c₁₂).f i₁₂ = (φ.f i₁).f i₂ ≫ L.ιTotalOrZero c₁₂ i₁ i₂ i₁₂

Tactic:
by
  simp [total.map, ιTotalOrZero]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
  (Homotopy.ofEq ⋯).trans
    ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
          (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
      (Homotopy.ofEq ⋯))
j j' : J
i₁ : I₁
i₂ : I₂
hj : c₁.π c₂ c (i₁, i₂) = j
⊢ K₁.ιMapBifunctor K₂ F c i₁ i₂ j hj ≫ hom₂ f₁ h₂ F c j j' = K₁.ιMapBifunctor K₂ F c i₁ i₂ j hj ≫ H.hom j j'

Tactic:
dsimp [H, mapBifunctorMapHomotopy₁]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
I₁ : Type u_4
I₂ : Type u_5
J : Type u_6
inst✝¹¹ : Category.{v_1, u_1} C₁
inst✝¹⁰ : Category.{v_2, u_2} C₂
inst✝⁹ : Category.{v_3, u_3} D
inst✝⁸ : Preadditive C₁
inst✝⁷ : Preadditive C₂
inst✝⁶ : Preadditive D
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K₁ L₁ : HomologicalComplex C₁ c₁
f₁ f₁' : K₁ ⟶ L₁
h₁ : Homotopy f₁ f₁'
K₂ L₂ : HomologicalComplex C₂ c₂
f₂ f₂' : K₂ ⟶ L₂
h₂ : Homotopy f₂ f₂'
F : C₁ ⥤ C₂ ⥤ D
inst✝⁵ : F.Additive
inst✝⁴ : ∀ (X₁ : C₁), (F.obj X₁).Additive
c : ComplexShape J
inst✝³ : DecidableEq J
inst✝² : TotalComplexShape c₁ c₂ c
inst✝¹ : K₁.HasMapBifunctor K₂ F c
inst✝ : L₁.HasMapBifunctor L₂ F c
this✝² : TotalComplexShape c₂ c₁ c := TotalComplexShape.symm c₁ c₂ c
this✝¹ : TotalComplexShapeSymmetry c₁ c₂ c := TotalComplexShape.symmSymmetry c₁ c₂ c
this✝ : F.flip.Additive
this : ∀ (X₁ : C₂), (F.flip.obj X₁).Additive
H : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁ f₂' F c) :=
  (Homotopy.ofEq ⋯).trans
    ((((mapBifunctorMapHomotopy₁ h₂ f₁ F.flip c).compRight (L₁.mapBifunctorFlipIso L₂ F c).hom).compLeft
          (K₁.mapBifunctorFlipIso K₂ F c).inv).trans
      (Homotopy.ofEq ⋯))
j j' : J
i₁ : I₁
i₂ : I₂
hj : c₁.π c₂ c (i₁, i₂) = j
⊢ K₁.ιMapBifunctor K₂ F c i₁ i₂ j hj ≫ hom₂ f₁ h₂ F c j j' =
    K₁.ιMapBifunctor K₂ F c i₁ i₂ j hj ≫
      (0 +
        ((K₁.mapBifunctorFlipIso K₂ F c).inv.f j ≫ hom₁ h₂ f₁ F.flip c j j' ≫ (L₁.mapBifunctorFlipIso L₂ F c).hom.f j' +
          0))
Module: Mathlib.Algebra.Homology.TotalComplexShift

Goal state before:
pp: case neg
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 : ¬(up ℤ).Rel n₀ n₁
⊢ ((shiftFunctor₂ C y).obj K).D₂ (up ℤ) n₀ n₁ ≫ (K.totalShift₂XIso y n₁ n₁' h₁).hom =
    y.negOnePow • (K.totalShift₂XIso y n₀ n₀' h₀).hom ≫ K.D₂ (up ℤ) n₀' n₁'

Tactic:
· rw [D₂_shape _ _ _ _ h, zero_comp, D₂_shape, comp_zero, smul_zero]
    simp_all only [up_Rel]
    grind

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : HasZeroMorphisms C₂
inst✝³ : Preadditive D
K₁ L₁ : CochainComplex C₁ ℤ
f₁ : K₁ ⟶ L₁
K₂ : CochainComplex C₂ ℤ
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms
x : ℤ
inst✝ : K₁.HasMapBifunctor K₂ F
i✝¹ j✝ : ℤ
a✝ : (ComplexShape.up ℤ).Rel i✝¹ j✝
i✝ : ℤ
⊢ 𝟙 ((F.obj (K₁.X (i✝¹ + x))).obj (K₂.X i✝)) ≫ (x.negOnePow • (F.map (K₁.d (i✝¹ + x) (j✝ + x))).app (K₂.X i✝)) =
    (F.map (x.negOnePow • K₁.d (i✝¹ + x) (j✝ + x))).app (K₂.X i✝) ≫ 𝟙 ((F.obj (K₁.X (j✝ + x))).obj (K₂.X i✝))

Tactic:
simp only [Linear.comp_units_smul, id_comp, Functor.map_units_smul,
      NatTrans.app_units_zsmul, comp_id]

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

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_3} D
inst✝⁵ : Preadditive C₁
inst✝⁴ : Preadditive C₂
inst✝³ : Preadditive D
F : C₁ ⥤ C₂ ⥤ D
inst✝² : F.Additive
inst✝¹ : ∀ (X₁ : C₁), (F.obj X₁).Additive
inst✝ : ∀ (K₁ : CochainComplex C₁ ℤ) (K₂ : CochainComplex C₂ ℤ), K₁.HasMapBifunctor K₂ F
K₁ : CochainComplex C₁ ℤ
K₂ : CochainComplex C₂ ℤ
p q : ℤ
this :
  (K₁.mapBifunctorShift₁Iso ((shiftFunctor (CochainComplex C₂ ℤ) q).obj K₂) F p).hom ≫
      (shiftFunctor (CochainComplex D ℤ) p).map (K₁.mapBifunctorShift₂Iso K₂ F q).hom =
    (p * q).negOnePow •
      (((shiftFunctor (CochainComplex C₁ ℤ) p).obj K₁).mapBifunctorShift₂Iso K₂ F q).hom ≫
        (shiftFunctor (CochainComplex D ℤ) q).map (K₁.mapBifunctorShift₁Iso K₂ F p).hom ≫
          (shiftFunctorComm (CochainComplex D ℤ) p q).hom.app (K₁.mapBifunctor K₂ F)
⊢ (commShiftIso (F.map₂CochainComplex.obj ((shiftFunctor (CochainComplex C₁ ℤ) p).obj K₁)) q).hom.app K₂ ≫
      (shiftFunctor (CochainComplex D ℤ) q).map ((commShiftIso (F.map₂CochainComplex.flip.obj K₂) p).hom.app K₁) =
    (commShiftIso (F.map₂CochainComplex.flip.obj ((shiftFunctor (CochainComplex C₂ ℤ) q).obj K₂)) p).hom.app K₁ ≫
      (shiftFunctor (CochainComplex D ℤ) p).map ((commShiftIso (F.map₂CochainComplex.obj K₁) q).hom.app K₂) ≫
        (shiftComm ((F.map₂CochainComplex.obj K₁).obj K₂) p q).inv ≫
          (↑(CommShift₂Setup.int.ε p q)).app
            ((shiftFunctor (CochainComplex D ℤ) q).obj
              ((shiftFunctor (CochainComplex D ℤ) p).obj ((F.map₂CochainComplex.obj K₁).obj K₂)))

Tactic:
simp [commShiftIso_map₂CochainComplex_hom_app,
      commShiftIso_map₂CochainComplex_flip_hom_app,
      reassoc_of% this, smul_smul]

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

Goal state before:
pp: case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := ⋯
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ Homotopy (Cocycle.equivHomShift.symm y₁) (Cocycle.equivHomShift.symm y₂)

Tactic:
apply HomotopyCategory.homotopyOfEq

Goal state after:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
K L : CochainComplex C ℤ
n : ℤ
inst✝ : HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
x : CohomologyClass K L n
this : HasDerivedCategory C := ⋯
y₁ y₂ : Cocycle K L n
h : y₁ ≈ y₂
⊢ (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (Cocycle.equivHomShift.symm y₁) =
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (Cocycle.equivHomShift.symm y₂)
Module: Mathlib.Algebra.Homology.HomotopyCategory.KInjective

Goal state before:
pp: case inr
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
hp : n + 1 ≤ n + 1
hpq : n + 1 + 0 = n + 1
⊢ (δ (-1) 0 (α + Cochain.single β (-1))).v (n + 1) (n + 1) hpq = (Cochain.ofHom f).v (n + 1) (n + 1) hpq

Tactic:
rw [δ_v (-1) 0 (neg_add_cancel 1) _ (n + 1) (n + 1) (by lia) n (n + 2)
      (by lia) (by lia), Cochain.add_v,
      Cochain.single_v_eq_zero _ _ _ _ _ (by lia)]
    simp [hβ, u]

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : CategoryWithCofibrations C
inst✝¹ : HasInitial C
inst✝ : (cofibrations C).RespectsIso
A X : C
i : A ⟶ X
hA : IsInitial A
⊢ IsCofibrant X ↔ Cofibration i

Tactic:
simp only [cofibration_iff]

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : CategoryWithCofibrations C
inst✝¹ : HasInitial C
inst✝ : (cofibrations C).RespectsIso
A X : C
i : A ⟶ X
hA : IsInitial A
⊢ cofibrations C (initial.to X) ↔ cofibrations C i
Module: Mathlib.AlgebraicTopology.ModelCategory.IsCofibrant

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : CategoryWithCofibrations C
inst✝² : HasInitial C
X Y : C
inst✝¹ : (cofibrations C).IsStableUnderCobaseChange
inst✝ : HasBinaryCoproduct X Y
hX : IsCofibrant X
⊢ Cofibration coprod.inr

Tactic:
by
  rw [isCofibrant_iff] at hX
  rw [cofibration_iff] at hX ⊢
  exact MorphismProperty.of_isPushout
    (IsPushout.of_isColimit_binaryCofan_of_isInitial
    (colimit.isColimit (pair X Y)) initialIsInitial) hX

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y : C
f : X ⟶ Y
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : IsIso f
⊢ Fibration f

Tactic:
have := (cofibrations C).rlp_of_isIso f

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : CategoryWithWeakEquivalences C
inst✝³ : CategoryWithCofibrations C
inst✝² : CategoryWithFibrations C
X Y : C
f : X ⟶ Y
inst✝¹ : (cofibrations C).IsWeakFactorizationSystem (trivialFibrations C)
inst✝ : IsIso f
this : (cofibrations C).rlp f
⊢ Fibration f
Module: Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : ModelCategory C
inst✝ : IsCofibrant X
f g : X ⟶ Y
⊢ mk f = mk g ↔ LeftHomotopyRel f g

Tactic:
rw [← (LeftHomotopyRel.equivalence X Y).eqvGen_iff]
  exact Quot.eq

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
⊢ ∀ {v₁₂ : X₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁}
    (h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles) {v₂₃ : X₃ ⟶ Z₂₃}
    {w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂} (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles)
    {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁}
    (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles),
    Nonempty (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
v₁₂

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasShift C ℤ
inst✝⁴ : HasZeroObject C
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : Cᵒᵖ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
⊢ ∀ {w₁₂ : Z₁₂ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁} (h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ Pretriangulated.distinguishedTriangles)
    {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₂}
    (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ Pretriangulated.distinguishedTriangles) {v₁₃ : X₃ ⟶ Z₁₃}
    {w₁₃ : Z₁₃ ⟶ (shiftFunctor Cᵒᵖ 1).obj X₁} (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ Pretriangulated.distinguishedTriangles),
    Nonempty (Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃)
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
⊢ plus C K.obj

Tactic:
exact K.property

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
F : C ⥤ D
inst✝ : F.Additive
K : HomologicalComplex C (ComplexShape.up ℤ)
n : ℤ
h✝ : CochainComplex.IsStrictlyGE K n
⊢ CochainComplex.plus D
    ((F.mapHomologicalComplex (ComplexShape.up ℤ)).obj ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj K).as)

Tactic:
exact ⟨n, inferInstanceAs (CochainComplex.IsStrictlyGE
        ((F.mapHomologicalComplex _).obj K) n)⟩

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

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
P : ObjectProperty C
t : TStructure C
inst✝ : P.IsTriangulated
h : P.HasInducedTStructure t
X Y : P.FullSubcategory
f : X ⟶ Y
hX : t.le 0 X.obj
hY : t.ge 1 Y.obj
⊢ P.ι.map f = P.ι.map 0

Tactic:
by
    rw [Functor.map_zero]
    exact t.zero' (P.ι.map f) hX hY

Goal state after: