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

Goal state before:
pp: ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
i : ι
α : Type u_5
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
n : α
⊢ F.map 0 = 0

Tactic:
Functor.map_zero

Goal state after:
ι : Type u_1
V : Type u
inst✝¹¹ : Category.{v, u} V
inst✝¹⁰ : Preadditive V
W : Type u_2
inst✝⁹ : Category.{v_1, u_2} W
inst✝⁸ : Preadditive W
W₁ : Type u_3
W₂ : Type u_4
inst✝⁷ : Category.{v_2, u_3} W₁
inst✝⁶ : Category.{v_3, u_4} W₂
inst✝⁵ : HasZeroMorphisms W₁
inst✝⁴ : HasZeroMorphisms W₂
c : ComplexShape ι
C D : HomologicalComplex V c
f : C ⟶ D
i : ι
α : Type u_5
inst✝³ : AddRightCancelSemigroup α
inst✝² : One α
inst✝¹ : DecidableEq α
F : W₁ ⥤ W₂
inst✝ : F.PreservesZeroMorphisms
X : α → W₁
d : (n : α) → X (n + 1) ⟶ X n
sq : ∀ (n : α), d (n + 1) ≫ d n = 0
n : α
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Shift.Basic

Goal state before:
pp: C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
X : C
i j : A
⊢ (shiftComm X i j).symm = shiftComm X j i

Tactic:
ext
  exact NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorComm_symm C i j)) X

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✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m₁ m₂ m₃ : A
X : C
⊢ (shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫
      (shiftFunctor C m₁).map ((shiftFunctorAdd C m₂ m₃).hom.app X) ≫
        (shiftFunctorComm C m₁ m₃).inv.app ((shiftFunctor C m₂).obj X) ≫
          (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).inv.app X) =
    (shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X) ≫
      (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).hom.app X) ≫
        𝟙 ((shiftFunctor C m₃).obj ((shiftFunctor C m₁).obj ((shiftFunctor C m₂).obj X))) ≫
          (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).inv.app X)

Tactic:
simp only [Category.id_comp, ← Functor.map_comp, Iso.hom_inv_id_app]

Goal state after:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddCommMonoid A
inst✝ : HasShift C A
m₁ m₂ m₃ : A
X : C
⊢ (shiftFunctorComm C m₁ (m₂ + m₃)).hom.app X ≫
      (shiftFunctor C m₁).map ((shiftFunctorAdd C m₂ m₃).hom.app X) ≫
        (shiftFunctorComm C m₁ m₃).inv.app ((shiftFunctor C m₂).obj X) ≫
          (shiftFunctor C m₃).map ((shiftFunctorComm C m₁ m₂).inv.app X) =
    (shiftFunctorAdd C m₂ m₃).hom.app ((shiftFunctor C m₁).obj X) ≫
      (shiftFunctor C m₃).map (𝟙 ((shiftFunctor C m₁ ⋙ shiftFunctor C m₂).obj X))
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
⊢ ∀ (a b : S), ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)) (single a b) = b𝖣a

Tactic:
intro a b

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
a b : S
⊢ ((derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ linearCombination S ⇑(D R S)) (single a b) = b𝖣a
Module: Mathlib.RingTheory.Kaehler.Basic

Goal state before:
pp: case h
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
h : Function.Surjective ⇑(algebraMap A B)
x : A →₀ A
hx : x ∈ ↑(mapRange.linearMap (Algebra.linearMap A B) ∘ₗ lmapDomain A A ⇑(algebraMap A B)).ker
c : B
a✝ : c ∈ Finset.image (⇑(algebraMap A B)) x.support
this : ∑ i ∈ x.support with (algebraMap A B) i = c, x i ∈ RingHom.ker (algebraMap A B)
a : A
ha : (algebraMap A B) a = c
⊢ 1 ⊗ₜ[A] ((∑ x_1 ∈ x.support with (algebraMap A B) x_1 = c, x x_1) • (D R A) a) = 0

Tactic:
rw [← TensorProduct.smul_tmul, ← Algebra.algebraMap_eq_smul_one, RingHom.mem_ker.mp this,
        TensorProduct.zero_tmul]

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

Goal state before:
pp: 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
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
hj : c.Rel j (c.next j)
⊢ (φ ≫ inr φ).f j =
    ((dNext j) fun i j ↦ if hij : c.Rel j i then inlX φ i j hij else 0) + inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j

pp: 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
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ (φ ≫ inr φ).f j =
    ((dNext j) fun i j ↦ if hij : c.Rel j i then inlX φ i j hij else 0) + inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j

Tactic:
· simp only [comp_f, homotopyCofiber_d, zero_f, add_zero,
        inlX_d φ i j _ hij hj, dNext_eq _ hj, dif_pos hj,
        add_neg_cancel_left, inr_f]

Goal state after:
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
hc : ∀ (j : ι), ∃ i, c.Rel i j
j i : ι
hij : c.Rel i j
hj : ¬c.Rel j (c.next j)
⊢ (φ ≫ inr φ).f j =
    ((dNext j) fun i j ↦ if hij : c.Rel j i then inlX φ i j hij else 0) + inlX φ j i hij ≫ (homotopyCofiber φ).d i j +
      Hom.f 0 j
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplex

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
p : ℤ
eq : φ₁.f p = (dNext p) h.hom + (prevD p) h.hom + φ₂.f p
⊢ (δ (-1) 0 (Cochain.ofHomotopy h)).v p p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯

Tactic:
dNext_eq h.hom (show (ComplexShape.up ℤ).Rel p (p + 1) by simp),

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ₁ φ₂ : F ⟶ G
h : Homotopy φ₁ φ₂
p : ℤ
eq : φ₁.f p = F.d p (p + 1) ≫ h.hom (p + 1) p + (prevD p) h.hom + φ₂.f p
⊢ (δ (-1) 0 (Cochain.ofHomotopy h)).v p p ⋯ = (Cochain.ofHom φ₁ - Cochain.ofHom φ₂).v p p ⋯
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:
by
          #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.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
f g : C ⟶ D
h : homotopyEquivalences V c f
hfg : Homotopy f g
⊢ homotopyEquivalences V c g

Tactic:
obtain ⟨e, rfl⟩ := h

Goal state after:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
c : ComplexShape ι
C D : HomologicalComplex V c
g : C ⟶ D
e : HomotopyEquiv C D
hfg : Homotopy e.hom g
⊢ homotopyEquivalences V c g
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)
f : X ⟶ Y
⊢ (functor r).map 0 = 0

Tactic:
Functor.map_zero

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)
f : X ⟶ Y
⊢ 0 = 0
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 ι
inst✝ : HasZeroObject V
⊢ (quotient V c).map 0 = 0

Tactic:
Functor.map_zero

Goal state after:
R : Type u_1
inst✝³ : Semiring R
ι : Type u_2
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : Preadditive V
c : ComplexShape ι
inst✝ : HasZeroObject V
⊢ 0 = 0
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 ι
W : Type u_3
inst✝⁴ : Category.{v_1, u_3} W
inst✝³ : Preadditive W
F : V ⥤ W
inst✝² : F.Full
inst✝¹ : F.Faithful
inst✝ : F.Additive
⊢ ∀ {X Y : HomotopyCategory V c}, Function.Injective (F.mapHomotopyCategory c).map

Tactic:
by
    rintro ⟨K⟩ ⟨L⟩ f₁ f₂ h
    obtain ⟨f₁, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective f₁
    obtain ⟨f₂, rfl⟩ := (HomotopyCategory.quotient _ _).map_surjective f₂
    exact HomotopyCategory.eq_of_homotopy _ _
      (F.preimageHomotopy (HomotopyCategory.homotopyOfEq _ _ h))

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K : CochainComplex C ℤ
a b ab : ℤ
h : a + b = ab
n : ℤ
⊢ ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) a b ab h).hom.app K).f n = (XIsoOfEq K ⋯).hom

Tactic:
by
  subst h
  rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftFunctorAdd_hom_app_f]

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
p q : ℤ
hpq : p + n = q
p' : ℤ
hp' : p' + n' = q
⊢ (γ.leftUnshift n hn).v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a p' p ⋯).inv ≫ γ.v p' q ⋯

Tactic:
obtain rfl : p' = p - a := by lia

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n' a : ℤ
γ : Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n'
n : ℤ
hn : n + a = n'
p q : ℤ
hpq : p + n = q
hp' : p - a + n' = q
⊢ (γ.leftUnshift n hn).v p q hpq =
    (a * n' + a * (a - 1) / 2).negOnePow • (K.shiftFunctorObjXIso a (p - a) p ⋯).inv ≫ γ.v (p - a) q ⋯
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
n : A
X : C
⊢ (((whiskeringLeft C D D).obj F).map (Induced.add F s i 0 n).hom).app X =
    (((whiskeringLeft C D D).obj F).map (eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n))).app X

Tactic:
have eq := dcongr_arg (fun a => (i a).hom.app X) (zero_add n)

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
n : A
X : C
eq : (i (0 + n)).hom.app X = eqToHom ⋯ ≫ (i n).hom.app X ≫ eqToHom ⋯
⊢ (((whiskeringLeft C D D).obj F).map (Induced.add F s i 0 n).hom).app X =
    (((whiskeringLeft C D D).obj F).map (eqToHom ⋯ ≫ whiskerRight (Induced.zero F s i).inv (s n))).app X
Module: Mathlib.CategoryTheory.Shift.CommShift

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
F : C ⥤ D
B : Type u_5
inst✝³ : AddCommMonoid B
inst✝² : HasShift C B
inst✝¹ : HasShift D B
inst✝ : F.CommShift B
X : C
a b : B
⊢ F.map ((shiftFunctorComm 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) ≫
        (shiftFunctorComm D a b).hom.app (F.obj X) ≫
          (shiftFunctor D a).map ((commShiftIso F b).inv.app X) ≫ (commShiftIso F a).inv.app ((shiftFunctor C b).obj X)

Tactic:
by
  have eq := NatTrans.congr_app (congr_arg Iso.hom (F.commShiftIso_add a b)) X
  simp only [comp_obj, CommShift.isoAdd_hom_app,
    ← cancel_epi (F.map ((shiftFunctorAdd C a b).inv.app X)),
    ← F.map_comp_assoc, Iso.inv_hom_id_app, F.map_id, Category.id_comp] at eq
  simp only [shiftFunctorComm_eq D a b _ rfl]
  dsimp
  simp only [shiftFunctorAdd'_eq_shiftFunctorAdd, Category.assoc,
    ← reassoc_of% eq, shiftFunctorComm_eq C a b _ rfl]
  dsimp
  rw [Functor.map_comp]
  simp only [NatTrans.congr_app (congr_arg Iso.hom (F.commShiftIso_add' (add_comm b a))) X,
    CommShift.isoAdd'_hom_app, Category.assoc, Iso.inv_hom_id_app_assoc,
    ← Functor.map_comp_assoc, Iso.hom_inv_id_app,
    Functor.map_id, Category.id_comp, comp_obj, Category.comp_id]

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₁
T' : Triangle C
φ : (j : J) → T' ⟶ T j
⊢ T'.mor₃ ≫ (shiftFunctor C 1).map (Pi.lift fun j ↦ (φ j).hom₁) =
    (Pi.lift fun j ↦ (φ j).hom₃) ≫ (productTriangle T).mor₃

Tactic:
dsimp
    rw [← cancel_mono (piComparison _ _), assoc, assoc, assoc, IsIso.inv_hom_id, comp_id]
    cat_disch

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 : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₂ : IsZero T.obj₂
h₁ : 𝟙 T.obj₁ = 0
⊢ (CategoryTheory.shiftFunctor C 1).map 0 = 0

Tactic:
Functor.map_zero

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
h₂ : IsZero T.obj₂
h₁ : 𝟙 T.obj₁ = 0
⊢ 0 = 0
Module: Mathlib.CategoryTheory.Triangulated.Triangulated

Goal state before:
pp: 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
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
h : Octahedron' comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk v₁₃ u₁₃ w₁₃).mor₁ ≫ u₁₂ = h.m₃ ≫ (Triangle.mk v₂₃ u₂₃ w₂₃).mor₁

Tactic:
dsimp
    rw [h.comm₄]

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

Goal state before:
pp: V : Type u₁
inst✝ : Quiver V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : (of V).obj v ⟶ (of V).obj w), P q → P ((of V).map p ≫ q)
⊢ ∀ {a b : Paths V} (f : a ⟶ b), P f

Tactic:
intro a b

Goal state after:
V : Type u₁
inst✝ : Quiver V
P : {a b : Paths V} → (a ⟶ b) → Prop
id : ∀ {v : V}, P (𝟙 ((of V).obj v))
comp : ∀ {u v w : V} (p : u ⟶ v) (q : (of V).obj v ⟶ (of V).obj w), P q → P ((of V).map p ≫ q)
a b : Paths V
⊢ ∀ (f : a ⟶ b), P f
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
V : Type u₁
inst✝ : Quiver V
F G : Paths V ⥤ C
α_app : (v : V) → F.obj v ⟶ G.obj v
α_nat : ∀ {X Y : V} (f : X ⟶ Y), F.map f.toPath ≫ α_app Y = α_app X ≫ G.map f.toPath
⊢ ∀ ⦃X Y : Paths V⦄ (f : X ⟶ Y), F.map f ≫ α_app Y = α_app X ≫ G.map f

Tactic:
by
    apply MorphismProperty.of_eq_top
      (P := MorphismProperty.naturalityProperty (F₁ := F) α_app)
    exact morphismProperty_eq_top_of_isMultiplicative _ _ α_nat

Goal state after:
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case refine_1.cons
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
b✝ c✝ : C
q' : Path Y b✝
f : b✝ ⟶ c✝
h' : W.paths (p.comp q') → W.paths p
h : W.paths (p.comp (q'.cons f))
⊢ W.paths p

Tactic:
Path.comp_cons

Goal state after:
case refine_1.cons
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
b✝ c✝ : C
q' : Path Y b✝
f : b✝ ⟶ c✝
h' : W.paths (p.comp q') → W.paths p
h : W.paths ((p.comp q').cons f)
⊢ W.paths p
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: case refine_2.cons
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
b✝ c✝ : C
q' : Path Y b✝
f : b✝ ⟶ c✝
h' : W.paths (p.comp q') → W.paths q'
h : W.paths (p.comp (q'.cons f))
⊢ W.paths (q'.cons f)

Tactic:
Path.comp_cons

Goal state after:
case refine_2.cons
C : Type u_1
inst✝ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y Z : C
p : Path X Y
b✝ c✝ : C
q' : Path Y b✝
f : b✝ ⟶ c✝
h' : W.paths (p.comp q') → W.paths q'
h : W.paths ((p.comp q').cons f)
⊢ W.paths (q'.cons f)
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: case inr
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
X Y : LocQuiver W
g : Y.obj ⟶ X.obj
hg : W g
this : IsIso (G.map g)
⊢ G.obj X.obj ⟶ G.obj Y.obj

Tactic:
exact inv (G.map g)

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
G : C ⥤ D
hG : W.IsInvertedBy G
⊢ ∀ (x y : Paths (LocQuiver W)) (f₁ f₂ : x ⟶ y),
    relations W f₁ f₂ → (liftToPathCategory G hG).map f₁ = (liftToPathCategory G hG).map f₂

Tactic:
by
      rintro ⟨X⟩ ⟨Y⟩ f₁ f₂ r
      rcases r with ⟨⟩ <;> all_goals aesop

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
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ LeftFractionRel z₁ z₃

Tactic:
refine ⟨Z₇, t₁ ≫ v₄ ≫ w, u₃ ≫ v₅ ≫ w, ?_, ?_, ?_⟩

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ z₁.s ≫ t₁ ≫ v₄ ≫ w = z₃.s ≫ u₃ ≫ v₅ ≫ w

case refine_2
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ z₁.f ≫ t₁ ≫ v₄ ≫ w = z₃.f ≫ u₃ ≫ v₅ ≫ w

case refine_3
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ z₃ : W.LeftFraction X Y
inst✝ : W.HasLeftCalculusOfFractions
Z₄ : C
t₁ : z₁.Y' ⟶ Z₄
t₂ : z₂.Y' ⟶ Z₄
hst : z₁.s ≫ t₁ = z₂.s ≫ t₂
hft : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
Z₅ : C
u₂ : z₂.Y' ⟶ Z₅
u₃ : z₃.Y' ⟶ Z₅
hsu : z₂.s ≫ u₂ = z₃.s ≫ u₃
hfu : z₂.f ≫ u₂ = z₃.f ≫ u₃
hu : W (z₂.s ≫ u₂)
Y'✝ : C
v₄ : Z₄ ⟶ Y'✝
v₅ : Z₅ ⟶ Y'✝
hv₅ : W v₅
fac : z₃.s ≫ u₃ ≫ v₅ = z₁.s ≫ t₁ ≫ v₄
eq : z₂.s ≫ u₂ ≫ v₅ = z₂.s ≫ t₂ ≫ v₄
Z₇ : C
w : Y'✝ ⟶ Z₇
hw : W w
fac' : u₂ ≫ v₅ ≫ w = t₂ ≫ v₄ ≫ w
⊢ W (z₁.s ≫ t₁ ≫ v₄ ≫ 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 : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ add' W f (L.map 0) = f

Tactic:
add'_eq W f (L.map 0) (LeftFraction₂.mk α.f 0 α.s α.hs) 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 : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ { Y' := α.Y', f := α.f, f' := 0, s := α.s, hs := ⋯ }.add.map L ⋯ = f

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 : L.obj X ⟶ L.obj Y
α : W.LeftFraction X Y
hα : f = α.map L ⋯
⊢ L.map 0 = { Y' := α.Y', f := α.f, f' := 0, s := α.s, hs := ⋯ }.snd.map L ⋯