awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y : C
m : M
inst_7 : HasSmallLocalizedShiftedHom W M X Y
inst_8 : HasSmallLocalizedShiftedHom W M X Y
e : SmallShiftedHom W X Y m
e_a :
  Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) Y))
    ((SmallHom.equiv W L : (a : SmallShiftedHom W X Y m) → L.obj X ⟶ L.obj ((shiftFunctor C m).obj Y))
        ((chgUniv (W := W) : (a : SmallShiftedHom W X Y m) → SmallShiftedHom W X Y m) e) :
      L.obj X ⟶ L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) Y))
    ((SmallHom.equiv W L : (a : SmallShiftedHom W X Y m) → L.obj X ⟶ L.obj ((shiftFunctor C m).obj Y)) e :
      L.obj X ⟶ L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) Y))
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj X) (L.obj Y) m)
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) Y))
        ((SmallHom.equiv W L : (a : SmallShiftedHom W X Y m) → L.obj X ⟶ L.obj ((shiftFunctor C m).obj Y))
          ((chgUniv (W := W) : (a : SmallShiftedHom W X Y m) → SmallShiftedHom W X Y m) e))
        (NatTrans.app (Iso.hom (Functor.commShiftIso L m)) Y) :
      L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D m) (L.obj Y))
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) Y))
        ((SmallHom.equiv W L : (a : SmallShiftedHom W X Y m) → L.obj X ⟶ L.obj ((shiftFunctor C m).obj Y)) e)
        (NatTrans.app (Iso.hom (Functor.commShiftIso L m)) Y) :
      L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D m) (L.obj Y))

Tactic:
congr
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C M
inst_4 : HasShift.{v₂, u₂, w'} D M
L : Functor.{v₁, v₂, u₁, u₂} C D
inst_5 : L.IsLocalization W
inst_6 : L.CommShift M
X Y : C
m : M
inst_7 : HasSmallLocalizedShiftedHom W M X Y
inst_8 : HasSmallLocalizedShiftedHom W M X Y
e : SmallShiftedHom W X Y m
⊢ Eq.{v₂ + 1} (α := L.obj X ⟶ L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) Y))
    ((SmallHom.equiv W L : (a : SmallShiftedHom W X Y m) → L.obj X ⟶ L.obj ((shiftFunctor C m).obj Y))
        ((chgUniv (W := W) : (a : SmallShiftedHom W X Y m) → SmallShiftedHom W X Y m) e) :
      L.obj X ⟶ L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) Y))
    ((SmallHom.equiv W L : (a : SmallShiftedHom W X Y m) → L.obj X ⟶ L.obj ((shiftFunctor C m).obj Y)) e :
      L.obj X ⟶ L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m) Y))

Tactic:
apply SmallHom.equiv_chgUniv

Premises used: CategoryTheory.Localization.SmallHom.equiv_chgUniv
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
D₁ : Type u₁'
inst_2 : Category.{v₁', u₁'} D₁
D₂ : Type u₂'
inst_3 : Category.{v₂', u₂'} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₁', u₁, u₁'} C₁ D₁
L₂ : Functor.{v₂, v₂', u₂, u₂'} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
M : Type w'
inst_6 : AddMonoid M
inst_7 : HasShift.{v₁, u₁, w'} C₁ M
inst_8 : HasShift.{v₂, u₂, w'} C₂ M
inst_9 : HasShift.{v₁', u₁', w'} D₁ M
inst_10 : HasShift.{v₂', u₂', w'} D₂ M
inst_11 : L₁.CommShift M
inst_12 : L₂.CommShift M
inst_13 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst_14 : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst_15 : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst_16 : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst_17 : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ≅ X₂
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁ ≅ Y₂
G : Functor.{v₁', v₂', u₁', u₂'} D₁ D₂
inst_18 : G.CommShift M
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
inst_19 : NatTrans.CommShift e.hom M
m : M
f : SmallShiftedHom W₁ X₁ Y₁ m
⊢ HasSmallLocalizedHom W₂ X₂ X₂

Tactic:
have := hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀.{w''} W₂ M X₂ X₂
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
D₁ : Type u₁'
inst_2 : Category.{v₁', u₁'} D₁
D₂ : Type u₂'
inst_3 : Category.{v₂', u₂'} D₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₁', u₁, u₁'} C₁ D₁
L₂ : Functor.{v₂, v₂', u₂, u₂'} C₂ D₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
M : Type w'
inst_6 : AddMonoid M
inst_7 : HasShift.{v₁, u₁, w'} C₁ M
inst_8 : HasShift.{v₂, u₂, w'} C₂ M
inst_9 : HasShift.{v₁', u₁', w'} D₁ M
inst_10 : HasShift.{v₂', u₂', w'} D₂ M
inst_11 : L₁.CommShift M
inst_12 : L₂.CommShift M
inst_13 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst_14 : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst_15 : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst_16 : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst_17 : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ≅ X₂
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁ ≅ Y₂
G : Functor.{v₁', v₂', u₁', u₂'} D₁ D₂
inst_18 : G.CommShift M
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
inst_19 : NatTrans.CommShift e.hom M
m : M
f : SmallShiftedHom W₁ X₁ Y₁ m
this : HasSmallLocalizedHom W₂ X₂ X₂
⊢ Eq.{v₂' + 1} (α := L₂.obj X₂ ⟶ L₂.obj (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor C₂ m) Y₂))
    ((SmallHom.equiv W₂ L₂ :
          (a : SmallHom W₂ X₂ ((shiftFunctor C₂ m).obj Y₂)) → L₂.obj X₂ ⟶ L₂.obj ((shiftFunctor C₂ m).obj Y₂))
        (Φ.smallShiftedHomMap (W₁ := W₁) (W₂ := W₂) eX eY f) :
      L₂.obj X₂ ⟶ L₂.obj (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor C₂ m) Y₂))
    (CategoryStruct.comp (Y := Functor.obj.{v₂', v₂', u₂', u₂'} (shiftFunctor D₂ m) (L₂.obj Y₂))
        (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (L₂.map eX.inv ≫ e.hom.app X₁))
          (ShiftedHom.comp
            (ShiftedHom.map
              (CategoryStruct.comp (Y := L₁.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C₁ m) Y₁))
                ((SmallHom.equiv W₁ L₁ :
                    (a : SmallHom W₁ X₁ ((shiftFunctor C₁ m).obj Y₁)) → L₁.obj X₁ ⟶ L₁.obj ((shiftFunctor C₁ m).obj Y₁))
                  f)
                (NatTrans.app (Iso.hom (Functor.commShiftIso L₁ m)) Y₁))
              G)
            (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Y₁ ≫ L₂.map eY.hom)) ⋯)
          ⋯)
        (NatTrans.app (Iso.inv (Functor.commShiftIso L₂ m)) Y₂) :
      L₂.obj X₂ ⟶ L₂.obj (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor C₂ m) Y₂))

Tactic:
(Φ.equiv_smallHomMap' L₁ L₂ _ _ G e f).trans ?_

Premises used: CategoryTheory.LocalizerMorphism.equiv_smallHomMap', CategoryTheory.LocalizerMorphism.smallShiftedHomMap, Eq.trans
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C₁ M
inst_4 : HasShift.{v₂, u₂, w'} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst_6 : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst_7 : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst_8 : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst_9 : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ≅ X₂
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁ ≅ Y₂
inst_10 : W₁.IsCompatibleWithShift M
inst_11 : W₂.IsCompatibleWithShift M
m : M
f : ShiftedHom X₁ Y₁ m
a :
  Eq (α := ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Y₂) m)
    ((SmallShiftedHom.equiv W₂ W₂.Q : (a : SmallShiftedHom W₂ X₂ Y₂ m) → ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Y₂) m)
        (smallShiftedHomMap.{w'', w, w', v₁, v₂, u₁, u₂} (W₁ := W₁) (W₂ := W₂) Φ eX eY (SmallShiftedHom.mk W₁ f)) :
      ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Y₂) m)
    ((SmallShiftedHom.equiv W₂ W₂.Q : (a : SmallShiftedHom W₂ X₂ Y₂ m) → ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Y₂) m)
        (SmallShiftedHom.mk W₂
          (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ eX.inv)
            (ShiftedHom.comp (f.map (Φ.functor (W₁ := W₁) (W₂ := W₂))) (ShiftedHom.mk₀ 0 ⋯ eY.hom) ⋯) ⋯)) :
      ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Y₂) m)
⊢ Eq.{w'' + 1} (α := SmallShiftedHom W₂ X₂ Y₂ m)
    (smallShiftedHomMap.{w'', w, w', v₁, v₂, u₁, u₂} (W₁ := W₁) (W₂ := W₂) Φ eX eY (SmallShiftedHom.mk W₁ f))
    (SmallShiftedHom.mk W₂
      (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ eX.inv)
        (ShiftedHom.comp (f.map (Φ.functor (W₁ := W₁) (W₂ := W₂))) (ShiftedHom.mk₀ 0 ⋯ eY.hom) ⋯) ⋯))

Tactic:
apply (SmallShiftedHom.equiv W₂ W₂.Q).injective

Premises used: CategoryTheory.MorphismProperty.Q, Equiv.injective, CategoryTheory.Localization.SmallShiftedHom.equiv
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C₁ M
inst_4 : HasShift.{v₂, u₂, w'} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst_6 : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst_7 : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst_8 : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst_9 : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ≅ X₂
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁ ≅ Y₂
inst_10 : W₁.IsCompatibleWithShift M
inst_11 : W₂.IsCompatibleWithShift M
m : M
f : ShiftedHom X₁ Y₁ m
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
⊢ Eq (α := ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Y₂) m)
    (W₂.Q.map eX.inv ≫
      e.hom.app X₁ ≫
        (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).map (W₁.Q.map f) ≫
          CategoryStruct.comp (Y :=
            (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).obj
              (W₁.Q.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C₁ m) Y₁)))
            ((Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).map
              (CategoryStruct.comp (Y := Functor.obj (shiftFunctor W₁.Localization m) (W₁.Q.obj Y₁))
                (NatTrans.app (Iso.hom (Functor.commShiftIso W₁.Q m)) Y₁)
                (NatTrans.app (Iso.inv (Functor.commShiftIso W₁.Q m)) Y₁)))
            (e.inv.app (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C₁ m) Y₁) ≫
              CategoryStruct.comp (Y :=
                W₂.Q.obj (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor C₂ m) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁)))
                (W₂.Q.map (NatTrans.app (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂)) m)) Y₁))
                (NatTrans.app (Iso.hom (Functor.commShiftIso W₂.Q m)) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁) ≫
                  Functor.map (shiftFunctor W₂.Localization m) (W₂.Q.map eY.hom))))
    (W₂.Q.map eX.inv ≫
      W₂.Q.map (Φ.functor (W₁ := W₁) (W₂ := W₂).map f) ≫
        CategoryStruct.comp (Y :=
          W₂.Q.obj (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor C₂ m) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁)))
          (W₂.Q.map (NatTrans.app (Iso.hom (Functor.commShiftIso (Φ.functor (W₁ := W₁) (W₂ := W₂)) m)) Y₁))
          (NatTrans.app (Iso.hom (Functor.commShiftIso W₂.Q m)) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁) ≫
            Functor.map (shiftFunctor W₂.Localization m) (W₂.Q.map eY.hom)))

Tactic:
simp [reassoc_of% (NatIso.naturality_2 e f)]

Premises used: CategoryTheory.NatIso.naturality_2
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C₁ M
inst_4 : HasShift.{v₂, u₂, w'} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
X₁ Y₁ : C₁
X₂ Y₂ : C₂
inst_6 : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst_7 : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst_8 : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst_9 : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ≅ X₂
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁ ≅ Y₂
inst_10 : W₁.IsCompatibleWithShift M
inst_11 : W₂.IsCompatibleWithShift M
m₀ : M
hm₀ : m₀ = 0
f : X₁ ⟶ Y₁
⊢ Eq.{w'' + 1} (α := SmallShiftedHom W₂ X₂ Y₂ m₀)
    (smallShiftedHomMap.{w'', w, w', v₁, v₂, u₁, u₂} (W₁ := W₁) (W₂ := W₂) Φ eX eY (SmallShiftedHom.mk₀ W₁ m₀ hm₀ f))
    (SmallShiftedHom.mk₀ W₂ m₀ hm₀ (eX.inv ≫ Φ.functor (W₁ := W₁) (W₂ := W₂).map f ≫ eY.hom))

Tactic:
simp [SmallShiftedHom.mk₀]

Premises used: CategoryTheory.Localization.SmallShiftedHom.mk₀
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C₁ M
inst_4 : HasShift.{v₂, u₂, w'} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
X₁ Y₁ Z₁ : C₁
X₂ Y₂ Z₂ : C₂
inst_6 : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst_7 : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst_8 : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst_9 : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ≅ X₂
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁ ≅ Y₂
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z₁ ≅ Z₂
inst_10 : W₁.IsCompatibleWithShift M
inst_11 : W₂.IsCompatibleWithShift M
inst_12 : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst_13 : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst_14 : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst_15 : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst_16 : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst_17 : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
a₁ :
  Eq (α := ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Z₂) c)
    ((SmallShiftedHom.equiv W₂ W₂.Q : (a : SmallShiftedHom W₂ X₂ Z₂ c) → ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Z₂) c)
        (Φ.smallShiftedHomMap (W₁ := W₁) (W₂ := W₂) eX eZ (f.comp (W := W₁) g h)) :
      ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Z₂) c)
    ((SmallShiftedHom.equiv W₂ W₂.Q : (a : SmallShiftedHom W₂ X₂ Z₂ c) → ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Z₂) c)
        (SmallShiftedHom.comp (W := W₂) (Φ.smallShiftedHomMap (W₁ := W₁) (W₂ := W₂) eX eY f)
          (Φ.smallShiftedHomMap (W₁ := W₁) (W₂ := W₂) eY eZ g) h) :
      ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Z₂) c)
⊢ Eq.{w'' + 1} (α := SmallShiftedHom W₂ X₂ Z₂ c)
    (Φ.smallShiftedHomMap (W₁ := W₁) (W₂ := W₂) eX eZ (f.comp (W := W₁) g h))
    (SmallShiftedHom.comp (W := W₂) (Φ.smallShiftedHomMap (W₁ := W₁) (W₂ := W₂) eX eY f)
      (Φ.smallShiftedHomMap (W₁ := W₁) (W₂ := W₂) eY eZ g) h)

Tactic:
apply (SmallShiftedHom.equiv W₂ W₂.Q).injective

Premises used: CategoryTheory.MorphismProperty.Q, Equiv.injective, CategoryTheory.Localization.SmallShiftedHom.equiv
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C₁ M
inst_4 : HasShift.{v₂, u₂, w'} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
X₁ Y₁ Z₁ : C₁
X₂ Y₂ Z₂ : C₂
inst_6 : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst_7 : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst_8 : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst_9 : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ≅ X₂
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁ ≅ Y₂
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z₁ ≅ Z₂
inst_10 : W₁.IsCompatibleWithShift M
inst_11 : W₂.IsCompatibleWithShift M
inst_12 : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst_13 : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst_14 : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst_15 : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst_16 : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst_17 : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
⊢ 0 + b + a = c

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C₁ M
inst_4 : HasShift.{v₂, u₂, w'} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
X₁ Y₁ Z₁ : C₁
X₂ Y₂ Z₂ : C₂
inst_6 : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst_7 : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst_8 : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst_9 : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ≅ X₂
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁ ≅ Y₂
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z₁ ≅ Z₂
inst_10 : W₁.IsCompatibleWithShift M
inst_11 : W₂.IsCompatibleWithShift M
inst_12 : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst_13 : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst_14 : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst_15 : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst_16 : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst_17 : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
⊢ b + a + 0 = c

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C₁ M
inst_4 : HasShift.{v₂, u₂, w'} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
X₁ Y₁ Z₁ : C₁
X₂ Y₂ Z₂ : C₂
inst_6 : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst_7 : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst_8 : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst_9 : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ≅ X₂
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁ ≅ Y₂
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z₁ ≅ Z₂
inst_10 : W₁.IsCompatibleWithShift M
inst_11 : W₂.IsCompatibleWithShift M
inst_12 : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst_13 : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst_14 : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst_15 : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst_16 : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst_17 : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
⊢ b + 0 + a = c

Tactic:
simpa
-- Module: Mathlib.CategoryTheory.Localization.SmallShiftedHom
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
M : Type w'
inst_2 : AddMonoid M
inst_3 : HasShift.{v₁, u₁, w'} C₁ M
inst_4 : HasShift.{v₂, u₂, w'} C₂ M
inst_5 : Φ.functor (W₁ := W₁) (W₂ := W₂).CommShift M
X₁ Y₁ Z₁ : C₁
X₂ Y₂ Z₂ : C₂
inst_6 : HasSmallLocalizedShiftedHom W₁ M X₁ Y₁
inst_7 : HasSmallLocalizedShiftedHom W₂ M X₂ X₂
inst_8 : HasSmallLocalizedShiftedHom W₂ M X₂ Y₂
inst_9 : HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂
eX : Φ.functor (W₁ := W₁) (W₂ := W₂).obj X₁ ≅ X₂
eY : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y₁ ≅ Y₂
eZ : Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z₁ ≅ Z₂
inst_10 : W₁.IsCompatibleWithShift M
inst_11 : W₂.IsCompatibleWithShift M
inst_12 : HasSmallLocalizedShiftedHom W₁ M Y₁ Z₁
inst_13 : HasSmallLocalizedShiftedHom W₂ M Z₂ Z₂
inst_14 : HasSmallLocalizedShiftedHom W₂ M Y₂ Z₂
inst_15 : HasSmallLocalizedShiftedHom W₁ M X₁ Z₁
inst_16 : HasSmallLocalizedShiftedHom W₁ M Z₁ Z₁
inst_17 : HasSmallLocalizedShiftedHom W₂ M X₂ Z₂
a b c : M
f : SmallShiftedHom W₁ X₁ Y₁ a
g : SmallShiftedHom W₁ Y₁ Z₁ b
h : b + a = c
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q :=
  CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)
⊢ b + 0 + 0 = b

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
W : MorphismProperty.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
inst_3 : L.IsLocalization W
inst_4 : L'.IsLocalization W
X : C
f : StructuredArrow (L.obj X) L
obtain :
  ∀ (Y : C) (f : L.obj X ⟶ L.obj Y),
    (fun (f : StructuredArrow (L'.obj X) L') ↦
          (StructuredArrow.mk (Y := f.right)
              (((homEquiv W L' L : Equiv.{v_3 + 1, v_2 + 1} (L'.obj X ⟶ L'.obj f.right) (L.obj X ⟶ L.obj f.right)) :
                  (a : L'.obj X ⟶ L'.obj f.right) → L.obj X ⟶ L.obj f.right)
                f.hom) :
            StructuredArrow (L.obj X) L))
        ((fun (f : StructuredArrow (L.obj X) L) ↦
            (StructuredArrow.mk (Y := f.right)
                (((homEquiv W L L' : Equiv.{v_2 + 1, v_3 + 1} (L.obj X ⟶ L.obj f.right) (L'.obj X ⟶ L'.obj f.right)) :
                    (a : L.obj X ⟶ L.obj f.right) → L'.obj X ⟶ L'.obj f.right)
                  f.hom) :
              StructuredArrow (L'.obj X) L'))
          (StructuredArrow.mk f)) =
      StructuredArrow.mk f
⊢ (fun (f : StructuredArrow (L'.obj X) L') ↦
        (StructuredArrow.mk (Y := f.right)
            (((homEquiv W L' L : Equiv.{v_3 + 1, v_2 + 1} (L'.obj X ⟶ L'.obj f.right) (L.obj X ⟶ L.obj f.right)) :
                (a : L'.obj X ⟶ L'.obj f.right) → L.obj X ⟶ L.obj f.right)
              f.hom) :
          StructuredArrow (L.obj X) L))
      ((fun (f : StructuredArrow (L.obj X) L) ↦
          (StructuredArrow.mk (Y := f.right)
              (((homEquiv W L L' : Equiv.{v_2 + 1, v_3 + 1} (L.obj X ⟶ L.obj f.right) (L'.obj X ⟶ L'.obj f.right)) :
                  (a : L.obj X ⟶ L.obj f.right) → L'.obj X ⟶ L'.obj f.right)
                f.hom) :
            StructuredArrow (L'.obj X) L'))
        f) =
    f

Tactic:
obtain ⟨Y, f, rfl⟩ := f.mk_surjective

Premises used: CategoryTheory.StructuredArrow.mk_surjective, rfl