[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ X.left = Y.left
[PROOFSTEP]
cases H
[GOAL]
case refl
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ X.left = X.left
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ (eqToHom H).left = eqToHom (_ : X.left = Y.left)
[PROOFSTEP]
cases H
[GOAL]
case refl
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ (eqToHom (_ : X = X)).left = eqToHom (_ : X.left = X.left)
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ X.right = Y.right
[PROOFSTEP]
cases H
[GOAL]
case refl
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ X.right = X.right
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X Y : Comma L R
H : X = Y
⊢ (eqToHom H).right = eqToHom (_ : X.right = Y.right)
[PROOFSTEP]
cases H
[GOAL]
case refl
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
X : Comma L R
⊢ (eqToHom (_ : X = X)).right = eqToHom (_ : X.right = X.right)
[PROOFSTEP]
rfl
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : autoParam (L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom) _auto✝
⊢ L₁.map l.inv ≫ X.hom = Y.hom ≫ R₁.map r.inv
[PROOFSTEP]
rw [← L₁.mapIso_inv l, Iso.inv_comp_eq, L₁.mapIso_hom, ← Category.assoc, h, Category.assoc, ← R₁.map_comp]
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
X Y : Comma L₁ R₁
l : X.left ≅ Y.left
r : X.right ≅ Y.right
h : autoParam (L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom) _auto✝
⊢ X.hom = X.hom ≫ R₁.map (r.hom ≫ r.inv)
[PROOFSTEP]
simp
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
l l' : L₁ ⟶ L₂
h : l = l'
X : Comma L₂ R
⊢ L₁.map (Iso.refl ((mapLeft R l).obj X).left).hom ≫ ((mapLeft R l').obj X).hom =
    ((mapLeft R l).obj X).hom ≫ R.map (Iso.refl ((mapLeft R l).obj X).right).hom
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
l l' : L₁ ⟶ L₂
h : l = l'
⊢ ∀ {X Y : Comma L₂ R} (f : X ⟶ Y),
    (mapLeft R l).map f ≫
        ((fun X => isoMk (Iso.refl ((mapLeft R l).obj X).left) (Iso.refl ((mapLeft R l).obj X).right)) Y).hom =
      ((fun X => isoMk (Iso.refl ((mapLeft R l).obj X).left) (Iso.refl ((mapLeft R l).obj X).right)) X).hom ≫
        (mapLeft R l').map f
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
r r' : R₁ ⟶ R₂
h : r = r'
X : Comma L R₁
⊢ L.map (Iso.refl ((mapRight L r).obj X).left).hom ≫ ((mapRight L r').obj X).hom =
    ((mapRight L r).obj X).hom ≫ R₂.map (Iso.refl ((mapRight L r).obj X).right).hom
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u₁
inst✝² : Category.{v₁, u₁} A
B : Type u₂
inst✝¹ : Category.{v₂, u₂} B
T : Type u₃
inst✝ : Category.{v₃, u₃} T
L : A ⥤ T
R : B ⥤ T
L₁ L₂ L₃ : A ⥤ T
R₁ R₂ R₃ : B ⥤ T
r r' : R₁ ⟶ R₂
h : r = r'
⊢ ∀ {X Y : Comma L R₁} (f : X ⟶ Y),
    (mapRight L r).map f ≫
        ((fun X => isoMk (Iso.refl ((mapRight L r).obj X).left) (Iso.refl ((mapRight L r).obj X).right)) Y).hom =
      ((fun X => isoMk (Iso.refl ((mapRight L r).obj X).left) (Iso.refl ((mapRight L r).obj X).right)) X).hom ≫
        (mapRight L r').map f
[PROOFSTEP]
aesop_cat
[GOAL]
A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
T : Type u₃
inst✝² : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝¹ : Category.{v₄, u₄} C
D : Type u₅
inst✝ : Category.{v₅, u₅} D
F : C ⥤ A
L : A ⥤ T
R : B ⥤ T
X✝ Y✝ : Comma (F ⋙ L) R
f : X✝ ⟶ Y✝
⊢ L.map (F.map f.left) ≫ ((fun X => { left := F.obj X.left, right := X.right, hom := X.hom }) Y✝).hom =
    ((fun X => { left := F.obj X.left, right := X.right, hom := X.hom }) X✝).hom ≫ R.map f.right
[PROOFSTEP]
simpa using f.w
[GOAL]
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝² : Category.{v₄, u₄} C
D : Type u₅
inst✝¹ : Category.{v₅, u₅} D
F : C ⥤ A
L : A ⥤ T
R : B ⥤ T
inst✝ : Faithful F
X Y : Comma (F ⋙ L) R
f g : X ⟶ Y
h : (preLeft F L R).map f = (preLeft F L R).map g
⊢ f.right = g.right
[PROOFSTEP]
apply congrArg CommaMorphism.right h
[GOAL]
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝² : Category.{v₄, u₄} C
D : Type u₅
inst✝¹ : Category.{v₅, u₅} D
F : C ⥤ A
L : A ⥤ T
R : B ⥤ T
inst✝ : Full F
X Y : Comma (F ⋙ L) R
f : (preLeft F L R).obj X ⟶ (preLeft F L R).obj Y
⊢ (F ⋙ L).map (F.preimage f.left) ≫ Y.hom = X.hom ≫ R.map f.right
[PROOFSTEP]
simpa using f.w
[GOAL]
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝² : Category.{v₄, u₄} C
D : Type u₅
inst✝¹ : Category.{v₅, u₅} D
F : C ⥤ A
L : A ⥤ T
R : B ⥤ T
inst✝ : EssSurj F
Y : Comma L R
⊢ L.map (Functor.objObjPreimageIso F Y.left).hom ≫ Y.hom =
    ((preLeft F L R).obj
          { left := Functor.objPreimage F Y.left, right := Y.right,
            hom := (L.mapIso (Functor.objObjPreimageIso F Y.left)).hom ≫ Y.hom }).hom ≫
      R.map
        (Iso.refl
            ((preLeft F L R).obj
                { left := Functor.objPreimage F Y.left, right := Y.right,
                  hom := (L.mapIso (Functor.objObjPreimageIso F Y.left)).hom ≫ Y.hom }).right).hom
[PROOFSTEP]
simp
[GOAL]
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝² : Category.{v₄, u₄} C
D : Type u₅
inst✝¹ : Category.{v₅, u₅} D
L : A ⥤ T
F : C ⥤ B
R : B ⥤ T
inst✝ : Faithful F
X Y : Comma L (F ⋙ R)
f g : X ⟶ Y
h : (preRight L F R).map f = (preRight L F R).map g
⊢ f.left = g.left
[PROOFSTEP]
apply congrArg CommaMorphism.left h
[GOAL]
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝² : Category.{v₄, u₄} C
D : Type u₅
inst✝¹ : Category.{v₅, u₅} D
L : A ⥤ T
F : C ⥤ B
R : B ⥤ T
inst✝ : Full F
X Y : Comma L (F ⋙ R)
f : (preRight L F R).obj X ⟶ (preRight L F R).obj Y
⊢ L.map f.left ≫ Y.hom = X.hom ≫ (F ⋙ R).map (F.preimage f.right)
[PROOFSTEP]
simpa using f.w
[GOAL]
A : Type u₁
inst✝⁵ : Category.{v₁, u₁} A
B : Type u₂
inst✝⁴ : Category.{v₂, u₂} B
T : Type u₃
inst✝³ : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝² : Category.{v₄, u₄} C
D : Type u₅
inst✝¹ : Category.{v₅, u₅} D
L : A ⥤ T
F : C ⥤ B
R : B ⥤ T
inst✝ : EssSurj F
Y : Comma L R
⊢ L.map
        (Iso.refl
            ((preRight L F R).obj
                { left := Y.left, right := Functor.objPreimage F Y.right,
                  hom := Y.hom ≫ (R.mapIso (Functor.objObjPreimageIso F Y.right)).inv }).left).hom ≫
      Y.hom =
    ((preRight L F R).obj
          { left := Y.left, right := Functor.objPreimage F Y.right,
            hom := Y.hom ≫ (R.mapIso (Functor.objObjPreimageIso F Y.right)).inv }).hom ≫
      R.map (Functor.objObjPreimageIso F Y.right).hom
[PROOFSTEP]
simp [← R.map_comp]
[GOAL]
A : Type u₁
inst✝⁴ : Category.{v₁, u₁} A
B : Type u₂
inst✝³ : Category.{v₂, u₂} B
T : Type u₃
inst✝² : Category.{v₃, u₃} T
L✝ : A ⥤ T
R✝ : B ⥤ T
C : Type u₄
inst✝¹ : Category.{v₄, u₄} C
D : Type u₅
inst✝ : Category.{v₅, u₅} D
L : A ⥤ T
R : B ⥤ T
F : T ⥤ C
X✝ Y✝ : Comma L R
f : X✝ ⟶ Y✝
⊢ (L ⋙ F).map f.left ≫ ((fun X => { left := X.left, right := X.right, hom := F.map X.hom }) Y✝).hom =
    ((fun X => { left := X.left, right := X.right, hom := F.map X.hom }) X✝).hom ≫ (R ⋙ F).map f.right
[PROOFSTEP]
simp only [Functor.comp_map, ← F.map_comp, f.w]
