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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ ((mapHomologicalComplexXIso φ H n).hom ≫
          (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1)) ≫
        (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
          (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
          (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    ((mapHomologicalComplexXIso φ H n).hom ≫
          (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1)) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯ =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯

Tactic:
assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
        (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1) ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
          (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    ((mapHomologicalComplexXIso φ H n).hom ≫
          (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1)) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯ =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
        (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1) ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
          (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    ((mapHomologicalComplexXIso φ H n).hom ≫
          (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1)) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯ =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯

Tactic:
assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
        (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1) ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    ((mapHomologicalComplexXIso φ H n).hom ≫
          (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1)) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯ =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
        (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1) ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    ((mapHomologicalComplexXIso φ H n).hom ≫
          (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1)) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯ =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯

Tactic:
d_fst_v _ _ _ _ rfl,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
        (-(↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F).d (n + 1) (n + 2)) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    ((mapHomologicalComplexXIso φ H n).hom ≫
          (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1)) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯ =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
        (-(↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F).d (n + 1) (n + 2)) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    ((mapHomologicalComplexXIso φ H n).hom ≫
          (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1)) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯ =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯

Tactic:
assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
        (-(↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F).d (n + 1) (n + 2)) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    (mapHomologicalComplexXIso φ H n).hom ≫
        (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1) ≫
          (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯ =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
        (-(↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F).d (n + 1) (n + 2)) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    (mapHomologicalComplexXIso φ H n).hom ≫
        (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1) ≫
          (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯ =
      (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
          (mapHomologicalComplexXIso φ H (n + 1)).hom) ≫
        (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯

Tactic:
assoc,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{v, u_1} C
inst✝⁵ : Category.{v', u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ (mapHomologicalComplexXIso φ H n).hom ≫
        (-(↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v n (n + 1) ⋯ ≫
            ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj F).d (n + 1) (n + 2)) =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (↑(fst ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ))).v (n + 1) (n + 2)
            (CochainComplex.mappingCone.mapHomologicalComplexIso._proof_1 n) ∧
    (mapHomologicalComplexXIso φ H n).hom ≫
        (mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).d n (n + 1) ≫
          (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯ =
      ((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (mappingCone φ)).d n (n + 1) ≫
        (mapHomologicalComplexXIso φ H (n + 1)).hom ≫
          (snd ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).v (n + 1) (n + 1) ⋯
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: case pos
ι✝ : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : c.Rel i (c.next i)
⊢ f.f (c.next i) =
    K.d (c.next i) (c.next (c.next i)) ≫ ho.hom (c.next (c.next i)) (c.next i) +
        ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)

pp: case neg
ι✝ : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : ¬c.Rel i (c.next i)
⊢ f.f (c.next i) =
    f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i) + ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)

Tactic:
· rw [ho.comm (c.next i)]
      dsimp [dFrom, dTo, fromNext, toPrev]
      rw [congr_arg (fun j => ho.hom (c.next i) j ≫ L.d j (c.next i)) (c.prev_eq' h)]

Goal state after:
case neg
ι✝ : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : Preadditive V
c✝ : ComplexShape ι✝
C✝ D E : HomologicalComplex V c✝
f✝ g✝ : C✝ ⟶ D
h✝ k : D ⟶ E
i✝ : ι✝
C : Type u_2
inst✝² : Category.{v_1, u_2} C
inst✝¹ : Preadditive C
ι : Type ?u.42
c : ComplexShape ι
inst✝ : DecidableRel c.Rel
K L : HomologicalComplex C c
f g : K ⟶ L
ho : Homotopy f g
i : ι
h : ¬c.Rel i (c.next i)
⊢ f.f (c.next i) =
    f.f (c.next i) - g.f (c.next i) - ho.hom (c.next i) i ≫ L.d i (c.next i) + ho.hom (c.next i) i ≫ L.d i (c.next i) +
      g.f (c.next i)
Module: Mathlib.CategoryTheory.Quotient.Linear

Goal state before:
pp: R : Type u_1
C : Type u_2
inst✝⁶ : Semiring R
inst✝⁵ : Category.{v_1, u_2} C
inst✝⁴ : Preadditive C
inst✝³ : Linear R C
r : HomRel C
inst✝² : Congruence r
hr : ∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)
inst✝¹ : Preadditive (Quotient r)
inst✝ : (functor r).Additive
this : (X Y : Quotient r) → Module R (X ⟶ Y) := Linear.module r hr
⊢ ∀ (X Y Z : Quotient r) (r_1 : R) (f : X ⟶ Y) (g : Y ⟶ Z), (r_1 • f) ≫ g = r_1 • f ≫ g

Tactic:
by
        rintro ⟨X⟩ ⟨Y⟩ ⟨Z⟩ a f g
        obtain ⟨f, rfl⟩ := (functor r).map_surjective f
        obtain ⟨g, rfl⟩ := (functor r).map_surjective g
        rw [Linear.smul_eq, ← Functor.map_comp, ← Functor.map_comp,
          Linear.smul_eq, Linear.smul_comp]

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

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (lift r F hF).map ((Functor.CommShift.isoZero (functor r) A).inv.app X) ≫ (Functor.commShiftIso F 0).hom.app X =
    (Functor.CommShift.isoZero (lift r F hF) A).hom.app ((functor r).obj X)

Tactic:
Functor.CommShift.isoZero_hom_app,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (lift r F hF).map ((Functor.CommShift.isoZero (functor r) A).inv.app X) ≫ (Functor.commShiftIso F 0).hom.app X =
    (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (shiftFunctorZero D A).inv.app ((lift r F hF).obj ((functor r).obj X))
Module: Mathlib.CategoryTheory.Shift.Quotient

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ ((lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
        (lift r F hF).map ((functor r).map ((shiftFunctorZero C A).inv.app X))) ≫
      (Functor.commShiftIso F 0).hom.app X =
    (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (shiftFunctorZero D A).inv.app ((lift r F hF).obj ((functor r).obj X))

Tactic:
assoc,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (lift r F hF).map ((functor r).map ((shiftFunctorZero C A).inv.app X)) ≫ (Functor.commShiftIso F 0).hom.app X =
    (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (shiftFunctorZero D A).inv.app ((lift r F hF).obj ((functor r).obj X))
Module: Mathlib.CategoryTheory.Shift.Quotient

Goal state before:
pp: C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (lift r F hF).map ((functor r).map ((shiftFunctorZero C A).inv.app X)) ≫
        (Functor.CommShift.isoZero F A).hom.app X =
    (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (shiftFunctorZero D A).inv.app ((lift r F hF).obj ((functor r).obj X))

Tactic:
Functor.CommShift.isoZero_hom_app,

Goal state after:
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (lift r F hF).map ((functor r).map ((shiftFunctorZero C A).inv.app X)) ≫
        F.map ((shiftFunctorZero C A).hom.app X) ≫ (shiftFunctorZero D A).inv.app (F.obj X) =
    (lift r F hF).map ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      (shiftFunctorZero D A).inv.app ((lift r F hF).obj ((functor r).obj X))
Module: Mathlib.CategoryTheory.Shift.Induced

Goal state before:
pp: C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
⊢ ∀ (X : D),
    (Induced.add F s i (m₁ + m₂) m₃).hom.app X ≫ (s m₃).map ((Induced.add F s i m₁ m₂).hom.app X) =
      eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom.app X ≫ (Induced.add F s i m₂ m₃).hom.app ((s m₁).obj X)

Tactic:
suffices (Induced.add F s i (m₁ + m₂) m₃).hom ≫
            whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
            eqToHom (by rw [add_assoc]) ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom ≫
              whiskerLeft (s m₁) (Induced.add F s i m₂ m₃).hom by
          intro X
          simpa using NatTrans.congr_app this X

Goal state after:
C : Type ?u.2
D : Type ?u.4
inst✝⁵ : Category.{v_1, ?u.2} C
inst✝⁴ : Category.{v_2, ?u.4} D
F : C ⥤ D
A : Type ?u.15
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
m₁ m₂ m₃ : A
⊢ (Induced.add F s i (m₁ + m₂) m₃).hom ≫ whiskerRight (Induced.add F s i m₁ m₂).hom (s m₃) =
    eqToHom ⋯ ≫ (Induced.add F s i m₁ (m₂ + m₃)).hom ≫ (s m₁).whiskerLeft (Induced.add F s i m₂ m₃).hom