awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₂
D₁ : Type u₃
inst_2 : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
X Y : C₁
inst_6 : HasSmallLocalizedHom W₁ X Y
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
G : Functor.{v₃, v₄, u₃, u₄} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
f : SmallHom W₁ X Y
⊢ (SmallHom.equiv W₂ L₂ :
        (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) → L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y))
      (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f) =
    e.hom.app X ≫ G.map ((SmallHom.equiv W₁ L₁ : (a : SmallHom W₁ X Y) → L₁.obj X ⟶ L₁.obj Y) f) ≫ e.inv.app Y
have obtain : ∀ (g : W₁.Q.obj X ⟶ W₁.Q.obj Y),
  (SmallHom.equiv W₂ L₂ :
        (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) → L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y))
      (smallHomMap.{w, w', v₁, v₂, u₁, u₂} (W₁ := W₁) (W₂ := W₂) Φ
        ((Equiv.symm (SmallHom.equiv W₁ W₁.Q) : (a : W₁.Q.obj X ⟶ W₁.Q.obj Y) → SmallHom W₁ X Y) g)) =
    e.hom.app X ≫
      G.map
          ((SmallHom.equiv W₁ L₁ : (a : SmallHom W₁ X Y) → L₁.obj X ⟶ L₁.obj Y)
            ((Equiv.symm (SmallHom.equiv W₁ W₁.Q) : (a : W₁.Q.obj X ⟶ W₁.Q.obj Y) → SmallHom W₁ X Y) g)) ≫
        e.inv.app Y
Tactic: obtain ⟨g, rfl⟩ := (SmallHom.equiv W₁ W₁.Q).symm.surjective f
Cleared hypotheses: f
-- 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₂
D₁ : Type u₃
inst_2 : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
X Y : C₁
inst_6 : HasSmallLocalizedHom W₁ X Y
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
G : Functor.{v₃, v₄, u₃, u₄} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X ⟶ W₁.Q.obj Y
⊢ (SmallHom.equiv W₂ L₂ :
        (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) → L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y))
      (smallHomMap.{w, w', v₁, v₂, u₁, u₂} (W₁ := W₁) (W₂ := W₂) Φ
        ((Equiv.symm (SmallHom.equiv W₁ W₁.Q) : (a : W₁.Q.obj X ⟶ W₁.Q.obj Y) → SmallHom W₁ X Y) g)) =
    e.hom.app X ≫
      G.map
          ((SmallHom.equiv W₁ L₁ : (a : SmallHom W₁ X Y) → L₁.obj X ⟶ L₁.obj Y)
            ((Equiv.symm (SmallHom.equiv W₁ W₁.Q) : (a : W₁.Q.obj X ⟶ W₁.Q.obj Y) → SmallHom W₁ X Y) g)) ≫
        e.inv.app Y
have simp : (SmallHom.equiv W₂ L₂ :
      (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) → L₂.obj (Φ.functor.obj X) ⟶ L₂.obj (Φ.functor.obj Y))
    ((Equiv.symm (SmallHom.equiv W₂ W₂.Q) :
        (a : W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Y)) → SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y))
      ((Iso.homCongr
              (Iso.app
                (Iso.symm
                  (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
                    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
                X)
              (Iso.app
                (Iso.symm
                  (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
                    (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
                Y) :
            (a : (W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q).obj X ⟶ (W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q).obj Y) →
              (Φ.functor ⋙ W₂.Q).obj X ⟶ (Φ.functor ⋙ W₂.Q).obj Y)
          ((Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).map g) :
        (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).obj X ⟶ (Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q).obj Y)) =
  e.hom.app X ≫
    G.map
        ((SmallHom.equiv W₁ L₁ : (a : SmallHom W₁ X Y) → L₁.obj X ⟶ L₁.obj Y)
          ((Equiv.symm (SmallHom.equiv W₁ W₁.Q) : (a : W₁.Q.obj X ⟶ W₁.Q.obj Y) → SmallHom W₁ X Y) g)) ≫
      e.inv.app Y
Tactic: simp only [smallHomMap, Equiv.apply_symm_apply]
-- 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₂
D₁ : Type u₃
inst_2 : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
X Y : C₁
inst_6 : HasSmallLocalizedHom W₁ X Y
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
G : Functor.{v₃, v₄, u₃, u₄} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X ⟶ W₁.Q.obj Y
G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
β : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q G'
E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor
α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor
α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
⊢ α₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
      E₂.map
          ((Iso.homCongr
                (Iso.app
                  (Iso.symm
                    (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
                      (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
                  X)
                (Iso.app
                  (Iso.symm
                    (CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q
                      (Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q)))
                  Y) :
              (a : (W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q).obj X ⟶ (W₁.Q ⋙ Φ.localizedFunctor W₁.Q W₂.Q).obj Y) →
                (Φ.functor ⋙ W₂.Q).obj X ⟶ (Φ.functor ⋙ W₂.Q).obj Y)
            ((Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q).map g)) ≫
        α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) =
    e.hom.app X ≫ G.map (α₁.inv.app X ≫ E₁.map g ≫ α₁.hom.app Y) ≫ e.inv.app Y
have change : α₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
    E₂.map (β.hom.app X ≫ G'.map g ≫ β.inv.app Y) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) =
  e.hom.app X ≫ G.map (α₁.inv.app X ≫ E₁.map g ≫ α₁.hom.app Y) ≫ e.inv.app Y
Tactic: change α₂.inv.app _ ≫ E₂.map (β.hom.app X ≫ G'.map g ≫ β.inv.app Y) ≫ _ = _
-- 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₂
D₁ : Type u₃
inst_2 : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
X Y : C₁
inst_6 : HasSmallLocalizedHom W₁ X Y
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
G : Functor.{v₃, v₄, u₃, u₄} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X ⟶ W₁.Q.obj Y
G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
β : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q G'
E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor
α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor
α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
γ : G' ⋙ E₂ ≅ E₁ ⋙ G :=
  liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) (G' ⋙ E₂) (E₁ ⋙ G)
    ((W₁.Q.associator G' E₂).symm ≪≫
      Functor.isoWhiskerRight β.symm E₂ ≪≫
        Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂ ≪≫
          Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft α₂ ≪≫
            e ≪≫ Functor.isoWhiskerRight α₁.symm G ≪≫ W₁.Q.associator E₁ G)
⊢ α₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
      E₂.map (β.hom.app X ≫ G'.map g ≫ β.inv.app Y) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) =
    e.hom.app X ≫ G.map (α₁.inv.app X ≫ E₁.map g ≫ α₁.hom.app Y) ≫ e.inv.app Y
have hγ : ∀ (X : C₁),
  γ.hom.app (W₁.Q.obj X) =
    E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫ e.hom.app X ≫ G.map (α₁.inv.app X)
Tactic: have hγ : ∀ (X : C₁), γ.hom.app (W₁.Q.obj X) =
      E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor.obj X) ≫
        e.hom.app X ≫ G.map (α₁.inv.app X) := fun X ↦ by
    simp [γ, id_comp, comp_id]
-- 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₂
D₁ : Type u₃
inst_2 : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
X Y : C₁
inst_6 : HasSmallLocalizedHom W₁ X Y
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
G : Functor.{v₃, v₄, u₃, u₄} D₁ D₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
g : W₁.Q.obj X ⟶ W₁.Q.obj Y
G' : W₁.Localization ⥤ W₂.Localization := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) W₁.Q W₂.Q
β : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ W₂.Q ≅ W₁.Q ⋙ G' := CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) W₁.Q W₂.Q G'
E₁ : W₁.Localization ⥤ D₁ := (uniq W₁.Q L₁ W₁).functor
α₁ : W₁.Q ⋙ E₁ ≅ L₁ := compUniqFunctor W₁.Q L₁ W₁
E₂ : W₂.Localization ⥤ D₂ := (uniq W₂.Q L₂ W₂).functor
α₂ : W₂.Q ⋙ E₂ ≅ L₂ := compUniqFunctor W₂.Q L₂ W₂
γ : G' ⋙ E₂ ≅ E₁ ⋙ G :=
  liftNatIso W₁.Q W₁ (W₁.Q ⋙ G' ⋙ E₂) (W₁.Q ⋙ E₁ ⋙ G) (G' ⋙ E₂) (E₁ ⋙ G)
    ((W₁.Q.associator G' E₂).symm ≪≫
      Functor.isoWhiskerRight β.symm E₂ ≪≫
        Φ.functor (W₁ := W₁) (W₂ := W₂).associator W₂.Q E₂ ≪≫
          Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft α₂ ≪≫
            e ≪≫ Functor.isoWhiskerRight α₁.symm G ≪≫ W₁.Q.associator E₁ G)
hγ :
  ∀ (X : C₁),
    γ.hom.app (W₁.Q.obj X) =
      E₂.map (β.inv.app X) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫ e.hom.app X ≫ G.map (α₁.inv.app X)
⊢ α₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
      E₂.map (β.hom.app X ≫ G'.map g ≫ β.inv.app Y) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) =
    e.hom.app X ≫ G.map (α₁.inv.app X ≫ E₁.map g ≫ α₁.hom.app Y) ≫ e.inv.app Y
have simp : γ.hom.app (W₁.Q.obj X) ≫
    G.map (α₁.hom.app X) ≫
      e.inv.app X ≫
        α₂.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
          E₂.map (β.hom.app X) ≫
            (G' ⋙ E₂).map g ≫ E₂.map (β.inv.app Y) ≫ α₂.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) =
  (G' ⋙ E₂).map g ≫ γ.hom.app (W₁.Q.obj Y) ≫ G.map (α₁.hom.app Y) ≫ e.inv.app Y
Tactic: simp only [Functor.map_comp, ← NatIso.naturality_1 γ, ← Functor.comp_map,
    ← cancel_epi (e.inv.app X), ← cancel_epi (G.map (α₁.hom.app X)),
    ← cancel_epi (γ.hom.app (W₁.Q.obj X)), assoc, Iso.inv_hom_id_app_assoc,
    ← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.map_id, id_comp,
    Iso.hom_inv_id_app_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 : C₁
inst_2 : HasSmallLocalizedHom W₁ X Y
inst_3 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
f : X ⟶ Y
⊢ Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y))
    (smallHomMap.{w, w', v₁, v₂, u₁, u₂} (W₁ := W₁) (W₂ := W₂) Φ (SmallHom.mk W₁ f))
    (SmallHom.mk W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).map f))
have a : Eq (α := W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y))
  ((SmallHom.equiv W₂ W₂.Q :
        (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) → W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Y))
      (smallHomMap.{w, w', v₁, v₂, u₁, u₂} (W₁ := W₁) (W₂ := W₂) Φ (SmallHom.mk W₁ f)) :
    W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y))
  ((SmallHom.equiv W₂ W₂.Q :
        (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Y)) → W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Y))
      (SmallHom.mk W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).map f)) :
    W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y))
Tactic: apply (SmallHom.equiv W₂ W₂.Q).injective
-- 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
inst_5 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
inst_6 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
inst_7 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
f : SmallHom W₁ X Y
g : SmallHom W₁ Y Z
⊢ Eq.{w' + 1} (α := SmallHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z))
    (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) (f.comp (W := W₁) g))
    (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g))
have a : Eq (α := W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z))
  ((SmallHom.equiv W₂ W₂.Q :
        (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)) → W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Z))
      (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) (f.comp (W := W₁) g)) :
    W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z))
  ((SmallHom.equiv W₂ W₂.Q :
        (a : SmallHom W₂ (Φ.functor.obj X) (Φ.functor.obj Z)) → W₂.Q.obj (Φ.functor.obj X) ⟶ W₂.Q.obj (Φ.functor.obj Z))
      (SmallHom.comp (W := W₂) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) f) (Φ.smallHomMap (W₁ := W₁) (W₂ := W₂) g)) :
    W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ⟶ W₂.Q.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z))
Tactic: apply (SmallHom.equiv W₂ W₂.Q).injective
-- 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₂
D₁ : Type u₃
inst_2 : Category.{v₃, u₃} D₁
D₂ : Type u₄
inst_3 : Category.{v₄, u₄} D₂
Φ : LocalizerMorphism W₁ W₂
L₁ : Functor.{v₁, v₃, u₁, u₃} C₁ D₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v₂, v₄, u₂, u₄} C₂ D₂
inst_5 : L₂.IsLocalization W₂
X Y : C₁
inst_6 : HasSmallLocalizedHom W₁ X Y
X' Y' : C₂
inst_7 : HasSmallLocalizedHom W₂ X' X'
inst_8 : HasSmallLocalizedHom W₂ X' Y'
inst_9 : HasSmallLocalizedHom W₂ 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₂
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G
f : SmallHom W₁ X Y
⊢ (SmallHom.equiv W₂ L₂ : (a : SmallHom W₂ X' Y') → L₂.obj X' ⟶ L₂.obj Y')
      (Φ.smallHomMap' (W₁ := W₁) (W₂ := W₂) eX eY f) =
    L₂.map eX.inv ≫
      e.hom.app X ≫
        G.map ((SmallHom.equiv W₁ L₁ : (a : SmallHom W₁ X Y) → L₁.obj X ⟶ L₁.obj Y) f) ≫ e.inv.app Y ≫ L₂.map eY.hom
have this : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Y'
Tactic: have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm (Iso.refl Y')
-- 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
⊢ 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 X) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)
Tactic: have := hasSmallLocalizedHom_of_isos.{w'} W₂ eX.symm 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 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) (Φ.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) Y'
Tactic: have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm (Iso.refl Y')
-- 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 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) 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 X) Z'
Tactic: have := hasSmallLocalizedHom_of_isos.{w'} W₂ eX.symm (Iso.refl Z')
-- 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 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) 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₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Z)
Tactic: have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm eZ.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 : HasSmallLocalizedHom W₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) (Φ.functor (W₁ := W₁) (W₂ := W₂).obj 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₂ (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) Z'
Tactic: have := hasSmallLocalizedHom_of_isos.{w'} W₂ eY.symm (Iso.refl Z')