[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ Nonempty
    (Octahedron (_ : 𝟙 X ≫ 𝟙 X = 𝟙 X) (_ : contractibleTriangle X ∈ distinguishedTriangles)
      (_ : contractibleTriangle X ∈ distinguishedTriangles) (_ : contractibleTriangle X ∈ distinguishedTriangles))
[PROOFSTEP]
refine'
  ⟨⟨0, 0, _, _, _, _,
      isomorphic_distinguished _ (contractible_distinguished (0 : C)) _
        (Triangle.isoMk _ _ (by rfl) (by rfl) (by rfl))⟩⟩
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (0 ≫ (shiftFunctor C 1).map 0)).obj₁ ≅ (contractibleTriangle 0).obj₁
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (0 ≫ (shiftFunctor C 1).map 0)).obj₂ ≅ (contractibleTriangle 0).obj₂
[PROOFSTEP]
rfl
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ (Triangle.mk 0 0 (0 ≫ (shiftFunctor C 1).map 0)).obj₃ ≅ (contractibleTriangle 0).obj₃
[PROOFSTEP]
rfl
[GOAL]
case refine'_1
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 𝟙 X ≫ 0
case refine'_2
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 0
case refine'_3
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 0
case refine'_4
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ (shiftFunctor C 1).map (𝟙 X) = 0 ≫ 0
[PROOFSTEP]
all_goals apply Subsingleton.elim
[GOAL]
case refine'_1
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 𝟙 X ≫ 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case refine'_2
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case refine'_3
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ 0 = 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
case refine'_4
C : Type u_1
inst✝⁵ : Category.{?u.9027, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X : C
⊢ 0 ≫ (shiftFunctor C 1).map (𝟙 X) = 0 ≫ 0
[PROOFSTEP]
apply Subsingleton.elim
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.25095, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk u₁₂ v₁₂ w₁₂).mor₁ ≫ u₂₃ = 𝟙 X₁ ≫ (Triangle.mk u₁₃ v₁₃ w₁₃).mor₁
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.25095, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ u₁₂ ≫ u₂₃ = 𝟙 X₁ ≫ u₁₃
[PROOFSTEP]
rw [id_comp, comm]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.25095, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk u₁₂ v₁₂ w₁₂).mor₃ ≫ (shiftFunctor C 1).map (𝟙 X₁) = h.m₁ ≫ (Triangle.mk u₁₃ v₁₃ w₁₃).mor₃
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.25095, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ w₁₂ ≫ (shiftFunctor C 1).map (𝟙 X₁) = h.m₁ ≫ w₁₃
[PROOFSTEP]
simpa only [Functor.map_id, comp_id] using h.comm₂.symm
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.30829, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk u₁₃ v₁₃ w₁₃).mor₁ ≫ 𝟙 X₃ = u₁₂ ≫ (Triangle.mk u₂₃ v₂₃ w₂₃).mor₁
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.30829, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ u₁₃ ≫ 𝟙 X₃ = u₁₂ ≫ u₂₃
[PROOFSTEP]
rw [comp_id, comm]
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.30829, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ (Triangle.mk u₁₃ v₁₃ w₁₃).mor₂ ≫ h.m₃ = 𝟙 X₃ ≫ (Triangle.mk u₂₃ v₂₃ w₂₃).mor₂
[PROOFSTEP]
dsimp
[GOAL]
C : Type u_1
inst✝⁵ : Category.{?u.30829, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), Functor.Additive (shiftFunctor C n)
inst✝ : Pretriangulated C
X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C
u₁₂ : X₁ ⟶ X₂
u₂₃ : X₂ ⟶ X₃
u₁₃ : X₁ ⟶ X₃
comm : u₁₂ ≫ u₂₃ = u₁₃
v₁₂ : X₂ ⟶ Z₁₂
w₁₂ : Z₁₂ ⟶ (shiftFunctor C 1).obj X₁
h₁₂ : Triangle.mk u₁₂ v₁₂ w₁₂ ∈ distinguishedTriangles
v₂₃ : X₃ ⟶ Z₂₃
w₂₃ : Z₂₃ ⟶ (shiftFunctor C 1).obj X₂
h₂₃ : Triangle.mk u₂₃ v₂₃ w₂₃ ∈ distinguishedTriangles
v₁₃ : X₃ ⟶ Z₁₃
w₁₃ : Z₁₃ ⟶ (shiftFunctor C 1).obj X₁
h₁₃ : Triangle.mk u₁₃ v₁₃ w₁₃ ∈ distinguishedTriangles
h : Octahedron comm h₁₂ h₂₃ h₁₃
⊢ v₁₃ ≫ h.m₃ = 𝟙 X₃ ≫ v₂₃
[PROOFSTEP]
rw [id_comp, h.comm₃]


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A B : Triangle C
iso₁ : A.obj₁ ≅ B.obj₁
iso₂ : A.obj₂ ≅ B.obj₂
iso₃ : A.obj₃ ≅ B.obj₃
comm₁ : autoParam (A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁) _auto✝
comm₂ : autoParam (A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂) _auto✝
comm₃ : autoParam (A.mor₃ ≫ (shiftFunctor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃) _auto✝
⊢ B.mor₁ ≫ iso₂.inv = iso₁.inv ≫ A.mor₁
[PROOFSTEP]
simp only [← cancel_mono iso₂.hom, assoc, Iso.inv_hom_id, comp_id, comm₁, Iso.inv_hom_id_assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A B : Triangle C
iso₁ : A.obj₁ ≅ B.obj₁
iso₂ : A.obj₂ ≅ B.obj₂
iso₃ : A.obj₃ ≅ B.obj₃
comm₁ : autoParam (A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁) _auto✝
comm₂ : autoParam (A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂) _auto✝
comm₃ : autoParam (A.mor₃ ≫ (shiftFunctor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃) _auto✝
⊢ B.mor₂ ≫ iso₃.inv = iso₂.inv ≫ A.mor₂
[PROOFSTEP]
simp only [← cancel_mono iso₃.hom, assoc, Iso.inv_hom_id, comp_id, comm₂, Iso.inv_hom_id_assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasShift C ℤ
T₁ T₂ T₃ A B : Triangle C
iso₁ : A.obj₁ ≅ B.obj₁
iso₂ : A.obj₂ ≅ B.obj₂
iso₃ : A.obj₃ ≅ B.obj₃
comm₁ : autoParam (A.mor₁ ≫ iso₂.hom = iso₁.hom ≫ B.mor₁) _auto✝
comm₂ : autoParam (A.mor₂ ≫ iso₃.hom = iso₂.hom ≫ B.mor₂) _auto✝
comm₃ : autoParam (A.mor₃ ≫ (shiftFunctor C 1).map iso₁.hom = iso₃.hom ≫ B.mor₃) _auto✝
⊢ B.mor₃ ≫ (shiftFunctor C 1).map iso₁.inv = iso₃.inv ≫ A.mor₃
[PROOFSTEP]
simp only [← cancel_mono (iso₁.hom⟦(1 : ℤ)⟧'), Category.assoc, comm₃, Iso.inv_hom_id_assoc, ← Functor.map_comp,
  Iso.inv_hom_id, Functor.map_id, Category.comp_id]


[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
x y : Elements F
h₁ : x.fst = y.fst
h₂ : F.map (eqToHom h₁) x.snd = y.snd
⊢ x = y
[PROOFSTEP]
cases x
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
y : Elements F
fst✝ : C
snd✝ : F.obj fst✝
h₁ : { fst := fst✝, snd := snd✝ }.fst = y.fst
h₂ : F.map (eqToHom h₁) { fst := fst✝, snd := snd✝ }.snd = y.snd
⊢ { fst := fst✝, snd := snd✝ } = y
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝¹ : C
snd✝¹ : F.obj fst✝¹
fst✝ : C
snd✝ : F.obj fst✝
h₁ : { fst := fst✝¹, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝ }.fst
h₂ : F.map (eqToHom h₁) { fst := fst✝¹, snd := snd✝¹ }.snd = { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝¹, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
cases h₁
[GOAL]
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝ : C
snd✝¹ snd✝ : F.obj fst✝
h₂ :
  F.map (eqToHom (_ : { fst := fst✝, snd := snd✝¹ }.fst = { fst := fst✝, snd := snd✝¹ }.fst))
      { fst := fst✝, snd := snd✝¹ }.snd =
    { fst := fst✝, snd := snd✝ }.snd
⊢ { fst := fst✝, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
simp only [eqToHom_refl, FunctorToTypes.map_id_apply] at h₂
[GOAL]
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
fst✝ : C
snd✝¹ snd✝ : F.obj fst✝
h₂ : snd✝¹ = snd✝
⊢ { fst := fst✝, snd := snd✝¹ } = { fst := fst✝, snd := snd✝ }
[PROOFSTEP]
simp [h₂]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
p : Functor.Elements F
⊢ F.map (𝟙 p.fst) p.snd = p.snd
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y Z : Functor.Elements F
f : X ⟶ Y
g : Y ⟶ Z
⊢ F.map (↑f ≫ ↑g) X.snd = Z.snd
[PROOFSTEP]
simp [f.2, g.2]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
p q : Functor.Elements F
f : p ⟶ q
⊢ F.map (inv ↑f) q.snd = F.map (inv ↑f) (F.map (↑f) p.snd)
[PROOFSTEP]
rw [f.2]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
p q : Functor.Elements F
f : p ⟶ q
⊢ (F.map ↑f ≫ F.map (inv ↑f)) p.snd = p.snd
[PROOFSTEP]
rw [← F.map_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
p q : Functor.Elements F
f : p ⟶ q
⊢ F.map (↑f ≫ inv ↑f) p.snd = p.snd
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : Functor.Elements F
x✝ : X✝ ⟶ Y✝
⊢ (fun {p q} f => { val := inv ↑f, property := (_ : F.map (inv ↑f) q.snd = p.snd) }) x✝ ≫ x✝ = 𝟙 Y✝
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : Functor.Elements F
x✝ : X✝ ⟶ Y✝
⊢ ↑((fun {p q} f => { val := inv ↑f, property := (_ : F.map (inv ↑f) q.snd = p.snd) }) x✝ ≫ x✝) = ↑(𝟙 Y✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : Functor.Elements F
x✝ : X✝ ⟶ Y✝
⊢ x✝ ≫ (fun {p q} f => { val := inv ↑f, property := (_ : F.map (inv ↑f) q.snd = p.snd) }) x✝ = 𝟙 X✝
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝¹ : Category.{v, u} C
G : Type u
inst✝ : Groupoid G
F : G ⥤ Type w
X✝ Y✝ : Functor.Elements F
x✝ : X✝ ⟶ Y✝
⊢ ↑(x✝ ≫ (fun {p q} f => { val := inv ↑f, property := (_ : F.map (inv ↑f) q.snd = p.snd) }) x✝) = ↑(𝟙 X✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F F₁ F₂ : C ⥤ Type w
α : F₁ ⟶ F₂
t₁ t₂ : Functor.Elements F₁
k : t₁ ⟶ t₂
⊢ F₂.map (↑k) ((fun t => { fst := t.fst, snd := NatTrans.app α t.fst t.snd }) t₁).snd =
    ((fun t => { fst := t.fst, snd := NatTrans.app α t.fst t.snd }) t₂).snd
[PROOFSTEP]
simpa [← k.2] using (FunctorToTypes.naturality _ _ α k.1 t₁.2).symm
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : Functor.Elements F
f : X ⟶ Y
⊢ ((fun X => StructuredArrow.mk fun x => X.snd) X).hom ≫ F.map ↑f = ((fun X => StructuredArrow.mk fun x => X.snd) Y).hom
[PROOFSTEP]
funext
[GOAL]
case h
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y : Functor.Elements F
f : X ⟶ Y
x✝ : (Functor.fromPUnit PUnit).obj ((fun X => StructuredArrow.mk fun x => X.snd) X).left
⊢ (((fun X => StructuredArrow.mk fun x => X.snd) X).hom ≫ F.map ↑f) x✝ =
    Comma.hom ((fun X => StructuredArrow.mk fun x => X.snd) Y) x✝
[PROOFSTEP]
simp [f.2]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X : Functor.Elements F
⊢ (𝟭 (Functor.Elements F)).obj X = (toStructuredArrow F ⋙ fromStructuredArrow F).obj X
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X✝ Y✝ : (Functor.Elements F)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ (fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) X✝ ⟶
    (fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) Y✝
[PROOFSTEP]
fapply CostructuredArrow.homMk
[GOAL]
case g
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X✝ Y✝ : (Functor.Elements F)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) X✝).left ⟶
    ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) Y✝).left
[PROOFSTEP]
exact f.unop.val.unop
[GOAL]
case w
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X✝ Y✝ : (Functor.Elements F)ᵒᵖ
f : X✝ ⟶ Y✝
⊢ autoParam
    (yoneda.map (↑f.unop).unop ≫
        ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) Y✝).hom =
      ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) X✝).hom)
    _auto✝
[PROOFSTEP]
ext Z y
[GOAL]
case w.w.h.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X✝ Y✝ : (Functor.Elements F)ᵒᵖ
f : X✝ ⟶ Y✝
Z : Cᵒᵖ
y :
  (yoneda.obj
        ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) X✝).left).obj
    Z
⊢ NatTrans.app
      (yoneda.map (↑f.unop).unop ≫
        ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) Y✝).hom)
      Z y =
    NatTrans.app
      ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) X✝).hom Z y
[PROOFSTEP]
dsimp
[GOAL]
case w.w.h.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X✝ Y✝ : (Functor.Elements F)ᵒᵖ
f : X✝ ⟶ Y✝
Z : Cᵒᵖ
y :
  (yoneda.obj
        ((fun X => CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F).inv { down := X.unop.snd })) X✝).left).obj
    Z
⊢ F.map (↑f.unop ≫ y.op) Y✝.unop.snd = F.map y.op X✝.unop.snd
[PROOFSTEP]
simp only [FunctorToTypes.map_comp_apply, ← f.unop.2]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
⊢ F.map f.unop.left.op ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) X).snd =
    ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).snd
[PROOFSTEP]
convert (congr_fun ((unop X).hom.naturality f.unop.left.op) (𝟙 _)).symm
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
e_1✝ :
  F.obj ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).fst =
    ((Functor.fromPUnit F).obj X.unop.right).obj (op Y.unop.left)
⊢ ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).snd =
    ((yoneda.obj X.unop.left).map f.unop.left.op ≫ NatTrans.app X.unop.hom (op Y.unop.left)) (𝟙 (op X.unop.left).unop)
[PROOFSTEP]
simp only [Equiv.toFun_as_coe, Quiver.Hom.unop_op, yonedaEquiv_apply, types_comp_apply, Category.comp_id,
  yoneda_obj_map]
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
e_1✝ :
  F.obj ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).fst =
    ((Functor.fromPUnit F).obj X.unop.right).obj (op Y.unop.left)
⊢ NatTrans.app Y.unop.hom (op Y.unop.left) (𝟙 Y.unop.left) = NatTrans.app X.unop.hom (op Y.unop.left) f.unop.left
[PROOFSTEP]
have : yoneda.map f.unop.left ≫ (unop X).hom = (unop Y).hom := by convert f.unop.3
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
e_1✝ :
  F.obj ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).fst =
    ((Functor.fromPUnit F).obj X.unop.right).obj (op Y.unop.left)
⊢ yoneda.map f.unop.left ≫ X.unop.hom = Y.unop.hom
[PROOFSTEP]
convert f.unop.3
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
e_1✝ :
  F.obj ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).fst =
    ((Functor.fromPUnit F).obj X.unop.right).obj (op Y.unop.left)
this : yoneda.map f.unop.left ≫ X.unop.hom = Y.unop.hom
⊢ NatTrans.app Y.unop.hom (op Y.unop.left) (𝟙 Y.unop.left) = NatTrans.app X.unop.hom (op Y.unop.left) f.unop.left
[PROOFSTEP]
erw [← this]
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
e_1✝ :
  F.obj ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).fst =
    ((Functor.fromPUnit F).obj X.unop.right).obj (op Y.unop.left)
this : yoneda.map f.unop.left ≫ X.unop.hom = Y.unop.hom
⊢ NatTrans.app (yoneda.map f.unop.left ≫ X.unop.hom) (op Y.unop.left) (𝟙 Y.unop.left) =
    NatTrans.app X.unop.hom (op Y.unop.left) f.unop.left
[PROOFSTEP]
simp only [yoneda_map_app, FunctorToTypes.comp]
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : (CostructuredArrow yoneda F)ᵒᵖ
f : X ⟶ Y
e_1✝ :
  F.obj ((fun X => { fst := op X.unop.left, snd := Equiv.toFun yonedaEquiv X.unop.hom }) Y).fst =
    ((Functor.fromPUnit F).obj X.unop.right).obj (op Y.unop.left)
this : yoneda.map f.unop.left ≫ X.unop.hom = Y.unop.hom
⊢ NatTrans.app X.unop.hom (op Y.unop.left) (𝟙 Y.unop.left ≫ f.unop.left) =
    NatTrans.app X.unop.hom (op Y.unop.left) f.unop.left
[PROOFSTEP]
erw [Category.id_comp]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ (toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F = 𝟭 (Functor.Elements F)
[PROOFSTEP]
refine' Functor.ext _ _
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ ∀ (X : Functor.Elements F),
    ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X = (𝟭 (Functor.Elements F)).obj X
[PROOFSTEP]
intro X
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : Functor.Elements F
⊢ ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X = (𝟭 (Functor.Elements F)).obj X
[PROOFSTEP]
exact Functor.Elements.ext _ _ rfl (by simp [yonedaEquiv])
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : Functor.Elements F
⊢ F.map
      (eqToHom
        (_ :
          (((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X).fst =
            (((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X).fst))
      (((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X).snd =
    ((𝟭 (Functor.Elements F)).obj X).snd
[PROOFSTEP]
simp [yonedaEquiv]
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ ∀ (X Y : Functor.Elements F) (f : X ⟶ Y),
    ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).map f =
      eqToHom (_ : ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X = (𝟭 (Functor.Elements F)).obj X) ≫
        (𝟭 (Functor.Elements F)).map f ≫
          eqToHom
            (_ : (𝟭 (Functor.Elements F)).obj Y = ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj Y)
[PROOFSTEP]
intro X Y f
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
⊢ ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).map f =
    eqToHom (_ : ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X = (𝟭 (Functor.Elements F)).obj X) ≫
      (𝟭 (Functor.Elements F)).map f ≫
        eqToHom (_ : (𝟭 (Functor.Elements F)).obj Y = ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj Y)
[PROOFSTEP]
have : ∀ {a b : F.Elements} (H : a = b), (eqToHom H).1 = eqToHom (show a.fst = b.fst by cases H; rfl) :=
  by
  rintro _ _ rfl
  simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
a b : Functor.Elements F
H : a = b
⊢ a.fst = b.fst
[PROOFSTEP]
cases H
[GOAL]
case refl
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
a : Functor.Elements F
⊢ a.fst = a.fst
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
⊢ ∀ {a b : Functor.Elements F} (H : a = b), ↑(eqToHom H) = eqToHom (_ : a.fst = b.fst)
[PROOFSTEP]
rintro _ _ rfl
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
a✝ : Functor.Elements F
⊢ ↑(eqToHom (_ : a✝ = a✝)) = eqToHom (_ : a✝.fst = a✝.fst)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
this : ∀ {a b : Functor.Elements F} (H : a = b), ↑(eqToHom H) = eqToHom (_ : a.fst = b.fst)
⊢ ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).map f =
    eqToHom (_ : ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X = (𝟭 (Functor.Elements F)).obj X) ≫
      (𝟭 (Functor.Elements F)).map f ≫
        eqToHom (_ : (𝟭 (Functor.Elements F)).obj Y = ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj Y)
[PROOFSTEP]
ext
[GOAL]
case refine'_2.w
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : Functor.Elements F
f : X ⟶ Y
this : ∀ {a b : Functor.Elements F} (H : a = b), ↑(eqToHom H) = eqToHom (_ : a.fst = b.fst)
⊢ ↑(((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).map f) =
    ↑(eqToHom (_ : ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj X = (𝟭 (Functor.Elements F)).obj X) ≫
        (𝟭 (Functor.Elements F)).map f ≫
          eqToHom
            (_ : (𝟭 (Functor.Elements F)).obj Y = ((toCostructuredArrow F).rightOp ⋙ fromCostructuredArrow F).obj Y))
[PROOFSTEP]
simp [this]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ (fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F = 𝟭 (CostructuredArrow yoneda F)
[PROOFSTEP]
refine' Functor.ext _ _
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ ∀ (X : CostructuredArrow yoneda F),
    ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X = (𝟭 (CostructuredArrow yoneda F)).obj X
[PROOFSTEP]
intro X
[GOAL]
case refine'_1
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X : CostructuredArrow yoneda F
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X = (𝟭 (CostructuredArrow yoneda F)).obj X
[PROOFSTEP]
cases' X with X_left X_right X_hom
[GOAL]
case refine'_1.mk
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
X_right : Discrete PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj X_right
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj { left := X_left, right := X_right, hom := X_hom } =
    (𝟭 (CostructuredArrow yoneda F)).obj { left := X_left, right := X_right, hom := X_hom }
[PROOFSTEP]
cases X_right
[GOAL]
case refine'_1.mk.mk
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj
      { left := X_left, right := { as := as✝ }, hom := X_hom } =
    (𝟭 (CostructuredArrow yoneda F)).obj { left := X_left, right := { as := as✝ }, hom := X_hom }
[PROOFSTEP]
simp only [Functor.id_obj, Functor.rightOp_obj, toCostructuredArrow_obj, Functor.comp_obj, CostructuredArrow.mk]
[GOAL]
case refine'_1.mk.mk
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
⊢ {
      left :=
        (op
                ((fromCostructuredArrow F).obj
                  (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.fst.unop,
      right := { as := PUnit.unit },
      hom :=
        (yonedaSections
              (op
                      ((fromCostructuredArrow F).obj
                        (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.fst.unop
              F).inv
          {
            down :=
              (op
                    ((fromCostructuredArrow F).obj
                      (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.snd } } =
    { left := X_left, right := { as := as✝ }, hom := X_hom }
[PROOFSTEP]
congr
[GOAL]
case refine'_1.mk.mk.e_hom
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
⊢ (yonedaSections
          (op
                  ((fromCostructuredArrow F).obj
                    (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.fst.unop
          F).inv
      {
        down :=
          (op
                ((fromCostructuredArrow F).obj
                  (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.snd } =
    X_hom
[PROOFSTEP]
ext x f
[GOAL]
case refine'_1.mk.mk.e_hom.w.h.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
x : Cᵒᵖ
f :
  (yoneda.obj
        (op
                ((fromCostructuredArrow F).obj
                  (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.fst.unop).obj
    x
⊢ NatTrans.app
      ((yonedaSections
            (op
                    ((fromCostructuredArrow F).obj
                      (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.fst.unop
            F).inv
        {
          down :=
            (op
                  ((fromCostructuredArrow F).obj
                    (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.snd })
      x f =
    NatTrans.app X_hom x f
[PROOFSTEP]
convert congr_fun (X_hom.naturality f.op).symm (𝟙 X_left)
[GOAL]
case h.e'_3.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X_left : C
as✝ : PUnit
X_hom : yoneda.obj X_left ⟶ (Functor.fromPUnit F).obj { as := as✝ }
x : Cᵒᵖ
f :
  (yoneda.obj
        (op
                ((fromCostructuredArrow F).obj
                  (op { left := X_left, right := { as := as✝ }, hom := X_hom }))).unop.fst.unop).obj
    x
e_1✝ : F.obj x = ((Functor.fromPUnit F).obj { as := as✝ }).obj (op x.unop)
⊢ NatTrans.app X_hom x f = ((yoneda.obj X_left).map f.op ≫ NatTrans.app X_hom (op x.unop)) (𝟙 X_left)
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
⊢ ∀ (X Y : CostructuredArrow yoneda F) (f : X ⟶ Y),
    ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).map f =
      eqToHom
          (_ :
            ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X =
              (𝟭 (CostructuredArrow yoneda F)).obj X) ≫
        (𝟭 (CostructuredArrow yoneda F)).map f ≫
          eqToHom
            (_ :
              (𝟭 (CostructuredArrow yoneda F)).obj Y =
                ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj Y)
[PROOFSTEP]
intro X Y f
[GOAL]
case refine'_2
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : CostructuredArrow yoneda F
f : X ⟶ Y
⊢ ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).map f =
    eqToHom
        (_ :
          ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X = (𝟭 (CostructuredArrow yoneda F)).obj X) ≫
      (𝟭 (CostructuredArrow yoneda F)).map f ≫
        eqToHom
          (_ :
            (𝟭 (CostructuredArrow yoneda F)).obj Y = ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj Y)
[PROOFSTEP]
ext
[GOAL]
case refine'_2.h
C : Type u
inst✝ : Category.{v, u} C
F✝ : C ⥤ Type w
F : Cᵒᵖ ⥤ Type v
X Y : CostructuredArrow yoneda F
f : X ⟶ Y
⊢ (((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).map f).left =
    (eqToHom
          (_ :
            ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj X =
              (𝟭 (CostructuredArrow yoneda F)).obj X) ≫
        (𝟭 (CostructuredArrow yoneda F)).map f ≫
          eqToHom
            (_ :
              (𝟭 (CostructuredArrow yoneda F)).obj Y =
                ((fromCostructuredArrow F).rightOp ⋙ toCostructuredArrow F).obj Y)).left
[PROOFSTEP]
simp [CostructuredArrow.eqToHom_left]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ (map α).op ⋙ toCostructuredArrow F₂ = toCostructuredArrow F₁ ⋙ CostructuredArrow.map α
[PROOFSTEP]
fapply Functor.ext
[GOAL]
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ ∀ (X : (Functor.Elements F₁)ᵒᵖ),
    ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X
[PROOFSTEP]
intro X
[GOAL]
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
⊢ ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X
[PROOFSTEP]
simp only [CostructuredArrow.map_mk, toCostructuredArrow_obj, Functor.op_obj, Functor.comp_obj]
[GOAL]
case h_obj
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
⊢ CostructuredArrow.mk
      ((yonedaSections (op ((map α).obj X.unop)).unop.fst.unop F₂).inv { down := (op ((map α).obj X.unop)).unop.snd }) =
    CostructuredArrow.mk ((yonedaSections X.unop.fst.unop F₁).inv { down := X.unop.snd } ≫ α)
[PROOFSTEP]
congr
[GOAL]
case h_obj.e_f
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
⊢ (yonedaSections (op ((map α).obj X.unop)).unop.fst.unop F₂).inv { down := (op ((map α).obj X.unop)).unop.snd } =
    (yonedaSections X.unop.fst.unop F₁).inv { down := X.unop.snd } ≫ α
[PROOFSTEP]
ext _ f
[GOAL]
case h_obj.e_f.w.h.h
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X : (Functor.Elements F₁)ᵒᵖ
x✝ : Cᵒᵖ
f : (yoneda.obj (op ((map α).obj X.unop)).unop.fst.unop).obj x✝
⊢ NatTrans.app
      ((yonedaSections (op ((map α).obj X.unop)).unop.fst.unop F₂).inv { down := (op ((map α).obj X.unop)).unop.snd })
      x✝ f =
    NatTrans.app ((yonedaSections X.unop.fst.unop F₁).inv { down := X.unop.snd } ≫ α) x✝ f
[PROOFSTEP]
simpa using congr_fun (α.naturality f.op).symm (unop X).snd
[GOAL]
case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
⊢ autoParam
    (∀ (X Y : (Functor.Elements F₁)ᵒᵖ) (f : X ⟶ Y),
      ((map α).op ⋙ toCostructuredArrow F₂).map f =
        eqToHom
            (_ :
              ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X) ≫
          (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫
            eqToHom
              (_ :
                (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj Y = ((map α).op ⋙ toCostructuredArrow F₂).obj Y))
    _auto✝
[PROOFSTEP]
intro X Y f
[GOAL]
case h_map
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X Y : (Functor.Elements F₁)ᵒᵖ
f : X ⟶ Y
⊢ ((map α).op ⋙ toCostructuredArrow F₂).map f =
    eqToHom
        (_ : ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X) ≫
      (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫
        eqToHom
          (_ : (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj Y = ((map α).op ⋙ toCostructuredArrow F₂).obj Y)
[PROOFSTEP]
ext
[GOAL]
case h_map.h
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
F₁ F₂ : Cᵒᵖ ⥤ Type v
α : F₁ ⟶ F₂
X Y : (Functor.Elements F₁)ᵒᵖ
f : X ⟶ Y
⊢ (((map α).op ⋙ toCostructuredArrow F₂).map f).left =
    (eqToHom
          (_ : ((map α).op ⋙ toCostructuredArrow F₂).obj X = (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj X) ≫
        (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).map f ≫
          eqToHom
            (_ :
              (toCostructuredArrow F₁ ⋙ CostructuredArrow.map α).obj Y =
                ((map α).op ⋙ toCostructuredArrow F₂).obj Y)).left
[PROOFSTEP]
simp [CostructuredArrow.eqToHom_left]


[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
⊢ IsReflexivePair (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
[PROOFSTEP]
apply IsReflexivePair.mk' ((F).map ((adj).unit.app _)) _ _
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
⊢ F.map (NatTrans.app adj.unit A.A) ≫ F.map A.a = 𝟙 (F.obj ((𝟭 C).obj A.A))
[PROOFSTEP]
rw [← (F).map_comp, ← (F).map_id]
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
⊢ F.map (NatTrans.app adj.unit A.A ≫ A.a) = F.map (𝟙 ((𝟭 C).obj A.A))
[PROOFSTEP]
exact congr_arg (F).map A.unit
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
⊢ F.map (NatTrans.app adj.unit A.A) ≫ NatTrans.app adj.counit (F.obj A.A) = 𝟙 (F.obj ((𝟭 C).obj A.A))
[PROOFSTEP]
rw [(adj).left_triangle_components]
[GOAL]
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
⊢ 𝟙 (F.obj A.A) = 𝟙 (F.obj ((𝟭 C).obj A.A))
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
B : D
inst✝ : HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
⊢ { f // F.map A.a ≫ f = NatTrans.app adj.counit (F.obj A.A) ≫ f } ≃
    { g // G.map (F.map g) ≫ G.map (NatTrans.app adj.counit B) = A.a ≫ g }
[PROOFSTEP]
refine' ((adj).homEquiv _ _).subtypeEquiv _
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
B : D
inst✝ : HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
⊢ ∀ (a : F.obj A.A ⟶ B),
    F.map A.a ≫ a = NatTrans.app adj.counit (F.obj A.A) ≫ a ↔
      G.map (F.map (↑(Adjunction.homEquiv adj A.A B) a)) ≫ G.map (NatTrans.app adj.counit B) =
        A.a ≫ ↑(Adjunction.homEquiv adj A.A B) a
[PROOFSTEP]
intro f
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
B : D
inst✝ : HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ F.map A.a ≫ f = NatTrans.app adj.counit (F.obj A.A) ≫ f ↔
    G.map (F.map (↑(Adjunction.homEquiv adj A.A B) f)) ≫ G.map (NatTrans.app adj.counit B) =
      A.a ≫ ↑(Adjunction.homEquiv adj A.A B) f
[PROOFSTEP]
rw [← ((adj).homEquiv _ _).injective.eq_iff, Adjunction.homEquiv_naturality_left, (adj).homEquiv_unit,
  (adj).homEquiv_unit, G.map_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
B : D
inst✝ : HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ NatTrans.app adj.unit A.A ≫ G.map f =
      NatTrans.app adj.unit ((Adjunction.toMonad adj).toFunctor.obj A.A) ≫
        G.map (NatTrans.app adj.counit (F.obj A.A)) ≫ G.map f ↔
    G.map (F.map (NatTrans.app adj.unit A.A ≫ G.map f)) ≫ G.map (NatTrans.app adj.counit B) =
      A.a ≫ NatTrans.app adj.unit A.A ≫ G.map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
B : D
inst✝ : HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ NatTrans.app adj.unit A.A ≫ G.map f =
      NatTrans.app adj.unit (G.obj (F.obj A.A)) ≫ G.map (NatTrans.app adj.counit (F.obj A.A)) ≫ G.map f ↔
    G.map (F.map (NatTrans.app adj.unit A.A ≫ G.map f)) ≫ G.map (NatTrans.app adj.counit B) =
      A.a ≫ NatTrans.app adj.unit A.A ≫ G.map f
[PROOFSTEP]
rw [(adj).right_triangle_components_assoc, ← G.map_comp, (F).map_comp, Category.assoc, (adj).counit_naturality,
  (adj).left_triangle_components_assoc]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
B : D
inst✝ : HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
f : F.obj A.A ⟶ B
⊢ A.a ≫ NatTrans.app adj.unit A.A ≫ G.map f = G.map f ↔ G.map f = A.a ≫ NatTrans.app adj.unit A.A ≫ G.map f
[PROOFSTEP]
apply eq_comm
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
B : D
inst✝ : HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
g : { g // G.map (F.map g) ≫ G.map (NatTrans.app adj.counit B) = A.a ≫ g }
⊢ (fun f =>
        { val := f.f,
          property := (_ : (Adjunction.toMonad adj).toFunctor.map f.f ≫ ((comparison adj).obj B).a = A.a ≫ f.f) })
      ((fun g => Algebra.Hom.mk ↑g) g) =
    g
[PROOFSTEP]
ext
[GOAL]
case a
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
B : D
inst✝ : HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
g : { g // G.map (F.map g) ≫ G.map (NatTrans.app adj.counit B) = A.a ≫ g }
⊢ ↑((fun f =>
          { val := f.f,
            property := (_ : (Adjunction.toMonad adj).toFunctor.map f.f ≫ ((comparison adj).obj B).a = A.a ≫ f.f) })
        ((fun g => Algebra.Hom.mk ↑g) g)) =
    ↑g
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
B : D
inst✝ : HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
f : A ⟶ (comparison adj).obj B
⊢ (fun g => Algebra.Hom.mk ↑g)
      ((fun f =>
          { val := f.f,
            property := (_ : (Adjunction.toMonad adj).toFunctor.map f.f ≫ ((comparison adj).obj B).a = A.a ≫ f.f) })
        f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
B : D
inst✝ : HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
f : A ⟶ (comparison adj).obj B
⊢ ((fun g => Algebra.Hom.mk ↑g)
        ((fun f =>
            { val := f.f,
              property := (_ : (Adjunction.toMonad adj).toFunctor.map f.f ≫ ((comparison adj).obj B).a = A.a ≫ f.f) })
          f)).f =
    f.f
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : ∀ (A : Algebra (Adjunction.toMonad adj)), HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
⊢ Algebra (Adjunction.toMonad adj) ⥤ D
[PROOFSTEP]
refine'
  Adjunction.leftAdjointOfEquiv (G := comparison adj) (F_obj := fun A => comparisonLeftAdjointObj A) (fun A B => _) _
[GOAL]
case refine'_1
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : ∀ (A : Algebra (Adjunction.toMonad adj)), HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
A : Algebra (Adjunction.toMonad adj)
B : D
⊢ ((fun A => comparisonLeftAdjointObj A) A ⟶ B) ≃ (A ⟶ (comparison adj).obj B)
[PROOFSTEP]
apply comparisonLeftAdjointHomEquiv
[GOAL]
case refine'_2
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : ∀ (A : Algebra (Adjunction.toMonad adj)), HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
⊢ ∀ (X : Algebra (Adjunction.toMonad adj)) (Y Y' : D) (g : Y ⟶ Y') (h : (fun A => comparisonLeftAdjointObj A) X ⟶ Y),
    ↑((fun A B => comparisonLeftAdjointHomEquiv A B) X Y') (h ≫ g) =
      ↑((fun A B => comparisonLeftAdjointHomEquiv A B) X Y) h ≫ (comparison adj).map g
[PROOFSTEP]
intro A B B' g h
[GOAL]
case refine'_2
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : ∀ (A : Algebra (Adjunction.toMonad adj)), HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
A : Algebra (Adjunction.toMonad adj)
B B' : D
g : B ⟶ B'
h : (fun A => comparisonLeftAdjointObj A) A ⟶ B
⊢ ↑((fun A B => comparisonLeftAdjointHomEquiv A B) A B') (h ≫ g) =
    ↑((fun A B => comparisonLeftAdjointHomEquiv A B) A B) h ≫ (comparison adj).map g
[PROOFSTEP]
ext1
  -- Porting note: the goal was previously closed by the following, which succeeds until
      -- `Category.assoc`.
      -- dsimp [comparisonLeftAdjointHomEquiv]
      -- rw [← (adj).homEquiv_naturality_right, Category.assoc]
[GOAL]
case refine'_2.h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : ∀ (A : Algebra (Adjunction.toMonad adj)), HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
A : Algebra (Adjunction.toMonad adj)
B B' : D
g : B ⟶ B'
h : (fun A => comparisonLeftAdjointObj A) A ⟶ B
⊢ (↑((fun A B => comparisonLeftAdjointHomEquiv A B) A B') (h ≫ g)).f =
    (↑((fun A B => comparisonLeftAdjointHomEquiv A B) A B) h ≫ (comparison adj).map g).f
[PROOFSTEP]
simp [Cofork.IsColimit.homIso]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
inst✝ : HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
⊢ G.map (F.map A.a) ≫ G.map (coequalizer.π (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))) =
    G.map (NatTrans.app adj.counit (F.obj A.A)) ≫
      G.map (coequalizer.π (F.map A.a) (NatTrans.app adj.counit (F.obj A.A)))
[PROOFSTEP]
change _ = G.map _ ≫ _
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
A : Algebra (Adjunction.toMonad adj)
inst✝ : HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
⊢ G.map (F.map A.a) ≫ G.map (coequalizer.π (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))) =
    G.map (NatTrans.app adj.counit (F.obj A.A)) ≫
      G.map (coequalizer.π (F.map A.a) (NatTrans.app adj.counit (F.obj A.A)))
[PROOFSTEP]
rw [← G.map_comp, coequalizer.condition, G.map_comp]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : ∀ (A : Algebra (Adjunction.toMonad adj)), HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
A : Algebra (Adjunction.toMonad adj)
⊢ (NatTrans.app comparisonAdjunction.unit A).f = IsColimit.desc (beckCoequalizer A) (unitCofork A)
[PROOFSTEP]
apply Limits.Cofork.IsColimit.hom_ext (beckCoequalizer A)
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : ∀ (A : Algebra (Adjunction.toMonad adj)), HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
A : Algebra (Adjunction.toMonad adj)
⊢ Cofork.π (beckCofork A) ≫ (NatTrans.app comparisonAdjunction.unit A).f =
    Cofork.π (beckCofork A) ≫ IsColimit.desc (beckCoequalizer A) (unitCofork A)
[PROOFSTEP]
rw [Cofork.IsColimit.π_desc]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : ∀ (A : Algebra (Adjunction.toMonad adj)), HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
A : Algebra (Adjunction.toMonad adj)
⊢ Cofork.π (beckCofork A) ≫ (NatTrans.app comparisonAdjunction.unit A).f = Cofork.π (unitCofork A)
[PROOFSTEP]
dsimp only [beckCofork_π, unitCofork_π]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : ∀ (A : Algebra (Adjunction.toMonad adj)), HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
A : Algebra (Adjunction.toMonad adj)
⊢ A.a ≫ (NatTrans.app comparisonAdjunction.unit A).f =
    G.map (coequalizer.π (F.map A.a) (NatTrans.app adj.counit (F.obj A.A)))
[PROOFSTEP]
rw [comparisonAdjunction_unit_f_aux, ← (adj).homEquiv_naturality_left A.a, coequalizer.condition,
  (adj).homEquiv_naturality_right, (adj).homEquiv_unit, Category.assoc]
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : ∀ (A : Algebra (Adjunction.toMonad adj)), HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
A : Algebra (Adjunction.toMonad adj)
⊢ NatTrans.app adj.unit ((Adjunction.toMonad adj).toFunctor.obj A.A) ≫
      G.map (NatTrans.app adj.counit (F.obj A.A)) ≫
        G.map (coequalizer.π (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))) =
    G.map (coequalizer.π (F.map A.a) (NatTrans.app adj.counit (F.obj A.A)))
[PROOFSTEP]
apply (adj).right_triangle_components_assoc
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : ∀ (A : Algebra (Adjunction.toMonad adj)), HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
B : D
⊢ NatTrans.app comparisonAdjunction.counit B =
    colimit.desc (parallelPair (F.map (G.map (NatTrans.app adj.counit B))) (NatTrans.app adj.counit (F.obj (G.obj B))))
      (counitCofork B)
[PROOFSTEP]
apply coequalizer.hom_ext
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : ∀ (A : Algebra (Adjunction.toMonad adj)), HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
B : D
⊢ coequalizer.π (F.map ((comparison adj).obj B).a) (NatTrans.app adj.counit (F.obj ((comparison adj).obj B).A)) ≫
      NatTrans.app comparisonAdjunction.counit B =
    coequalizer.π (F.map ((comparison adj).obj B).a) (NatTrans.app adj.counit (F.obj ((comparison adj).obj B).A)) ≫
      colimit.desc
        (parallelPair (F.map (G.map (NatTrans.app adj.counit B))) (NatTrans.app adj.counit (F.obj (G.obj B))))
        (counitCofork B)
[PROOFSTEP]
change
  coequalizer.π _ _ ≫ coequalizer.desc (((adj).homEquiv _ B).symm (𝟙 _)) _ = coequalizer.π _ _ ≫ coequalizer.desc _ _
[GOAL]
case h
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : ∀ (A : Algebra (Adjunction.toMonad adj)), HasCoequalizer (F.map A.a) (NatTrans.app adj.counit (F.obj A.A))
B : D
⊢ coequalizer.π (F.map ((comparison adj).obj B).a) (NatTrans.app adj.counit (F.obj ((comparison adj).obj B).A)) ≫
      coequalizer.desc (↑(Adjunction.homEquiv adj (G.obj B) B).symm (𝟙 (G.obj B)))
        (_ :
          F.map ((comparison adj).obj B).a ≫
              ↑(↑(Equiv.subtypeEquiv (Adjunction.homEquiv adj ((comparison adj).obj B).A ((𝟭 D).obj B))
                        (_ :
                          ∀ (f : F.obj ((comparison adj).obj B).A ⟶ (𝟭 D).obj B),
                            F.map ((comparison adj).obj B).a ≫ f =
                                NatTrans.app adj.counit (F.obj ((comparison adj).obj B).A) ≫ f ↔
                              G.map (F.map (↑(Adjunction.homEquiv adj ((comparison adj).obj B).A ((𝟭 D).obj B)) f)) ≫
                                  G.map (NatTrans.app adj.counit ((𝟭 D).obj B)) =
                                ((comparison adj).obj B).a ≫
                                  ↑(Adjunction.homEquiv adj ((comparison adj).obj B).A ((𝟭 D).obj B)) f)).symm
                  (↑{ toFun := fun g => Algebra.Hom.mk ↑g,
                          invFun := fun f =>
                            { val := f.f,
                              property :=
                                (_ :
                                  (Adjunction.toMonad adj).toFunctor.map f.f ≫ ((comparison adj).obj ((𝟭 D).obj B)).a =
                                    ((comparison adj).obj B).a ≫ f.f) },
                          left_inv :=
                            (_ :
                              ∀
                                (g :
                                  { g //
                                    G.map (F.map g) ≫ G.map (NatTrans.app adj.counit ((𝟭 D).obj B)) =
                                      ((comparison adj).obj B).a ≫ g }),
                                (fun f =>
                                      { val := f.f,
                                        property :=
                                          (_ :
                                            (Adjunction.toMonad adj).toFunctor.map f.f ≫
                                                ((comparison adj).obj ((𝟭 D).obj B)).a =
                                              ((comparison adj).obj B).a ≫ f.f) })
                                    ((fun g => Algebra.Hom.mk ↑g) g) =
                                  g),
                          right_inv :=
                            (_ :
                              ∀ (f : (comparison adj).obj B ⟶ (comparison adj).obj ((𝟭 D).obj B)),
                                (fun g => Algebra.Hom.mk ↑g)
                                    ((fun f =>
                                        { val := f.f,
                                          property :=
                                            (_ :
                                              (Adjunction.toMonad adj).toFunctor.map f.f ≫
                                                  ((comparison adj).obj ((𝟭 D).obj B)).a =
                                                ((comparison adj).obj B).a ≫ f.f) })
                                      f) =
                                  f) }.symm
                    (𝟙 ((comparison adj).obj B)))) =
            NatTrans.app adj.counit (F.obj ((comparison adj).obj B).A) ≫
              ↑(↑(Equiv.subtypeEquiv (Adjunction.homEquiv adj ((comparison adj).obj B).A ((𝟭 D).obj B))
                        (_ :
                          ∀ (f : F.obj ((comparison adj).obj B).A ⟶ (𝟭 D).obj B),
                            F.map ((comparison adj).obj B).a ≫ f =
                                NatTrans.app adj.counit (F.obj ((comparison adj).obj B).A) ≫ f ↔
                              G.map (F.map (↑(Adjunction.homEquiv adj ((comparison adj).obj B).A ((𝟭 D).obj B)) f)) ≫
                                  G.map (NatTrans.app adj.counit ((𝟭 D).obj B)) =
                                ((comparison adj).obj B).a ≫
                                  ↑(Adjunction.homEquiv adj ((comparison adj).obj B).A ((𝟭 D).obj B)) f)).symm
                  (↑{ toFun := fun g => Algebra.Hom.mk ↑g,
                          invFun := fun f =>
                            { val := f.f,
                              property :=
                                (_ :
                                  (Adjunction.toMonad adj).toFunctor.map f.f ≫ ((comparison adj).obj ((𝟭 D).obj B)).a =
                                    ((comparison adj).obj B).a ≫ f.f) },
                          left_inv :=
                            (_ :
                              ∀
                                (g :
                                  { g //
                                    G.map (F.map g) ≫ G.map (NatTrans.app adj.counit ((𝟭 D).obj B)) =
                                      ((comparison adj).obj B).a ≫ g }),
                                (fun f =>
                                      { val := f.f,
                                        property :=
                                          (_ :
                                            (Adjunction.toMonad adj).toFunctor.map f.f ≫
                                                ((comparison adj).obj ((𝟭 D).obj B)).a =
                                              ((comparison adj).obj B).a ≫ f.f) })
                                    ((fun g => Algebra.Hom.mk ↑g) g) =
                                  g),
                          right_inv :=
                            (_ :
                              ∀ (f : (comparison adj).obj B ⟶ (comparison adj).obj ((𝟭 D).obj B)),
                                (fun g => Algebra.Hom.mk ↑g)
                                    ((fun f =>
                                        { val := f.f,
                                          property :=
                                            (_ :
                                              (Adjunction.toMonad adj).toFunctor.map f.f ≫
                                                  ((comparison adj).obj ((𝟭 D).obj B)).a =
                                                ((comparison adj).obj B).a ≫ f.f) })
                                      f) =
                                  f) }.symm
                    (𝟙 ((comparison adj).obj B))))) =
    coequalizer.π (F.map ((comparison adj).obj B).a) (NatTrans.app adj.counit (F.obj ((comparison adj).obj B).A)) ≫
      coequalizer.desc (NatTrans.app adj.counit B)
        (_ :
          F.map (G.map (NatTrans.app adj.counit B)) ≫ NatTrans.app adj.counit ((𝟭 D).obj B) =
            NatTrans.app adj.counit ((G ⋙ F).obj B) ≫ NatTrans.app adj.counit B)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : Functor.IsSplitPair G f g
⊢ CreatesColimit (parallelPair f g) G
[PROOFSTEP]
apply (config := { allowSynthFailures := true }) monadicCreatesColimitOfPreservesColimit
[GOAL]
case inst
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : Functor.IsSplitPair G f g
⊢ PreservesColimit (parallelPair f g ⋙ G) (F ⋙ G)
[PROOFSTEP]
apply @preservesColimitOfIsoDiagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : Functor.IsSplitPair G f g
⊢ PreservesColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))
    (F ⋙ G)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : Functor.IsSplitPair G f g
⊢ PreservesColimit (parallelPair (G.map f) (G.map g)) (F ⋙ G)
[PROOFSTEP]
infer_instance
[GOAL]
case inst
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : Functor.IsSplitPair G f g
⊢ PreservesColimit ((parallelPair f g ⋙ G) ⋙ F ⋙ G) (F ⋙ G)
[PROOFSTEP]
apply @preservesColimitOfIsoDiagram _ _ _ _ _ _ _ _ _ (diagramIsoParallelPair.{v₁} _).symm ?_
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : Functor.IsSplitPair G f g
⊢ PreservesColimit
    (parallelPair (((parallelPair f g ⋙ G) ⋙ F ⋙ G).map WalkingParallelPairHom.left)
      (((parallelPair f g ⋙ G) ⋙ F ⋙ G).map WalkingParallelPairHom.right))
    (F ⋙ G)
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : MonadicRightAdjoint G
A B : D
f g : A ⟶ B
inst✝ : Functor.IsSplitPair G f g
⊢ PreservesColimit (parallelPair (G.map (F.map (G.map f))) (G.map (F.map (G.map g)))) (F ⋙ G)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
⊢ MonadicRightAdjoint G
[PROOFSTEP]
let i : IsRightAdjoint (comparison (ofRightAdjoint G)) := ⟨_, comparisonAdjunction⟩
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
⊢ MonadicRightAdjoint G
[PROOFSTEP]
constructor
[GOAL]
case eqv
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
⊢ IsEquivalence (comparison adj)
[PROOFSTEP]
let _ : ∀ X : (ofRightAdjoint G).toMonad.Algebra, IsIso ((ofRightAdjoint (comparison (ofRightAdjoint G))).unit.app X) :=
  by
  intro X
  apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget (ofRightAdjoint G).toMonad) ?_ _
  · change IsIso (comparisonAdjunction.unit.app X).f
    rw [comparisonAdjunction_unit_f]
    change IsIso (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X) (unitColimitOfPreservesCoequalizer X)).hom
    refine' IsIso.of_iso (IsColimit.coconePointUniqueUpToIso _ _)
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
⊢ ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X)
[PROOFSTEP]
intro X
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
X : Algebra (toMonad adj)
⊢ IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X)
[PROOFSTEP]
apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget (ofRightAdjoint G).toMonad) ?_ _
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
X : Algebra (toMonad adj)
⊢ IsIso ((forget (toMonad adj)).map (NatTrans.app (ofRightAdjoint (comparison adj)).unit X))
[PROOFSTEP]
change IsIso (comparisonAdjunction.unit.app X).f
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
X : Algebra (toMonad adj)
⊢ IsIso (NatTrans.app comparisonAdjunction.unit X).f
[PROOFSTEP]
rw [comparisonAdjunction_unit_f]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
X : Algebra (toMonad adj)
⊢ IsIso (IsColimit.desc (beckCoequalizer X) (unitCofork X))
[PROOFSTEP]
change IsIso (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X) (unitColimitOfPreservesCoequalizer X)).hom
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
X : Algebra (toMonad adj)
⊢ IsIso (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X) (unitColimitOfPreservesCoequalizer X)).hom
[PROOFSTEP]
refine' IsIso.of_iso (IsColimit.coconePointUniqueUpToIso _ _)
[GOAL]
case eqv
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
⊢ IsEquivalence (comparison adj)
[PROOFSTEP]
let _ : ∀ Y : D, IsIso ((ofRightAdjoint (comparison (ofRightAdjoint G))).counit.app Y) :=
  by
  intro Y
  change IsIso (comparisonAdjunction.counit.app Y)
  rw [comparisonAdjunction_counit_app]
    -- Porting note: passing instances through
  change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom
  infer_instance
    -- Porting note: passing instances through
  apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ ?_
  letI _ :
    G.IsSplitPair ((leftAdjoint G).map (G.map ((Adjunction.ofRightAdjoint G).counit.app Y)))
      ((Adjunction.ofRightAdjoint G).counit.app ((leftAdjoint G).obj (G.obj Y))) :=
    MonadicityInternal.main_pair_G_split ((comparison (Adjunction.ofRightAdjoint G)).obj Y)
  infer_instance
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
⊢ ∀ (Y : D), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).counit Y)
[PROOFSTEP]
intro Y
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).counit Y)
[PROOFSTEP]
change IsIso (comparisonAdjunction.counit.app Y)
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ IsIso (NatTrans.app comparisonAdjunction.counit Y)
[PROOFSTEP]
rw [comparisonAdjunction_counit_app]
  -- Porting note: passing instances through
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ IsIso
    (colimit.desc (parallelPair (F.map (G.map (NatTrans.app adj.counit Y))) (NatTrans.app adj.counit (F.obj (G.obj Y))))
      (counitCofork Y))
[PROOFSTEP]
change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom
[GOAL]
case refine_2
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ IsIso
    (IsColimit.coconePointUniqueUpToIso
        (colimit.isColimit
          (parallelPair (F.map (G.map (NatTrans.app adj.counit Y))) (NatTrans.app adj.counit (F.obj (G.obj Y)))))
        ?refine_1).hom
case refine_1
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ IsColimit (counitCofork Y)
[PROOFSTEP]
infer_instance
  -- Porting note: passing instances through
[GOAL]
case refine_1
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ IsColimit (counitCofork Y)
[PROOFSTEP]
apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ ?_
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ ReflectsColimit (parallelPair (F.map (G.map (NatTrans.app adj.counit Y))) (NatTrans.app adj.counit (F.obj (G.obj Y))))
    G
[PROOFSTEP]
letI _ :
  G.IsSplitPair ((leftAdjoint G).map (G.map ((Adjunction.ofRightAdjoint G).counit.app Y)))
    ((Adjunction.ofRightAdjoint G).counit.app ((leftAdjoint G).obj (G.obj Y))) :=
  MonadicityInternal.main_pair_G_split ((comparison (Adjunction.ofRightAdjoint G)).obj Y)
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝¹ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
x✝ : Functor.IsSplitPair G (F.map (G.map (NatTrans.app adj.counit Y))) (NatTrans.app adj.counit (F.obj (G.obj Y))) :=
  main_pair_G_split ((comparison adj).obj Y)
⊢ ReflectsColimit (parallelPair (F.map (G.map (NatTrans.app adj.counit Y))) (NatTrans.app adj.counit (F.obj (G.obj Y))))
    G
[PROOFSTEP]
infer_instance
[GOAL]
case eqv
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
inst✝ : ReflectsColimitOfIsSplitPair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝¹ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
x✝ : ∀ (Y : D), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).counit Y) :=
  fun Y =>
    let_fun this :=
      Eq.mpr
        (_root_.id (comparisonAdjunction_counit_app Y ▸ Eq.refl (IsIso (NatTrans.app comparisonAdjunction.counit Y))))
        (let_fun this := inferInstance;
        this);
    this
⊢ IsEquivalence (comparison adj)
[PROOFSTEP]
exact Adjunction.isRightAdjointToIsEquivalence
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : CreatesColimitOfIsSplitPair G
⊢ MonadicRightAdjoint G
[PROOFSTEP]
let I {A B} (f g : A ⟶ B) [G.IsSplitPair f g] : HasColimit (parallelPair f g ⋙ G) :=
  by
  apply @hasColimitOfIso _ _ _ _ _ _ ?_ (diagramIsoParallelPair.{v₁} _)
  exact inferInstanceAs <| HasCoequalizer (G.map f) (G.map g)
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝² : IsRightAdjoint G
inst✝¹ : CreatesColimitOfIsSplitPair G
A B : D
f g : A ⟶ B
inst✝ : Functor.IsSplitPair G f g
⊢ HasColimit (parallelPair f g ⋙ G)
[PROOFSTEP]
apply @hasColimitOfIso _ _ _ _ _ _ ?_ (diagramIsoParallelPair.{v₁} _)
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝² : IsRightAdjoint G
inst✝¹ : CreatesColimitOfIsSplitPair G
A B : D
f g : A ⟶ B
inst✝ : Functor.IsSplitPair G f g
⊢ HasColimit
    (parallelPair ((parallelPair f g ⋙ G).map WalkingParallelPairHom.left)
      ((parallelPair f g ⋙ G).map WalkingParallelPairHom.right))
[PROOFSTEP]
exact inferInstanceAs <| HasCoequalizer (G.map f) (G.map g)
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [inst : Functor.IsSplitPair G f g], HasColimit (parallelPair f g ⋙ G) :=
  fun {A B} f g [Functor.IsSplitPair G f g] => hasColimitOfIso (diagramIsoParallelPair (parallelPair f g ⋙ G))
⊢ MonadicRightAdjoint G
[PROOFSTEP]
apply @monadicOfHasPreservesReflectsGSplitCoequalizers _ _ _ _ _ _ ?_ ?_ ?_
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [inst : Functor.IsSplitPair G f g], HasColimit (parallelPair f g ⋙ G) :=
  fun {A B} f g [Functor.IsSplitPair G f g] => hasColimitOfIso (diagramIsoParallelPair (parallelPair f g ⋙ G))
⊢ HasCoequalizerOfIsSplitPair G
[PROOFSTEP]
constructor
[GOAL]
case out
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [inst : Functor.IsSplitPair G f g], HasColimit (parallelPair f g ⋙ G) :=
  fun {A B} f g [Functor.IsSplitPair G f g] => hasColimitOfIso (diagramIsoParallelPair (parallelPair f g ⋙ G))
⊢ ∀ {A B : D} (f g : A ⟶ B) [inst : Functor.IsSplitPair G f g], HasCoequalizer f g
[PROOFSTEP]
intros
[GOAL]
case out
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝² : IsRightAdjoint G
inst✝¹ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [inst : Functor.IsSplitPair G f g], HasColimit (parallelPair f g ⋙ G) :=
  fun {A B} f g [Functor.IsSplitPair G f g] => hasColimitOfIso (diagramIsoParallelPair (parallelPair f g ⋙ G))
A✝ B✝ : D
f✝ g✝ : A✝ ⟶ B✝
inst✝ : Functor.IsSplitPair G f✝ g✝
⊢ HasCoequalizer f✝ g✝
[PROOFSTEP]
apply hasColimit_of_created (parallelPair _ _) G
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [inst : Functor.IsSplitPair G f g], HasColimit (parallelPair f g ⋙ G) :=
  fun {A B} f g [Functor.IsSplitPair G f g] => hasColimitOfIso (diagramIsoParallelPair (parallelPair f g ⋙ G))
⊢ PreservesColimitOfIsSplitPair G
[PROOFSTEP]
constructor
[GOAL]
case out
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [inst : Functor.IsSplitPair G f g], HasColimit (parallelPair f g ⋙ G) :=
  fun {A B} f g [Functor.IsSplitPair G f g] => hasColimitOfIso (diagramIsoParallelPair (parallelPair f g ⋙ G))
⊢ {A B : D} → (f g : A ⟶ B) → [inst : Functor.IsSplitPair G f g] → PreservesColimit (parallelPair f g) G
[PROOFSTEP]
intros
[GOAL]
case out
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝² : IsRightAdjoint G
inst✝¹ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [inst : Functor.IsSplitPair G f g], HasColimit (parallelPair f g ⋙ G) :=
  fun {A B} f g [Functor.IsSplitPair G f g] => hasColimitOfIso (diagramIsoParallelPair (parallelPair f g ⋙ G))
A✝ B✝ : D
f✝ g✝ : A✝ ⟶ B✝
inst✝ : Functor.IsSplitPair G f✝ g✝
⊢ PreservesColimit (parallelPair f✝ g✝) G
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [inst : Functor.IsSplitPair G f g], HasColimit (parallelPair f g ⋙ G) :=
  fun {A B} f g [Functor.IsSplitPair G f g] => hasColimitOfIso (diagramIsoParallelPair (parallelPair f g ⋙ G))
⊢ ReflectsColimitOfIsSplitPair G
[PROOFSTEP]
constructor
[GOAL]
case out
C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₁, u₂} D
G : D ⥤ C
inst✝¹ : IsRightAdjoint G
inst✝ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [inst : Functor.IsSplitPair G f g], HasColimit (parallelPair f g ⋙ G) :=
  fun {A B} f g [Functor.IsSplitPair G f g] => hasColimitOfIso (diagramIsoParallelPair (parallelPair f g ⋙ G))
⊢ {A B : D} → (f g : A ⟶ B) → [inst : Functor.IsSplitPair G f g] → ReflectsColimit (parallelPair f g) G
[PROOFSTEP]
intros
[GOAL]
case out
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝² : IsRightAdjoint G
inst✝¹ : CreatesColimitOfIsSplitPair G
I : ∀ {A B : D} (f g : A ⟶ B) [inst : Functor.IsSplitPair G f g], HasColimit (parallelPair f g ⋙ G) :=
  fun {A B} f g [Functor.IsSplitPair G f g] => hasColimitOfIso (diagramIsoParallelPair (parallelPair f g ⋙ G))
A✝ B✝ : D
f✝ g✝ : A✝ ⟶ B✝
inst✝ : Functor.IsSplitPair G f✝ g✝
⊢ ReflectsColimit (parallelPair f✝ g✝) G
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasCoequalizerOfIsSplitPair G
inst✝ : PreservesColimitOfIsSplitPair G
⊢ MonadicRightAdjoint G
[PROOFSTEP]
apply (config := { allowSynthFailures := true }) @monadicOfHasPreservesReflectsGSplitCoequalizers
[GOAL]
case inst
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasCoequalizerOfIsSplitPair G
inst✝ : PreservesColimitOfIsSplitPair G
⊢ ReflectsColimitOfIsSplitPair G
[PROOFSTEP]
constructor
[GOAL]
case inst.out
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : ReflectsIsomorphisms G
inst✝¹ : HasCoequalizerOfIsSplitPair G
inst✝ : PreservesColimitOfIsSplitPair G
⊢ {A B : D} → (f g : A ⟶ B) → [inst : Functor.IsSplitPair G f g] → ReflectsColimit (parallelPair f g) G
[PROOFSTEP]
intro _ _ f g _
[GOAL]
case inst.out
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝⁴ : IsRightAdjoint G
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
A✝ B✝ : D
f g : A✝ ⟶ B✝
inst✝ : Functor.IsSplitPair G f g
⊢ ReflectsColimit (parallelPair f g) G
[PROOFSTEP]
have := HasCoequalizerOfIsSplitPair.out G f g
[GOAL]
case inst.out
C : Type u₁
D : Type u₂
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝⁴ : IsRightAdjoint G
inst✝³ : ReflectsIsomorphisms G
inst✝² : HasCoequalizerOfIsSplitPair G
inst✝¹ : PreservesColimitOfIsSplitPair G
A✝ B✝ : D
f g : A✝ ⟶ B✝
inst✝ : Functor.IsSplitPair G f g
this : HasCoequalizer f g
⊢ ReflectsColimit (parallelPair f g) G
[PROOFSTEP]
apply reflectsColimitOfReflectsIsomorphisms
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
⊢ MonadicRightAdjoint G
[PROOFSTEP]
letI i : IsRightAdjoint (comparison (Adjunction.ofRightAdjoint G)) := ⟨_, comparisonAdjunction⟩
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
⊢ MonadicRightAdjoint G
[PROOFSTEP]
constructor
[GOAL]
case eqv
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
⊢ IsEquivalence (comparison adj)
[PROOFSTEP]
let _ :
  ∀ X : (Adjunction.ofRightAdjoint G).toMonad.Algebra,
    IsIso ((Adjunction.ofRightAdjoint (comparison (Adjunction.ofRightAdjoint G))).unit.app X) :=
  by
  intro X
  apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget (Adjunction.ofRightAdjoint G).toMonad) ?_ _
  · change IsIso (comparisonAdjunction.unit.app X).f
    rw [comparisonAdjunction_unit_f]
    change IsIso (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X) (unitColimitOfPreservesCoequalizer X)).hom
    apply IsIso.of_iso (IsColimit.coconePointUniqueUpToIso _ _)
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
⊢ ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X)
[PROOFSTEP]
intro X
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
X : Algebra (toMonad adj)
⊢ IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X)
[PROOFSTEP]
apply @isIso_of_reflects_iso _ _ _ _ _ _ _ (Monad.forget (Adjunction.ofRightAdjoint G).toMonad) ?_ _
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
X : Algebra (toMonad adj)
⊢ IsIso ((forget (toMonad adj)).map (NatTrans.app (ofRightAdjoint (comparison adj)).unit X))
[PROOFSTEP]
change IsIso (comparisonAdjunction.unit.app X).f
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
X : Algebra (toMonad adj)
⊢ IsIso (NatTrans.app comparisonAdjunction.unit X).f
[PROOFSTEP]
rw [comparisonAdjunction_unit_f]
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
X : Algebra (toMonad adj)
⊢ IsIso (IsColimit.desc (beckCoequalizer X) (unitCofork X))
[PROOFSTEP]
change IsIso (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X) (unitColimitOfPreservesCoequalizer X)).hom
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
X : Algebra (toMonad adj)
⊢ IsIso (IsColimit.coconePointUniqueUpToIso (beckCoequalizer X) (unitColimitOfPreservesCoequalizer X)).hom
[PROOFSTEP]
apply IsIso.of_iso (IsColimit.coconePointUniqueUpToIso _ _)
[GOAL]
case eqv
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
⊢ IsEquivalence (comparison adj)
[PROOFSTEP]
let _ : ∀ Y : D, IsIso ((ofRightAdjoint (comparison (Adjunction.ofRightAdjoint G))).counit.app Y) :=
  by
  intro Y
  change IsIso (comparisonAdjunction.counit.app Y)
  rw [comparisonAdjunction_counit_app]
    -- Porting note: passing instances through
  change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom
  infer_instance
    -- Porting note: passing instances through
  apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ ?_
  apply reflectsColimitOfReflectsIsomorphisms
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
⊢ ∀ (Y : D), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).counit Y)
[PROOFSTEP]
intro Y
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).counit Y)
[PROOFSTEP]
change IsIso (comparisonAdjunction.counit.app Y)
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ IsIso (NatTrans.app comparisonAdjunction.counit Y)
[PROOFSTEP]
rw [comparisonAdjunction_counit_app]
  -- Porting note: passing instances through
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ IsIso
    (colimit.desc (parallelPair (F.map (G.map (NatTrans.app adj.counit Y))) (NatTrans.app adj.counit (F.obj (G.obj Y))))
      (counitCofork Y))
[PROOFSTEP]
change IsIso (IsColimit.coconePointUniqueUpToIso _ ?_).hom
[GOAL]
case refine_2
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ IsIso
    (IsColimit.coconePointUniqueUpToIso
        (colimit.isColimit
          (parallelPair (F.map (G.map (NatTrans.app adj.counit Y))) (NatTrans.app adj.counit (F.obj (G.obj Y)))))
        ?refine_1).hom
case refine_1
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ IsColimit (counitCofork Y)
[PROOFSTEP]
infer_instance
  -- Porting note: passing instances through
[GOAL]
case refine_1
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ IsColimit (counitCofork Y)
[PROOFSTEP]
apply @counitCoequalizerOfReflectsCoequalizer _ _ _ _ _ _ _ ?_
[GOAL]
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
Y : D
⊢ ReflectsColimit (parallelPair (F.map (G.map (NatTrans.app adj.counit Y))) (NatTrans.app adj.counit (F.obj (G.obj Y))))
    G
[PROOFSTEP]
apply reflectsColimitOfReflectsIsomorphisms
[GOAL]
case eqv
C : Type u₁
D : Type u₂
inst✝⁵ : Category.{v₁, u₁} C
inst✝⁴ : Category.{v₁, u₂} D
G : D ⥤ C
inst✝³ : IsRightAdjoint G
inst✝² : HasReflexiveCoequalizers D
inst✝¹ : ReflectsIsomorphisms G
inst✝ : PreservesColimitOfIsReflexivePair G
i : IsRightAdjoint (comparison adj) := { left := leftAdjointComparison, adj := comparisonAdjunction }
x✝¹ : ∀ (X : Algebra (toMonad adj)), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) :=
  fun X => isIso_of_reflects_iso (NatTrans.app (ofRightAdjoint (comparison adj)).unit X) (forget (toMonad adj))
x✝ : ∀ (Y : D), IsIso (NatTrans.app (ofRightAdjoint (comparison adj)).counit Y) :=
  fun Y =>
    let_fun this :=
      Eq.mpr
        (_root_.id (comparisonAdjunction_counit_app Y ▸ Eq.refl (IsIso (NatTrans.app comparisonAdjunction.counit Y))))
        (let_fun this := inferInstance;
        this);
    this
⊢ IsEquivalence (comparison adj)
[PROOFSTEP]
exact Adjunction.isRightAdjointToIsEquivalence