mathlib-initiative/mathlib-tactics huggingface dataset:
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
z : W.LeftFraction X Y
⊢ Hom.mk ((ofHom W (𝟙 X)).comp₀ z (ofHom W z.f)) = Hom.mk z

Tactic:
]

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
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
z : W.LeftFraction X Y
⊢ Hom.mk ((ofHom W (𝟙 X)).comp₀ z (ofHom W z.f)) = Hom.mk z
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
H : ∀ (J : Type w) [Finite J], P.IsClosedUnderColimitsOfShape (Discrete J)
J : Type
x✝ : Finite J
⊢ P.IsClosedUnderColimitsOfShape (Discrete (Shrink.{w, 0} J))

Tactic:
]

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
P : ObjectProperty C
H : ∀ (J : Type w) [Finite J], P.IsClosedUnderColimitsOfShape (Discrete J)
J : Type
x✝ : Finite J
⊢ P.IsClosedUnderColimitsOfShape (Discrete (Shrink.{w, 0} J))
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
z : W.LeftFraction X Y
⊢ Hom.mk (z.comp₀ (ofHom W (𝟙 Y)) (ofInv z.s ⋯)) = Hom.mk z

Tactic:
]

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
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
z : W.LeftFraction X Y
⊢ Hom.mk (z.comp₀ (ofHom W (𝟙 Y)) (ofInv z.s ⋯)) = Hom.mk z
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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
⊢ (z₁.comp z₂).comp (Hom.mk z₃) = (Hom.mk z₁).comp (z₂.comp z₃)

Tactic:
]

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
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
⊢ (z₁.comp z₂).comp (Hom.mk z₃) = (Hom.mk z₁).comp (z₂.comp z₃)
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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ z₂.s ≫ z₁₂.s ≫ z'.f = z₂.s ≫ z₁₂.s ≫ z'.f

Tactic:
]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ z₂.f ≫ z₁₂.s ≫ z'.f = z₂.f ≫ z₁₂.s ≫ z'.f

Tactic:
]

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

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_2, u_2} D
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ Hom.mk
      ({ Y' := z₁₂.Y', f := z₁.f ≫ z₁₂.f, s := z₂.s ≫ z₁₂.s, hs := ⋯ }.comp₀ z₃
        { Y' := z'.Y', f := z'.f, s := z₂₃.s ≫ z'.s, hs := ⋯ }) =
    z₁.comp { Y' := z₂₃.Y', f := z₂.f ≫ z₂₃.f, s := z₃.s ≫ z₂₃.s, hs := ⋯ }

Tactic:
comp_eq z₁ _ (mk (z₁₂.f ≫ z'.f) z'.s z'.hs)
        (by dsimp; rw [assoc, ← reassoc_of% fac₁₂, fac])

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
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ Hom.mk
      ({ Y' := z₁₂.Y', f := z₁.f ≫ z₁₂.f, s := z₂.s ≫ z₁₂.s, hs := ⋯ }.comp₀ z₃
        { Y' := z'.Y', f := z'.f, s := z₂₃.s ≫ z'.s, hs := ⋯ }) =
    Hom.mk
      (z₁.comp₀ { Y' := z₂₃.Y', f := z₂.f ≫ z₂₃.f, s := z₃.s ≫ z₂₃.s, hs := ⋯ }
        { Y' := z'.Y', f := z₁₂.f ≫ z'.f, s := z'.s, hs := ⋯ })
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₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ Hom.mk
      ({ Y' := z₁₂.Y', f := z₁.f ≫ z₁₂.f, s := z₂.s ≫ z₁₂.s, hs := ⋯ }.comp₀ z₃
        { Y' := z'.Y', f := z'.f, s := z₂₃.s ≫ z'.s, hs := ⋯ }) =
    Hom.mk
      (z₁.comp₀ { Y' := z₂₃.Y', f := z₂.f ≫ z₂₃.f, s := z₃.s ≫ z₂₃.s, hs := ⋯ }
        { Y' := z'.Y', f := z₁₂.f ≫ z'.f, s := z'.s, hs := ⋯ })

Tactic:
]

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
inst✝ : W.HasLeftCalculusOfFractions
X₁ X₂ X₃ X₄ : C
z₁ : W.LeftFraction X₁ X₂
z₂ : W.LeftFraction X₂ X₃
z₃ : W.LeftFraction X₃ X₄
z₁₂ : W.LeftFraction z₁.Y' z₂.Y'
fac₁₂ : z₂.f ≫ z₁₂.s = z₁.s ≫ z₁₂.f
z₂₃ : W.LeftFraction z₂.Y' z₃.Y'
fac₂₃ : z₃.f ≫ z₂₃.s = z₂.s ≫ z₂₃.f
z' : W.LeftFraction z₁₂.Y' z₂₃.Y'
fac : z₂₃.f ≫ z'.s = z₁₂.s ≫ z'.f
⊢ Hom.mk
      ({ Y' := z₁₂.Y', f := z₁.f ≫ z₁₂.f, s := z₂.s ≫ z₁₂.s, hs := ⋯ }.comp₀ z₃
        { Y' := z'.Y', f := z'.f, s := z₂₃.s ≫ z'.s, hs := ⋯ }) =
    Hom.mk
      (z₁.comp₀ { Y' := z₂₃.Y', f := z₂.f ≫ z₂₃.f, s := z₃.s ≫ z₂₃.s, hs := ⋯ }
        { Y' := z'.Y', f := z₁₂.f ≫ z'.f, s := z'.s, hs := ⋯ })
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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.mk (ofHom W (f ≫ g)) = Hom.mk ((ofHom W f).comp₀ (ofHom W g) (ofHom W g))

Tactic:
]

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
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ Hom.mk (ofHom W (f ≫ g)) = Hom.mk ((ofHom W f).comp₀ (ofHom W g) (ofHom W g))
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Z : C
z₁ : W.LeftFraction X Y
z₂ : W.LeftFraction Y Z
z₃ : W.LeftFraction z₁.Y' z₂.Y'
h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f
⊢ Hom.mk (z₁.comp₀ z₂ z₃) = homMk (z₁.comp₀ z₂ z₃)

Tactic:
]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ homMk ((ofHom W f).comp₀ (ofInv s hs) (ofHom W (𝟙 (ofHom W f).Y'))) = homMk { Y' := Y', f := f, s := s, hs := hs }

Tactic:
]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y Y' : C
f : X ⟶ Y'
s : Y ⟶ Y'
hs : W s
⊢ homMk ((ofHom W f).comp₀ (ofInv s hs) (ofHom W (𝟙 (ofHom W f).Y'))) = homMk { Y' := Y', f := f, s := s, hs := hs }
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
⊢ homMk { Y' := Y, f := s, s := s, hs := hs } = 𝟙 ((Q W).obj X)

Tactic:
]

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
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
⊢ homMk { Y' := Y, f := s, s := s, hs := hs } = 𝟙 ((Q W).obj X)
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
⊢ homMk ((ofInv s hs).comp₀ (ofHom W s) (ofHom W (𝟙 Y))) = 𝟙 ((Q W).obj Y)

Tactic:
]

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
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
s : X ⟶ Y
hs : W s
⊢ homMk ((ofInv s hs).comp₀ (ofHom W s) (ofHom W (𝟙 Y))) = 𝟙 ((Q W).obj Y)
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₁ a₂ : W.LeftFraction X Y
Z : C
t₁ : a₁.Y' ⟶ Z
t₂ : a₂.Y' ⟶ Z
hst : a₁.s ≫ t₁ = a₂.s ≫ t₂
hft : a₁.f ≫ t₁ = a₂.f ≫ t₂
h : W (a₁.s ≫ t₁)
this : IsIso (F.map (a₁.s ≫ t₁))
⊢ F.map a₂.f ≫ F.map t₂ = F.map a₂.f ≫ F.map t₂

Tactic:
]

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

Goal state before:
pp: case refine_2
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁶ : HasShift C ℤ
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : HasShift D ℤ
inst✝ : L.CommShift ℤ
H :
  ∀ (T₁' T₂' : Triangle C),
    T₁' ∈ distinguishedTriangles →
      T₂' ∈ distinguishedTriangles →
        ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
          L.map T₁'.mor₁ ≫ b = a ≫ L.map T₂'.mor₁ → ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b
T₁ T₂ : Triangle D
a : T₁.obj₁ ⟶ T₂.obj₁
b : T₁.obj₂ ⟶ T₂.obj₂
fac : T₁.mor₁ ≫ b = a ≫ T₂.mor₁
T₁' : Triangle C
e₁ : T₁ ≅ L.mapTriangle.obj T₁'
hT₁' : T₁' ∈ distinguishedTriangles
T₂' : Triangle C
e₂ : T₂ ≅ L.mapTriangle.obj T₂'
hT₂' : T₂' ∈ distinguishedTriangles
comm₁ : L.map T₁'.mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ L.map T₂'.mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ L.map T₁'.mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ L.map T₂'.mor₂
comm₃' :
  T₂.mor₃ ≫ (shiftFunctor D 1).map e₂.hom.hom₁ = e₂.hom.hom₃ ≫ L.map T₂'.mor₃ ≫ (commShiftIso L 1).hom.app T₂'.obj₁
comm₃ :
  L.map T₁'.mor₃ ≫ (commShiftIso L 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃
φ : L.mapTriangle.obj T₁' ⟶ L.mapTriangle.obj T₂'
hφ₁ : φ.hom₁ = e₁.inv.hom₁ ≫ a ≫ e₂.hom.hom₁
hφ₂ : φ.hom₂ = e₁.inv.hom₂ ≫ b ≫ e₂.hom.hom₂
h₂ : L.map T₁'.mor₂ ≫ φ.hom₃ = φ.hom₂ ≫ L.map T₂'.mor₂
h₃ :
  L.map T₁'.mor₃ ≫ (commShiftIso L 1).hom.app T₁'.obj₁ ≫ (shiftFunctor D 1).map φ.hom₁ =
    φ.hom₃ ≫ L.map T₂'.mor₃ ≫ (commShiftIso L 1).hom.app T₂'.obj₁
⊢ φ.hom₃ ≫ L.map T₂'.mor₃ ≫ (commShiftIso L 1).hom.app T₂'.obj₁ =
    φ.hom₃ ≫ L.map T₂'.mor₃ ≫ (commShiftIso L 1).hom.app T₂'.obj₁

Tactic:
]

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
F : C ⥤ E
hF : W.IsInvertedBy F
X : C
⊢ 𝟙 (F.obj X) = 𝟙 (F.obj X)

Tactic:
]

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
F : C ⥤ E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction f.Y' g.Y'
fac : { X' := Y, s := f.s, hs := ⋯, f := g.f }.f ≫ z.s = { X' := Y, s := f.s, hs := ⋯, f := g.f }.s ≫ z.f
⊢ (f.comp₀ g z).map F hF = f.map F hF ≫ g.map F hF

Tactic:
]

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
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction f.Y' g.Y'
fac : { X' := Y, s := f.s, hs := ⋯, f := g.f }.f ≫ z.s = { X' := Y, s := f.s, hs := ⋯, f := g.f }.s ≫ z.f
⊢ (f.comp₀ g z).map F hF = f.map F hF ≫ g.map F hF
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
F : C ⥤ E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction f.Y' g.Y'
fac : g.f ≫ z.s = f.s ≫ z.f
this✝ : IsIso (F.map g.s)
this : IsIso (F.map z.s)
⊢ F.map { Y' := z.Y', f := f.f ≫ z.f, s := g.s ≫ z.s, hs := ⋯ }.f = f.map F hF ≫ F.map (f.s ≫ z.f)

Tactic:
]

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
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction f.Y' g.Y'
fac : g.f ≫ z.s = f.s ≫ z.f
this✝ : IsIso (F.map g.s)
this : IsIso (F.map z.s)
⊢ F.map { Y' := z.Y', f := f.f ≫ z.f, s := g.s ≫ z.s, hs := ⋯ }.f = f.map F hF ≫ F.map (f.s ≫ z.f)
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
F : C ⥤ E
hF : W.IsInvertedBy F
X Y Z : C
f : W.LeftFraction X Y
g : W.LeftFraction Y Z
z : W.LeftFraction f.Y' g.Y'
fac : g.f ≫ z.s = f.s ≫ z.f
this✝ : IsIso (F.map g.s)
this : IsIso (F.map z.s)
⊢ F.map f.f ≫ F.map z.f = F.map f.f ≫ F.map z.f

Tactic:
]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F : C ⥤ E
hF : W.IsInvertedBy F
X Y : C
f : X ⟶ Y
⊢ F.map f = F.map f

Tactic:
]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ F₁.map ((Q W).map f.f) ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯ ≫ F₂.map ((Q W).map f.f) ≫ F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ F₁.map ((Q W).map f.f) ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯ ≫ F₂.map ((Q W).map f.f) ≫ F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ (eqToHom ⋯ ≫ (Q W ⋙ F₂).map f.f ≫ eqToHom ⋯) ≫ F₁.map (Qinv f.s ⋯) =
    eqToHom ⋯ ≫ F₂.map ((Q W).map f.f) ≫ F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ (eqToHom ⋯ ≫ (Q W ⋙ F₂).map f.f ≫ eqToHom ⋯) ≫ F₁.map (Qinv f.s ⋯) =
    eqToHom ⋯ ≫ F₂.map ((Q W).map f.f) ≫ F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ eqToHom ⋯ ≫ (Q W ⋙ F₂).map f.f ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) =
    eqToHom ⋯ ≫ F₂.map ((Q W).map f.f) ≫ F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯

Tactic:
]

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
⊢ eqToHom ⋯ ≫ (Q W ⋙ F₂).map f.f ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) =
    eqToHom ⋯ ≫ F₂.map ((Q W).map f.f) ≫ F₂.map (Qinv f.s ⋯) ≫ eqToHom ⋯
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ F₂.map ((Q W).map f.s) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯

Tactic:
]

Goal state after:
case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ F₂.map ((Q W).map f.s) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ (eqToHom ⋯ ≫ (Q W ⋙ F₁).map f.s ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯

Tactic:
]

Goal state after:
case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ (eqToHom ⋯ ≫ (Q W ⋙ F₁).map f.s ≫ eqToHom ⋯) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ eqToHom ⋯ ≫ F₁.map (𝟙 ((Q W).obj Y)) = eqToHom ⋯

Tactic:
]

Goal state after:
case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ eqToHom ⋯ ≫ F₁.map (𝟙 ((Q W).obj Y)) = eqToHom ⋯
Module: Mathlib.CategoryTheory.Localization.Triangulated

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : Category.{v_2, u_2} D
L : C ⥤ D
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
fac : L.map (T₁.mor₁ ≫ γ.f) = α.map L ⋯ ≫ L.map T₂.mor₁ ≫ L.map β.s ≫ L.map γ.s
hγ : b ≫ L.map β.s = γ.map L ⋯
⊢ L.map (α.f ≫ β.f ≫ γ.s) = L.map (T₁.mor₁ ≫ γ.f)

Tactic:
]

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
inst✝⁹ : HasShift C ℤ
inst✝⁸ : Preadditive C
inst✝⁷ : HasZeroObject C
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : Pretriangulated C
inst✝⁴ : HasShift D ℤ
inst✝³ : L.CommShift ℤ
W : MorphismProperty C
inst✝² : L.IsLocalization W
inst✝¹ : W.HasLeftCalculusOfFractions
inst✝ : W.IsCompatibleWithTriangulation
T₁ T₂ : Triangle C
hT₁ : T₁ ∈ distinguishedTriangles
hT₂ : T₂ ∈ distinguishedTriangles
a : L.obj T₁.obj₁ ⟶ L.obj T₂.obj₁
b : L.obj T₁.obj₂ ⟶ L.obj T₂.obj₂
α : W.LeftFraction T₁.obj₁ T₂.obj₁
hα : a = α.map L ⋯
β : W.LeftFraction α.Y' T₂.obj₂
hβ : T₂.mor₁ ≫ β.s = α.s ≫ β.f
γ : W.LeftFraction T₁.obj₂ β.Y'
fac : L.map (T₁.mor₁ ≫ γ.f) = α.map L ⋯ ≫ L.map T₂.mor₁ ≫ L.map β.s ≫ L.map γ.s
hγ : b ≫ L.map β.s = γ.map L ⋯
⊢ L.map (α.f ≫ β.f ≫ γ.s) = L.map (T₁.mor₁ ≫ γ.f)
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

Goal state before:
pp: case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝¹ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝ : Category.{v_3, u_3} E
F₁ F₂ : Localization W ⥤ E
h : Q W ⋙ F₁ = Q W ⋙ F₂
X Y : C
f : W.LeftFraction X Y
this : IsIso ((Q W).map f.s)
⊢ eqToHom ⋯ = eqToHom ⋯

Tactic:
]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f : W.LeftFraction X Y
⊢ (Q W).map f.f = (Q W).map f.f

Tactic:
]

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯
⊢ f.map (Q W) ⋯ = g.map (Q W) ⋯

Tactic:
]

Goal state after:
case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f g : W.LeftFraction X Y
h : (Hom.mk f).map (Q W) ⋯ = (Hom.mk g).map (Q W) ⋯
⊢ f.map (Q W) ⋯ = g.map (Q W) ⋯