awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
W : MorphismProperty.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
inst_3 : L.IsLocalization W
inst_4 : L'.IsLocalization W
X Y : C
f : L.obj X ⟶ L.obj Y
dsimp :
  StructuredArrow.mk (Y := Y)
      (((homEquiv W L' L : Equiv.{v_3 + 1, v_2 + 1} (L'.obj X ⟶ L'.obj Y) (L.obj X ⟶ L.obj Y)) :
          (a : L'.obj X ⟶ L'.obj Y) → L.obj X ⟶ L.obj Y)
        (((homEquiv W L L' : Equiv.{v_2 + 1, v_3 + 1} (L.obj X ⟶ L.obj Y) (L'.obj X ⟶ L'.obj Y)) :
            (a : L.obj X ⟶ L.obj Y) → L'.obj X ⟶ L'.obj Y)
          f)) =
    StructuredArrow.mk f
⊢ (fun (f : StructuredArrow (L'.obj X) L') ↦
        (StructuredArrow.mk (Y := f.right)
            (((homEquiv W L' L : Equiv.{v_3 + 1, v_2 + 1} (L'.obj X ⟶ L'.obj f.right) (L.obj X ⟶ L.obj f.right)) :
                (a : L'.obj X ⟶ L'.obj f.right) → L.obj X ⟶ L.obj f.right)
              f.hom) :
          StructuredArrow (L.obj X) L))
      ((fun (f : StructuredArrow (L.obj X) L) ↦
          (StructuredArrow.mk (Y := f.right)
              (((homEquiv W L L' : Equiv.{v_2 + 1, v_3 + 1} (L.obj X ⟶ L.obj f.right) (L'.obj X ⟶ L'.obj f.right)) :
                  (a : L.obj X ⟶ L.obj f.right) → L'.obj X ⟶ L'.obj f.right)
                f.hom) :
            StructuredArrow (L'.obj X) L'))
        (StructuredArrow.mk f)) =
    StructuredArrow.mk f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
W : MorphismProperty.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
inst_3 : L.IsLocalization W
inst_4 : L'.IsLocalization W
X Y : C
f : L.obj X ⟶ L.obj Y
rw :
  StructuredArrow.mk (Y := Y)
      (((Equiv.symm (homEquiv W L L') : Equiv.{v_3 + 1, v_2 + 1} (L'.obj X ⟶ L'.obj Y) (L.obj X ⟶ L.obj Y)) :
          (a : L'.obj X ⟶ L'.obj Y) → L.obj X ⟶ L.obj Y)
        (((homEquiv W L L' : Equiv.{v_2 + 1, v_3 + 1} (L.obj X ⟶ L.obj Y) (L'.obj X ⟶ L'.obj Y)) :
            (a : L.obj X ⟶ L.obj Y) → L'.obj X ⟶ L'.obj Y)
          f)) =
    StructuredArrow.mk f
rw₁ rw₂ : StructuredArrow.mk f = StructuredArrow.mk f
⊢ StructuredArrow.mk (Y := Y)
      (((homEquiv W L' L : Equiv.{v_3 + 1, v_2 + 1} (L'.obj X ⟶ L'.obj Y) (L.obj X ⟶ L.obj Y)) :
          (a : L'.obj X ⟶ L'.obj Y) → L.obj X ⟶ L.obj Y)
        (((homEquiv W L L' : Equiv.{v_2 + 1, v_3 + 1} (L.obj X ⟶ L.obj Y) (L'.obj X ⟶ L'.obj Y)) :
            (a : L.obj X ⟶ L.obj Y) → L'.obj X ⟶ L'.obj Y)
          f)) =
    StructuredArrow.mk f

Tactic:
rw [← homEquiv_symm_apply, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, CategoryTheory.Localization.homEquiv_symm_apply
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
W : MorphismProperty.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
inst_3 : L.IsLocalization W
inst_4 : L'.IsLocalization W
X : C
f : StructuredArrow (L'.obj X) L'
obtain :
  ∀ (Y : C) (f : L'.obj X ⟶ L'.obj Y),
    (fun (f : StructuredArrow (L.obj X) L) ↦
          (StructuredArrow.mk (Y := f.right)
              (((homEquiv W L L' : Equiv.{v_2 + 1, v_3 + 1} (L.obj X ⟶ L.obj f.right) (L'.obj X ⟶ L'.obj f.right)) :
                  (a : L.obj X ⟶ L.obj f.right) → L'.obj X ⟶ L'.obj f.right)
                f.hom) :
            StructuredArrow (L'.obj X) L'))
        ((fun (f : StructuredArrow (L'.obj X) L') ↦
            (StructuredArrow.mk (Y := f.right)
                (((homEquiv W L' L : Equiv.{v_3 + 1, v_2 + 1} (L'.obj X ⟶ L'.obj f.right) (L.obj X ⟶ L.obj f.right)) :
                    (a : L'.obj X ⟶ L'.obj f.right) → L.obj X ⟶ L.obj f.right)
                  f.hom) :
              StructuredArrow (L.obj X) L))
          (StructuredArrow.mk f)) =
      StructuredArrow.mk f
⊢ (fun (f : StructuredArrow (L.obj X) L) ↦
        (StructuredArrow.mk (Y := f.right)
            (((homEquiv W L L' : Equiv.{v_2 + 1, v_3 + 1} (L.obj X ⟶ L.obj f.right) (L'.obj X ⟶ L'.obj f.right)) :
                (a : L.obj X ⟶ L.obj f.right) → L'.obj X ⟶ L'.obj f.right)
              f.hom) :
          StructuredArrow (L'.obj X) L'))
      ((fun (f : StructuredArrow (L'.obj X) L') ↦
          (StructuredArrow.mk (Y := f.right)
              (((homEquiv W L' L : Equiv.{v_3 + 1, v_2 + 1} (L'.obj X ⟶ L'.obj f.right) (L.obj X ⟶ L.obj f.right)) :
                  (a : L'.obj X ⟶ L'.obj f.right) → L.obj X ⟶ L.obj f.right)
                f.hom) :
            StructuredArrow (L.obj X) L))
        f) =
    f

Tactic:
obtain ⟨Y, f, rfl⟩ := f.mk_surjective

Premises used: CategoryTheory.StructuredArrow.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
W : MorphismProperty.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
inst_3 : L.IsLocalization W
inst_4 : L'.IsLocalization W
X Y : C
f : L'.obj X ⟶ L'.obj Y
dsimp :
  StructuredArrow.mk (Y := Y)
      (((homEquiv W L L' : Equiv.{v_2 + 1, v_3 + 1} (L.obj X ⟶ L.obj Y) (L'.obj X ⟶ L'.obj Y)) :
          (a : L.obj X ⟶ L.obj Y) → L'.obj X ⟶ L'.obj Y)
        (((homEquiv W L' L : Equiv.{v_3 + 1, v_2 + 1} (L'.obj X ⟶ L'.obj Y) (L.obj X ⟶ L.obj Y)) :
            (a : L'.obj X ⟶ L'.obj Y) → L.obj X ⟶ L.obj Y)
          f)) =
    StructuredArrow.mk f
⊢ (fun (f : StructuredArrow (L.obj X) L) ↦
        (StructuredArrow.mk (Y := f.right)
            (((homEquiv W L L' : Equiv.{v_2 + 1, v_3 + 1} (L.obj X ⟶ L.obj f.right) (L'.obj X ⟶ L'.obj f.right)) :
                (a : L.obj X ⟶ L.obj f.right) → L'.obj X ⟶ L'.obj f.right)
              f.hom) :
          StructuredArrow (L'.obj X) L'))
      ((fun (f : StructuredArrow (L'.obj X) L') ↦
          (StructuredArrow.mk (Y := f.right)
              (((homEquiv W L' L : Equiv.{v_3 + 1, v_2 + 1} (L'.obj X ⟶ L'.obj f.right) (L.obj X ⟶ L.obj f.right)) :
                  (a : L'.obj X ⟶ L'.obj f.right) → L.obj X ⟶ L.obj f.right)
                f.hom) :
            StructuredArrow (L.obj X) L))
        (StructuredArrow.mk f)) =
    StructuredArrow.mk f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
D' : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} D'
W : MorphismProperty.{v_1, u_1} C
L : Functor.{v_1, v_2, u_1, u_2} C D
L' : Functor.{v_1, v_3, u_1, u_3} C D'
inst_3 : L.IsLocalization W
inst_4 : L'.IsLocalization W
X Y : C
f : L'.obj X ⟶ L'.obj Y
rw :
  StructuredArrow.mk (Y := Y)
      (((Equiv.symm (homEquiv W L' L) : Equiv.{v_2 + 1, v_3 + 1} (L.obj X ⟶ L.obj Y) (L'.obj X ⟶ L'.obj Y)) :
          (a : L.obj X ⟶ L.obj Y) → L'.obj X ⟶ L'.obj Y)
        (((homEquiv W L' L : Equiv.{v_3 + 1, v_2 + 1} (L'.obj X ⟶ L'.obj Y) (L.obj X ⟶ L.obj Y)) :
            (a : L'.obj X ⟶ L'.obj Y) → L.obj X ⟶ L.obj Y)
          f)) =
    StructuredArrow.mk f
rw₁ rw₂ : StructuredArrow.mk f = StructuredArrow.mk f
⊢ StructuredArrow.mk (Y := Y)
      (((homEquiv W L L' : Equiv.{v_2 + 1, v_3 + 1} (L.obj X ⟶ L.obj Y) (L'.obj X ⟶ L'.obj Y)) :
          (a : L.obj X ⟶ L.obj Y) → L'.obj X ⟶ L'.obj Y)
        (((homEquiv W L' L : Equiv.{v_3 + 1, v_2 + 1} (L'.obj X ⟶ L'.obj Y) (L.obj X ⟶ L.obj Y)) :
            (a : L'.obj X ⟶ L'.obj Y) → L.obj X ⟶ L.obj Y)
          f)) =
    StructuredArrow.mk f

Tactic:
rw [← homEquiv_symm_apply, Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply, CategoryTheory.Localization.homEquiv_symm_apply
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
let : P g
⊢ P g

Tactic:
let X₀ : Paths (LocQuiver W) := ⟨X⟩
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := LocQuiver.mk (W := W) X
this : ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀), P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
obtain : ∀ (Y : C) (g : W.Q.obj X ⟶ W.Q.obj Y), P (StructuredArrow.mk g)
⊢ P g

Tactic:
obtain ⟨Y, g, rfl⟩ := g.mk_surjective

Premises used: CategoryTheory.StructuredArrow.mk_surjective, rfl
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
X₀ : Paths (LocQuiver W) := LocQuiver.mk (W := W) X
this : ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀), P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
Y : C
g : W.Q.obj X ⟶ W.Q.obj Y
obtain :
  ∀
    (g :
      Quiver.Hom (V := Paths (LocQuiver W)) (Prefunctor.obj (Paths.of (LocQuiver W)) (LocQuiver.mk (W := W) X))
        (Prefunctor.obj (Paths.of (LocQuiver W)) (LocQuiver.mk (W := W) Y))),
    P (StructuredArrow.mk ((Quotient.functor (relations W)).map g))
⊢ P (StructuredArrow.mk g)

Tactic:
obtain ⟨g, rfl⟩ := (Quotient.functor (relations W)).map_surjective g

Premises used: CategoryTheory.Quotient.functor, CategoryTheory.Localization.Construction.relations, rfl, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
X₀ : Paths (LocQuiver W) := LocQuiver.mk (W := W) X
this : ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀), P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
Y : C
g :
  Quiver.Hom (V := Paths (LocQuiver W)) (Prefunctor.obj (Paths.of (LocQuiver W)) (LocQuiver.mk (W := W) X))
    (Prefunctor.obj (Paths.of (LocQuiver W)) (LocQuiver.mk (W := W) Y))
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map g))

Tactic:
this g
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
X₀ : Paths (LocQuiver W) := LocQuiver.mk (W := W) X
this : ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀), P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
Y : C
g :
  Quiver.Hom (V := Paths (LocQuiver W)) (Prefunctor.obj (Paths.of (LocQuiver W)) (LocQuiver.mk (W := W) X))
    (Prefunctor.obj (Paths.of (LocQuiver W)) (LocQuiver.mk (W := W) Y))
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map g))

Tactic:
exact this g
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := LocQuiver.mk (W := W) X
suffices : ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀), P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
⊢ P g

Tactic:
suffices ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀),
      P (StructuredArrow.mk ((Quotient.functor (relations W)).map f)) by
    obtain ⟨Y, g, rfl⟩ := g.mk_surjective
    obtain ⟨g, rfl⟩ := (Quotient.functor (relations W)).map_surjective g
    exact this g
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := LocQuiver.mk (W := W) X
Y₀ : Paths (LocQuiver W)
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map Quiver.Path.nil))

Tactic:
hP₀

Premises used: CategoryTheory.Paths
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := LocQuiver.mk (W := W) X
Y₀ : Paths (LocQuiver W)
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map Quiver.Path.nil))

Tactic:
exact hP₀
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g_1 : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := LocQuiver.mk (W := W) X
Y₀ b c : Paths (LocQuiver W)
f : Quiver.Path.{v_1, u_1} X₀ b
g : b ⟶ c
hf : P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
cons :
  ∀ (g : b.obj (W := W) ⟶ c.obj (W := W)),
    P (StructuredArrow.mk ((Quotient.functor (relations W)).map (f.cons (Sum.inl g))))
cons₁ :
  ∀ (w : c.obj (W := W) ⟶ b.obj (W := W)) (hw : W w),
    P
      (StructuredArrow.mk
        ((Quotient.functor (relations W)).map
          (f.cons (Sum.inr (Subtype.mk (p := fun (f : c.obj (W := W) ⟶ b.obj (W := W)) ↦ W f) w hw)))))
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map (f.cons g)))

Tactic:
obtain (g | ⟨w, hw⟩) := g
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g_1 : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := LocQuiver.mk (W := W) X
Y₀ b c : Paths (LocQuiver W)
f : Quiver.Path.{v_1, u_1} X₀ b
hf : P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
g : b.obj (W := W) ⟶ c.obj (W := W)
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map (f.cons (Sum.inl g))))

Tactic:
hP₁ g _ hf

Premises used: CategoryTheory.Localization.Construction.ψ₁, CategoryTheory.Paths, Quiver.Hom.toPath, CategoryTheory.Quotient.comp, Quiver.Path.comp
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g_1 : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := LocQuiver.mk (W := W) X
Y₀ b c : Paths (LocQuiver W)
f : Quiver.Path.{v_1, u_1} X₀ b
hf : P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
g : b.obj (W := W) ⟶ c.obj (W := W)
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map (f.cons (Sum.inl g))))

Tactic:
exact hP₁ g _ hf
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := LocQuiver.mk (W := W) X
Y₀ b c : Paths (LocQuiver W)
f : Quiver.Path.{v_1, u_1} X₀ b
hf : P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
w : c.obj (W := W) ⟶ b.obj (W := W)
hw : W w
⊢ P
    (StructuredArrow.mk
      ((Quotient.functor (relations W)).map
        (f.cons (Sum.inr (Subtype.mk (p := fun (f : c.obj (W := W) ⟶ b.obj (W := W)) ↦ W f) w hw)))))

Tactic:
simpa only [← Construction.wInv_eq_isoOfHom_inv w hw] using hP₂ w hw _ hf

Premises used: CategoryTheory.Localization.Construction.wInv_eq_isoOfHom_inv
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
W : MorphismProperty.{v_1, u_1} C
X : C
P : StructuredArrow (W.Q.obj X) W.Q → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (W.Q.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : W.Q.obj X ⟶ W.Q.obj Y₁),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ W.Q.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : W.Q.obj X ⟶ W.Q.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom W.Q W w hw).inv))
g : StructuredArrow (W.Q.obj X) W.Q
X₀ : Paths (LocQuiver W) := LocQuiver.mk (W := W) X
Y₀ : Paths (LocQuiver W)
f : X₀ ⟶ Y₀
nil : P (StructuredArrow.mk ((Quotient.functor (relations W)).map Quiver.Path.nil))
cons :
  ∀ {b c : Paths (LocQuiver W)} (f : Quiver.Path.{v_1, u_1} X₀ b) (g : b ⟶ c)
    (hf : P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))),
    P (StructuredArrow.mk ((Quotient.functor (relations W)).map (f.cons g)))
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))

Tactic:
induction f with
  | nil => exact hP₀
  | cons f g hf =>
      obtain (g | ⟨w, hw⟩) := g
      · exact hP₁ g _ hf
      · simpa only [← Construction.wInv_eq_isoOfHom_inv w hw] using hP₂ w hw _ hf
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
let : P g
⊢ P g

Tactic:
let P' : StructuredArrow (W.Q.obj X) W.Q → Prop :=
    fun g ↦ P (structuredArrowEquiv W W.Q L g)
-- Module: Mathlib.CategoryTheory.Localization.StructuredArrow
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
L : Functor.{v_1, v_2, u_1, u_2} C D
W : MorphismProperty.{v_1, u_1} C
inst_2 : L.IsLocalization W
X : C
P : StructuredArrow (L.obj X) L → Prop
hP₀ : P (StructuredArrow.mk (𝟙 (L.obj X)))
hP₁ :
  ∀ ⦃Y₁ Y₂ : C⦄ (f : Y₁ ⟶ Y₂) (φ : L.obj X ⟶ L.obj Y₁), P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ L.map f))
hP₂ :
  ∀ ⦃Y₁ Y₂ : C⦄ (w : Y₁ ⟶ Y₂) (hw : W w) (φ : L.obj X ⟶ L.obj Y₂),
    P (StructuredArrow.mk φ) → P (StructuredArrow.mk (φ ≫ (isoOfHom L W w hw).inv))
g : StructuredArrow (L.obj X) L
P' : StructuredArrow (W.Q.obj X) W.Q → Prop :=
  fun (g : StructuredArrow (W.Q.obj X) W.Q) ↦
    P ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L) g)
rw :
  P
    ((structuredArrowEquiv W W.Q L : (a : StructuredArrow (W.Q.obj X) W.Q) → StructuredArrow (L.obj X) L)
      ((Equiv.symm (structuredArrowEquiv W W.Q L) : (a : StructuredArrow (L.obj X) L) → StructuredArrow (W.Q.obj X) W.Q)
        g))
⊢ P g

Tactic:
rw [← (structuredArrowEquiv W W.Q L).apply_symm_apply g]

Premises used: Equiv.apply_symm_apply, CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.structuredArrowEquiv