C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ Φ = lift r (functor r ⋙ Φ) H
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
Φ : Quotient r ⥤ D
hΦ : functor r ⋙ Φ = F
⊢ Φ = lift r F H
subst_vars
case h_obj
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ ∀ (X : Quotient r), Φ.obj X = (lift r (functor r ⋙ Φ) H).obj X

case h_map
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ ∀ (X Y : Quotient r) (f : X ⟶ Y), HEq (Φ.map f) ((lift r (functor r ⋙ Φ) H).map f)
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ Φ = lift r (functor r ⋙ Φ) H
fapply Functor.hext
case h_obj
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X : Quotient r
⊢ Φ.obj X = (lift r (functor r ⋙ Φ) H).obj X
case h_obj
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ ∀ (X : Quotient r), Φ.obj X = (lift r (functor r ⋙ Φ) H).obj X
rintro X
case h_obj
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X : Quotient r
⊢ Φ.obj X = Φ.obj ((functor r).obj X.as)
case h_obj
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X : Quotient r
⊢ Φ.obj X = (lift r (functor r ⋙ Φ) H).obj X
dsimp [lift, Functor]
no goals
case h_obj
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X : Quotient r
⊢ Φ.obj X = Φ.obj ((functor r).obj X.as)
congr
case h_map
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ HEq (Φ.map f) ((lift r (functor r ⋙ Φ) H).map f)
case h_map
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
⊢ ∀ (X Y : Quotient r) (f : X ⟶ Y), HEq (Φ.map f) ((lift r (functor r ⋙ Φ) H).map f)
rintro _ _ f
case h_map
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ HEq (Φ.map f)
    (Quot.liftOn f (fun f => Φ.map (Quot.mk (CompClosure r) f))
      (_ :
        ∀ (a b : X✝.as ⟶ Y✝.as),
          CompClosure r a b → (fun f => (functor r ⋙ Φ).map f) a = (fun f => (functor r ⋙ Φ).map f) b))
case h_map
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ HEq (Φ.map f) ((lift r (functor r ⋙ Φ) H).map f)
dsimp [lift, Functor]
case h_map
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
x✝ : X✝.as ⟶ Y✝.as
⊢ HEq (Φ.map (Quot.mk (CompClosure r) x✝))
    (Quot.liftOn (Quot.mk (CompClosure r) x✝) (fun f => Φ.map (Quot.mk (CompClosure r) f))
      (_ :
        ∀ (a b : X✝.as ⟶ Y✝.as),
          CompClosure r a b → (fun f => (functor r ⋙ Φ).map f) a = (fun f => (functor r ⋙ Φ).map f) b))
case h_map
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ HEq (Φ.map f)
    (Quot.liftOn f (fun f => Φ.map (Quot.mk (CompClosure r) f))
      (_ :
        ∀ (a b : X✝.as ⟶ Y✝.as),
          CompClosure r a b → (fun f => (functor r ⋙ Φ).map f) a = (fun f => (functor r ⋙ Φ).map f) b))
refine Quot.inductionOn f (fun _ ↦ ?_)
case h_map
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
x✝ : X✝.as ⟶ Y✝.as
⊢ HEq (Φ.map (Quot.mk (CompClosure r) x✝)) (Φ.map (Quot.mk (CompClosure r) x✝))
case h_map
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
x✝ : X✝.as ⟶ Y✝.as
⊢ HEq (Φ.map (Quot.mk (CompClosure r) x✝))
    (Quot.liftOn (Quot.mk (CompClosure r) x✝) (fun f => Φ.map (Quot.mk (CompClosure r) f))
      (_ :
        ∀ (a b : X✝.as ⟶ Y✝.as),
          CompClosure r a b → (fun f => (functor r ⋙ Φ).map f) a = (fun f => (functor r ⋙ Φ).map f) b))
simp only [Quot.liftOn_mk, Functor.comp_map]
no goals
case h_map
C : Type u_3
inst✝¹ : Category C
r : HomRel C
D : Type u_4
inst✝ : Category D
Φ : Quotient r ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → (functor r ⋙ Φ).map f₁ = (functor r ⋙ Φ).map f₂
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
x✝ : X✝.as ⟶ Y✝.as
⊢ HEq (Φ.map (Quot.mk (CompClosure r) x✝)) (Φ.map (Quot.mk (CompClosure r) x✝))
congr