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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' +
      m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (single (f ≫ L.d q q') m).v p'' q'' hpq'' + (m.negOnePow • single (K.d p' p ≫ f) m).v p'' q'' hpq''

Tactic:
units_smul_v

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' +
      m.negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (single (f ≫ L.d q q') m).v p'' q'' hpq'' + m.negOnePow • (single (K.d p' p ≫ f) m).v p'' q'' hpq''
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n m : ℤ
hm : n + 1 = m
p' q' : ℤ
hp' : p' + 1 = p
hq' : q + 1 = q'
p'' q'' : ℤ
hpq'' : p'' + m = q''
h : ¬p'' = p
⊢ (single f n).v p'' (q'' - 1) ⋯ ≫ L.d (q'' - 1) q'' = (single (f ≫ L.d q q') m).v p'' q'' hpq''

Tactic:
· rw [single_v_eq_zero _ _ _ _ _ h, single_v_eq_zero _ _ _ _ _ h, zero_comp]

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

Goal state before:
pp: case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''

Tactic:
by_cases h : p'' = p'

Goal state after:
case pos
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
h : p'' = p'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''

case neg
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p n p' q' : ℤ
hp' : p' + 1 = p
p'' q'' : ℤ
hpq'' : p'' + (n + 1) = q''
f : K.X p ⟶ L.X q''
hq' : q'' + 1 = q'
h : ¬p'' = p'
⊢ (n + 1).negOnePow • K.d p'' (p'' + 1) ≫ (single f n).v (p'' + 1) q'' ⋯ =
    (n + 1).negOnePow • (single (K.d p' p ≫ f) (n + 1)).v p'' q'' hpq''
Module: Mathlib.Algebra.Homology.HomotopyCategory.Shift

Goal state before:
pp: case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K L : CochainComplex C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i j : ℤ
hij : ¬(ComplexShape.up ℤ).Rel j i
hij' : (ComplexShape.up ℤ).Rel (j + n) (i + n)
⊢ False

Tactic:
dsimp at hij hij'

Goal state after:
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
D : Type u'
inst✝¹ : Category.{v', u'} D
inst✝ : Preadditive D
K L : CochainComplex C ℤ
φ₁ φ₂ : K ⟶ L
h : Homotopy φ₁ φ₂
n i j : ℤ
hij : ¬j + 1 = i
hij' : j + n + 1 = i + n
⊢ False
Module: Mathlib.CategoryTheory.Shift.CommShift

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
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
eq :
  F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (commShiftIso F (a + b)).hom.app X =
    (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)
⊢ F.map ((shiftFunctorComm C a b).hom.app X) =
    (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫
        (shiftFunctorComm D a b).hom.app (F.obj X) ≫
          (shiftFunctor D a).map ((commShiftIso F b).inv.app X) ≫ (commShiftIso F a).inv.app ((shiftFunctor C b).obj X)

Tactic:
simp only [shiftFunctorComm_eq D a b _ rfl]

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
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
eq :
  F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (commShiftIso F (a + b)).hom.app X =
    (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫ (shiftFunctorAdd D a b).inv.app (F.obj X)
⊢ F.map ((shiftFunctorComm C a b).hom.app X) =
    (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
      (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫
        ((shiftFunctorAdd' D a b (a + b) ⋯).symm ≪≫ shiftFunctorAdd' D b a (a + b) ⋯).hom.app (F.obj X) ≫
          (shiftFunctor D a).map ((commShiftIso F b).inv.app X) ≫ (commShiftIso F a).inv.app ((shiftFunctor C b).obj X)
Module: Mathlib.CategoryTheory.Shift.CommShift

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
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
inst✝⁴ : HasShift D A
inst✝³ : F₁.CommShift A
inst✝² : F₂.CommShift A
inst✝¹ : IsIso τ
inst✝ : CommShift τ A
⊢ CommShift (inv τ) A

Tactic:
by
  have : NatTrans.CommShift (asIso τ).hom A := by assumption
  change NatTrans.CommShift (asIso τ).inv A
  infer_instance

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

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 M : CochainComplex C ℤ
n✝ n' a : ℤ
γ : Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
⊢ δ n (n + 1) ((↑γ).leftUnshift n hn) = 0

Tactic:
Cochain.δ_leftUnshift _ n hn (n + 1) (n + 1 + a) rfl,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L M : CochainComplex C ℤ
n✝ n' a : ℤ
γ : Cocycle ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
⊢ a.negOnePow • (δ n' (n + 1 + a) ↑γ).leftUnshift (n + 1) ⋯ = 0
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
n : ℤ
H : ℤ → Prop := fun n ↦ ∀ T ∈ distinguishedTriangles, (shiftFunctor C n).obj T ∈ distinguishedTriangles
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
⊢ H n

Tactic:
obtain (n | n) := n

Goal state after:
case ofNat
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
H : ℤ → Prop := fun n ↦ ∀ T ∈ distinguishedTriangles, (shiftFunctor C n).obj T ∈ distinguishedTriangles
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
n : ℕ
⊢ H (Int.ofNat n)

case negSucc
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
H : ℤ → Prop := fun n ↦ ∀ T ∈ distinguishedTriangles, (shiftFunctor C n).obj T ∈ distinguishedTriangles
H_zero : H 0
H_one : H 1
H_neg_one : H (-1)
H_add : ∀ {a b c : ℤ}, H a → H b → a + b = c → H c
n : ℕ
⊢ H (Int.negSucc n)
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp ↦ ihp ≫ Φ.map f.toPath) p
⊢ Φ.map (p.cons f') = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp ↦ ihp ≫ Φ.map f.toPath) p ≫ Φ.map f'.toPath

Tactic:
have : Φ.map (Quiver.Path.cons p f') = Φ.map p ≫ Φ.map (Quiver.Hom.toPath f') := by
        convert! Functor.map_comp Φ p (Quiver.Hom.toPath f')

Goal state after:
case h_map.cons
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
X Y b✝ c✝ : Paths V
p : Quiver.Path X b✝
f' : b✝ ⟶ c✝
ih : Φ.map p = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp ↦ ihp ≫ Φ.map f.toPath) p
this : Φ.map (p.cons f') = Φ.map p ≫ Φ.map f'.toPath
⊢ Φ.map (p.cons f') = Quiver.Path.rec (𝟙 (Φ.obj X)) (fun {b c} x f ihp ↦ ihp ≫ Φ.map f.toPath) p ≫ Φ.map f'.toPath
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
D₁ : Type u₄
D₂ : Type u₅
inst✝⁶ : Category.{v₁, u₁} C₁
inst✝⁵ : Category.{v₂, u₂} C₂
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝² : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝¹ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝ : CatCommSq Φ.functor L₁ L₂ G
hG : G.FullyFaithful
⊢ Nonempty G.FullyFaithful

Tactic:
exact ⟨hG⟩

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteProducts
J : Type u_2
inst✝ : Finite J
f : J → C
F : Fan f
hF : IsLimit F
h : ∀ (j : J), P (f j)
⊢ ∀ (j : Discrete J), P ((Discrete.functor f).obj j)

Tactic:
by intro ⟨j⟩; exact h j

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst✝ : Finite J
f : J → C
F : Cofan f
hF : IsColimit F
h : ∀ (j : J), P (f j)
⊢ ∀ (j : Discrete J), P ((Discrete.functor f).obj j)

Tactic:
by intro ⟨j⟩; exact h j

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
⊢ Hom.comp (homMk z₁) (homMk z₂) = homMk (z₁.comp₀ z₂ z₃)

Tactic:
rw [Hom.comp_eq, comp_eq z₁ z₂ z₃ h₃]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ (Q W).map f ≫ Qinv s hs = homMk { Y' := Y', f := f, s := s, hs := hs }

Tactic:
by
  dsimp only [Q_map, Qinv]
  rw [homMk_comp_homMk (ofHom W f) (ofInv s hs) (ofHom W (𝟙 _)) (by simp)]
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
Z : C
t₁ : (LeftFraction.ofHom W f₁).Y' ⟶ Z
t₂ : (LeftFraction.ofHom W f₂).Y' ⟶ Z
hst : (LeftFraction.ofHom W f₁).s ≫ t₁ = (LeftFraction.ofHom W f₂).s ≫ t₂
hft : (LeftFraction.ofHom W f₁).f ≫ t₁ = (LeftFraction.ofHom W f₂).f ≫ t₂
ht : W ((LeftFraction.ofHom W f₁).s ≫ t₁)
⊢ ∃ Z s, ∃ (_ : W s), f₁ ≫ s = f₂ ≫ s

Tactic:
dsimp at t₁ t₂ hst hft ht

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ : X ⟶ Y
Z : C
t₁ t₂ : Y ⟶ Z
hst : 𝟙 Y ≫ t₁ = 𝟙 Y ≫ t₂
hft : f₁ ≫ t₁ = f₂ ≫ t₂
ht : W (𝟙 Y ≫ t₁)
⊢ ∃ Z s, ∃ (_ : W s), f₁ ≫ s = f₂ ≫ s
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
Y Z✝ : C
f₁ f₂ : Y ⟶ Z✝
Z : C
t₁ : Z ⟶ (RightFraction.ofHom W f₁).X'
t₂ : Z ⟶ (RightFraction.ofHom W f₂).X'
hst : t₁ ≫ (RightFraction.ofHom W f₁).s = t₂ ≫ (RightFraction.ofHom W f₂).s
hft : t₁ ≫ (RightFraction.ofHom W f₁).f = t₂ ≫ (RightFraction.ofHom W f₂).f
ht : W (t₁ ≫ (RightFraction.ofHom W f₁).s)
⊢ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂

Tactic:
dsimp at t₁ t₂ hst hft ht

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
Y Z✝ : C
f₁ f₂ : Y ⟶ Z✝
Z : C
t₁ t₂ : Z ⟶ Y
hst : t₁ ≫ 𝟙 Y = t₂ ≫ 𝟙 Y
hft : t₁ ≫ f₁ = t₂ ≫ f₂
ht : W (t₁ ≫ 𝟙 Y)
⊢ ∃ X s, ∃ (_ : W s), s ≫ f₁ = s ≫ f₂
Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
K : C
⊢ (induced.shiftIso L G M F' e' (m + n) a a'' ⋯).hom.app (L.obj K) =
    (F' a).map ((shiftFunctorAdd D m n).hom.app (L.obj K)) ≫
      𝟙 ((F' a).obj ((shiftFunctor D n).obj ((shiftFunctor D m).obj (L.obj K)))) ≫
        (induced.shiftIso L G M F' e' n a a' ha').hom.app ((shiftFunctor D m).obj (L.obj K)) ≫
          (induced.shiftIso L G M F' e' m a' a'' ha'').hom.app (L.obj K)

Tactic:
simp only [id_comp, induced.shiftIso_hom_app_obj,
      G.shiftIso_add_hom_app n m a a' a'' ha' ha'', L.commShiftIso_add,
      comp_obj, CommShift.isoAdd_inv_app, (F' a).map_comp, assoc,
      ← (e' a).hom.naturality_assoc, comp_map]

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
K : C
⊢ (F' a).map ((shiftFunctorAdd D m n).hom.app (L.obj K)) ≫
      (F' a).map ((shiftFunctor D n).map ((commShiftIso L m).inv.app K)) ≫
        (F' a).map ((commShiftIso L n).inv.app ((shiftFunctor C m).obj K)) ≫
          (F' a).map (L.map ((shiftFunctorAdd C m n).inv.app K)) ≫
            (F' a).map (L.map ((shiftFunctorAdd C m n).hom.app K)) ≫
              (e' a).hom.app ((shiftFunctor C n).obj ((shiftFunctor C m).obj K)) ≫
                (G.shiftIso n a a' ha').hom.app ((shiftFunctor C m).obj K) ≫
                  (G.shiftIso m a' a'' ha'').hom.app K ≫ (e' a'').inv.app K =
    (F' a).map ((shiftFunctorAdd D m n).hom.app (L.obj K)) ≫
      (induced.shiftIso L G M F' e' n a a' ha').hom.app ((shiftFunctor D m).obj (L.obj K)) ≫
        (F' a').map ((commShiftIso L m).inv.app K) ≫
          (e' a').hom.app ((shiftFunctor C m).obj K) ≫ (G.shiftIso m a' a'' ha'').hom.app K ≫ (e' a'').inv.app K
Module: Mathlib.Algebra.Homology.Embedding.ExtendHomology

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✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk'✝ : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
hk' : e.f k = k'
⊢ φ ≫ K.d j k = 0 ↔ φ ≫ K.d j k ≫ (K.extendXIso e hk').inv = 0

Tactic:
← cancel_mono (K.extendXIso e hk').inv,

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✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
K : HomologicalComplex C c
e : c.Embedding c'
j k : ι
j' k' : ι'
hj' : e.f j = j'
hk : c.next j = k
hk'✝ : c'.next j' = k'
W : C
φ : W ⟶ K.X j
hjk : c.Rel j k
hk' : e.f k = k'
⊢ (φ ≫ K.d j k) ≫ (K.extendXIso e hk').inv = 0 ≫ (K.extendXIso e hk').inv ↔ φ ≫ K.d j k ≫ (K.extendXIso e hk').inv = 0
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K K' : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
α : K' ⟶ K
ψ : K ⟶ L.extend e
⊢ e.homRestrict (α ≫ ψ) = restrictionMap α e ≫ e.homRestrict ψ

Tactic:
ext i
  simp [homRestrict_f _ _ rfl, restrictionXIso]

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

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✝⁶ : HasZeroMorphisms C
K L M : HomologicalComplex C c'
φ : K ⟶ L
φ' : L ⟶ M
e : c.Embedding c'
inst✝⁵ : e.IsTruncGE
inst✝⁴ : ∀ (i' : ι'), K.HasHomology i'
inst✝³ : ∀ (i' : ι'), L.HasHomology i'
inst✝² : ∀ (i' : ι'), M.HasHomology i'
inst✝¹ : HasZeroObject C
inst✝ : K.IsStrictlySupported e
this : ∀ (i' : ι'), IsIso ((K.πTruncGE e).f i')
⊢ IsIso (K.πTruncGE e)

Tactic:
by
    apply Hom.isIso_of_components

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

Goal state before:
pp: case mpr
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝⁴ : Category.{v_1, u_3} C
inst✝³ : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝² : e.IsTruncGE
inst✝¹ : ∀ (i' : ι'), K.HasHomology i'
inst✝ : HasZeroObject C
⊢ K.IsSupportedOutside e → (K.truncGE e).Acyclic

Tactic:
intro hK i'
    by_cases hi' : ∃ i, e.f i = i'
    · obtain ⟨i, rfl⟩ := hi'
      simpa only [← exactAt_iff_of_quasiIsoAt (K.πTruncGE e)] using hK.exactAt i
    · exact exactAt_of_isSupported _ e i' (by simpa using hi')

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : HasZeroMorphisms C
K : CochainComplex C ℤ
inst✝¹ : HasZeroObject C
inst✝ : ∀ (i : ℤ), HasHomology K i
n q : ℤ
hq : q ≤ n
⊢ QuasiIsoAt (K.ιTruncLE n) q

Tactic:
by
  obtain ⟨k, rfl⟩ := Int.le.dest hq
  exact HomologicalComplex.quasiIsoAt_ιTruncLE (j := k) _ _ (by simp)

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

Goal state before:
pp: case mpr
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
K : CochainComplex C ℤ
n : ℤ
⊢ (∀ (i : ℤ), autoParam (i < n) isStrictlyGE_iff._auto_1 → IsZero (K.X i)) → K.IsStrictlyGE n

Tactic:
· intro h
    refine IsStrictlySupported.mk (fun i hi ↦ ?_)
    rw [notMem_range_embeddingUpIntGE_iff] at hi
    exact h i hi

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
X Y : CochainComplex C ℤ
f : Q.obj X ⟶ Q.obj Y
⊢ ∃ X' s, ∃ (x : IsIso (Q.map s)), ∃ g, f = inv (Q.map s) ≫ Q.map g

Tactic:
by
  have ⟨φ, hφ⟩ := Localization.exists_rightFraction Qh (HomotopyCategory.quasiIso C _) f
  obtain ⟨X', s, hs, g, rfl⟩ := φ.cases
  obtain ⟨X', rfl⟩ := HomotopyCategory.quotient_obj_surjective X'
  obtain ⟨s, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective s
  obtain ⟨g, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective g
  rw [← isIso_Qh_map_iff] at hs
  exact ⟨X', s, hs, g, hφ⟩

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

Goal state before:
pp: case refine_2
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : Abelian C
inst✝³ : HasDerivedCategory C
X Y : CochainComplex C ℤ
a b : ℤ
inst✝² : X.IsStrictlyLE b
inst✝¹ : Y.IsStrictlyGE a
inst✝ : Y.IsStrictlyLE b
f : Q.obj X ⟶ Q.obj Y
Y' : CochainComplex C ℤ
hY' : Y'.IsStrictlyGE a
g : X ⟶ Y'
s : Y ⟶ Y'
hs : IsIso (Q.map s)
fac : f = Q.map g ≫ inv (Q.map s)
this : IsIso (Q.map (CochainComplex.truncLEMap s b))
⊢ f =
    Q.map (inv (X.ιTruncLE b) ≫ CochainComplex.truncLEMap g b) ≫
      inv (Q.map (inv (Y.ιTruncLE b) ≫ CochainComplex.truncLEMap s b))

Tactic:
· simp only [Functor.map_comp, Functor.map_inv, IsIso.inv_comp, IsIso.inv_inv, assoc, fac,
      ← cancel_mono (Q.map s), IsIso.inv_hom_id, comp_id]
    rw [← Functor.map_comp, ← CochainComplex.ιTruncLE_naturality s b,
      Functor.map_comp, IsIso.inv_hom_id_assoc,
      ← Functor.map_comp, CochainComplex.ιTruncLE_naturality g b,
      Functor.map_comp, IsIso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom

Goal state before:
pp: C : Type u₁
inst✝⁹ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
W : MorphismProperty C
M : Type w'
inst✝⁷ : AddMonoid M
inst✝⁶ : HasShift C M
inst✝⁵ : HasShift D M
L : C ⥤ D
inst✝⁴ : L.IsLocalization W
inst✝³ : L.CommShift M
X Y : C
inst✝² : W.IsCompatibleWithShift M
a : M
inst✝¹ : HasSmallLocalizedShiftedHom W M X Y
inst✝ : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ (SmallHom.equiv W L) (f.shift n a' h) =
    (Functor.commShiftIso L n).hom.app X ≫
      (shiftFunctor D n).map ((SmallHom.equiv W L) f) ≫
        (shiftFunctor D n).map ((Functor.commShiftIso L a).hom.app Y) ≫
          (shiftFunctorAdd' D a n a' h).inv.app (L.obj Y) ≫ (Functor.commShiftIso L a').inv.app Y

Tactic:
simp only [shift, SmallHom.equiv_comp, SmallHom.equiv_shift, SmallHom.equiv_mk, assoc,
    L.commShiftIso_add' h, Functor.CommShift.isoAdd'_inv_app, Iso.inv_hom_id_app_assoc,
    ← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.comp_obj, comp_id]

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasExt C
X Y : C
a b : ℤ
inst✝ : HasDerivedCategory C
⊢ Small.{w, w'} ((singleFunctor C a).obj X ⟶ (singleFunctor C b).obj Y)

Tactic:
by
  have (a b : ℤ) :
      Small.{w} (((singleFunctor C 0).obj X)⟦a⟧ ⟶ ((singleFunctor C 0).obj Y)⟦b⟧) :=
    (hasSmallLocalizedShiftedHom_iff.{w}
      (W := (HomologicalComplex.quasiIso C (ComplexShape.up ℤ))) (M := ℤ)
      (X := (CochainComplex.singleFunctor C 0).obj X)
      (Y := (CochainComplex.singleFunctor C 0).obj Y) Q).1 inferInstance a b
  exact small_of_injective
    (β := ((singleFunctor C 0).obj X)⟦-a⟧ ⟶ ((singleFunctor C 0).obj Y)⟦-b⟧)
    (f := fun φ ↦
      ((singleFunctors C).shiftIso (-a) a 0 (by simp)).hom.app X ≫ φ ≫
        ((singleFunctors C).shiftIso (-b) b 0 (by simp)).inv.app Y)
    (fun φ₁ φ₂ h ↦ by simpa using h)

Goal state after:
Module: Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
X Y : C
⊢ mk₀ 0 = 0

Tactic:
let := HasDerivedCategory.standard C; ext; simp [zero_hom']

Goal state after: