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

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✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (-(CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
          ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ)) ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        (𝟙 ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)) =
    ((Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).inv.app K ≫
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (rotateHomotopyEquiv φ).hom) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle (inr φ)).mor₃ ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app L

Tactic:
CategoryTheory.Functor.map_id,

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✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
⊢ (-(CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
          ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map φ)) ≫
      𝟙
        ((CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).obj
          ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj L)) =
    ((Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).inv.app K ≫
        (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (rotateHomotopyEquiv φ).hom) ≫
      (HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (triangle (inr φ)).mor₃ ≫
        (Functor.commShiftIso (HomotopyCategory.quotient C (ComplexShape.up ℤ)) 1).hom.app L
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T₁ T₂ : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
K₁ L₁ : CochainComplex C ℤ
φ₁ : K₁ ⟶ L₁
e₁ : T₁ ≅ triangleh φ₁
K₂ L₂ : CochainComplex C ℤ
φ₂ : K₂ ⟶ L₂
e₂ : T₂ ≅ triangleh φ₂
a'' : K₁ ⟶ K₂
ha' : (quotient C (ComplexShape.up ℤ)).map a'' = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
b'' : L₁ ⟶ L₂
hb' : (quotient C (ComplexShape.up ℤ)).map b'' = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
⊢ (quotient C (ComplexShape.up ℤ)).map (φ₁ ≫ b'') = (quotient C (ComplexShape.up ℤ)).map (a'' ≫ φ₂)

Tactic:
have comm₁₁ := e₁.inv.comm₁
    have comm₁₂ := e₂.hom.comm₁
    dsimp at comm₁₁ comm₁₂
    simp only [Functor.map_comp, ha', hb', reassoc_of% comm₁₁,
      reassoc_of% fac, comm₁₂, assoc]

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

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
F : C ⥤ A
π : C ⥤ D
H : D ⥤ A
e : π ⋙ H ≅ F
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
G : Type u_5
inst✝³ : AddGroup G
inst✝² : HasShift C G
inst✝¹ : π.CommShift M
inst✝ : H.ShiftSequence M
a : M
⊢ ((shiftFunctor C 0).associator π (H.shift a)).symm ≪≫
      isoWhiskerRight (commShiftIso π 0) (H.shift a) ≪≫
        π.associator (shiftFunctor D 0) (H.shift a) ≪≫ π.isoWhiskerLeft (H.shiftIso 0 a a ⋯) =
    isoWhiskerRight (shiftFunctorZero C M) (π ⋙ H.shift a) ≪≫ (π ⋙ H.shift a).leftUnitor

Tactic:
ext K

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
F : C ⥤ A
π : C ⥤ D
H : D ⥤ A
e : π ⋙ H ≅ F
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
G : Type u_5
inst✝³ : AddGroup G
inst✝² : HasShift C G
inst✝¹ : π.CommShift M
inst✝ : H.ShiftSequence M
a : M
K : C
⊢ (((shiftFunctor C 0).associator π (H.shift a)).symm ≪≫
            isoWhiskerRight (commShiftIso π 0) (H.shift a) ≪≫
              π.associator (shiftFunctor D 0) (H.shift a) ≪≫ π.isoWhiskerLeft (H.shiftIso 0 a a ⋯)).hom.app
      K =
    (isoWhiskerRight (shiftFunctorZero C M) (π ⋙ H.shift a) ≪≫ (π ⋙ H.shift a).leftUnitor).hom.app K
Module: Mathlib.CategoryTheory.Shift.ShiftSequence

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
F : C ⥤ A
π : C ⥤ D
H : D ⥤ A
e : π ⋙ H ≅ F
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
G : Type u_5
inst✝³ : AddGroup G
inst✝² : HasShift C G
inst✝¹ : π.CommShift M
inst✝ : H.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ ((shiftFunctor C (m + n)).associator π (H.shift a)).symm ≪≫
      isoWhiskerRight (commShiftIso π (m + n)) (H.shift a) ≪≫
        π.associator (shiftFunctor D (m + n)) (H.shift a) ≪≫ π.isoWhiskerLeft (H.shiftIso (m + n) a a'' ⋯) =
    isoWhiskerRight (shiftFunctorAdd C m n) (π ⋙ H.shift a) ≪≫
      (shiftFunctor C m).associator (shiftFunctor C n) (π ⋙ H.shift a) ≪≫
        (shiftFunctor C m).isoWhiskerLeft
            (((shiftFunctor C n).associator π (H.shift a)).symm ≪≫
              isoWhiskerRight (commShiftIso π n) (H.shift a) ≪≫
                π.associator (shiftFunctor D n) (H.shift a) ≪≫ π.isoWhiskerLeft (H.shiftIso n a a' ha')) ≪≫
          ((shiftFunctor C m).associator π (H.shift a')).symm ≪≫
            isoWhiskerRight (commShiftIso π m) (H.shift a') ≪≫
              π.associator (shiftFunctor D m) (H.shift a') ≪≫ π.isoWhiskerLeft (H.shiftIso m a' a'' ha'')

Tactic:
ext K

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
F : C ⥤ A
π : C ⥤ D
H : D ⥤ A
e : π ⋙ H ≅ F
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : HasShift D M
G : Type u_5
inst✝³ : AddGroup G
inst✝² : HasShift C G
inst✝¹ : π.CommShift M
inst✝ : H.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
K : C
⊢ (((shiftFunctor C (m + n)).associator π (H.shift a)).symm ≪≫
            isoWhiskerRight (commShiftIso π (m + n)) (H.shift a) ≪≫
              π.associator (shiftFunctor D (m + n)) (H.shift a) ≪≫
                π.isoWhiskerLeft (H.shiftIso (m + n) a a'' ⋯)).hom.app
      K =
    (isoWhiskerRight (shiftFunctorAdd C m n) (π ⋙ H.shift a) ≪≫
            (shiftFunctor C m).associator (shiftFunctor C n) (π ⋙ H.shift a) ≪≫
              (shiftFunctor C m).isoWhiskerLeft
                  (((shiftFunctor C n).associator π (H.shift a)).symm ≪≫
                    isoWhiskerRight (commShiftIso π n) (H.shift a) ≪≫
                      π.associator (shiftFunctor D n) (H.shift a) ≪≫ π.isoWhiskerLeft (H.shiftIso n a a' ha')) ≪≫
                ((shiftFunctor C m).associator π (H.shift a')).symm ≪≫
                  isoWhiskerRight (commShiftIso π m) (H.shift a') ≪≫
                    π.associator (shiftFunctor D m) (H.shift a') ≪≫ π.isoWhiskerLeft (H.shiftIso m a' a'' ha'')).hom.app
      K
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
⊢ { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := cyclesMap S.f i, g := cyclesMap S.g i,
      zero := ⋯ }.Exact

Tactic:
have : Mono (ShortComplex.map S (eval C c i)).f := by dsimp; infer_instance

Goal state after:
C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
⊢ { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := cyclesMap S.f i, g := cyclesMap S.g i,
      zero := ⋯ }.Exact
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.IsStableUnderComposition
X Y : C
p : Path X Y
hp : W.paths p
h : 0 < p.length
⊢ W (composePath p)

Tactic:
revert hp h

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.IsStableUnderComposition
X Y : C
p : Path X Y
⊢ W.paths p → 0 < p.length → W (composePath p)
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : C
f : X ⟶ Y
⊢ (lift G hG).map (W.Q.map f) = G.map f

Tactic:
dsimp [MorphismProperty.Q, Quot.liftOn, Quotient.functor]

Goal state after:
C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
X Y : C
f : X ⟶ Y
⊢ composePath (G.map f).toPath = G.map f
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
W : MorphismProperty C
X Y : C
φ : W.LeftFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ φ.map L hL ≫ L.map φ.s = L.map φ.f

Tactic:
let := hL _ φ.hs
  simp [map]

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

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
W : MorphismProperty C
X Y : C
φ : W.RightFraction X Y
L : C ⥤ D
hL : W.IsInvertedBy L
⊢ L.map φ.s ≫ φ.map L hL = L.map φ.f

Tactic:
let := hL _ φ.hs
  simp [map]

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

Goal state before:
pp: C₁ : Type u₁
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₃} C₃
inst✝⁴ : Category.{v₄, u₄} D₁
inst✝³ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
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✝ : Φ.IsLocalizedFullyFaithful
⊢ Φ.op.IsLocalizedFullyFaithful

Tactic:
let G := Φ.localizedFunctor W₁.Q W₂.Q
  let : CatCommSq Φ.op.functor W₁.Q.op W₂.Q.op G.op :=
    ⟨NatIso.op (CatCommSq.iso Φ.functor W₁.Q W₂.Q G).symm⟩
  exact IsLocalizedFullyFaithful.mk' Φ.op W₁.Q.op W₂.Q.op G.op
    (Φ.fullyFaithful W₁.Q W₂.Q G).op

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

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.f ≫ α.s = { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ α.f
ψ : W.LeftFraction₂ X Y := { Y' := α.Y', f := φ.f ≫ α.f, f' := φ'.f ≫ α.s, s := φ'.s ≫ α.s, hs := ⋯ }
this : IsIso (L.map (φ'.s ≫ α.s))
⊢ f ≫ L.map { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ L.map α.f = L.map ψ.fst.f

Tactic:
hφ,

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.f ≫ α.s = { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ α.f
ψ : W.LeftFraction₂ X Y := { Y' := α.Y', f := φ.f ≫ α.f, f' := φ'.f ≫ α.s, s := φ'.s ≫ α.s, hs := ⋯ }
this : IsIso (L.map (φ'.s ≫ α.s))
⊢ φ.map L ⋯ ≫ L.map { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ L.map α.f = L.map ψ.fst.f
Module: Mathlib.Order.TransfiniteIteration

Goal state before:
pp: case isMin
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k : J
hk : IsMin ⊥
hkj : k ≤ ⊥
⊢ (fun j ↦ transfiniteIterate φ j i₀) k ≤ (fun j ↦ transfiniteIterate φ j i₀) ⊥

Tactic:
obtain rfl : k = ⊥ := by simpa using hkj

Goal state after:
case isMin
I : Type u
inst✝⁴ : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst✝³ : LinearOrder J
inst✝² : OrderBot J
inst✝¹ : SuccOrder J
inst✝ : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
hk : IsMin ⊥
hkj : ⊥ ≤ ⊥
⊢ (fun j ↦ transfiniteIterate φ j i₀) ⊥ ≤ (fun j ↦ transfiniteIterate φ j i₀) ⊥
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
⊢ P.IsClosedUnderLimitsOfShape (Discrete J)

Tactic:
by
  obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin J
  have : P.IsClosedUnderLimitsOfShape (Discrete (Fin n)) :=
    IsClosedUnderFiniteProducts.isClosedUnderLimitsOfShape _
  exact IsClosedUnderLimitsOfShape.of_equivalence (Discrete.equivalence e.symm)

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

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : P.IsStableUnderShift A
inst✝¹ : Preadditive C
n : A
inst✝ : (shiftFunctor C n).Additive
⊢ (shiftFunctor P.FullSubcategory n).Additive

Tactic:
by
  have := Functor.additive_of_iso (P.ι.commShiftIso n).symm
  apply Functor.additive_of_comp_faithful _ P.ι

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

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
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
⊢ ∀ {X Y Z : Localization W} (f : X ⟶ Y) (g : Y ⟶ Z), Hom.map (f ≫ g) F hF = Hom.map f F hF ≫ Hom.map g F hF

Tactic:
by
    rintro (X Y Z : C) f g
    obtain ⟨f, rfl⟩ := Hom.mk_surjective f
    obtain ⟨g, rfl⟩ := Hom.mk_surjective g
    dsimp
    obtain ⟨z, fac⟩ := HasLeftCalculusOfFractions.exists_leftFraction
      (RightFraction.mk f.s f.hs g.f)
    rw [homMk_comp_homMk f g z fac, Hom.map_mk]
    dsimp at fac ⊢
    have := hF _ g.hs
    have := hF _ z.hs
    rw [← cancel_mono (F.map g.s), assoc, map_comp_map_s,
      ← cancel_mono (F.map z.s), assoc, assoc, ← F.map_comp,
      ← F.map_comp, map_comp_map_s, fac]
    dsimp
    rw [F.map_comp, F.map_comp, map_comp_map_s_assoc]

Goal state after:
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
a : M
⊢ ((whiskeringLeft C D A).obj L).map (induced.shiftIso L G M F' e' 0 a a ⋯).hom =
    ((whiskeringLeft C D A).obj L).map (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor).hom

Tactic:
ext K

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
a : M
K : C
⊢ (((whiskeringLeft C D A).obj L).map (induced.shiftIso L G M F' e' 0 a a ⋯).hom).app K =
    (((whiskeringLeft C D A).obj L).map (isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor).hom).app K
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
a : M
⊢ induced.shiftIso L G M F' e' 0 a a ⋯ = isoWhiskerRight (shiftFunctorZero D M) (F' a) ≪≫ (F' a).leftUnitor

Tactic:
ext1
    apply ((whiskeringLeft C D A).obj L).map_injective
    ext K
    dsimp
    simp only [induced.shiftIso_hom_app_obj, shiftIso_zero_hom_app, id_obj,
      NatTrans.naturality, comp_map, Iso.hom_inv_id_app_assoc,
      comp_id, ← Functor.map_comp, L.commShiftIso_zero, CommShift.isoZero_inv_app, assoc,
      Iso.inv_hom_id_app, Functor.map_id]

Goal state after:
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''
⊢ ((whiskeringLeft C D A).obj L).map (induced.shiftIso L G M F' e' (m + n) a a'' ⋯).hom =
    ((whiskeringLeft C D A).obj L).map
      (isoWhiskerRight (shiftFunctorAdd D m n) (F' a) ≪≫
          (shiftFunctor D m).associator (shiftFunctor D n) (F' a) ≪≫
            (shiftFunctor D m).isoWhiskerLeft (induced.shiftIso L G M F' e' n a a' ha') ≪≫
              induced.shiftIso L G M F' e' m a' a'' ha'').hom

Tactic:
ext K

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
⊢ (((whiskeringLeft C D A).obj L).map (induced.shiftIso L G M F' e' (m + n) a a'' ⋯).hom).app K =
    (((whiskeringLeft C D A).obj L).map
          (isoWhiskerRight (shiftFunctorAdd D m n) (F' a) ≪≫
              (shiftFunctor D m).associator (shiftFunctor D n) (F' a) ≪≫
                (shiftFunctor D m).isoWhiskerLeft (induced.shiftIso L G M F' e' n a a' ha') ≪≫
                  induced.shiftIso L G M F' e' m a' a'' ha'').hom).app
      K
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
a : ℤ
⊢ ShiftSequence.shiftIso C 0 a a ⋯ =
    Functor.isoWhiskerRight (shiftFunctorZero (HomologicalComplex C (up ℤ)) ℤ) (homologyFunctor C (up ℤ) a) ≪≫
      (homologyFunctor C (up ℤ) a).leftUnitor

Tactic:
ext K

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
a : ℤ
K : HomologicalComplex C (up ℤ)
⊢ (ShiftSequence.shiftIso C 0 a a ⋯).hom.app K =
    (Functor.isoWhiskerRight (shiftFunctorZero (HomologicalComplex C (up ℤ)) ℤ) (homologyFunctor C (up ℤ) a) ≪≫
            (homologyFunctor C (up ℤ) a).leftUnitor).hom.app
      K
Module: Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
⊢ ShiftSequence.shiftIso C (m + n) a a'' ⋯ =
    Functor.isoWhiskerRight (shiftFunctorAdd (HomologicalComplex C (up ℤ)) m n) (homologyFunctor C (up ℤ) a) ≪≫
      (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) m).associator
          (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n) (homologyFunctor C (up ℤ) a) ≪≫
        (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) m).isoWhiskerLeft
            (ShiftSequence.shiftIso C n a a' ha') ≪≫
          ShiftSequence.shiftIso C m a' a'' ha''

Tactic:
ext K

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : CategoryWithHomology C
n m a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : HomologicalComplex C (up ℤ)
⊢ (ShiftSequence.shiftIso C (m + n) a a'' ⋯).hom.app K =
    (Functor.isoWhiskerRight (shiftFunctorAdd (HomologicalComplex C (up ℤ)) m n) (homologyFunctor C (up ℤ) a) ≪≫
            (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) m).associator
                (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n) (homologyFunctor C (up ℤ) a) ≪≫
              (CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) m).isoWhiskerLeft
                  (ShiftSequence.shiftIso C n a a' ha') ≪≫
                ShiftSequence.shiftIso C m a' a'' ha'').hom.app
      K
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

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
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F G : SingleFunctors C D A
e : F ≅ G
n : A
⊢ e.hom.hom n ≫ e.inv.hom n = 𝟙 (F.functor n)

Tactic:
← comp_hom,

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
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F G : SingleFunctors C D A
e : F ≅ G
n : A
⊢ (e.hom ≫ e.inv).hom n = 𝟙 (F.functor n)
Module: Mathlib.CategoryTheory.Shift.SingleFunctors

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
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F G : SingleFunctors C D A
e : F ≅ G
n : A
⊢ e.inv.hom n ≫ e.hom.hom n = 𝟙 (G.functor n)

Tactic:
← comp_hom,

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
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F G : SingleFunctors C D A
e : F ≅ G
n : A
⊢ (e.inv ≫ e.hom).hom n = 𝟙 (G.functor n)
Module: Mathlib.Algebra.Homology.DerivedCategory.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ Qh.map (𝟙 (((HomotopyCategory.singleFunctors C).functor n).obj X)) ≫
      𝟙 ((singleFunctor C n).obj X) ≫
        𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) =
    𝟙 (((singleFunctors C).functor n).obj X)

Tactic:
CategoryTheory.Functor.map_id,

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
n : ℤ
X : C
⊢ 𝟙 (Qh.obj (((HomotopyCategory.singleFunctors C).functor n).obj X)) ≫
      𝟙 ((singleFunctor C n).obj X) ≫
        𝟙 (HomologicalComplexUpToQuasiIso.Q.obj (((CochainComplex.singleFunctors C).functor n).obj X)) =
    𝟙 (((singleFunctors C).functor n).obj X)