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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
refine_1 : (Quotient.functor (relations W) ⋙ G₁).obj = (Quotient.functor (relations W) ⋙ G₂).obj
refine_2 :
  ∀ (a b : LocQuiver W) (e : a ⟶ b),
    (Quotient.functor (relations W) ⋙ G₁).map e.toPath =
      eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map e.toPath ≫ eqToHom ⋯
⊢ Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂

Tactic:
refine Paths.ext_functor ?_ ?_

Premises used: CategoryTheory.Paths.ext_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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
refine_1 :
  ∀ (X : Paths (LocQuiver W)), (Quotient.functor (relations W) ⋙ G₁).obj X = (Quotient.functor (relations W) ⋙ G₂).obj X
⊢ (Quotient.functor (relations W) ⋙ G₁).obj = (Quotient.functor (relations W) ⋙ G₂).obj

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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X : Paths (LocQuiver W)
refine_1 :
  ∀ (obj : C),
    (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) obj) =
      (Quotient.functor (relations W) ⋙ G₂).obj (LocQuiver.mk (W := W) obj)
⊢ (Quotient.functor (relations W) ⋙ G₁).obj X = (Quotient.functor (relations W) ⋙ G₂).obj X

Tactic:
cases 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
obj : C
⊢ (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) obj) =
    (Quotient.functor (relations W) ⋙ G₂).obj (LocQuiver.mk (W := W) obj)

Tactic:
apply Functor.congr_obj h

Premises used: CategoryTheory.Functor.congr_obj
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
f : LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y)
⊢ Eq (α :=
    (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) X) ⟶
      (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) Y))
    ((Quotient.functor (relations W) ⋙ G₁).map (Quiver.Hom.toPath (Sum.inl f)))
    (eqToHom ⋯ ≫ (Quotient.functor (relations W) ⋙ G₂).map (Quiver.Hom.toPath (Sum.inl f)) ≫ eqToHom ⋯)

Tactic:
simpa only using Functor.congr_hom h f

Premises used: CategoryTheory.Functor.congr_hom
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)
hw : W w
⊢ W.Q.map w = (wIso (W := W) w hw).hom

Tactic:
have hw : W.Q.map w = (wIso w hw).hom := 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)
hw_1 : W w
hw : W.Q.map w = (wIso (W := W) w hw_1).hom
⊢ (W.Q ⋙ G₁).map w = eqToHom ⋯ ≫ (W.Q ⋙ G₂).map w ≫ eqToHom ⋯

Tactic:
have hw' := Functor.congr_hom h w
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)
hw_1 : W w
hw : W.Q.map w = (wIso (W := W) w hw_1).hom
hw' : (W.Q ⋙ G₁).map w = eqToHom ⋯ ≫ (W.Q ⋙ G₂).map w ≫ eqToHom ⋯
⊢ G₁.map (wIso (W := W) w hw_1).hom = eqToHom ⋯ ≫ G₂.map (wIso (W := W) w hw_1).hom ≫ eqToHom ⋯

Tactic:
simp only [Functor.comp_map, hw] at hw'

Premises used: CategoryTheory.Functor.comp_map
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)
hw_1 : W w
hw : W.Q.map w = (wIso (W := W) w hw_1).hom
hw' : G₁.map (wIso (W := W) w hw_1).hom = eqToHom ⋯ ≫ G₂.map (wIso (W := W) w hw_1).hom ≫ eqToHom ⋯
⊢ Eq (α :=
    (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) X) ⟶
      (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) Y))
    ((Quotient.functor (relations W) ⋙ G₁).map
      (Quiver.Hom.toPath
        (Sum.inr
          (Subtype.mk (p :=
            fun
              (f :
                LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
            W f) w hw_1))))
    (eqToHom ⋯ ≫
      (Quotient.functor (relations W) ⋙ G₂).map
          (Quiver.Hom.toPath
            (Sum.inr
              (Subtype.mk (p :=
                fun
                  (f :
                    LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶
                      LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
                W f) w hw_1))) ≫
        eqToHom ⋯)

Tactic:
Functor.congr_inv_of_congr_hom _ _ _ ?_ ?_ hw'

Premises used: CategoryTheory.Functor.congr_inv_of_congr_hom, Quiver.Hom.toPath
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)
hw_1 : W w
hw : W.Q.map w = (wIso (W := W) w hw_1).hom
hw' : G₁.map (wIso (W := W) w hw_1).hom = eqToHom ⋯ ≫ G₂.map (wIso (W := W) w hw_1).hom ≫ eqToHom ⋯
refine_2 : G₁.obj (W.Q.obj Y) = G₂.obj (W.Q.obj Y)
refine_2₁ : G₁.obj (W.Q.obj X) = G₂.obj (W.Q.obj X)
⊢ Eq (α :=
    (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) X) ⟶
      (Quotient.functor (relations W) ⋙ G₁).obj (LocQuiver.mk (W := W) Y))
    ((Quotient.functor (relations W) ⋙ G₁).map
      (Quiver.Hom.toPath
        (Sum.inr
          (Subtype.mk (p :=
            fun
              (f :
                LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
            W f) w hw_1))))
    (eqToHom ⋯ ≫
      (Quotient.functor (relations W) ⋙ G₂).map
          (Quiver.Hom.toPath
            (Sum.inr
              (Subtype.mk (p :=
                fun
                  (f :
                    LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶
                      LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)) ↦
                W f) w hw_1))) ≫
        eqToHom ⋯)

Tactic:
refine Functor.congr_inv_of_congr_hom _ _ _ ?_ ?_ hw'

Premises used: CategoryTheory.Functor.congr_inv_of_congr_hom
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)
hw_1 : W w
hw : W.Q.map w = (wIso (W := W) w hw_1).hom
hw' : G₁.map (wIso (W := W) w hw_1).hom = eqToHom ⋯ ≫ G₂.map (wIso (W := W) w hw_1).hom ≫ eqToHom ⋯
⊢ G₁.obj (W.Q.obj Y) = G₂.obj (W.Q.obj Y)

Tactic:
apply Functor.congr_obj h

Premises used: CategoryTheory.Functor.congr_obj
-- 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
X Y : C
w : LocQuiver.obj (W := W) (LocQuiver.mk (W := W) Y) ⟶ LocQuiver.obj (W := W) (LocQuiver.mk (W := W) X)
hw_1 : W w
hw : W.Q.map w = (wIso (W := W) w hw_1).hom
hw' : G₁.map (wIso (W := W) w hw_1).hom = eqToHom ⋯ ≫ G₂.map (wIso (W := W) w hw_1).hom ≫ eqToHom ⋯
⊢ G₁.obj (W.Q.obj X) = G₂.obj (W.Q.obj X)

Tactic:
apply Functor.congr_obj h

Premises used: CategoryTheory.Functor.congr_obj
-- 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 : C
⊢ W.Q.obj
      ((fun (X : W.Localization) ↦ X.as (r := relations W).obj (W := W))
        (Quotient.mk (r := relations W) (LocQuiver.mk (W := W) X))) =
    Quotient.mk (r := relations W) (LocQuiver.mk (W := W) X)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
h : ∀ (X Y : W.Localization) (f : X ⟶ Y), P f = ⊤ f
⊢ P = ⊤

Tactic:
funext X Y f
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : P f ↔ ⊤ f
⊢ P f = ⊤ f

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : P f → ⊤ f
h₁ : ⊤ f → P f
⊢ P f ↔ ⊤ f

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : P f
⊢ ⊤ f

Tactic:
apply MorphismProperty.top_apply

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
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h_1 : ⊤ f
h : P f
⊢ P f

Tactic:
let G : _ ⥤ W.Localization := Quotient.functor _
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
⊢ G.Full

Tactic:
haveI : G.Full := Quotient.full_functor _
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this_1 : G.Full
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
rcases : ∀ (X : C) (f : Quotient.mk (r := relations W) (LocQuiver.mk (W := W) X) ⟶ Y), ⊤ f → P f
⊢ P f

Tactic:
rcases X with ⟨⟨X⟩⟩
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
Y : W.Localization
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this_1 : G.Full
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
X : C
f : Quotient.mk (r := relations W) (LocQuiver.mk (W := W) X) ⟶ Y
h : ⊤ f
rcases :
  ∀ (Y : C)
    (f :
      Quiver.Hom (V := W.Localization) (Quotient.mk (r := relations W) (LocQuiver.mk (W := W) X))
        (Quotient.mk (r := relations W) (LocQuiver.mk (W := W) Y))),
    ⊤ f → P f
⊢ P f

Tactic:
rcases Y with ⟨⟨Y⟩⟩
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this_1 : G.Full
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
X Y : C
f :
  Quiver.Hom (V := W.Localization) (Quotient.mk (r := relations W) (LocQuiver.mk (W := W) X))
    (Quotient.mk (r := relations W) (LocQuiver.mk (W := W) Y))
h : ⊤ f
⊢ P f

Tactic:
simpa only [Functor.map_preimage] using this _ _ (G.preimage f)

Premises used: CategoryTheory.Functor.preimage, CategoryTheory.Functor.map_preimage
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h_1 : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
h : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
⊢ P f

Tactic:
suffices ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f) by
      rcases X with ⟨⟨X⟩⟩
      rcases Y with ⟨⟨Y⟩⟩
      simpa only [Functor.map_preimage] using this _ _ (G.preimage f)
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂ : Paths (LocQuiver W)
⊢ P (X := G.obj X₁) (G.map Quiver.Path.nil)

Tactic:
simpa only [Functor.map_id] using hP₁ (𝟙 X₁.obj)

Premises used: CategoryTheory.Localization.Construction.LocQuiver.obj, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map_id
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h_1 : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂_1 X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path.{uC', uC} X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
h : P (G.map (p.cons g))
⊢ P (G.map (p.cons g))

Tactic:
let p' : X₁ ⟶ X₂ := p
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂_1 X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path.{uC', uC} X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ Quiver.Path.cons p' g = p' ≫ g.toPath

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h_1 : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂_1 X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path.{uC', uC} X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
h : P (G.map p' ≫ G.map g.toPath)
⊢ P (G.map (p.cons g))

Tactic:
rw [show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl, G.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂_1 X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path.{uC', uC} X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map p' ≫ G.map g.toPath)

Tactic:
P.comp_mem _ _ hp ?_

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h_1 : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂_1 X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path.{uC', uC} X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
h : P (G.map g.toPath)
⊢ P (G.map p' ≫ G.map g.toPath)

Tactic:
refine P.comp_mem _ _ hp ?_

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h_1 : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂_1 X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path.{uC', uC} X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
h : ∀ (g : X₂.obj (W := W) ⟶ X₃.obj (W := W)), P (X := G.obj X₂) (Y := G.obj X₃) (G.map (Quiver.Hom.toPath (Sum.inl g)))
h₁ :
  ∀ (g : X₃.obj (W := W) ⟶ X₂.obj (W := W)) (hg : W g),
    P (X := G.obj X₂) (Y := G.obj X₃)
      (G.map (Quiver.Hom.toPath (Sum.inr (Subtype.mk (p := fun (f : X₃.obj (W := W) ⟶ X₂.obj (W := W)) ↦ W f) g hg))))
⊢ P (G.map g.toPath)

Tactic:
rcases g with (g | ⟨g, hg⟩)
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂_1 X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path.{uC', uC} X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₂.obj (W := W) ⟶ X₃.obj (W := W)
⊢ P (X := G.obj X₂) (Y := G.obj X₃) (G.map (Quiver.Hom.toPath (Sum.inl g)))

Tactic:
apply hP₁
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂_1 X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path.{uC', uC} X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₃.obj (W := W) ⟶ X₂.obj (W := W)
hg : W g
⊢ P (X := G.obj X₂) (Y := G.obj X₃)
    (G.map (Quiver.Hom.toPath (Sum.inr (Subtype.mk (p := fun (f : X₃.obj (W := W) ⟶ X₂.obj (W := W)) ↦ W f) g hg))))

Tactic:
apply hP₂
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv (W := W) w hw)
X Y : W.Localization
f : X ⟶ Y
h_1 : ⊤ f
G : Paths (LocQuiver W) ⥤ W.Localization := Quotient.functor (relations W)
this : G.Full
X₁ X₂ : Paths (LocQuiver W)
p : X₁ ⟶ X₂
h : P (X := G.obj X₁) (G.map Quiver.Path.nil)
h₁ :
  ∀ {X₂ X₃ : Paths (LocQuiver W)} (p : Quiver.Path.{uC', uC} X₁ X₂) (g : X₂ ⟶ X₃) (hp : P (G.map p)),
    P (G.map (p.cons g))
⊢ P (G.map p)

Tactic:
induction p with
    | nil => simpa only [Functor.map_id] using hP₁ (𝟙 X₁.obj)
    | @cons X₂ X₃ p g hp =>
      let p' : X₁ ⟶ X₂ := p
      rw [show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl, G.map_comp]
      refine P.comp_mem _ _ hp ?_
      rcases g with (g | ⟨g, hg⟩)
      · apply hP₁
      · apply hP₂

Premises used: CategoryTheory.Localization.Construction.LocQuiver.obj, CategoryTheory.CategoryStruct.id, CategoryTheory.Functor.map_id, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
P : MorphismProperty W.Localization
inst_1 : P.IsStableUnderComposition
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)
hP₂ : ∀ ⦃X Y : W.Localization⦄ (e : X ≅ Y), P e.hom → P e.inv
⊢ P = ⊤

Tactic:
morphismProperty_eq_top P hP₁ (fun _ _ w _ => hP₂ _ (hP₁ w))

Premises used: CategoryTheory.Localization.Construction.morphismProperty_eq_top, CategoryTheory.Localization.Construction.wIso
-- 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₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
X : C
simp : τ.app ((objEquiv W).invFun (W.Q.obj X)) = τ.app X
⊢ app (W := W) τ (W.Q.obj X) = τ.app X

Tactic:
simp only [app, eqToHom_refl, comp_id, id_comp]

Premises used: CategoryTheory.Localization.Construction.NatTransExtension.app, CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, 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
F₁ F₂ : W.Localization ⥤ D
τ : W.Q ⋙ F₁ ⟶ W.Q ⋙ F₂
X : C
⊢ τ.app ((objEquiv W).invFun (W.Q.obj X)) = τ.app X

Tactic:
rfl