case h.h.h
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ P f = ⊤ f
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
⊢ P = ⊤
funext X Y f
case h.h.h.a
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ P f ↔ ⊤ f
case h.h.h
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ P f = ⊤ f
ext
case h.h.h.a.mp
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ P f → ⊤ f

case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ ⊤ f → P f
case h.h.h.a
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ P f ↔ ⊤ f
constructor
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ ⊤ f → P f
case h.h.h.a.mp
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ P f → ⊤ f

case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ ⊤ f → P f
. intro
  apply MorphismProperty.top_apply
case h.h.h.a.mp
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : P f
⊢ ⊤ f
case h.h.h.a.mp
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ P f → ⊤ f
intro
no goals
case h.h.h.a.mp
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : P f
⊢ ⊤ f
apply MorphismProperty.top_apply
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
⊢ P f
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
⊢ ⊤ f → P f
intro
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
⊢ P f
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
⊢ P f
let G : _ ⥤ W.Localization := Quotient.functor _
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
⊢ P f
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
⊢ P f
haveI : Full G := Quotient.fullFunctor _
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
⊢ ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
⊢ P f
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.image_preimage] using this _ _ (G.preimage f)
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂ : Paths (LocQuiver W)
p : X₁ ⟶ X₂
⊢ P (G.map p)
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
⊢ ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
intros X₁ X₂ p
case h.h.h.a.mpr.nil
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂ : Paths (LocQuiver W)
⊢ P (G.map Quiver.Path.nil)

case h.h.h.a.mpr.cons
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
⊢ P (G.map (Quiver.Path.cons p g))
case h.h.h.a.mpr
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂ : Paths (LocQuiver W)
p : X₁ ⟶ X₂
⊢ P (G.map p)
induction' p with X₂ X₃ p g hp
no goals
case h.h.h.a.mpr.cons
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
⊢ P (G.map (Quiver.Path.cons p g))
. let p' : X₁ ⟶X₂ := p
  rw [show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl, G.map_comp]
  refine' hP₃ _ _ hp _
  rcases g with (g | ⟨g, hg⟩)
  . apply hP₁
  . apply hP₂
case mk.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
Y : MorphismProperty.Localization W
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this✝ : Full G
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
X : C
f : { as := { obj := X } } ⟶ Y
a✝ : ⊤ f
⊢ P f
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this✝ : Full G
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
⊢ P f
rcases X with ⟨⟨X⟩⟩
case mk.mk.mk.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this✝ : Full G
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
X Y : C
f : { as := { obj := X } } ⟶ { as := { obj := Y } }
a✝ : ⊤ f
⊢ P f
case mk.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
Y : MorphismProperty.Localization W
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this✝ : Full G
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
X : C
f : { as := { obj := X } } ⟶ Y
a✝ : ⊤ f
⊢ P f
rcases Y with ⟨⟨Y⟩⟩
no goals
case mk.mk.mk.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this✝ : Full G
this : ∀ (X₁ X₂ : Paths (LocQuiver W)) (f : X₁ ⟶ X₂), P (G.map f)
X Y : C
f : { as := { obj := X } } ⟶ { as := { obj := Y } }
a✝ : ⊤ f
⊢ P f
simpa only [Functor.image_preimage] using this _ _ (G.preimage f)
no goals
case h.h.h.a.mpr.nil
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂ : Paths (LocQuiver W)
⊢ P (G.map Quiver.Path.nil)
simpa only [Functor.map_id] using hP₁ (𝟙 X₁.obj)
case h.h.h.a.mpr.cons
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map (Quiver.Path.cons p g))
case h.h.h.a.mpr.cons
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
⊢ P (G.map (Quiver.Path.cons p g))
let p' : X₁ ⟶X₂ := p
case h.h.h.a.mpr.cons
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map p' ≫ G.map (Quiver.Hom.toPath g))
case h.h.h.a.mpr.cons
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map (Quiver.Path.cons p g))
rw [show p'.cons g = p' ≫ Quiver.Hom.toPath g by rfl, G.map_comp]
case h.h.h.a.mpr.cons
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map (Quiver.Hom.toPath g))
case h.h.h.a.mpr.cons
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map p' ≫ G.map (Quiver.Hom.toPath g))
refine' hP₃ _ _ hp _
case h.h.h.a.mpr.cons.inl
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₂.obj ⟶ X₃.obj
⊢ P (G.map (Quiver.Hom.toPath (Sum.inl g)))

case h.h.h.a.mpr.cons.inr.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₃.obj ⟶ X₂.obj
hg : W g
⊢ P (G.map (Quiver.Hom.toPath (Sum.inr { val := g, property := hg })))
case h.h.h.a.mpr.cons
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ P (G.map (Quiver.Hom.toPath g))
rcases g with (g | ⟨g, hg⟩)
case h.h.h.a.mpr.cons.inr.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₃.obj ⟶ X₂.obj
hg : W g
⊢ P (G.map (Quiver.Hom.toPath (Sum.inr { val := g, property := hg })))
case h.h.h.a.mpr.cons.inl
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₂.obj ⟶ X₃.obj
⊢ P (G.map (Quiver.Hom.toPath (Sum.inl g)))

case h.h.h.a.mpr.cons.inr.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₃.obj ⟶ X₂.obj
hg : W g
⊢ P (G.map (Quiver.Hom.toPath (Sum.inr { val := g, property := hg })))
. apply hP₁
no goals
case h.h.h.a.mpr.cons.inr.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₃.obj ⟶ X₂.obj
hg : W g
⊢ P (G.map (Quiver.Hom.toPath (Sum.inr { val := g, property := hg })))
. apply hP₂
no goals
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
g : X₂ ⟶ X₃
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
⊢ Quiver.Path.cons p' g = p' ≫ Quiver.Hom.toPath g
rfl
no goals
case h.h.h.a.mpr.cons.inl
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₂.obj ⟶ X₃.obj
⊢ P (G.map (Quiver.Hom.toPath (Sum.inl g)))
apply hP₁
no goals
case h.h.h.a.mpr.cons.inr.mk
C : Type u_1
inst✝¹ : Category C
W : MorphismProperty C
D : Type ?u.29447
inst✝ : Category D
G✝ : C ⥤ D
hG : MorphismProperty.IsInvertedBy W G✝
P : MorphismProperty (MorphismProperty.Localization W)
hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P ((MorphismProperty.Q W).map f)
hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (winv w hw)
hP₃ : MorphismProperty.StableUnderComposition P
X Y : MorphismProperty.Localization W
f : X ⟶ Y
a✝ : ⊤ f
G : Paths (LocQuiver W) ⥤ MorphismProperty.Localization W := Quotient.functor (relations W)
this : Full G
X₁ X₂✝ X₂ X₃ : Paths (LocQuiver W)
p : Quiver.Path X₁ X₂
hp : P (G.map p)
p' : X₁ ⟶ X₂ := p
g : X₃.obj ⟶ X₂.obj
hg : W g
⊢ P (G.map (Quiver.Hom.toPath (Sum.inr { val := g, property := hg })))
apply hP₂