awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst : Category.{v_2, u_2} C₁
inst_1 : Category.{v_3, u_3} C₂
inst_2 : Category.{v_4, u_4} C₃
inst_3 : Category.{v_5, u_5} D₁
inst_4 : Category.{v_6, u_6} D₂
inst_5 : Category.{v_7, u_7} D₃
W₁ : MorphismProperty.{v_2, u_2} C₁
W₂ : MorphismProperty.{v_3, u_3} C₂
W₃ : MorphismProperty.{v_4, u_4} C₃
Φ : LocalizerMorphism W₁ W₂
Ψ : LocalizerMorphism W₂ W₃
L₁ : Functor.{v_2, v_5, u_2, u_5} C₁ D₁
inst_6 : L₁.IsLocalization W₁
L₂ : Functor.{v_3, v_6, u_3, u_6} C₂ D₂
inst_7 : L₂.IsLocalization W₂
L₃ : Functor.{v_4, v_7, u_4, u_7} C₃ D₃
inst_8 : L₃.IsLocalization W₃
X Y : C₁
f : L₁.obj X ⟶ L₁.obj Y
G : Functor.{v_5, v_6, u_5, u_6} D₁ D₂ := Φ.localizedFunctor (W₁ := W₁) (W₂ := W₂) L₁ L₂
G' : Functor.{v_6, v_7, u_6, u_7} D₂ D₃ := Ψ.localizedFunctor (W₁ := W₂) (W₂ := W₃) L₂ L₃
e : Φ.functor (W₁ := W₁) (W₂ := W₂) ⋙ L₂ ≅ L₁ ⋙ G := CatCommSq.iso (Φ.functor (W₁ := W₁) (W₂ := W₂)) L₁ L₂ G
e' : Ψ.functor (W₁ := W₂) (W₂ := W₃) ⋙ L₃ ≅ L₂ ⋙ G' := CatCommSq.iso (Ψ.functor (W₁ := W₂) (W₂ := W₃)) L₂ L₃ G'
⊢ e'.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
      G'.map (e.hom.app X ≫ G.map f ≫ e.inv.app Y) ≫ e'.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) =
    (Φ.functor (W₁ := W₁) (W₂ := W₂).associator (Ψ.functor (W₁ := W₂) (W₂ := W₃)) L₃ ≪≫
              Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft e' ≪≫
                (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ G').symm ≪≫
                  Functor.isoWhiskerRight e G' ≪≫ L₁.associator G G').hom.app
        X ≫
      (G ⋙ G').map f ≫
        (Φ.functor (W₁ := W₁) (W₂ := W₂).associator (Ψ.functor (W₁ := W₂) (W₂ := W₃)) L₃ ≪≫
                Φ.functor (W₁ := W₁) (W₂ := W₂).isoWhiskerLeft e' ≪≫
                  (Φ.functor (W₁ := W₁) (W₂ := W₂).associator L₂ G').symm ≪≫
                    Functor.isoWhiskerRight e G' ≪≫ L₁.associator G G').inv.app
          Y
have dsimp : e'.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
    G'.map (e.hom.app X ≫ G.map f ≫ e.inv.app Y) ≫ e'.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y) =
  (𝟙 (L₃.obj (Ψ.functor (W₁ := W₂) (W₂ := W₃).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))) ≫
      e'.hom.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X) ≫
        𝟙 (G'.obj (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj X))) ≫
          G'.map (e.hom.app X) ≫ 𝟙 (G'.obj (G.obj (L₁.obj X)))) ≫
    G'.map (G.map f) ≫
      (((𝟙 (G'.obj (G.obj (L₁.obj Y))) ≫ G'.map (e.inv.app Y)) ≫
            𝟙 (G'.obj (L₂.obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)))) ≫
          e'.inv.app (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)) ≫
        𝟙 (L₃.obj (Ψ.functor (W₁ := W₂) (W₂ := W₃).obj (Φ.functor (W₁ := W₁) (W₂ := W₂).obj Y)))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
inst_4 : Category.{v_5, u_5} D₁
inst_5 : Category.{v_6, u_6} D₂
inst_6 : Category.{v_7, u_7} D₃
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_7 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_8 : L₂.IsLocalization W
L₃ : Functor.{v_1, v_7, u_1, u_7} C D₃
inst_9 : L₃.IsLocalization W
X Y Z : C
f : L₁.obj X ⟶ L₁.obj Y
⊢ (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₂ L₁
      ((LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₂ f) =
    f
have rw : ((LocalizerMorphism.id W).comp (W₁ := W) (W₂ := W) (W₃ := W) (LocalizerMorphism.id W)).homMap (W₁ := W) (W₂ := W) L₁ L₁
    f =
  f
Tactic: rw [LocalizerMorphism.homMap_homMap]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} C₁
inst_2 : Category.{v_3, u_3} C₂
inst_3 : Category.{v_4, u_4} C₃
inst_4 : Category.{v_5, u_5} D₁
inst_5 : Category.{v_6, u_6} D₂
inst_6 : Category.{v_7, u_7} D₃
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_7 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_8 : L₂.IsLocalization W
L₃ : Functor.{v_1, v_7, u_1, u_7} C D₃
inst_9 : L₃.IsLocalization W
X Y Z : C
g : L₂.obj X ⟶ L₂.obj Y
⊢ (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₂
      ((LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₂ L₁ g) =
    g
have rw : ((LocalizerMorphism.id W).comp (W₁ := W) (W₂ := W) (W₃ := W) (LocalizerMorphism.id W)).homMap (W₁ := W) (W₂ := W) L₂ L₂
    g =
  g
Tactic: rw [LocalizerMorphism.homMap_homMap]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
G : Functor.{v_5, v_6, u_5, u_6} D₁ D₂
e : L₁ ⋙ G ≅ L₂
f : L₁.obj X ⟶ L₁.obj Y
⊢ ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      f =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y
have rw : (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₂ f = e.inv.app X ≫ G.map f ≫ e.hom.app Y
Tactic: rw [homEquiv_apply, LocalizerMorphism.homMap_apply (LocalizerMorphism.id W) L₁ L₂ G e.symm,
    Iso.symm_hom, Iso.symm_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
G : Functor.{v_5, v_6, u_5, u_6} D₁ D₂
e : L₁ ⋙ G ≅ L₂
f : L₁.obj X ⟶ L₁.obj Y
rw : (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₂ f = e.inv.app X ≫ G.map f ≫ e.hom.app Y
⊢ ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      f =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y
have rw₁ : e.symm.hom.app X ≫ G.map f ≫ e.symm.inv.app Y = e.inv.app X ≫ G.map f ≫ e.hom.app Y
Tactic: rw [homEquiv_apply, LocalizerMorphism.homMap_apply (LocalizerMorphism.id W) L₁ L₂ G e.symm,
    Iso.symm_hom, Iso.symm_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
G : Functor.{v_5, v_6, u_5, u_6} D₁ D₂
e : L₁ ⋙ G ≅ L₂
f : L₁.obj X ⟶ L₁.obj Y
rw : (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₂ f = e.inv.app X ≫ G.map f ≫ e.hom.app Y
rw₁ : e.symm.hom.app X ≫ G.map f ≫ e.symm.inv.app Y = e.inv.app X ≫ G.map f ≫ e.hom.app Y
⊢ ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      f =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y
have rw₂ : e.inv.app X ≫ G.map f ≫ e.symm.inv.app Y = e.inv.app X ≫ G.map f ≫ e.hom.app Y
Tactic: rw [homEquiv_apply, LocalizerMorphism.homMap_apply (LocalizerMorphism.id W) L₁ L₂ G e.symm,
    Iso.symm_hom, Iso.symm_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
G : Functor.{v_5, v_6, u_5, u_6} D₁ D₂
e : L₁ ⋙ G ≅ L₂
f : L₁.obj X ⟶ L₁.obj Y
rw : (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₂ f = e.inv.app X ≫ G.map f ≫ e.hom.app Y
rw₁ : e.symm.hom.app X ≫ G.map f ≫ e.symm.inv.app Y = e.inv.app X ≫ G.map f ≫ e.hom.app Y
rw₂ : e.inv.app X ≫ G.map f ≫ e.symm.inv.app Y = e.inv.app X ≫ G.map f ≫ e.hom.app Y
⊢ ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      f =
    e.inv.app X ≫ G.map f ≫ e.hom.app Y
have rw₃ : e.inv.app X ≫ G.map f ≫ e.hom.app Y = e.inv.app X ≫ G.map f ≫ e.hom.app Y
Tactic: rw [homEquiv_apply, LocalizerMorphism.homMap_apply (LocalizerMorphism.id W) L₁ L₂ G e.symm,
    Iso.symm_hom, Iso.symm_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
D₃ : Type u_7
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
inst_3 : Category.{v_7, u_7} D₃
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_4 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_5 : L₂.IsLocalization W
L₃ : Functor.{v_1, v_7, u_1, u_7} C D₃
inst_6 : L₃.IsLocalization W
X Y : C
f : L₁.obj X ⟶ L₁.obj Y
⊢ Eq.{v_7 + 1} (α := L₃.obj X ⟶ L₃.obj Y)
    (((homEquiv W L₂ L₃ : Equiv.{v_6 + 1, v_7 + 1} (L₂.obj X ⟶ L₂.obj Y) (L₃.obj X ⟶ L₃.obj Y)) :
          (a : L₂.obj X ⟶ L₂.obj Y) → L₃.obj X ⟶ L₃.obj Y)
        (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          f) :
      L₃.obj X ⟶ L₃.obj Y)
    (((homEquiv W L₁ L₃ : Equiv.{v_5 + 1, v_7 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₃.obj X ⟶ L₃.obj Y)) :
          (a : L₁.obj X ⟶ L₁.obj Y) → L₃.obj X ⟶ L₃.obj Y)
        f :
      L₃.obj X ⟶ L₃.obj Y)
have dsimp : (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₂ L₃
    ((LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₂ f) =
  (LocalizerMorphism.id W).homMap (W₁ := W) (W₂ := W) L₁ L₃ f
Tactic: dsimp only [homEquiv_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
⊢ ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      (isoOfHom L₁ W f hf).inv =
    (isoOfHom L₂ W f hf).inv
have rw : ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      (isoOfHom L₁ W f hf).inv ≫
    (isoOfHom L₂ W f hf).hom =
  (isoOfHom L₂ W f hf).inv ≫ (isoOfHom L₂ W f hf).hom
Tactic: rw [← cancel_mono (isoOfHom L₂ W f hf).hom, Iso.inv_hom_id, isoOfHom_hom,
    ← homEquiv_map W L₁ L₂ f, ← homEquiv_comp, isoOfHom_inv_hom_id, homEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
rw :
  ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
          (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
        (isoOfHom L₁ W f hf).inv ≫
      (isoOfHom L₂ W f hf).hom =
    (isoOfHom L₂ W f hf).inv ≫ (isoOfHom L₂ W f hf).hom
⊢ ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      (isoOfHom L₁ W f hf).inv =
    (isoOfHom L₂ W f hf).inv
have rw₁ : Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
  (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
          (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
        (isoOfHom L₁ W f hf).inv ≫
      (isoOfHom L₂ W f hf).hom :
    L₂.obj X ⟶ L₂.obj X)
  (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
Tactic: rw [← cancel_mono (isoOfHom L₂ W f hf).hom, Iso.inv_hom_id, isoOfHom_hom,
    ← homEquiv_map W L₁ L₂ f, ← homEquiv_comp, isoOfHom_inv_hom_id, homEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
rw :
  ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
          (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
        (isoOfHom L₁ W f hf).inv ≫
      (isoOfHom L₂ W f hf).hom =
    (isoOfHom L₂ W f hf).inv ≫ (isoOfHom L₂ W f hf).hom
rw₁ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv ≫
        (isoOfHom L₂ W f hf).hom :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
⊢ ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      (isoOfHom L₁ W f hf).inv =
    (isoOfHom L₂ W f hf).inv
have rw₂ : Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
  (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
          (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
        (isoOfHom L₁ W f hf).inv ≫
      L₂.map f :
    L₂.obj X ⟶ L₂.obj X)
  (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
Tactic: rw [← cancel_mono (isoOfHom L₂ W f hf).hom, Iso.inv_hom_id, isoOfHom_hom,
    ← homEquiv_map W L₁ L₂ f, ← homEquiv_comp, isoOfHom_inv_hom_id, homEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
rw :
  ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
          (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
        (isoOfHom L₁ W f hf).inv ≫
      (isoOfHom L₂ W f hf).hom =
    (isoOfHom L₂ W f hf).inv ≫ (isoOfHom L₂ W f hf).hom
rw₁ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv ≫
        (isoOfHom L₂ W f hf).hom :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₂ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv ≫
        L₂.map f :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
⊢ ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      (isoOfHom L₁ W f hf).inv =
    (isoOfHom L₂ W f hf).inv
have rw₃ : Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
  (CategoryStruct.comp (Y := L₂.obj Y)
      (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
          (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
        (isoOfHom L₁ W f hf).inv)
      (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj Y ⟶ L₁.obj X) (L₂.obj Y ⟶ L₂.obj X)) :
          (a : L₁.obj Y ⟶ L₁.obj X) → L₂.obj Y ⟶ L₂.obj X)
        (L₁.map f)) :
    L₂.obj X ⟶ L₂.obj X)
  (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
Tactic: rw [← cancel_mono (isoOfHom L₂ W f hf).hom, Iso.inv_hom_id, isoOfHom_hom,
    ← homEquiv_map W L₁ L₂ f, ← homEquiv_comp, isoOfHom_inv_hom_id, homEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
rw :
  ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
          (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
        (isoOfHom L₁ W f hf).inv ≫
      (isoOfHom L₂ W f hf).hom =
    (isoOfHom L₂ W f hf).inv ≫ (isoOfHom L₂ W f hf).hom
rw₁ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv ≫
        (isoOfHom L₂ W f hf).hom :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₂ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv ≫
        L₂.map f :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₃ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (CategoryStruct.comp (Y := L₂.obj Y)
        (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv)
        (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj Y ⟶ L₁.obj X) (L₂.obj Y ⟶ L₂.obj X)) :
            (a : L₁.obj Y ⟶ L₁.obj X) → L₂.obj Y ⟶ L₂.obj X)
          (L₁.map f)) :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
⊢ ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      (isoOfHom L₁ W f hf).inv =
    (isoOfHom L₂ W f hf).inv
have rw₄ : Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
  (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj X) (L₂.obj X ⟶ L₂.obj X)) :
        (a : L₁.obj X ⟶ L₁.obj X) → L₂.obj X ⟶ L₂.obj X)
      ((isoOfHom L₁ W f hf).inv ≫ L₁.map f) :
    L₂.obj X ⟶ L₂.obj X)
  (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
Tactic: rw [← cancel_mono (isoOfHom L₂ W f hf).hom, Iso.inv_hom_id, isoOfHom_hom,
    ← homEquiv_map W L₁ L₂ f, ← homEquiv_comp, isoOfHom_inv_hom_id, homEquiv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.HomEquiv (goal)
Goal:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_5} D₁
inst_2 : Category.{v_6, u_6} D₂
W : MorphismProperty.{v_1, u_1} C
L₁ : Functor.{v_1, v_5, u_1, u_5} C D₁
inst_3 : L₁.IsLocalization W
L₂ : Functor.{v_1, v_6, u_1, u_6} C D₂
inst_4 : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
rw :
  ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
          (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
        (isoOfHom L₁ W f hf).inv ≫
      (isoOfHom L₂ W f hf).hom =
    (isoOfHom L₂ W f hf).inv ≫ (isoOfHom L₂ W f hf).hom
rw₁ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv ≫
        (isoOfHom L₂ W f hf).hom :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₂ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv ≫
        L₂.map f :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₃ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (CategoryStruct.comp (Y := L₂.obj Y)
        (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
            (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
          (isoOfHom L₁ W f hf).inv)
        (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj Y ⟶ L₁.obj X) (L₂.obj Y ⟶ L₂.obj X)) :
            (a : L₁.obj Y ⟶ L₁.obj X) → L₂.obj Y ⟶ L₂.obj X)
          (L₁.map f)) :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
rw₄ :
  Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
    (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj X) (L₂.obj X ⟶ L₂.obj X)) :
          (a : L₁.obj X ⟶ L₁.obj X) → L₂.obj X ⟶ L₂.obj X)
        ((isoOfHom L₁ W f hf).inv ≫ L₁.map f) :
      L₂.obj X ⟶ L₂.obj X)
    (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
⊢ ((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj Y) (L₂.obj X ⟶ L₂.obj Y)) :
        (a : L₁.obj X ⟶ L₁.obj Y) → L₂.obj X ⟶ L₂.obj Y)
      (isoOfHom L₁ W f hf).inv =
    (isoOfHom L₂ W f hf).inv
have rw₅ : Eq.{v_6 + 1} (α := L₂.obj X ⟶ L₂.obj X)
  (((homEquiv W L₁ L₂ : Equiv.{v_5 + 1, v_6 + 1} (L₁.obj X ⟶ L₁.obj X) (L₂.obj X ⟶ L₂.obj X)) :
        (a : L₁.obj X ⟶ L₁.obj X) → L₂.obj X ⟶ L₂.obj X)
      (𝟙 (L₁.obj X)) :
    L₂.obj X ⟶ L₂.obj X)
  (𝟙 (L₂.obj X) : L₂.obj X ⟶ L₂.obj X)
Tactic: rw [← cancel_mono (isoOfHom L₂ W f hf).hom, Iso.inv_hom_id, isoOfHom_hom,
    ← homEquiv_map W L₁ L₂ f, ← homEquiv_comp, isoOfHom_inv_hom_id, homEquiv_id]