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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)
i j : ℕ
h : i + 1 = j
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q h).hom =
    (xNextIso P h).inv ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ j).fst

Tactic:
subst j

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
e : P ⟶ Q
zero : P.X 0 ⟶ Q.X 1
comm_zero : e.f 0 = zero ≫ Q.d 1 0
one : P.X 1 ⟶ Q.X 2
comm_one : e.f 1 = P.d 1 0 ≫ zero + one ≫ Q.d 2 1
succ :
  (n : ℕ) →
    (p :
        (f : P.X n ⟶ Q.X (n + 1)) ×'
          (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×' e.f (n + 1) = P.d (n + 1) n ≫ f + f' ≫ Q.d (n + 2) (n + 1)) →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×' e.f (n + 2) = P.d (n + 2) (n + 1) ≫ p.snd.fst + f'' ≫ Q.d (n + 3) (n + 2)
i : ℕ
⊢ (mkInductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst ≫ (xPrevIso Q ⋯).hom =
    (xNextIso P ⋯).inv ≫ (mkInductiveAux₂ e zero comm_zero one comm_one succ (i + 1)).fst
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

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
F G K L : CochainComplex C ℤ
n m : ℤ
z : Cochain F G (-1)
i j : ℤ
hij : (ComplexShape.up ℤ).Rel j i
⊢ i + -1 = j

Tactic:
dsimp at hij; rw [← hij, add_neg_cancel_right]

Goal state after:
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 φ
K : CochainComplex C ℤ
f₁ f₂ : mappingCone φ ⟶ K
γ₁ : Cochain F K (-2)
γ₂ : Cochain G K (-1)
h₁ :
  (inl φ).comp (Cochain.ofHom f₁) ⋯ = δ (-2) (-1) γ₁ + (Cochain.ofHom φ).comp γ₂ ⋯ + (inl φ).comp (Cochain.ofHom f₂) ⋯
h₂ : Cochain.ofHom (inr φ ≫ f₁) = δ (-1) 0 γ₂ + Cochain.ofHom (inr φ ≫ f₂)
⊢ Cochain.ofHom f₁ = δ (-1) 0 (descCochain φ γ₁ γ₂ descHomotopy._proof_1) + Cochain.ofHom f₂

Tactic:
by
    simp only [Cochain.ofHom_comp] at h₂
    simp [ext_cochain_from_iff _ _ _ (neg_add_cancel 1),
      δ_descCochain _ _ _ _ _ (neg_add_cancel 1), h₁, h₂]

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
i j : ℕ
h : i + 1 = j
⊢ (xNextIso P h).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ j).fst ≫ (xPrevIso Q h).hom

Tactic:
subst j

Goal state after:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : CochainComplex V ℕ
e : P ⟶ Q
zero : P.X 1 ⟶ Q.X 0
comm_zero : e.f 0 = P.d 0 1 ≫ zero
one : P.X 2 ⟶ Q.X 1
comm_one : e.f 1 = zero ≫ Q.d 0 1 + P.d 1 2 ≫ one
succ :
  (n : ℕ) →
    (p :
        (f : P.X (n + 1) ⟶ Q.X n) ×'
          (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×' e.f (n + 1) = f ≫ Q.d n (n + 1) + P.d (n + 1) (n + 2) ≫ f') →
      (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×' e.f (n + 2) = p.snd.fst ≫ Q.d (n + 1) (n + 2) + P.d (n + 2) (n + 3) ≫ f''
i : ℕ
⊢ (xNextIso P ⋯).inv ≫ (mkCoinductiveAux₂ e zero comm_zero one comm_one succ i).snd.fst =
    (mkCoinductiveAux₂ e zero comm_zero one comm_one succ (i + 1)).fst ≫ (xPrevIso Q ⋯).hom
Module: Mathlib.Algebra.Homology.Homotopy

Goal state before:
pp: ι✝ : 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 : ι
⊢ ((shortComplexFunctor C c i).map f).τ₁ =
    (((shortComplexFunctor C c i).obj K).f ≫ ho.hom i (c.prev i) +
        if c.Rel (c.prev i) i then ho.hom (c.prev i) (c.prev (c.prev i)) ≫ L.d (c.prev (c.prev i)) (c.prev i)
        else f.f (c.prev i) - g.f (c.prev i) - K.d (c.prev i) i ≫ ho.hom i (c.prev i)) +
      ((shortComplexFunctor C c i).map g).τ₁

Tactic:
dsimp
    split_ifs with h
    · rw [ho.comm (c.prev i)]
      dsimp [dFrom, dTo, fromNext, toPrev]
      rw [congr_arg (fun j => d K (c.prev i) j ≫ ho.hom j (c.prev i)) (c.next_eq' h)]
    · abel

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 ((shiftFunctorZero (Quotient r) A).hom.app ((functor r).obj X)) ≫
      F.map ((shiftFunctorZero C A).inv.app X ≫ (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))

Tactic:
Iso.inv_hom_id_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)) ≫
      F.map (𝟙 ((𝟭 C).obj 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.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A B : Triangle C
iso₁ : A.obj₁ ≅ B.obj₁
iso₂ : A.obj₂ ≅ B.obj₂
iso₃ : A.obj₃ ≅ B.obj₃
comm₁ : A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁
comm₂ : A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂
comm₃ : A.mor₃ ≫ (shiftFunctor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃
⊢ B.mor₃ ≫ (shiftFunctor C 1).map iso₁.inv = iso₃.inv ≫ A.mor₃

Tactic:
simp only [← cancel_mono (iso₁.hom⟦(1 : ℤ)⟧'), Category.assoc, comm₃,
      Iso.inv_hom_id_assoc, ← Functor.map_comp, Iso.inv_hom_id,
      Functor.map_id, Category.comp_id]

Goal state after:
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
this : HasShift D A := HasShift.induced F A s i
a b : A
X : C
⊢ (i (a + b)).inv.app X =
    F.map ((shiftFunctorAdd C a b).hom.app X) ≫
      (i b).inv.app ((shiftFunctor C a).obj X) ≫
        (s b).map ((i a).inv.app X ≫ (i a).hom.app X) ≫
          (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X

Tactic:
Iso.inv_hom_id_app

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
this : HasShift D A := HasShift.induced F A s i
a b : A
X : C
⊢ (i (a + b)).inv.app X =
    F.map ((shiftFunctorAdd C a b).hom.app X) ≫
      (i b).inv.app ((shiftFunctor C a).obj X) ≫
        (s b).map (𝟙 ((shiftFunctor C a ⋙ F).obj X)) ≫
          (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X
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 : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
⊢ productTriangle T ∈ distinguishedTriangles

Tactic:
let φ : ∀ j, T' ⟶ T j := fun j => completeDistinguishedTriangleMorphism _ _
    hT' (hT j) (Pi.π _ j) (Pi.π _ j) (by simp [f₁, T'])

Goal state after:
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : HasZeroObject C
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
J : Type u_1
T : J → Triangle C
hT : ∀ (j : J), T j ∈ distinguishedTriangles
inst✝³ : HasProduct fun j ↦ (T j).obj₁
inst✝² : HasProduct fun j ↦ (T j).obj₂
inst✝¹ : HasProduct fun j ↦ (T j).obj₃
inst✝ : HasProduct fun j ↦ (shiftFunctor C 1).obj (T j).obj₁
f₁ : (∏ᶜ fun j ↦ (T j).obj₁) ⟶ ∏ᶜ fun j ↦ (T j).obj₂ := Limits.Pi.map fun j ↦ (T j).mor₁
Z : C
f₂ : (∏ᶜ fun j ↦ (T j).obj₂) ⟶ Z
f₃ : Z ⟶ (shiftFunctor C 1).obj (∏ᶜ fun j ↦ (T j).obj₁)
T' : Triangle C := Triangle.mk f₁ f₂ f₃
hT' : T' ∈ distinguishedTriangles
φ : (j : J) → T' ⟶ T j :=
  fun j ↦
    completeDistinguishedTriangleMorphism T' (T j) hT' ⋯ (Pi.π (fun j ↦ (T j).obj₁) j) (Pi.π (fun j ↦ (T j).obj₂) j) ⋯
⊢ productTriangle T ∈ distinguishedTriangles
Module: Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated

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
inst✝³ : Preadditive C
inst✝² : HasBinaryBiproducts C
inst✝¹ : Preadditive D
inst✝ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
n : ℤ
⊢ (n.negOnePow • (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ) ≫
      (n.negOnePow • 𝟙 ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L)) =
    𝟙 ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) ≫
      (CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ

Tactic:
simp only [Linear.comp_units_smul, comp_id, id_comp, smul_smul,
      Int.units_mul_self, one_smul]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
inst✝⁵ : HasShift E ℤ
F : C ⥤ D
inst✝⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝³ : G.CommShift ℤ
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : F.Additive
n : ℤ
T : Triangle C
⊢ n.negOnePow •
      F.map ((shiftFunctor C n).map T.mor₃) ≫
        F.map ((shiftFunctorComm C 1 n).hom.app T.obj₁) ≫
          (commShiftIso F 1).hom.app ((shiftFunctor C n).obj T.obj₁) ≫
            (shiftFunctor D 1).map ((commShiftIso F n).hom.app T.obj₁) =
    n.negOnePow •
      F.map ((shiftFunctor C n).map T.mor₃) ≫
        (commShiftIso F n).hom.app ((shiftFunctor C 1).obj T.obj₁) ≫
          (shiftFunctor D n).map ((commShiftIso F 1).hom.app T.obj₁) ≫ (shiftFunctorComm D 1 n).hom.app (F.obj T.obj₁)

Tactic:
rw [F.map_shiftFunctorComm_hom_app T.obj₁ 1 n]

Goal state after:
C : Type u_1
D : Type u_2
E : Type u_3
inst✝¹⁰ : Category.{v_1, u_1} C
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Category.{v_3, u_3} E
inst✝⁷ : HasShift C ℤ
inst✝⁶ : HasShift D ℤ
inst✝⁵ : HasShift E ℤ
F : C ⥤ D
inst✝⁴ : F.CommShift ℤ
G : D ⥤ E
inst✝³ : G.CommShift ℤ
inst✝² : Preadditive C
inst✝¹ : Preadditive D
inst✝ : F.Additive
n : ℤ
T : Triangle C
⊢ n.negOnePow •
      F.map ((shiftFunctor C n).map T.mor₃) ≫
        ((commShiftIso F n).hom.app ((shiftFunctor C 1).obj T.obj₁) ≫
            (shiftFunctor D n).map ((commShiftIso F 1).hom.app T.obj₁) ≫
              (shiftFunctorComm D 1 n).hom.app (F.obj T.obj₁) ≫
                (shiftFunctor D 1).map ((commShiftIso F n).inv.app T.obj₁) ≫
                  (commShiftIso F 1).inv.app ((shiftFunctor C n).obj T.obj₁)) ≫
          (commShiftIso F 1).hom.app ((shiftFunctor C n).obj T.obj₁) ≫
            (shiftFunctor D 1).map ((commShiftIso F n).hom.app T.obj₁) =
    n.negOnePow •
      F.map ((shiftFunctor C n).map T.mor₃) ≫
        (commShiftIso F n).hom.app ((shiftFunctor C 1).obj T.obj₁) ≫
          (shiftFunctor D n).map ((commShiftIso F 1).hom.app T.obj₁) ≫ (shiftFunctorComm D 1 n).hom.app (F.obj T.obj₁)
Module: Mathlib.CategoryTheory.Triangulated.Pretriangulated

Goal state before:
pp: case refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₃ : T₁.obj₃ ≅ T₂.obj₃
comm : T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = e₃.hom ≫ T₂.mor₃
h :
  ∃ e',
    e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom ∧
      e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk ((shiftFunctor C (-1)).mapIso e₃) e₁ ⋯).hom
e : T₁.invRotate ≅ T₂.invRotate := h.choose
h₁ : e.hom.hom₁ = (shiftFunctor C (-1)).map e₃.hom
h₂ : e₁.hom = e.hom.hom₂
h₃ :
  (T₁.mor₂ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T₁.3) ≫ (shiftFunctor C 1).map e.hom.hom₁ =
    e.hom.hom₃ ≫ T₂.mor₂ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app T₂.3
h₄ :
  e₃.hom ≫ (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_4).inv.app T₂.obj₃ =
    (shiftFunctorCompIsoId C (-1) 1 isoTriangleOfIso₁₃._proof_4).inv.app T₁.obj₃ ≫
      (shiftFunctor C 1).map ((shiftFunctor C (-1)).map e₃.hom)
⊢ T₁.mor₁ ≫ (Triangle.π₃.mapIso e).hom = e₁.hom ≫ T₂.mor₁

Tactic:
convert! e.hom.comm₂ using 2

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
a : M
⊢ ((shiftFunctor C 0).associator (shiftFunctor C a) F).symm ≪≫ isoWhiskerRight (shiftFunctorAdd' C 0 a a ⋯).symm F =
    isoWhiskerRight (shiftFunctorZero C M) (shiftFunctor C a ⋙ F) ≪≫ (shiftFunctor C a ⋙ F).leftUnitor

Tactic:
rw [shiftFunctorAdd'_zero_add]

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
a : M
⊢ ((shiftFunctor C 0).associator (shiftFunctor C a) F).symm ≪≫
      isoWhiskerRight
        ((shiftFunctor C a).leftUnitor.symm ≪≫ isoWhiskerRight (shiftFunctorZero C M).symm (shiftFunctor C a)).symm F =
    isoWhiskerRight (shiftFunctorZero C M) (shiftFunctor C a ⋙ F) ≪≫ (shiftFunctor C a ⋙ F).leftUnitor
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: case refine_5
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
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ (shiftFunctor C 1).map v₁₃ = (shiftFunctor C 1).map v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ : (shiftFunctor C 1).map v₁₃ ≫ (shiftFunctor C 1).map u₁₂ = o.m₃ ≫ (shiftFunctor C 1).map v₂₃
⊢ v₂₃ ≫ w₁₂ ≫ (shiftFunctor C 1).map ((shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₂) =
    (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₂₃ ≫
      (shiftFunctor C (-1)).map ((shiftFunctor C 1).map v₂₃) ≫
        (shiftFunctor C (-1)).map ((shiftFunctor C 1).map w₁₂) ≫
          (shiftFunctorComm C 1 (-1)).hom.app ((shiftFunctor C 1).obj Z₁₂)

Tactic:
shift_shift_neg',

Goal state after:
case refine_5
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
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ (shiftFunctor C 1).map v₁₃ = (shiftFunctor C 1).map v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ : (shiftFunctor C 1).map v₁₃ ≫ (shiftFunctor C 1).map u₁₂ = o.m₃ ≫ (shiftFunctor C 1).map v₂₃
⊢ v₂₃ ≫ w₁₂ ≫ (shiftFunctor C 1).map ((shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₁₂) =
    (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₂₃ ≫
      ((shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Z₂₃ ≫ v₂₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app X₂) ≫
        (shiftFunctor C (-1)).map ((shiftFunctor C 1).map w₁₂) ≫
          (shiftFunctorComm C 1 (-1)).hom.app ((shiftFunctor C 1).obj Z₁₂)
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
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
⊢ τ₁ = τ₂

Tactic:
ext X
  have eq := (objEquiv W).right_inv X
  simp only [objEquiv] at eq
  rw [← eq, ← NatTrans.id_hcomp_app, ← NatTrans.id_hcomp_app, h]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
| F'.map
      ((commShiftIso L b).inv.app ((shiftFunctor C a).obj X) ≫
        L.map ((shiftFunctorAdd C a b).inv.app X ≫ (shiftFunctorAdd C a b).hom.app X)) ≫
    (Lifting.iso L W F F').hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
          (shiftFunctorAdd E a b).inv.app (F.obj X) ≫ (shiftFunctor E (a + b)).map ((Lifting.iso L W F F').inv.app X)

Tactic:
Iso.inv_hom_id_app

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
| F'.map
      ((commShiftIso L b).inv.app ((shiftFunctor C a).obj X) ≫
        L.map (𝟙 ((shiftFunctor C a ⋙ shiftFunctor C b).obj X))) ≫
    (Lifting.iso L W F F').hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
          (shiftFunctorAdd E a b).inv.app (F.obj X) ≫ (shiftFunctor E (a + b)).map ((Lifting.iso L W F F').inv.app X)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
f : X' ⟶ Y'
g₁ g₂ : Y' ⟶ Z'
⊢ f ≫ add W eY eZ g₁ g₂ = add W eX eZ (f ≫ g₁) (f ≫ g₂)

Tactic:
by
  obtain ⟨f, rfl⟩ := (homEquiv eX eY).symm.surjective f
  simp [add]

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

Goal state before:
pp: case refine_1
C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : J a ⥤ C
inst✝ : HasLimit F
o : J a → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' : ∀ (j : J a), transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (o j) P (F.obj j)
⊢ Cardinal.mk (Shrink.{w, u'} (J a)) < κ.ord.cof

pp: case refine_2
C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : J a ⥤ C
inst✝ : HasLimit F
o : J a → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' : ∀ (j : J a), transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (o j) P (F.obj j)
j : J a
⊢ o j ≤ ⨆ j, o ((equivShrink (J a)).symm j)

Tactic:
· rw [hκ.cof_ord, ← hasCardinalLT_iff_cardinal_mk_lt _ κ,
          ← hasCardinalLT_iff_of_equiv (equivShrink.{w} (J a))]
        exact h a

Goal state after:
case refine_2
C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : J a ⥤ C
inst✝ : HasLimit F
o : J a → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' : ∀ (j : J a), transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (o j) P (F.obj j)
j : J a
⊢ o j ≤ ⨆ j, o ((equivShrink (J a)).symm j)
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
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
⊢ (Q W ⋙ lift F hF).map f = eqToHom ⋯ ≫ F.map f ≫ eqToHom ⋯

Tactic:
by
    dsimp [lift]
    rw [Q_map, Hom.map_mk, id_comp, comp_id, map_ofHom]

Goal state after: