mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C (0 + a)).obj X = (shiftFunctor C a).obj ((𝟭 C).obj X)

Tactic:
dsimp; rw [zero_add]

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

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
a : A
X : C
⊢ (shiftFunctor C a).obj ((𝟭 C).obj X) = (shiftFunctor C (0 + a)).obj X

Tactic:
dsimp; rw [zero_add]

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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C C₁ C₂ C₃ : HomologicalComplex V c
f : (i : ι) → C₁.X i ≅ C₂.X i
hf : ∀ (i j : ι), c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom
⊢ { f := fun i ↦ (f i).hom, comm' := hf } ≫ { f := fun i ↦ (f i).inv, comm' := ⋯ } = 𝟙 C₁

Tactic:
by
    ext i
    exact (f i).hom_inv_id

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
J : Type u_3
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_3} J
c : ComplexShape ι
inst✝ : HasZeroMorphisms C
F : J ⥤ HomologicalComplex C c
s : Cocone F
hs : (i : ι) → IsColimit ((eval C c i).mapCocone s)
t : Cocone F
i i' : ι
x✝ : c.Rel i i'
⊢ (hs i).desc ((eval C c i).mapCocone t) ≫ t.pt.d i i' = s.pt.d i i' ≫ (hs i').desc ((eval C c i').mapCocone t)

Tactic:
apply IsColimit.hom_ext (hs i)
        intro j
        have eq := fun k => (hs k).fac ((eval C c k).mapCocone t)
        simp only [Functor.mapCocone_ι_app, eval_map] at eq
        simp only [Functor.mapCocone_ι_app, eval_map]
        rw [reassoc_of% (eq i), Hom.comm_assoc, eq i', Hom.comm]

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 : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q' = q
⊢ p + n = q'

Tactic:
rw [hq', hpq]

Goal state after:
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 : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ (dNext k₁) hom + (prevD k₁) hom = C.d k₁ k₀ ≫ hom k₀ k₁

Tactic:
rw [dNext_eq hom r₁₀, prevD, AddMonoidHom.mk'_apply, D.shape, comp_zero, add_zero]

Goal state after:
case a
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
k₁ k₀ : ι
r₁₀ : c.Rel k₁ k₀
hk₁ : ∀ (l : ι), ¬c.Rel l k₁
hom : (i j : ι) → C.X i ⟶ D.X j
⊢ ¬c.Rel (c.prev k₁) k₁
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 : ℤ
⊢ δ 1 2 (Cochain.diff K) = 0

Tactic:
by
    ext p q hpq
    simp only [Cochain.zero_v, δ_v 1 2 rfl _ p q hpq _ _ rfl rfl, Cochain.diff_v,
      HomologicalComplex.d_comp_d, smul_zero, add_zero]

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 : ℤ
φ₁ φ₂ : F ⟶ G
z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p q : ℤ
hpq : p + -1 = q
⊢ (if hij : p + -1 = q then (↑z).v p q hij else 0) = (↑z).v p q hpq

Tactic:
dif_pos hpq

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
φ₁ φ₂ : F ⟶ G
z : { z // ofHom φ₁ = δ (-1) 0 z + ofHom φ₂ }
p q : ℤ
hpq : p + -1 = q
⊢ (↑z).v p q hpq = (↑z).v p q hpq
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
r : HomRel C
inst✝¹ : IsStableUnderPrecomp r
inst✝ : IsStableUnderPostcomp r
⊢ CompClosure r = r

Tactic:
dsimp [HomRel]
  ext
  simp only [compClosure_iff_self]

Goal state after:
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
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a b : R
f : X ⟶ Y
⊢ (functor r).map ((a * b) • f) = (functor r).map (a • b • f)

Tactic:
mul_smul

Goal state after:
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
X Y : C
smul : SMul R ((functor r).obj X ⟶ (functor r).obj Y) := Linear.smul r hr ((functor r).obj X) ((functor r).obj Y)
a b : R
f : X ⟶ Y
⊢ (functor r).map (a • b • f) = (functor r).map (a • b • f)
Module: Mathlib.Algebra.Homology.HomotopyCategory

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_2
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
f : HomotopyEquiv C D
⊢ (quotient V c).map f.hom ≫ (quotient V c).map f.inv = 𝟙 ((quotient V c).obj C)

Tactic:
rw [← (quotient V c).map_comp, ← (quotient V c).map_id]
    exact eq_of_homotopy _ _ f.homotopyHomInvId

Goal state after:
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 : HomologicalComplex C c
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✝⁴ : ∀ (i : ι), HasBinaryBiproduct (F.X i) (F.X i)
inst✝³ : HasHomotopyCofiber (biprod.lift (𝟙 F) (-𝟙 F))
inst✝² :
  ∀ (i : ι), HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i) (((H.mapHomologicalComplex c).obj F).X i)
inst✝¹ :
  HasHomotopyCofiber (biprod.lift (𝟙 ((H.mapHomologicalComplex c).obj F)) (-𝟙 ((H.mapHomologicalComplex c).obj F)))
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex c).map (biprod.lift (𝟙 F) (-𝟙 F)))
hc : ∀ (j : ι), ∃ i, c.Rel i j
⊢ (H.mapHomologicalComplex c).map (ι₀ F) ≫ (mapHomologicalComplexObjIso F H hc).hom =
    ι₀ ((H.mapHomologicalComplex c).obj F)

Tactic:
by
  dsimp [mapHomologicalComplexObjIso, ι₀, homotopyCofiber.mapArrowHom]
  rw [Functor.map_comp, assoc, homotopyCofiber.inr_mapHomologicalComplexObjIso_hom_assoc,
    homotopyCofiber.inr_desc, ← Category.assoc]
  congr 1
  apply biprod.hom_ext <;> simp [← Functor.map_comp]

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

Goal state before:
pp: ι : Type u_3
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
f : K ⟶ L
x✝ : IsIso ((quotient V c).map f)
g : L ⟶ K
hg : (quotient V c).map g = inv ((quotient V c).map f)
⊢ homotopyEquivalences V c f

Tactic:
let e : HomotopyEquiv K L :=
    { hom := f
      inv := g
      homotopyHomInvId := HomotopyCategory.homotopyOfEq _ _ (by cat_disch)
      homotopyInvHomId := HomotopyCategory.homotopyOfEq _ _ (by cat_disch) }

Goal state after:
ι : Type u_3
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
K L : HomologicalComplex V c
f : K ⟶ L
x✝ : IsIso ((quotient V c).map f)
g : L ⟶ K
hg : (quotient V c).map g = inv ((quotient V c).map f)
e : HomotopyEquiv K L :=
  { hom := f, inv := g, homotopyHomInvId := homotopyOfEq (f ≫ g) (𝟙 K) ⋯,
    homotopyInvHomId := homotopyOfEq (g ≫ f) (𝟙 L) ⋯ }
⊢ homotopyEquivalences V c f
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.hom.hom₃ ≫ e.inv.hom₃ = 𝟙 A.obj₃

Tactic:
← comp_hom₃,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ (e.hom ≫ e.inv).hom₃ = 𝟙 A.obj₃
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ e.inv.hom₃ ≫ e.hom.hom₃ = 𝟙 B.obj₃

Tactic:
← comp_hom₃,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
A B : Triangle C
e : A ≅ B
⊢ (e.inv ≫ e.hom).hom₃ = 𝟙 B.obj₃
Module: Mathlib.CategoryTheory.Triangulated.Rotate

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
X : C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
⊢ (rotate C).IsEquivalence

Tactic:
by
  change (triangleRotation C).functor.IsEquivalence
  infer_instance

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

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
F G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a b : A
X : C
⊢ F.map ((shiftFunctorAdd C a b).hom.app X) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫
          (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (shiftFunctor D (a + b)).map (e.hom.app X) =
    F.map ((shiftFunctorAdd C a b).hom.app X) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map (e.hom.app ((shiftFunctor C a).obj X)) ≫
          (shiftFunctor D b).map (e.inv.app ((shiftFunctor C a).obj X)) ≫
            (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫
              (shiftFunctor D b).map ((shiftFunctor D a).map (e.hom.app X)) ≫ (shiftFunctorAdd D a b).inv.app (G.obj X)

Tactic:
simp only [← Functor.map_comp_assoc, e.hom_inv_id_app_assoc]

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
F G : C ⥤ D
e : F ≅ G
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
a b : A
X : C
⊢ F.map ((shiftFunctorAdd C a b).hom.app X) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map ((commShiftIso F a).hom.app X) ≫
          (shiftFunctorAdd D a b).inv.app (F.obj X) ≫ (shiftFunctor D (a + b)).map (e.hom.app X) =
    F.map ((shiftFunctorAdd C a b).hom.app X) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map ((commShiftIso F a).hom.app X ≫ (shiftFunctor D a).map (e.hom.app X)) ≫
          (shiftFunctorAdd D a b).inv.app (G.obj X)
Module: Mathlib.CategoryTheory.Triangulated.TriangleShift

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasShift C ℤ
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
n : ℤ
X✝ Y✝ : Triangle C
f : X✝ ⟶ Y✝
⊢ (n.negOnePow • (CategoryTheory.shiftFunctor C n).map X✝.mor₂) ≫ (CategoryTheory.shiftFunctor C n).map f.hom₃ =
    (CategoryTheory.shiftFunctor C n).map f.hom₂ ≫ (n.negOnePow • (CategoryTheory.shiftFunctor C n).map Y✝.mor₂)

Tactic:
simp only [Linear.units_smul_comp, Linear.comp_units_smul, ← Functor.map_comp, f.comm₂]

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
X : C
⊢ Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X)) ∈ distinguishedTriangles

Tactic:
refine isomorphic_distinguished _
    (inv_rot_of_distTriang _ (contractible_distinguished₁ (X⟦(1 : ℤ)⟧))) _ ?_

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
X : C
⊢ Triangle.mk 0 0 (𝟙 ((shiftFunctor C 1).obj X)) ≅ (Triangle.mk 0 (𝟙 ((shiftFunctor C 1).obj X)) 0).invRotate
Module: Mathlib.CategoryTheory.Triangulated.Functor

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✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasZeroObject D
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
inst✝³ : F.CommShift ℤ
inst✝² : F.IsTriangulated
inst✝¹ : (F.mapComposableArrows 2).EssSurj
inst✝ : IsTriangulated C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
⊢ ∀ {u₁₂ : Y₁ ⟶ Y₂} {u₂₃ : Y₂ ⟶ Y₃} {u₁₃ : Y₁ ⟶ Y₃} (comm : u₁₂ ≫ u₂₃ = u₁₃) {v₁₂ : Y₂ ⟶ Z₁₂}
    {w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁} (h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles) {v₂₃ : Y₃ ⟶ Z₂₃}
    {w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂} (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles) {v₁₃ : Y₃ ⟶ Z₁₃}
    {w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁} (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles),
    Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)

Tactic:
u₁₂

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✝¹³ : HasShift C ℤ
inst✝¹² : HasShift D ℤ
inst✝¹¹ : HasZeroObject C
inst✝¹⁰ : HasZeroObject D
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : Pretriangulated D
F : C ⥤ D
inst✝³ : F.CommShift ℤ
inst✝² : F.IsTriangulated
inst✝¹ : (F.mapComposableArrows 2).EssSurj
inst✝ : IsTriangulated C
Y₁ Y₂ Y₃ Z₁₂ Z₂₃ Z₁₃ : D
u₁₂ : Y₁ ⟶ Y₂
⊢ ∀ {u₂₃ : Y₂ ⟶ Y₃} {u₁₃ : Y₁ ⟶ Y₃} (comm : u₁₂ ≫ u₂₃ = u₁₃) {v₁₂ : Y₂ ⟶ Z₁₂} {w₁₂ : Z₁₂ ⟶ (shiftFunctor D 1).obj Y₁}
    (h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles) {v₂₃ : Y₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (shiftFunctor D 1).obj Y₂}
    (h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles) {v₁₃ : Y₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (shiftFunctor D 1).obj Y₁}
    (h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles), Nonempty (Octahedron comm h₁₂ h₂₃ h₁₃)
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: case refine_2
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✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Epi (S.map (eval C c i)).g
hj : IsColimit (CokernelCofork.ofπ (S.map (eval C c i)).g ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : opcyclesMap S.f i ≫ k = 0
H : { l // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
⊢ S.X₂.pOpcycles i ≫ opcyclesMap S.g i ≫ S.X₃.descOpcycles (↑H) (c.prev i) ⋯ ⋯ = S.X₂.pOpcycles i ≫ k

Tactic:
opcyclesMap_comp_descOpcycles,

Goal state after:
case refine_2
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✝³ : Epi S.g
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Epi (S.map (eval C c i)).g
hj : IsColimit (CokernelCofork.ofπ (S.map (eval C c i)).g ⋯)
A : C
k : S.X₂.opcycles i ⟶ A
hk : opcyclesMap S.f i ≫ k = 0
H : { l // S.g.f i ≫ l = S.X₂.pOpcycles i ≫ k }
⊢ S.X₂.pOpcycles i ≫ S.X₂.descOpcycles (S.g.f i ≫ ↑H) (c.prev i) ⋯ ⋯ = S.X₂.pOpcycles i ≫ k
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
h : W (𝟙 X)
⊢ W.paths p → W (composePath p)

Tactic:
exact p.rec (by simpa) fun p f hp hp' ↦ W.comp_mem _ _ (hp hp'.1) hp'.2

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

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : ↑(of V)
f : X ⟶ Y
⊢ ({ obj := ⇑e, map := fun {X Y} ↦ ⇑(he X Y) } ≫
          { obj := ⇑e.symm, map := fun {X Y} f ↦ (he (e.symm X) (e.symm Y)).symm (Quiver.homOfEq f ⋯ ⋯) }).map
      f =
    Quiver.homOfEq ((𝟙 (of V)).map f) ⋯ ⋯

Tactic:
by
    dsimp [Quiv.id_eq_id, Quiv.comp_eq_comp]
    apply (he _ _).injective
    apply Quiver.homOfEq_injective (X' := e X) (Y' := e Y) (by simp) (by simp)
    simp

Goal state after:
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ B.functor.map (L.map (T.unitIso.hom.app X)) =
    (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ B.functor.map (L.map (T.unitIso.hom.app X))

Tactic:
← Functor.comp_map

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ≌ C₂
L : C₁ ⥤ C₃
R : C₂ ⥤ C₄
B : C₃ ≌ C₄
h : CatCommSq T.functor L R B.functor
X : C₁
⊢ (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X) =
    (iso T.symm.inverse L R B.symm.inverse).hom.app X ≫ (L ⋙ B.functor).map (T.unitIso.hom.app X)
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
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
⊢ ∀ ⦃X Y : W.Localization⦄ (f : X ⟶ Y), F₁.map f ≫ NatTransExtension.app τ Y = NatTransExtension.app τ X ≫ F₂.map f

Tactic:
suffices MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤ by
      intro X Y f
      simpa only [← this] using! MorphismProperty.top_apply f
    refine morphismProperty_eq_top'
      (MorphismProperty.naturalityProperty (NatTransExtension.app τ))
      ?_ (MorphismProperty.naturalityProperty.stableUnderInverse _)
    intro X Y f
    dsimp
    simpa only [NatTransExtension.app_eq] using! τ.naturality f

Goal state after:
Module: Mathlib.CategoryTheory.CatCommSq

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ⥤ C₂
L : C₁ ≌ C₃
R : C₂ ≌ C₄
B : C₃ ⥤ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ (R.functor.map (T.map (L.unitIso.hom.app X)) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))

Tactic:
← Functor.comp_map

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
C₄ : Type u_4
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
inst✝ : Category.{v_4, u_4} C₄
T : C₁ ⥤ C₂
L : C₁ ≌ C₃
R : C₂ ≌ C₄
B : C₃ ⥤ C₄
h : CatCommSq T L.functor R.functor B
X : C₁
⊢ ((T ⋙ R.functor).map (L.unitIso.hom.app X) ≫
        R.functor.map
            (R.unitIso.hom.app (T.obj (L.inverse.obj (L.functor.obj X))) ≫
              R.inverse.map ((iso T L.functor R.functor B).hom.app (L.inverse.obj (L.functor.obj X))) ≫
                R.inverse.map (B.map (L.counitIso.hom.app (L.functor.obj X)))) ≫
          R.counitIso.hom.app (B.obj (L.functor.obj X))) ≫
      B.map (L.functor.map (L.unitIso.hom.app X)) =
    (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))
Module: Mathlib.CategoryTheory.Localization.Equivalence

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} D
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ≤ W₂.isoClosure.inverseImage E.functor
hW₂ : W₂.IsInvertedBy L₂
inst✝ : L₁.IsLocalization W₁
iso : E.functor ⋙ L₂ ≅ L₁
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
⊢ IsIso ((E.functor ⋙ W₂.Q).map f)

Tactic:
obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf
    exact ((MorphismProperty.isomorphisms _).arrow_mk_iso_iff
      (W₂.Q.mapArrow.mapIso e)).1 (Localization.inverts W₂.Q W₂ _ hf')

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

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

Tactic:
have hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u := by
      rw [← reassoc_of% hst, ← reassoc_of% hα, ← reassoc_of% hst']

Goal state after:
case mp
C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
φ ψ : W.LeftFraction₂ X Y
Z : C
t₁ : φ.Y' ⟶ Z
t₂ : ψ.Y' ⟶ Z
hst : φ.s ≫ t₁ = ψ.s ≫ t₂
hft : φ.f ≫ t₁ = ψ.f ≫ t₂
ht : W (φ.s ≫ t₁)
Z' : C
t₁' : φ.Y' ⟶ Z'
t₂' : ψ.Y' ⟶ Z'
hst' : φ.s ≫ t₁' = ψ.s ≫ t₂'
hft' : φ.f' ≫ t₁' = ψ.f' ≫ t₂'
ht' : W (φ.s ≫ t₁')
α : W.LeftFraction Z Z'
hα : φ.s ≫ t₁' ≫ α.s = φ.s ≫ t₁ ≫ α.f
Z'' : C
u : α.Y' ⟶ Z''
hu : W u
fac : (t₁' ≫ α.s) ≫ u = (t₁ ≫ α.f) ≫ u
hα' : ψ.s ≫ t₂ ≫ α.f ≫ u = ψ.s ≫ t₂' ≫ α.s ≫ u
⊢ LeftFraction₂Rel φ ψ
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 : C
s : X ⟶ Y
hs : W s
⊢ (Q W).map s ≫ Qinv s hs = 𝟙 ((Q W).obj X)

Tactic:
by
    rw [Q_map_comp_Qinv]
    apply homMk_eq_of_leftFractionRel
    exact ⟨_, 𝟙 Y, s, by simp, by simp, by simpa using hs⟩

Goal state after: