awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
D : Type uD
inst_1 : Category.{uD', uD} D
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
X : C
⊢ app (W := W) τ (W.Q.obj X) = τ.app X
have simp : τ.app ((objEquiv W).invFun (W.Q.obj X)) = τ.app X
Tactic: simp only [app, eqToHom_refl, comp_id, id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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 : W.Localization⦄ (f : X ⟶ Y),
    F₁.map f ≫ NatTransExtension.app (W := W) τ Y = NatTransExtension.app (W := W) τ X ≫ F₂.map f
have suffices : MorphismProperty.naturalityProperty (NatTransExtension.app (W := W) τ) = ⊤
Tactic: suffices MorphismProperty.naturalityProperty (NatTransExtension.app τ) = ⊤ by
      intro X Y f
      simpa only [← this] using MorphismProperty.top_apply f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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) τ) = ⊤
have refine : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), MorphismProperty.naturalityProperty (NatTransExtension.app (W := W) τ) (W.Q.map f)
Tactic: refine morphismProperty_eq_top'
      (MorphismProperty.naturalityProperty (NatTransExtension.app τ))
      ?_ (MorphismProperty.naturalityProperty.stableUnderInverse _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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 ◫ τ₂
⊢ τ₁ = τ₂
have w : ∀ (X : W.Localization), τ₁.app X = τ₂.app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (hypothesis)
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
⊢ τ₁.app X = τ₂.app X
have eq : (objEquiv W).toFun ((objEquiv W).invFun X) = X
Tactic: have eq := (objEquiv W).right_inv X
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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
⊢ τ₁.app X = τ₂.app X
have 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))))
Tactic: rw [← eq, ← NatTrans.id_hcomp_app, ← NatTrans.id_hcomp_app, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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))))
⊢ τ₁.app X = τ₂.app X
have 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))))
Tactic: rw [← eq, ← NatTrans.id_hcomp_app, ← NatTrans.id_hcomp_app, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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))))
⊢ τ₁.app X = τ₂.app X
have 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)))
Tactic: rw [← eq, ← NatTrans.id_hcomp_app, ← NatTrans.id_hcomp_app, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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)))
⊢ τ₁.app X = τ₂.app X
have 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)))
Tactic: rw [← eq, ← NatTrans.id_hcomp_app, ← NatTrans.id_hcomp_app, h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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
⊢ 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)
have 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)
Tactic: rw [fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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
⊢ 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)) ⋯
have 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)
Tactic: rw [fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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.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)) ⋯)
have rw : eqToHom sorry ≫ InducedCategory.Hom.hom (𝟙 G) ≫ eqToHom sorry =
  𝟙 W.Q ◫ 𝟙 (lift (W := W) (G.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)) sorry)
Tactic: rw [natTransExtension_hcomp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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
⊢ 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)) ⋯)
have w : ∀ (X : C),
  (eqToHom sorry ≫ InducedCategory.Hom.hom (𝟙 G) ≫ eqToHom sorry).app X =
    (𝟙 W.Q ◫ 𝟙 (lift (W := W) (G.obj (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F)) sorry)).app X
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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
⊢ (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
have 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)) sorry).obj (W.Q.obj 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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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.Q ◫ natTransExtension (W := W) (eqToHom ⋯ ≫ (τ₁ ≫ τ₂).hom ≫ eqToHom ⋯) =
    𝟙 W.Q ◫
      (natTransExtension (W := W) (eqToHom ⋯ ≫ τ₁.hom ≫ eqToHom ⋯) ≫
        natTransExtension (W := W) (eqToHom ⋯ ≫ τ₂.hom ≫ eqToHom ⋯))
have w : ∀ (X_1 : C),
  (𝟙 W.Q ◫ natTransExtension (W := W) (eqToHom sorry ≫ (τ₁ ≫ τ₂).hom ≫ eqToHom sorry)).app X_1 =
    (𝟙 W.Q ◫
          (natTransExtension (W := W) (eqToHom sorry ≫ τ₁.hom ≫ eqToHom sorry) ≫
            natTransExtension (W := W) (eqToHom sorry ≫ τ₂.hom ≫ eqToHom sorry))).app
      X_1
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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.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
have w : (τ₁ ≫ τ₂).hom.app X = τ₁.hom.app X ≫ τ₂.hom.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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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)
have refine_1 : ∀ (G : W.Localization ⥤ D), obj (𝟭 (W.Localization ⥤ D)) G = obj (functor W D ⋙ inverse W D) G
Tactic: refine Functor.ext (fun G => ?_) fun G₁ G₂ τ => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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
⊢ Eq (α := (W.Localization ⥤ D) ⥤ W.Localization ⥤ D) (𝟭 (W.Localization ⥤ D)) (functor W D ⋙ inverse W D)
have 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 sorry)
      (map (functor W D ⋙ inverse W D) τ ≫ eqToHom sorry))
Tactic: refine Functor.ext (fun G => ?_) fun G₁ G₂ τ => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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
⊢ obj (𝟭 (W.Localization ⥤ D)) G = obj (functor W D ⋙ inverse W D) G
have refine_1 : W.Q ⋙ obj (𝟭 (W.Localization ⥤ D)) G = W.Q ⋙ obj (functor W D ⋙ inverse W D) G
Tactic: apply uniq
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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₂
⊢ 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 ⋯))
have 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 sorry)
      (map (functor W D ⋙ inverse W D) τ ≫ eqToHom sorry))
Tactic: apply natTrans_hcomp_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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₂
⊢ 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 ⋯))
have 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 sorry)
          (map (functor W D ⋙ inverse W D) τ ≫ eqToHom sorry))
      X)
Tactic: ext X
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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))
have 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
Tactic: refine Functor.ext ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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
⊢ 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))
have 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 sorry ≫ map (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)) f ≫ eqToHom sorry)
Tactic: refine Functor.ext ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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 (𝟭 (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)
have 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))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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₁ : Functor.{uC', uD', uC, uD} C D
hG₁ : W.IsInvertedBy G₁
G₂ : Functor.{uC', uD', uC, uD} C D
hG₂ : W.IsInvertedBy G₂
f :
  Quiver.Hom (V := 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₁)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₂ hG₂)
⊢ Eq (α :=
    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 (inverse W D ⋙ functor W D)
        (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₂ hG₂))
    (map (inverse W D ⋙ functor W D) f)
    (CategoryStruct.comp (Y :=
      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₁))
      (eqToHom ⋯) (map (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)) f ≫ eqToHom ⋯))
have refine_2 : ∀ (x : C),
  Eq (α :=
    (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).obj
        x ⟶
      (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).obj
        x)
    (NatTrans.app (InducedCategory.Hom.hom (map (inverse W D ⋙ functor W D) f)) x)
    (NatTrans.app
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y :=
          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₁))
          (eqToHom sorry) (map (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)) f ≫ eqToHom sorry)))
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.Construction (goal)
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₁ : Functor.{uC', uD', uC, uD} C D
hG₁ : W.IsInvertedBy G₁
G₂ : Functor.{uC', uD', uC, uD} C D
hG₂ : W.IsInvertedBy G₂
f :
  Quiver.Hom (V := 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₁)
    (ObjectProperty.FullSubcategory.mk (P := fun (F : Functor.{uC', uD', uC, uD} C D) ↦ W.IsInvertedBy F) G₂ hG₂)
x : C
⊢ Eq (α :=
    (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).obj
        x ⟶
      (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).obj
        x)
    (NatTrans.app (InducedCategory.Hom.hom (map (inverse W D ⋙ functor W D) f)) x)
    (NatTrans.app
      (InducedCategory.Hom.hom
        (CategoryStruct.comp (Y :=
          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₁))
          (eqToHom ⋯) (map (𝟭 (MorphismProperty.FunctorsInverting.{uC', uC, uD', uD} W D)) f ≫ eqToHom ⋯)))
      x)
have refine_2 : Eq (α :=
  G₁.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)))
  (NatTransExtension.app (W := W) (eqToHom sorry ≫ f.hom ≫ eqToHom sorry) (W.Q.obj x))
  (CategoryStruct.comp (Y := G₁.obj x) (NatTrans.app (InducedCategory.Hom.hom (eqToHom sorry)) x)
    (f.hom.app x ≫ NatTrans.app (InducedCategory.Hom.hom (eqToHom sorry)) x))
Tactic: dsimp