case h_map
C : Type u_1
inst✝¹ : Category C
r : HomRel C
D : Type u_3
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      (functor r ⋙ lift r F H).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫ F.map f ≫ eqToHom (_ : F.obj Y = (functor r ⋙ lift r F H).obj Y))
    _auto✝

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

case h_map
C : Type u_1
inst✝¹ : Category C
r : HomRel C
D : Type u_3
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      (functor r ⋙ lift r F H).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫ F.map f ≫ eqToHom (_ : F.obj Y = (functor r ⋙ lift r F H).obj Y))
    _auto✝
case h_map
C : Type u_1
inst✝¹ : Category C
r : HomRel C
D : Type u_3
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      (functor r ⋙ lift r F H).map f =
        eqToHom (_ : ?F.obj X = ?G.obj X) ≫ F.map f ≫ eqToHom (_ : F.obj Y = (functor r ⋙ lift r F H).obj Y))
    _auto✝

case h_obj
C : Type u_1
inst✝¹ : Category C
r : HomRel C
D : Type u_3
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ ∀ (X : C), (functor r ⋙ lift r F H).obj X = F.obj X
rotate_left
case h_obj
C : Type u_1
inst✝¹ : Category C
r : HomRel C
D : Type u_3
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (functor r ⋙ lift r F H).obj X = F.obj X
case h_obj
C : Type u_1
inst✝¹ : Category C
r : HomRel C
D : Type u_3
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ ∀ (X : C), (functor r ⋙ lift r F H).obj X = F.obj X
rintro X
no goals
case h_obj
C : Type u_1
inst✝¹ : Category C
r : HomRel C
D : Type u_3
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X : C
⊢ (functor r ⋙ lift r F H).obj X = F.obj X
rfl
case h_map
C : Type u_1
inst✝¹ : Category C
r : HomRel C
D : Type u_3
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : C
f : X ⟶ Y
⊢ (functor r ⋙ lift r F H).map f =
    eqToHom (_ : (functor r ⋙ lift r F H).obj X = (functor r ⋙ lift r F H).obj X) ≫
      F.map f ≫ eqToHom (_ : F.obj Y = (functor r ⋙ lift r F H).obj Y)
case h_map
C : Type u_1
inst✝¹ : Category C
r : HomRel C
D : Type u_3
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ autoParam
    (∀ (X Y : C) (f : X ⟶ Y),
      (functor r ⋙ lift r F H).map f =
        eqToHom (_ : (functor r ⋙ lift r F H).obj X = (functor r ⋙ lift r F H).obj X) ≫
          F.map f ≫ eqToHom (_ : F.obj Y = (functor r ⋙ lift r F H).obj Y))
    _auto✝
rintro X Y f
no goals
case h_map
C : Type u_1
inst✝¹ : Category C
r : HomRel C
D : Type u_3
inst✝ : Category D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
X Y : C
f : X ⟶ Y
⊢ (functor r ⋙ lift r F H).map f =
    eqToHom (_ : (functor r ⋙ lift r F H).obj X = (functor r ⋙ lift r F H).obj X) ≫
      F.map f ≫ eqToHom (_ : F.obj Y = (functor r ⋙ lift r F H).obj Y)
simp