mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.Quiv

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

Tactic:
exact (Prefunctor.congr_hom e.inv_hom_id.symm f).symm

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:
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:
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:
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:
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:
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:
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:
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:
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:
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:
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
⊢ Quiver.homOfEq
      ((he (e.symm (e X)) (e.symm (e Y))) ((he (e.symm (e X)) (e.symm (e Y))).symm (Quiver.homOfEq ((he X Y) f) ⋯ ⋯))) ⋯
      ⋯ =
    Quiver.homOfEq ((he (e.symm (e X)) (e.symm (e Y))) (Quiver.homOfEq f ⋯ ⋯)) ⋯ ⋯

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

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

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

Goal state before:
pp: case refine_5
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
inst✝ : IsTriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : Z₁₂ ⟶ X₁
w₁₂ : X₂ ⟶ (shiftFunctor C 1).obj Z₁₂
h₁₂ : Triangle.mk v₁₂ u₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : Z₂₃ ⟶ X₂
w₂₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₂₃
h₂₃ : Triangle.mk v₂₃ u₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : Z₁₃ ⟶ X₁
w₁₃ : X₃ ⟶ (shiftFunctor C 1).obj Z₁₃
h₁₃ : Triangle.mk v₁₃ u₁₃ w₁₃ ∈ distinguishedTriangles
o : Octahedron comm ⋯ ⋯ ⋯ := someOctahedron comm ⋯ ⋯ ⋯
m₁ : Z₁₂ ⟶ Z₁₃ := (shiftShiftNeg Z₁₂ 1).inv ≫ (shiftFunctor C (-1)).map o.m₁ ≫ (shiftShiftNeg Z₁₃ 1).hom
m₃ : Z₁₃ ⟶ Z₂₃ := (shiftShiftNeg Z₁₃ 1).inv ≫ (shiftFunctor C (-1)).map o.m₃ ≫ (shiftShiftNeg Z₂₃ 1).hom
eq₁ : w₁₂ ≫ o.m₁ = u₂₃ ≫ w₁₃
eq₂ : o.m₁ ≫ (shiftFunctor C 1).map v₁₃ = (shiftFunctor C 1).map v₁₂
eq₃ : w₁₃ ≫ o.m₃ = w₂₃
eq₄ : (shiftFunctor C 1).map v₁₃ ≫ (shiftFunctor C 1).map u₁₂ = o.m₃ ≫ (shiftFunctor C 1).map v₂₃
⊢ v₂₃ ≫ w₁₂ ≫ (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app ((shiftFunctor C 1).obj Z₁₂) =
    (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app Z₂₃ ≫
      ((shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app Z₂₃ ≫ v₂₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app X₂) ≫
        ((shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app X₂ ≫
            w₁₂ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).inv.app ((shiftFunctor C 1).obj Z₁₂)) ≫
          (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app ((shiftFunctor C 1).obj Z₁₂) ≫
            (shiftFunctorCompIsoId C (-1) 1 ⋯).inv.app ((shiftFunctor C 1).obj Z₁₂)

Tactic:
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:
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₁ G₂ : W.Localization ⥤ D
τ : G₁ ⟶ G₂
X : C
⊢ (𝟙 W.Q ◫ (𝟭 (W.Localization ⥤ D)).map τ).app X =
    (𝟙 W.Q ◫ (eqToHom ⋯ ≫ (functor W D ⋙ inverse W D).map τ ≫ eqToHom ⋯)).app X

Tactic:
simp

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.obj ((L.functor ⋙ L.inverse).obj X))) =
    (iso T L.functor R.functor B).hom.app X ≫ B.map (L.functor.map (L.unitIso.hom.app X))

Tactic:
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
⊢ (eqToHom ⋯ ≫ f.hom ≫ eqToHom ⋯).app x✝ = (eqToHom ⋯).app x✝ ≫ f.hom.app x✝ ≫ (eqToHom ⋯).app x✝

Tactic:
simp

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
inst✝ : L.IsLocalization ⊤
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ ⊤ f

Tactic:
simp

Goal state after:
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₂)
⊢ (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence

Tactic:
have : IsIso (whiskerRight ε₁ W₁.Q) := by
      rw [NatTrans.isIso_iff_isIso_app]
      exact fun _ ↦ Localization.inverts W₁.Q W₁ _ (hε₁ _)

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)
⊢ (Φ.localizedFunctor W₁.Q W₂.Q).IsEquivalence
Module: Mathlib.CategoryTheory.Localization.LocalizerMorphism

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁹ : Category.{v₁, u₁} C₁
inst✝⁸ : Category.{v₂, u₂} C₂
inst✝⁷ : Category.{v₃, u₃} C₃
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝⁴ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝² : Φ.functor.IsEquivalence
inst✝¹ : Φ.IsInduced
inst✝ : W₂.RespectsIso
X Y : C₂
f : X ⟶ Y
⊢ W₂ f → (W₂.inverseImage Φ.functor).inverseImage Φ.functor.inv f

Tactic:
hf

Goal state after:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
D₁ : Type u₄
D₂ : Type u₅
inst✝⁹ : Category.{v₁, u₁} C₁
inst✝⁸ : Category.{v₂, u₂} C₂
inst✝⁷ : Category.{v₃, u₃} C₃
inst✝⁶ : Category.{v₄, u₄} D₁
inst✝⁵ : Category.{v₅, u₅} D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
W₃ : MorphismProperty C₃
Φ : LocalizerMorphism W₁ W₂
L₁ : C₁ ⥤ D₁
inst✝⁴ : L₁.IsLocalization W₁
L₂ : C₂ ⥤ D₂
inst✝³ : L₂.IsLocalization W₂
G : D₁ ⥤ D₂
inst✝² : Φ.functor.IsEquivalence
inst✝¹ : Φ.IsInduced
inst✝ : W₂.RespectsIso
X Y : C₂
f : X ⟶ Y
hf : W₂ f
⊢ (W₂.inverseImage Φ.functor).inverseImage Φ.functor.inv f
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions

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
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), LeftFractionRel a₁ a₂ → a₁.comp b = a₂.comp b

Tactic:
rintro a₁ a₂ b ⟨U, t₁, t₂, hst, hft, ht⟩

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
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₁)
⊢ a₁.comp b = a₂.comp b
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:
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:
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:
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:
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:
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 ℤ
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.mapTriangle.obj T₁').mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ (L.mapTriangle.obj T₂').mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ (L.mapTriangle.obj T₁').mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ (L.mapTriangle.obj T₂').mor₂
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃

Tactic:
have comm₃ := e₁.inv.comm₃

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 ℤ
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.mapTriangle.obj T₁').mor₁ ≫ e₁.inv.hom₂ = e₁.inv.hom₁ ≫ T₁.mor₁
comm₁' : T₂.mor₁ ≫ e₂.hom.hom₂ = e₂.hom.hom₁ ≫ (L.mapTriangle.obj T₂').mor₁
comm₂ : T₁.mor₂ ≫ e₁.hom.hom₃ = e₁.hom.hom₂ ≫ (L.mapTriangle.obj T₁').mor₂
comm₂' : T₂.mor₂ ≫ e₂.hom.hom₃ = e₂.hom.hom₂ ≫ (L.mapTriangle.obj T₂').mor₂
comm₃ : (L.mapTriangle.obj T₁').mor₃ ≫ (shiftFunctor D 1).map e₁.inv.hom₁ = e₁.inv.hom₃ ≫ T₁.mor₃
⊢ ∃ c, T₁.mor₂ ≫ c = b ≫ T₂.mor₂ ∧ T₁.mor₃ ≫ (shiftFunctor D 1).map a = c ≫ T₂.mor₃
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case isMin
C : Type u
inst✝⁵ : Category.{v, u} C
P : ObjectProperty C
α : Type t
J : α → Type u'
inst✝⁴ : (a : α) → Category.{v', u'} (J a)
β : Type w'
inst✝³ : LinearOrder β
inst✝² : OrderBot β
inst✝¹ : SuccOrder β
inst✝ : WellFoundedLT β
hb : IsMin ⊥
⊢ P.strictLimitsClosureIter J ⊥ ≤ P.limitsClosure J

Tactic:
simp

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) κ
⊢ (P.strictLimitsClosureIter J κ.ord).strictLimitsClosureStep J = P.strictLimitsClosureIter J κ.ord

Tactic:
have hκ : κ.IsRegular := Fact.out

Goal state after:
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
⊢ (P.strictLimitsClosureIter J κ.ord).strictLimitsClosureStep J = P.strictLimitsClosureIter J κ.ord
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case inr
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
hF : ∀ (j : J a), P.strictLimitsClosureIter J κ.ord (F.obj j)
⊢ P.strictLimitsClosureIter J κ.ord (limit F)

Tactic:
simp only [strictLimitsClosureIter, transfiniteIterate_limit _ _ _
      (Cardinal.isSuccLimit_ord hκ.aleph0_le), prop_iSup_iff,
      Subtype.exists, Set.mem_Iio, exists_prop] at hF

Goal state after:
case inr
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
hF : ∀ (j : J a), ∃ a_1 < κ.ord, transfiniteIterate (fun Q ↦ Q.strictLimitsClosureStep J) a_1 P (F.obj j)
⊢ P.strictLimitsClosureIter J κ.ord (limit F)
Module: Mathlib.CategoryTheory.ObjectProperty.LimitsClosure

Goal state before:
pp: case refine_1
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)
⊢ Cardinal.mk (Shrink.{w, u'} (J a)) < κ.ord.cof

Tactic:
rw [hκ.cof_ord, ← hasCardinalLT_iff_cardinal_mk_lt _ κ,
          ← hasCardinalLT_iff_of_equiv (equivShrink.{w} (J a))]
        exact h a

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

Goal state after: