awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
this : MorphismProperty.naturalityProperty (NatTransExtension.app (W := W) τ) = ⊤
X Y : W.Localization
f : X ⟶ Y
⊢ F₁.map f ≫ NatTransExtension.app (W := W) τ Y = NatTransExtension.app (W := W) τ X ≫ F₂.map f

Tactic:
simpa only [← this] using MorphismProperty.top_apply f

Premises used: CategoryTheory.MorphismProperty.top_apply
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
suffices : MorphismProperty.naturalityProperty (NatTransExtension.app (W := W) τ) = ⊤
⊢ ∀ ⦃X Y : W.Localization⦄ (f : X ⟶ Y),
    F₁.map f ≫ NatTransExtension.app (W := W) τ Y = NatTransExtension.app (W := W) τ X ≫ F₂.map f

Tactic:
suffices MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤ by
      intro X Y f
      simpa only [← this] using MorphismProperty.top_apply f
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
⊢ MorphismProperty.naturalityProperty (NatTransExtension.app (W := W) τ) = ⊤

Tactic:
morphismProperty_eq_top'
      (MorphismProperty.naturalityProperty (NatTransExtension.app τ))
      ?_ (MorphismProperty.naturalityProperty.stableUnderInverse _)

Premises used: CategoryTheory.MorphismProperty.naturalityProperty, CategoryTheory.MorphismProperty.naturalityProperty.stableUnderInverse, CategoryTheory.Localization.Construction.morphismProperty_eq_top', CategoryTheory.Localization.Construction.NatTransExtension.app
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
refine : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), MorphismProperty.naturalityProperty (NatTransExtension.app (W := W) τ) (W.Q.map f)
⊢ MorphismProperty.naturalityProperty (NatTransExtension.app (W := W) τ) = ⊤

Tactic:
refine morphismProperty_eq_top'
      (MorphismProperty.naturalityProperty (NatTransExtension.app τ))
      ?_ (MorphismProperty.naturalityProperty.stableUnderInverse _)

Premises used: CategoryTheory.MorphismProperty.naturalityProperty, CategoryTheory.MorphismProperty.naturalityProperty.stableUnderInverse, CategoryTheory.Localization.Construction.morphismProperty_eq_top', CategoryTheory.Localization.Construction.NatTransExtension.app
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
X Y : C
f : X ⟶ Y
⊢ F₁.map (W.Q.map f) ≫ NatTransExtension.app (W := W) τ (W.Q.obj Y) =
    NatTransExtension.app (W := W) τ (W.Q.obj X) ≫ F₂.map (W.Q.map f)

Tactic:
simpa only [NatTransExtension.app_eq] using τ.naturality f

Premises used: CategoryTheory.Localization.Construction.NatTransExtension.app_eq, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ : W.Q ⋙ F ⟶ W.Q ⋙ G
⊢ 𝟙 W.Q ◫ natTransExtension (W := W) τ = τ

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
w : ∀ (X : W.Localization), τ₁.app X = τ₂.app X
⊢ τ₁ = τ₂

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
X : W.Localization
⊢ (objEquiv W).toFun ((objEquiv W).invFun X) = X

Tactic:
have eq := (objEquiv W).right_inv X
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
F G : W.Localization ⥤ D
τ₁ τ₂ : F ⟶ G
h : 𝟙 W.Q ◫ τ₁ = 𝟙 W.Q ◫ τ₂
X : W.Localization
eq : W.Q.obj (X.as (r := relations W).obj (W := W)) = X
w :
  Eq (α :=
    F.obj (W.Q.obj (X.as (r := relations W).obj (W := W))) ⟶ G.obj (W.Q.obj (X.as (r := relations W).obj (W := W))))
    (τ₁.app (W.Q.obj (X.as (r := relations W).obj (W := W)))) (τ₂.app (W.Q.obj (X.as (r := relations W).obj (W := W))))
w₁ :
  Eq (α :=
    F.obj (W.Q.obj (X.as (r := relations W).obj (W := W))) ⟶ G.obj (W.Q.obj (X.as (r := relations W).obj (W := W))))
    ((𝟙 W.Q ◫ τ₁).app (X.as (r := relations W).obj (W := W))) (τ₂.app (W.Q.obj (X.as (r := relations W).obj (W := W))))
w₂ :
  Eq (α :=
    F.obj (W.Q.obj (X.as (r := relations W).obj (W := W))) ⟶ G.obj (W.Q.obj (X.as (r := relations W).obj (W := W))))
    ((𝟙 W.Q ◫ τ₁).app (X.as (r := relations W).obj (W := W))) ((𝟙 W.Q ◫ τ₂).app (X.as (r := relations W).obj (W := W)))
w₃ w₄ :
  Eq (α :=
    F.obj (W.Q.obj (X.as (r := relations W).obj (W := W))) ⟶ G.obj (W.Q.obj (X.as (r := relations W).obj (W := W))))
    ((𝟙 W.Q ◫ τ₂).app (X.as (r := relations W).obj (W := W))) ((𝟙 W.Q ◫ τ₂).app (X.as (r := relations W).obj (W := W)))
⊢ τ₁.app X = τ₂.app X

Tactic:
rw [← eq, ← NatTrans.id_hcomp_app, ← NatTrans.id_hcomp_app, h]

Premises used: CategoryTheory.NatTrans.id_hcomp_app
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
X Y : MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D
τ : X ⟶ Y
rw rw₁ :
  X.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) =
    X.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)
⊢ W.Q ⋙ lift (W := W) (X.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)) ⋯ =
    X.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)

Tactic:
rw [fac]

Premises used: CategoryTheory.Localization.Construction.fac
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
X Y : MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D
τ : X ⟶ Y
rw rw₁ :
  Y.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) =
    Y.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)
⊢ Y.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) =
    W.Q ⋙ lift (W := W) (Y.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)) ⋯

Tactic:
rw [fac]

Premises used: CategoryTheory.Localization.Construction.fac
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G_1 : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G_1
G : MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D
rw :
  eqToHom ⋯ ≫ InducedCategory.Hom.hom (𝟙 G) ≫ eqToHom ⋯ =
    𝟙 W.Q ◫ 𝟙 (lift (W := W) (G.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)) ⋯)
⊢ 𝟙 W.Q ◫ natTransExtension (W := W) (eqToHom ⋯ ≫ InducedCategory.Hom.hom (𝟙 G) ≫ eqToHom ⋯) =
    𝟙 W.Q ◫ 𝟙 (lift (W := W) (G.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)) ⋯)

Tactic:
rw [natTransExtension_hcomp]

Premises used: CategoryTheory.Localization.Construction.natTransExtension_hcomp
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G_1 : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G_1
G : MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D
w :
  ∀ (X : C),
    (eqToHom ⋯ ≫ InducedCategory.Hom.hom (𝟙 G) ≫ eqToHom ⋯).app X =
      (𝟙 W.Q ◫ 𝟙 (lift (W := W) (G.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)) ⋯)).app X
⊢ eqToHom ⋯ ≫ InducedCategory.Hom.hom (𝟙 G) ≫ eqToHom ⋯ =
    𝟙 W.Q ◫ 𝟙 (lift (W := W) (G.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)) ⋯)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G_1 : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G_1
G : MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D
X : C
w :
  (InducedCategory.Hom.hom (𝟙 G)).app X =
    𝟙 ((lift (W := W) (G.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)) ⋯).obj (W.Q.obj X))
⊢ (eqToHom ⋯ ≫ InducedCategory.Hom.hom (𝟙 G) ≫ eqToHom ⋯).app X =
    (𝟙 W.Q ◫ 𝟙 (lift (W := W) (G.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)) ⋯)).app X

Tactic:
simp only [NatTrans.comp_app, eqToHom_app, eqToHom_refl, comp_id, id_comp,
          NatTrans.hcomp_id_app, NatTrans.id_app, Functor.map_id]

Premises used: CategoryTheory.NatTrans.hcomp_id_app, CategoryTheory.eqToHom_app, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G_1 : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G_1
G : MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D
X : C
⊢ (InducedCategory.Hom.hom (𝟙 G)).app X =
    𝟙 ((lift (W := W) (G.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)) ⋯).obj (W.Q.obj X))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
X Y Z : MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D
τ₁ : X ⟶ Y
τ₂ : Y ⟶ Z
w :
  ∀ (X_1 : C),
    (𝟙 W.Q ◫ natTransExtension (W := W) (eqToHom ⋯ ≫ (τ₁ ≫ τ₂).hom ≫ eqToHom ⋯)).app X_1 =
      (𝟙 W.Q ◫
            (natTransExtension (W := W) (eqToHom ⋯ ≫ τ₁.hom ≫ eqToHom ⋯) ≫
              natTransExtension (W := W) (eqToHom ⋯ ≫ τ₂.hom ≫ eqToHom ⋯))).app
        X_1
⊢ 𝟙 W.Q ◫ natTransExtension (W := W) (eqToHom ⋯ ≫ (τ₁ ≫ τ₂).hom ≫ eqToHom ⋯) =
    𝟙 W.Q ◫
      (natTransExtension (W := W) (eqToHom ⋯ ≫ τ₁.hom ≫ eqToHom ⋯) ≫
        natTransExtension (W := W) (eqToHom ⋯ ≫ τ₂.hom ≫ eqToHom ⋯))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
X_1 Y Z : MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D
τ₁ : X_1 ⟶ Y
τ₂ : Y ⟶ Z
X : C
w : (τ₁ ≫ τ₂).hom.app X = τ₁.hom.app X ≫ τ₂.hom.app X
⊢ (𝟙 W.Q ◫ natTransExtension (W := W) (eqToHom ⋯ ≫ (τ₁ ≫ τ₂).hom ≫ eqToHom ⋯)).app X =
    (𝟙 W.Q ◫
          (natTransExtension (W := W) (eqToHom ⋯ ≫ τ₁.hom ≫ eqToHom ⋯) ≫
            natTransExtension (W := W) (eqToHom ⋯ ≫ τ₂.hom ≫ eqToHom ⋯))).app
      X

Tactic:
simp only [natTransExtension_hcomp, NatTrans.comp_app, eqToHom_app, eqToHom_refl,
          id_comp, comp_id, NatTrans.hcomp_app, NatTrans.id_app, Functor.map_id,
          natTransExtension_app, NatTransExtension.app_eq]

Premises used: CategoryTheory.Localization.Construction.natTransExtension_hcomp, CategoryTheory.NatTrans.hcomp_app, CategoryTheory.eqToHom_app, CategoryTheory.Localization.Construction.NatTransExtension.app_eq, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.NatTrans.id_app, CategoryTheory.NatTrans.comp_app, CategoryTheory.Localization.Construction.natTransExtension_app, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
X_1 Y Z : MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D
τ₁ : X_1 ⟶ Y
τ₂ : Y ⟶ Z
X : C
⊢ (τ₁ ≫ τ₂).hom.app X = τ₁.hom.app X ≫ τ₂.hom.app X

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
⊢ Eq (α := (W.Localization ⥤ D) ⥤ W.Localization ⥤ D) (𝟭 (W.Localization ⥤ D)) (functor W D ⋙ inverse W D)

Tactic:
Functor.ext (fun G => ?_) fun G₁ G₂ τ => ?_

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
refine_1 : ∀ (G : W.Localization ⥤ D), obj (𝟭 (W.Localization ⥤ D)) G = obj (functor W D ⋙ inverse W D) G
refine_2 :
  ∀ (G₁ G₂ : W.Localization ⥤ D) (τ : G₁ ⟶ G₂),
    Eq (α := obj (𝟭 (W.Localization ⥤ D)) G₁ ⟶ obj (𝟭 (W.Localization ⥤ D)) G₂) (map (𝟭 (W.Localization ⥤ D)) τ)
      (CategoryStruct.comp (Y := obj (functor W D ⋙ inverse W D) G₁) (eqToHom ⋯)
        (map (functor W D ⋙ inverse W D) τ ≫ eqToHom ⋯))
⊢ Eq (α := (W.Localization ⥤ D) ⥤ W.Localization ⥤ D) (𝟭 (W.Localization ⥤ D)) (functor W D ⋙ inverse W D)

Tactic:
refine Functor.ext (fun G => ?_) fun G₁ G₂ τ => ?_

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G_1 : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G_1
G : W.Localization ⥤ D
refine_1 : W.Q ⋙ obj (𝟭 (W.Localization ⥤ D)) G = W.Q ⋙ obj (functor W D ⋙ inverse W D) G
⊢ obj (𝟭 (W.Localization ⥤ D)) G = obj (functor W D ⋙ inverse W D) G

Tactic:
apply uniq

Premises used: CategoryTheory.Localization.Construction.uniq
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G_1 : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G_1
G : W.Localization ⥤ D
⊢ W.Q ⋙ obj (𝟭 (W.Localization ⥤ D)) G = W.Q ⋙ obj (functor W D ⋙ inverse W D) G

Tactic:
simp [functor, inverse, fac]

Premises used: CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.inverse, CategoryTheory.Localization.Construction.fac, CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
G₁ G₂ : W.Localization ⥤ D
τ : G₁ ⟶ G₂
refine_2 :
  Eq (α := W.Q ⋙ obj (𝟭 (W.Localization ⥤ D)) G₁ ⟶ W.Q ⋙ obj (𝟭 (W.Localization ⥤ D)) G₂)
    (𝟙 W.Q ◫ map (𝟭 (W.Localization ⥤ D)) τ)
    (𝟙 W.Q ◫
      CategoryStruct.comp (Y := obj (functor W D ⋙ inverse W D) G₁) (eqToHom ⋯)
        (map (functor W D ⋙ inverse W D) τ ≫ eqToHom ⋯))
⊢ Eq (α := obj (𝟭 (W.Localization ⥤ D)) G₁ ⟶ obj (𝟭 (W.Localization ⥤ D)) G₂) (map (𝟭 (W.Localization ⥤ D)) τ)
    (CategoryStruct.comp (Y := obj (functor W D ⋙ inverse W D) G₁) (eqToHom ⋯)
      (map (functor W D ⋙ inverse W D) τ ≫ eqToHom ⋯))

Tactic:
apply natTrans_hcomp_injective

Premises used: CategoryTheory.Localization.Construction.natTrans_hcomp_injective
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
G₁ G₂ : W.Localization ⥤ D
τ : G₁ ⟶ G₂
refine_2 :
  ∀ (X : C),
    Eq (α := (W.Q ⋙ obj (𝟭 (W.Localization ⥤ D)) G₁).obj X ⟶ (W.Q ⋙ obj (𝟭 (W.Localization ⥤ D)) G₂).obj X)
      (NatTrans.app (𝟙 W.Q ◫ map (𝟭 (W.Localization ⥤ D)) τ) X)
      (NatTrans.app
        (𝟙 W.Q ◫
          CategoryStruct.comp (Y := obj (functor W D ⋙ inverse W D) G₁) (eqToHom ⋯)
            (map (functor W D ⋙ inverse W D) τ ≫ eqToHom ⋯))
        X)
⊢ Eq (α := W.Q ⋙ obj (𝟭 (W.Localization ⥤ D)) G₁ ⟶ W.Q ⋙ obj (𝟭 (W.Localization ⥤ D)) G₂)
    (𝟙 W.Q ◫ map (𝟭 (W.Localization ⥤ D)) τ)
    (𝟙 W.Q ◫
      CategoryStruct.comp (Y := obj (functor W D ⋙ inverse W D) G₁) (eqToHom ⋯)
        (map (functor W D ⋙ inverse W D) τ ≫ eqToHom ⋯))

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
G₁ G₂ : W.Localization ⥤ D
τ : G₁ ⟶ G₂
X : C
⊢ Eq (α := (W.Q ⋙ obj (𝟭 (W.Localization ⥤ D)) G₁).obj X ⟶ (W.Q ⋙ obj (𝟭 (W.Localization ⥤ D)) G₂).obj X)
    (NatTrans.app (𝟙 W.Q ◫ map (𝟭 (W.Localization ⥤ D)) τ) X)
    (NatTrans.app
      (𝟙 W.Q ◫
        CategoryStruct.comp (Y := obj (functor W D ⋙ inverse W D) G₁) (eqToHom ⋯)
          (map (functor W D ⋙ inverse W D) τ ≫ eqToHom ⋯))
      X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
⊢ Eq (α :=
    MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D ⥤
      MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)
    (inverse W D ⋙ functor W D) (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D))

Tactic:
Functor.ext ?_ ?_

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
refine_1 :
  ∀ (X : MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D),
    obj (inverse W D ⋙ functor W D) X = obj (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)) X
refine_2 :
  ∀ (X Y : MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D) (f : X ⟶ Y),
    Eq (α := obj (inverse W D ⋙ functor W D) X ⟶ obj (inverse W D ⋙ functor W D) Y) (map (inverse W D ⋙ functor W D) f)
      (eqToHom ⋯ ≫ map (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)) f ≫ eqToHom ⋯)
⊢ Eq (α :=
    MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D ⥤
      MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)
    (inverse W D ⋙ functor W D) (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D))

Tactic:
refine Functor.ext ?_ ?_

Premises used: CategoryTheory.Functor.ext
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G_1 : Functor.{uC', uD', uC, uD} C D
hG_1 : W.IsInvertedBy G_1
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
refine_1 :
  (obj (inverse W D ⋙ functor W D)
          (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G
            hG)).obj
      (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) =
    ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)
      (obj (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D))
        (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G hG))
⊢ obj (inverse W D ⋙ functor W D)
      (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G hG) =
    obj (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D))
      (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G hG)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G_1 : Functor.{uC', uD', uC, uD} C D
hG_1 : W.IsInvertedBy G_1
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
⊢ (obj (inverse W D ⋙ functor W D)
          (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G
            hG)).obj
      (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) =
    ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)
      (obj (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D))
        (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G hG))

Tactic:
fac G hG

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Localization.Construction.fac
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
G_1 : Functor.{uC', uD', uC, uD} C D
hG_1 : W.IsInvertedBy G_1
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
⊢ (obj (inverse W D ⋙ functor W D)
          (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G
            hG)).obj
      (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) =
    ObjectProperty.FullSubcategory.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)
      (obj (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D))
        (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G hG))

Tactic:
exact fac G hG

Premises used: CategoryTheory.Localization.Construction.fac