[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.549, u_1} C
inst✝ : HasZeroMorphisms C
A B : C
c : BinaryCofan A B
hc : IsColimit c
⊢ Mono (BinaryCofan.inl c)
[PROOFSTEP]
haveI : IsSplitMono c.inl := IsSplitMono.mk' (SplitMono.mk (hc.desc (BinaryCofan.mk (𝟙 A) 0)) (IsColimit.fac _ _ _))
[GOAL]
C : Type u_1
inst✝¹ : Category.{?u.549, u_1} C
inst✝ : HasZeroMorphisms C
A B : C
c : BinaryCofan A B
hc : IsColimit c
this : IsSplitMono (BinaryCofan.inl c)
⊢ Mono (BinaryCofan.inl c)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
⊢ Mono (BinaryCofan.inr c)
[PROOFSTEP]
haveI hc' : IsColimit (BinaryCofan.mk c.inr c.inl) :=
  BinaryCofan.IsColimit.mk _ (fun f₁ f₂ => hc.desc (BinaryCofan.mk f₂ f₁)) (by aesop_cat) (by aesop_cat)
    (fun f₁ f₂ m h₁ h₂ => BinaryCofan.IsColimit.hom_ext hc (by aesop_cat) (by aesop_cat))
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
⊢ ∀ {T : C} (f : (pair A B).obj { as := WalkingPair.right } ⟶ T) (g : (pair A B).obj { as := WalkingPair.left } ⟶ T),
    BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)) ≫
        (fun {T} f₁ f₂ => IsColimit.desc hc (BinaryCofan.mk f₂ f₁)) f g =
      f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
⊢ ∀ {T : C} (f : (pair A B).obj { as := WalkingPair.right } ⟶ T) (g : (pair A B).obj { as := WalkingPair.left } ⟶ T),
    BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)) ≫
        (fun {T} f₁ f₂ => IsColimit.desc hc (BinaryCofan.mk f₂ f₁)) f g =
      g
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
T✝ : C
f₁ : (pair A B).obj { as := WalkingPair.right } ⟶ T✝
f₂ : (pair A B).obj { as := WalkingPair.left } ⟶ T✝
m : (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)).pt ⟶ T✝
h₁ : BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)) ≫ m = f₂
⊢ BinaryCofan.inl c ≫ m = BinaryCofan.inl c ≫ (fun {T} f₁ f₂ => IsColimit.desc hc (BinaryCofan.mk f₂ f₁)) f₁ f₂
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
T✝ : C
f₁ : (pair A B).obj { as := WalkingPair.right } ⟶ T✝
f₂ : (pair A B).obj { as := WalkingPair.left } ⟶ T✝
m : (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)).pt ⟶ T✝
h₁ : BinaryCofan.inl (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c)) ≫ m = f₂
⊢ BinaryCofan.inr c ≫ m = BinaryCofan.inr c ≫ (fun {T} f₁ f₂ => IsColimit.desc hc (BinaryCofan.mk f₂ f₁)) f₁ f₂
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
A B : C
inst✝ : MonoCoprod C
c : BinaryCofan A B
hc : IsColimit c
hc' : IsColimit (BinaryCofan.mk (BinaryCofan.inr c) (BinaryCofan.inl c))
⊢ Mono (BinaryCofan.inr c)
[PROOFSTEP]
exact binaryCofan_inl _ hc'
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Mono (BinaryCofan.inl c₁) ↔ Mono (BinaryCofan.inl c₂)
[PROOFSTEP]
suffices ∀ (c₁ c₂ : BinaryCofan A B) (_ : IsColimit c₁) (_ : IsColimit c₂) (_ : Mono c₁.inl), Mono c₂.inl by
  exact ⟨fun h₁ => this _ _ hc₁ hc₂ h₁, fun h₂ => this _ _ hc₂ hc₁ h₂⟩
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
this : ∀ (c₁ c₂ : BinaryCofan A B), IsColimit c₁ → IsColimit c₂ → Mono (BinaryCofan.inl c₁) → Mono (BinaryCofan.inl c₂)
⊢ Mono (BinaryCofan.inl c₁) ↔ Mono (BinaryCofan.inl c₂)
[PROOFSTEP]
exact ⟨fun h₁ => this _ _ hc₁ hc₂ h₁, fun h₂ => this _ _ hc₂ hc₁ h₂⟩
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ ∀ (c₁ c₂ : BinaryCofan A B), IsColimit c₁ → IsColimit c₂ → Mono (BinaryCofan.inl c₁) → Mono (BinaryCofan.inl c₂)
[PROOFSTEP]
intro c₁ c₂ hc₁ hc₂
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
⊢ Mono (BinaryCofan.inl c₁) → Mono (BinaryCofan.inl c₂)
[PROOFSTEP]
intro
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
A B : C
c₁✝ c₂✝ : BinaryCofan A B
hc₁✝ : IsColimit c₁✝
hc₂✝ : IsColimit c₂✝
c₁ c₂ : BinaryCofan A B
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
x✝ : Mono (BinaryCofan.inl c₁)
⊢ Mono (BinaryCofan.inl c₂)
[PROOFSTEP]
simpa only [IsColimit.comp_coconePointUniqueUpToIso_hom] using mono_comp c₁.inl (hc₁.coconePointUniqueUpToIso hc₂).hom
[GOAL]
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (A B : C), ∃ c x, Mono (BinaryCofan.inl c)
A B : C
c' : BinaryCofan A B
hc' : IsColimit c'
⊢ Mono (BinaryCofan.inl c')
[PROOFSTEP]
obtain ⟨c, hc₁, hc₂⟩ := h A B
[GOAL]
case intro.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
h : ∀ (A B : C), ∃ c x, Mono (BinaryCofan.inl c)
A B : C
c' : BinaryCofan A B
hc' : IsColimit c'
c : BinaryCofan A B
hc₁ : IsColimit c
hc₂ : Mono (BinaryCofan.inl c)
⊢ Mono (BinaryCofan.inl c')
[PROOFSTEP]
simpa only [mono_inl_iff hc' hc₁] using hc₂
[GOAL]
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B : Type u
⊢ ∃ c x, Mono (BinaryCofan.inl c)
[PROOFSTEP]
refine' ⟨BinaryCofan.mk (Sum.inl : A ⟶ Sum A B) Sum.inr, _, _⟩
[GOAL]
case refine'_1
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B : Type u
⊢ IsColimit (BinaryCofan.mk Sum.inl Sum.inr)
[PROOFSTEP]
exact
  BinaryCofan.IsColimit.mk _
    (fun f₁ f₂ x => by
      rcases x with x | x
      exacts [f₁ x, f₂ x])
    (fun f₁ f₂ => by rfl) (fun f₁ f₂ => by rfl)
    (fun f₁ f₂ m h₁ h₂ => by
      funext x
      rcases x with x | x
      · exact congr_fun h₁ x
      · exact congr_fun h₂ x)
[GOAL]
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
x : (BinaryCofan.mk Sum.inl Sum.inr).pt
⊢ T✝
[PROOFSTEP]
rcases x with x | x
[GOAL]
case inl
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
x : A
⊢ T✝
case inr C : Type u_1 inst✝ : Category.{?u.12890, u_1} C A B T✝ : Type u f₁ : A ⟶ T✝ f₂ : B ⟶ T✝ x : B ⊢ T✝
[PROOFSTEP]
exacts [f₁ x, f₂ x]
[GOAL]
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
⊢ BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) ≫
      (fun {T} f₁ f₂ x => Sum.casesOn x (fun x => f₁ x) fun x => f₂ x) f₁ f₂ =
    f₁
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
⊢ BinaryCofan.inr (BinaryCofan.mk Sum.inl Sum.inr) ≫
      (fun {T} f₁ f₂ x => Sum.casesOn x (fun x => f₁ x) fun x => f₂ x) f₁ f₂ =
    f₂
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
m : (BinaryCofan.mk Sum.inl Sum.inr).pt ⟶ T✝
h₁ : BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₂
⊢ m = (fun {T} f₁ f₂ x => Sum.casesOn x (fun x => f₁ x) fun x => f₂ x) f₁ f₂
[PROOFSTEP]
funext x
[GOAL]
case h
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
m : (BinaryCofan.mk Sum.inl Sum.inr).pt ⟶ T✝
h₁ : BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₂
x : (BinaryCofan.mk Sum.inl Sum.inr).pt
⊢ m x = (fun {T} f₁ f₂ x => Sum.casesOn x (fun x => f₁ x) fun x => f₂ x) f₁ f₂ x
[PROOFSTEP]
rcases x with x | x
[GOAL]
case h.inl
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
m : (BinaryCofan.mk Sum.inl Sum.inr).pt ⟶ T✝
h₁ : BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₂
x : A
⊢ m (Sum.inl x) = (fun {T} f₁ f₂ x => Sum.casesOn x (fun x => f₁ x) fun x => f₂ x) f₁ f₂ (Sum.inl x)
[PROOFSTEP]
exact congr_fun h₁ x
[GOAL]
case h.inr
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B T✝ : Type u
f₁ : A ⟶ T✝
f₂ : B ⟶ T✝
m : (BinaryCofan.mk Sum.inl Sum.inr).pt ⟶ T✝
h₁ : BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₁
h₂ : BinaryCofan.inr (BinaryCofan.mk Sum.inl Sum.inr) ≫ m = f₂
x : B
⊢ m (Sum.inr x) = (fun {T} f₁ f₂ x => Sum.casesOn x (fun x => f₁ x) fun x => f₂ x) f₁ f₂ (Sum.inr x)
[PROOFSTEP]
exact congr_fun h₂ x
[GOAL]
case refine'_2
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B : Type u
⊢ Mono (BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr))
[PROOFSTEP]
rw [mono_iff_injective]
[GOAL]
case refine'_2
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B : Type u
⊢ Function.Injective (BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr))
[PROOFSTEP]
intro a₁ a₂ h
[GOAL]
case refine'_2
C : Type u_1
inst✝ : Category.{?u.12890, u_1} C
A B : Type u
a₁ a₂ : (pair A B).obj { as := WalkingPair.left }
h : BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) a₁ = BinaryCofan.inl (BinaryCofan.mk Sum.inl Sum.inr) a₂
⊢ a₁ = a₂
[PROOFSTEP]
simpa using h


[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : HasPullbacks C
X Y : C
f : X ⟶ Y
g h : Over Y
k : g ⟶ h
⊢ (pullback.fst ≫ k.left) ≫ h.hom = pullback.snd ≫ f
[PROOFSTEP]
simp [pullback.condition]
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ (map f).obj g ⟶ h
[PROOFSTEP]
refine' Over.homMk _ _
[GOAL]
case refine'_1
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ ((map f).obj g).left ⟶ h.left
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ ?refine'_1 ≫ h.hom = ((map f).obj g).hom
[PROOFSTEP]
refine' Y.left ≫ pullback.fst
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ (Y.left ≫ pullback.fst) ≫ h.hom = ((map f).obj g).hom
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ (Y.left ≫ pullback.fst) ≫ h.hom = g.hom ≫ f
[PROOFSTEP]
rw [← Over.w Y, Category.assoc, pullback.condition, Category.assoc]
[GOAL]
case refine'_2
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ Y.left ≫ pullback.snd ≫ f = Y.left ≫ ((pullback f).obj h).hom ≫ f
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
X : (map f).obj g ⟶ h
⊢ (fun Y => homMk (Y.left ≫ pullback.fst))
      ((fun X => homMk (pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom))) X) =
    X
[PROOFSTEP]
ext
[GOAL]
case h
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
X : (map f).obj g ⟶ h
⊢ ((fun Y => homMk (Y.left ≫ pullback.fst))
        ((fun X => homMk (pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom))) X)).left =
    X.left
[PROOFSTEP]
dsimp
[GOAL]
case h
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
X : (map f).obj g ⟶ h
⊢ pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom) ≫ pullback.fst = X.left
[PROOFSTEP]
simp
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ (fun X => homMk (pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom)))
      ((fun Y => homMk (Y.left ≫ pullback.fst)) Y) =
    Y
[PROOFSTEP]
apply OverMorphism.ext
[GOAL]
case h
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ ((fun X => homMk (pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom)))
        ((fun Y => homMk (Y.left ≫ pullback.fst)) Y)).left =
    Y.left
[PROOFSTEP]
apply pullback.hom_ext
[GOAL]
case h.h₀
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ ((fun X => homMk (pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom)))
          ((fun Y => homMk (Y.left ≫ pullback.fst)) Y)).left ≫
      pullback.fst =
    Y.left ≫ pullback.fst
[PROOFSTEP]
dsimp
[GOAL]
case h.h₀
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ pullback.lift (Y.left ≫ pullback.fst) g.hom (_ : (homMk (Y.left ≫ pullback.fst)).left ≫ h.hom = ((map f).obj g).hom) ≫
      pullback.fst =
    Y.left ≫ pullback.fst
[PROOFSTEP]
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]
[GOAL]
case h.h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ ((fun X => homMk (pullback.lift X.left g.hom (_ : X.left ≫ h.hom = ((map f).obj g).hom)))
          ((fun Y => homMk (Y.left ≫ pullback.fst)) Y)).left ≫
      pullback.snd =
    Y.left ≫ pullback.snd
[PROOFSTEP]
dsimp
[GOAL]
case h.h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ pullback.lift (Y.left ≫ pullback.fst) g.hom (_ : (homMk (Y.left ≫ pullback.fst)).left ≫ h.hom = ((map f).obj g).hom) ≫
      pullback.snd =
    Y.left ≫ pullback.snd
[PROOFSTEP]
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app, ← Over.w Y]
[GOAL]
case h.h₁
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X : C
inst✝ : HasPullbacks C
A B : C
f : A ⟶ B
g : Over A
h : Over B
Y : g ⟶ (pullback f).obj h
⊢ Y.left ≫ ((pullback f).obj h).hom = Y.left ≫ pullback.snd
[PROOFSTEP]
rfl
[GOAL]
J : Type v
inst✝² : SmallCategory J
C : Type u
inst✝¹ : Category.{v, u} C
X✝ : C
inst✝ : HasPushouts C
X Y : C
f : X ⟶ Y
g h : Under X
k : g ⟶ h
⊢ g.hom ≫ k.right ≫ pushout.inl = f ≫ pushout.inr
[PROOFSTEP]
simp [← pushout.condition]


[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasTerminal C
inst✝ : PreservesLimit (Functor.empty C) G
F : Discrete PEmpty ⥤ D
⊢ HasLimit F
[PROOFSTEP]
haveI := HasLimit.mk ⟨_, isLimitOfHasTerminalOfPreservesLimit G⟩
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasTerminal C
inst✝ : PreservesLimit (Functor.empty C) G
F : Discrete PEmpty ⥤ D
this : HasLimit (Functor.empty D)
⊢ HasLimit F
[PROOFSTEP]
apply hasLimitOfIso F.uniqueFromEmpty.symm
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ PreservesLimit (Functor.empty C) G
[PROOFSTEP]
apply preservesLimitOfPreservesLimitCone terminalIsTerminal
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ IsLimit (G.mapCone (asEmptyCone (⊤_ C)))
[PROOFSTEP]
apply (isLimitMapConeEmptyConeEquiv _ _).symm _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
i : IsIso (terminalComparison G)
⊢ IsTerminal (G.obj (⊤_ C))
[PROOFSTEP]
exact @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (Functor.empty.{0} D)) i
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
f : G.obj (⊤_ C) ⟶ ⊤_ D
i : IsIso f
⊢ PreservesLimit (Functor.empty C) G
[PROOFSTEP]
rw [Subsingleton.elim f (terminalComparison G)] at i
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasTerminal C
inst✝ : HasTerminal D
f : G.obj (⊤_ C) ⟶ ⊤_ D
i : IsIso (terminalComparison G)
⊢ PreservesLimit (Functor.empty C) G
[PROOFSTEP]
exact PreservesTerminal.ofIsoComparison G
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝² : HasTerminal C
inst✝¹ : HasTerminal D
inst✝ : PreservesLimit (Functor.empty C) G
⊢ IsIso (terminalComparison G)
[PROOFSTEP]
rw [← PreservesTerminal.iso_hom]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝² : HasTerminal C
inst✝¹ : HasTerminal D
inst✝ : PreservesLimit (Functor.empty C) G
⊢ IsIso (PreservesTerminal.iso G).hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasInitial C
inst✝ : PreservesColimit (Functor.empty C) G
F : Discrete PEmpty ⥤ D
⊢ HasColimit F
[PROOFSTEP]
haveI := HasColimit.mk ⟨_, isColimitOfHasInitialOfPreservesColimit G⟩
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasInitial C
inst✝ : PreservesColimit (Functor.empty C) G
F : Discrete PEmpty ⥤ D
this : HasColimit (Functor.empty D)
⊢ HasColimit F
[PROOFSTEP]
apply hasColimitOfIso F.uniqueFromEmpty
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ PreservesColimit (Functor.empty C) G
[PROOFSTEP]
apply preservesColimitOfPreservesColimitCocone initialIsInitial
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ IsColimit (G.mapCocone (asEmptyCocone (⊥_ C)))
[PROOFSTEP]
apply (isColimitMapCoconeEmptyCoconeEquiv _ _).symm _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasInitial C
inst✝ : HasInitial D
i : IsIso (initialComparison G)
⊢ IsInitial (G.obj (⊥_ C))
[PROOFSTEP]
exact @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (Functor.empty.{0} D)) i
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasInitial C
inst✝ : HasInitial D
f : ⊥_ D ⟶ G.obj (⊥_ C)
i : IsIso f
⊢ PreservesColimit (Functor.empty C) G
[PROOFSTEP]
rw [Subsingleton.elim f (initialComparison G)] at i
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝¹ : HasInitial C
inst✝ : HasInitial D
f : ⊥_ D ⟶ G.obj (⊥_ C)
i : IsIso (initialComparison G)
⊢ PreservesColimit (Functor.empty C) G
[PROOFSTEP]
exact PreservesInitial.ofIsoComparison G
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝² : HasInitial C
inst✝¹ : HasInitial D
inst✝ : PreservesColimit (Functor.empty C) G
⊢ IsIso (initialComparison G)
[PROOFSTEP]
rw [← PreservesInitial.iso_hom]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X : C
inst✝² : HasInitial C
inst✝¹ : HasInitial D
inst✝ : PreservesColimit (Functor.empty C) G
⊢ IsIso (PreservesInitial.iso G).inv
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
⊢ IsColimit ((prod.functor.obj F).mapCocone c)
[PROOFSTEP]
apply evaluationJointlyReflectsColimits _ fun {k} => ?_
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
⊢ IsColimit (((evaluation C D).obj k).mapCocone ((prod.functor.obj F).mapCocone c))
[PROOFSTEP]
change IsColimit ((prod.functor.obj F ⋙ (evaluation _ _).obj k).mapCocone c)
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
⊢ IsColimit ((prod.functor.obj F ⋙ (evaluation C D).obj k).mapCocone c)
[PROOFSTEP]
let this := isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
⊢ IsColimit ((prod.functor.obj F ⋙ (evaluation C D).obj k).mapCocone c)
[PROOFSTEP]
apply IsColimit.mapCoconeEquiv _ this
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
⊢ (evaluation C D).obj k ⋙ prod.functor.obj (F.obj k) ≅ prod.functor.obj F ⋙ (evaluation C D).obj k
[PROOFSTEP]
apply (NatIso.ofComponents _ _).symm
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
⊢ (X : C ⥤ D) →
    (prod.functor.obj F ⋙ (evaluation C D).obj k).obj X ≅ ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).obj X
[PROOFSTEP]
intro G
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
G : C ⥤ D
⊢ (prod.functor.obj F ⋙ (evaluation C D).obj k).obj G ≅ ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).obj G
[PROOFSTEP]
apply asIso (prodComparison ((evaluation C D).obj k) F G)
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
⊢ ∀ {X Y : C ⥤ D} (f : X ⟶ Y),
    (prod.functor.obj F ⋙ (evaluation C D).obj k).map f ≫ (asIso (prodComparison ((evaluation C D).obj k) F Y)).hom =
      (asIso (prodComparison ((evaluation C D).obj k) F X)).hom ≫
        ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).map f
[PROOFSTEP]
intro G G'
[GOAL]
C : Type u
inst✝⁶ : Category.{v₁, u} C
D : Type u₂
inst✝⁵ : Category.{u, u₂} D
E : Type u
inst✝⁴ : Category.{v₂, u} E
inst✝³ : HasBinaryProducts D
inst✝² : HasColimits D
inst✝¹ : (X : D) → PreservesColimits (prod.functor.obj X)
F : C ⥤ D
J : Type u
inst✝ : Category.{u, u} J
K : J ⥤ C ⥤ D
c : Cocone K
t : IsColimit c
k : C
this : IsColimit (((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).mapCocone c) :=
  isColimitOfPreserves ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)) t
G G' : C ⥤ D
⊢ ∀ (f : G ⟶ G'),
    (prod.functor.obj F ⋙ (evaluation C D).obj k).map f ≫ (asIso (prodComparison ((evaluation C D).obj k) F G')).hom =
      (asIso (prodComparison ((evaluation C D).obj k) F G)).hom ≫
        ((evaluation C D).obj k ⋙ prod.functor.obj (F.obj k)).map f
[PROOFSTEP]
apply prodComparison_natural ((evaluation C D).obj k) (𝟙 F)
[GOAL]
C : Type u
inst✝³ : Category.{v₁, u} C
D : Type u₂
inst✝² : Category.{u, u₂} D
E : Type u
inst✝¹ : Category.{v₂, u} E
inst✝ : HasLimits D
F : C ⥤ E
J : Type u
hJ : Category.{u, u} J
K : J ⥤ E ⥤ D
c : Cone K
hc : IsLimit c
⊢ IsLimit (((whiskeringLeft C E D).obj F).mapCone c)
[PROOFSTEP]
apply evaluationJointlyReflectsLimits
[GOAL]
case t
C : Type u
inst✝³ : Category.{v₁, u} C
D : Type u₂
inst✝² : Category.{u, u₂} D
E : Type u
inst✝¹ : Category.{v₂, u} E
inst✝ : HasLimits D
F : C ⥤ E
J : Type u
hJ : Category.{u, u} J
K : J ⥤ E ⥤ D
c : Cone K
hc : IsLimit c
⊢ (k : C) → IsLimit (((evaluation C D).obj k).mapCone (((whiskeringLeft C E D).obj F).mapCone c))
[PROOFSTEP]
intro Y
[GOAL]
case t
C : Type u
inst✝³ : Category.{v₁, u} C
D : Type u₂
inst✝² : Category.{u, u₂} D
E : Type u
inst✝¹ : Category.{v₂, u} E
inst✝ : HasLimits D
F : C ⥤ E
J : Type u
hJ : Category.{u, u} J
K : J ⥤ E ⥤ D
c : Cone K
hc : IsLimit c
Y : C
⊢ IsLimit (((evaluation C D).obj Y).mapCone (((whiskeringLeft C E D).obj F).mapCone c))
[PROOFSTEP]
change IsLimit (((evaluation E D).obj (F.obj Y)).mapCone c)
[GOAL]
case t
C : Type u
inst✝³ : Category.{v₁, u} C
D : Type u₂
inst✝² : Category.{u, u₂} D
E : Type u
inst✝¹ : Category.{v₂, u} E
inst✝ : HasLimits D
F : C ⥤ E
J : Type u
hJ : Category.{u, u} J
K : J ⥤ E ⥤ D
c : Cone K
hc : IsLimit c
Y : C
⊢ IsLimit (((evaluation E D).obj (F.obj Y)).mapCone c)
[PROOFSTEP]
exact PreservesLimit.preserves hc
[GOAL]
C✝ : Type u
inst✝⁸ : Category.{v₁, u} C✝
D✝ : Type u₂
inst✝⁷ : Category.{u, u₂} D✝
E✝ : Type u
inst✝⁶ : Category.{v₂, u} E✝
C : Type u
inst✝⁵ : Category.{?u.25923, u} C
D : Type u_1
inst✝⁴ : Category.{u, u_1} D
E : Type u_2
inst✝³ : Category.{u, u_2} E
J : Type u
inst✝² : SmallCategory J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cone K
hc : IsLimit c
⊢ IsLimit (((whiskeringRight C D E).obj F).mapCone c)
[PROOFSTEP]
apply evaluationJointlyReflectsLimits _ (fun k => ?_)
[GOAL]
C✝ : Type u
inst✝⁸ : Category.{v₁, u} C✝
D✝ : Type u₂
inst✝⁷ : Category.{u, u₂} D✝
E✝ : Type u
inst✝⁶ : Category.{v₂, u} E✝
C : Type u
inst✝⁵ : Category.{?u.25923, u} C
D : Type u_1
inst✝⁴ : Category.{u, u_1} D
E : Type u_2
inst✝³ : Category.{u, u_2} E
J : Type u
inst✝² : SmallCategory J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cone K
hc : IsLimit c
k : C
⊢ IsLimit (((evaluation C E).obj k).mapCone (((whiskeringRight C D E).obj F).mapCone c))
[PROOFSTEP]
change IsLimit (((evaluation _ _).obj k ⋙ F).mapCone c)
[GOAL]
C✝ : Type u
inst✝⁸ : Category.{v₁, u} C✝
D✝ : Type u₂
inst✝⁷ : Category.{u, u₂} D✝
E✝ : Type u
inst✝⁶ : Category.{v₂, u} E✝
C : Type u
inst✝⁵ : Category.{?u.25923, u} C
D : Type u_1
inst✝⁴ : Category.{u, u_1} D
E : Type u_2
inst✝³ : Category.{u, u_2} E
J : Type u
inst✝² : SmallCategory J
inst✝¹ : HasLimitsOfShape J D
F : D ⥤ E
inst✝ : PreservesLimitsOfShape J F
K : J ⥤ C ⥤ D
c : Cone K
hc : IsLimit c
k : C
⊢ IsLimit (((evaluation C D).obj k ⋙ F).mapCone c)
[PROOFSTEP]
exact PreservesLimit.preserves hc
[GOAL]
C✝ : Type u
inst✝⁶ : Category.{v₁, u} C✝
D✝ : Type u₂
inst✝⁵ : Category.{u, u₂} D✝
E : Type u
inst✝⁴ : Category.{v₂, u} E
C D : Type u
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
F : C ⥤ D
J : Type u
inst✝¹ : SmallCategory J
inst✝ : PreservesLimitsOfShape J (lan F.op)
⊢ PreservesLimitsOfShape J F
[PROOFSTEP]
apply @preservesLimitsOfShapeOfReflectsOfPreserves _ _ _ _ _ _ _ _ F yoneda ?_
[GOAL]
C✝ : Type u
inst✝⁶ : Category.{v₁, u} C✝
D✝ : Type u₂
inst✝⁵ : Category.{u, u₂} D✝
E : Type u
inst✝⁴ : Category.{v₂, u} E
C D : Type u
inst✝³ : SmallCategory C
inst✝² : SmallCategory D
F : C ⥤ D
J : Type u
inst✝¹ : SmallCategory J
inst✝ : PreservesLimitsOfShape J (lan F.op)
⊢ PreservesLimitsOfShape J (F ⋙ yoneda)
[PROOFSTEP]
exact preservesLimitsOfShapeOfNatIso (compYonedaIsoYonedaCompLan F).symm


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ (L ⋙ R).map (NatTrans.app (whiskerRight (whiskerLeft L h.counit) R) X) ≫
      NatTrans.app (whiskerRight (whiskerLeft L h.counit) R) X =
    NatTrans.app (whiskerRight (whiskerLeft L h.counit) R) ((L ⋙ R).obj X) ≫
      NatTrans.app (whiskerRight (whiskerLeft L h.counit) R) X
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (R.map (NatTrans.app h.counit (L.obj X)))) ≫ R.map (NatTrans.app h.counit (L.obj X)) =
    R.map (NatTrans.app h.counit (L.obj (R.obj (L.obj X)))) ≫ R.map (NatTrans.app h.counit (L.obj X))
[PROOFSTEP]
rw [← R.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (R.map (NatTrans.app h.counit (L.obj X))) ≫ NatTrans.app h.counit (L.obj X)) =
    R.map (NatTrans.app h.counit (L.obj (R.obj (L.obj X)))) ≫ R.map (NatTrans.app h.counit (L.obj X))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ (L ⋙ R).map (NatTrans.app h.unit X) ≫ NatTrans.app (whiskerRight (whiskerLeft L h.counit) R) X =
    𝟙 ((L ⋙ R).obj ((𝟭 C).obj X))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (NatTrans.app h.unit X)) ≫ R.map (NatTrans.app h.counit (L.obj X)) = 𝟙 (R.obj (L.obj X))
[PROOFSTEP]
rw [← R.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ R.map (L.map (NatTrans.app h.unit X) ≫ NatTrans.app h.counit (L.obj X)) = 𝟙 (R.obj (L.obj X))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ NatTrans.app (whiskerRight (whiskerLeft R h.unit) L) X ≫
      (R ⋙ L).map (NatTrans.app (whiskerRight (whiskerLeft R h.unit) L) X) =
    NatTrans.app (whiskerRight (whiskerLeft R h.unit) L) X ≫
      NatTrans.app (whiskerRight (whiskerLeft R h.unit) L) ((R ⋙ L).obj X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (NatTrans.app h.unit (R.obj X)) ≫ L.map (R.map (L.map (NatTrans.app h.unit (R.obj X)))) =
    L.map (NatTrans.app h.unit (R.obj X)) ≫ L.map (NatTrans.app h.unit (R.obj (L.obj (R.obj X))))
[PROOFSTEP]
rw [← L.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (NatTrans.app h.unit (R.obj X) ≫ R.map (L.map (NatTrans.app h.unit (R.obj X)))) =
    L.map (NatTrans.app h.unit (R.obj X)) ≫ L.map (NatTrans.app h.unit (R.obj (L.obj (R.obj X))))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ NatTrans.app (whiskerRight (whiskerLeft R h.unit) L) X ≫ (R ⋙ L).map (NatTrans.app h.counit X) = 𝟙 ((R ⋙ L).obj X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (NatTrans.app h.unit (R.obj X)) ≫ L.map (R.map (NatTrans.app h.counit X)) = 𝟙 (L.obj (R.obj X))
[PROOFSTEP]
rw [← L.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ L.map (NatTrans.app h.unit (R.obj X) ≫ R.map (NatTrans.app h.counit X)) = 𝟙 (L.obj (R.obj X))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ NatTrans.app (μ (Adjunction.toMonad h)) (R.obj X) ≫ R.map (NatTrans.app h.counit X) =
    (Adjunction.toMonad h).toFunctor.map (R.map (NatTrans.app h.counit X)) ≫ R.map (NatTrans.app h.counit X)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : D
⊢ R.map (NatTrans.app h.counit (L.obj (R.obj X))) ≫ R.map (NatTrans.app h.counit X) =
    R.map (L.map (R.map (NatTrans.app h.counit X))) ≫ R.map (NatTrans.app h.counit X)
[PROOFSTEP]
rw [← R.map_comp, ← Adjunction.counit_naturality, R.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ (Adjunction.toMonad h).toFunctor.map (R.map f) ≫
      ((fun X => Algebra.mk (R.obj X) (R.map (NatTrans.app h.counit X))) Y✝).a =
    ((fun X => Algebra.mk (R.obj X) (R.map (NatTrans.app h.counit X))) X✝).a ≫ R.map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ R.map (L.map (R.map f)) ≫ R.map (NatTrans.app h.counit Y✝) = R.map (NatTrans.app h.counit X✝) ≫ R.map f
[PROOFSTEP]
rw [← R.map_comp, Adjunction.counit_naturality, R.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
T : Monad C
x✝¹ x✝ : Monad.Algebra T
f : (Monad.comparison (Monad.adj T)).obj x✝¹ ⟶ (Monad.comparison (Monad.adj T)).obj x✝
⊢ T.map f.f ≫ x✝.a = x✝¹.a ≫ f.f
[PROOFSTEP]
simpa using f.h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
T : Monad C
X : Monad.Algebra (Adjunction.toMonad (Monad.adj T))
⊢ NatTrans.app (Monad.η T) X.A ≫ X.a = 𝟙 X.A
[PROOFSTEP]
simpa using X.unit
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
T : Monad C
X : Monad.Algebra (Adjunction.toMonad (Monad.adj T))
⊢ NatTrans.app (Monad.μ T) X.A ≫ X.a = T.map X.a ≫ X.a
[PROOFSTEP]
simpa using X.assoc
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ L.map (NatTrans.app h.unit X) ≫ NatTrans.app (δ (Adjunction.toComonad h)) (L.obj X) =
    L.map (NatTrans.app h.unit X) ≫ (Adjunction.toComonad h).toFunctor.map (L.map (NatTrans.app h.unit X))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X : C
⊢ L.map (NatTrans.app h.unit X) ≫ L.map (NatTrans.app h.unit (R.obj (L.obj X))) =
    L.map (NatTrans.app h.unit X) ≫ L.map (R.map (L.map (NatTrans.app h.unit X)))
[PROOFSTEP]
rw [← L.map_comp, ← Adjunction.unit_naturality, L.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ((fun X => Coalgebra.mk (L.obj X) (L.map (NatTrans.app h.unit X))) X✝).a ≫
      (Adjunction.toComonad h).toFunctor.map (L.map f) =
    L.map f ≫ ((fun X => Coalgebra.mk (L.obj X) (L.map (NatTrans.app h.unit X))) Y✝).a
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ L.map (NatTrans.app h.unit X✝) ≫ L.map (R.map (L.map f)) = L.map f ≫ L.map (NatTrans.app h.unit Y✝)
[PROOFSTEP]
rw [← L.map_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ L.map (NatTrans.app h.unit X✝ ≫ R.map (L.map f)) = L.map f ≫ L.map (NatTrans.app h.unit Y✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
G : Comonad C
X✝ Y✝ : Comonad.Coalgebra G
f : (Comonad.comparison (Comonad.adj G)).obj X✝ ⟶ (Comonad.comparison (Comonad.adj G)).obj Y✝
⊢ X✝.a ≫ G.map f.f = f.f ≫ Y✝.a
[PROOFSTEP]
simpa using f.h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
G : Comonad C
X : Comonad.Coalgebra (Adjunction.toComonad (Comonad.adj G))
⊢ X.a ≫ NatTrans.app (Comonad.ε G) X.A = 𝟙 X.A
[PROOFSTEP]
simpa using X.counit
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
G : Comonad C
X : Comonad.Coalgebra (Adjunction.toComonad (Comonad.adj G))
⊢ X.a ≫ NatTrans.app (Comonad.δ G) X.A = X.a ≫ G.map X.a
[PROOFSTEP]
simpa using X.coassoc
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
⊢ IsIso (Monad.μ (Adjunction.toMonad (Adjunction.ofRightAdjoint R)))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
⊢ IsIso (whiskerRight (whiskerLeft (leftAdjoint R) (Adjunction.ofRightAdjoint R).counit) R)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ X.a ≫ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A = 𝟙 ((leftAdjoint R ⋙ R).obj X.A)
[PROOFSTEP]
dsimp only [Functor.id_obj]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ X.a ≫ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A = 𝟙 ((leftAdjoint R ⋙ R).obj X.A)
[PROOFSTEP]
rw [← (Adjunction.ofRightAdjoint R).unit_naturality]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ NatTrans.app (Adjunction.ofRightAdjoint R).unit ((leftAdjoint R ⋙ R).obj X.A) ≫ R.map ((leftAdjoint R).map X.a) =
    𝟙 ((leftAdjoint R ⋙ R).obj X.A)
[PROOFSTEP]
dsimp only [Functor.comp_obj, Adjunction.toMonad_coe]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ NatTrans.app (Adjunction.ofRightAdjoint R).unit (R.obj ((leftAdjoint R).obj X.A)) ≫ R.map ((leftAdjoint R).map X.a) =
    𝟙 (R.obj ((leftAdjoint R).obj X.A))
[PROOFSTEP]
rw [unit_obj_eq_map_unit, ← Functor.map_comp, ← Functor.map_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ R.map ((leftAdjoint R).map (NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A ≫ X.a)) =
    𝟙 (R.obj ((leftAdjoint R).obj X.A))
[PROOFSTEP]
erw [X.unit]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ R.map ((leftAdjoint R).map (𝟙 X.A)) = 𝟙 (R.obj ((leftAdjoint R).obj X.A))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
⊢ EssSurj (Monad.comparison (Adjunction.ofRightAdjoint R))
[PROOFSTEP]
refine' ⟨fun X => ⟨(leftAdjoint R).obj X.A, ⟨_⟩⟩⟩
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ (Monad.comparison (Adjunction.ofRightAdjoint R)).obj ((leftAdjoint R).obj X.A) ≅ X
[PROOFSTEP]
symm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ X ≅ (Monad.comparison (Adjunction.ofRightAdjoint R)).obj ((leftAdjoint R).obj X.A)
[PROOFSTEP]
refine' Monad.Algebra.isoMk _ _
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ X.A ≅ ((Monad.comparison (Adjunction.ofRightAdjoint R)).obj ((leftAdjoint R).obj X.A)).A
[PROOFSTEP]
exact asIso ((Adjunction.ofRightAdjoint R).unit.app X.A)
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ (Adjunction.toMonad (Adjunction.ofRightAdjoint R)).toFunctor.map
        (asIso (NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A)).hom ≫
      ((Monad.comparison (Adjunction.ofRightAdjoint R)).obj ((leftAdjoint R).obj X.A)).a =
    X.a ≫ (asIso (NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A)).hom
[PROOFSTEP]
dsimp only [Functor.comp_map, Monad.comparison_obj_a, asIso_hom, Functor.comp_obj, Monad.comparison_obj_A,
  Adjunction.toMonad_coe]
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ R.map ((leftAdjoint R).map (NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A)) ≫
      R.map (NatTrans.app (Adjunction.ofRightAdjoint R).counit ((leftAdjoint R).obj X.A)) =
    X.a ≫ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A
[PROOFSTEP]
rw [← cancel_epi ((Adjunction.ofRightAdjoint R).unit.app X.A)]
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A ≫
      R.map ((leftAdjoint R).map (NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A)) ≫
        R.map (NatTrans.app (Adjunction.ofRightAdjoint R).counit ((leftAdjoint R).obj X.A)) =
    NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A ≫ X.a ≫ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A
[PROOFSTEP]
dsimp only [Functor.id_obj, Functor.comp_obj]
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A ≫
      R.map ((leftAdjoint R).map (NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A)) ≫
        R.map (NatTrans.app (Adjunction.ofRightAdjoint R).counit ((leftAdjoint R).obj X.A)) =
    NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A ≫ X.a ≫ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A
[PROOFSTEP]
rw [Adjunction.unit_naturality_assoc, Adjunction.right_triangle_components, comp_id]
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
inst✝ : Reflective R
X : Monad.Algebra (Adjunction.toMonad (Adjunction.ofRightAdjoint R))
⊢ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A =
    NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A ≫ X.a ≫ NatTrans.app (Adjunction.ofRightAdjoint R).unit X.A
[PROOFSTEP]
apply (X.unit_assoc _).symm


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
⊢ ∀ (j : Discrete WalkingPair),
    NatTrans.app ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).π j =
      (Iso.refl ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).pt).hom ≫
        NatTrans.app (BinaryFan.mk (G.map f) (G.map g)).π j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case mk.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
⊢ NatTrans.app ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).π
      { as := WalkingPair.left } =
    (Iso.refl ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).pt).hom ≫
      NatTrans.app (BinaryFan.mk (G.map f) (G.map g)).π { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
⊢ NatTrans.app ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).π
      { as := WalkingPair.right } =
    (Iso.refl ((Cones.postcompose (diagramIsoPair (pair X Y ⋙ G)).hom).obj (G.mapCone (BinaryFan.mk f g))).pt).hom ≫
      NatTrans.app (BinaryFan.mk (G.map f) (G.map g)).π { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ PreservesLimit (pair X Y) G
[PROOFSTEP]
apply preservesLimitOfPreservesLimitCone (prodIsProd X Y)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ IsLimit (G.mapCone (BinaryFan.mk prod.fst prod.snd))
[PROOFSTEP]
apply (isLimitMapConeBinaryFanEquiv _ _ _).symm _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ IsLimit (BinaryFan.mk (G.map prod.fst) (G.map prod.snd))
[PROOFSTEP]
refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (pair (G.obj X) (G.obj Y))) ?_
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝¹ : HasBinaryProduct X Y
inst✝ : HasBinaryProduct (G.obj X) (G.obj Y)
i : IsIso (prodComparison G X Y)
⊢ IsIso (IsLimit.lift (limit.isLimit (pair (G.obj X) (G.obj Y))) (BinaryFan.mk (G.map prod.fst) (G.map prod.snd)))
[PROOFSTEP]
apply i
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ IsIso (prodComparison G X Y)
[PROOFSTEP]
rw [← PreservesLimitPair.iso_hom]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : P ⟶ X
g : P ⟶ Y
inst✝² : HasBinaryProduct X Y
inst✝¹ : HasBinaryProduct (G.obj X) (G.obj Y)
inst✝ : PreservesLimit (pair X Y) G
⊢ IsIso (PreservesLimitPair.iso G X Y).hom
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
⊢ ∀ (j : Discrete WalkingPair),
    NatTrans.app
          ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).ι j ≫
        (Iso.refl
            ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj
                (G.mapCocone (BinaryCofan.mk f g))).pt).hom =
      NatTrans.app (BinaryCofan.mk (G.map f) (G.map g)).ι j
[PROOFSTEP]
rintro (_ | _)
[GOAL]
case mk.left
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
⊢ NatTrans.app ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).ι
        { as := WalkingPair.left } ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj
              (G.mapCocone (BinaryCofan.mk f g))).pt).hom =
    NatTrans.app (BinaryCofan.mk (G.map f) (G.map g)).ι { as := WalkingPair.left }
[PROOFSTEP]
simp
[GOAL]
case mk.right
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
⊢ NatTrans.app ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj (G.mapCocone (BinaryCofan.mk f g))).ι
        { as := WalkingPair.right } ≫
      (Iso.refl
          ((Cocones.precompose (diagramIsoPair (pair X Y ⋙ G)).symm.hom).obj
              (G.mapCocone (BinaryCofan.mk f g))).pt).hom =
    NatTrans.app (BinaryCofan.mk (G.map f) (G.map g)).ι { as := WalkingPair.right }
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ PreservesColimit (pair X Y) G
[PROOFSTEP]
apply preservesColimitOfPreservesColimitCocone (coprodIsCoprod X Y)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsColimit (G.mapCocone (BinaryCofan.mk coprod.inl coprod.inr))
[PROOFSTEP]
apply (isColimitMapCoconeBinaryCofanEquiv _ _ _).symm _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsColimit (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr))
[PROOFSTEP]
refine @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (pair (G.obj X) (G.obj Y))) ?_
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝¹ : HasBinaryCoproduct X Y
inst✝ : HasBinaryCoproduct (G.obj X) (G.obj Y)
i : IsIso (coprodComparison G X Y)
⊢ IsIso
    (IsColimit.desc (colimit.isColimit (pair (G.obj X) (G.obj Y)))
      (BinaryCofan.mk (G.map coprod.inl) (G.map coprod.inr)))
[PROOFSTEP]
apply i
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝² : HasBinaryCoproduct X Y
inst✝¹ : HasBinaryCoproduct (G.obj X) (G.obj Y)
inst✝ : PreservesColimit (pair X Y) G
⊢ IsIso (coprodComparison G X Y)
[PROOFSTEP]
rw [← PreservesColimitPair.iso_hom]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
P X Y Z : C
f : X ⟶ P
g : Y ⟶ P
inst✝² : HasBinaryCoproduct X Y
inst✝¹ : HasBinaryCoproduct (G.obj X) (G.obj Y)
inst✝ : PreservesColimit (pair X Y) G
⊢ IsIso (PreservesColimitPair.iso G X Y).hom
[PROOFSTEP]
infer_instance


[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝¹ : Category.{w', w} J
F : J ⥤ C
inst✝ : PreservesLimit F G
c₁ c₂ : Cone F
t : IsLimit c₁
⊢ ∀ (j : J), G.map (IsLimit.lift t c₂) ≫ NatTrans.app (G.mapCone c₁).π j = NatTrans.app (G.mapCone c₂).π j
[PROOFSTEP]
simp [← G.map_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : PreservesLimit F G
inst✝¹ : HasLimit F
inst✝ : HasLimit (F ⋙ G)
t : Cone F
⊢ G.map (limit.lift F t) ≫ (preservesLimitIso G F).hom = limit.lift (F ⋙ G) (G.mapCone t)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : PreservesLimit F G
inst✝¹ : HasLimit F
inst✝ : HasLimit (F ⋙ G)
t : Cone F
j✝ : J
⊢ (G.map (limit.lift F t) ≫ (preservesLimitIso G F).hom) ≫ limit.π (F ⋙ G) j✝ =
    limit.lift (F ⋙ G) (G.mapCone t) ≫ limit.π (F ⋙ G) j✝
[PROOFSTEP]
simp [← G.map_comp]
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesLimit F G
inst✝⁴ : HasLimit F
inst✝³ : HasLimit (F ⋙ G)
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
⊢ ∀ {X Y : J ⥤ C} (f : X ⟶ Y),
    (lim ⋙ G).map f ≫ ((fun F => preservesLimitIso G F) Y).hom =
      ((fun F => preservesLimitIso G F) X).hom ≫ ((whiskeringRight J C D).obj G ⋙ lim).map f
[PROOFSTEP]
intro _ _ f
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesLimit F G
inst✝⁴ : HasLimit F
inst✝³ : HasLimit (F ⋙ G)
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ (lim ⋙ G).map f ≫ ((fun F => preservesLimitIso G F) Y✝).hom =
    ((fun F => preservesLimitIso G F) X✝).hom ≫ ((whiskeringRight J C D).obj G ⋙ lim).map f
[PROOFSTEP]
apply limit.hom_ext
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesLimit F G
inst✝⁴ : HasLimit F
inst✝³ : HasLimit (F ⋙ G)
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ ∀ (j : J),
    ((lim ⋙ G).map f ≫ ((fun F => preservesLimitIso G F) Y✝).hom) ≫ limit.π (((whiskeringRight J C D).obj G).obj Y✝) j =
      (((fun F => preservesLimitIso G F) X✝).hom ≫ ((whiskeringRight J C D).obj G ⋙ lim).map f) ≫
        limit.π (((whiskeringRight J C D).obj G).obj Y✝) j
[PROOFSTEP]
intro j
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesLimit F G
inst✝⁴ : HasLimit F
inst✝³ : HasLimit (F ⋙ G)
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ ((lim ⋙ G).map f ≫ ((fun F => preservesLimitIso G F) Y✝).hom) ≫ limit.π (((whiskeringRight J C D).obj G).obj Y✝) j =
    (((fun F => preservesLimitIso G F) X✝).hom ≫ ((whiskeringRight J C D).obj G ⋙ lim).map f) ≫
      limit.π (((whiskeringRight J C D).obj G).obj Y✝) j
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesLimit F G
inst✝⁴ : HasLimit F
inst✝³ : HasLimit (F ⋙ G)
inst✝² : PreservesLimitsOfShape J G
inst✝¹ : HasLimitsOfShape J D
inst✝ : HasLimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ (G.map (limMap f) ≫ (preservesLimitIso G Y✝).hom) ≫ limit.π (Y✝ ⋙ G) j =
    ((preservesLimitIso G X✝).hom ≫ limMap (whiskerRight f G)) ≫ limit.π (Y✝ ⋙ G) j
[PROOFSTEP]
simp only [preservesLimitsIso_hom_π, whiskerRight_app, limMap_π, Category.assoc, preservesLimitsIso_hom_π_assoc, ←
  G.map_comp]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝¹ : Category.{w', w} J
F : J ⥤ C
inst✝ : PreservesColimit F G
c₁ c₂ : Cocone F
t : IsColimit c₁
⊢ ∀ (j : J), NatTrans.app (G.mapCocone c₁).ι j ≫ G.map (IsColimit.desc t c₂) = NatTrans.app (G.mapCocone c₂).ι j
[PROOFSTEP]
simp [← G.map_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : PreservesColimit F G
inst✝¹ : HasColimit F
inst✝ : HasColimit (F ⋙ G)
t : Cocone F
⊢ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) = colimit.desc (F ⋙ G) (G.mapCocone t)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝³ : Category.{w', w} J
F : J ⥤ C
inst✝² : PreservesColimit F G
inst✝¹ : HasColimit F
inst✝ : HasColimit (F ⋙ G)
t : Cocone F
j✝ : J
⊢ colimit.ι (F ⋙ G) j✝ ≫ (preservesColimitIso G F).inv ≫ G.map (colimit.desc F t) =
    colimit.ι (F ⋙ G) j✝ ≫ colimit.desc (F ⋙ G) (G.mapCocone t)
[PROOFSTEP]
simp [← G.map_comp]
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
⊢ ∀ {X Y : J ⥤ C} (f : X ⟶ Y),
    (colim ⋙ G).map f ≫ ((fun F => preservesColimitIso G F) Y).hom =
      ((fun F => preservesColimitIso G F) X).hom ≫ ((whiskeringRight J C D).obj G ⋙ colim).map f
[PROOFSTEP]
intro _ _ f
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ (colim ⋙ G).map f ≫ ((fun F => preservesColimitIso G F) Y✝).hom =
    ((fun F => preservesColimitIso G F) X✝).hom ≫ ((whiskeringRight J C D).obj G ⋙ colim).map f
[PROOFSTEP]
rw [← Iso.inv_comp_eq, ← Category.assoc, ← Iso.eq_comp_inv]
[GOAL]
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ ((fun F => preservesColimitIso G F) X✝).inv ≫ (colim ⋙ G).map f =
    ((whiskeringRight J C D).obj G ⋙ colim).map f ≫ ((fun F => preservesColimitIso G F) Y✝).inv
[PROOFSTEP]
apply colimit.hom_ext
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
⊢ ∀ (j : J),
    colimit.ι (((whiskeringRight J C D).obj G).obj X✝) j ≫
        ((fun F => preservesColimitIso G F) X✝).inv ≫ (colim ⋙ G).map f =
      colimit.ι (((whiskeringRight J C D).obj G).obj X✝) j ≫
        ((whiskeringRight J C D).obj G ⋙ colim).map f ≫ ((fun F => preservesColimitIso G F) Y✝).inv
[PROOFSTEP]
intro j
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ colimit.ι (((whiskeringRight J C D).obj G).obj X✝) j ≫
      ((fun F => preservesColimitIso G F) X✝).inv ≫ (colim ⋙ G).map f =
    colimit.ι (((whiskeringRight J C D).obj G).obj X✝) j ≫
      ((whiskeringRight J C D).obj G ⋙ colim).map f ≫ ((fun F => preservesColimitIso G F) Y✝).inv
[PROOFSTEP]
dsimp
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ colimit.ι (X✝ ⋙ G) j ≫ (preservesColimitIso G X✝).inv ≫ G.map (colimMap f) =
    colimit.ι (X✝ ⋙ G) j ≫ colimMap (whiskerRight f G) ≫ (preservesColimitIso G Y✝).inv
[PROOFSTEP]
erw [ι_colimMap_assoc]
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ colimit.ι (X✝ ⋙ G) j ≫ (preservesColimitIso G X✝).inv ≫ G.map (colimMap f) =
    NatTrans.app (whiskerRight f G) j ≫ colimit.ι (Y✝ ⋙ G) j ≫ (preservesColimitIso G Y✝).inv
[PROOFSTEP]
simp only [ι_preservesColimitsIso_inv, whiskerRight_app, Category.assoc, ι_preservesColimitsIso_inv_assoc, ← G.map_comp]
[GOAL]
case w
C : Type u₁
inst✝⁸ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁷ : Category.{v₂, u₂} D
G : C ⥤ D
J : Type w
inst✝⁶ : Category.{w', w} J
F : J ⥤ C
inst✝⁵ : PreservesColimit F G
inst✝⁴ : HasColimit F
inst✝³ : HasColimit (F ⋙ G)
inst✝² : PreservesColimitsOfShape J G
inst✝¹ : HasColimitsOfShape J D
inst✝ : HasColimitsOfShape J C
X✝ Y✝ : J ⥤ C
f : X✝ ⟶ Y✝
j : J
⊢ G.map (colimit.ι X✝ j ≫ colimMap f) = G.map (NatTrans.app f j ≫ colimit.ι Y✝ j)
[PROOFSTEP]
erw [ι_colimMap]


[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y : C
f : X ⟶ Y
⊢ f = 0 → F.map f = 0
[PROOFSTEP]
rintro rfl
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroMorphisms D
F : C ⥤ D
inst✝¹ : PreservesZeroMorphisms F
inst✝ : Faithful F
X Y : C
⊢ F.map 0 = 0
[PROOFSTEP]
exact F.map_zero _ _
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsLeftAdjoint F
X Y : C
⊢ F.map 0 = 0
[PROOFSTEP]
let adj := Adjunction.ofLeftAdjoint F
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsLeftAdjoint F
X Y : C
adj : F ⊣ rightAdjoint F := Adjunction.ofLeftAdjoint F
⊢ F.map 0 = 0
[PROOFSTEP]
calc
  F.map (0 : X ⟶ Y) = F.map 0 ≫ F.map (adj.unit.app Y) ≫ adj.counit.app (F.obj Y) := ?_
  _ = F.map 0 ≫ F.map ((rightAdjoint F).map (0 : F.obj X ⟶ _)) ≫ adj.counit.app (F.obj Y) := ?_
  _ = 0 := ?_
[GOAL]
case calc_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsLeftAdjoint F
X Y : C
adj : F ⊣ rightAdjoint F := Adjunction.ofLeftAdjoint F
⊢ F.map 0 = F.map 0 ≫ F.map (NatTrans.app adj.unit Y) ≫ NatTrans.app adj.counit (F.obj Y)
[PROOFSTEP]
rw [Adjunction.left_triangle_components]
[GOAL]
case calc_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsLeftAdjoint F
X Y : C
adj : F ⊣ rightAdjoint F := Adjunction.ofLeftAdjoint F
⊢ F.map 0 = F.map 0 ≫ 𝟙 (F.obj Y)
[PROOFSTEP]
exact (Category.comp_id _).symm
[GOAL]
case calc_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsLeftAdjoint F
X Y : C
adj : F ⊣ rightAdjoint F := Adjunction.ofLeftAdjoint F
⊢ F.map 0 ≫ F.map (NatTrans.app adj.unit Y) ≫ NatTrans.app adj.counit (F.obj Y) =
    F.map 0 ≫ F.map ((rightAdjoint F).map 0) ≫ NatTrans.app adj.counit (F.obj Y)
[PROOFSTEP]
simp only [← Category.assoc, ← F.map_comp, zero_comp]
[GOAL]
case calc_3
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : IsLeftAdjoint F
X Y : C
adj : F ⊣ rightAdjoint F := Adjunction.ofLeftAdjoint F
⊢ F.map 0 ≫ F.map ((rightAdjoint F).map 0) ≫ NatTrans.app adj.counit (F.obj Y) = 0
[PROOFSTEP]
simp only [Adjunction.counit_naturality, comp_zero]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : IsRightAdjoint G
X Y : C
⊢ G.map 0 = 0
[PROOFSTEP]
let adj := Adjunction.ofRightAdjoint G
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : IsRightAdjoint G
X Y : C
adj : leftAdjoint G ⊣ G := Adjunction.ofRightAdjoint G
⊢ G.map 0 = 0
[PROOFSTEP]
calc
  G.map (0 : X ⟶ Y) = adj.unit.app (G.obj X) ≫ G.map (adj.counit.app X) ≫ G.map 0 := ?_
  _ = adj.unit.app (G.obj X) ≫ G.map ((leftAdjoint G).map (0 : _ ⟶ G.obj X)) ≫ G.map 0 := ?_
  _ = 0 := ?_
[GOAL]
case calc_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : IsRightAdjoint G
X Y : C
adj : leftAdjoint G ⊣ G := Adjunction.ofRightAdjoint G
⊢ G.map 0 = NatTrans.app adj.unit (G.obj X) ≫ G.map (NatTrans.app adj.counit X) ≫ G.map 0
[PROOFSTEP]
rw [Adjunction.right_triangle_components_assoc]
[GOAL]
case calc_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : IsRightAdjoint G
X Y : C
adj : leftAdjoint G ⊣ G := Adjunction.ofRightAdjoint G
⊢ NatTrans.app adj.unit (G.obj X) ≫ G.map (NatTrans.app adj.counit X) ≫ G.map 0 =
    NatTrans.app adj.unit (G.obj X) ≫ G.map ((leftAdjoint G).map 0) ≫ G.map 0
[PROOFSTEP]
simp only [← G.map_comp, comp_zero]
[GOAL]
case calc_3
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
G : C ⥤ D
inst✝ : IsRightAdjoint G
X Y : C
adj : leftAdjoint G ⊣ G := Adjunction.ofRightAdjoint G
⊢ NatTrans.app adj.unit (G.obj X) ≫ G.map ((leftAdjoint G).map 0) ≫ G.map 0 = 0
[PROOFSTEP]
simp only [id_obj, comp_obj, Adjunction.unit_naturality_assoc, zero_comp]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Full F
X Y : C
⊢ F.map 0 = F.map (0 ≫ F.preimage 0)
[PROOFSTEP]
rw [zero_comp]
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : Full F
X Y : C
⊢ F.map (0 ≫ F.preimage 0) = 0
[PROOFSTEP]
rw [F.map_comp, F.image_preimage, comp_zero]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroObject D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
⊢ 0 ≫ 0 = 𝟙 (F.obj 0)
[PROOFSTEP]
rw [← F.map_id, id_zero, F.map_zero, zero_comp]
[GOAL]
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
inst✝⁴ : HasZeroObject C
inst✝³ : HasZeroObject D
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroMorphisms D
F : C ⥤ D
inst✝ : PreservesZeroMorphisms F
⊢ 0 ≫ 0 = 𝟙 0
[PROOFSTEP]
rw [id_zero, comp_zero]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 = F.map 0 ≫ F.map 0
[PROOFSTEP]
rw [← Functor.map_comp, comp_zero]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 ≫ F.map 0 = F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0
[PROOFSTEP]
rw [Iso.hom_inv_id, Category.id_comp]
[GOAL]
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroObject C
inst✝² : HasZeroObject D
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroMorphisms D
F : C ⥤ D
i : F.obj 0 ≅ 0
X Y : C
⊢ F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0 = 0
[PROOFSTEP]
simp only [zero_of_to_zero i.hom, zero_comp, comp_zero]