awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
hW₂₃' : W₂' ≤ W₃.map W₁.Q
⊢ StrictUniversalPropertyFixedTarget (W₁.Q ⋙ W₂'.Q) W₃ W₃.Localization

Tactic:
exact (StrictUniversalPropertyFixedTarget.comp
        (strictUniversalPropertyFixedTargetQ W₁ _)
        (strictUniversalPropertyFixedTargetQ W₂' _) W₃ hW₃' hW₁₃ hW₂₃')

Premises used: CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ, CategoryTheory.Localization.StrictUniversalPropertyFixedTarget.comp
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
hW₂₃' : W₂' ≤ W₃.map W₁.Q
⊢ (W₁.Q ⋙ W₂'.Q).IsLocalization W₃

Tactic:
have : (W₁.Q ⋙ W₂'.Q).IsLocalization W₃ := by
    refine IsLocalization.mk' _ _ ?_ ?_
    all_goals
      exact (StrictUniversalPropertyFixedTarget.comp
        (strictUniversalPropertyFixedTargetQ W₁ _)
        (strictUniversalPropertyFixedTargetQ W₂' _) W₃ hW₃' hW₁₃ hW₂₃')
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this_1 : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
hW₂₃' : W₂' ≤ W₃.map W₁.Q
this : (W₁.Q ⋙ W₂'.Q).IsLocalization W₃
⊢ (L₁ ⋙ L₂).IsLocalization W₃

Tactic:
IsLocalization.of_equivalence_target _ W₃ _ E₃.symm iso

Premises used: CategoryTheory.Functor.IsLocalization.of_equivalence_target, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
inst_3 : L₁.IsLocalization W₁
inst_4 : L₂.IsLocalization W₂
W₃ : MorphismProperty.{v₁, u₁} C₁
hW₃ : W₃.IsInvertedBy (L₁ ⋙ L₂)
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ ≤ W₃.map L₁
E₂ : C₂ ≌ W₁.Localization := uniq L₁ W₁.Q W₁
W₂' : MorphismProperty W₁.Localization := W₂.map E₂.functor
Φ : LocalizerMorphism W₂ W₂' := LocalizerMorphism.mk (W₁ := W₂) (W₂ := W₂') E₂.functor ⋯
this_1 : Φ.IsLocalizedEquivalence (W₁ := W₂) (W₂ := W₂')
E₃ : C₃ ≌ W₂'.Localization := (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q).asEquivalence
iso : (W₁.Q ⋙ W₂'.Q) ⋙ E₃.inverse ≅ L₁ ⋙ L₂ :=
  Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
    (Trans.trans (r := Iso) (s := Iso) (t := fun (x1 x2 : Functor.{v₁, v₃, u₁, u₃} C₁ C₃) ↦ x1 ≅ x2)
      (W₁.Q.associator W₂'.Q E₃.inverse ≪≫
        isoWhiskerRight (Iso.symm (compUniqFunctor L₁ W₁.Q W₁)) (W₂'.Q ⋙ E₃.inverse) ≪≫
          L₁.associator (uniq L₁ W₁.Q W₁).functor (W₂'.Q ⋙ E₃.inverse))
      (L₁.isoWhiskerLeft
        ((E₂.functor.associator W₂'.Q E₃.inverse).symm ≪≫
          isoWhiskerRight
              (CatCommSq.iso (Φ.functor (W₁ := W₂) (W₂ := W₂')) L₂ W₂'.Q
                (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q))
              E₃.inverse ≪≫
            L₂.associator (Φ.localizedFunctor (W₁ := W₂) (W₂ := W₂') L₂ W₂'.Q) E₃.inverse)))
    (L₁.isoWhiskerLeft (L₂.isoWhiskerLeft E₃.unitIso.symm ≪≫ L₂.rightUnitor))
hW₃' : W₃.IsInvertedBy (W₁.Q ⋙ W₂'.Q)
hW₂₃' : W₂' ≤ W₃.map W₁.Q
this : (W₁.Q ⋙ W₂'.Q).IsLocalization W₃
⊢ (L₁ ⋙ L₂).IsLocalization W₃

Tactic:
exact IsLocalization.of_equivalence_target _ W₃ _ E₃.symm iso

Premises used: CategoryTheory.Functor.IsLocalization.of_equivalence_target, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₁, u₁} C₁
inst_3 : L₁.IsLocalization W₁
inst_4 : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
X Y : C₁
f : X ⟶ Y
hf : W₃ f
⊢ W₂ (L₁.map f)

Tactic:
simpa only [hW₂₃] using W₃.map_mem_map _ _ hf

Premises used: CategoryTheory.MorphismProperty.map_mem_map
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₁, u₁} C₁
inst_3 : L₁.IsLocalization W₁
inst_4 : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
rw rw₁ : W₃.map L₁ ≤ W₃.map L₁
⊢ W₂ ≤ W₃.map L₁

Tactic:
rw [hW₂₃]
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₁, u₁} C₁
inst_3 : L₁.IsLocalization W₁
inst_4 : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
⊢ (L₁ ⋙ W₂.Q).IsLocalization W₃

Tactic:
have : (L₁ ⋙ W₂.Q).IsLocalization W₃ :=
      comp L₁ W₂.Q W₁ W₂ W₃ (fun X Y f hf => Localization.inverts W₂.Q W₂ _
        (by simpa only [hW₂₃] using W₃.map_mem_map _ _ hf)) hW₁₃
        (by rw [hW₂₃])
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₁, u₁} C₁
inst_3 : L₁.IsLocalization W₁
inst_4 : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
this : (L₁ ⋙ W₂.Q).IsLocalization W₃
⊢ L₂.IsLocalization W₂

Tactic:
IsLocalization.of_equivalence_target W₂.Q W₂ L₂
      (Localization.uniq (L₁ ⋙ W₂.Q) (L₁ ⋙ L₂) W₃)
      (liftNatIso L₁ W₁ _ _ _ _
        ((Functor.associator _ _ _).symm ≪≫
          Localization.compUniqFunctor (L₁ ⋙ W₂.Q) (L₁ ⋙ L₂) W₃))

Premises used: CategoryTheory.Localization.liftNatIso, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.Functor.associator, CategoryTheory.Localization.uniq, CategoryTheory.Localization.compUniqFunctor, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.IsLocalization.of_equivalence_target
-- Module: Mathlib.CategoryTheory.Localization.Composition
Goal:
C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst : Category.{v₁, u₁} C₁
inst_1 : Category.{v₂, u₂} C₂
inst_2 : Category.{v₃, u₃} C₃
L₁ : Functor.{v₁, v₂, u₁, u₂} C₁ C₂
L₂ : Functor.{v₂, v₃, u₂, u₃} C₂ C₃
W₁ : MorphismProperty.{v₁, u₁} C₁
W₂ : MorphismProperty.{v₂, u₂} C₂
W₃ : MorphismProperty.{v₁, u₁} C₁
inst_3 : L₁.IsLocalization W₁
inst_4 : (L₁ ⋙ L₂).IsLocalization W₃
hW₁₃ : W₁ ≤ W₃
hW₂₃ : W₂ = W₃.map L₁
this : (L₁ ⋙ W₂.Q).IsLocalization W₃
⊢ L₂.IsLocalization W₂

Tactic:
exact IsLocalization.of_equivalence_target W₂.Q W₂ L₂
      (Localization.uniq (L₁ ⋙ W₂.Q) (L₁ ⋙ L₂) W₃)
      (liftNatIso L₁ W₁ _ _ _ _
        ((Functor.associator _ _ _).symm ≪≫
          Localization.compUniqFunctor (L₁ ⋙ W₂.Q) (L₁ ⋙ L₂) W₃))

Premises used: CategoryTheory.Localization.liftNatIso, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.comp, CategoryTheory.Functor.associator, CategoryTheory.Localization.uniq, CategoryTheory.Localization.compUniqFunctor, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Functor.IsLocalization.of_equivalence_target
-- 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
X Y : C
w : X ⟶ Y
hw : W w
⊢ Quiver.Hom (V := Paths (LocQuiver W)) (LocQuiver.mk (W := W) Y) (LocQuiver.mk (W := W) X)

Tactic:
exact (Paths.of _).map (Sum.inr ⟨w, hw⟩)

Premises used: Prefunctor.map, CategoryTheory.Paths.of
-- Module: Mathlib.CategoryTheory.Localization.Construction
Goal:
C : Type uC
inst : Category.{uC', uC} C
W : MorphismProperty.{uC', uC} C
⊢ W.IsInvertedBy W.Q

Tactic:
fun _ _ w hw =>
  (Localization.Construction.wIso w hw).isIso_hom

Premises used: CategoryTheory.MorphismProperty.IsInvertedBy, CategoryTheory.Iso.isIso_hom, 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
G : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
X Y : LocQuiver W
f : X.obj (W := W) ⟶ Y.obj (W := W)
⊢ G.obj (X.obj (W := W)) ⟶ G.obj (Y.obj (W := W))

Tactic:
exact G.map f

Premises used: CategoryTheory.Functor.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 : Functor.{uC', uD', uC, uD} C D
hG : W.IsInvertedBy G
X Y : LocQuiver W
g : Y.obj (W := W) ⟶ X.obj (W := W)
hg : W g
⊢ IsIso (G.map g)

Tactic:
haveI := hG g hg
-- 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 : LocQuiver W
g : Y.obj (W := W) ⟶ X.obj (W := W)
hg : W g
this : IsIso (G.map g)
⊢ G.obj (X.obj (W := W)) ⟶ G.obj (Y.obj (W := W))

Tactic:
exact inv (G.map g)

Premises used: CategoryTheory.Functor.map, CategoryTheory.inv
-- 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 : C
f₁ f₂ : Quiver.Hom (V := Paths (LocQuiver W)) (LocQuiver.mk (W := W) X) (LocQuiver.mk (W := W) Y)
r : relations W f₁ f₂
id :
  ∀ ⦃X_1 Y : Paths (LocQuiver W)⦄,
    (liftToPathCategory (W := W) G hG).map (ψ₁ W (𝟙 X)) = (liftToPathCategory (W := W) G hG).map (𝟙 (ιPaths W X))
comp :
  ∀ ⦃X_1 Y_1 : Paths (LocQuiver W)⦄ {Y_2 : C} (f : X ⟶ Y_2) (g : Y_2 ⟶ Y),
    (liftToPathCategory (W := W) G hG).map (ψ₁ W (f ≫ g)) = (liftToPathCategory (W := W) G hG).map (ψ₁ W f ≫ ψ₁ W g)
Winv₁ :
  ∀ ⦃X_1 Y : Paths (LocQuiver W)⦄ {Y : C} (w : X ⟶ Y) (hw : W w),
    (liftToPathCategory (W := W) G hG).map (ψ₁ W w ≫ ψ₂ W w hw) =
      (liftToPathCategory (W := W) G hG).map (𝟙 (ιPaths W X))
Winv₂ :
  ∀ ⦃X_1 Y : Paths (LocQuiver W)⦄ {X_2 : C} (w : X_2 ⟶ X) (hw : W w),
    (liftToPathCategory (W := W) G hG).map (ψ₂ W w hw ≫ ψ₁ W w) =
      (liftToPathCategory (W := W) G hG).map (𝟙 (ιPaths W X))
⊢ (liftToPathCategory (W := W) G hG).map f₁ = (liftToPathCategory (W := W) G hG).map f₂

Tactic:
rcases r with ⟨⟩
-- 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 : C
X Y : Paths (LocQuiver W)
⊢ (liftToPathCategory (W := W) G hG).map (ψ₁ W (𝟙 X_1)) = (liftToPathCategory (W := W) G hG).map (𝟙 (ιPaths W X_1))

Tactic:
aesop
-- 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 : C
X Y : Paths (LocQuiver W)
⊢ (liftToPathCategory (W := W) G hG).map (ψ₁ W (𝟙 X_1)) = (liftToPathCategory (W := W) G hG).map (𝟙 (ιPaths W X_1))

Tactic:
all_goals aesop
-- 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_1 : C
X Y : Paths (LocQuiver W)
Y_2 : C
f : X_1 ⟶ Y_2
g : Y_2 ⟶ Y_1
⊢ (liftToPathCategory (W := W) G hG).map (ψ₁ W (f ≫ g)) = (liftToPathCategory (W := W) G hG).map (ψ₁ W f ≫ ψ₁ W g)

Tactic:
aesop
-- 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_1 : C
X Y : Paths (LocQuiver W)
Y_2 : C
f : X_1 ⟶ Y_2
g : Y_2 ⟶ Y_1
⊢ (liftToPathCategory (W := W) G hG).map (ψ₁ W (f ≫ g)) = (liftToPathCategory (W := W) G hG).map (ψ₁ W f ≫ ψ₁ W g)

Tactic:
all_goals aesop
-- 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 : C
X Y : Paths (LocQuiver W)
Y_1 : C
w : X_1 ⟶ Y_1
hw : W w
⊢ (liftToPathCategory (W := W) G hG).map (ψ₁ W w ≫ ψ₂ W w hw) =
    (liftToPathCategory (W := W) G hG).map (𝟙 (ιPaths W X_1))

Tactic:
aesop
-- 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 : C
X Y : Paths (LocQuiver W)
Y_1 : C
w : X_1 ⟶ Y_1
hw : W w
⊢ (liftToPathCategory (W := W) G hG).map (ψ₁ W w ≫ ψ₂ W w hw) =
    (liftToPathCategory (W := W) G hG).map (𝟙 (ιPaths W X_1))

Tactic:
all_goals aesop
-- 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 : C
X Y : Paths (LocQuiver W)
X_2 : C
w : X_2 ⟶ X_1
hw : W w
⊢ (liftToPathCategory (W := W) G hG).map (ψ₂ W w hw ≫ ψ₁ W w) =
    (liftToPathCategory (W := W) G hG).map (𝟙 (ιPaths W X_1))

Tactic:
aesop
-- 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 : C
X Y : Paths (LocQuiver W)
X_2 : C
w : X_2 ⟶ X_1
hw : W w
⊢ (liftToPathCategory (W := W) G hG).map (ψ₂ W w hw ≫ ψ₁ W w) =
    (liftToPathCategory (W := W) G hG).map (𝟙 (ιPaths W X_1))

Tactic:
all_goals aesop
-- 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 : C
f : X ⟶ Y
simp : (lift (W := W) G hG).map (W.Q.map f) = G.map f
⊢ (W.Q ⋙ lift (W := W) G hG).map f = eqToHom ⋯ ≫ G.map f ≫ eqToHom ⋯

Tactic:
simp only [Functor.comp_map, eqToHom_refl, comp_id, id_comp]

Premises used: CategoryTheory.eqToHom_refl, CategoryTheory.Category.comp_id, CategoryTheory.Functor.comp_map, 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 Y : C
f : X ⟶ Y
dsimp : composePath (G.map f).toPath = G.map f
⊢ (lift (W := W) G hG).map (W.Q.map f) = G.map f

Tactic:
dsimp [MorphismProperty.Q, Quot.liftOn, Quotient.functor]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Quotient.functor, Quot.liftOn
-- 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 : C
f : X ⟶ Y
rw rw₁ : G.map f = G.map f
⊢ composePath (G.map f).toPath = G.map f

Tactic:
rw [composePath_toPath]

Premises used: CategoryTheory.composePath_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₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ G₁ = G₂

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

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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
X : C
⊢ G₁.obj (Quotient.mk (r := relations W) (LocQuiver.mk (W := W) X)) =
    G₂.obj (Quotient.mk (r := relations W) (LocQuiver.mk (W := W) 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₁ G₂ : W.Localization ⥤ D
h : W.Q ⋙ G₁ = W.Q ⋙ G₂
h' : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
X Y : C
f_1 :
  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 :
  Quiver.Hom (V := Paths (LocQuiver W))
    (Quotient.as (r := relations W) (Quotient.mk (r := relations W) (LocQuiver.mk (W := W) X)))
    (Quotient.as (r := relations W) (Quotient.mk (r := relations W) (LocQuiver.mk (W := W) Y)))
⊢ G₁.map (Quot.mk (HomRel.CompClosure (relations W)) f) =
    eqToHom ⋯ ≫ G₂.map (Quot.mk (HomRel.CompClosure (relations W)) f) ≫ eqToHom ⋯

Tactic:
apply Functor.congr_hom h'

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₂
suffices : Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂
⊢ G₁ = G₂

Tactic:
suffices h' : Quotient.functor _ ⋙ G₁ = Quotient.functor _ ⋙ G₂ by
    refine Functor.ext ?_ ?_
    · rintro ⟨⟨X⟩⟩
      apply Functor.congr_obj h
    · rintro ⟨⟨X⟩⟩ ⟨⟨Y⟩⟩ ⟨f⟩
      apply Functor.congr_hom h'
-- 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₂
⊢ Quotient.functor (relations W) ⋙ G₁ = Quotient.functor (relations W) ⋙ G₂

Tactic:
Paths.ext_functor ?_ ?_

Premises used: CategoryTheory.Paths.ext_functor