mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.PathCategory.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
W : MorphismProperty C
inst✝ : W.IsStableUnderComposition
X Y : C
p : Path X Y
b✝¹ c✝ : C
f : b✝¹ ⟶ c✝
b✝ : C
a✝¹ : Path X b✝
a✝ : b✝ ⟶ b✝¹
hp : W.paths (a✝¹.cons a✝) → 0 < (a✝¹.cons a✝).length → W (composePath (a✝¹.cons a✝))
hp' : W.paths ((a✝¹.cons a✝).cons f)
hp'' : 0 < ((a✝¹.cons a✝).cons f).length
⊢ 0 < (a✝¹.cons a✝).length

Tactic:
by simp

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

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ X = e.hom.obj (e.inv.obj X)

Tactic:
by simp

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

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑W
f : X ⟶ Y
⊢ Y = e.hom.obj (e.inv.obj Y)

Tactic:
by simp

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

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑V
f : X ⟶ Y
⊢ X = e.inv.obj (e.hom.obj X)

Tactic:
by simp

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

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑V
f : X ⟶ Y
⊢ Y = e.inv.obj (e.hom.obj Y)

Tactic:
by simp

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

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑V
g : e.hom.obj X ⟶ e.hom.obj Y
⊢ e.inv.obj (e.hom.obj X) = X

Tactic:
by simp

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

Goal state before:
pp: V✝ W✝ : Quiv
e✝ : V✝ ≅ W✝
V W : Quiv
e : V ≅ W
X Y : ↑V
g : e.hom.obj X ⟶ e.hom.obj Y
⊢ e.inv.obj (e.hom.obj Y) = Y

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this✝ : Epi S.g
this : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i)
⊢ (asIso (S.X₁.homologyι i)).hom ≫ (S.map (HomologicalComplex.opcyclesFunctor C c i)).f =
    (S.map (HomologicalComplex.homologyFunctor C c i)).f ≫ (asIso (S.X₂.homologyι i)).hom

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i : ι
h : ¬c.Rel i (c.next i)
this✝ : Epi S.g
this : ∀ (K : HomologicalComplex C c), IsIso (K.homologyι i)
⊢ (asIso (S.X₂.homologyι i)).hom ≫ (S.map (HomologicalComplex.opcyclesFunctor C c i)).g =
    (S.map (HomologicalComplex.homologyFunctor C c i)).g ≫ (asIso (S.X₃.homologyι i)).hom

Tactic:
by simp

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

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : ↑(of W)
f : X ⟶ Y
⊢ X = e (e.symm X)

Tactic:
by simp

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

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : ↑(of W)
f : X ⟶ Y
⊢ Y = e (e.symm Y)

Tactic:
by simp

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

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : ↑(of V)
f : X ⟶ Y
⊢ e (e.symm (e X)) = e X

Tactic:
by simp

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

Goal state before:
pp: V W : Type u
inst✝¹ : Quiver V
inst✝ : Quiver W
e : V ≃ W
he : (X Y : V) → (X ⟶ Y) ≃ (e X ⟶ e Y)
X Y : ↑(of V)
f : X ⟶ Y
⊢ e (e.symm (e Y)) = e Y

Tactic:
by simp

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

Goal state before:
pp: C : Type u
D : Type u₁
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
⊢ ∀ {X Y : C} (f : X ⟶ Y),
    (Cat.freeMap F.toPrefunctor ⋙ pathComposition D).map f.toPath ≫
        (Iso.refl ((Cat.freeMap F.toPrefunctor ⋙ pathComposition D).obj Y)).hom =
      (Iso.refl ((Cat.freeMap F.toPrefunctor ⋙ pathComposition D).obj X)).hom ≫ (pathComposition C ⋙ F).map f.toPath

Tactic:
by simp

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

Goal state before:
pp: C : Type u
D : Type u₁
inst✝¹ : Category.{v, u} C
inst✝ : Category.{v₁, u₁} D
F : C ⥤ D
⊢ ∀ (a b : C) (e : a ⟶ b),
    (Cat.freeMap F.toPrefunctor ⋙ pathComposition D).map e.toPath =
      eqToHom ⋯ ≫ (pathComposition C ⋙ F).map e.toPath ≫ eqToHom ⋯

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
ι : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
c : ComplexShape ι
S : ShortComplex (HomologicalComplex C c)
hS : S.ShortExact
i j : ι
hij : c.Rel i j
A : C
x₃ : A ⟶ S.X₃.X i
hx₃ : x₃ ≫ S.X₃.d i j = 0
x₂ : A ⟶ S.X₂.X i
hx₂ : x₂ ≫ S.g.f i = x₃
x₁ : A ⟶ S.X₁.X j
hx₁ : x₁ ≫ S.f.f j = x₂ ≫ S.X₂.d i j
k : ι
hk : c.next j = k
⊢ x₁ ≫ S.X₁.d j k = 0

Tactic:
have := hS.mono_f
        rw [← cancel_mono (S.f.f k), assoc, ← S.f.comm, reassoc_of% hx₁,
          d_comp_d, comp_zero, zero_comp]

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

Goal state before:
pp: V : Type u
inst✝ : Quiver V
⊢ ∀ {X Y : V} (f : X ⟶ Y),
    (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)).map f.toPath ≫
        (Iso.refl ((Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)).obj Y)).hom =
      (Iso.refl ((Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)).obj X)).hom ≫ (𝟭 (Paths V)).map f.toPath

Tactic:
by simp

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

Goal state before:
pp: V : Type u
inst✝ : Quiver V
⊢ ∀ (a b : V) (e : a ⟶ b),
    (Cat.freeMap (Paths.of V) ⋙ pathComposition (Paths V)).map e.toPath =
      eqToHom ⋯ ≫ (𝟭 (Paths V)).map e.toPath ≫ eqToHom ⋯

Tactic:
by simp

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
F G : W.Localization ⥤ D
τ : W.Q ⋙ F ⟶ W.Q ⋙ G
⊢ 𝟙 W.Q ◫ natTransExtension τ = τ

Tactic:
by simp

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

Goal state before:
pp: case refine_2
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
G₁ : C ⥤ D
hG₁ : W.IsInvertedBy G₁
G₂ : C ⥤ D
hG₂ : W.IsInvertedBy G₂
f : { obj := G₁, property := hG₁ } ⟶ { obj := G₂, property := hG₂ }
x✝ : C
⊢ NatTransExtension.app (eqToHom ⋯ ≫ f.hom ≫ eqToHom ⋯) (W.Q.obj x✝) =
    (eqToHom ⋯).hom.app x✝ ≫ f.hom.app x✝ ≫ (eqToHom ⋯).hom.app x✝

Tactic:
rw [NatTransExtension.app_eq, InducedCategory.eqToHom_hom,
          InducedCategory.eqToHom_hom]

Goal state after:
case refine_2
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
G₁ : C ⥤ D
hG₁ : W.IsInvertedBy G₁
G₂ : C ⥤ D
hG₂ : W.IsInvertedBy G₂
f : { obj := G₁, property := hG₁ } ⟶ { obj := G₂, property := hG₂ }
x✝ : C
⊢ (eqToHom ⋯ ≫ f.hom ≫ eqToHom ⋯).app x✝ = (eqToHom ⋯).app x✝ ≫ f.hom.app x✝ ≫ (eqToHom ⋯).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
inst✝ : L.IsLocalization ⊤
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ ⊤ f

Tactic:
by simp

Goal state after:
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 + φ.snd.map F hF) ≫ F.map φ.s

Tactic:
add_comp,

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)
⊢ φ.add.map F hF ≫ F.map φ.s = φ.fst.map F hF ≫ F.map φ.s + φ.snd.map F hF ≫ F.map φ.s
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor ⋙ Ψ.functor
ε₂ : 𝟭 C₂ ⟶ Ψ.functor ⋙ Φ.functor
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
⊢ IsIso (whiskerRight ε₁ W₁.Q)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor ⋙ Ψ.functor
ε₂ : 𝟭 C₂ ⟶ Ψ.functor ⋙ Φ.functor
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
⊢ ∀ (X : C₁), IsIso ((whiskerRight ε₁ W₁.Q).app X)
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor ⋙ Ψ.functor
ε₂ : 𝟭 C₂ ⟶ Ψ.functor ⋙ Φ.functor
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this : IsIso (whiskerRight ε₁ W₁.Q)
⊢ IsIso (whiskerRight ε₂ W₂.Q)

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
inst✝¹ : Category.{v₁, u₁} C₁
inst✝ : Category.{v₂, u₂} C₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₁
ε₁ : 𝟭 C₁ ⟶ Φ.functor ⋙ Ψ.functor
ε₂ : 𝟭 C₂ ⟶ Ψ.functor ⋙ Φ.functor
hε₁ : ∀ (X₁ : C₁), W₁ (ε₁.app X₁)
hε₂ : ∀ (X₂ : C₂), W₂ (ε₂.app X₂)
this : IsIso (whiskerRight ε₁ W₁.Q)
⊢ ∀ (X : C₂), IsIso ((whiskerRight ε₂ W₂.Q).app X)
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φ₁ : φ₀.fst.map L ⋯ = φ.fst.map L ⋯
hφ₂ : φ₀.snd.map L ⋯ = φ.snd.map L ⋯
hφ₀ : add' W (φ₀.fst.map L ⋯) (φ₀.snd.map L ⋯) = φ₀.add.map L ⋯
Z : C
t₁ : φ₀.Y' ⟶ Z
t₂ : φ.Y' ⟶ Z
hst : φ₀.s ≫ t₁ = φ.s ≫ t₂
hft : φ₀.f ≫ t₁ = φ.f ≫ t₂
hft' : φ₀.f' ≫ t₁ = φ.f' ≫ t₂
ht : W (φ₀.s ≫ t₁)
this : IsIso (L.map (φ₀.s ≫ t₁))
⊢ L.map (φ₀.add.f ≫ t₁) = L.map (φ.add.f ≫ t₂)

Tactic:
add_comp,

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

Tactic:
add_comp,

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

Tactic:
by
  rw [add'_comm, add'_zero]

Goal state after:
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₁ f₂ f₃ : L.obj X ⟶ L.obj Y
⊢ add' W (add' W f₁ f₂) f₃ = add' W f₁ (add' W f₂ f₃)

Tactic:
obtain ⟨α, h₁, h₂, h₃⟩ := exists_leftFraction₃ L W f₁ f₂ f₃
  rw [add'_eq W f₁ f₂ α.forgetThd h₁ h₂, add'_eq W f₂ f₃ α.forgetFst h₂ h₃,
    add'_eq W _ _ (LeftFraction₂.mk (α.f + α.f') α.f'' α.s α.hs) rfl h₃,
    add'_eq W _ _ (LeftFraction₂.mk α.f (α.f' + α.f'') α.s α.hs) h₁ rfl]
  dsimp [LeftFraction₂.add]
  rw [add_assoc]

Goal state after:
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 Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
x✝ : X' ⟶ Y'
⊢ (fun g ↦ eX.inv ≫ g ≫ eY.hom) ((fun f ↦ eX.hom ≫ f ≫ eY.inv) x✝) = x✝

Tactic:
by simp

Goal state after:
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 Z : C
X' Y' Z' : D
eX : L.obj X ≅ X'
eY : L.obj Y ≅ Y'
eZ : L.obj Z ≅ Z'
x✝ : L.obj X ⟶ L.obj Y
⊢ (fun f ↦ eX.hom ≫ f ≫ eY.inv) ((fun g ↦ eX.inv ≫ g ≫ eY.hom) x✝) = x✝

Tactic:
by simp

Goal state after:
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 ℤ
inst✝³ : L.EssSurj
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
inst✝ : L.PreservesZeroMorphisms
X : D
⊢ ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).mor₁ ≫
      (Iso.refl ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).obj₂).hom =
    (Iso.refl ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).obj₁).hom ≫
      (L.mapTriangle.obj (contractibleTriangle (L.objPreimage X))).mor₁

Tactic:
by simp

Goal state after:
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 ℤ
inst✝³ : L.EssSurj
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
inst✝ : L.PreservesZeroMorphisms
X : D
⊢ ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).mor₂ ≫ L.mapZeroObject.symm.hom =
    (Iso.refl ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).obj₂).hom ≫
      (L.mapTriangle.obj (contractibleTriangle (L.objPreimage X))).mor₂

Tactic:
by simp

Goal state after:
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 ℤ
inst✝³ : L.EssSurj
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms D
inst✝ : L.PreservesZeroMorphisms
X : D
⊢ ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).mor₃ ≫
      (shiftFunctor D 1).map (Iso.refl ((contractibleTriangleFunctor D).obj (L.obj (L.objPreimage X))).obj₁).hom =
    L.mapZeroObject.symm.hom ≫ (L.mapTriangle.obj (contractibleTriangle (L.objPreimage X))).mor₃

Tactic:
by simp

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

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
⊢ G.map (φ.add.map L ⋯ ≫ L.map φ.s) = (G.map (φ.fst.map L ⋯) + G.map (φ.snd.map L ⋯)) ≫ G.map (L.map φ.s)

Tactic:
add_comp,

Goal state after:
case mpr
C : Type u_1
D : Type u_2
inst✝⁸ : Category.{v_1, u_1} C
inst✝⁷ : Category.{v_2, u_2} D
inst✝⁶ : Preadditive C
L : C ⥤ D
W : MorphismProperty C
inst✝⁵ : L.IsLocalization W
inst✝⁴ : W.HasLeftCalculusOfFractions
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : Preadditive E
inst✝¹ : Preadditive D
inst✝ : L.Additive
G : D ⥤ E
h : (L ⋙ G).Additive
X Y : C
φ : W.LeftFraction₂ X Y
⊢ G.map (φ.add.map L ⋯ ≫ L.map φ.s) =
    G.map (φ.fst.map L ⋯) ≫ G.map (L.map φ.s) + G.map (φ.snd.map L ⋯) ≫ G.map (L.map φ.s)
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝ : (a : α) → Category.{v', u'} (J a)
⊢ P.isoClosure.limitsClosure J = P.limitsClosure J

Tactic:
refine le_antisymm (limitsClosure_le ?_)
    (limitsClosure_monotone _ P.le_isoClosure)
  rw [isoClosure_le_iff]
  exact le_limitsClosure P J

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

Goal state before:
pp: case of_colimitPresentation
C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
Q : ObjectProperty C
inst✝¹ : Q.IsClosedUnderIsomorphisms
inst✝ : ∀ (a : α), Q.IsClosedUnderColimitsOfShape (J a)
h✝ : P ≤ Q
X X✝ : C
a✝ : α
pres : ColimitPresentation (J a✝) X✝
h : ∀ (j : J a✝), P.colimitsClosure J (pres.diag.obj j)
h' : ∀ (j : J a✝), Q (pres.diag.obj j)
⊢ Q X✝

Tactic:
exact Q.prop_of_isColimit pres.isColimit h'

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝² : (a : α) → Category.{v', u'} (J a)
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
h : ∀ (a : α), HasCardinalLT (J a) κ
hκ : κ.IsRegular
this : ∀ (a : α), Small.{w, u'} (J a)
a : α
F : J a ⥤ C
inst✝ : HasLimit F
o : J a → Ordinal.{w}
ho : ∀ (j : J a), o j < κ.ord
ho' : ∀ (j : J a), transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) (o j) P (F.obj j)
m : Ordinal.{w}
hm : m < κ.ord
hm' : ∀ (j : J a), o j ≤ m
⊢ ¬IsMax m

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasTerminal C
inst✝¹ : P.IsClosedUnderLimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryProducts
X Y : C
e : X ≅ Y
hX : P X
⊢ ∀ {T : C} (f : T ⟶ ⊤_ C) (g : T ⟶ X), (g ≫ e.hom) ≫ (BinaryFan.mk (terminal.from Y) e.inv).snd = g

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
P : ObjectProperty C
G : Type u_4
inst✝³ : AddGroup G
inst✝² : HasShift C G
inst✝¹ : P.IsStableUnderShift G
inst✝ : P.IsClosedUnderIsomorphisms
X : C
g : G
hX : P ((shiftFunctor C g).obj X)
⊢ g + -g = 0

Tactic:
by simp

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 Y : C
z : W.LeftFraction X Y
⊢ z.f ≫ (ofHom W z.f).s = (ofHom W (𝟙 X)).s ≫ (ofHom W z.f).f

Tactic:
by simp

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

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : HasInitial C
inst✝¹ : P.IsClosedUnderColimitsOfShape (Discrete PEmpty.{1})
inst✝ : P.IsClosedUnderBinaryCoproducts
X Y : C
e : X ≅ Y
hX : P X
⊢ ∀ {T : C} (f : ⊥_ C ⟶ T) (g : X ⟶ T), (BinaryCofan.mk (initial.to Y) e.hom).inr ≫ e.inv ≫ g = g

Tactic:
by simp

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 Y : C
z : W.LeftFraction X Y
⊢ (ofHom W (𝟙 Y)).f ≫ (ofInv z.s ⋯).s = z.s ≫ (ofInv z.s ⋯).f

Tactic:
by simp

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 Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
⊢ (ofHom W g).f ≫ (ofHom W g).s = (ofHom W f).s ≫ (ofHom W g).f

Tactic:
by simp

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
⊢ (ofInv s hs).f ≫ (ofHom W (𝟙 (ofHom W f).Y')).s = (ofHom W f).s ≫ (ofHom W (𝟙 (ofHom W f).Y')).f

Tactic:
by simp

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 Y : C
s : X ⟶ Y
hs : W s
⊢ { Y' := Y, f := s, s := s, hs := hs }.s ≫ 𝟙 Y = (ofHom W (𝟙 ((Q W).obj X))).s ≫ s

Tactic:
by simp

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 Y : C
s : X ⟶ Y
hs : W s
⊢ { Y' := Y, f := s, s := s, hs := hs }.f ≫ 𝟙 Y = (ofHom W (𝟙 ((Q W).obj X))).f ≫ s

Tactic:
by simp

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 Y : C
s : X ⟶ Y
hs : W s
⊢ (ofHom W s).f ≫ (ofHom W (𝟙 Y)).s = (ofInv s hs).s ≫ (ofHom W (𝟙 Y)).f

Tactic:
by simp

Goal state after: