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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
⊢ f.f j =
    (desc φ (inr φ ≫ f) ((Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))).f j

Tactic:
by_cases hj : c.Rel j (c.next j)

Goal state after:
case pos
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
hj : c.Rel j (c.next j)
⊢ f.f j =
    (desc φ (inr φ ≫ f) ((Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))).f j

case neg
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
f : homotopyCofiber φ ⟶ K
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
hj : ¬c.Rel j (c.next j)
⊢ f.f j =
    (desc φ (inr φ ≫ f) ((Homotopy.ofEq ⋯).trans (((inrCompHomotopy φ hc).compRight f).trans (Homotopy.ofEq ⋯)))).f j
Module: Mathlib.Algebra.Homology.HomotopyCategory.MappingCone

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ (inl φ).v i j hij ≫ (mappingCone φ).d j i = φ.f i ≫ (inr φ).f i - F.d i k ≫ (inl φ).v k i hik

Tactic:
by
  dsimp [mappingCone, inl, inr]
  rw [homotopyCofiber.inlX_d φ j i k (by dsimp; lia) (by dsimp; lia)]
  abel

Goal state after:
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 : ℤ
hm : n + 1 = m
s : Fork ((K.HomComplex L).d n m) 0
x✝¹ x✝ : ↑s.1
⊢ ⟨(ConcreteCategory.hom s.ι) (x✝¹ + x✝), ⋯⟩ = ⟨(ConcreteCategory.hom s.ι) x✝¹, ⋯⟩ + ⟨(ConcreteCategory.hom s.ι) x✝, ⋯⟩

Tactic:
#adaptation_note /-- Prior to https://github.com/leanprover/lean4/pull/12244
          this was just `cat_disch`. -/
          simp +instances only [HomComplex_X, map_add]
          rfl

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

Goal state before:
pp: case h₁
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i j : ι
hij : c.Rel i j
⊢ inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫ (mapHomologicalComplexObjXIso φ H i).inv ≫ H.map (d φ i j) =
    inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫
      d ((H.mapHomologicalComplex c).map φ) i j ≫ (mapHomologicalComplexObjXIso φ H j).inv

Tactic:
by_cases hj : c.Rel j (c.next j)

Goal state after:
case pos
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i j : ι
hij : c.Rel i j
hj : c.Rel j (c.next j)
⊢ inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫ (mapHomologicalComplexObjXIso φ H i).inv ≫ H.map (d φ i j) =
    inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫
      d ((H.mapHomologicalComplex c).map φ) i j ≫ (mapHomologicalComplexObjXIso φ H j).inv

case neg
C : Type u_1
inst✝⁷ : Category.{v_1, u_1} C
inst✝⁶ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G K : HomologicalComplex C c
φ : F ⟶ G
inst✝⁵ : HasHomotopyCofiber φ
inst✝⁴ : DecidableRel c.Rel
D : Type u_3
inst✝³ : Category.{v_2, u_3} D
inst✝² : Preadditive D
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)
i j : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫ (mapHomologicalComplexObjXIso φ H i).inv ≫ H.map (d φ i j) =
    inlX ((H.mapHomologicalComplex c).map φ) j i hij ≫
      d ((H.mapHomologicalComplex c).map φ) i j ≫ (mapHomologicalComplexObjXIso φ H j).inv
Module: Mathlib.CategoryTheory.Quotient.Preadditive

Goal state before:
pp: C : Type ?u.2
inst✝² : Category.{v_1, ?u.2} C
inst✝¹ : Preadditive C
r : HomRel C
inst✝ : Congruence r
hr : ∀ ⦃X Y : C⦄ (f₁ f₂ g₁ g₂ : X ⟶ Y), r f₁ f₂ → r g₁ g₂ → r (f₁ + g₁) (f₂ + g₂)
X Y : Quotient r
f g✝ : X ⟶ Y
f₁ f₂ g : X.as ⟶ Y.as
h₁₂ : r f₁ f₂
⊢ r (f₁ + g) (f₂ + g)

Tactic:
exact hr _ _ _ _ h₁₂ (Congruence.equivalence.refl g)

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 : CochainComplex C ℤ
n' a : ℤ
γ : Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'
n : ℤ
hn : n' + a = n
x : Rˣ
⊢ (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn

Tactic:
apply rightUnshift_smul

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
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₁
s : Fan T
m : s.pt ⟶ (fan T).pt
⊢ (∀ (j : J), m ≫ (fan T).proj j = s.proj j) → m = lift T s.proj

Tactic:
hm

Goal state after:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
T : J → Triangle C
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₁
s : Fan T
m : s.pt ⟶ (fan T).pt
hm : ∀ (j : J), m ≫ (fan T).proj j = s.proj j
⊢ m = lift T s.proj
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
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
b : T₁.obj₂ ⟶ T₂.obj₂
c : T₁.obj₃ ⟶ T₂.obj₃
comm : T₁.mor₂ ≫ c = b ≫ T₂.mor₂
⊢ ∃ a, T₁.mor₁ ≫ b = a ≫ T₂.mor₁ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₂.mor₃

Tactic:
by
  obtain ⟨a, ⟨ha₁, ha₂⟩⟩ := complete_distinguished_triangle_morphism _ _
    (rot_of_distTriang _ hT₁) (rot_of_distTriang _ hT₂) b c comm
  refine ⟨(shiftFunctor C (1 : ℤ)).preimage a, ⟨?_, ?_⟩⟩
  · apply (shiftFunctor C (1 : ℤ)).map_injective
    dsimp at ha₂
    rw [neg_comp, comp_neg, neg_inj] at ha₂
    simpa only [Functor.map_comp, Functor.map_preimage] using! ha₂
  · simpa only [Functor.map_preimage] using! ha₁

Goal state after:
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
j : J
⊢ T'.mor₁ ≫ Pi.π (fun j ↦ (T j).obj₂) j = Pi.π (fun j ↦ (T j).obj₁) j ≫ (T j).mor₁

Tactic:
by simp [f₁, T']

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 ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (Triangle.mk (F.map X✝.mor₁) (F.map X✝.mor₂) (F.map X✝.mor₃ ≫ (commShiftIso F 1).hom.app X✝.obj₁)).mor₂ ≫
      F.map f.hom₃ =
    F.map f.hom₂ ≫
      (Triangle.mk (F.map Y✝.mor₁) (F.map Y✝.mor₂) (F.map Y✝.mor₃ ≫ (commShiftIso F 1).hom.app Y✝.obj₁)).mor₂

Tactic:
dsimp; simp only [← F.map_comp, f.comm₂]

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✝¹ : F.Full
inst✝ : F.Faithful
X Y : Triangle C
f : F.mapTriangle.obj X ⟶ F.mapTriangle.obj Y
⊢ F.map (X.mor₂ ≫ F.preimage f.hom₃) = F.map (F.preimage f.hom₂ ≫ Y.mor₂)

Tactic:
simpa only [mapTriangle_obj, map_comp, map_preimage] using! f.comm₂

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
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ m + n + a = m + a'

Tactic:
← ha',

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
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ m + n + a = m + (n + a)
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✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ m + n + a = m + a'

Tactic:
← ha',

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✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ m + n + a = m + (n + a)
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✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ m + n + a = m + a'

Tactic:
← ha',

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✝ : F.ShiftSequence M
n m mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ m + n + a = m + (n + a)
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✝ : F.ShiftSequence M
X Y : C
m : M
f : X ⟶ (shiftFunctor C m).obj Y
n mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ mn + a = m + a'

Tactic:
← ha',

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✝ : F.ShiftSequence M
X Y : C
m : M
f : X ⟶ (shiftFunctor C m).obj Y
n mn : M
hnm : m + n = mn
a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
⊢ mn + a = m + (n + a)
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✝¹ : F.ShiftSequence M
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ n + a' = a

Tactic:
← ha',

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✝¹ : F.ShiftSequence M
inst✝ : F.ShiftSequence G
X Y : C
m : G
f : X ⟶ (shiftFunctor C m).obj Y
n : G
hnm : n + m = 0
a a' : G
ha' : m + a = a'
⊢ n + (m + a) = a
Module: Mathlib.CategoryTheory.PathCategory.Basic

Goal state before:
pp: V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
⊢ F = G

Tactic:
fapply Functor.ext
  · intro X
    rw [h_obj]
  · intro X Y f
    induction f with
    | nil => erw [F.map_id, G.map_id, Category.id_comp, eqToHom_trans, eqToHom_refl]
    | cons g e ih =>
      erw [F.map_comp g (Quiver.Hom.toPath e), G.map_comp g (Quiver.Hom.toPath e), ih, h]
      simp only [Category.id_comp, eqToHom_refl, eqToHom_trans_assoc, Category.assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Category.Quiv

Goal state before:
pp: ⊢ Functor.whiskerRight { app := fun x ↦ Paths.of ↑((𝟭 Quiv).obj x), naturality := adj._proof_1 } Cat.free ≫
      (Cat.free.associator forget Cat.free).hom ≫
        Cat.free.whiskerLeft { app := fun C ↦ (pathComposition ↑C).toCatHom, naturality := ⋯ } =
    NatTrans.id (𝟭 Quiv ⋙ Cat.free)

Tactic:
by
      ext V
      exact freeMap_pathsOf_pathComposition V

Goal state after:
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 ◫ τ₂
X : W.Localization
eq : (objEquiv W).toFun ((objEquiv W).invFun X) = X
⊢ τ₁.app X = τ₂.app X

Tactic:
simp only [objEquiv] at eq

Goal state after:
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 ◫ τ₂
X : W.Localization
eq : W.Q.obj X.as.obj = X
⊢ τ₁.app X = τ₂.app X
Module: Mathlib.CategoryTheory.Localization.Predicate

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
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₂
F₁ : W.Localization ⥤ D := Construction.lift L₁ ⋯
⊢ L₂.IsLocalization W

Tactic:
let F₂ := Localization.Construction.lift L₂ h

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
W : MorphismProperty C
L₁ L₂ : C ⥤ D
e : L₁ ≅ L₂
inst✝ : L₁.IsLocalization W
h : W.IsInvertedBy L₂
F₁ : W.Localization ⥤ D := Construction.lift L₁ ⋯
F₂ : W.Localization ⥤ D := Construction.lift L₂ h
⊢ L₂.IsLocalization W
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 : C
f₁ f₂ f₃ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₃ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
h₃ : f₃ = α.thd.map L ⋯
⊢ add' W (α.forgetThd.add.map L ⋯) f₃ = add' W f₁ (α.forgetFst.add.map L ⋯)

Tactic:
add'_eq W _ _ (LeftFraction₂.mk (α.f + α.f') α.f'' α.s α.hs) rfl h₃,

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f₁ f₂ f₃ : L.obj X ⟶ L.obj Y
α : W.LeftFraction₃ X Y
h₁ : f₁ = α.fst.map L ⋯
h₂ : f₂ = α.snd.map L ⋯
h₃ : f₃ = α.thd.map L ⋯
⊢ { Y' := α.Y', f := α.f + α.f', f' := α.f'', s := α.s, hs := ⋯ }.add.map L ⋯ = add' W f₁ (α.forgetFst.add.map L ⋯)
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
⊢ AddCommGroup (L.obj X ⟶ L.obj Y)

Tactic:
by
  letI : Zero (L.obj X ⟶ L.obj Y) := ⟨L.map 0⟩
  letI : Add (L.obj X ⟶ L.obj Y) := ⟨add' W⟩
  letI : Neg (L.obj X ⟶ L.obj Y) := ⟨neg' W⟩
  exact
    { add_assoc := add'_assoc _
      add_zero := add'_zero _
      add_comm := add'_comm _
      zero_add := zero_add' _
      neg_add_cancel := neg'_add'_self _
      nsmul := nsmulRec
      zsmul := zsmulRec }

Goal state after:
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:
obtain ⟨f, rfl⟩ := (homEquiv eX eY).symm.surjective f

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
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'
g₁ g₂ : Y' ⟶ Z'
f : L.obj X ⟶ L.obj Y
⊢ (homEquiv eX eY).symm f ≫ add W eY eZ g₁ g₂ =
    add W eX eZ ((homEquiv eX eY).symm f ≫ g₁) ((homEquiv eX eY).symm f ≫ g₂)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive

Goal state before:
pp: case mpr
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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
⊢ G.map (L.map φ.add.f) = G.map (L.map φ.fst.f) + G.map (L.map φ.snd.f)

Tactic:
← Functor.comp_map,

Goal state after:
case mpr
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
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
⊢ (L ⋙ G).map φ.add.f = G.map (L.map φ.fst.f) + G.map (L.map φ.snd.f)
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
this : HasCardinalLT (ULift.{max u' w, u} T₁ × ULift.{max u w, u'} T₂) κ
⊢ HasCardinalLT (T₁ × T₂) κ

Tactic:
exact this.of_surjective (fun ⟨x₁, x₂⟩ ↦ ⟨ULift.down x₁, ULift.down x₂⟩) (fun ⟨x₁, x₂⟩ ↦
    ⟨⟨ULift.up x₁, ULift.up x₂⟩, rfl⟩)

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
⊢ ∀ {X Y : Localization W} (f : Hom W X Y), (Hom.mk (ofHom W (𝟙 X))).comp f = f

Tactic:
by
    rintro (X Y : C) f
    obtain ⟨z, rfl⟩ := Hom.mk_surjective f
    rw [Hom.comp_eq, comp_eq (ofHom W (𝟙 X)) z (ofHom W z.f) (by simp)]
    dsimp
    simp only [id_comp, comp_id]

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

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
L : C ⥤ D
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Preadditive C
inst✝⁶ : HasZeroObject C
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁴ : Pretriangulated C
inst✝³ : HasShift D ℤ
inst✝² : L.CommShift ℤ
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : D
f : X ⟶ Y
this : L.mapArrow.EssSurj
φ : Arrow C
e : L.mapArrow.obj φ ≅ Arrow.mk f
Z : C
g : φ.right ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj φ.left
H : Triangle.mk φ.hom g h ∈ distinguishedTriangles
⊢ (L.map h ≫ (Functor.commShiftIso L 1).hom.app φ.left ≫ (shiftFunctor D 1).map (Arrow.Hom.left e.hom)) ≫
      (shiftFunctor D 1).map e.inv.left =
    𝟙 (L.obj Z) ≫ L.map h ≫ (Functor.commShiftIso L 1).hom.app φ.left

Tactic:
simp only [assoc, id_comp, ← Functor.map_comp, ← Arrow.comp_left, e.hom_inv_id, Arrow.id_left,
    Functor.mapArrow_obj, Arrow.mk_left, Functor.map_id, comp_id]

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
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
⊢ ∀ (X Y : Localization W) (f : X ⟶ Y), F₁.map f = eqToHom ⋯ ≫ F₂.map f ≫ eqToHom ⋯

Tactic:
by
    rintro (X Y : C) f
    obtain ⟨f, rfl⟩ := Hom.mk_surjective f
    rw [show Hom.mk f = homMk (mk f.f f.s f.hs) by rfl,
      ← Q_map_comp_Qinv f.f f.s f.hs, F₁.map_comp, F₂.map_comp, assoc]
    erw [Functor.congr_hom h f.f]
    rw [assoc, assoc]
    congr 2
    have := inverts W _ f.hs
    rw [← cancel_epi (F₂.map ((Q W).map f.s)), ← F₂.map_comp_assoc,
      Qiso_hom_inv_id, Functor.map_id, id_comp]
    erw [Functor.congr_hom h.symm f.s]
    dsimp
    rw [assoc, assoc, eqToHom_trans_assoc, eqToHom_refl, id_comp, ← F₁.map_comp,
      Qiso_hom_inv_id]
    dsimp
    rw [F₁.map_id, comp_id]

Goal state after: