mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℤ
γ : Cochain K L n
a n' m' : ℤ
hn' : n + a = n'
m : ℤ
hm' : m + a = m'
⊢ δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (δ n m γ).leftShift a m' hm'

Tactic:
by_cases hnm : n + 1 = m
  · have hnm' : n' + 1 = m' := by lia
    ext p q hpq
    dsimp
    rw [(δ n m γ).leftShift_v a m' hm' p q hpq (p + a) (by lia),
      δ_v n m hnm _ (p + a) q (by lia) (p + n') (p + 1 + a) (by lia) (by lia),
      δ_v n' m' hnm' _ p q hpq (p + n') (p + 1) (by lia) rfl,
      γ.leftShift_v a n' hn' p (p + n') rfl (p + a) (by lia),
      γ.leftShift_v a n' hn' (p + 1) q (by lia) (p + 1 + a) (by lia)]
    simp only [shiftFunctor_obj_X, shiftFunctorObjXIso, HomologicalComplex.XIsoOfEq_rfl,
      Iso.refl_hom, id_comp, Linear.units_smul_comp, shiftFunctor_obj_d',
      Linear.comp_units_smul, smul_add, smul_smul]
    congr 2
    · rw [← hnm', add_comm n', mul_add, mul_one]
      simp only [Int.negOnePow_add, ← mul_assoc, Int.units_mul_self, one_mul]
    · simp only [← Int.negOnePow_add, ← hn', ← hm', ← hnm]
      congr 1
      linarith
  · have hnm' : ¬ n' + 1 = m' := fun _ => hnm (by lia)
    rw [δ_shape _ _ hnm', δ_shape _ _ hnm, leftShift_zero, smul_zero]

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

Goal state before:
pp: case refine_3
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₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
X₁' X₂' X₃' Z₁₂' Z₂₃' Z₁₃' : C
u₁₂' : X₁' ⟶ X₂'
u₂₃' : X₂' ⟶ X₃'
u₁₃' : X₁' ⟶ X₃'
comm' : u₁₂' ≫ u₂₃' = u₁₃'
e₁ : X₁ ≅ X₁'
e₂ : X₂ ≅ X₂'
e₃ : X₃ ≅ X₃'
comm₁₂ : u₁₂ ≫ e₂.hom = e₁.hom ≫ u₁₂'
comm₂₃ : u₂₃ ≫ e₃.hom = e₂.hom ≫ u₂₃'
v₁₂' : X₂' ⟶ Z₁₂'
w₁₂' : Z₁₂' ⟶ (shiftFunctor C 1).obj X₁'
h₁₂' : Triangle.mk u₁₂' v₁₂' w₁₂' ∈ distinguishedTriangles
v₂₃' : X₃' ⟶ Z₂₃'
w₂₃' : Z₂₃' ⟶ (shiftFunctor C 1).obj X₂'
h₂₃' : Triangle.mk u₂₃' v₂₃' w₂₃' ∈ distinguishedTriangles
v₁₃' : X₃' ⟶ Z₁₃'
w₁₃' : Z₁₃' ⟶ (shiftFunctor C 1).obj X₁'
h₁₃' : Triangle.mk u₁₃' v₁₃' w₁₃' ∈ distinguishedTriangles
H : Octahedron comm' h₁₂' h₂₃' h₁₃'
iso₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ≅ Triangle.mk u₁₂' v₁₂' w₁₂' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂
iso₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ≅ Triangle.mk u₂₃' v₂₃' w₂₃' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃
iso₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ≅ Triangle.mk u₁₃' v₁₃' w₁₃' :=
  isoTriangleOfIso₁₂ (Triangle.mk u₁₃ v₁₃ w₁₃) (Triangle.mk u₁₃' v₁₃' w₁₃') h₁₃ h₁₃' e₁ e₃ ⋯
eq₁₂ :
  v₁₂ ≫ (isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂).hom.hom₃ =
    e₂.hom ≫ v₁₂'
eq₁₂' :
  w₁₂ ≫ (shiftFunctor C 1).map e₁.hom =
    (isoTriangleOfIso₁₂ (Triangle.mk u₁₂ v₁₂ w₁₂) (Triangle.mk u₁₂' v₁₂' w₁₂') h₁₂ h₁₂' e₁ e₂ comm₁₂).hom.hom₃ ≫ w₁₂'
eq₁₃ :
  v₁₃ ≫ (isoTriangleOfIso₁₂ (Triangle.mk u₁₃ v₁₃ w₁₃) (Triangle.mk u₁₃' v₁₃' w₁₃') h₁₃ h₁₃' e₁ e₃ ⋯).hom.hom₃ =
    e₃.hom ≫ v₁₃'
eq₁₃' :
  w₁₃ ≫ (shiftFunctor C 1).map e₁.hom =
    (isoTriangleOfIso₁₂ (Triangle.mk u₁₃ v₁₃ w₁₃) (Triangle.mk u₁₃' v₁₃' w₁₃') h₁₃ h₁₃' e₁ e₃ ⋯).hom.hom₃ ≫ w₁₃'
eq₂₃ :
  v₂₃ ≫ (isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃).hom.hom₃ =
    e₃.hom ≫ v₂₃'
eq₂₃' :
  w₂₃ ≫ (shiftFunctor C 1).map e₂.hom =
    (isoTriangleOfIso₁₂ (Triangle.mk u₂₃ v₂₃ w₂₃) (Triangle.mk u₂₃' v₂₃' w₂₃') h₂₃ h₂₃' e₂ e₃ comm₂₃).hom.hom₃ ≫ w₂₃'
rel₁₂ : v₁₂' ≫ H.m₁ = u₂₃' ≫ v₁₃'
rel₁₃ : w₁₂' = H.m₁ ≫ w₁₃'
rel₂₂ : v₁₃' ≫ H.m₃ = v₂₃'
rel₂₃ : w₁₃' ≫ (shiftFunctor C 1).map u₁₂' = H.m₃ ≫ w₂₃'
⊢ v₁₃ ≫ iso₁₃.hom.hom₃ ≫ H.m₃ ≫ iso₂₃.inv.hom₃ = v₂₃

Tactic:
rw [reassoc_of% eq₁₃, reassoc_of% rel₂₂, ← cancel_mono iso₂₃.hom.hom₃, assoc, assoc,
      iso₂₃.inv_hom_id_triangle_hom₃, eq₂₃]
    dsimp
    rw [comp_id]

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
p : ℤ
this : Mono (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ (δ 1 2 (Cochain.mk fun p q x ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r)).v p (p + 2) ⋯ = 0

Tactic:
δ_v 1 2 (by lia) _ p (p + 2) (by lia) (p + 1) (p + 1)
        (by lia) (by lia),

Goal state after:
C : Type u_1
inst✝¹ : Category.{v, u_1} C
inst✝ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
p : ℤ
this : Mono (S.f.f (p + 2))
r_f : ∀ (n : ℤ), (σ n).r ≫ S.f.f n = 𝟙 (S.X₂.X n) - S.g.f n ≫ (σ n).s
s_g : ∀ (n : ℤ), (σ n).s ≫ S.g.f n = 𝟙 (S.X₃.X n)
⊢ (Cochain.mk fun p q x ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r).v p (p + 1) ⋯ ≫ S.X₁.d (p + 1) (p + 2) +
      Int.negOnePow 2 • S.X₃.d p (p + 1) ≫ (Cochain.mk fun p q x ↦ (σ p).s ≫ S.X₂.d p q ≫ (σ q).r).v (p + 1) (p + 2) ⋯ =
    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✝¹² : HasZeroObject C
inst✝¹¹ : HasZeroObject D
inst✝¹⁰ : HasZeroObject E
inst✝⁹ : Preadditive C
inst✝⁸ : Preadditive D
inst✝⁷ : Preadditive E
inst✝⁶ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor E n).Additive
inst✝³ : Pretriangulated C
inst✝² : Pretriangulated D
inst✝¹ : Pretriangulated E
inst✝ : F.IsTriangulated
⊢ PreservesLimitsOfShape (Discrete WalkingPair) F

Tactic:
suffices ∀ (X₁ X₃ : C), IsIso (prodComparison F X₁ X₃) by
    have := fun (X₁ X₃ : C) ↦ PreservesLimitPair.of_iso_prod_comparison F X₁ X₃
    exact ⟨fun {K} ↦ preservesLimit_of_iso_diagram F (diagramIsoPair K).symm⟩
  intro X₁ X₃
  let φ : F.mapTriangle.obj (binaryProductTriangle X₁ X₃) ⟶
      binaryProductTriangle (F.obj X₁) (F.obj X₃) :=
    { hom₁ := 𝟙 _
      hom₂ := prodComparison F X₁ X₃
      hom₃ := 𝟙 _
      comm₁ := by
        dsimp
        ext
        · simp only [assoc, prodComparison_fst, prod.comp_lift, comp_id, comp_zero,
            limit.lift_π, BinaryFan.mk_pt, BinaryFan.π_app_left, BinaryFan.mk_fst,
            ← F.map_comp, F.map_id]
        · simp only [assoc, prodComparison_snd, prod.comp_lift, comp_id, comp_zero,
            limit.lift_π, BinaryFan.mk_pt, BinaryFan.π_app_right, BinaryFan.mk_snd,
            ← F.map_comp, F.map_zero]
      comm₂ := by simp
      comm₃ := by simp }
  exact isIso₂_of_isIso₁₃ φ (F.map_distinguished _ (binaryProductTriangle_distinguished X₁ X₃))
    (binaryProductTriangle_distinguished _ _)
    (by dsimp [φ]; infer_instance) (by dsimp [φ]; infer_instance)

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

Goal state before:
pp: V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
⊢ Φ = lift (of V ⋙q Φ.toPrefunctor)

Tactic:
fapply Functor.ext

Goal state after:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
⊢ ∀ (X : Paths V), Φ.obj X = (lift (of V ⋙q Φ.toPrefunctor)).obj X

case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
Φ : Paths V ⥤ C
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), Φ.map f = eqToHom ⋯ ≫ (lift (of V ⋙q Φ.toPrefunctor)).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1
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
⊢ { 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 := ⋯ }.Exact

Tactic:
have : Epi (ShortComplex.map S (eval C c i)).g := by dsimp; infer_instance
  have hj := (hS.map (HomologicalComplex.eval C c i)).gIsCokernel
  apply ShortComplex.exact_of_g_is_cokernel
  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.CategoryTheory.PathCategory.Basic

Goal state before:
pp: V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
⊢ F = G

Tactic:
fapply Functor.ext

Goal state after:
case h_obj
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
⊢ ∀ (X : Paths V), F.obj X = G.obj X

case h_map
V : Type u₁
inst✝¹ : Quiver V
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : Paths V ⥤ C
h_obj : F.obj = G.obj
h : ∀ (a b : V) (e : a ⟶ b), F.map e.toPath = eqToHom ⋯ ≫ G.map e.toPath ≫ eqToHom ⋯
⊢ autoParam (∀ (X Y : Paths V) (f : X ⟶ Y), F.map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯) Functor.ext._auto_1
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 ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
⊢ k ≫ cyclesMap S.g i ≫ S.X₃.iCycles i = 0

Tactic:
reassoc_of% hk,

Goal state after:
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 ⟶ S.X₂.cycles i
hk : k ≫ cyclesMap S.g i = 0
⊢ 0 ≫ S.X₃.iCycles i = 0
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
X : C
hX : W (𝟙 X)
⊢ (isoOfHom L W (𝟙 X) hX).inv ≫ (isoOfHom L W (𝟙 X) hX).hom = 𝟙 (L.obj X) ≫ (isoOfHom L W (𝟙 X) hX).hom

Tactic:
Iso.inv_hom_id,

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
X : C
hX : W (𝟙 X)
⊢ 𝟙 (L.obj X) = 𝟙 (L.obj X) ≫ (isoOfHom L W (𝟙 X) hX).hom
Module: Mathlib.CategoryTheory.Localization.Construction

Goal state before:
pp: C : Type uC
inst✝¹ : Category.{uC', uC} C
W : MorphismProperty C
D : Type uD
inst✝ : Category.{uD', uD} D
G : C ⥤ D
hG : W.IsInvertedBy G
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
⊢ ∀ ⦃X Y : W.Localization⦄ (f : X ⟶ Y), F₁.map f ≫ NatTransExtension.app τ Y = NatTransExtension.app τ X ≫ F₂.map f

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

Goal state after:
Module: Mathlib.CategoryTheory.CatCommSq

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

Tactic:
Iso.inv_hom_id,

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

Tactic:
Iso.inv_hom_id,

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 ≫ 𝟙 (L.1 Y) = (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: 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 = (uniq W.Q L W).functor.map (𝟙 (W.Q.obj Y)) ≫ e.hom.app Y

Tactic:
map_id,

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 = 𝟙 ((uniq W.Q L W).functor.obj (W.Q.obj Y)) ≫ e.hom.app Y
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
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
F : C ⥤ D
hF : W.IsInvertedBy F
inst✝¹ : Preadditive D
inst✝ : F.Additive
this : IsIso (F.map φ.s)
⊢ φ.add.map F hF ≫ F.map φ.s = φ.fst.map F hF ≫ F.map φ.s + φ.snd.map F hF ≫ F.map φ.s

Tactic:
LeftFraction.map_comp_map_s,

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
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
F : C ⥤ D
hF : W.IsInvertedBy F
inst✝¹ : Preadditive D
inst✝ : F.Additive
this : IsIso (F.map φ.s)
⊢ F.map φ.add.f = φ.fst.map F hF ≫ F.map φ.s + φ.snd.map F hF ≫ F.map φ.s
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
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
F : C ⥤ D
hF : W.IsInvertedBy F
inst✝¹ : Preadditive D
inst✝ : F.Additive
this : IsIso (F.map φ.s)
⊢ F.map φ.add.f = φ.fst.map F hF ≫ F.map φ.s + φ.snd.map F hF ≫ F.map φ.s

Tactic:
LeftFraction.map_comp_map_s,

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
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
F : C ⥤ D
hF : W.IsInvertedBy F
inst✝¹ : Preadditive D
inst✝ : F.Additive
this : IsIso (F.map φ.s)
⊢ F.map φ.add.f = F.map φ.fst.f + φ.snd.map F hF ≫ F.map φ.s
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
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
F : C ⥤ D
hF : W.IsInvertedBy F
inst✝¹ : Preadditive D
inst✝ : F.Additive
this : IsIso (F.map φ.s)
⊢ F.map φ.add.f = F.map φ.fst.f + φ.snd.map F hF ≫ F.map φ.s

Tactic:
LeftFraction.map_comp_map_s,

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
W : MorphismProperty C
X Y : C
φ : W.LeftFraction₂ X Y
F : C ⥤ D
hF : W.IsInvertedBy F
inst✝¹ : Preadditive D
inst✝ : F.Additive
this : IsIso (F.map φ.s)
⊢ F.map φ.add.f = F.map φ.fst.f + F.map φ.snd.f
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
φ φ₀ : W.LeftFraction X Y
hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
Y' : C
t₁ : φ₀.Y' ⟶ Y'
t₂ : φ.Y' ⟶ Y'
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ neg' W (φ₀.map L ⋯) = φ.neg.map L ⋯

Tactic:
rw [← cancel_mono (L.map (φ₀.s ≫ t₁))]

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
φ φ₀ : W.LeftFraction X Y
hφ₀ : neg' W (φ₀.map L ⋯) = φ₀.neg.map L ⋯
Y' : C
t₁ : φ₀.Y' ⟶ Y'
t₂ : φ.Y' ⟶ Y'
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ neg' W (φ₀.map L ⋯) ≫ L.map (φ₀.s ≫ t₁) = φ.neg.map L ⋯ ≫ L.map (φ₀.s ≫ t₁)
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
α : W.LeftFraction X Y
⊢ add' W (neg' W (α.map L ⋯)) (α.map L ⋯) = L.map 0

Tactic:
add'_eq W _ _ (LeftFraction₂.mk (-α.f) α.f α.s α.hs) (neg'_eq W _ _ rfl) rfl

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
α : W.LeftFraction X Y
⊢ { Y' := α.Y', f := -α.f, f' := α.f, s := α.s, hs := ⋯ }.add.map L ⋯ = L.map 0
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.f ≫ α.s = { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ α.f
ψ : W.LeftFraction₂ X Y := { Y' := α.Y', f := φ.f ≫ α.f, f' := φ'.f ≫ α.s, s := φ'.s ≫ α.s, hs := ⋯ }
this : IsIso (L.map (φ'.s ≫ α.s))
⊢ f ≫ L.map (φ'.s ≫ α.s) = ψ.fst.map L ⋯ ≫ L.map (φ'.s ≫ α.s)

Tactic:
LeftFraction.map_comp_map_s,

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.f ≫ α.s = { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ α.f
ψ : W.LeftFraction₂ X Y := { Y' := α.Y', f := φ.f ≫ α.f, f' := φ'.f ≫ α.s, s := φ'.s ≫ α.s, hs := ⋯ }
this : IsIso (L.map (φ'.s ≫ α.s))
⊢ f ≫ L.map (φ'.s ≫ α.s) = L.map ψ.fst.f
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

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
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.f ≫ α.s = { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ α.f
ψ : W.LeftFraction₂ X Y := { Y' := α.Y', f := φ.f ≫ α.f, f' := φ'.f ≫ α.s, s := φ'.s ≫ α.s, hs := ⋯ }
this : IsIso (L.map (φ'.s ≫ α.s))
⊢ L.map φ'.f ≫ L.map α.s = ψ.snd.map L ⋯ ≫ L.map (φ'.s ≫ α.s)

Tactic:
LeftFraction.map_comp_map_s,

Goal state after:
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
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
X Y : C
f f' : L.obj X ⟶ L.obj Y
φ : W.LeftFraction X Y
hφ : f = φ.map L ⋯
φ' : W.LeftFraction X Y
hφ' : f' = φ'.map L ⋯
α : W.LeftFraction φ.Y' φ'.Y'
hα : { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.f ≫ α.s = { X' := Y, s := φ.s, hs := ⋯, f := φ'.s }.s ≫ α.f
ψ : W.LeftFraction₂ X Y := { Y' := α.Y', f := φ.f ≫ α.f, f' := φ'.f ≫ α.s, s := φ'.s ≫ α.s, hs := ⋯ }
this : IsIso (L.map (φ'.s ≫ α.s))
⊢ L.map φ'.f ≫ L.map α.s = L.map ψ.snd.f