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

Goal state before:
pp: ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ c.Rel i (Exists.choose ?hc)

pp: case hc
ι : Type u_1
c : ComplexShape ι
i j : ι
h : c.Rel i j
⊢ ∃ j, c.Rel i j

Tactic:
exact Exists.choose_spec ⟨j, h⟩

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
s : M.sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ 1 ((ModuleCat.Hom.hom ((unit R).map f)) 1) • ↑s Y = (ModuleCat.Hom.hom (M.map f)) (1 • ↑s X)

Tactic:
change R.map f 1 • s.eval Y = M.map f (1 • s.eval X)

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M✝ M₁ M₂ : PresheafOfModules R
M : PresheafOfModules R
s : M.sections
X Y : Cᵒᵖ
f : X ⟶ Y
⊢ (ConcreteCategory.hom (R.map f)) 1 • s.eval Y = (ConcreteCategory.hom (M.map f)) (1 • s.eval X)
Module: Mathlib.CategoryTheory.Monoidal.End

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) =
    (μ F m₂ m₃).app ((F.obj m₁).obj X) ≫
      (μ F m₁ (m₂ ⊗ m₃)).app X ≫ (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (δ F (m₁ ⊗ m₂) m₃).app X

Tactic:
rw [← associativity_app_assoc]

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{v_1, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m₁ m₂ m₃ : M
X : C
inst✝ : F.Monoidal
⊢ (F.obj m₃).map ((μ F m₁ m₂).app X) =
    (F.obj m₃).map ((μ F m₁ m₂).app X) ≫
      (μ F (m₁ ⊗ m₂) m₃).app X ≫
        (F.map (α_ m₁ m₂ m₃).hom).app X ≫ (F.map (α_ m₁ m₂ m₃).inv).app X ≫ (δ F (m₁ ⊗ m₂) m₃).app X
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
n : ℕ
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3) =
    (succ
        { X₁ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 2), X₂ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 1),
          X₃ := (mk X₀ X₁ X₂ d₀ d₁ s succ).X n, f := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 2) (n + 1),
          g := (mk X₀ X₁ X₂ d₀ d₁ s succ).d (n + 1) n, zero := ⋯ }).fst

Tactic:
← mk_congr_succ_X₃ succ
      (mkAux_eq_shortComplex_mk_d_comp_d X₀ X₁ X₂ d₀ d₁ s succ n)

Goal state after:
ι : 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
n : ℕ
⊢ (mk X₀ X₁ X₂ d₀ d₁ s succ).X (n + 3) = (succ (mkAux X₀ X₁ X₂ d₀ d₁ s succ n)).fst
Module: Mathlib.Algebra.Homology.HomologicalComplexLimits

Goal state before:
pp: case neg
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
inst✝¹ : HasZeroObject C
inst✝ : DecidableEq ι
i j : ι
h : ¬j = i
⊢ PreservesColimitsOfShape J (single C c i ⋙ eval C c j)

Tactic:
exact Functor.preservesColimitsOfShape_of_isZero _ (isZero_single_comp_eval C c _ _ h) _

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 : R
y : S
⊢ single ((algebraMap R S) x) y ∈ kerTotal R S

Tactic:
← Finsupp.smul_single_one _ y

Goal state after:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
y : S
⊢ y • single ((algebraMap R S) x) 1 ∈ kerTotal R S
Module: Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
K : CochainComplex C ℕ
X : C
φ : X ⟶ K.X 0
inst✝ : HomologicalComplex.HasHomology K 0
hφ✝ : φ ≫ K.d 0 1 = 0
hφ : φ ≫ K.d 0 ((ComplexShape.up ℕ).next 0) = 0
α : { X₁ := X, X₂ := X, X₃ := X, f := 0, g := 0, zero := ⋯ } ⟶ HomologicalComplex.sc K 0 :=
  { τ₁ := 0, τ₂ := φ, τ₃ := 0, comm₁₂ := ⋯, comm₂₃ := ⋯ }
⊢ IsIso (HomologicalComplex.liftCycles K φ ((ComplexShape.up ℕ).next 0) ⋯ hφ) ↔
    { X₁ := X, X₂ := K.X 0, X₃ := K.X ((ComplexShape.up ℕ).next 0), f := φ, g := K.d 0 ((ComplexShape.up ℕ).next 0),
          zero := hφ }.Exact ∧
      Mono φ

Tactic:
exact (ShortComplex.quasiIso_iff_isIso_liftCycles α rfl rfl (by simp)).symm.trans
    (ShortComplex.quasiIso_iff_of_zeros α rfl rfl (by simp))

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
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
⊢ inrX φ i ≫ d φ i j = G.d i j ≫ inrX φ j

Tactic:
by_cases hij : c.Rel i j
  · by_cases hj : c.Rel j (c.next j)
    · apply ext_to_X _ _ _ hj
      · simp [d_fstX φ _ _ _ hij]
      · simp [d_sndX φ _ _ hij]
    · apply ext_to_X' _ _ hj
      simp [d_sndX φ _ _ hij]
  · rw [shape φ _ _ hij, G.shape _ _ hij, zero_comp, comp_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 : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq : φ₁.f p = F.d p (p + 1) ≫ (↑z).v (p + 1) p ⋯ + (↑z).v p (p - 1) ⋯ ≫ G.d (p - 1) p + φ₂.f p
⊢ F.d p (p + 1) ≫ (↑z).v (p + 1) p ⋯ + (↑z).v p (p - 1) ⋯ ≫ G.d (p - 1) p + φ₂.f p =
    F.d p (p + 1) ≫ (↑z).v (p + 1) p ?hc + (if hij : p + -1 = p - 1 then (↑z).v p (p - 1) hij else 0) ≫ G.d (p - 1) p +
      φ₂.f p

pp: case hc
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 : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq : φ₁.f p = F.d p (p + 1) ≫ (↑z).v (p + 1) p ⋯ + (↑z).v p (p - 1) ⋯ ≫ G.d (p - 1) p + φ₂.f p
⊢ p + 1 + -1 = p

Tactic:
dif_pos

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 : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq : φ₁.f p = F.d p (p + 1) ≫ (↑z).v (p + 1) p ⋯ + (↑z).v p (p - 1) ⋯ ≫ G.d (p - 1) p + φ₂.f p
⊢ F.d p (p + 1) ≫ (↑z).v (p + 1) p ⋯ + (↑z).v p (p - 1) ⋯ ≫ G.d (p - 1) p + φ₂.f p =
    F.d p (p + 1) ≫ (↑z).v (p + 1) p ?hc✝ + (↑z).v p (p - 1) ?hc ≫ G.d (p - 1) p + φ₂.f p

case hc
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 : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq : φ₁.f p = F.d p (p + 1) ≫ (↑z).v (p + 1) p ⋯ + (↑z).v p (p - 1) ⋯ ≫ G.d (p - 1) p + φ₂.f p
⊢ p + -1 = p - 1

case hc
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 : ℤ
h₁ : (ComplexShape.up ℤ).Rel (p - 1) p
h₂ : (ComplexShape.up ℤ).Rel p (p + 1)
eq : φ₁.f p = F.d p (p + 1) ≫ (↑z).v (p + 1) p ⋯ + (↑z).v p (p - 1) ⋯ ≫ G.d (p - 1) p + φ₂.f p
⊢ p + 1 + -1 = 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 : ℤ
φ₁ φ₂ : F ⟶ G
ho : Homotopy φ₁ φ₂
⊢ (fun z ↦ { hom := fun i j ↦ if hij : i + -1 = j then (↑z).v i j hij else 0, zero := ⋯, comm := ⋯ })
      ((fun ho ↦ ⟨ofHomotopy ho, ⋯⟩) ho) =
    ho

Tactic:
by
    ext i j
    dsimp
    split_ifs with h
    · rfl
    · rw [ho.zero i j (fun h' => h (by dsimp at h'; lia))]

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

Goal state before:
pp: case e_a
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ (lift r F hF).map ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X)) ≫
      (lift r F hF).map ((Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X)) ≫
        F.map ((shiftFunctorAdd C a b).inv.app X) ≫
          F.map ((shiftFunctorAdd C a b).hom.app X) ≫
            (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
              (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫
                (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
      (shiftFunctor D b).map
          ((lift r F hF).map ((Functor.commShiftIso (functor r) a).inv.app X) ≫ (Functor.commShiftIso F a).hom.app X) ≫
        (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))

Tactic:
← cancel_epi ((shiftFunctor (Quotient r) b ⋙ lift r F hF).map
      (NatTrans.app (Functor.commShiftIso (functor r) a).hom X))

Goal state after:
case e_a
C : Type u
inst✝⁶ : Category.{v, u} C
D : Type u'
inst✝⁵ : Category.{v', u'} D
F : C ⥤ D
r : HomRel C
A : Type w
inst✝⁴ : AddMonoid A
inst✝³ : HasShift C A
inst✝² : HasShift D A
inst✝¹ : r.IsCompatibleWithShift A
inst✝ : F.CommShift A
hF : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : A
X : C
⊢ (shiftFunctor (Quotient r) b ⋙ lift r F hF).map ((Functor.commShiftIso (functor r) a).hom.app X) ≫
      (lift r F hF).map ((shiftFunctor (Quotient r) b).map ((Functor.commShiftIso (functor r) a).inv.app X)) ≫
        (lift r F hF).map ((Functor.commShiftIso (functor r) b).inv.app ((shiftFunctor C a).obj X)) ≫
          F.map ((shiftFunctorAdd C a b).inv.app X) ≫
            F.map ((shiftFunctorAdd C a b).hom.app X) ≫
              (Functor.commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
                (shiftFunctor D b).map ((Functor.commShiftIso F a).hom.app X) ≫
                  (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (shiftFunctor (Quotient r) b ⋙ lift r F hF).map ((Functor.commShiftIso (functor r) a).hom.app X) ≫
      (LiftCommShift.iso F r hF b).hom.app ((shiftFunctor (Quotient r) a).obj ((functor r).obj X)) ≫
        (shiftFunctor D b).map
            ((lift r F hF).map ((Functor.commShiftIso (functor r) a).inv.app X) ≫
              (Functor.commShiftIso F a).hom.app X) ≫
          (shiftFunctorAdd D a b).inv.app ((lift r F hF).obj ((functor r).obj X))
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 n' : ℤ
hn' : n + a = n'
⊢ leftUnshift 0 n hn' = 0

Tactic:
change (leftShiftAddEquiv K L n a n' hn').symm 0 = 0

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n + a = n'
⊢ (leftShiftAddEquiv K L n a n' hn').symm 0 = 0
Module: Mathlib.CategoryTheory.Triangulated.Basic

Goal state before:
pp: case h₁
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasShift C ℤ
T₁ T₂ T₃ : Triangle C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
A B : J ⥤ Triangle C
hom₁ : A ⋙ π₁ ⟶ B ⋙ π₁
hom₂ : A ⋙ π₂ ⟶ B ⋙ π₂
hom₃ : A ⋙ π₃ ⟶ B ⋙ π₃
comm₁ : A.whiskerLeft π₁Toπ₂ ≫ hom₂ = hom₁ ≫ B.whiskerLeft π₁Toπ₂
comm₂ : A.whiskerLeft π₂Toπ₃ ≫ hom₃ = hom₂ ≫ B.whiskerLeft π₂Toπ₃
comm₃ : A.whiskerLeft π₃Toπ₁ ≫ whiskerRight hom₁ (shiftFunctor C 1) = hom₃ ≫ B.whiskerLeft π₃Toπ₁
x✝¹ x✝ : J
φ : x✝¹ ⟶ x✝
⊢ (A.map φ ≫
        { hom₁ := hom₁.app x✝, hom₂ := hom₂.app x✝, hom₃ := hom₃.app x✝, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ }).hom₁ =
    ({ hom₁ := hom₁.app x✝¹, hom₂ := hom₂.app x✝¹, hom₃ := hom₃.app x✝¹, comm₁ := ⋯, comm₂ := ⋯, comm₃ := ⋯ } ≫
        B.map φ).hom₁

Tactic:
exact hom₁.naturality φ

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
X : C
f : T.obj₂ ⟶ X
hf : T.mor₁ ≫ f = 0
g : T.obj₃ ⟶ (mk 0 (𝟙 X) 0).obj₃
hg₁ : T.mor₂ ≫ g = f ≫ (mk 0 (𝟙 X) 0).mor₂
right✝ : T.mor₃ ≫ (CategoryTheory.shiftFunctor C 1).map 0 = g ≫ (mk 0 (𝟙 X) 0).mor₃
⊢ f = T.mor₂ ≫ g

Tactic:
simpa using hg₁.symm

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
X : C
f : X ⟶ T.obj₂
hf : f ≫ T.mor₂ = 0
⊢ ∃ g, f = g ≫ T.mor₁

Tactic:
obtain ⟨a, ⟨ha₁, _⟩⟩ := complete_distinguished_triangle_morphism₁ _ T
    (contractible_distinguished X) hT f 0 (by cat_disch)
  exact ⟨a, by simpa using ha₁⟩

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

Goal state before:
pp: case mp
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 : T.mor₁ = 0
X : C
g : X ⟶ T.obj₂
hg : g ≫ T.mor₂ = 0
⊢ g = 0

Tactic:
obtain ⟨f, rfl⟩ := coyoneda_exact₂ T hT g hg

Goal state after:
case mp
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 : T.mor₁ = 0
X : C
f : X ⟶ T.obj₁
hg : (f ≫ T.mor₁) ≫ T.mor₂ = 0
⊢ f ≫ T.mor₁ = 0
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.Faithful
X Y : Triangle C
f g : X ⟶ Y
h : F.mapTriangle.map f = F.mapTriangle.map g
⊢ f = g

Tactic:
ext <;> apply F.map_injective
    · exact congr_arg TriangleMorphism.hom₁ h
    · exact congr_arg TriangleMorphism.hom₂ h
    · exact congr_arg TriangleMorphism.hom₃ h

Goal state after:
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 ℤ
F : C ⥤ D
inst✝¹⁰ : F.CommShift ℤ
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
inst✝¹ : F.IsTriangulated
inst✝ : F.mapArrow.EssSurj
T : Triangle D
hT : T ∈ distinguishedTriangles
⊢ ∃ T', ∃ (_ : T' ∈ distinguishedTriangles), Nonempty (F.mapTriangle.obj T' ≅ T)

Tactic:
obtain ⟨X, Y, f, e₁, e₂, w⟩ : ∃ (X Y : C) (f : X ⟶ Y) (e₁ : F.obj X ≅ T.obj₁)
    (e₂ : F.obj Y ≅ T.obj₂), F.map f ≫ e₂.hom = e₁.hom ≫ T.mor₁ := by
      let e := F.mapArrow.objObjPreimageIso (Arrow.mk T.mor₁)
      exact ⟨_, _, _, Arrow.leftFunc.mapIso e, Arrow.rightFunc.mapIso e, e.hom.w.symm⟩
  obtain ⟨W, g, h, H⟩ := distinguished_cocone_triangle f
  exact ⟨_, H, ⟨isoTriangleOfIso₁₂ _ _ (F.map_distinguished _ H) hT e₁ e₂ w⟩⟩

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

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

Tactic:
intro a f

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

Goal state before:
pp: V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ e.hom.map (e.inv.map f) = Quiver.homOfEq f ⋯ ⋯

Tactic:
← Prefunctor.comp_map

Goal state after:
V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ (e.inv ⋙q e.hom).map f = Quiver.homOfEq f ⋯ ⋯
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₂
this : MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤
X Y : W.Localization
f : X ⟶ Y
⊢ F₁.map f ≫ NatTransExtension.app τ Y = NatTransExtension.app τ X ≫ F₂.map f

Tactic:
simpa only [← this] using! MorphismProperty.top_apply f

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_4
inst✝¹ : Category.{v_4, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ W.IsInvertedBy L'

Tactic:
rw [← MorphismProperty.IsInvertedBy.iff_of_iso W e]

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
E : Type u_4
inst✝¹ : Category.{v_4, u_4} E
L' : C ⥤ E
eq : D ≌ E
inst✝ : L.IsLocalization W
e : L ⋙ eq.functor ≅ L'
⊢ W.IsInvertedBy (L ⋙ eq.functor)
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
w✝¹ w✝ : C₂
f' : w✝¹ ⟶ w✝
hf' : W₂ f'
e : Arrow.mk f' ≅ Arrow.mk (E.functor.map f)
⊢ IsIso ((E.functor ⋙ W₂.Q).map f)

Tactic:
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

Goal state before:
pp: case refine_1
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' ⟶ U
t₂ : b₂.Y' ⟶ U
hst : b₁.s ≫ t₁ = b₂.s ≫ t₂
hft : b₁.f ≫ t₁ = b₂.f ≫ t₂
ht : W (b₁.s ≫ t₁)
z₁ : W.LeftFraction a.Y' b₁.Y'
fac₁ : { X' := Y, s := a.s, hs := ⋯, f := b₁.f }.f ≫ z₁.s = { X' := Y, s := a.s, hs := ⋯, f := b₁.f }.s ≫ z₁.f
z₂ : W.LeftFraction a.Y' b₂.Y'
fac₂ : { X' := Y, s := a.s, hs := ⋯, f := b₂.f }.f ≫ z₂.s = { X' := Y, s := a.s, hs := ⋯, f := b₂.f }.s ≫ z₂.f
w₁ : W.LeftFraction z₁.Y' U
fac₁' : { X' := b₁.Y', s := z₁.s, hs := ⋯, f := t₁ }.f ≫ w₁.s = { X' := b₁.Y', s := z₁.s, hs := ⋯, f := t₁ }.s ≫ w₁.f
⊢ a.comp b₁ = a.comp b₂

Tactic:
obtain ⟨w₂, fac₂'⟩ := exists_leftFraction (RightFraction.mk z₂.s z₂.hs t₂)

Goal state after:
case refine_1
C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a : W.LeftFraction X Y
b₁ b₂ : W.LeftFraction Y Z
U : C
t₁ : b₁.Y' ⟶ U
t₂ : b₂.Y' ⟶ U
hst : b₁.s ≫ t₁ = b₂.s ≫ t₂
hft : b₁.f ≫ t₁ = b₂.f ≫ t₂
ht : W (b₁.s ≫ t₁)
z₁ : W.LeftFraction a.Y' b₁.Y'
fac₁ : { X' := Y, s := a.s, hs := ⋯, f := b₁.f }.f ≫ z₁.s = { X' := Y, s := a.s, hs := ⋯, f := b₁.f }.s ≫ z₁.f
z₂ : W.LeftFraction a.Y' b₂.Y'
fac₂ : { X' := Y, s := a.s, hs := ⋯, f := b₂.f }.f ≫ z₂.s = { X' := Y, s := a.s, hs := ⋯, f := b₂.f }.s ≫ z₂.f
w₁ : W.LeftFraction z₁.Y' U
fac₁' : { X' := b₁.Y', s := z₁.s, hs := ⋯, f := t₁ }.f ≫ w₁.s = { X' := b₁.Y', s := z₁.s, hs := ⋯, f := t₁ }.s ≫ w₁.f
w₂ : W.LeftFraction z₂.Y' U
fac₂' : { X' := b₂.Y', s := z₂.s, hs := ⋯, f := t₂ }.f ≫ w₂.s = { X' := b₂.Y', s := z₂.s, hs := ⋯, f := t₂ }.s ≫ w₂.f
⊢ a.comp b₁ = a.comp b₂
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case refine_2.refine_1
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 Z : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
eq : a₁.s ≫ z₁.f ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
⊢ LeftFractionRel (a₁.comp₀ b z₁) p₁

Tactic:
obtain ⟨Z, u, hu, fac₃⟩ := HasLeftCalculusOfFractions.ext _ _ _ a₁.hs eq

Goal state after:
case refine_2.refine_1
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 Z✝ : C
z₁✝ : Hom W X Y
z₂✝ : Hom W Y Z✝
a₁ a₂ : W.LeftFraction X Y
b : W.LeftFraction Y Z✝
U : C
t₁ : a₁.Y' ⟶ U
t₂ : a₂.Y' ⟶ U
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
ht : W (a₁.s ≫ t₁)
z₁ : W.LeftFraction a₁.Y' b.Y'
fac₁ : b.f ≫ z₁.s = a₁.s ≫ z₁.f
z₂ : W.LeftFraction a₂.Y' b.Y'
fac₂ : b.f ≫ z₂.s = a₂.s ≫ z₂.f
w₁ : W.LeftFraction U z₁.Y'
w₂ : W.LeftFraction U z₂.Y'
p₁ : W.LeftFraction X Z✝ := { Y' := w₁.Y', f := a₁.f ≫ t₁ ≫ w₁.f, s := b.s ≫ z₁.s ≫ w₁.s, hs := ⋯ }
p₂ : W.LeftFraction X Z✝ := { Y' := w₂.Y', f := a₂.f ≫ t₂ ≫ w₂.f, s := b.s ≫ z₂.s ≫ w₂.s, hs := ⋯ }
fac₁' : b.f ≫ z₁.s ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
fac₂' : b.f ≫ z₂.s ≫ w₂.s = a₂.s ≫ t₂ ≫ w₂.f
eq : a₁.s ≫ z₁.f ≫ w₁.s = a₁.s ≫ t₁ ≫ w₁.f
Z : C
u : w₁.Y' ⟶ Z
hu : W u
fac₃ : (z₁.f ≫ w₁.s) ≫ u = (t₁ ≫ w₁.f) ≫ u
⊢ LeftFractionRel (a₁.comp₀ b z₁) p₁