[GOAL]
B : Type u
inst✝ : Bicategory B
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
a : B
⊢ leftZigzag (ρ_ (𝟙 a)).inv (ρ_ (𝟙 a)).hom = (λ_ (𝟙 a)).hom ≫ (ρ_ (𝟙 a)).inv
[PROOFSTEP]
dsimp
[GOAL]
B : Type u
inst✝ : Bicategory B
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
a : B
⊢ (ρ_ (𝟙 a)).inv ▷ 𝟙 a ⊗≫ 𝟙 a ◁ (ρ_ (𝟙 a)).hom = (λ_ (𝟙 a)).hom ≫ (ρ_ (𝟙 a)).inv
[PROOFSTEP]
coherence
[GOAL]
B : Type u
inst✝ : Bicategory B
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
a : B
⊢ rightZigzag (ρ_ (𝟙 a)).inv (ρ_ (𝟙 a)).hom = (ρ_ (𝟙 a)).hom ≫ (λ_ (𝟙 a)).inv
[PROOFSTEP]
dsimp
[GOAL]
B : Type u
inst✝ : Bicategory B
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
a : B
⊢ 𝟙 a ◁ (ρ_ (𝟙 a)).inv ⊗≫ (ρ_ (𝟙 a)).hom ▷ 𝟙 a = (ρ_ (𝟙 a)).hom ≫ (λ_ (𝟙 a)).inv
[PROOFSTEP]
coherence
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (leftZigzagIso η ε).inv = rightZigzag ε.inv η.inv
[PROOFSTEP]
simp [bicategoricalComp, bicategoricalIsoComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (rightZigzagIso η ε).inv = leftZigzag ε.inv η.inv
[PROOFSTEP]
simp [bicategoricalComp, bicategoricalIsoComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ leftZigzagIso η (adjointifyCounit η ε) = λ_ f ≪≫ (ρ_ f).symm
[PROOFSTEP]
apply Iso.ext
[GOAL]
case w
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ (leftZigzagIso η (adjointifyCounit η ε)).hom = (λ_ f ≪≫ (ρ_ f).symm).hom
[PROOFSTEP]
dsimp [adjointifyCounit, bicategoricalIsoComp]
[GOAL]
case w
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ η.hom ▷ f ≫
      ((α_ f g f).hom ≫ 𝟙 f ▷ (g ≫ f)) ≫
        f ◁ (g ◁ ((ρ_ f).inv ≫ (f ◁ ε.inv ≫ (𝟙 f ▷ (g ≫ f) ≫ (α_ f g f).inv) ≫ η.inv ▷ f) ≫ (λ_ f).hom) ≫ ε.hom) =
    (λ_ f).hom ≫ (ρ_ f).inv
[PROOFSTEP]
calc
  _ = 𝟙 _ ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom := by simp [bicategoricalComp];
    coherence
  _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom := by
    rw [← whisker_exchange η.hom (f ◁ ε.inv)]; simp [bicategoricalComp]; coherence
  _ = 𝟙 _ ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom := by rw [← whisker_exchange η.hom η.inv]; coherence
  _ = 𝟙 _ ⊗≫ f ◁ (ε.inv ≫ ε.hom) := by rw [Iso.inv_hom_id]; simp [bicategoricalComp]
  _ = _ := by rw [Iso.inv_hom_id]; simp [bicategoricalComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ η.hom ▷ f ≫
      ((α_ f g f).hom ≫ 𝟙 f ▷ (g ≫ f)) ≫
        f ◁ (g ◁ ((ρ_ f).inv ≫ (f ◁ ε.inv ≫ (𝟙 f ▷ (g ≫ f) ≫ (α_ f g f).inv) ≫ η.inv ▷ f) ≫ (λ_ f).hom) ≫ ε.hom) =
    𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom
[PROOFSTEP]
simp [bicategoricalComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ η.hom ▷ f ≫
      (α_ f g f).hom ≫
        (ρ_ (f ≫ g ≫ f)).inv ≫
          (α_ f (g ≫ f) (𝟙 b)).hom ≫
            f ◁ (α_ g f (𝟙 b)).hom ≫
              f ◁ g ◁ f ◁ ε.inv ≫ f ◁ g ◁ (α_ f g f).inv ≫ f ◁ g ◁ η.inv ▷ f ≫ f ◁ g ◁ (λ_ f).hom ≫ f ◁ ε.hom =
    (λ_ f).hom ≫
      (ρ_ f).inv ≫
        (λ_ (f ≫ 𝟙 b)).inv ≫
          (α_ (𝟙 a) f (𝟙 b)).inv ≫
            (ρ_ (𝟙 a ≫ f)).hom ≫
              η.hom ▷ f ≫
                (ρ_ ((f ≫ g) ≫ f)).inv ≫
                  (α_ (f ≫ g) f (𝟙 b)).hom ≫
                    (α_ f g (f ≫ 𝟙 b)).hom ≫
                      f ◁ g ◁ f ◁ ε.inv ≫ f ◁ g ◁ (α_ f g f).inv ≫ f ◁ g ◁ η.inv ▷ f ≫ f ◁ g ◁ (λ_ f).hom ≫ f ◁ ε.hom
[PROOFSTEP]
coherence
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ (η.hom ▷ (f ≫ 𝟙 b) ≫ (f ≫ g) ◁ f ◁ ε.inv) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
[PROOFSTEP]
rw [← whisker_exchange η.hom (f ◁ ε.inv)]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ (𝟙 a ◁ f ◁ ε.inv ≫ η.hom ▷ (f ≫ g ≫ f)) ⊗≫ f ◁ g ◁ η.inv ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom
[PROOFSTEP]
simp [bicategoricalComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ f ◁ ε.inv ≫
      (λ_ (f ≫ g ≫ f)).inv ≫
        (α_ (𝟙 a) f (g ≫ f)).inv ≫
          (α_ (𝟙 a ≫ f) g f).inv ≫
            η.hom ▷ f ▷ g ▷ f ≫
              (α_ ((f ≫ g) ≫ f) g f).hom ≫
                (α_ (f ≫ g) f (g ≫ f)).hom ≫
                  (α_ f g (f ≫ g ≫ f)).hom ≫
                    f ◁ g ◁ (α_ f g f).inv ≫ f ◁ g ◁ η.inv ▷ f ≫ f ◁ g ◁ (λ_ f).hom ≫ f ◁ ε.hom =
    f ◁ ε.inv ≫
      (α_ f g f).inv ≫
        (λ_ ((f ≫ g) ≫ f)).inv ≫
          (α_ (𝟙 a) (f ≫ g) f).inv ≫
            (α_ (𝟙 a) f g).inv ▷ f ≫
              η.hom ▷ f ▷ g ▷ f ≫
                (α_ (f ≫ g) f g).hom ▷ f ≫
                  (α_ (f ≫ g) (f ≫ g) f).hom ≫
                    (α_ f g ((f ≫ g) ≫ f)).hom ≫ f ◁ g ◁ η.inv ▷ f ≫ f ◁ g ◁ (λ_ f).hom ≫ f ◁ ε.hom
[PROOFSTEP]
coherence
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.hom ▷ (f ≫ g) ≫ (f ≫ g) ◁ η.inv) ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom
[PROOFSTEP]
rw [← whisker_exchange η.hom η.inv]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (𝟙 a ◁ η.inv ≫ η.hom ▷ 𝟙 a) ▷ f ⊗≫ f ◁ ε.hom =
    𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom
[PROOFSTEP]
coherence
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ (η.inv ≫ η.hom) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)
[PROOFSTEP]
rw [Iso.inv_hom_id]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ ε.inv ⊗≫ 𝟙 (f ≫ g) ▷ f ⊗≫ f ◁ ε.hom = 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom)
[PROOFSTEP]
simp [bicategoricalComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ (ε.inv ≫ ε.hom) = (λ_ f).hom ≫ (ρ_ f).inv
[PROOFSTEP]
rw [Iso.inv_hom_id]
[GOAL]
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g : b ⟶ a
η✝ : 𝟙 a ≅ f ≫ g
ε✝ : g ≫ f ≅ 𝟙 b
η : 𝟙 a ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
⊢ 𝟙 (𝟙 a ≫ f) ⊗≫ f ◁ 𝟙 (𝟙 b) = (λ_ f).hom ≫ (ρ_ f).inv
[PROOFSTEP]
simp [bicategoricalComp]
[GOAL]
B : Type u
inst✝ : Bicategory B
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
η : 𝟙 a✝ ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
a : B
⊢ leftZigzagIso (ρ_ (𝟙 a)).symm (ρ_ (𝟙 a)) = λ_ (𝟙 a) ≪≫ (ρ_ (𝟙 a)).symm
[PROOFSTEP]
ext
[GOAL]
case w
B : Type u
inst✝ : Bicategory B
a✝ b c : B
f : a✝ ⟶ b
g : b ⟶ a✝
η : 𝟙 a✝ ≅ f ≫ g
ε : g ≫ f ≅ 𝟙 b
a : B
⊢ (leftZigzagIso (ρ_ (𝟙 a)).symm (ρ_ (𝟙 a))).hom = (λ_ (𝟙 a) ≪≫ (ρ_ (𝟙 a)).symm).hom
[PROOFSTEP]
simp [bicategoricalIsoComp]


[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
⊢ IsIso f
[PROOFSTEP]
skip
[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
⊢ IsIso f
[PROOFSTEP]
haveI i' : IsIso ((forget D).map ((forget₂ C D).map f)) := Functor.map_isIso (forget D) _
[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
⊢ IsIso f
[PROOFSTEP]
haveI : IsIso ((forget C).map f) := by
  have := @HasForget₂.forget_comp C D
  rw [← this]
  exact i'
[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
⊢ IsIso ((forget C).map f)
[PROOFSTEP]
have := @HasForget₂.forget_comp C D
[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
this :
  ∀ [inst : Category.{?u.1872, u + 1} C] [inst_1 : ConcreteCategory C] [inst_2 : Category.{?u.1871, u + 1} D]
    [inst_3 : ConcreteCategory D] [self : HasForget₂ C D], HasForget₂.forget₂ ⋙ forget D = forget C
⊢ IsIso ((forget C).map f)
[PROOFSTEP]
rw [← this]
[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
this :
  ∀ [inst : Category.{u_1, u + 1} C] [inst_1 : ConcreteCategory C] [inst_2 : Category.{u_2, u + 1} D]
    [inst_3 : ConcreteCategory D] [self : HasForget₂ C D], HasForget₂.forget₂ ⋙ forget D = forget C
⊢ IsIso ((HasForget₂.forget₂ ⋙ forget D).map f)
[PROOFSTEP]
exact i'
[GOAL]
C : Type (u + 1)
inst✝⁵ : Category.{u_1, u + 1} C
inst✝⁴ : ConcreteCategory C
D : Type (u + 1)
inst✝³ : Category.{u_2, u + 1} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : ReflectsIsomorphisms (forget C)
X Y : C
f : X ⟶ Y
i : IsIso ((forget₂ C D).map f)
i' : IsIso ((forget D).map ((forget₂ C D).map f))
this : IsIso ((forget C).map f)
⊢ IsIso f
[PROOFSTEP]
apply isIso_of_reflects_iso f (forget C)


[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ ((evaluation C D).obj X).map (kernel.ι α) ≫ (Iso.refl (((evaluation C D).obj X).obj F)).hom =
    (PreservesKernel.iso ((evaluation C D).obj X) α).hom ≫ kernel.ι (NatTrans.app α X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ NatTrans.app (kernel.ι α) X ≫ 𝟙 (F.obj X) =
    (PreservesKernel.iso ((evaluation C D).obj X) α).hom ≫ kernel.ι (NatTrans.app α X)
[PROOFSTEP]
simp only [Category.comp_id, PreservesKernel.iso_hom]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ NatTrans.app (kernel.ι α) X = kernelComparison α ((evaluation C D).obj X) ≫ kernel.ι (NatTrans.app α X)
[PROOFSTEP]
exact (kernelComparison_comp_ι _ ((evaluation C D).obj X)).symm
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ ((evaluation C D).obj X).map (cokernel.π α) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).hom =
    (Iso.refl (((evaluation C D).obj X).obj G)).hom ≫ cokernel.π (NatTrans.app α X)
[PROOFSTEP]
apply (cancel_mono (PreservesCokernel.iso ((evaluation C D).obj X) α).inv).1
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (((evaluation C D).obj X).map (cokernel.π α) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).hom) ≫
      (PreservesCokernel.iso ((evaluation C D).obj X) α).inv =
    ((Iso.refl (((evaluation C D).obj X).obj G)).hom ≫ cokernel.π (NatTrans.app α X)) ≫
      (PreservesCokernel.iso ((evaluation C D).obj X) α).inv
[PROOFSTEP]
simp only [Category.assoc, Iso.hom_inv_id]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ ((evaluation C D).obj X).map (cokernel.π α) ≫ 𝟙 (((evaluation C D).obj X).obj (cokernel α)) =
    (Iso.refl (((evaluation C D).obj X).obj G)).hom ≫
      cokernel.π (NatTrans.app α X) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).inv
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ NatTrans.app (cokernel.π α) X ≫ 𝟙 ((cokernel α).obj X) =
    𝟙 (G.obj X) ≫ cokernel.π (NatTrans.app α X) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).inv
[PROOFSTEP]
simp only [PreservesCokernel.iso_inv, Category.id_comp, Category.comp_id]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ NatTrans.app (cokernel.π α) X = cokernel.π (NatTrans.app α X) ≫ cokernelComparison α ((evaluation C D).obj X)
[PROOFSTEP]
exact (π_comp_cokernelComparison _ ((evaluation C D).obj X)).symm
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ coimageImageComparison (NatTrans.app α X) =
    (coimageObjIso α X).inv ≫ NatTrans.app (coimageImageComparison α) X ≫ (imageObjIso α X).hom
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (coequalizer.π (kernel.ι (NatTrans.app α X)) 0 ≫ coimageImageComparison (NatTrans.app α X)) ≫
      equalizer.ι (cokernel.π (NatTrans.app α X)) 0 =
    (coequalizer.π (kernel.ι (NatTrans.app α X)) 0 ≫
        (coimageObjIso α X).inv ≫ NatTrans.app (coimageImageComparison α) X ≫ (imageObjIso α X).hom) ≫
      equalizer.ι (cokernel.π (NatTrans.app α X)) 0
[PROOFSTEP]
dsimp
[GOAL]
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (cokernel.π (kernel.ι (NatTrans.app α X)) ≫ coimageImageComparison (NatTrans.app α X)) ≫
      kernel.ι (cokernel.π (NatTrans.app α X)) =
    (cokernel.π (kernel.ι (NatTrans.app α X)) ≫
        (coimageObjIso α X).inv ≫ NatTrans.app (coimageImageComparison α) X ≫ (imageObjIso α X).hom) ≫
      kernel.ι (cokernel.π (NatTrans.app α X))
[PROOFSTEP]
dsimp [imageObjIso, coimageObjIso, cokernel.map]
[GOAL]
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ (cokernel.π (kernel.ι (NatTrans.app α X)) ≫ coimageImageComparison (NatTrans.app α X)) ≫
      kernel.ι (cokernel.π (NatTrans.app α X)) =
    (cokernel.π (kernel.ι (NatTrans.app α X)) ≫
        (cokernel.desc (kernel.ι (NatTrans.app α X)) (𝟙 (F.obj X) ≫ cokernel.π (NatTrans.app (kernel.ι α) X))
              (_ : kernel.ι (NatTrans.app α X) ≫ 𝟙 (F.obj X) ≫ cokernel.π (NatTrans.app (kernel.ι α) X) = 0) ≫
            (PreservesCokernel.iso ((evaluation C D).obj X) (kernel.ι α)).inv) ≫
          NatTrans.app (coimageImageComparison α) X ≫
            (PreservesKernel.iso ((evaluation C D).obj X) (cokernel.π α)).hom ≫
              kernel.map (NatTrans.app (cokernel.π α) X) (cokernel.π (NatTrans.app α X)) (𝟙 (G.obj X))
                (PreservesCokernel.iso ((evaluation C D).obj X) α).hom
                (_ :
                  ((evaluation C D).obj X).map (cokernel.π α) ≫ (PreservesCokernel.iso ((evaluation C D).obj X) α).hom =
                    (Iso.refl (((evaluation C D).obj X).obj G)).hom ≫ cokernel.π (NatTrans.app α X))) ≫
      kernel.ι (cokernel.π (NatTrans.app α X))
[PROOFSTEP]
simp only [coimage_image_factorisation, PreservesKernel.iso_hom, Category.assoc, kernel.lift_ι, Category.comp_id,
  PreservesCokernel.iso_inv, cokernel.π_desc_assoc, Category.id_comp]
[GOAL]
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ NatTrans.app α X =
    cokernel.π (NatTrans.app (kernel.ι α) X) ≫
      cokernelComparison (kernel.ι α) ((evaluation C D).obj X) ≫
        NatTrans.app (coimageImageComparison α) X ≫
          kernelComparison (cokernel.π α) ((evaluation C D).obj X) ≫ kernel.ι (NatTrans.app (cokernel.π α) X)
[PROOFSTEP]
erw [kernelComparison_comp_ι _ ((evaluation C D).obj X), π_comp_cokernelComparison_assoc _ ((evaluation C D).obj X)]
[GOAL]
case h.h
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ NatTrans.app α X =
    ((evaluation C D).obj X).map (cokernel.π (kernel.ι α)) ≫
      NatTrans.app (coimageImageComparison α) X ≫ ((evaluation C D).obj X).map (kernel.ι (cokernel.π α))
[PROOFSTEP]
conv_lhs => rw [← coimage_image_factorisation α]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
| NatTrans.app α X
[PROOFSTEP]
rw [← coimage_image_factorisation α]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
| NatTrans.app α X
[PROOFSTEP]
rw [← coimage_image_factorisation α]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
| NatTrans.app α X
[PROOFSTEP]
rw [← coimage_image_factorisation α]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ NatTrans.app (coimageImageComparison α) X =
    (coimageObjIso α X).hom ≫ coimageImageComparison (NatTrans.app α X) ≫ (imageObjIso α X).inv
[PROOFSTEP]
simp only [coimageImageComparison_app, Iso.hom_inv_id_assoc, Iso.hom_inv_id, Category.assoc, Category.comp_id]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ IsIso (coimageImageComparison α)
[PROOFSTEP]
have : ∀ X : C, IsIso ((Abelian.coimageImageComparison α).app X) :=
  by
  intros
  rw [coimageImageComparison_app']
  infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
⊢ ∀ (X : C), IsIso (NatTrans.app (coimageImageComparison α) X)
[PROOFSTEP]
intros
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X X✝ : C
⊢ IsIso (NatTrans.app (coimageImageComparison α) X✝)
[PROOFSTEP]
rw [coimageImageComparison_app']
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X X✝ : C
⊢ IsIso ((coimageObjIso α X✝).hom ≫ coimageImageComparison (NatTrans.app α X✝) ≫ (imageObjIso α X✝).inv)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type w
inst✝¹ : Category.{z, w} D
inst✝ : Abelian D
F G : C ⥤ D
α : F ⟶ G
X : C
this : ∀ (X : C), IsIso (NatTrans.app (coimageImageComparison α) X)
⊢ IsIso (coimageImageComparison α)
[PROOFSTEP]
apply NatIso.isIso_of_isIso_app


[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
⊢ pseudoApply δ (pseudoApply h c) = pseudoApply h' (pseudoApply γ c)
[PROOFSTEP]
rw [← Pseudoelement.comp_apply, ← comm₃, Pseudoelement.comp_apply]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
⊢ pseudoApply h' (pseudoApply γ c) = pseudoApply h' 0
[PROOFSTEP]
rw [hc]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
this : pseudoApply h c = 0
b : Pseudoelement B
hb : pseudoApply g b = c
⊢ pseudoApply g' (pseudoApply β b) = pseudoApply γ (pseudoApply g b)
[PROOFSTEP]
rw [← Pseudoelement.comp_apply, comm₂, Pseudoelement.comp_apply]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
this : pseudoApply h c = 0
b : Pseudoelement B
hb : pseudoApply g b = c
⊢ pseudoApply γ (pseudoApply g b) = pseudoApply γ c
[PROOFSTEP]
rw [hb]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
this✝ : pseudoApply h c = 0
b : Pseudoelement B
hb : pseudoApply g b = c
this : pseudoApply g' (pseudoApply β b) = 0
a' : Pseudoelement A'
ha' : pseudoApply f' a' = pseudoApply β b
a : Pseudoelement A
ha : pseudoApply α a = a'
⊢ pseudoApply β (pseudoApply f a) = pseudoApply f' (pseudoApply α a)
[PROOFSTEP]
rw [← Pseudoelement.comp_apply, ← comm₁, Pseudoelement.comp_apply]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
this✝ : pseudoApply h c = 0
b : Pseudoelement B
hb : pseudoApply g b = c
this : pseudoApply g' (pseudoApply β b) = 0
a' : Pseudoelement A'
ha' : pseudoApply f' a' = pseudoApply β b
a : Pseudoelement A
ha : pseudoApply α a = a'
⊢ pseudoApply f' (pseudoApply α a) = pseudoApply f' a'
[PROOFSTEP]
rw [ha]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hfg : Exact f g
hgh : Exact g h
hf'g' : Exact f' g'
hα : Epi α
hβ : Mono β
hδ : Mono δ
c : Pseudoelement C
hc : pseudoApply γ c = 0
this✝¹ : pseudoApply h c = 0
b : Pseudoelement B
hb : pseudoApply g b = c
this✝ : pseudoApply g' (pseudoApply β b) = 0
a' : Pseudoelement A'
ha' : pseudoApply f' a' = pseudoApply β b
a : Pseudoelement A
ha : pseudoApply α a = a'
this : pseudoApply f a = b
⊢ pseudoApply g b = pseudoApply g (pseudoApply f a)
[PROOFSTEP]
rw [this]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
⊢ r = 0
[PROOFSTEP]
have hf'r : f' ≫ r = 0 :=
  Limits.zero_of_epi_comp α <|
    calc
      α ≫ f' ≫ r = f ≫ β ≫ r := by rw [reassoc_of% comm₁]
      _ = f ≫ 0 := by rw [hβr]
      _ = 0 := HasZeroMorphisms.comp_zero _ _
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
⊢ α ≫ f' ≫ r = f ≫ β ≫ r
[PROOFSTEP]
rw [reassoc_of% comm₁]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
⊢ f ≫ β ≫ r = f ≫ 0
[PROOFSTEP]
rw [hβr]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
⊢ r = 0
[PROOFSTEP]
let y : R ⟶ pushout r g' := pushout.inl
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
⊢ r = 0
[PROOFSTEP]
let z : C' ⟶ pushout r g' := pushout.inr
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
⊢ r = 0
[PROOFSTEP]
have : Mono (cokernel.desc f' g' hf'g'.w) := mono_cokernel_desc_of_exact _ _ hf'g'
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
⊢ r = 0
[PROOFSTEP]
have : Mono y :=
  mono_inl_of_factor_thru_epi_mono_factorization r g' (cokernel.π f') (cokernel.desc f' g' hf'g'.w) (by simp)
    (cokernel.desc f' r hf'r) (by simp) _ (colimit.isColimit _)
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
⊢ cokernel.π f' ≫ cokernel.desc f' g' (_ : f' ≫ g' = 0) = g'
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
⊢ cokernel.π f' ≫ cokernel.desc f' r hf'r = r
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
⊢ r = 0
[PROOFSTEP]
have hz : g ≫ γ ≫ z = 0 :=
  calc
    g ≫ γ ≫ z = β ≫ g' ≫ z := by rw [← reassoc_of% comm₂]
    _ = β ≫ r ≫ y := by rw [← pushout.condition]
    _ = 0 ≫ y := by rw [reassoc_of% hβr]
    _ = 0 := HasZeroMorphisms.zero_comp _ _
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
⊢ g ≫ γ ≫ z = β ≫ g' ≫ z
[PROOFSTEP]
rw [← reassoc_of% comm₂]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
⊢ β ≫ g' ≫ z = β ≫ r ≫ y
[PROOFSTEP]
rw [← pushout.condition]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
⊢ β ≫ r ≫ y = 0 ≫ y
[PROOFSTEP]
rw [reassoc_of% hβr]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
hz : g ≫ γ ≫ z = 0
⊢ r = 0
[PROOFSTEP]
let v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
⊢ r = 0
[PROOFSTEP]
let w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
⊢ r = 0
[PROOFSTEP]
have : Mono (cokernel.desc g h hgh.w) := mono_cokernel_desc_of_exact _ _ hgh
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝¹ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this : Mono (cokernel.desc g h (_ : g ≫ h = 0))
⊢ r = 0
[PROOFSTEP]
have : Mono v :=
  mono_inl_of_factor_thru_epi_mono_factorization _ _ (cokernel.π g) (cokernel.desc g h hgh.w ≫ δ) (by simp)
    (cokernel.desc _ _ hz) (by simp) _ (colimit.isColimit _)
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝¹ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this : Mono (cokernel.desc g h (_ : g ≫ h = 0))
⊢ cokernel.π g ≫ cokernel.desc g h (_ : g ≫ h = 0) ≫ δ = h ≫ δ
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝¹ : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this : Mono (cokernel.desc g h (_ : g ≫ h = 0))
⊢ cokernel.π g ≫ cokernel.desc g (γ ≫ z) hz = γ ≫ z
[PROOFSTEP]
simp
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
⊢ r = 0
[PROOFSTEP]
have hzv : z ≫ v = h' ≫ w :=
  (cancel_epi γ).1 <|
    calc
      γ ≫ z ≫ v = h ≫ δ ≫ w := by rw [← Category.assoc, pushout.condition, Category.assoc]
      _ = γ ≫ h' ≫ w := by rw [reassoc_of% comm₃]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
⊢ γ ≫ z ≫ v = h ≫ δ ≫ w
[PROOFSTEP]
rw [← Category.assoc, pushout.condition, Category.assoc]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
⊢ h ≫ δ ≫ w = γ ≫ h' ≫ w
[PROOFSTEP]
rw [reassoc_of% comm₃]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
hzv : z ≫ v = h' ≫ w
⊢ r = 0
[PROOFSTEP]
suffices (r ≫ y) ≫ v = 0 from zero_of_comp_mono _ (zero_of_comp_mono _ this)
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
hzv : z ≫ v = h' ≫ w
⊢ (r ≫ y) ≫ v = 0
[PROOFSTEP]
calc
  (r ≫ y) ≫ v = g' ≫ z ≫ v := by rw [pushout.condition, Category.assoc]
  _ = g' ≫ h' ≫ w := by rw [hzv]
  _ = 0 ≫ w := (hg'h'.w_assoc _)
  _ = 0 := HasZeroMorphisms.zero_comp _ _
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
hzv : z ≫ v = h' ≫ w
⊢ (r ≫ y) ≫ v = g' ≫ z ≫ v
[PROOFSTEP]
rw [pushout.condition, Category.assoc]
[GOAL]
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
hgh : Exact g h
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hα : Epi α
hγ : Epi γ
hδ : Mono δ
R : V
r : B' ⟶ R
hβr : β ≫ r = 0
hf'r : f' ≫ r = 0
y : R ⟶ pushout r g' := pushout.inl
z : C' ⟶ pushout r g' := pushout.inr
this✝² : Mono (cokernel.desc f' g' (_ : f' ≫ g' = 0))
this✝¹ : Mono y
hz : g ≫ γ ≫ z = 0
v : pushout r g' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inl
w : D' ⟶ pushout (γ ≫ z) (h ≫ δ) := pushout.inr
this✝ : Mono (cokernel.desc g h (_ : g ≫ h = 0))
this : Mono v
hzv : z ≫ v = h' ≫ w
⊢ g' ≫ z ≫ v = g' ≫ h' ≫ w
[PROOFSTEP]
rw [hzv]
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
⊢ Mono γ
[PROOFSTEP]
apply mono_of_epi_of_mono_of_mono comm₁ comm₂ comm₃ hfg hgh hf'g'
[GOAL]
case hα
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
⊢ Epi α
[PROOFSTEP]
infer_instance
[GOAL]
case hβ
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
⊢ Mono β
[PROOFSTEP]
infer_instance
[GOAL]
case hδ
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
⊢ Mono δ
[PROOFSTEP]
infer_instance
[GOAL]
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
this : Mono γ
⊢ Epi γ
[PROOFSTEP]
apply epi_of_epi_of_epi_of_mono comm₂ comm₃ comm₄ hhi hg'h' hh'i'
[GOAL]
case hα
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
this : Mono γ
⊢ Epi β
[PROOFSTEP]
infer_instance
[GOAL]
case hγ
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
this : Mono γ
⊢ Epi δ
[PROOFSTEP]
infer_instance
[GOAL]
case hδ
V : Type u
inst✝⁵ : Category.{v, u} V
inst✝⁴ : Abelian V
A B C D A' B' C' D' : V
f : A ⟶ B
g : B ⟶ C
h : C ⟶ D
f' : A' ⟶ B'
g' : B' ⟶ C'
h' : C' ⟶ D'
α : A ⟶ A'
β : B ⟶ B'
γ : C ⟶ C'
δ : D ⟶ D'
comm₁ : α ≫ f' = f ≫ β
comm₂ : β ≫ g' = g ≫ γ
comm₃ : γ ≫ h' = h ≫ δ
E E' : V
i : D ⟶ E
i' : D' ⟶ E'
ε : E ⟶ E'
comm₄ : δ ≫ i' = i ≫ ε
hfg : Exact f g
hgh : Exact g h
hhi : Exact h i
hf'g' : Exact f' g'
hg'h' : Exact g' h'
hh'i' : Exact h' i'
inst✝³ : Epi α
inst✝² : IsIso β
inst✝¹ : IsIso δ
inst✝ : Mono ε
this : Mono γ
⊢ Mono ε
[PROOFSTEP]
infer_instance


[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
⊢ Category.{?u.1823, u + 1} (Bundled c)
[PROOFSTEP]
refine'
  { Hom := fun X Y => @hom X Y X.str Y.str
    id := fun X => @BundledHom.id c hom 𝒞 X X.str
    comp := @fun X Y Z f g => @BundledHom.comp c hom 𝒞 X Y Z X.str Y.str Z.str g f
    comp_id := _
    id_comp := _
    assoc := _ }
[GOAL]
case refine'_1
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
⊢ ∀ {X Y : Bundled c} (f : X ⟶ Y), 𝟙 X ≫ f = f
[PROOFSTEP]
intros
[GOAL]
case refine'_2
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
⊢ ∀ {X Y : Bundled c} (f : X ⟶ Y), f ≫ 𝟙 Y = f
[PROOFSTEP]
intros
[GOAL]
case refine'_3
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
⊢ ∀ {W X Y Z : Bundled c} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
intros
[GOAL]
case refine'_1
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ : Bundled c
f✝ : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f✝ = f✝
[PROOFSTEP]
apply 𝒞.hom_ext
[GOAL]
case refine'_2
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ : Bundled c
f✝ : X✝ ⟶ Y✝
⊢ f✝ ≫ 𝟙 Y✝ = f✝
[PROOFSTEP]
apply 𝒞.hom_ext
[GOAL]
case refine'_3
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
W✝ X✝ Y✝ Z✝ : Bundled c
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
[PROOFSTEP]
apply 𝒞.hom_ext
[GOAL]
case refine'_1.a
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ : Bundled c
f✝ : X✝ ⟶ Y✝
⊢ toFun 𝒞 X✝.str Y✝.str (𝟙 X✝ ≫ f✝) = toFun 𝒞 X✝.str Y✝.str f✝
[PROOFSTEP]
aesop_cat
[GOAL]
case refine'_2.a
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ : Bundled c
f✝ : X✝ ⟶ Y✝
⊢ toFun 𝒞 X✝.str Y✝.str (f✝ ≫ 𝟙 Y✝) = toFun 𝒞 X✝.str Y✝.str f✝
[PROOFSTEP]
aesop_cat
[GOAL]
case refine'_3.a
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
W✝ X✝ Y✝ Z✝ : Bundled c
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
⊢ toFun 𝒞 W✝.str Z✝.str ((f✝ ≫ g✝) ≫ h✝) = toFun 𝒞 W✝.str Z✝.str (f✝ ≫ g✝ ≫ h✝)
[PROOFSTEP]
aesop_cat
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ Z✝ : Bundled c
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => ↑X, map := fun X Y f => toFun 𝒞 X.str Y.str f }.map (f ≫ g) =
    { obj := fun X => ↑X, map := fun X Y f => toFun 𝒞 X.str Y.str f }.map f ≫
      { obj := fun X => ↑X, map := fun X Y f => toFun 𝒞 X.str Y.str f }.map g
[PROOFSTEP]
dsimp
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ Z✝ : Bundled c
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ toFun 𝒞 X✝.str Z✝.str (f ≫ g) = toFun 𝒞 X✝.str Y✝.str f ≫ toFun 𝒞 Y✝.str Z✝.str g
[PROOFSTEP]
erw [𝒞.comp_toFun]
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ Z✝ : Bundled c
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ toFun 𝒞 Y✝.str Z✝.str g ∘ toFun 𝒞 X✝.str Y✝.str f = toFun 𝒞 X✝.str Y✝.str f ≫ toFun 𝒞 Y✝.str Z✝.str g
[PROOFSTEP]
rfl
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
⊢ ∀ {X Y : Bundled c},
    Function.Injective (Functor.mk { obj := fun X => ↑X, map := fun X Y f => toFun 𝒞 X.str Y.str f }).map
[PROOFSTEP]
intros
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
X✝ Y✝ : Bundled c
⊢ Function.Injective (Functor.mk { obj := fun X => ↑X, map := fun X Y f => toFun 𝒞 X.str Y.str f }).map
[PROOFSTEP]
apply 𝒞.hom_ext
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
d : Type u → Type u
hom_d : ⦃α β : Type u⦄ → d α → d β → Type u
inst✝ : BundledHom hom_d
obj : ⦃α : Type u⦄ → c α → d α
map : {X Y : Bundled c} → (X ⟶ Y) → (Bundled.map obj X ⟶ Bundled.map obj Y)
h_map : ∀ {X Y : Bundled c} (f : X ⟶ Y), ↑(map f) = ↑f
⊢ ∀ {X Y : Bundled c} {f : X ⟶ Y}, HEq ((forget (Bundled d)).map ((fun {X Y} => map) f)) ((forget (Bundled c)).map f)
[PROOFSTEP]
intros X Y f
[GOAL]
c : Type u → Type u
hom : ⦃α β : Type u⦄ → c α → c β → Type u
𝒞 : BundledHom hom
d : Type u → Type u
hom_d : ⦃α β : Type u⦄ → d α → d β → Type u
inst✝ : BundledHom hom_d
obj : ⦃α : Type u⦄ → c α → d α
map : {X Y : Bundled c} → (X ⟶ Y) → (Bundled.map obj X ⟶ Bundled.map obj Y)
h_map : ∀ {X Y : Bundled c} (f : X ⟶ Y), ↑(map f) = ↑f
X Y : Bundled c
f : X ⟶ Y
⊢ HEq ((forget (Bundled d)).map ((fun {X Y} => map) f)) ((forget (Bundled c)).map f)
[PROOFSTEP]
rw [heq_eq_eq, forget_map_eq_coe, forget_map_eq_coe, h_map f]


[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : Discrete PUnit ⥤ C
⊢ ∀ ⦃X Y : Discrete PUnit⦄ (f : X ⟶ Y),
    ((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).map f ≫
        (fun x =>
            match x with
            | { as := PUnit.unit } =>
              𝟙 (((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit }))
          Y =
      (fun x =>
            match x with
            | { as := PUnit.unit } =>
              𝟙 (((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit }))
          X ≫
        F.map f
[PROOFSTEP]
intro X Y f
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : Discrete PUnit ⥤ C
X Y : Discrete PUnit
f : X ⟶ Y
⊢ ((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).map f ≫
      (fun x =>
          match x with
          | { as := PUnit.unit } =>
            𝟙 (((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit }))
        Y =
    (fun x =>
          match x with
          | { as := PUnit.unit } =>
            𝟙 (((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit }))
        X ≫
      F.map f
[PROOFSTEP]
match X, Y, f with
| .mk A, .mk B, .up g => aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : Discrete PUnit ⥤ C
X Y : Discrete PUnit
f : X ⟶ Y
A B : PUnit
g : PLift ({ as := A }.as = { as := B }.as)
⊢ ((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).map { down := g } ≫
      (fun x =>
          match x with
          | { as := PUnit.unit } =>
            𝟙 (((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit }))
        { as := B } =
    (fun x =>
          match x with
          | { as := PUnit.unit } =>
            𝟙 (((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).obj { as := PUnit.unit }))
        { as := A } ≫
      F.map { down := g }
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cone F
j j' : J
f : j ⟶ j'
⊢ NatTrans.app c.π j ≫ F.map f = NatTrans.app c.π j'
[PROOFSTEP]
rw [← c.π.naturality f]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cone F
j j' : J
f : j ⟶ j'
⊢ ((const J).obj c.pt).map f ≫ NatTrans.app c.π j' = NatTrans.app c.π j'
[PROOFSTEP]
apply id_comp
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : Discrete PUnit ⥤ C
⊢ ∀ ⦃X Y : Discrete PUnit⦄ (f : X ⟶ Y),
    F.map f ≫
        (fun x =>
            match x with
            | { as := PUnit.unit } => 𝟙 (F.obj { as := PUnit.unit }))
          Y =
      (fun x =>
            match x with
            | { as := PUnit.unit } => 𝟙 (F.obj { as := PUnit.unit }))
          X ≫
        ((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).map f
[PROOFSTEP]
intro X Y f
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : Discrete PUnit ⥤ C
X Y : Discrete PUnit
f : X ⟶ Y
⊢ F.map f ≫
      (fun x =>
          match x with
          | { as := PUnit.unit } => 𝟙 (F.obj { as := PUnit.unit }))
        Y =
    (fun x =>
          match x with
          | { as := PUnit.unit } => 𝟙 (F.obj { as := PUnit.unit }))
        X ≫
      ((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).map f
[PROOFSTEP]
match X, Y, f with
| .mk A, .mk B, .up g => aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : Discrete PUnit ⥤ C
X Y : Discrete PUnit
f : X ⟶ Y
A B : PUnit
g : PLift ({ as := A }.as = { as := B }.as)
⊢ F.map { down := g } ≫
      (fun x =>
          match x with
          | { as := PUnit.unit } => 𝟙 (F.obj { as := PUnit.unit }))
        { as := B } =
    (fun x =>
          match x with
          | { as := PUnit.unit } => 𝟙 (F.obj { as := PUnit.unit }))
        { as := A } ≫
      ((const (Discrete PUnit)).obj (F.obj { as := PUnit.unit })).map { down := g }
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
j j' : J
f : j ⟶ j'
⊢ F.map f ≫ NatTrans.app c.ι j' = NatTrans.app c.ι j
[PROOFSTEP]
rw [c.ι.naturality f]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
j j' : J
f : j ⟶ j'
⊢ NatTrans.app c.ι j ≫ ((const J).obj c.pt).map f = NatTrans.app c.ι j
[PROOFSTEP]
apply comp_id
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
⊢ ((fun c => { fst := op c.pt, snd := c.π }) ≫ fun c => { pt := c.fst.unop, π := c.snd }) = 𝟙 (Cone F)
[PROOFSTEP]
funext X
[GOAL]
case h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
X : Cone F
⊢ ((fun c => { fst := op c.pt, snd := c.π }) ≫ fun c => { pt := c.fst.unop, π := c.snd }) X = 𝟙 (Cone F) X
[PROOFSTEP]
cases X
[GOAL]
case h.mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
pt✝ : C
π✝ : (const J).obj pt✝ ⟶ F
⊢ ((fun c => { fst := op c.pt, snd := c.π }) ≫ fun c => { pt := c.fst.unop, π := c.snd }) { pt := pt✝, π := π✝ } =
    𝟙 (Cone F) { pt := pt✝, π := π✝ }
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
⊢ ((fun c => { pt := c.fst.unop, π := c.snd }) ≫ fun c => { fst := op c.pt, snd := c.π }) =
    𝟙 ((X : Cᵒᵖ) × (Functor.cones F).obj X)
[PROOFSTEP]
funext X
[GOAL]
case h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
X : (X : Cᵒᵖ) × (Functor.cones F).obj X
⊢ ((fun c => { pt := c.fst.unop, π := c.snd }) ≫ fun c => { fst := op c.pt, snd := c.π }) X =
    𝟙 ((X : Cᵒᵖ) × (Functor.cones F).obj X) X
[PROOFSTEP]
cases X
[GOAL]
case h.mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
fst✝ : Cᵒᵖ
snd✝ : (Functor.cones F).obj fst✝
⊢ ((fun c => { pt := c.fst.unop, π := c.snd }) ≫ fun c => { fst := op c.pt, snd := c.π }) { fst := fst✝, snd := snd✝ } =
    𝟙 ((X : Cᵒᵖ) × (Functor.cones F).obj X) { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
⊢ ((fun c => { fst := c.pt, snd := c.ι }) ≫ fun c => { pt := c.fst, ι := c.snd }) = 𝟙 (Cocone F)
[PROOFSTEP]
funext X
[GOAL]
case h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
X : Cocone F
⊢ ((fun c => { fst := c.pt, snd := c.ι }) ≫ fun c => { pt := c.fst, ι := c.snd }) X = 𝟙 (Cocone F) X
[PROOFSTEP]
cases X
[GOAL]
case h.mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
pt✝ : C
ι✝ : F ⟶ (const J).obj pt✝
⊢ ((fun c => { fst := c.pt, snd := c.ι }) ≫ fun c => { pt := c.fst, ι := c.snd }) { pt := pt✝, ι := ι✝ } =
    𝟙 (Cocone F) { pt := pt✝, ι := ι✝ }
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
⊢ ((fun c => { pt := c.fst, ι := c.snd }) ≫ fun c => { fst := c.pt, snd := c.ι }) =
    𝟙 ((X : C) × (Functor.cocones F).obj X)
[PROOFSTEP]
funext X
[GOAL]
case h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
X : (X : C) × (Functor.cocones F).obj X
⊢ ((fun c => { pt := c.fst, ι := c.snd }) ≫ fun c => { fst := c.pt, snd := c.ι }) X =
    𝟙 ((X : C) × (Functor.cocones F).obj X) X
[PROOFSTEP]
cases X
[GOAL]
case h.mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F✝ F : J ⥤ C
fst✝ : C
snd✝ : (Functor.cocones F).obj fst✝
⊢ ((fun c => { pt := c.fst, ι := c.snd }) ≫ fun c => { fst := c.pt, snd := c.ι }) { fst := fst✝, snd := snd✝ } =
    𝟙 ((X : C) × (Functor.cocones F).obj X) { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
rfl
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cone F
f g : c ⟶ c'
w : f.Hom = g.Hom
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cone F
g : c ⟶ c'
Hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), Hom✝ ≫ NatTrans.app c'.π j = NatTrans.app c.π j
w : (mk Hom✝).Hom = g.Hom
⊢ mk Hom✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cone F
Hom✝¹ : c.pt ⟶ c'.pt
w✝¹ : ∀ (j : J), Hom✝¹ ≫ NatTrans.app c'.π j = NatTrans.app c.π j
Hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), Hom✝ ≫ NatTrans.app c'.π j = NatTrans.app c.π j
w : (mk Hom✝¹).Hom = (mk Hom✝).Hom
⊢ mk Hom✝¹ = mk Hom✝
[PROOFSTEP]
congr
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝² : Category.{v₂, u₂} K✝
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F K : J ⥤ C
c d : Cone K
f : c ⟶ d
i : IsIso f.Hom
⊢ f ≫ ConeMorphism.mk (inv f.Hom) = 𝟙 c ∧ ConeMorphism.mk (inv f.Hom) ≫ f = 𝟙 d
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
e : K ≌ J
s : Cone (e.functor ⋙ F)
⊢ ∀ (j : K),
    NatTrans.app
        (((whiskering e.inverse ⋙ postcompose (Equivalence.invFunIdAssoc e F).hom) ⋙ whiskering e.functor).obj s).π j =
      (Iso.refl
            (((whiskering e.inverse ⋙ postcompose (Equivalence.invFunIdAssoc e F).hom) ⋙ whiskering e.functor).obj
                s).pt).hom ≫
        NatTrans.app ((𝟭 (Cone (e.functor ⋙ F))).obj s).π j
[PROOFSTEP]
intro k
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
e : K ≌ J
s : Cone (e.functor ⋙ F)
k : K
⊢ NatTrans.app
      (((whiskering e.inverse ⋙ postcompose (Equivalence.invFunIdAssoc e F).hom) ⋙ whiskering e.functor).obj s).π k =
    (Iso.refl
          (((whiskering e.inverse ⋙ postcompose (Equivalence.invFunIdAssoc e F).hom) ⋙ whiskering e.functor).obj
              s).pt).hom ≫
      NatTrans.app ((𝟭 (Cone (e.functor ⋙ F))).obj s).π k
[PROOFSTEP]
simpa [e.counit_app_functor] using s.w (e.unitInv.app k)
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
A : Cone F
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    ((const J).obj (G.obj A.pt)).map f ≫ (fun j => G.map (NatTrans.app A.π j)) Y =
      (fun j => G.map (NatTrans.app A.π j)) X ≫ (F ⋙ G).map f
[PROOFSTEP]
intros
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
A : Cone F
X✝ Y✝ : J
f✝ : X✝ ⟶ Y✝
⊢ ((const J).obj (G.obj A.pt)).map f✝ ≫ (fun j => G.map (NatTrans.app A.π j)) Y✝ =
    (fun j => G.map (NatTrans.app A.π j)) X✝ ≫ (F ⋙ G).map f✝
[PROOFSTEP]
erw [← G.map_comp]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
A : Cone F
X✝ Y✝ : J
f✝ : X✝ ⟶ Y✝
⊢ ((const J).obj (G.obj A.pt)).map f✝ ≫ (fun j => G.map (NatTrans.app A.π j)) Y✝ =
    G.map (NatTrans.app A.π X✝ ≫ F.map f✝)
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
X✝ Y✝ : Cone F
f : X✝ ⟶ Y✝
j : J
⊢ G.map f.Hom ≫
      NatTrans.app ((fun A => { pt := G.obj A.pt, π := NatTrans.mk fun j => G.map (NatTrans.app A.π j) }) Y✝).π j =
    NatTrans.app ((fun A => { pt := G.obj A.pt, π := NatTrans.mk fun j => G.map (NatTrans.app A.π j) }) X✝).π j
[PROOFSTEP]
simp [-ConeMorphism.w, ← f.w j]
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝¹ : Full G
inst✝ : Faithful G
X✝ Y✝ : Cone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
j : J
⊢ G.map (G.preimage t.Hom ≫ NatTrans.app Y✝.π j) = G.map (NatTrans.app X✝.π j)
[PROOFSTEP]
simpa using t.w j
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝ : Faithful G
c c' : Cone F
f g : c ⟶ c'
e : (functoriality F G).map f = (functoriality F G).map g
⊢ f = g
[PROOFSTEP]
apply ConeMorphism.ext f g
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝ : Faithful G
c c' : Cone F
f g : c ⟶ c'
e : (functoriality F G).map f = (functoriality F G).map g
⊢ f.Hom = g.Hom
[PROOFSTEP]
let f := ConeMorphism.mk.inj e
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝ : Faithful G
c c' : Cone F
f✝ g : c ⟶ c'
e : (functoriality F G).map f✝ = (functoriality F G).map g
f : G.map f✝.Hom = G.map g.Hom := ConeMorphism.mk.inj e
⊢ f✝.Hom = g.Hom
[PROOFSTEP]
apply G.map_injective f
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝³ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
K : J ⥤ C
⊢ ReflectsIsomorphisms (functoriality K F)
[PROOFSTEP]
constructor
[GOAL]
case reflects
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝³ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
K : J ⥤ C
⊢ ∀ {A B : Cone K} (f : A ⟶ B) [inst : IsIso ((functoriality K F).map f)], IsIso f
[PROOFSTEP]
intro A B f _
[GOAL]
case reflects
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : ReflectsIsomorphisms F
K : J ⥤ C
A B : Cone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
⊢ IsIso f
[PROOFSTEP]
haveI : IsIso (F.map f.Hom) := (Cones.forget (K ⋙ F)).map_isIso ((Cones.functoriality K F).map f)
[GOAL]
case reflects
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : ReflectsIsomorphisms F
K : J ⥤ C
A B : Cone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
this : IsIso (F.map f.Hom)
⊢ IsIso f
[PROOFSTEP]
haveI := ReflectsIsomorphisms.reflects F f.Hom
[GOAL]
case reflects
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : ReflectsIsomorphisms F
K : J ⥤ C
A B : Cone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
this✝ : IsIso (F.map f.Hom)
this : IsIso f.Hom
⊢ IsIso f
[PROOFSTEP]
apply cone_iso_of_hom_iso
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cocone F
f g : c ⟶ c'
w : f.Hom = g.Hom
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cocone F
g : c ⟶ c'
Hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), NatTrans.app c.ι j ≫ Hom✝ = NatTrans.app c'.ι j
w : (mk Hom✝).Hom = g.Hom
⊢ mk Hom✝ = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c c' : Cocone F
Hom✝¹ : c.pt ⟶ c'.pt
w✝¹ : ∀ (j : J), NatTrans.app c.ι j ≫ Hom✝¹ = NatTrans.app c'.ι j
Hom✝ : c.pt ⟶ c'.pt
w✝ : ∀ (j : J), NatTrans.app c.ι j ≫ Hom✝ = NatTrans.app c'.ι j
w : (mk Hom✝¹).Hom = (mk Hom✝).Hom
⊢ mk Hom✝¹ = mk Hom✝
[PROOFSTEP]
congr
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝² : Category.{v₂, u₂} K✝
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F K : J ⥤ C
c d : Cocone K
f : c ⟶ d
i : IsIso f.Hom
⊢ f ≫ CoconeMorphism.mk (inv f.Hom) = 𝟙 c ∧ CoconeMorphism.mk (inv f.Hom) ≫ f = 𝟙 d
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
e : K ≌ J
s : Cocone (e.functor ⋙ F)
k : K
⊢ NatTrans.app
        (((whiskering e.inverse ⋙
                  precompose
                    ((leftUnitor F).inv ≫ whiskerRight e.counitIso.inv F ≫ (associator e.inverse e.functor F).inv)) ⋙
                whiskering e.functor).obj
            s).ι
        k ≫
      (Iso.refl
          (((whiskering e.inverse ⋙
                    precompose
                      ((leftUnitor F).inv ≫ whiskerRight e.counitIso.inv F ≫ (associator e.inverse e.functor F).inv)) ⋙
                  whiskering e.functor).obj
              s).pt).hom =
    NatTrans.app ((𝟭 (Cocone (e.functor ⋙ F))).obj s).ι k
[PROOFSTEP]
simpa [e.counitInv_app_functor k] using s.w (e.unit.app k)
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
A : Cocone F
⊢ ∀ ⦃X Y : J⦄ (f : X ⟶ Y),
    (F ⋙ G).map f ≫ (fun j => G.map (NatTrans.app A.ι j)) Y =
      (fun j => G.map (NatTrans.app A.ι j)) X ≫ ((const J).obj (G.obj A.pt)).map f
[PROOFSTEP]
intros
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
A : Cocone F
X✝ Y✝ : J
f✝ : X✝ ⟶ Y✝
⊢ (F ⋙ G).map f✝ ≫ (fun j => G.map (NatTrans.app A.ι j)) Y✝ =
    (fun j => G.map (NatTrans.app A.ι j)) X✝ ≫ ((const J).obj (G.obj A.pt)).map f✝
[PROOFSTEP]
erw [← G.map_comp]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
A : Cocone F
X✝ Y✝ : J
f✝ : X✝ ⟶ Y✝
⊢ G.map (F.map f✝ ≫ NatTrans.app A.ι Y✝) =
    (fun j => G.map (NatTrans.app A.ι j)) X✝ ≫ ((const J).obj (G.obj A.pt)).map f✝
[PROOFSTEP]
aesop_cat
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
X✝ Y✝ : Cocone F
f : X✝ ⟶ Y✝
⊢ ∀ (j : J),
    NatTrans.app ((fun A => { pt := G.obj A.pt, ι := NatTrans.mk fun j => G.map (NatTrans.app A.ι j) }) X✝).ι j ≫
        G.map f.Hom =
      NatTrans.app ((fun A => { pt := G.obj A.pt, ι := NatTrans.mk fun j => G.map (NatTrans.app A.ι j) }) Y✝).ι j
[PROOFSTEP]
intros
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
X✝ Y✝ : Cocone F
f : X✝ ⟶ Y✝
j✝ : J
⊢ NatTrans.app ((fun A => { pt := G.obj A.pt, ι := NatTrans.mk fun j => G.map (NatTrans.app A.ι j) }) X✝).ι j✝ ≫
      G.map f.Hom =
    NatTrans.app ((fun A => { pt := G.obj A.pt, ι := NatTrans.mk fun j => G.map (NatTrans.app A.ι j) }) Y✝).ι j✝
[PROOFSTEP]
rw [← Functor.map_comp, CoconeMorphism.w]
[GOAL]
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K : Type u₂
inst✝⁴ : Category.{v₂, u₂} K
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝¹ : Full G
inst✝ : Faithful G
X✝ Y✝ : Cocone F
t : (functoriality F G).obj X✝ ⟶ (functoriality F G).obj Y✝
j : J
⊢ G.map (NatTrans.app X✝.ι j ≫ G.preimage t.Hom) = G.map (NatTrans.app Y✝.ι j)
[PROOFSTEP]
simpa using t.w j
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝ : Faithful G
X Y : Cocone F
f g : X ⟶ Y
e : (functoriality F G).map f = (functoriality F G).map g
⊢ f = g
[PROOFSTEP]
apply CoconeMorphism.ext
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝ : Faithful G
X Y : Cocone F
f g : X ⟶ Y
e : (functoriality F G).map f = (functoriality F G).map g
⊢ f.Hom = g.Hom
[PROOFSTEP]
let h := CoconeMorphism.mk.inj e
[GOAL]
case w
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K : Type u₂
inst✝³ : Category.{v₂, u₂} K
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
inst✝ : Faithful G
X Y : Cocone F
f g : X ⟶ Y
e : (functoriality F G).map f = (functoriality F G).map g
h : G.map f.Hom = G.map g.Hom := CoconeMorphism.mk.inj e
⊢ f.Hom = g.Hom
[PROOFSTEP]
apply G.map_injective h
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
G : C ⥤ D
e : C ≌ D
f : (F ⋙ e.functor) ⋙ e.inverse ≅ F :=
  associator F e.functor e.inverse ≪≫ isoWhiskerLeft F e.unitIso.symm ≪≫ rightUnitor F
c : Cocone (F ⋙ e.functor)
j : J
⊢ NatTrans.app
        (((functoriality (F ⋙ e.functor) e.inverse ⋙ (precomposeEquivalence f.symm).functor) ⋙
                functoriality F e.functor).obj
            c).ι
        j ≫
      (e.counitIso.app c.pt).hom =
    NatTrans.app ((𝟭 (Cocone (F ⋙ e.functor))).obj c).ι j
[PROOFSTEP]
simp [← Equivalence.counitInv_app_functor]
[GOAL]
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝³ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
K : J ⥤ C
⊢ ReflectsIsomorphisms (functoriality K F)
[PROOFSTEP]
constructor
[GOAL]
case reflects
J : Type u₁
inst✝⁴ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝³ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝² : Category.{v₃, u₃} C
D : Type u₄
inst✝¹ : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝ : ReflectsIsomorphisms F
K : J ⥤ C
⊢ ∀ {A B : Cocone K} (f : A ⟶ B) [inst : IsIso ((functoriality K F).map f)], IsIso f
[PROOFSTEP]
intro A B f _
[GOAL]
case reflects
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : ReflectsIsomorphisms F
K : J ⥤ C
A B : Cocone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
⊢ IsIso f
[PROOFSTEP]
haveI : IsIso (F.map f.Hom) := (Cocones.forget (K ⋙ F)).map_isIso ((Cocones.functoriality K F).map f)
[GOAL]
case reflects
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : ReflectsIsomorphisms F
K : J ⥤ C
A B : Cocone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
this : IsIso (F.map f.Hom)
⊢ IsIso f
[PROOFSTEP]
haveI := ReflectsIsomorphisms.reflects F f.Hom
[GOAL]
case reflects
J : Type u₁
inst✝⁵ : Category.{v₁, u₁} J
K✝ : Type u₂
inst✝⁴ : Category.{v₂, u₂} K✝
C : Type u₃
inst✝³ : Category.{v₃, u₃} C
D : Type u₄
inst✝² : Category.{v₄, u₄} D
F✝ : J ⥤ C
G F : C ⥤ D
inst✝¹ : ReflectsIsomorphisms F
K : J ⥤ C
A B : Cocone K
f : A ⟶ B
inst✝ : IsIso ((functoriality K F).map f)
this✝ : IsIso (F.map f.Hom)
this : IsIso f.Hom
⊢ IsIso f
[PROOFSTEP]
apply cocone_iso_of_hom_iso
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ f.Hom.op ≫ NatTrans.app (Cocone.op X).π j = NatTrans.app (Cocone.op Y).π j
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ (f.Hom.op ≫ NatTrans.app (Cocone.op X).π j).unop = (NatTrans.app (Cocone.op Y).π j).unop
[PROOFSTEP]
dsimp
[GOAL]
case a
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : Cocone F
f : X ⟶ Y
j : Jᵒᵖ
⊢ NatTrans.app X.ι j.unop ≫ f.Hom = NatTrans.app Y.ι j.unop
[PROOFSTEP]
apply CoconeMorphism.w
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ NatTrans.app ((fun c => Cone.unop c.unop) X).ι j ≫ f.unop.Hom.unop = NatTrans.app ((fun c => Cone.unop c.unop) Y).ι j
[PROOFSTEP]
apply Quiver.Hom.op_inj
[GOAL]
case a
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ (NatTrans.app ((fun c => Cone.unop c.unop) X).ι j ≫ f.unop.Hom.unop).op =
    (NatTrans.app ((fun c => Cone.unop c.unop) Y).ι j).op
[PROOFSTEP]
dsimp
[GOAL]
case a
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
j : J
⊢ f.unop.Hom ≫ NatTrans.app X.unop.π (op j) = NatTrans.app Y.unop.π (op j)
[PROOFSTEP]
apply ConeMorphism.w
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : (Cone F.op)ᵒᵖ
⊢ (Functor.mk { obj := fun c => Cone.unop c.unop, map := fun {X Y} f => CoconeMorphism.mk f.unop.Hom.unop } ⋙
          Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj
      c ≅
    (𝟭 (Cone F.op)ᵒᵖ).obj c
[PROOFSTEP]
induction c
[GOAL]
case h
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ : Cone F.op
⊢ (Functor.mk { obj := fun c => Cone.unop c.unop, map := fun {X Y} f => CoconeMorphism.mk f.unop.Hom.unop } ⋙
          Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj
      (op X✝) ≅
    (𝟭 (Cone F.op)ᵒᵖ).obj (op X✝)
[PROOFSTEP]
apply Iso.op
[GOAL]
case h.α
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X✝ : Cone F.op
⊢ X✝ ≅
    Cocone.op
      ((Functor.mk { obj := fun c => Cone.unop c.unop, map := fun {X Y} f => CoconeMorphism.mk f.unop.Hom.unop }).obj
        (op X✝))
[PROOFSTEP]
exact Cones.ext (Iso.refl _)
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
X Y : (Cone F.op)ᵒᵖ
f : X ⟶ Y
⊢ ((Functor.mk { obj := fun c => Cone.unop c.unop, map := fun {X Y} f => CoconeMorphism.mk f.unop.Hom.unop } ⋙
                Functor.mk
                  { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).map
            f ≫
          ((fun c => Opposite.rec' (fun X => Iso.op (Cones.ext (Iso.refl X.pt))) c) Y).hom).unop.Hom =
    (((fun c => Opposite.rec' (fun X => Iso.op (Cones.ext (Iso.refl X.pt))) c) X).hom ≫
          (𝟭 (Cone F.op)ᵒᵖ).map f).unop.Hom
[PROOFSTEP]
simp
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ (Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).map
        (NatTrans.app (NatIso.ofComponents fun c => Cocones.ext (Iso.refl ((𝟭 (Cocone F)).obj c).pt)).hom c) ≫
      NatTrans.app (NatIso.ofComponents fun c => Opposite.rec' (fun X => Iso.op (Cones.ext (Iso.refl X.pt))) c).hom
        ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj c) =
    𝟙 ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj c)
[PROOFSTEP]
apply Quiver.Hom.unop_inj
[GOAL]
case a
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).map
          (NatTrans.app (NatIso.ofComponents fun c => Cocones.ext (Iso.refl ((𝟭 (Cocone F)).obj c).pt)).hom c) ≫
        NatTrans.app (NatIso.ofComponents fun c => Opposite.rec' (fun X => Iso.op (Cones.ext (Iso.refl X.pt))) c).hom
          ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj
            c)).unop =
    (𝟙
        ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj
          c)).unop
[PROOFSTEP]
apply ConeMorphism.ext
[GOAL]
case a.w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).map
            (NatTrans.app (NatIso.ofComponents fun c => Cocones.ext (Iso.refl ((𝟭 (Cocone F)).obj c).pt)).hom c) ≫
          NatTrans.app (NatIso.ofComponents fun c => Opposite.rec' (fun X => Iso.op (Cones.ext (Iso.refl X.pt))) c).hom
            ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj
              c)).unop.Hom =
    (𝟙
          ((Functor.mk { obj := fun c => op (Cocone.op c), map := fun {X Y} f => (ConeMorphism.mk f.Hom.op).op }).obj
            c)).unop.Hom
[PROOFSTEP]
dsimp
[GOAL]
case a.w
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ C
c : Cocone F
⊢ 𝟙 (op c.pt) ≫ 𝟙 (op c.pt) = 𝟙 (op c.pt)
[PROOFSTEP]
apply comp_id
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
j : J
⊢ NatTrans.app (coconeOfConeLeftOp c).ι j = (NatTrans.app c.π (op j)).op
[PROOFSTEP]
dsimp only [coconeOfConeLeftOp]
[GOAL]
J : Type u₁
inst✝³ : Category.{v₁, u₁} J
K : Type u₂
inst✝² : Category.{v₂, u₂} K
C : Type u₃
inst✝¹ : Category.{v₃, u₃} C
D : Type u₄
inst✝ : Category.{v₄, u₄} D
F : J ⥤ Cᵒᵖ
c : Cone F.leftOp
j : J
⊢ NatTrans.app (NatTrans.removeLeftOp c.π) j = (NatTrans.app c.π (op j)).op
[PROOFSTEP]
simp