awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (hypothesis)
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
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'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
this_4 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'
⊢ Eq.{w' + 1} (α := SmallHom W₂ X' Z') (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eX eZ (f.comp (W := W₁) g))
    (SmallHom.comp (W := W₂) (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eX eY f)
      (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eY eZ g))
have this₁ : HasSmallLocalizedHom W₂ Y' (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
Tactic: have := hasSmallLocalizedHom_of_isos.{w'} W₂ (Iso.refl Y') eY.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (hypothesis)
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
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'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
this_4 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
this_5 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'
this : HasSmallLocalizedHom W₂ Y' (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
⊢ Eq.{w' + 1} (α := SmallHom W₂ X' Z') (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eX eZ (f.comp (W := W₁) g))
    (SmallHom.comp (W := W₂) (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eX eY f)
      (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eY eZ g))
have this₁ : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
Tactic: have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm eY.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
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'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
this_4 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
this_5 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'
this_6 : HasSmallLocalizedHom W₂ Y' (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
⊢ Eq.{w' + 1} (α := SmallHom W₂ X' Z') (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eX eZ (f.comp (W := W₁) g))
    (SmallHom.comp (W := W₂) (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eX eY f)
      (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eY eZ g))
have simp : Eq.{w' + 1} (α := SmallHom W₂ X' Z')
  (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eX.inv)
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f)
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))
  (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eX.inv)
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f)
      (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom)
        (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.inv)
          (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))))
Tactic: simp only [smallHomMap', smallHomMap_comp, SmallHom.comp_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
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'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
this_4 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
this_5 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'
this_6 : HasSmallLocalizedHom W₂ Y' (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
⊢ Eq.{w' + 1} (α := SmallHom W₂ X' Z')
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eX.inv)
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f)
        (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eX.inv)
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f)
        (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom)
          (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.inv)
            (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))))
have e_β : Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
  (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
  (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom)
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.inv)
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))
Tactic: congr 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
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'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
this_4 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
this_5 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'
this_6 : HasSmallLocalizedHom W₂ Y' (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
⊢ Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom)
      (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.inv)
        (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))
have e_β : Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
  (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
  (SmallHom.comp (W := W₂) (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom) (SmallHom.mk W₂ eY.inv))
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom)))
Tactic: rw [← SmallHom.comp_assoc, SmallHom.mk_comp_mk, eY.hom_inv_id, SmallHom.mk_id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
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'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
this_4 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
this_5 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'
this_6 : HasSmallLocalizedHom W₂ Y' (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
e_β :
  Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
    (SmallHom.comp (W := W₂) (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom) (SmallHom.mk W₂ eY.inv))
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom)))
⊢ Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom)
      (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.inv)
        (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))
have e_β₁ : Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
  (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
  (SmallHom.comp (W := W₂) (SmallHom.mk W₂ (eY.hom ≫ eY.inv))
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom)))
Tactic: rw [← SmallHom.comp_assoc, SmallHom.mk_comp_mk, eY.hom_inv_id, SmallHom.mk_id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.SmallHom (goal)
Goal:
C₁ : Type u₁
inst : Category.{v₁, u₁} C₁
W₁ : MorphismProperty.{v₁, u₁} C₁
C₂ : Type u₂
inst_1 : Category.{v₂, u₂} C₂
W₂ : MorphismProperty.{v₂, u₂} C₂
Φ : LocalizerMorphism W₁ W₂
X Y Z : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₁ Y Z
inst_4 : HasSmallLocalizedHom W₁ X Z
X' Y' Z' : C₂
inst_5 : HasSmallLocalizedHom W₂ X' X'
inst_6 : HasSmallLocalizedHom W₂ Y' Y'
inst_7 : HasSmallLocalizedHom W₂ Z' Z'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ Y' Z'
inst_10 : HasSmallLocalizedHom W₂ X' Z'
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'
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
this_1 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this_2 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
this_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) Z'
this_4 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
this_5 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'
this_6 : HasSmallLocalizedHom W₂ Y' (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
e_β :
  Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
    (SmallHom.comp (W := W₂) (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom) (SmallHom.mk W₂ eY.inv))
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom)))
e_β₁ :
  Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ (eY.hom ≫ eY.inv))
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom)))
⊢ Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
    (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.hom)
      (SmallHom.comp (W := W₂) (SmallHom.mk W₂ eY.inv)
        (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))))
have e_β₂ : Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z')
  (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom))
  (SmallHom.comp (W := W₂) (SmallHom.mk W₂ (𝟙 (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)))
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g) (SmallHom.mk W₂ eZ.hom)))
Tactic: rw [← SmallHom.comp_assoc, SmallHom.mk_comp_mk, eY.hom_inv_id, SmallHom.mk_id_comp]
-- 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
⊢ (∀ (a b : M),
      HasSmallLocalizedHom W (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) X)
        (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) Y)) ↔
    ∀ (a b : M),
      Small.{w, v₂}
        (Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj X) ⟶
          Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D b) (L.obj Y))
have eq : ∀ (a b : M),
  Small.{w, v₂} ((shiftFunctor C a ⋙ L).obj X ⟶ (shiftFunctor C b ⋙ L).obj Y) ↔
    Small.{w, v₂} ((L ⋙ shiftFunctor D a).obj X ⟶ (L ⋙ shiftFunctor D b).obj Y)
Tactic: have eq := fun (a b : M) ↦ small_congr.{w}
    (Iso.homCongr ((L.commShiftIso a).app X) ((L.commShiftIso b).app Y))
-- 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 : W.IsCompatibleWithShift M
a : M
inst_8 : HasSmallLocalizedShiftedHom W M X Y
inst_9 : HasSmallLocalizedShiftedHom W M Y Y
f : SmallShiftedHom W X Y a
n a' : M
h : a + n = a'
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X)) (L.obj Y) a')
    ((equiv W L :
          (a : SmallShiftedHom W ((shiftFunctor C n).obj X) Y a') →
            ShiftedHom (L.obj ((shiftFunctor C n).obj X)) (L.obj Y) a')
        (f.shift (W := W) n a' h) :
      ShiftedHom (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X)) (L.obj Y) a')
    (CategoryStruct.comp (Y := (L ⋙ shiftFunctor D n).obj X) (NatTrans.app (Iso.hom (Functor.commShiftIso L n)) X)
        (Functor.map (shiftFunctor D n)
            ((equiv W L : (a_1 : SmallShiftedHom W X Y a) → ShiftedHom (L.obj X) (L.obj Y) a) f) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D a n a' h)) (L.obj Y)) :
      (shiftFunctor C n ⋙ L).obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a') (L.obj Y))
have dsimp : Eq.{v₂ + 1} (α := ShiftedHom (L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X)) (L.obj Y) a')
  (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a') Y))
      ((SmallHom.equiv W L :
          (a : SmallShiftedHom W ((shiftFunctor C n).obj X) Y a') →
            L.obj ((shiftFunctor C n).obj X) ⟶ L.obj ((shiftFunctor C a').obj Y))
        (f.shift (W := W) n a' h))
      (NatTrans.app (Iso.hom (Functor.commShiftIso L a')) Y) :
    L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X) ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a') (L.obj Y))
  (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D n) (L.obj X))
      (NatTrans.app (Iso.hom (Functor.commShiftIso L n)) X)
      (Functor.map (shiftFunctor D n)
          (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y))
            ((SmallHom.equiv W L : (a_1 : SmallShiftedHom W X Y a) → L.obj X ⟶ L.obj ((shiftFunctor C a).obj Y)) f)
            (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) Y)) ≫
        NatTrans.app (Iso.inv (shiftFunctorAdd' D a n a' h)) (L.obj Y)) :
    L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C n) X) ⟶
      Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a') (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 Z : C
inst_7 : W.IsCompatibleWithShift M
inst_8 : HasSmallLocalizedShiftedHom W M X Y
inst_9 : HasSmallLocalizedShiftedHom W M Y Z
inst_10 : HasSmallLocalizedShiftedHom W M X Z
inst_11 : HasSmallLocalizedShiftedHom W M Z Z
a b c : M
f : SmallShiftedHom W X Y a
g : SmallShiftedHom W Y Z b
h : b + a = c
⊢ Eq.{v₂ + 1} (α := ShiftedHom (L.obj X) (L.obj Z) c)
    ((equiv W L : (a : SmallShiftedHom W X Z c) → ShiftedHom (L.obj X) (L.obj Z) c) (f.comp (W := W) g h) :
      ShiftedHom (L.obj X) (L.obj Z) c)
    (ShiftedHom.comp (Y := L.obj Y) ((equiv W L : (a_1 : SmallShiftedHom W X Y a) → ShiftedHom (L.obj X) (L.obj Y) a) f)
        ((equiv W L : (a : SmallShiftedHom W Y Z b) → ShiftedHom (L.obj Y) (L.obj Z) b) g) h :
      ShiftedHom (L.obj X) (L.obj Z) c)
have dsimp : Eq.{v₂ + 1} (α := ShiftedHom (L.obj X) (L.obj Z) c)
  (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C c) Z))
      ((SmallHom.equiv W L : (a : SmallShiftedHom W X Z c) → L.obj X ⟶ L.obj ((shiftFunctor C c).obj Z))
        (SmallHom.comp (W := W) f (g.shift (W := W) a c h)))
      (NatTrans.app (Iso.hom (Functor.commShiftIso L c)) Z) :
    L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D c) (L.obj Z))
  (CategoryStruct.comp (Y := Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj Y))
      (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C a) Y))
          ((SmallHom.equiv W L : (a_1 : SmallShiftedHom W X Y a) → L.obj X ⟶ L.obj ((shiftFunctor C a).obj Y)) f)
          (NatTrans.app (Iso.hom (Functor.commShiftIso L a)) Y) :
        L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj Y))
      (Functor.map (shiftFunctor D a)
            (CategoryStruct.comp (Y := L.obj (Functor.obj.{v₁, v₁, u₁, u₁} (shiftFunctor C b) Z))
              ((SmallHom.equiv W L : (a : SmallShiftedHom W Y Z b) → L.obj Y ⟶ L.obj ((shiftFunctor C b).obj Z)) g)
              (NatTrans.app (Iso.hom (Functor.commShiftIso L b)) Z)) ≫
          NatTrans.app (Iso.inv (shiftFunctorAdd' D b a c h)) (L.obj Z) :
        Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D a) (L.obj Y) ⟶
          Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D c) (L.obj Z)) :
    L.obj X ⟶ Functor.obj.{v₂, v₂, u₂, u₂} (shiftFunctor D c) (L.obj Z))
Tactic: dsimp [comp, equiv, ShiftedHom.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
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
⊢ 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₀) (mk₀ W m₀ hm₀ f) :
      ShiftedHom (L.obj X) (L.obj Y) m₀)
    (ShiftedHom.mk₀ m₀ hm₀ (L.map f) : ShiftedHom (L.obj X) (L.obj Y) m₀)
have subst : 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 sorry f) :
    ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
  (ShiftedHom.mk₀ 0 sorry (L.map f) : ShiftedHom.{v₂, u₂, w'} (M := M) (L.obj X) (L.obj Y) 0)
Tactic: subst hm₀
Cleared hypotheses: m₀, hm₀