awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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
inst_7 : HasSmallLocalizedShiftedHom W M X Y
f : X ⟶ Y
⊢ Eq (α := ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
    ((equiv W L : (a : SmallShiftedHom W X Y 0) → ShiftedHom (L.obj X) (L.obj Y) 0) (mk₀ W 0 ⋯ f) :
      ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
    (ShiftedHom.mk₀ 0 ⋯ (L.map f) : ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
have dsimp : Eq.{v₂ + 1} (α := ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
  (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w'} C (A := M) 0) Y))
      ((SmallHom.equiv W L : (a : SmallShiftedHom W X Y 0) → L.obj X ⟶ L.obj ((shiftFunctor C 0).obj Y))
        (mk W (ShiftedHom.mk₀ 0 sorry f)))
      (NatTrans.app (Iso.hom (Functor.commShiftIso L 0)) Y) :
    L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w'} D (A := M) 0) (L.obj Y))
  (ShiftedHom.mk₀ 0 sorry (L.map f) : ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
Tactic: dsimp [equiv, mk₀]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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
inst_7 : HasSmallLocalizedShiftedHom W M X Y
f : X ⟶ Y
⊢ Eq.{v₂ + 1} (α := ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w'} C (A := M) 0) Y))
        ((SmallHom.equiv W L : (a : SmallShiftedHom W X Y 0) → L.obj X ⟶ L.obj ((shiftFunctor C 0).obj Y))
          (mk W (ShiftedHom.mk₀ 0 ⋯ f)))
        (NatTrans.app (Iso.hom (Functor.commShiftIso L 0)) Y) :
      L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w'} D (A := M) 0) (L.obj Y))
    (ShiftedHom.mk₀ 0 ⋯ (L.map f) : ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
have erw : Eq (α := ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
  (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w'} C (A := M) 0) Y))
    (L.map f ≫ L.map (NatTrans.app (Iso.inv (shiftFunctorZero' C 0 sorry)) Y))
    (NatTrans.app (Iso.hom (Functor.commShiftIso L 0)) Y))
  (ShiftedHom.mk₀ 0 sorry (L.map f))
Tactic: erw [SmallHom.equiv_mk, Functor.map_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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
inst_7 : HasSmallLocalizedShiftedHom W M X Y
f : X ⟶ Y
⊢ Eq (α := ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
    (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w'} C (A := M) 0) Y))
      (L.map f ≫ L.map (NatTrans.app (Iso.inv (shiftFunctorZero' C 0 ⋯)) Y))
      (NatTrans.app (Iso.hom (Functor.commShiftIso L 0)) Y))
    (ShiftedHom.mk₀ 0 ⋯ (L.map f))
have dsimp : (L.map f ≫
      L.map
        (NatTrans.app (Iso.inv (shiftFunctorZero C M)) Y ≫
          𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor.{v₁, u₁, w'} C (A := M) 0) Y))) ≫
    NatTrans.app (Iso.hom (Functor.commShiftIso L 0)) Y =
  L.map f ≫
    NatTrans.app (Iso.inv (shiftFunctorZero D M)) (L.obj Y) ≫
      𝟙 (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor.{v₂, u₂, w'} D (A := M) 0) (L.obj Y))
Tactic: dsimp [equiv, mk₀, ShiftedHom.mk₀, shiftFunctorZero']
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (hypothesis)
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
inst_7 : HasSmallLocalizedShiftedHom W M Y X
inst_8 : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
hf : W f
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj Y) (L.obj X) m₀)
    ((equiv W L : (a : SmallShiftedHom W Y X m₀) → ShiftedHom (L.obj Y) (L.obj X) m₀) (mk₀Inv (W := W) m₀ hm₀ f hf) :
      ShiftedHom (L.obj Y) (L.obj X) m₀)
    (ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv : ShiftedHom (L.obj Y) (L.obj X) m₀)
have hf' : W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m₀) X) (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f)
Tactic: have hf' : W ((shiftFunctorZero' C m₀ hm₀).hom.app X ≫ f) :=
    MorphismProperty.RespectsIso.precomp _ _ _ hf
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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
inst_7 : HasSmallLocalizedShiftedHom W M Y X
inst_8 : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
hf : W f
hf' :
  W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m₀) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f)
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj Y) (L.obj X) m₀)
    ((equiv W L : (a : SmallShiftedHom W Y X m₀) → ShiftedHom (L.obj Y) (L.obj X) m₀) (mk₀Inv (W := W) m₀ hm₀ f hf) :
      ShiftedHom (L.obj Y) (L.obj X) m₀)
    (ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv : ShiftedHom (L.obj Y) (L.obj X) m₀)
have refine : Eq (α := L.obj Y ⟶ (L ⋙ shiftFunctor D m₀).obj X)
  ((isoOfHom L W (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f) hf').inv ≫
    Iso.hom (Iso.app (Functor.commShiftIso L m₀) X))
  (ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv)
Tactic: refine (SmallHom.equiv_mkInv L _ hf' =≫ _).trans ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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
inst_7 : HasSmallLocalizedShiftedHom W M Y X
inst_8 : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
hf : W f
hf' :
  W (X := Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m₀) X)
    (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f)
⊢ Eq (α := L.obj Y ⟶ (L ⋙ shiftFunctor D m₀).obj X)
    ((isoOfHom L W (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f) hf').inv ≫
      Iso.hom (Iso.app (Functor.commShiftIso L m₀) X))
    (ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv)
have rw : Eq (α := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C m₀) X) ⟶ (L ⋙ shiftFunctor D m₀).obj X)
  (Iso.hom (Iso.app (Functor.commShiftIso L m₀) X))
  ((isoOfHom L W (NatTrans.app (Iso.hom (shiftFunctorZero' C m₀ hm₀)) X ≫ f) hf').hom ≫
    ShiftedHom.mk₀ m₀ hm₀ (isoOfHom L W f hf).inv)
Tactic: rw [← cancel_epi (isoOfHom L W _ hf').hom, Iso.hom_inv_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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
inst_5 : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst_6 : HasSmallLocalizedShiftedHom W M X Y
inst_7 : HasSmallLocalizedShiftedHom W M X Z
inst_8 : HasSmallLocalizedShiftedHom W M X T
inst_9 : HasSmallLocalizedShiftedHom W M Y Z
inst_10 : HasSmallLocalizedShiftedHom W M Y T
inst_11 : HasSmallLocalizedShiftedHom W M Z T
inst_12 : HasSmallLocalizedShiftedHom W M Z Z
inst_13 : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ a₃ + a₁₂ = a
have rw : a₃ + (a₂ + a₁) = a
Tactic: rw [← h₁₂, ← add_assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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
inst_5 : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst_6 : HasSmallLocalizedShiftedHom W M X Y
inst_7 : HasSmallLocalizedShiftedHom W M X Z
inst_8 : HasSmallLocalizedShiftedHom W M X T
inst_9 : HasSmallLocalizedShiftedHom W M Y Z
inst_10 : HasSmallLocalizedShiftedHom W M Y T
inst_11 : HasSmallLocalizedShiftedHom W M Z T
inst_12 : HasSmallLocalizedShiftedHom W M Z Z
inst_13 : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
rw : a₃ + (a₂ + a₁) = a
rw₁ : a₃ + a₂ + a₁ = a
⊢ a₃ + a₁₂ = a
have rw₂ : a = a
Tactic: rw [← h₁₂, ← add_assoc, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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
inst_5 : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst_6 : HasSmallLocalizedShiftedHom W M X Y
inst_7 : HasSmallLocalizedShiftedHom W M X Z
inst_8 : HasSmallLocalizedShiftedHom W M X T
inst_9 : HasSmallLocalizedShiftedHom W M Y Z
inst_10 : HasSmallLocalizedShiftedHom W M Y T
inst_11 : HasSmallLocalizedShiftedHom W M Z T
inst_12 : HasSmallLocalizedShiftedHom W M Z Z
inst_13 : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h rw : a₃ + a₂ + a₁ = a
⊢ a₂₃ + a₁ = a
have rw₁ : a = a
Tactic: rw [← h₂₃, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
W : MorphismProperty.{v₁, u₁} C
M : Type w'
inst_1 : AddMonoid M
inst_2 : HasShift.{v₁, u₁, w'} C M
inst_3 : W.IsCompatibleWithShift M
X Y Z T : C
a₁ a₂ a₃ a₁₂ a₂₃ a : M
inst_4 : HasSmallLocalizedShiftedHom W M X Y
inst_5 : HasSmallLocalizedShiftedHom W M X Z
inst_6 : HasSmallLocalizedShiftedHom W M X T
inst_7 : HasSmallLocalizedShiftedHom W M Y Z
inst_8 : HasSmallLocalizedShiftedHom W M Y T
inst_9 : HasSmallLocalizedShiftedHom W M Z T
inst_10 : HasSmallLocalizedShiftedHom W M Z Z
inst_11 : HasSmallLocalizedShiftedHom W M T T
α : SmallShiftedHom W X Y a₁
β : SmallShiftedHom W Y Z a₂
γ : SmallShiftedHom W Z T a₃
h₁₂ : a₂ + a₁ = a₁₂
h₂₃ : a₃ + a₂ = a₂₃
h : a₃ + a₂ + a₁ = a
⊢ Eq (α := SmallShiftedHom W X T a) (comp (W := W) (α.comp (W := W) β h₁₂) γ ⋯)
    (α.comp (W := W) (β.comp (W := W) γ h₂₃) ⋯)
have a₄ : Eq (α := ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
  ((equiv W W.Q : (a_1 : SmallShiftedHom W X T a) → ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
      (comp (W := W) (α.comp (W := W) β h₁₂) γ sorry) :
    ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
  ((equiv W W.Q : (a_1 : SmallShiftedHom W X T a) → ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
      (α.comp (W := W) (β.comp (W := W) γ h₂₃) sorry) :
    ShiftedHom (W.Q.obj X) (W.Q.obj T) a)
Tactic: apply (equiv W W.Q).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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
X Y : C
inst_5 : HasSmallLocalizedShiftedHom W M X Y
inst_6 : HasSmallLocalizedShiftedHom W M Y Y
inst_7 : HasSmallLocalizedShiftedHom W M Y X
inst_8 : W.IsCompatibleWithShift M
inst_9 : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
⊢ m₀ + m₀ = m₀
have subst : HAdd.hAdd (α := M) 0 0 = 0
Tactic: subst hm₀
Cleared hypotheses: m₀, hm₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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
X Y : C
inst_5 : HasSmallLocalizedShiftedHom W M X Y
inst_6 : HasSmallLocalizedShiftedHom W M X X
inst_7 : HasSmallLocalizedShiftedHom W M Y X
inst_8 : W.IsCompatibleWithShift M
inst_9 : W.RespectsIso
m₀ : M
hm₀ : m₀ = 0
f : Y ⟶ X
hf : W f
⊢ m₀ + m₀ = m₀
have subst : HAdd.hAdd (α := M) 0 0 = 0
Tactic: subst hm₀
Cleared hypotheses: m₀, hm₀
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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} (α := ShiftedHom (L.obj X) (L.obj Y) m)
    ((equiv W L : (a : SmallShiftedHom W X Y m) → ShiftedHom (L.obj X) (L.obj Y) m)
        ((chgUniv (W := W) : (a : SmallShiftedHom W X Y m) → SmallShiftedHom W X Y m) e) :
      ShiftedHom (L.obj X) (L.obj Y) m)
    ((equiv W L : (a : SmallShiftedHom W X Y m) → ShiftedHom (L.obj X) (L.obj Y) m) e :
      ShiftedHom (L.obj X) (L.obj Y) m)
have dsimp : 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: dsimp [equiv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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} (α := 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))
have 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))
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (hypothesis)
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
⊢ Eq.{v₂' + 1} (α := ShiftedHom (L₂.obj X₂) (L₂.obj Y₂) m)
    ((SmallShiftedHom.equiv W₂ L₂ : (a : SmallShiftedHom W₂ X₂ Y₂ m) → ShiftedHom (L₂.obj X₂) (L₂.obj Y₂) m)
        (Φ.smallShiftedHomMap (W₁ := W₁) (W₂ := W₂) eX eY f) :
      ShiftedHom (L₂.obj X₂) (L₂.obj Y₂) m)
    (ShiftedHom.comp (ShiftedHom.mk₀ 0 ⋯ (L₂.map eX.inv ≫ e.hom.app X₁))
        (ShiftedHom.comp
          (ShiftedHom.map
            ((SmallShiftedHom.equiv W₁ L₁ : (a : SmallShiftedHom W₁ X₁ Y₁ m) → ShiftedHom (L₁.obj X₁) (L₁.obj Y₁) m) f)
            G)
          (ShiftedHom.mk₀ 0 ⋯ (e.inv.app Y₁ ≫ L₂.map eY.hom)) ⋯)
        ⋯ :
      ShiftedHom (L₂.obj X₂) (L₂.obj Y₂) m)
have this : HasSmallLocalizedHom W₂ X₂ X₂
Tactic: have := hasSmallLocalizedHom_of_hasSmallLocalizedShiftedHom₀.{w''} W₂ M X₂ X₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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
⊢ 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) ⋯) ⋯))
have 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 sorry eX.inv)
          (ShiftedHom.comp (f.map (Φ.functor (W₁ := W₁) (W₂ := W₂))) (ShiftedHom.mk₀ 0 sorry eY.hom) sorry) sorry)) :
    ShiftedHom (W₂.Q.obj X₂) (W₂.Q.obj Y₂) m)
Tactic: apply (SmallShiftedHom.equiv W₂ W₂.Q).injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallShiftedHom (goal)
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
⊢ 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)
have 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)
Tactic: apply (SmallShiftedHom.equiv W₂ W₂.Q).injective