[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
r : HomRel C
a b : C
m₁ m₂ : a ⟶ b
h : r m₁ m₂
⊢ CompClosure r m₁ m₂
[PROOFSTEP]
simpa using CompClosure.intro (𝟙 _) m₁ m₂ (𝟙 _) h
[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
r : HomRel C
a b c : C
f : a ⟶ b
a✝ b✝ : C
x : b ⟶ a✝
m₁ m₂ : a✝ ⟶ b✝
y : b✝ ⟶ c
h : r m₁ m₂
⊢ CompClosure r (f ≫ x ≫ m₁ ≫ y) (f ≫ x ≫ m₂ ≫ y)
[PROOFSTEP]
simpa using CompClosure.intro (f ≫ x) m₁ m₂ y h
[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
r : HomRel C
a b c : C
g : b ⟶ c
a✝ b✝ : C
x : a ⟶ a✝
m₁ m₂ : a✝ ⟶ b✝
y : b✝ ⟶ b
h : r m₁ m₂
⊢ CompClosure r ((x ≫ m₁ ≫ y) ≫ g) ((x ≫ m₂ ≫ y) ≫ g)
[PROOFSTEP]
simpa using CompClosure.intro x m₁ m₂ (y ≫ g) h
[GOAL]
C : Type ?u.6648
inst✝ : Category.{?u.6652, ?u.6648} C
r : HomRel C
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as), 𝟙 X✝ ≫ Quot.mk (CompClosure r) a = Quot.mk (CompClosure r) a
[PROOFSTEP]
simp
[GOAL]
C : Type ?u.6648
inst✝ : Category.{?u.6652, ?u.6648} C
r : HomRel C
X✝ Y✝ : Quotient r
f : X✝ ⟶ Y✝
⊢ ∀ (a : X✝.as ⟶ Y✝.as), Quot.mk (CompClosure r) a ≫ 𝟙 Y✝ = Quot.mk (CompClosure r) a
[PROOFSTEP]
simp
[GOAL]
C : Type ?u.6648
inst✝ : Category.{?u.6652, ?u.6648} C
r : HomRel C
W✝ X✝ Y✝ Z✝ : Quotient r
f : W✝ ⟶ X✝
g : X✝ ⟶ Y✝
h : Y✝ ⟶ Z✝
⊢ ∀ (a : Y✝.as ⟶ Z✝.as) (a_1 : X✝.as ⟶ Y✝.as) (a_2 : W✝.as ⟶ X✝.as),
    (Quot.mk (CompClosure r) a_2 ≫ Quot.mk (CompClosure r) a_1) ≫ Quot.mk (CompClosure r) a =
      Quot.mk (CompClosure r) a_2 ≫ Quot.mk (CompClosure r) a_1 ≫ Quot.mk (CompClosure r) a
[PROOFSTEP]
simp
[GOAL]
C : Type ?u.11008
inst✝ : Category.{?u.11012, ?u.11008} C
r : HomRel C
Y : Quotient r
⊢ (functor r).obj Y.as = Y
[PROOFSTEP]
ext
[GOAL]
case as
C : Type ?u.11008
inst✝ : Category.{?u.11012, ?u.11008} C
r : HomRel C
Y : Quotient r
⊢ ((functor r).obj Y.as).as = Y.as
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
P : {a b : Quotient r} → (a ⟶ b) → Prop
h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)
⊢ ∀ {a b : Quotient r} (f : a ⟶ b), P f
[PROOFSTEP]
rintro ⟨x⟩ ⟨y⟩ ⟨f⟩
[GOAL]
case mk.mk.mk
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
P : {a b : Quotient r} → (a ⟶ b) → Prop
h : ∀ {x y : C} (f : x ⟶ y), P ((functor r).map f)
x y : C
f✝ : { as := x } ⟶ { as := y }
f : { as := x }.as ⟶ { as := y }.as
⊢ P (Quot.mk (CompClosure r) f)
[PROOFSTEP]
exact h f
[GOAL]
C : Type u_2
inst✝ : Category.{u_1, u_2} C
r : HomRel C
a b : C
f₁ f₂ : a ⟶ b
h : r f₁ f₂
⊢ (functor r).map f₁ = (functor r).map f₂
[PROOFSTEP]
simpa using Quot.sound (CompClosure.intro (𝟙 a) f₁ f₂ (𝟙 b) h)
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ (functor r).map f = (functor r).map f' ↔ r f f'
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ (functor r).map f = (functor r).map f' → r f f'
[PROOFSTEP]
erw [Quot.eq]
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ EqvGen (CompClosure r) f f' → r f f'
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h✝ : Congruence r
X Y : C
f f' : X ⟶ Y
h : EqvGen (CompClosure r) f f'
⊢ r f f'
[PROOFSTEP]
induction' h with m m' hm
[GOAL]
case mp.rel
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' m m' : X ⟶ Y
hm : CompClosure r m m'
⊢ r m m'
[PROOFSTEP]
cases hm
[GOAL]
case mp.rel.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
a✝ b✝ : C
f✝ : X ⟶ a✝
m₁✝ m₂✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ Y
h✝ : r m₁✝ m₂✝
⊢ r (f✝ ≫ m₁✝ ≫ g✝) (f✝ ≫ m₂✝ ≫ g✝)
[PROOFSTEP]
apply Congruence.compLeft
[GOAL]
case mp.rel.intro.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
a✝ b✝ : C
f✝ : X ⟶ a✝
m₁✝ m₂✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ Y
h✝ : r m₁✝ m₂✝
⊢ r (m₁✝ ≫ g✝) (m₂✝ ≫ g✝)
[PROOFSTEP]
apply Congruence.compRight
[GOAL]
case mp.rel.intro.a.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
a✝ b✝ : C
f✝ : X ⟶ a✝
m₁✝ m₂✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ Y
h✝ : r m₁✝ m₂✝
⊢ r m₁✝ m₂✝
[PROOFSTEP]
assumption
[GOAL]
case mp.refl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ : X ⟶ Y
⊢ r x✝ x✝
[PROOFSTEP]
haveI :=
  (h.isEquiv : IsEquiv _ (@r X Y))
    -- porting note: had to add this line for `refl` (and name the `Congruence` argument)
[GOAL]
case mp.refl
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ : X ⟶ Y
this : IsEquiv (X ⟶ Y) r
⊢ r x✝ x✝
[PROOFSTEP]
apply refl
[GOAL]
case mp.symm
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ y✝ : X ⟶ Y
a✝ : EqvGen (CompClosure r) x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r y✝ x✝
[PROOFSTEP]
apply symm
[GOAL]
case mp.symm.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ y✝ : X ⟶ Y
a✝ : EqvGen (CompClosure r) x✝ y✝
a_ih✝ : r x✝ y✝
⊢ r x✝ y✝
[PROOFSTEP]
assumption
[GOAL]
case mp.trans
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ y✝ z✝ : X ⟶ Y
a✝¹ : EqvGen (CompClosure r) x✝ y✝
a✝ : EqvGen (CompClosure r) y✝ z✝
a_ih✝¹ : r x✝ y✝
a_ih✝ : r y✝ z✝
⊢ r x✝ z✝
[PROOFSTEP]
apply _root_.trans
[GOAL]
case mp.trans.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ y✝ z✝ : X ⟶ Y
a✝¹ : EqvGen (CompClosure r) x✝ y✝
a✝ : EqvGen (CompClosure r) y✝ z✝
a_ih✝¹ : r x✝ y✝
a_ih✝ : r y✝ z✝
⊢ r x✝ ?mp.trans.b
[PROOFSTEP]
assumption
[GOAL]
case mp.trans.a
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' x✝ y✝ z✝ : X ⟶ Y
a✝¹ : EqvGen (CompClosure r) x✝ y✝
a✝ : EqvGen (CompClosure r) y✝ z✝
a_ih✝¹ : r x✝ y✝
a_ih✝ : r y✝ z✝
⊢ r y✝ z✝
[PROOFSTEP]
assumption
[GOAL]
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f f' : X ⟶ Y
⊢ r f f' → (functor r).map f = (functor r).map f'
[PROOFSTEP]
apply Quotient.sound
[GOAL]
C : Type ?u.13725
inst✝¹ : Category.{?u.13729, ?u.13725} C
r : HomRel C
D : Type ?u.13757
inst✝ : Category.{?u.13761, ?u.13757} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : Quotient r
hf : a ⟶ b
⊢ ∀ (a_1 b_1 : a.as ⟶ b.as), CompClosure r a_1 b_1 → (fun f => F.map f) a_1 = (fun f => F.map f) b_1
[PROOFSTEP]
rintro _ _ ⟨_, _, _, _, h⟩
[GOAL]
case intro
C : Type ?u.13725
inst✝¹ : Category.{?u.13729, ?u.13725} C
r : HomRel C
D : Type ?u.13757
inst✝ : Category.{?u.13761, ?u.13757} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b : Quotient r
hf : a ⟶ b
a✝ b✝ : C
f✝ : a.as ⟶ a✝
m₁✝ m₂✝ : a✝ ⟶ b✝
g✝ : b✝ ⟶ b.as
h : r m₁✝ m₂✝
⊢ (fun f => F.map f) (f✝ ≫ m₁✝ ≫ g✝) = (fun f => F.map f) (f✝ ≫ m₂✝ ≫ g✝)
[PROOFSTEP]
simp [H _ _ _ _ h]
[GOAL]
C : Type ?u.13725
inst✝¹ : Category.{?u.13729, ?u.13725} C
r : HomRel C
D : Type ?u.13757
inst✝ : Category.{?u.13761, ?u.13757} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
⊢ ∀ {X Y Z : Quotient r} (f : X ⟶ Y) (g : Y ⟶ Z),
    { obj := fun a => F.obj a.as,
            map := fun a b hf =>
              Quot.liftOn hf (fun f => F.map f)
                (_ :
                  ∀ (a_1 b_1 : a.as ⟶ b.as),
                    CompClosure r a_1 b_1 → (fun f => F.map f) a_1 = (fun f => F.map f) b_1) }.map
        (f ≫ g) =
      { obj := fun a => F.obj a.as,
              map := fun a b hf =>
                Quot.liftOn hf (fun f => F.map f)
                  (_ :
                    ∀ (a_1 b_1 : a.as ⟶ b.as),
                      CompClosure r a_1 b_1 → (fun f => F.map f) a_1 = (fun f => F.map f) b_1) }.map
          f ≫
        { obj := fun a => F.obj a.as,
              map := fun a b hf =>
                Quot.liftOn hf (fun f => F.map f)
                  (_ :
                    ∀ (a_1 b_1 : a.as ⟶ b.as),
                      CompClosure r a_1 b_1 → (fun f => F.map f) a_1 = (fun f => F.map f) b_1) }.map
          g
[PROOFSTEP]
rintro a b c ⟨f⟩ ⟨g⟩
[GOAL]
case mk.mk
C : Type ?u.13725
inst✝¹ : Category.{?u.13729, ?u.13725} C
r : HomRel C
D : Type ?u.13757
inst✝ : Category.{?u.13761, ?u.13757} D
F : C ⥤ D
H : ∀ (x y : C) (f₁ f₂ : x ⟶ y), r f₁ f₂ → F.map f₁ = F.map f₂
a b c : Quotient r
f✝ : a ⟶ b
f : a.as ⟶ b.as
g✝ : b ⟶ c
g : b.as ⟶ c.as
⊢ { obj := fun a => F.obj a.as,
          map := fun a b hf =>
            Quot.liftOn hf (fun f => F.map f)
              (_ :
                ∀ (a_1 b_1 : a.as ⟶ b.as),
                  CompClosure r a_1 b_1 → (fun f => F.map f) a_1 = (fun f => F.map f) b_1) }.map
      (Quot.mk (CompClosure r) f ≫ Quot.mk (CompClosure r) g) =
    { obj := fun a => F.obj a.as,
            map := fun a b hf =>
              Quot.liftOn hf (fun f => F.map f)
                (_ :
                  ∀ (a_1 b_1 : a.as ⟶ b.as),
                    CompClosure r a_1 b_1 → (fun f => F.map f) a_1 = (fun f => F.map f) b_1) }.map
        (Quot.mk (CompClosure r) f) ≫
      { obj := fun a => F.obj a.as,
            map := fun a b hf =>
              Quot.liftOn hf (fun f => F.map f)
                (_ :
                  ∀ (a_1 b_1 : a.as ⟶ b.as),
                    CompClosure r a_1 b_1 → (fun f => F.map f) a_1 = (fun f => F.map f) b_1) }.map
        (Quot.mk (CompClosure r) g)
[PROOFSTEP]
exact F.map_comp f g
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
r : HomRel C
D : Type u_3
inst✝ : Category.{u_4, u_3} 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
[PROOFSTEP]
apply Functor.ext
[GOAL]
case h_map
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
r : HomRel C
D : Type u_3
inst✝ : Category.{u_4, u_3} 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.{u_2, u_1} C
r : HomRel C
D : Type u_3
inst✝ : Category.{u_4, u_3} 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
[PROOFSTEP]
rotate_left
[GOAL]
case h_obj
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
r : HomRel C
D : Type u_3
inst✝ : Category.{u_4, u_3} 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
[PROOFSTEP]
rintro X
[GOAL]
case h_obj
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
r : HomRel C
D : Type u_3
inst✝ : Category.{u_4, u_3} 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
[PROOFSTEP]
rfl
[GOAL]
case h_map
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
r : HomRel C
D : Type u_3
inst✝ : Category.{u_4, u_3} 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✝
[PROOFSTEP]
rintro X Y f
[GOAL]
case h_map
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
r : HomRel C
D : Type u_3
inst✝ : Category.{u_4, u_3} 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)
[PROOFSTEP]
simp
[GOAL]
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} 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
[PROOFSTEP]
subst_vars
[GOAL]
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} 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
[PROOFSTEP]
fapply Functor.hext
[GOAL]
case h_obj
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} 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
[PROOFSTEP]
rintro X
[GOAL]
case h_obj
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} 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
[PROOFSTEP]
dsimp [lift, Functor]
[GOAL]
case h_obj
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} 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)
[PROOFSTEP]
congr
[GOAL]
case h_map
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} 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)
[PROOFSTEP]
rintro _ _ f
[GOAL]
case h_map
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} 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)
[PROOFSTEP]
dsimp [lift, Functor]
[GOAL]
case h_map
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} 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))
[PROOFSTEP]
refine
  Quot.inductionOn f
    (fun _ ↦ ?_)
      -- porting note: this line was originally an `apply`
[GOAL]
case h_map
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} 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))
[PROOFSTEP]
simp only [Quot.liftOn_mk, Functor.comp_map]
[GOAL]
case h_map
C : Type u_3
inst✝¹ : Category.{u_1, u_3} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_2, u_4} 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✝))
[PROOFSTEP]
congr
[GOAL]
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_3, u_4} 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
⊢ (lift r F H).map ((functor r).map f) = F.map f
[PROOFSTEP]
rw [← NatIso.naturality_1 (lift.isLift r F H)]
[GOAL]
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_3, u_4} 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
⊢ (lift r F H).map ((functor r).map f) =
    NatTrans.app (lift.isLift r F H).inv X ≫ (functor r ⋙ lift r F H).map f ≫ NatTrans.app (lift.isLift r F H).hom Y
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_2
inst✝¹ : Category.{u_1, u_2} C
r : HomRel C
D : Type u_4
inst✝ : Category.{u_3, u_4} 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
⊢ Quot.liftOn (Quot.mk (CompClosure r) f) (fun f => F.map f)
      (_ :
        ∀ (a b : ((functor r).obj X).as ⟶ ((functor r).obj Y).as),
          CompClosure r a b → (fun f => F.map f) a = (fun f => F.map f) b) =
    𝟙 (F.obj X) ≫
      Quot.liftOn (Quot.mk (CompClosure r) f) (fun f => F.map f)
          (_ :
            ∀ (a b : ((functor r).obj X).as ⟶ ((functor r).obj Y).as),
              CompClosure r a b → (fun f => F.map f) a = (fun f => F.map f) b) ≫
        𝟙 (F.obj Y)
[PROOFSTEP]
simp
