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
X Y : C
f : X ⟶ Y
L : C ⥤ D
hL : W.IsInvertedBy L
inst✝ : W.ContainsIdentities
⊢ (ofHom W f).map L hL = L.map f

Tactic:
by
  simp [map]

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

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
| F'.map
      ((commShiftIso L b).inv.app ((shiftFunctor C a).obj X) ≫
        L.map (𝟙 ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)))) ≫
    (Lifting.iso L W F F').hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
          (shiftFunctorAdd E a b).inv.app (F.obj X) ≫ (shiftFunctor E (a + b)).map ((Lifting.iso L W F F').inv.app X)

Tactic:
rw [map_id, Category.comp_id, ← NatTrans.naturality]

Goal state after:
C : Type u₁
D : Type u₂
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : Category.{v₂, u₂} D
E : Type u₃
inst✝⁸ : Category.{v₃, u₃} E
L : C ⥤ D
W : MorphismProperty C
inst✝⁷ : L.IsLocalization W
A : Type w
inst✝⁶ : AddMonoid A
inst✝⁵ : HasShift C A
F : C ⥤ E
F' : D ⥤ E
inst✝⁴ : Lifting L W F F'
inst✝³ : HasShift D A
inst✝² : HasShift E A
inst✝¹ : L.CommShift A
inst✝ : F.CommShift A
a b : A
X : C
| F'.map ((commShiftIso L b).inv.app ((shiftFunctor C a).obj X)) ≫
    (Lifting.iso L W F F').hom.app ((shiftFunctor C b).obj ((shiftFunctor C a).obj X)) ≫
      (commShiftIso F b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor E b).map ((commShiftIso F a).hom.app X) ≫
          (shiftFunctor E a ⋙ shiftFunctor E b).map ((Lifting.iso L W F F').inv.app X) ≫
            (shiftFunctorAdd E a b).inv.app (F'.obj (L.obj X))
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions

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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝ : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
⊢ F.Faithful

Tactic:
refine F.faithful_of_comp_essSurj L (fun X₁ X₂ f g hfg ↦ ?_)

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
E : Type u_3
inst✝¹ : Category.{v_3, u_3} E
F : D ⥤ E
inst✝ : W.HasLeftCalculusOfFractions
h : ∀ ⦃X₁ X₂ : C⦄ (f g : X₁ ⟶ X₂), F.map (L.map f) = F.map (L.map g) → L.map f = L.map g
this : L.EssSurj
X₁ X₂ : C
f g : L.obj X₁ ⟶ L.obj X₂
hfg : F.map f = F.map g
⊢ f = g
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{v, u'} (Cardinal.mk Y) < Cardinal.lift.{u', v} κ

Tactic:
← Cardinal.lift_lt.{_, u},

Goal state after:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{u, max u' v} (Cardinal.lift.{v, u'} (Cardinal.mk Y)) <
    Cardinal.lift.{u, max u' v} (Cardinal.lift.{u', v} κ)
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{v, u'} (Cardinal.mk Y) < Cardinal.lift.{u', v} κ

Tactic:
← Cardinal.lift_lt.{_, u},

Goal state after:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : X → Y
hf : Function.Surjective f
⊢ Cardinal.lift.{u, max u' v} (Cardinal.lift.{v, u'} (Cardinal.mk Y)) <
    Cardinal.lift.{u, max u' v} (Cardinal.lift.{u', v} κ)
Module: Mathlib.SetTheory.Cardinal.HasCardinalLT

Goal state before:
pp: case mpr
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
hX : Cardinal.lift.{max w u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', w} κ
hY : Cardinal.lift.{w, u'} (Cardinal.mk Y) < Cardinal.lift.{u', w} κ
⊢ Cardinal.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ

Tactic:
← Cardinal.lift_lt.{_, u},

Goal state after:
case mpr
X : Type u
Y : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
hX : Cardinal.lift.{max w u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', w} κ
hY :
  Cardinal.lift.{u, max u' w} (Cardinal.lift.{w, u'} (Cardinal.mk Y)) <
    Cardinal.lift.{u, max u' w} (Cardinal.lift.{u', w} κ)
⊢ Cardinal.lift.{w, max u' u} (Cardinal.mk (X ⊕ Y)) < Cardinal.lift.{max u' u, w} κ
Module: Mathlib.CategoryTheory.ObjectProperty.FiniteProducts

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderFiniteProducts
J : Type u_2
inst✝ : Finite J
f : J → C
F : Fan f
hF : IsLimit F
h : ∀ (j : J), P (f j)
j : J
⊢ P ((Discrete.functor f).obj { as := j })

Tactic:
exact h j

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

Goal state before:
pp: case a
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : ObjectProperty C
inst✝² : P.IsClosedUnderIsomorphisms
G : Type u_4
inst✝¹ : AddGroup G
inst✝ : HasShift C G
⊢ P.shift 0 ≤ ⨆ x, P.shift x

Tactic:
exact le_iSup P.shift (0 : G)

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
⊢ P Y

Tactic:
let h : IsColimit (BinaryCofan.mk (initial.to Y) e.hom) :=
      BinaryCofan.IsColimit.mk _ (fun _ f ↦ e.inv ≫ f) (by cat_disch) (by simp) (by cat_disch)
    exact P.prop_of_isColimit_binaryCofan h P.prop_initial hX

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✝¹ : P.IsClosedUnderFiniteCoproducts
J : Type u_2
inst✝ : Finite J
f : J → C
F : Cofan f
hF : IsColimit F
h : ∀ (j : J), P (f j)
j : J
⊢ P ((Discrete.functor f).obj { as := j })

Tactic:
exact h j

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
⊢ Hom.map (Hom.mk f ≫ Hom.mk g) F hF = f.map F hF ≫ g.map F hF

Tactic:
rw [homMk_comp_homMk f g z fac, Hom.map_mk]

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

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

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)
⊢ eqToHom ⋯ ≫ F₁.map ((Q W).map f.s) ≫ eqToHom ⋯ ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯

Tactic:
eqToHom_refl,

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).map f.s) ≫ 𝟙 (F₁.obj f.Y') ≫ F₁.map (Qinv f.s ⋯) = eqToHom ⋯
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
X Y : C
φ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{v_3, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
⊢ (Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) =
    (Localization.compUniqFunctor L₁ L₂ W).hom.app X ≫ φ.map L₂ ⋯ ≫ (Localization.compUniqFunctor L₁ L₂ W).inv.app Y

Tactic:
let e := Localization.compUniqFunctor L₁ L₂ W

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
X Y : C
φ : W.LeftFraction X Y
E : Type u_3
inst✝² : Category.{v_3, u_3} E
L₁ : C ⥤ D
L₂ : C ⥤ E
inst✝¹ : L₁.IsLocalization W
inst✝ : L₂.IsLocalization W
e : L₁ ⋙ (Localization.uniq L₁ L₂ W).functor ≅ L₂ := Localization.compUniqFunctor L₁ L₂ W
⊢ (Localization.uniq L₁ L₂ W).functor.map (φ.map L₁ ⋯) =
    (Localization.compUniqFunctor L₁ L₂ W).hom.app X ≫ φ.map L₂ ⋯ ≫ (Localization.compUniqFunctor L₁ L₂ W).inv.app 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
L : C ⥤ D
W : MorphismProperty C
inst✝ : L.IsLocalization W
h : W.HasRightCalculusOfFractions
X' X Y : Cᵒᵖ
f₁ f₂ : X ⟶ Y
s : X' ⟶ X
hs : W.op s
eq : s ≫ f₁ = s ≫ f₂
⊢ ∃ Y' t, ∃ (_ : W.op t), f₁ ≫ t = f₂ ≫ t

Tactic:
by
    obtain ⟨Y', t, ht, fac⟩ := h.ext f₁.unop f₂.unop s.unop hs (Quiver.Hom.op_inj eq)
    exact ⟨Opposite.op Y', t.op, ht, Quiver.Hom.unop_inj fac⟩

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
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ ↔ RightFractionRel φ ψ

Tactic:
← leftFractionRel_op_iff,

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
inst✝ : W.HasRightCalculusOfFractions
X Y : C
φ ψ : W.RightFraction X Y
⊢ φ.map L ⋯ = ψ.map L ⋯ ↔ LeftFractionRel φ.op ψ.op
Module: Mathlib.CategoryTheory.Shift.InducedShiftSequence

Goal state before:
pp: C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ (F.shift a).map (L.map f) ≫
      (F.shift a).map ((commShiftIso L n).hom.app Y) ≫
        (F.shift a).map ((commShiftIso L n).inv.app Y) ≫
          (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y =
    (e' a).hom.app X ≫ ((G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y) ≫ (e' a').inv.app Y

Tactic:
assoc

Goal state after:
C : Type u_1
D : Type u_2
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Category.{v_3, u_3} A
L : C ⥤ D
F : D ⥤ A
G : C ⥤ A
e : L ⋙ F ≅ G
M : Type u_4
inst✝⁶ : AddMonoid M
inst✝⁵ : HasShift C M
inst✝⁴ : G.ShiftSequence M
F' : M → D ⥤ A
e' : (m : M) → L ⋙ F' m ≅ G.shift m
inst✝³ : ((whiskeringLeft C D A).obj L).Full
inst✝² : ((whiskeringLeft C D A).obj L).Faithful
inst✝¹ : HasShift D M
inst✝ : L.CommShift M
n : M
X Y : C
f : X ⟶ (shiftFunctor C n).obj Y
a a' : M
h : n + a = a'
⊢ (F.shift a).map (L.map f) ≫
      (F.shift a).map ((commShiftIso L n).hom.app Y) ≫
        (F.shift a).map ((commShiftIso L n).inv.app Y) ≫
          (e' a).hom.app ((shiftFunctor C n).obj Y) ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y =
    (e' a).hom.app X ≫ (G.shift a).map f ≫ (G.shiftIso n a a' h).hom.app Y ≫ (e' a').inv.app Y
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : 0 + 0 = 0
⊢ f ≫ g ≫ (shiftFunctorZero' C 0 ⋯).inv.app Z = (f ≫ g) ≫ (shiftFunctorZero' C 0 ⋯).inv.app Z

Tactic:
assoc

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
h : 0 + 0 = 0
⊢ f ≫ g ≫ (shiftFunctorZero' C 0 ⋯).inv.app Z = f ≫ g ≫ (shiftFunctorZero' C 0 ⋯).inv.app Z
Module: Mathlib.CategoryTheory.Shift.ShiftedHom

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y : C
a : M
f : ShiftedHom X Y a
⊢ f.map (𝟭 C) = f

Tactic:
by
  simp [map]

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

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P Q : ObjectProperty C
inst✝ : Q.ContainsZero
⊢ P ≤ P.extensionProduct Q

Tactic:
intro X hX
  rw [← extensionProduct_isoClosure_right]
  obtain ⟨Z, hZ, hQ⟩ := Q.exists_prop_of_containsZero
  refine ⟨_, _, _, _, _, contractible_distinguished X, hX, ?_⟩
  exact ⟨Z, hQ, ⟨IsZero.iso (isZero_zero C) hZ⟩⟩

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P Q R : ObjectProperty C
inst✝¹ : P.IsStableUnderShift ℤ
inst✝ : Q.IsStableUnderShift ℤ
a : ℤ
X Y Z : C
f : Y ⟶ X
g : X ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj Y
hT : Triangle.mk f g h ∈ distinguishedTriangles
hP : P Y
hQ : Q Z
⊢ P ((shiftFunctor C { as := a }.as).obj (Triangle.mk f g h).obj₁)

pp: case refine_2
C : Type u_1
inst✝¹⁵ : Category.{v_1, u_1} C
inst✝¹⁴ : HasZeroObject C
inst✝¹³ : HasShift C ℤ
inst✝¹² : Preadditive C
inst✝¹¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹⁰ : Pretriangulated C
D : Type u_2
inst✝⁹ : Category.{v_2, u_2} D
inst✝⁸ : Preadditive D
inst✝⁷ : HasZeroObject D
inst✝⁶ : HasShift D ℤ
inst✝⁵ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝⁴ : Pretriangulated D
E : Type u_3
inst✝³ : Category.{v_3, u_3} E
inst✝² : HasShift E ℤ
P Q R : ObjectProperty C
inst✝¹ : P.IsStableUnderShift ℤ
inst✝ : Q.IsStableUnderShift ℤ
a : ℤ
X Y Z : C
f : Y ⟶ X
g : X ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj Y
hT : Triangle.mk f g h ∈ distinguishedTriangles
hP : P Y
hQ : Q Z
⊢ Q ((shiftFunctor C { as := a }.as).obj (Triangle.mk f g h).obj₃)

Tactic:
all_goals apply IsStableUnderShiftBy.le_shift; assumption

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

Goal state before:
pp: case succ
C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasZeroObject C
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : Pretriangulated C
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P Q R : ObjectProperty C
inst✝ : P.Nonempty
n : ℕ
h : (P.extensionProductIter n).Nonempty
⊢ (P.extensionProductIter (n + 1)).Nonempty

Tactic:
extensionProductIter_succ

Goal state after:
case succ
C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasZeroObject C
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : Pretriangulated C
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P Q R : ObjectProperty C
inst✝ : P.Nonempty
n : ℕ
h : (P.extensionProductIter n).Nonempty
⊢ (P.extensionProduct (P.extensionProductIter n)).Nonempty
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasZeroObject C
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : Pretriangulated C
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P Q R : ObjectProperty C
inst✝ : P.Nonempty
n : ℕ
⊢ (P.extensionProductIter n).Nonempty

Tactic:
by
  induction n with
  | zero => rwa [extensionProductIter_zero]
  | succ n h => rw [extensionProductIter_succ]; infer_instance

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

Goal state before:
pp: case zero
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
m m' : ℕ
h : m = m' + 1
⊢ P.extensionProductIter (m' + 1) = P.extensionProduct (P.extensionProductIter m')

Tactic:
extensionProductIter_succ

Goal state after:
case zero
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P : ObjectProperty C
inst✝ : IsTriangulated C
m m' : ℕ
h : m = m' + 1
⊢ P.extensionProduct (P.extensionProductIter m') = P.extensionProduct (P.extensionProductIter m')
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n✝ : P.ContainsZero
n m✝ m : ℕ
hnm : n ≤ m
h : P.extensionProductIter n ≤ P.extensionProductIter m
⊢ P.extensionProductIter m ≤ P.extensionProductIter (m + 1)

Tactic:
extensionProductIter_succ

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : Preadditive C
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
P : ObjectProperty C
n✝ : P.ContainsZero
n m✝ m : ℕ
hnm : n ≤ m
h : P.extensionProductIter n ≤ P.extensionProductIter m
⊢ P.extensionProductIter m ≤ P.extensionProduct (P.extensionProductIter m)
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case succ
C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasZeroObject C
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : Pretriangulated C
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P Q R : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
n : ℕ
h : (P.extensionProductIter n).IsStableUnderShift ℤ
⊢ (P.extensionProductIter (n + 1)).IsStableUnderShift ℤ

Tactic:
extensionProductIter_succ

Goal state after:
case succ
C : Type u_1
inst✝¹⁴ : Category.{v_1, u_1} C
inst✝¹³ : HasZeroObject C
inst✝¹² : HasShift C ℤ
inst✝¹¹ : Preadditive C
inst✝¹⁰ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝⁹ : Pretriangulated C
D : Type u_2
inst✝⁸ : Category.{v_2, u_2} D
inst✝⁷ : Preadditive D
inst✝⁶ : HasZeroObject D
inst✝⁵ : HasShift D ℤ
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor D n).Additive
inst✝³ : Pretriangulated D
E : Type u_3
inst✝² : Category.{v_3, u_3} E
inst✝¹ : HasShift E ℤ
P Q R : ObjectProperty C
inst✝ : P.IsStableUnderShift ℤ
n : ℕ
h : (P.extensionProductIter n).IsStableUnderShift ℤ
⊢ (P.extensionProduct (P.extensionProductIter n)).IsStableUnderShift ℤ
Module: Mathlib.CategoryTheory.Triangulated.Subcategory

Goal state before:
pp: case succ
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P Q : ObjectProperty C
inst✝ : Q.IsTriangulatedClosed₂
h : P ≤ Q
n : ℕ
H : P.extensionProductIter n ≤ Q.isoClosure
⊢ P.extensionProductIter (n + 1) ≤ Q.isoClosure

Tactic:
extensionProductIter_succ

Goal state after:
case succ
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : HasZeroObject C
inst✝⁴ : HasShift C ℤ
inst✝³ : Preadditive C
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
P Q : ObjectProperty C
inst✝ : Q.IsTriangulatedClosed₂
h : P ≤ Q
n : ℕ
H : P.extensionProductIter n ≤ Q.isoClosure
⊢ P.extensionProduct (P.extensionProductIter n) ≤ Q.isoClosure