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

Goal state before:
pp: V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f g : A ⟶ B
w : (single V c j).map f = (single V c j).map g
⊢ f = g

Tactic:
← cancel_mono (singleObjXSelf c j B).inv,

Goal state after:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
inst✝¹ : HasZeroObject V
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A B : V
f g : A ⟶ B
w : (single V c j).map f = (single V c j).map g
⊢ f ≫ (singleObjXSelf c j B).inv = g ≫ (singleObjXSelf c j B).inv
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 ι
K : HomologicalComplex V c
p q : ι
h : p = q
⊢ K.X p = K.X q

Tactic:
rw [h]

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
i j k : A
h : i + j = k
⊢ shiftFunctor C k = shiftFunctor C (i + j)

Tactic:
rw [h]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) ≤
    Submodule.restrictScalars S
      (Submodule.span (S ⊗[R] S) ↑(Submodule.span S (Set.range fun s ↦ 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1)))

Tactic:
exact Submodule.subset_span

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : Ω[S⁄R]
⊢ x ∈ Submodule.span S (Set.range ⇑(D R S))

Tactic:
obtain ⟨⟨x, hx⟩, rfl⟩ := fromIdeal_surjective R S x

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S ⊗[R] S
hx : x ∈ ideal R S
⊢ (fromIdeal R S) ⟨x, hx⟩ ∈ Submodule.span S (Set.range ⇑(D R S))
Module: Mathlib.Algebra.Homology.HomologicalComplex

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝⁴ : Category.{v, u} V
inst✝³ : HasZeroMorphisms V
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X (n + 1) ⟶ X n
i j : α
h : i = j + 1
⊢ X i = X (j + 1)

Tactic:
rw [h]

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

Goal state before:
pp: V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
S S' : ShortComplex V
h : S = S'
⊢ (succ S).fst = (succ S').fst

Tactic:
rw [h]

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
X₀ X₁ X₂ : V
d₀ : X₁ ⟶ X₀
d₁ : X₂ ⟶ X₁
s : d₁ ≫ d₀ = 0
succ : (S : ShortComplex V) → (X₃ : V) ×' (d₂ : X₃ ⟶ S.X₁) ×' d₂ ≫ S.f = 0
succ' : {X₀ X₁ : V} → (f : X₁ ⟶ X₀) → (X₂ : V) ×' (d : X₂ ⟶ X₁) ×' d ≫ f = 0
X Y : V
f g : X ⟶ Y
h : f = g
⊢ (succ' f).fst = (succ' g).fst

Tactic:
rw [h]

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
α : Type u_2
inst✝² : AddRightCancelSemigroup α
inst✝¹ : One α
inst✝ : DecidableEq α
X : α → V
d : (n : α) → X n ⟶ X (n + 1)
i j : α
h : i + 1 = j
⊢ X (i + 1) = X j

Tactic:
rw [h]

Goal state after:
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case a
R : Type u
inst✝⁶ : CommRing R
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing A
inst✝⁴ : CommRing B
inst✝³ : Algebra R A
inst✝² : Algebra A B
inst✝¹ : Algebra R B
inst✝ : IsScalarTower R A B
x : B ⊗[A] Ω[A⁄R]
⊢ (mapBaseChange R A B) x ∈ (map R A B B).ker

Tactic:
induction x with
    | zero => simp
    | tmul r s =>
      obtain ⟨x, rfl⟩ := linearCombination_surjective _ _ s
      simp only [mapBaseChange_tmul, LinearMap.mem_ker, map_smul]
      induction x using Finsupp.induction_linear
      · simp
      · simp [smul_add, *]
      · simp
    | add => rw [map_add]; exact add_mem ‹_› ‹_›

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 G : HomologicalComplex C c
φ : F ⟶ G
K : HomologicalComplex C c
x y : (α : G ⟶ K) × Homotopy (φ ≫ α) 0
⊢ x = y ↔ x.fst = y.fst ∧ ∀ (i j : ι), c.Rel j i → x.snd.hom i j = y.snd.hom i j

Tactic:
by
  constructor
  · rintro rfl
    tauto
  · obtain ⟨x₁, x₂⟩ := x
    obtain ⟨y₁, y₂⟩ := y
    rintro ⟨rfl, h⟩
    simp only [Sigma.mk.inj_iff, heq_eq_eq, true_and]
    ext i j
    by_cases hij : c.Rel j i
    · exact h _ _ hij
    · simp only [Homotopy.zero _ _ _ hij]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
⊢ (if p = p ∧ q = q then 𝟙 (K.X p) ≫ f ≫ 𝟙 (L.X q) else 0) = f

Tactic:
if_pos,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
⊢ 𝟙 (K.X p) ≫ f ≫ 𝟙 (L.X q) = f

case hc
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
p q : ℤ
f : K.X p ⟶ L.X q
n : ℤ
hpq : p + n = q
⊢ p = p ∧ q = q
Module: Mathlib.CategoryTheory.Quotient

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
r : HomRel C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
F₁ F₂ : Quotient r ⥤ D
h : functor r ⋙ F₁ = functor r ⋙ F₂
⊢ functor r ⋙ F₁ = functor r ⋙ F₂

Tactic:
rw [h]

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
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
f g h : T₁ ⟶ T₂
⊢ f + g + h = f + (g + h)

Tactic:
by ext <;> apply add_assoc

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₁ X₂ Y : C
g : X₁ ⟶ Y
h : Y ⟶ X₂
mem : Triangle.mk g h 0 ∈ distinguishedTriangles
e : (Triangle.mk g h 0).obj₂ ≅ (Triangle.mk g h 0).obj₁ ⊞ (Triangle.mk g h 0).obj₃
he₁ : g ≫ e.hom = biprod.inl
he₂ : h = e.hom ≫ biprod.snd
⊢ Triangle.mk g h 0 ≅ binaryBiproductTriangle X₁ X₂

Tactic:
refine Triangle.isoMk _ _ (Iso.refl _) e (Iso.refl _)
    (by cat_disch) (by cat_disch) (by simp)

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
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
⊢ T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = (Triangle.π₃.mapIso h.choose).hom ≫ T₂.mor₃

Tactic:
have eq := h.choose_spec.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
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
e₁ : T₁.obj₁ ≅ T₂.obj₁
e₂ : T₁.obj₂ ≅ T₂.obj₂
comm : T₁.mor₁ ≫ e₂.hom = e₁.hom ≫ T₂.mor₁
h :
  ∃ e', e'.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom ∧ e'.hom.hom₂ = Arrow.Hom.right (Arrow.isoMk e₁ e₂ ⋯).hom
eq : h.choose.hom.hom₁ = Arrow.Hom.left (Arrow.isoMk e₁ e₂ ⋯).hom
⊢ T₁.mor₃ ≫ (shiftFunctor C 1).map e₁.hom = (Triangle.π₃.mapIso h.choose).hom ≫ T₂.mor₃
Module: Mathlib.Algebra.Homology.HomologySequence

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : 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 ⋯)
⊢ IsColimit
    (CokernelCofork.ofπ
      { X₁ := S.X₁.opcycles i, X₂ := S.X₂.opcycles i, X₃ := S.X₃.opcycles i, f := opcyclesMap S.f i,
          g := opcyclesMap S.g i, zero := ⋯ }.g
      ⋯)

Tactic:
refine CokernelCofork.IsColimit.ofπ' _ _ (fun {A} k hk => by
    dsimp at k hk ⊢
    have H := CokernelCofork.IsColimit.desc' hj (S.X₂.pOpcycles i ≫ k) (by
      dsimp
      rw [← p_opcyclesMap_assoc, hk, comp_zero])
    dsimp at H
    refine ⟨S.X₃.descOpcycles H.1 _ rfl ?_, ?_⟩
    · rw [← cancel_epi (S.g.f (c.prev i)), comp_zero, Hom.comm_assoc, H.2,
        d_pOpcycles_assoc, zero_comp]
    · rw [← cancel_epi (S.X₂.pOpcycles i), opcyclesMap_comp_descOpcycles, p_descOpcycles, H.2])

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.Exact
inst✝³ : Mono S.f
i : ι
inst✝² : S.X₁.HasHomology i
inst✝¹ : S.X₂.HasHomology i
inst✝ : S.X₃.HasHomology i
this : Mono (S.map (eval C c i)).f
hi : IsLimit (KernelFork.ofι (S.map (eval C c i)).f ⋯)
A : C
k :
  A ⟶
    { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := cyclesMap S.f i, g := cyclesMap S.g i,
        zero := ⋯ }.X₂
hk :
  k ≫
      { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := cyclesMap S.f i, g := cyclesMap S.g i,
          zero := ⋯ }.g =
    0
⊢ { l //
    l ≫
        { X₁ := S.X₁.cycles i, X₂ := S.X₂.cycles i, X₃ := S.X₃.cycles i, f := cyclesMap S.f i, g := cyclesMap S.g i,
            zero := ⋯ }.f =
      k }

Tactic:
by
    dsimp at k hk ⊢
    have H := KernelFork.IsLimit.lift' hi (k ≫ S.X₂.iCycles i) (by
      dsimp
      rw [assoc, ← cyclesMap_i, reassoc_of% hk, zero_comp])
    dsimp at H
    refine ⟨S.X₁.liftCycles H.1 _ rfl ?_, ?_⟩
    · rw [← cancel_mono (S.f.f _), assoc, zero_comp, ← Hom.comm, reassoc_of% H.2,
        iCycles_d, comp_zero]
    · rw [← cancel_mono (S.X₂.iCycles i), liftCycles_comp_cyclesMap, liftCycles_i, H.2]

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

Goal state before:
pp: V : Type u
C : Type u₁
inst✝¹ : Quiver V
inst✝ : Category.{v₁, u₁} C
F : Paths V ⥤ C
⊢ (fun G ↦ Cat.freeMap G ⋙ pathComposition C) ((fun F ↦ Paths.of V ⋙q F.toPrefunctor) F) = F

Tactic:
dsimp
    rw [Cat.freeMap_comp, Functor.assoc, pathComposition_naturality, ← Functor.assoc,
      freeMap_pathsOf_pathComposition, Functor.id_comp]

Goal state after:
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
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{v_3, u_3} E
this : Localization.Construction.lift W.Q ⋯ = 𝟭 W.Localization
⊢ (Localization.Construction.lift W.Q ⋯).IsEquivalence

Tactic:
by
      rw [this]
      infer_instance

Goal state after:
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
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
inst✝ : L.IsLocalization W
⊢ (inducedFunctor ObjectProperty.FullSubcategory.obj).Faithful

Tactic:
apply InducedCategory.faithful

Goal state after:
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₁
⊢ L₂.IsLocalization W

Tactic:
rw [MorphismProperty.IsInvertedBy.iff_of_iso W e] at 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₂
⊢ L₂.IsLocalization W
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
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
P : MorphismProperty D
inst✝¹ : P.RespectsIso
inst✝ : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ e.hom.app Y ≫ (isoOfHom L W f hf).inv = (uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X

Tactic:
← cancel_mono (isoOfHom L W f hf).hom,

Goal state after:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Category.{v_2, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : L.IsLocalization W
P : MorphismProperty D
inst✝¹ : P.RespectsIso
inst✝ : P.IsMultiplicative
h₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (L.map f)
h₂ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) (hf : W f), P (isoOfHom L W f hf).inv
e : W.Q ⋙ (uniq W.Q L W).functor ≅ L := compUniqFunctor W.Q L W
X Y : C
f : X ⟶ Y
hf : W f
⊢ (e.hom.app Y ≫ (isoOfHom L W f hf).inv) ≫ (isoOfHom L W f hf).hom =
    ((uniq W.Q L W).functor.map (isoOfHom W.Q W f hf).inv ≫ e.hom.app X) ≫ (isoOfHom L W f hf).hom
Module: Mathlib.CategoryTheory.Localization.Predicate

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
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
h : W.Q.map f = W.Q.map g
e : W.Q ⋙ (Localization.uniq W.Q L W).functor ≅ L := Localization.compUniqFunctor W.Q L W
⊢ e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map f) ≫ e.hom.app Y =
    e.inv.app X ≫ (Localization.uniq W.Q L W).functor.map (W.Q.map g) ≫ e.hom.app Y

Tactic:
rw [h]

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

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
L : C ⥤ D
W : MorphismProperty C
X Y : C
f g : X ⟶ Y
inst✝ : L.IsLocalization W
h : L.map f = L.map g
e : L ⋙ (Localization.uniq L W.Q W).functor ≅ W.Q := Localization.compUniqFunctor L W.Q W
⊢ e.inv.app X ≫ (Localization.uniq L W.Q W).functor.map (L.map f) ≫ e.hom.app Y =
    e.inv.app X ≫ (Localization.uniq L W.Q W).functor.map (L.map g) ≫ e.hom.app Y

Tactic:
rw [h]

Goal state after:
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 (φ.add.map L ⋯) = G.map (φ.fst.map L ⋯) + G.map (φ.snd.map L ⋯)

Tactic:
← cancel_mono (G.map (L.map φ.s)),

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
⊢ G.map (φ.add.map L ⋯) ≫ G.map (L.map φ.s) = (G.map (φ.fst.map L ⋯) + G.map (φ.snd.map L ⋯)) ≫ G.map (L.map φ.s)
Module: Mathlib.CategoryTheory.ObjectProperty.Shift

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝¹ : AddMonoid A
inst✝ : HasShift C A
h : P ≤ Q
X Y : C
a : A
i : X ≅ (shiftFunctor C a).obj Y
hY : P Y
⊢ Q.shiftClosure A X

Tactic:
refine ⟨Y, a, i, h Y hY⟩

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P Q : ObjectProperty C
A : Type u_2
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : Q.IsClosedUnderIsomorphisms
inst✝ : Q.IsStableUnderShift A
h : P ≤ Q
⊢ Q.shiftClosure A ≤ Q

Tactic:
rw [shiftClosure_eq_self]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
X Y : C
f : Hom W X Y
F : C ⥤ E
hF : W.IsInvertedBy F
⊢ ∀ (a b : W.LeftFraction X Y), LeftFractionRel a b → a.map F hF = b.map F hF

Tactic:
intro a₁ a₂ ⟨Z, t₁, t₂, hst, hft, h⟩
    have := hF _ h
    rw [← cancel_mono (F.map (a₁.s ≫ t₁)), F.map_comp, map_comp_map_s_assoc,
      ← F.map_comp, ← F.map_comp, hst, hft, F.map_comp,
      F.map_comp, map_comp_map_s_assoc]

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

Goal state before:
pp: C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
T₁ T₃ : Triangle C
mem₁ : T₁ ∈ distinguishedTriangles
mem₃ : T₃ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₃.obj₁
b : T₁.obj₂ ⟶ T₃.obj₂
Z₅ : C
g₅ : T₃.obj₁ ⟶ Z₅
h₅ : Z₅ ⟶ (shiftFunctor C 1).obj T₁.obj₁
mem₅ : Triangle.mk a g₅ h₅ ∈ distinguishedTriangles
mem₅' : P Z₅
Z₄ : C
g₄ : T₃.obj₂ ⟶ Z₄
h₄ : Z₄ ⟶ (shiftFunctor C 1).obj T₁.obj₂
mem₄ : Triangle.mk b g₄ h₄ ∈ distinguishedTriangles
mem₄' : P Z₄
comm : T₁.mor₁ ≫ b = a ≫ T₃.mor₁
⊢ ∃ c, ∃ (_ : P.trW c), T₁.mor₂ ≫ c = b ≫ T₃.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₃.mor₃

Tactic:
obtain ⟨Z₂, g₂, h₂, mem₂⟩ := distinguished_cocone_triangle (T₁.mor₁ ≫ b)

Goal state after:
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P : ObjectProperty C
inst✝¹ : IsTriangulated C
inst✝ : P.IsTriangulated
T₁ T₃ : Triangle C
mem₁ : T₁ ∈ distinguishedTriangles
mem₃ : T₃ ∈ distinguishedTriangles
a : T₁.obj₁ ⟶ T₃.obj₁
b : T₁.obj₂ ⟶ T₃.obj₂
Z₅ : C
g₅ : T₃.obj₁ ⟶ Z₅
h₅ : Z₅ ⟶ (shiftFunctor C 1).obj T₁.obj₁
mem₅ : Triangle.mk a g₅ h₅ ∈ distinguishedTriangles
mem₅' : P Z₅
Z₄ : C
g₄ : T₃.obj₂ ⟶ Z₄
h₄ : Z₄ ⟶ (shiftFunctor C 1).obj T₁.obj₂
mem₄ : Triangle.mk b g₄ h₄ ∈ distinguishedTriangles
mem₄' : P Z₄
comm : T₁.mor₁ ≫ b = a ≫ T₃.mor₁
Z₂ : C
g₂ : T₃.obj₂ ⟶ Z₂
h₂ : Z₂ ⟶ (shiftFunctor C 1).obj T₁.obj₁
mem₂ : Triangle.mk (T₁.mor₁ ≫ b) g₂ h₂ ∈ distinguishedTriangles
⊢ ∃ c, ∃ (_ : P.trW c), T₁.mor₂ ≫ c = b ≫ T₃.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor C 1).map a = c ≫ T₃.mor₃
Module: Mathlib.Algebra.Homology.DerivedCategory.HomologySequence

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasDerivedCategory C
T : Triangle (CochainComplex C ℤ)
hT : DerivedCategory.Q.mapTriangle.obj T ∈ distinguishedTriangles
n₀ n₁ : ℤ
h : n₀ + 1 = n₁
⊢ homologyδOfTriangle T n₀ n₁ h ≫ homologyMap T.mor₁ n₁ = 0

Tactic:
rw [← cancel_epi ((DerivedCategory.homologyFunctorFactors _ _).hom.app _),
    homologyFunctorFactors_hom_app_homologyδOfTriangle_assoc ..,
    ← DerivedCategory.homologyFunctorFactors_hom_naturality]
  dsimp
  rw [reassoc_of% dsimp% DerivedCategory.HomologySequence.δ_comp _ hT n₀ n₁ h]
  simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i✝ j✝ : Option ι
i j : ι
⊢ 𝟙 (X K.op (some i)) ≫ (d K (some j) (some i)).op = d K.op (some i) (some j) ≫ 𝟙 (X K.op (some j))

Tactic:
simp only [d_eq _ rfl rfl, op_comp, assoc, id_comp, comp_id]

Goal state after:
ι : Type u_1
c : ComplexShape ι
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
i✝ j✝ : Option ι
i j : ι
⊢ (XIso K ⋯).inv.op ≫ (K.d j i).op ≫ (XIso K ⋯).hom.op = (XIso K.op ⋯).hom ≫ K.op.d i j ≫ (XIso K.op ⋯).inv
Module: Mathlib.Algebra.Homology.HomotopyCategory.Triangulated

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v, u_1} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X₁✝ X₂✝ X₃✝ : CochainComplex C ℤ
f : X₁✝ ⟶ X₂✝
g : X₂✝ ⟶ X₃✝
inst✝ : HasZeroObject C
X₁ X₂ X₃ : CochainComplex C ℤ
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
α : mappingCone.triangle u₁₂ ⟶ mappingCone.triangle (u₁₂ ≫ u₂₃) := mappingCone.triangleMap u₁₂ (u₁₂ ≫ u₂₃) (𝟙 X₁) u₂₃ ⋯
β : mappingCone.triangle (u₁₂ ≫ u₂₃) ⟶ mappingCone.triangle u₂₃ := mappingCone.triangleMap (u₁₂ ≫ u₂₃) u₂₃ u₁₂ (𝟙 X₃) ⋯
⊢ ((quotient C (ComplexShape.up ℤ)).mapTriangle.obj (mappingCone.triangle u₁₂)).mor₃ ≫
      (CategoryTheory.shiftFunctor (HomotopyCategory C (ComplexShape.up ℤ)) 1).map
        ((quotient C (ComplexShape.up ℤ)).mapTriangle.map α).hom₁ =
    (quotient C (ComplexShape.up ℤ)).map (mappingCone.triangle u₁₂).mor₃ ≫
      (Functor.commShiftIso (quotient C (ComplexShape.up ℤ)) 1).hom.app (mappingCone.triangle u₁₂).obj₁

Tactic:
dsimp [α]; simp

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Extend

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝² : Category.{v_1, u_3} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
K : HomologicalComplex C c
e : c.Embedding c'
i' j' : ι'
j : ι
hj : e.f j = j'
hj' : ¬c.Rel (c.prev j) j
⊢ (K.extend e).d i' j' = 0

Tactic:
obtain hi' | ⟨i, hi⟩ := (e.r i').eq_none_or_eq_some
  · exact extend.d_none_eq_zero _ _ _ hi'
  · rw [extend_d_eq K e (e.f_eq_of_r_eq_some hi) hj, K.shape, zero_comp, comp_zero]
    intro hij
    obtain rfl := c.prev_eq' hij
    exact hj' hij

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
inst✝ : e.IsRelIff
i j : ι
hi : c.Rel i j
a✝ : c'.Rel (e.f i) (c'.next (e.f i))
⊢ c'.Rel (e.f i) (e.f j)

Tactic:
by simpa only [e.rel_iff] using hi

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.Boundary

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
hj : e.BoundaryLE j
k' : ι'
hk' : c'.Rel (e.f j) k'
a : ι
ha : e.f a = k'
⊢ c'.Rel (e.f j) (e.f a)

Tactic:
simpa only [ha] using hk'

Goal state after:
Module: Mathlib.Algebra.Homology.Embedding.HomEquiv

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
C : Type u_3
inst✝³ : Category.{v_1, u_3} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
K : HomologicalComplex C c'
L : HomologicalComplex C c
inst✝ : e.IsRelIff
ψ : K ⟶ L.extend e
⊢ e.HasLift (e.homRestrict ψ)

Tactic:
by
  intro j hj i' hij'
  have : (L.extend e).d i' (e.f j) = 0 := by
    apply (L.isZero_extend_X e i' (hj.notMem hij')).eq_of_src
  dsimp [homRestrict]
  rw [homRestrict.f_eq ψ rfl, restrictionXIso, eqToIso_refl, Iso.refl_hom, id_comp,
    ← ψ.comm_assoc, this, zero_comp, comp_zero]

Goal state after: