awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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
⊢ (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'))
        f) =
    f
have 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_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: obtain ⟨Y, f, rfl⟩ := f.mk_surjective
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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
⊢ (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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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
⊢ 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
have 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
Tactic: rw [← homEquiv_symm_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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
⊢ 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
have rw₁ : StructuredArrow.mk f = StructuredArrow.mk f
Tactic: rw [← homEquiv_symm_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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'
⊢ (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
have 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
Tactic: obtain ⟨Y, f, rfl⟩ := f.mk_surjective
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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
⊢ (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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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
⊢ 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
have 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
Tactic: rw [← homEquiv_symm_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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
⊢ 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
have rw₁ : StructuredArrow.mk f = StructuredArrow.mk f
Tactic: rw [← homEquiv_symm_apply, Equiv.symm_apply_apply]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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))
⊢ P g
have obtain : ∀ (Y : C) (g : W.Q.obj X ⟶ W.Q.obj Y), P (StructuredArrow.mk g)
Tactic: obtain ⟨Y, g, rfl⟩ := g.mk_surjective
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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
⊢ P (StructuredArrow.mk g)
have 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))
Tactic: obtain ⟨g, rfl⟩ := (Quotient.functor (relations W)).map_surjective g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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
⊢ P g
have suffices : ∀ ⦃Y₀ : Paths (LocQuiver W)⦄ (f : X₀ ⟶ Y₀), P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
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
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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))
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map (f.cons g)))
have cons : ∀ (g : b.obj (W := W) ⟶ c.obj (W := W)),
  P (StructuredArrow.mk ((Quotient.functor (relations W)).map (f.cons (Sum.inl g))))
Tactic: obtain (g | ⟨w, hw⟩) := g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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))))
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map (f.cons g)))
have 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)))))
Tactic: obtain (g | ⟨w, hw⟩) := g
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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₀
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
have nil : P (StructuredArrow.mk ((Quotient.functor (relations W)).map Quiver.Path.nil))
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
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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))
⊢ P (StructuredArrow.mk ((Quotient.functor (relations W)).map f))
have 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)))
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
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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)
⊢ P g
have 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))
Tactic: rw [← (structuredArrowEquiv W W.Q L).apply_symm_apply g]
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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)
⊢ 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))
have hP₃ : P' (StructuredArrow.mk (𝟙 (W.Q.obj X)))
Tactic: apply induction_structuredArrow' W P'
-- Lean 4 proof step from Mathlib.CategoryTheory.Localization.StructuredArrow (goal)
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)
hP₃ : P' (StructuredArrow.mk (𝟙 (W.Q.obj X)))
⊢ 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))
have 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))
Tactic: apply induction_structuredArrow' W P'