[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ (equalizerSubobjectIso f g).hom ≫ equalizer.ι f g = arrow (equalizerSubobject f g)
[PROOFSTEP]
simp [equalizerSubobjectIso]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ (equalizerSubobjectIso f g).inv ≫ arrow (equalizerSubobject f g) = equalizer.ι f g
[PROOFSTEP]
simp [equalizerSubobjectIso]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
⊢ arrow (equalizerSubobject f g) ≫ f = arrow (equalizerSubobject f g) ≫ g
[PROOFSTEP]
rw [← equalizerSubobject_arrow, Category.assoc, Category.assoc, equalizer.condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
W : C
h : W ⟶ X
w : h ≫ f = h ≫ g
⊢ equalizer.lift h w ≫ MonoOver.arrow (MonoOver.mk' (equalizer.ι f g)) = h
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f g : X ⟶ Y
inst✝ : HasEqualizer f g
W : C
h : W ⟶ X
w : Factors (equalizerSubobject f g) h
⊢ h ≫ f = h ≫ g
[PROOFSTEP]
rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, equalizerSubobject_arrow_comp, Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ (kernelSubobjectIso f).hom ≫ kernel.ι f = arrow (kernelSubobject f)
[PROOFSTEP]
simp [kernelSubobjectIso]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ (kernelSubobjectIso f).inv ≫ arrow (kernelSubobject f) = kernel.ι f
[PROOFSTEP]
simp [kernelSubobjectIso]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ arrow (kernelSubobject f) ≫ f = 0
[PROOFSTEP]
rw [← kernelSubobject_arrow]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
⊢ ((kernelSubobjectIso f).hom ≫ kernel.ι f) ≫ f = 0
[PROOFSTEP]
simp only [Category.assoc, kernel.condition, comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ kernel.lift f h w ≫ MonoOver.arrow (MonoOver.mk' (kernel.ι f)) = h
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : Factors (kernelSubobject f) h
⊢ h ≫ f = 0
[PROOFSTEP]
rw [← Subobject.factorThru_arrow _ _ w, Category.assoc, kernelSubobject_arrow_comp, comp_zero]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ factorThruKernelSubobject f h w ≫ arrow (kernelSubobject f) = h
[PROOFSTEP]
dsimp [factorThruKernelSubobject]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ factorThru (kernelSubobject f) h (_ : Factors (kernelSubobject f) h) ≫ arrow (kernelSubobject f) = h
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
W : C
h : W ⟶ X
w : h ≫ f = 0
⊢ (factorThruKernelSubobject f h w ≫ (kernelSubobjectIso f).hom) ≫ kernel.ι f = kernel.lift f h w ≫ kernel.ι f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ (arrow (kernelSubobject f) ≫ sq.left) ≫ f' = 0
[PROOFSTEP]
simp [sq.w]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ kernelSubobjectMap sq ≫ arrow (kernelSubobject f') = arrow (kernelSubobject f) ≫ sq.left
[PROOFSTEP]
simp [kernelSubobjectMap]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
⊢ kernelSubobjectMap (𝟙 (Arrow.mk f)) = 𝟙 (underlying.obj (kernelSubobject f))
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z : C
inst✝³ : HasZeroMorphisms C
f : X ⟶ Y
inst✝² : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝¹ : HasKernel f'
X'' Y'' : C
f'' : X'' ⟶ Y''
inst✝ : HasKernel f''
sq : Arrow.mk f ⟶ Arrow.mk f'
sq' : Arrow.mk f' ⟶ Arrow.mk f''
⊢ kernelSubobjectMap (sq ≫ sq') = kernelSubobjectMap sq ≫ kernelSubobjectMap sq'
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ kernel.map f f' sq.left sq.right (_ : (Arrow.mk f).hom ≫ (𝟭 C).map sq.right = (𝟭 C).map sq.left ≫ (Arrow.mk f').hom) ≫
      (kernelSubobjectIso f').inv =
    (kernelSubobjectIso f).inv ≫ kernelSubobjectMap sq
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
inst✝² : HasZeroMorphisms C
f : X ⟶ Y
inst✝¹ : HasKernel f
X' Y' : C
f' : X' ⟶ Y'
inst✝ : HasKernel f'
sq : Arrow.mk f ⟶ Arrow.mk f'
⊢ (kernelSubobjectIso f).hom ≫
      kernel.map f f' sq.left sq.right
        (_ : (Arrow.mk f).hom ≫ (𝟭 C).map sq.right = (𝟭 C).map sq.left ≫ (Arrow.mk f').hom) =
    kernelSubobjectMap sq ≫ (kernelSubobjectIso f').hom
[PROOFSTEP]
simp [← Iso.comp_inv_eq, kernel_map_comp_kernelSubobjectIso_inv]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
A B : C
⊢ IsIso (kernel.ι 0)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
inst✝¹ : HasZeroMorphisms C
f : X ⟶ Y
inst✝ : HasKernel f
A : Subobject X
h : arrow A ≫ f = 0
⊢ kernel.lift f (arrow A) h ≫ kernel.ι f = arrow A
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
X' : C
f : X' ⟶ X
inst✝¹ : IsIso f
g : X ⟶ Y
inst✝ : HasKernel g
⊢ (kernelSubobjectIsoComp f g).hom ≫ arrow (kernelSubobject g) = arrow (kernelSubobject (f ≫ g)) ≫ f
[PROOFSTEP]
simp [kernelSubobjectIsoComp]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
X' : C
f : X' ⟶ X
inst✝¹ : IsIso f
g : X ⟶ Y
inst✝ : HasKernel g
⊢ (kernelSubobjectIsoComp f g).inv ≫ arrow (kernelSubobject (f ≫ g)) = arrow (kernelSubobject g) ≫ inv f
[PROOFSTEP]
simp [kernelSubobjectIsoComp]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z✝ : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : HasKernel (f ≫ h)
⊢ arrow (kernelSubobject f) ≫ f ≫ h = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z✝ : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ (arrow (kernelSubobject (f ≫ h)) ≫ f) ≫ h = 0 ≫ h
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z✝ : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ IsIso (ofLE (kernelSubobject f) (kernelSubobject (f ≫ h)) (_ : kernelSubobject f ≤ kernelSubobject (f ≫ h)))
[PROOFSTEP]
rw [ofLE_mk_le_mk_of_comm (kernelCompMono f h).inv]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z✝ : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ IsIso ((underlyingIso (kernel.ι f)).hom ≫ (kernelCompMono f h).inv ≫ (underlyingIso (kernel.ι (f ≫ h))).inv)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z✝ : C
inst✝³ : HasZeroMorphisms C
f✝ : X ⟶ Y
inst✝² : HasKernel f✝
f : X ⟶ Y
inst✝¹ : HasKernel f
Z : C
h : Y ⟶ Z
inst✝ : Mono h
⊢ (kernelCompMono f h).inv ≫ kernel.ι (f ≫ h) = kernel.ι f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasCokernels C
X : C
⊢ ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g] (i : A ≅ B),
    i.hom ≫ g = f →
      (fun A f x => Subobject.mk (cokernel.π f).op) A f inst = (fun A f x => Subobject.mk (cokernel.π f).op) B g inst_1
[PROOFSTEP]
rintro A B f g hf hg i rfl
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasCokernels C
X A B : C
g : B ⟶ X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ (fun A f x => Subobject.mk (cokernel.π f).op) A (i.hom ≫ g) hf = (fun A f x => Subobject.mk (cokernel.π f).op) B g hg
[PROOFSTEP]
refine' Subobject.mk_eq_mk_of_comm _ _ (Iso.op _) (Quiver.Hom.unop_inj _)
[GOAL]
case refine'_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasCokernels C
X A B : C
g : B ⟶ X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ cokernel g ≅ cokernel (i.hom ≫ g)
[PROOFSTEP]
exact
  (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) (isCokernelEpiComp (colimit.isColimit _) i.hom rfl)).symm
[GOAL]
case refine'_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasCokernels C
X A B : C
g : B ⟶ X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ ((Iso.op
            (IsColimit.coconePointUniqueUpToIso (colimit.isColimit (parallelPair (i.hom ≫ g) 0))
                (isCokernelEpiComp (colimit.isColimit (parallelPair g 0)) i.hom
                  (_ : i.hom ≫ g = i.hom ≫ g))).symm).hom ≫
        (cokernel.π g).op).unop =
    (cokernel.π (i.hom ≫ g)).op.unop
[PROOFSTEP]
simp only [Iso.comp_inv_eq, Iso.op_hom, Iso.symm_hom, unop_comp, Quiver.Hom.unop_op,
  colimit.comp_coconePointUniqueUpToIso_hom, Cofork.ofπ_ι_app, coequalizer.cofork_π]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasCokernels C
X : C
⊢ ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst : Mono f] [inst_1 : Mono g],
    Subobject.mk f ≤ Subobject.mk g →
      Subobject.lift (fun A f x => Subobject.mk (cokernel.π f).op)
          (_ :
            ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [hf : Mono f] [hg : Mono g] (i : A ≅ B),
              i.hom ≫ g = f →
                (fun A f x => Subobject.mk (cokernel.π f).op) A f hf =
                  (fun A f x => Subobject.mk (cokernel.π f).op) B g hg)
          (Subobject.mk f) ≤
        Subobject.lift (fun A f x => Subobject.mk (cokernel.π f).op)
          (_ :
            ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [hf : Mono f] [hg : Mono g] (i : A ≅ B),
              i.hom ≫ g = f →
                (fun A f x => Subobject.mk (cokernel.π f).op) A f hf =
                  (fun A f x => Subobject.mk (cokernel.π f).op) B g hg)
          (Subobject.mk g)
[PROOFSTEP]
intro A B f g hf hg h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Subobject.lift (fun A f x => Subobject.mk (cokernel.π f).op)
      (_ :
        ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [hf : Mono f] [hg : Mono g] (i : A ≅ B),
          i.hom ≫ g = f →
            (fun A f x => Subobject.mk (cokernel.π f).op) A f hf = (fun A f x => Subobject.mk (cokernel.π f).op) B g hg)
      (Subobject.mk f) ≤
    Subobject.lift (fun A f x => Subobject.mk (cokernel.π f).op)
      (_ :
        ∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [hf : Mono f] [hg : Mono g] (i : A ≅ B),
          i.hom ≫ g = f →
            (fun A f x => Subobject.mk (cokernel.π f).op) A f hf = (fun A f x => Subobject.mk (cokernel.π f).op) B g hg)
      (Subobject.mk g)
[PROOFSTEP]
dsimp only [Subobject.lift_mk]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Subobject.mk (cokernel.π f).op ≤ Subobject.mk (cokernel.π g).op
[PROOFSTEP]
refine' Subobject.mk_le_mk_of_comm (cokernel.desc f (cokernel.π g) _).op _
[GOAL]
case refine'_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ f ≫ cokernel.π g = 0
[PROOFSTEP]
rw [← Subobject.ofMkLEMk_comp h, Category.assoc, cokernel.condition, comp_zero]
[GOAL]
case refine'_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasCokernels C
X A B : C
f : A ⟶ X
g : B ⟶ X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ (cokernel.desc f (cokernel.π g) (_ : f ≫ cokernel.π g = 0)).op ≫ (cokernel.π f).op = (cokernel.π g).op
[PROOFSTEP]
exact Quiver.Hom.unop_inj (cokernel.π_desc _ _ _)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
⊢ ∀ ⦃A B : Cᵒᵖ⦄ (f : A ⟶ op X) (g : B ⟶ op X) [inst : Mono f] [inst_1 : Mono g] (i : A ≅ B),
    i.hom ≫ g = f →
      (fun A f x => Subobject.mk (kernel.ι f.unop)) A f inst = (fun A f x => Subobject.mk (kernel.ι f.unop)) B g inst_1
[PROOFSTEP]
rintro A B f g hf hg i rfl
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ (fun A f x => Subobject.mk (kernel.ι f.unop)) A (i.hom ≫ g) hf = (fun A f x => Subobject.mk (kernel.ι f.unop)) B g hg
[PROOFSTEP]
refine' Subobject.mk_eq_mk_of_comm _ _ _ _
[GOAL]
case refine'_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ kernel (i.hom ≫ g).unop ≅ kernel g.unop
[PROOFSTEP]
exact
  IsLimit.conePointUniqueUpToIso (limit.isLimit _)
    (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.unop.hom rfl)
[GOAL]
case refine'_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ (IsLimit.conePointUniqueUpToIso (limit.isLimit (parallelPair (g.unop ≫ (Iso.unop i).hom) 0))
          (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) (Iso.unop i).hom
            (_ : g.unop ≫ (Iso.unop i).hom = g.unop ≫ (Iso.unop i).hom))).hom ≫
      kernel.ι g.unop =
    kernel.ι (i.hom ≫ g).unop
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
g : B ⟶ op X
hg : Mono g
i : A ≅ B
hf : Mono (i.hom ≫ g)
⊢ (IsLimit.conePointUniqueUpToIso (limit.isLimit (parallelPair (g.unop ≫ i.hom.unop) 0))
          (isKernelCompMono (limit.isLimit (parallelPair g.unop 0)) i.hom.unop
            (_ : g.unop ≫ i.hom.unop = g.unop ≫ i.hom.unop))).hom ≫
      kernel.ι g.unop =
    kernel.ι (g.unop ≫ i.hom.unop)
[PROOFSTEP]
simp only [← Iso.eq_inv_comp, limit.conePointUniqueUpToIso_inv_comp, Fork.ofι_π_app]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f : X✝ ⟶ Y
inst✝¹ : HasKernel f
inst✝ : HasKernels C
X : C
⊢ ∀ ⦃A B : Cᵒᵖ⦄ (f : A ⟶ op X) (g : B ⟶ op X) [inst : Mono f] [inst_1 : Mono g],
    Subobject.mk f ≤ Subobject.mk g →
      Subobject.lift (fun A f x => Subobject.mk (kernel.ι f.unop))
          (_ :
            ∀ ⦃A B : Cᵒᵖ⦄ (f : A ⟶ op X) (g : B ⟶ op X) [hf : Mono f] [hg : Mono g] (i : A ≅ B),
              i.hom ≫ g = f →
                (fun A f x => Subobject.mk (kernel.ι f.unop)) A f hf =
                  (fun A f x => Subobject.mk (kernel.ι f.unop)) B g hg)
          (Subobject.mk f) ≤
        Subobject.lift (fun A f x => Subobject.mk (kernel.ι f.unop))
          (_ :
            ∀ ⦃A B : Cᵒᵖ⦄ (f : A ⟶ op X) (g : B ⟶ op X) [hf : Mono f] [hg : Mono g] (i : A ≅ B),
              i.hom ≫ g = f →
                (fun A f x => Subobject.mk (kernel.ι f.unop)) A f hf =
                  (fun A f x => Subobject.mk (kernel.ι f.unop)) B g hg)
          (Subobject.mk g)
[PROOFSTEP]
intro A B f g hf hg h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Subobject.lift (fun A f x => Subobject.mk (kernel.ι f.unop))
      (_ :
        ∀ ⦃A B : Cᵒᵖ⦄ (f : A ⟶ op X) (g : B ⟶ op X) [hf : Mono f] [hg : Mono g] (i : A ≅ B),
          i.hom ≫ g = f →
            (fun A f x => Subobject.mk (kernel.ι f.unop)) A f hf = (fun A f x => Subobject.mk (kernel.ι f.unop)) B g hg)
      (Subobject.mk f) ≤
    Subobject.lift (fun A f x => Subobject.mk (kernel.ι f.unop))
      (_ :
        ∀ ⦃A B : Cᵒᵖ⦄ (f : A ⟶ op X) (g : B ⟶ op X) [hf : Mono f] [hg : Mono g] (i : A ≅ B),
          i.hom ≫ g = f →
            (fun A f x => Subobject.mk (kernel.ι f.unop)) A f hf = (fun A f x => Subobject.mk (kernel.ι f.unop)) B g hg)
      (Subobject.mk g)
[PROOFSTEP]
dsimp only [Subobject.lift_mk]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ Subobject.mk (kernel.ι f.unop) ≤ Subobject.mk (kernel.ι g.unop)
[PROOFSTEP]
refine' Subobject.mk_le_mk_of_comm (kernel.lift g.unop (kernel.ι f.unop) _) _
[GOAL]
case refine'_1
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ kernel.ι f.unop ≫ g.unop = 0
[PROOFSTEP]
rw [← Subobject.ofMkLEMk_comp h, unop_comp, kernel.condition_assoc, zero_comp]
[GOAL]
case refine'_2
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ kernel.lift g.unop (kernel.ι f.unop) (_ : kernel.ι f.unop ≫ g.unop = 0) ≫ kernel.ι g.unop = kernel.ι f.unop
[PROOFSTEP]
exact Quiver.Hom.op_inj (by simp)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
inst✝² : HasZeroMorphisms C
f✝ : X✝ ⟶ Y
inst✝¹ : HasKernel f✝
inst✝ : HasKernels C
X : C
A B : Cᵒᵖ
f : A ⟶ op X
g : B ⟶ op X
hf : Mono f
hg : Mono g
h : Subobject.mk f ≤ Subobject.mk g
⊢ (kernel.lift g.unop (kernel.ι f.unop) (_ : kernel.ι f.unop ≫ g.unop = 0) ≫ kernel.ι g.unop).op = (kernel.ι f.unop).op
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : HasImage f
⊢ (imageSubobjectIso f).hom ≫ image.ι f = arrow (imageSubobject f)
[PROOFSTEP]
simp [imageSubobjectIso]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : HasImage f
⊢ (imageSubobjectIso f).inv ≫ arrow (imageSubobject f) = image.ι f
[PROOFSTEP]
simp [imageSubobjectIso]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasEqualizers C
⊢ Epi (factorThruImageSubobject f)
[PROOFSTEP]
dsimp [factorThruImageSubobject]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasEqualizers C
⊢ Epi (factorThruImage f ≫ (imageSubobjectIso f).inv)
[PROOFSTEP]
apply epi_comp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : HasImage f
⊢ factorThruImageSubobject f ≫ arrow (imageSubobject f) = f
[PROOFSTEP]
simp [factorThruImageSubobject, imageSubobject_arrow]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
inst✝³ : HasImage f✝
inst✝² : HasZeroMorphisms C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : HasImage f
inst✝ : Epi (factorThruImageSubobject f)
h : f ≫ g = 0
⊢ factorThruImageSubobject f ≫ arrow (imageSubobject f) ≫ g = 0
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : HasImage f
W : C
k : W ⟶ X
⊢ (k ≫ factorThruImage f) ≫ MonoOver.arrow (MonoOver.mk' (image.ι f)) = k ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : HasImage f
W : C
k : W ⟶ X
h : Factors (imageSubobject f) (k ≫ f)
⊢ factorThru (imageSubobject f) (k ≫ f) h = k ≫ factorThruImageSubobject f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : HasImage f
W : C
k : W ⟶ X
h : Factors (imageSubobject f) (k ≫ f)
⊢ factorThru (imageSubobject f) (k ≫ f) h ≫ arrow (imageSubobject f) =
    (k ≫ factorThruImageSubobject f) ≫ arrow (imageSubobject f)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : HasImage f
W W' : C
k : W ⟶ W'
k' : W' ⟶ X
h : Factors (imageSubobject f) (k ≫ k' ≫ f)
⊢ factorThru (imageSubobject f) (k ≫ k' ≫ f) h = k ≫ k' ≫ factorThruImageSubobject f
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝ : HasImage f
W W' : C
k : W ⟶ W'
k' : W' ⟶ X
h : Factors (imageSubobject f) (k ≫ k' ≫ f)
⊢ factorThru (imageSubobject f) (k ≫ k' ≫ f) h ≫ arrow (imageSubobject f) =
    (k ≫ k' ≫ factorThruImageSubobject f) ≫ arrow (imageSubobject f)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
inst✝² : HasImage f✝
X' : C
h : X' ⟶ X
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage (h ≫ f)
⊢ image.preComp h f ≫ image.ι f = image.ι (h ≫ f)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ arrow (imageSubobject 0) = 0
[PROOFSTEP]
rw [← imageSubobject_arrow]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
⊢ (imageSubobjectIso 0).hom ≫ image.ι 0 = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
A B : C
⊢ (imageSubobjectIso 0 ≪≫ imageZero ≪≫ botCoeIsoZero.symm).hom ≫ arrow ⊥ = arrow (imageSubobject 0)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
inst✝⁴ : HasImage f✝
inst✝³ : HasEqualizers C
X' : C
h : X' ⟶ X
inst✝² : Epi h
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage (h ≫ f)
⊢ Epi (ofLE (imageSubobject (h ≫ f)) (imageSubobject f) (_ : imageSubobject (h ≫ f) ≤ imageSubobject f))
[PROOFSTEP]
rw [ofLE_mk_le_mk_of_comm (image.preComp h f)]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
inst✝⁴ : HasImage f✝
inst✝³ : HasEqualizers C
X' : C
h : X' ⟶ X
inst✝² : Epi h
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage (h ≫ f)
⊢ Epi ((underlyingIso (image.ι (h ≫ f))).hom ≫ image.preComp h f ≫ (underlyingIso (image.ι f)).inv)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
inst✝⁴ : HasImage f✝
inst✝³ : HasEqualizers C
X' : C
h : X' ⟶ X
inst✝² : Epi h
f : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage (h ≫ f)
⊢ image.preComp h f ≫ image.ι f = image.ι (h ≫ f)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
inst✝³ : HasImage f✝
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : HasImage f
Y' : C
h : Y ⟶ Y'
inst✝ : IsIso h
⊢ (imageSubobjectCompIso f h).hom ≫ arrow (imageSubobject f) = arrow (imageSubobject (f ≫ h)) ≫ inv h
[PROOFSTEP]
simp [imageSubobjectCompIso]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
inst✝³ : HasImage f✝
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : HasImage f
Y' : C
h : Y ⟶ Y'
inst✝ : IsIso h
⊢ (imageSubobjectCompIso f h).inv ≫ arrow (imageSubobject (f ≫ h)) = arrow (imageSubobject f) ≫ h
[PROOFSTEP]
simp [imageSubobjectCompIso]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
inst✝¹ : HasImage f✝
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageSubobjectIso f ≪≫ imageMonoIsoSource f ≪≫ (underlyingIso f).symm).hom ≫ arrow (Subobject.mk f) =
    arrow (imageSubobject f)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y Z : C
f✝ : X ⟶ Y
inst✝³ : HasImage f✝
inst✝² : HasEqualizers C
X' : C
h : X' ⟶ X
inst✝¹ : IsIso h
f : X ⟶ Y
inst✝ : HasImage f
⊢ inv (image.preComp h f) ≫ image.ι (h ≫ f) = image.ι f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X✝ Y Z : C
f✝ : X✝ ⟶ Y
inst✝¹ : HasImage f✝
A B : C
X : Subobject B
f : A ⟶ B
inst✝ : HasImage f
h : A ⟶ underlying.obj X
w : h ≫ arrow X = f
⊢ ((imageSubobjectIso f).hom ≫ image.lift (MonoFactorisation.mk (underlying.obj X) (arrow X) h)) ≫ arrow X =
    arrow (imageSubobject f)
[PROOFSTEP]
rw [assoc, image.lift_fac, imageSubobject_arrow]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y Z : C
f✝ : X✝ ⟶ Y
inst✝² : HasImage f✝
A B X : C
g : X ⟶ B
inst✝¹ : Mono g
f : A ⟶ B
inst✝ : HasImage f
h : A ⟶ X
w : h ≫ g = f
⊢ (h ≫ (underlyingIso g).inv) ≫ arrow (Subobject.mk g) = f
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
inst✝³ : HasImage f✝
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ imageSubobjectMap sq ≫ arrow (imageSubobject g) = arrow (imageSubobject f) ≫ sq.right
[PROOFSTEP]
simp only [imageSubobjectMap, Category.assoc, imageSubobject_arrow']
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
inst✝³ : HasImage f✝
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (imageSubobjectIso f).hom ≫ image.map sq ≫ image.ι g = arrow (imageSubobject f) ≫ sq.right
[PROOFSTEP]
erw [image.map_ι, ← Category.assoc, imageSubobject_arrow]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
inst✝³ : HasImage f✝
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ image.map sq ≫ (imageSubobjectIso (Arrow.mk g).hom).inv = (imageSubobjectIso f).inv ≫ imageSubobjectMap sq
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u
inst✝⁴ : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
inst✝³ : HasImage f✝
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (image.map sq ≫ (imageSubobjectIso (Arrow.mk g).hom).inv) ≫ arrow (imageSubobject (Arrow.mk g).hom) =
    ((imageSubobjectIso f).inv ≫ imageSubobjectMap sq) ≫ arrow (imageSubobject (Arrow.mk g).hom)
[PROOFSTEP]
simpa using image.map_ι sq
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X✝ Y✝ Z✝ : C
f✝ : X✝ ⟶ Y✝
inst✝³ : HasImage f✝
W X Y Z : C
f : W ⟶ X
inst✝² : HasImage f
g : Y ⟶ Z
inst✝¹ : HasImage g
sq : Arrow.mk f ⟶ Arrow.mk g
inst✝ : HasImageMap sq
⊢ (imageSubobjectIso (Arrow.mk f).hom).hom ≫ image.map sq = imageSubobjectMap sq ≫ (imageSubobjectIso g).hom
[PROOFSTEP]
erw [← Iso.comp_inv_eq, Category.assoc, ← (imageSubobjectIso f).eq_inv_comp, image_map_comp_imageSubobjectIso_inv sq]


[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : ((cocones J D).obj (op (K ⋙ F))).obj Y
j j' : J
f : j ⟶ j'
⊢ (op (op K).unop).unop.map f ≫ (fun j => ↑(homEquiv adj (K.obj j) Y) (NatTrans.app t j)) j' =
    (fun j => ↑(homEquiv adj (K.obj j) Y) (NatTrans.app t j)) j ≫ ((const J).obj (G.obj Y)).map f
[PROOFSTEP]
erw [← adj.homEquiv_naturality_left, t.naturality]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : ((cocones J D).obj (op (K ⋙ F))).obj Y
j j' : J
f : j ⟶ j'
⊢ ↑(homEquiv adj ((op (op K).unop).unop.obj j) Y) (NatTrans.app t j ≫ ((const J).obj Y).map f) =
    (fun j => ↑(homEquiv adj (K.obj j) Y) (NatTrans.app t j)) j ≫ ((const J).obj (G.obj Y)).map f
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : ((cocones J D).obj (op (K ⋙ F))).obj Y
j j' : J
f : j ⟶ j'
⊢ ↑(homEquiv adj (K.obj j) Y) (NatTrans.app t j ≫ 𝟙 Y) = ↑(homEquiv adj (K.obj j) Y) (NatTrans.app t j) ≫ 𝟙 (G.obj Y)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : (G ⋙ (cocones J C).obj (op K)).obj Y
j j' : J
f : j ⟶ j'
⊢ (op (op (K ⋙ F)).unop).unop.map f ≫ (fun j => ↑(homEquiv adj (K.obj j) Y).symm (NatTrans.app t j)) j' =
    (fun j => ↑(homEquiv adj (K.obj j) Y).symm (NatTrans.app t j)) j ≫ ((const J).obj Y).map f
[PROOFSTEP]
erw [← adj.homEquiv_naturality_left_symm, ← adj.homEquiv_naturality_right_symm, t.naturality]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : (G ⋙ (cocones J C).obj (op K)).obj Y
j j' : J
f : j ⟶ j'
⊢ ↑(homEquiv adj (K.obj j) (((const J).obj Y).obj j')).symm (NatTrans.app t j ≫ ((const J).obj (G.obj Y)).map f) =
    ↑(homEquiv adj (K.obj j) (((const J).obj Y).obj j')).symm (NatTrans.app t j ≫ G.map (((const J).obj Y).map f))
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ C
Y : D
t : (G ⋙ (cocones J C).obj (op K)).obj Y
j j' : J
f : j ⟶ j'
⊢ ↑(homEquiv adj (K.obj j) Y).symm (NatTrans.app t j ≫ 𝟙 (G.obj Y)) =
    ↑(homEquiv adj (K.obj j) Y).symm (NatTrans.app t j ≫ G.map (𝟙 Y))
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : (F.op ⋙ (cones J D).obj K).obj X
j j' : J
f : j ⟶ j'
⊢ ((const J).op.obj X).unop.map f ≫ (fun j => ↑(homEquiv adj X.unop (K.obj j)) (NatTrans.app t j)) j' =
    (fun j => ↑(homEquiv adj X.unop (K.obj j)) (NatTrans.app t j)) j ≫ (K ⋙ G).map f
[PROOFSTEP]
erw [← adj.homEquiv_naturality_right, ← t.naturality, Category.id_comp, Category.id_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : (F.op ⋙ (cones J D).obj K).obj X
j j' : J
f : j ⟶ j'
⊢ (fun j => ↑(homEquiv adj X.unop (K.obj j)) (NatTrans.app t j)) j' =
    ↑(homEquiv adj (((const J).op.obj X).unop.obj j) (K.obj j')) (NatTrans.app t j')
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
J : Type u
inst✝ : Category.{v, u} J
K : J ⥤ D
X : Cᵒᵖ
t : ((cones J C).obj (K ⋙ G)).obj X
j j' : J
f : j ⟶ j'
⊢ ((const J).op.obj (F.op.obj X)).unop.map f ≫ (fun j => ↑(homEquiv adj X.unop (K.obj j)).symm (NatTrans.app t j)) j' =
    (fun j => ↑(homEquiv adj X.unop (K.obj j)).symm (NatTrans.app t j)) j ≫ K.map f
[PROOFSTEP]
erw [← adj.homEquiv_naturality_right_symm, ← t.naturality, Category.id_comp, Category.id_comp]


[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.65, u_1} C
inst✝¹ : Category.{?u.69, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.118, u_3} E
h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ
F : Cᵒᵖ ⥤ E
hF : MorphismProperty.IsInvertedBy (MorphismProperty.op W) F
⊢ L.op ⋙ (fun F hF => (lift h F.rightOp (_ : MorphismProperty.IsInvertedBy W F.rightOp)).leftOp) F hF = F
[PROOFSTEP]
convert congr_arg Functor.leftOp (h.fac F.rightOp hF.rightOp)
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.65, u_1} C
inst✝¹ : Category.{?u.69, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.118, u_3} E
h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ
F₁ F₂ : Dᵒᵖ ⥤ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
⊢ F₁ = F₂
[PROOFSTEP]
suffices F₁.rightOp = F₂.rightOp by rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.65, u_1} C
inst✝¹ : Category.{?u.69, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.118, u_3} E
h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ
F₁ F₂ : Dᵒᵖ ⥤ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
this : F₁.rightOp = F₂.rightOp
⊢ F₁ = F₂
[PROOFSTEP]
rw [← F₁.rightOp_leftOp_eq, ← F₂.rightOp_leftOp_eq, this]
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.65, u_1} C
inst✝¹ : Category.{?u.69, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.118, u_3} E
h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ
F₁ F₂ : Dᵒᵖ ⥤ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
⊢ F₁.rightOp = F₂.rightOp
[PROOFSTEP]
have eq' := congr_arg Functor.rightOp eq
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{?u.65, u_1} C
inst✝¹ : Category.{?u.69, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝ : Category.{?u.118, u_3} E
h : StrictUniversalPropertyFixedTarget L W Eᵒᵖ
F₁ F₂ : Dᵒᵖ ⥤ E
eq : L.op ⋙ F₁ = L.op ⋙ F₂
eq' : (L.op ⋙ F₁).rightOp = (L.op ⋙ F₂).rightOp
⊢ F₁.rightOp = F₂.rightOp
[PROOFSTEP]
exact h.uniq _ _ eq'


[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁸ : Category.{u_1, u_1} C₁
inst✝⁷ : Category.{u_2, u_2} C₂
inst✝⁶ : Category.{?u.6190, u_3} D
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ (equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X) =
    (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).app X ≪≫ β.app X
[PROOFSTEP]
ext
[GOAL]
case w
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁸ : Category.{u_1, u_1} C₁
inst✝⁷ : Category.{u_2, u_2} C₂
inst✝⁶ : Category.{?u.6190, u_3} D
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ ((equivalence L₁ W₁ L₂ W₂ G G' F F' α β).counitIso.app (L₂.obj X)).hom =
    ((Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).app X ≪≫ β.app X).hom
[PROOFSTEP]
dsimp [equivalence, Equivalence.mk]
[GOAL]
case w
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁸ : Category.{u_1, u_1} C₁
inst✝⁷ : Category.{u_2, u_2} C₂
inst✝⁶ : Category.{?u.6190, u_3} D
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ NatTrans.app (liftNatTrans L₂ W₂ (F ⋙ G') L₂ (F' ⋙ G') (𝟭 D₂) β.hom) (L₂.obj X) =
    NatTrans.app (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom X ≫ NatTrans.app β.hom X
[PROOFSTEP]
rw [liftNatTrans_app]
[GOAL]
case w
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁸ : Category.{u_1, u_1} C₁
inst✝⁷ : Category.{u_2, u_2} C₂
inst✝⁶ : Category.{?u.6190, u_3} D
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ NatTrans.app (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom X ≫
      NatTrans.app β.hom X ≫ NatTrans.app (Lifting.iso L₂ W₂ L₂ (𝟭 D₂)).inv X =
    NatTrans.app (Lifting.iso L₂ W₂ (F ⋙ G') (F' ⋙ G')).hom X ≫ NatTrans.app β.hom X
[PROOFSTEP]
dsimp [Lifting.iso]
[GOAL]
case w
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁸ : Category.{u_1, u_1} C₁
inst✝⁷ : Category.{u_2, u_2} C₂
inst✝⁶ : Category.{?u.6190, u_3} D
inst✝⁵ : Category.{u_7, u_4} D₁
inst✝⁴ : Category.{u_6, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G : C₁ ⥤ D₂
G' : D₁ ⥤ D₂
inst✝¹ : Lifting L₁ W₁ G G'
F : C₂ ⥤ D₁
F' : D₂ ⥤ D₁
inst✝ : Lifting L₂ W₂ F F'
α : G ⋙ F' ≅ L₁
β : F ⋙ G' ≅ L₂
X : C₂
⊢ G'.map (NatTrans.app (Lifting.iso' W₂).hom X) ≫ NatTrans.app β.hom X ≫ 𝟙 (L₂.obj X) =
    G'.map (NatTrans.app (Lifting.iso' W₂).hom X) ≫ NatTrans.app β.hom X
[PROOFSTEP]
rw [comp_id]
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{u_1, u_1} C₁
inst✝⁴ : Category.{u_2, u_2} C₂
inst✝³ : Category.{u_6, u_3} D
inst✝² : Category.{?u.15305, u_4} D₁
inst✝¹ : Category.{?u.15309, u_5} D₂
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
inst✝ : IsLocalization L₁ W₁
iso : E.functor ⋙ L₂ ≅ L₁
⊢ IsLocalization L₂ W₂
[PROOFSTEP]
have h : W₁.IsInvertedBy (E.functor ⋙ W₂.Q) := fun _ _ f hf =>
  by
  obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf
  exact
    ((MorphismProperty.RespectsIso.isomorphisms _).arrow_mk_iso_iff (W₂.Q.mapArrow.mapIso e)).1
      (Localization.inverts W₂.Q W₂ _ hf')
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{u_1, u_1} C₁
inst✝⁴ : Category.{u_2, u_2} C₂
inst✝³ : Category.{u_6, u_3} D
inst✝² : Category.{?u.15305, u_4} D₁
inst✝¹ : Category.{?u.15309, u_5} D₂
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
inst✝ : IsLocalization L₁ W₁
iso : E.functor ⋙ L₂ ≅ L₁
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
⊢ IsIso ((E.functor ⋙ MorphismProperty.Q W₂).map f)
[PROOFSTEP]
obtain ⟨_, _, f', hf', ⟨e⟩⟩ := hW₁ f hf
[GOAL]
case intro.intro.intro.intro.intro
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{u_1, u_1} C₁
inst✝⁴ : Category.{u_2, u_2} C₂
inst✝³ : Category.{u_6, u_3} D
inst✝² : Category.{?u.15305, u_4} D₁
inst✝¹ : Category.{?u.15309, u_5} D₂
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
inst✝ : IsLocalization L₁ W₁
iso : E.functor ⋙ L₂ ≅ L₁
x✝¹ x✝ : C₁
f : x✝¹ ⟶ x✝
hf : W₁ f
w✝¹ w✝ : C₂
f' : w✝¹ ⟶ w✝
hf' : W₂ f'
e : Arrow.mk f' ≅ Arrow.mk (E.functor.map f)
⊢ IsIso ((E.functor ⋙ MorphismProperty.Q W₂).map f)
[PROOFSTEP]
exact
  ((MorphismProperty.RespectsIso.isomorphisms _).arrow_mk_iso_iff (W₂.Q.mapArrow.mapIso e)).1
    (Localization.inverts W₂.Q W₂ _ hf')
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{u_1, u_1} C₁
inst✝⁴ : Category.{u_2, u_2} C₂
inst✝³ : Category.{u_6, u_3} D
inst✝² : Category.{?u.15305, u_4} D₁
inst✝¹ : Category.{?u.15309, u_5} D₂
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
inst✝ : IsLocalization L₁ W₁
iso : E.functor ⋙ L₂ ≅ L₁
h : MorphismProperty.IsInvertedBy W₁ (E.functor ⋙ MorphismProperty.Q W₂)
⊢ IsLocalization L₂ W₂
[PROOFSTEP]
exact
  { inverts := hW₂
    nonempty_isEquivalence :=
      ⟨Localization.isEquivalence W₂.Q W₂ L₁ W₁ L₂ (Construction.lift L₂ hW₂) (E.functor ⋙ W₂.Q)
          (Localization.lift (E.functor ⋙ W₂.Q) h L₁)
          (by
            calc
              L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ ≅ _ := (leftUnitor _).symm
              _ ≅ _ := (isoWhiskerRight E.counitIso.symm _)
              _ ≅ E.inverse ⋙ E.functor ⋙ L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ := (Functor.associator _ _ _)
              _ ≅ E.inverse ⋙ L₁ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
                (isoWhiskerLeft E.inverse ((Functor.associator _ _ _).symm ≪≫ isoWhiskerRight iso _))
              _ ≅ E.inverse ⋙ E.functor ⋙ W₂.Q := (isoWhiskerLeft _ (Localization.fac (E.functor ⋙ W₂.Q) h L₁))
              _ ≅ (E.inverse ⋙ E.functor) ⋙ W₂.Q := (Functor.associator _ _ _).symm
              _ ≅ 𝟭 C₂ ⋙ W₂.Q := (isoWhiskerRight E.counitIso _)
              _ ≅ W₂.Q := leftUnitor _)
          (Functor.associator _ _ _ ≪≫ isoWhiskerLeft _ (Lifting.iso W₂.Q W₂ _ _) ≪≫ iso)⟩ }
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁵ : Category.{u_1, u_1} C₁
inst✝⁴ : Category.{u_2, u_2} C₂
inst✝³ : Category.{u_6, u_3} D
inst✝² : Category.{?u.15305, u_4} D₁
inst✝¹ : Category.{?u.15309, u_5} D₂
L₁ : C₁ ⥤ D
W₁ : MorphismProperty C₁
L₂ : C₂ ⥤ D
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
inst✝ : IsLocalization L₁ W₁
iso : E.functor ⋙ L₂ ≅ L₁
h : MorphismProperty.IsInvertedBy W₁ (E.functor ⋙ MorphismProperty.Q W₂)
⊢ L₂ ⋙ lift (E.functor ⋙ MorphismProperty.Q W₂) h L₁ ≅ MorphismProperty.Q W₂
[PROOFSTEP]
calc
  L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ ≅ _ := (leftUnitor _).symm
  _ ≅ _ := (isoWhiskerRight E.counitIso.symm _)
  _ ≅ E.inverse ⋙ E.functor ⋙ L₂ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ := (Functor.associator _ _ _)
  _ ≅ E.inverse ⋙ L₁ ⋙ lift (E.functor ⋙ W₂.Q) h L₁ :=
    (isoWhiskerLeft E.inverse ((Functor.associator _ _ _).symm ≪≫ isoWhiskerRight iso _))
  _ ≅ E.inverse ⋙ E.functor ⋙ W₂.Q := (isoWhiskerLeft _ (Localization.fac (E.functor ⋙ W₂.Q) h L₁))
  _ ≅ (E.inverse ⋙ E.functor) ⋙ W₂.Q := (Functor.associator _ _ _).symm
  _ ≅ 𝟭 C₂ ⋙ W₂.Q := (isoWhiskerRight E.counitIso _)
  _ ≅ W₂.Q := leftUnitor _
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁶ : Category.{u_1, u_1} C₁
inst✝⁵ : Category.{u_2, u_2} C₂
inst✝⁴ : Category.{?u.32200, u_3} D
inst✝³ : Category.{u_6, u_4} D₁
inst✝² : Category.{u_7, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝¹ : IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
E' : D₁ ≌ D₂
inst✝ : CatCommSq E.functor L₁ L₂ E'.functor
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
⊢ IsLocalization L₂ W₂
[PROOFSTEP]
haveI : (E.functor ⋙ L₂).IsLocalization W₁ := of_equivalence_target L₁ W₁ _ E' ((CatCommSq.iso _ _ _ _).symm)
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D : Type u_3
D₁ : Type u_4
D₂ : Type u_5
inst✝⁶ : Category.{u_1, u_1} C₁
inst✝⁵ : Category.{u_2, u_2} C₂
inst✝⁴ : Category.{?u.32200, u_3} D
inst✝³ : Category.{u_6, u_4} D₁
inst✝² : Category.{u_7, u_5} D₂
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝¹ : IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
E : C₁ ≌ C₂
E' : D₁ ≌ D₂
inst✝ : CatCommSq E.functor L₁ L₂ E'.functor
hW₁ : W₁ ⊆ MorphismProperty.inverseImage (MorphismProperty.isoClosure W₂) E.functor
hW₂ : MorphismProperty.IsInvertedBy W₂ L₂
this : IsLocalization (E.functor ⋙ L₂) W₁
⊢ IsLocalization L₂ W₂
[PROOFSTEP]
exact of_equivalence_source (E.functor ⋙ L₂) W₁ L₂ W₂ E hW₁ hW₂ (Iso.refl _)


[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A : Mon_ C
M : Mod_ A
⊢ (𝟙 A.X ⊗ M.act) ≫ M.act = (α_ A.X A.X M.X).inv ≫ (A.mul ⊗ 𝟙 M.X) ≫ M.act
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A : Mon_ C
M✝ M : Mod_ A
⊢ (𝟙 M).hom = 𝟙 M.X
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.one ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act = (λ_ M.X).hom
[PROOFSTEP]
slice_lhs 1 2 => rw [← comp_tensor_id]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (A.one ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (A.one ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (A.one ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.one ≫ f.hom ⊗ 𝟙 M.X) ≫ M.act = (λ_ M.X).hom
[PROOFSTEP]
rw [f.one_hom, one_act]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    (α_ A.X A.X M.X).hom ≫ (𝟙 A.X ⊗ (f.hom ⊗ 𝟙 M.X) ≫ M.act) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act
[PROOFSTEP]
slice_rhs 2 3 => rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 A.X ⊗ (f.hom ⊗ 𝟙 M.X) ≫ M.act) ≫ (f.hom ⊗ 𝟙 M.X)
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
[PROOFSTEP]
rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 A.X ⊗ (f.hom ⊗ 𝟙 M.X) ≫ M.act) ≫ (f.hom ⊗ 𝟙 M.X)
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
[PROOFSTEP]
rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 A.X ⊗ (f.hom ⊗ 𝟙 M.X) ≫ M.act) ≫ (f.hom ⊗ 𝟙 M.X)
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
[PROOFSTEP]
rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    (α_ A.X A.X M.X).hom ≫ ((f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (𝟙 B.X ⊗ (f.hom ⊗ 𝟙 M.X) ≫ M.act)) ≫ M.act
[PROOFSTEP]
rw [id_tensor_comp]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    (α_ A.X A.X M.X).hom ≫ ((f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X) ≫ (𝟙 B.X ⊗ M.act)) ≫ M.act
[PROOFSTEP]
slice_rhs 4 5 => rw [Mod_.assoc_flip]
[GOAL]
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ M.act) ≫ M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| f.hom ⊗ 𝟙 (A.X ⊗ M.X)
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| 𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X
[PROOFSTEP]
rw [Mod_.assoc_flip]
[GOAL]
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ M.act) ≫ M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| f.hom ⊗ 𝟙 (A.X ⊗ M.X)
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| 𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X
[PROOFSTEP]
rw [Mod_.assoc_flip]
[GOAL]
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ M.act) ≫ M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| f.hom ⊗ 𝟙 (A.X ⊗ M.X)
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| 𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X
[PROOFSTEP]
rw [Mod_.assoc_flip]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    (α_ A.X A.X M.X).hom ≫
      (f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X) ≫ (α_ B.X B.X M.X).inv ≫ (B.mul ⊗ 𝟙 M.X) ≫ M.act
[PROOFSTEP]
slice_rhs 3 4 => rw [associator_inv_naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X) ≫ (α_ B.X B.X M.X).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| f.hom ⊗ 𝟙 (A.X ⊗ M.X)
[PROOFSTEP]
rw [associator_inv_naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X) ≫ (α_ B.X B.X M.X).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| f.hom ⊗ 𝟙 (A.X ⊗ M.X)
[PROOFSTEP]
rw [associator_inv_naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom ⊗ 𝟙 M.X) ≫ (α_ B.X B.X M.X).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| f.hom ⊗ 𝟙 (A.X ⊗ M.X)
[PROOFSTEP]
rw [associator_inv_naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    (α_ A.X A.X M.X).hom ≫
      (f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (((α_ B.X A.X M.X).inv ≫ ((𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X)) ≫ (B.mul ⊗ 𝟙 M.X)) ≫ M.act
[PROOFSTEP]
slice_rhs 2 3 => rw [← tensor_id, associator_inv_naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (α_ B.X A.X M.X).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
[PROOFSTEP]
rw [← tensor_id, associator_inv_naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (α_ B.X A.X M.X).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
[PROOFSTEP]
rw [← tensor_id, associator_inv_naturality]
[GOAL]
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (f.hom ⊗ 𝟙 (A.X ⊗ M.X)) ≫ (α_ B.X A.X M.X).inv
case a.a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom
[PROOFSTEP]
rw [← tensor_id, associator_inv_naturality]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    (α_ A.X A.X M.X).hom ≫
      ((((α_ A.X A.X M.X).inv ≫ ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X)) ≫ ((𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X)) ≫ (B.mul ⊗ 𝟙 M.X)) ≫ M.act
[PROOFSTEP]
slice_rhs 1 3 => rw [Iso.hom_inv_id_assoc]
[GOAL]
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom ≫ (α_ A.X A.X M.X).inv ≫ ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X)
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [Iso.hom_inv_id_assoc]
[GOAL]
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom ≫ (α_ A.X A.X M.X).inv ≫ ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X)
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [Iso.hom_inv_id_assoc]
[GOAL]
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (α_ A.X A.X M.X).hom ≫ (α_ A.X A.X M.X).inv ≫ ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X)
case a.a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| (𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [Iso.hom_inv_id_assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act =
    ((((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X) ≫ ((𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X)) ≫ (B.mul ⊗ 𝟙 M.X)) ≫ M.act
[PROOFSTEP]
slice_rhs 1 2 => rw [← comp_tensor_id, tensor_id_comp_id_tensor]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X) ≫ ((𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X)
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id, tensor_id_comp_id_tensor]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X) ≫ ((𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X)
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id, tensor_id_comp_id_tensor]
[GOAL]
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| ((f.hom ⊗ 𝟙 A.X) ⊗ 𝟙 M.X) ≫ ((𝟙 B.X ⊗ f.hom) ⊗ 𝟙 M.X)
case a.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| B.mul ⊗ 𝟙 M.X
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id, tensor_id_comp_id_tensor]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act = (((f.hom ⊗ f.hom) ⊗ 𝟙 M.X) ≫ (B.mul ⊗ 𝟙 M.X)) ≫ M.act
[PROOFSTEP]
slice_rhs 1 2 => rw [← comp_tensor_id, ← f.mul_hom]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| ((f.hom ⊗ f.hom) ⊗ 𝟙 M.X) ≫ (B.mul ⊗ 𝟙 M.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id, ← f.mul_hom]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| ((f.hom ⊗ f.hom) ⊗ 𝟙 M.X) ≫ (B.mul ⊗ 𝟙 M.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id, ← f.mul_hom]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| ((f.hom ⊗ f.hom) ⊗ 𝟙 M.X) ≫ (B.mul ⊗ 𝟙 M.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
| M.act
[PROOFSTEP]
rw [← comp_tensor_id, ← f.mul_hom]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M✝ : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
M : Mod_ B
⊢ (A.mul ⊗ 𝟙 M.X) ≫ (f.hom ⊗ 𝟙 M.X) ≫ M.act = (A.mul ≫ f.hom ⊗ 𝟙 M.X) ≫ M.act
[PROOFSTEP]
rw [comp_tensor_id, Category.assoc]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
⊢ ((fun M => mk M.X ((f.hom ⊗ 𝟙 M.X) ≫ M.act)) X✝).act ≫ g.hom =
    (𝟙 A.X ⊗ g.hom) ≫ ((fun M => mk M.X ((f.hom ⊗ 𝟙 M.X) ≫ M.act)) Y✝).act
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
⊢ ((f.hom ⊗ 𝟙 X✝.X) ≫ X✝.act) ≫ g.hom = (𝟙 A.X ⊗ g.hom) ≫ (f.hom ⊗ 𝟙 Y✝.X) ≫ Y✝.act
[PROOFSTEP]
slice_rhs 1 2 => rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| (𝟙 A.X ⊗ g.hom) ≫ (f.hom ⊗ 𝟙 Y✝.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| Y✝.act
[PROOFSTEP]
rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| (𝟙 A.X ⊗ g.hom) ≫ (f.hom ⊗ 𝟙 Y✝.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| Y✝.act
[PROOFSTEP]
rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| (𝟙 A.X ⊗ g.hom) ≫ (f.hom ⊗ 𝟙 Y✝.X)
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| Y✝.act
[PROOFSTEP]
rw [id_tensor_comp_tensor_id, ← tensor_id_comp_id_tensor]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
⊢ ((f.hom ⊗ 𝟙 X✝.X) ≫ X✝.act) ≫ g.hom = ((f.hom ⊗ 𝟙 X✝.X) ≫ (𝟙 B.X ⊗ g.hom)) ≫ Y✝.act
[PROOFSTEP]
slice_rhs 2 3 => rw [← g.act_hom]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| (𝟙 B.X ⊗ g.hom) ≫ Y✝.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| f.hom ⊗ 𝟙 X✝.X
[PROOFSTEP]
rw [← g.act_hom]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| (𝟙 B.X ⊗ g.hom) ≫ Y✝.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| f.hom ⊗ 𝟙 X✝.X
[PROOFSTEP]
rw [← g.act_hom]
[GOAL]
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| (𝟙 B.X ⊗ g.hom) ≫ Y✝.act
case a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
| f.hom ⊗ 𝟙 X✝.X
[PROOFSTEP]
rw [← g.act_hom]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ : Mon_ C
M : Mod_ A✝
A B : Mon_ C
f : A ⟶ B
X✝ Y✝ : Mod_ B
g : X✝ ⟶ Y✝
⊢ ((f.hom ⊗ 𝟙 X✝.X) ≫ X✝.act) ≫ g.hom = (f.hom ⊗ 𝟙 X✝.X) ≫ X✝.act ≫ g.hom
[PROOFSTEP]
rw [Category.assoc]


[GOAL]
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ Category.{?u.391, u + 1} (KleisliCat m)
[PROOFSTEP]
refine' { id_comp := _, comp_id := _, assoc := _ }
[GOAL]
case refine'_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {X Y : KleisliCat m} (f : X ⟶ Y), 𝟙 X ≫ f = f
[PROOFSTEP]
intros
[GOAL]
case refine'_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {X Y : KleisliCat m} (f : X ⟶ Y), f ≫ 𝟙 Y = f
[PROOFSTEP]
intros
[GOAL]
case refine'_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
⊢ ∀ {W X Y Z : KleisliCat m} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z), (f ≫ g) ≫ h = f ≫ g ≫ h
[PROOFSTEP]
intros
[GOAL]
case refine'_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
⊢ 𝟙 X✝ ≫ f✝ = f✝
[PROOFSTEP]
refine funext (fun x => ?_)
[GOAL]
case refine'_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
⊢ f✝ ≫ 𝟙 Y✝ = f✝
[PROOFSTEP]
refine funext (fun x => ?_)
[GOAL]
case refine'_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
W✝ X✝ Y✝ Z✝ : KleisliCat m
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
⊢ (f✝ ≫ g✝) ≫ h✝ = f✝ ≫ g✝ ≫ h✝
[PROOFSTEP]
refine funext (fun x => ?_)
[GOAL]
case refine'_1
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x : X✝
⊢ (𝟙 X✝ ≫ f✝) x = f✝ x
[PROOFSTEP]
simp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]
[GOAL]
case refine'_2
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
X✝ Y✝ : KleisliCat m
f✝ : X✝ ⟶ Y✝
x : X✝
⊢ (f✝ ≫ 𝟙 Y✝) x = f✝ x
[PROOFSTEP]
simp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]
[GOAL]
case refine'_3
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
W✝ X✝ Y✝ Z✝ : KleisliCat m
f✝ : W✝ ⟶ X✝
g✝ : X✝ ⟶ Y✝
h✝ : Y✝ ⟶ Z✝
x : W✝
⊢ ((f✝ ≫ g✝) ≫ h✝) x = (f✝ ≫ g✝ ≫ h✝) x
[PROOFSTEP]
simp [CategoryStruct.id, CategoryStruct.comp, (· >=> ·)]


[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.1655, u_3} D₁
inst✝⁴ : Category.{?u.1659, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ 𝟭 D₁ ⟶ G' ⋙ F'
[PROOFSTEP]
letI : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := Lifting.mk (CatCommSq.hComp G F L₁ L₂ L₁ G' F').iso'.symm
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.1655, u_3} D₁
inst✝⁴ : Category.{?u.1659, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
this : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := { iso' := CatCommSq.iso'.symm }
⊢ 𝟭 D₁ ⟶ G' ⋙ F'
[PROOFSTEP]
exact Localization.liftNatTrans L₁ W₁ L₁ ((G ⋙ F) ⋙ L₁) (𝟭 D₁) (G' ⋙ F') (whiskerRight adj.unit L₁)
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{u_5, u_3} D₁
inst✝⁴ : Category.{u_6, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
⊢ NatTrans.app (ε adj L₁ W₁ L₂ G' F') (L₁.obj X₁) =
    L₁.map (NatTrans.app adj.unit X₁) ≫
      NatTrans.app (CatCommSq.iso F L₂ L₁ F').hom (G.obj X₁) ≫ F'.map (NatTrans.app (CatCommSq.iso G L₁ L₂ G').hom X₁)
[PROOFSTEP]
letI : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := Lifting.mk (CatCommSq.hComp G F L₁ L₂ L₁ G' F').iso'.symm
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{u_5, u_3} D₁
inst✝⁴ : Category.{u_6, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
this : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := { iso' := CatCommSq.iso'.symm }
⊢ NatTrans.app (ε adj L₁ W₁ L₂ G' F') (L₁.obj X₁) =
    L₁.map (NatTrans.app adj.unit X₁) ≫
      NatTrans.app (CatCommSq.iso F L₂ L₁ F').hom (G.obj X₁) ≫ F'.map (NatTrans.app (CatCommSq.iso G L₁ L₂ G').hom X₁)
[PROOFSTEP]
simp only [ε, liftNatTrans_app, Lifting.iso, Iso.symm, Functor.id_obj, Functor.comp_obj, Lifting.id_iso',
  Functor.rightUnitor_hom_app, whiskerRight_app, CatCommSq.hComp_iso'_hom_app, id_comp]
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.13571, u_3} D₁
inst✝⁴ : Category.{?u.13575, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ F' ⋙ G' ⟶ 𝟭 D₂
[PROOFSTEP]
letI : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := Lifting.mk (CatCommSq.hComp F G L₂ L₁ L₂ F' G').iso'.symm
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.13571, u_3} D₁
inst✝⁴ : Category.{?u.13575, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
this : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := { iso' := CatCommSq.iso'.symm }
⊢ F' ⋙ G' ⟶ 𝟭 D₂
[PROOFSTEP]
exact liftNatTrans L₂ W₂ ((F ⋙ G) ⋙ L₂) L₂ (F' ⋙ G') (𝟭 D₂) (whiskerRight adj.counit L₂)
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{u_6, u_3} D₁
inst✝⁴ : Category.{u_5, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
⊢ NatTrans.app (η adj L₁ L₂ W₂ G' F') (L₂.obj X₂) =
    G'.map (NatTrans.app (CatCommSq.iso F L₂ L₁ F').inv X₂) ≫
      NatTrans.app (CatCommSq.iso G L₁ L₂ G').inv (F.obj X₂) ≫ L₂.map (NatTrans.app adj.counit X₂)
[PROOFSTEP]
letI : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := Lifting.mk (CatCommSq.hComp F G L₂ L₁ L₂ F' G').iso'.symm
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{u_6, u_3} D₁
inst✝⁴ : Category.{u_5, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
this : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := { iso' := CatCommSq.iso'.symm }
⊢ NatTrans.app (η adj L₁ L₂ W₂ G' F') (L₂.obj X₂) =
    G'.map (NatTrans.app (CatCommSq.iso F L₂ L₁ F').inv X₂) ≫
      NatTrans.app (CatCommSq.iso G L₁ L₂ G').inv (F.obj X₂) ≫ L₂.map (NatTrans.app adj.counit X₂)
[PROOFSTEP]
simp only [η, liftNatTrans_app, Lifting.iso, Iso.symm, CatCommSq.hComp_iso'_inv_app, whiskerRight_app, Lifting.id_iso',
  Functor.rightUnitor_inv_app, comp_id, assoc]
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
      (Functor.associator G' F' G').hom ≫ whiskerLeft G' (Localization.η adj L₁ L₂ W₂ G' F') =
    NatTrans.id (𝟭 D₁ ⋙ G')
[PROOFSTEP]
apply natTrans_ext L₁ W₁
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ ∀ (X : C₁),
    NatTrans.app
        (whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
          (Functor.associator G' F' G').hom ≫ whiskerLeft G' (Localization.η adj L₁ L₂ W₂ G' F'))
        (L₁.obj X) =
      NatTrans.app (NatTrans.id (𝟭 D₁ ⋙ G')) (L₁.obj X)
[PROOFSTEP]
intro X₁
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
⊢ NatTrans.app
      (whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
        (Functor.associator G' F' G').hom ≫ whiskerLeft G' (Localization.η adj L₁ L₂ W₂ G' F'))
      (L₁.obj X₁) =
    NatTrans.app (NatTrans.id (𝟭 D₁ ⋙ G')) (L₁.obj X₁)
[PROOFSTEP]
have eq := congr_app adj.left_triangle X₁
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : NatTrans.app (whiskerRight adj.unit G ≫ whiskerLeft G adj.counit) X₁ = NatTrans.app (𝟙 (𝟭 C₁ ⋙ G)) X₁
⊢ NatTrans.app
      (whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
        (Functor.associator G' F' G').hom ≫ whiskerLeft G' (Localization.η adj L₁ L₂ W₂ G' F'))
      (L₁.obj X₁) =
    NatTrans.app (NatTrans.id (𝟭 D₁ ⋙ G')) (L₁.obj X₁)
[PROOFSTEP]
dsimp at eq
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (NatTrans.app adj.unit X₁) ≫ NatTrans.app adj.counit (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ NatTrans.app
      (whiskerRight (Localization.ε adj L₁ W₁ L₂ G' F') G' ≫
        (Functor.associator G' F' G').hom ≫ whiskerLeft G' (Localization.η adj L₁ L₂ W₂ G' F'))
      (L₁.obj X₁) =
    NatTrans.app (NatTrans.id (𝟭 D₁ ⋙ G')) (L₁.obj X₁)
[PROOFSTEP]
rw [NatTrans.comp_app, NatTrans.comp_app, whiskerRight_app, Localization.ε_app, Functor.associator_hom_app, id_comp,
  whiskerLeft_app, G'.map_comp, G'.map_comp, assoc, assoc]
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (NatTrans.app adj.unit X₁) ≫ NatTrans.app adj.counit (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ G'.map (L₁.map (NatTrans.app adj.unit X₁)) ≫
      G'.map (NatTrans.app (CatCommSq.iso F L₂ L₁ F').hom (G.obj X₁)) ≫
        G'.map (F'.map (NatTrans.app (CatCommSq.iso G L₁ L₂ G').hom X₁)) ≫
          NatTrans.app (Localization.η adj L₁ L₂ W₂ G' F') (G'.obj (L₁.obj X₁)) =
    NatTrans.app (NatTrans.id (𝟭 D₁ ⋙ G')) (L₁.obj X₁)
[PROOFSTEP]
erw [(Localization.η adj L₁ L₂ W₂ G' F').naturality, Localization.η_app, assoc, assoc, ← G'.map_comp_assoc, ←
  G'.map_comp_assoc, assoc, Iso.hom_inv_id_app, comp_id, (CatCommSq.iso G L₁ L₂ G').inv.naturality_assoc, ←
  L₂.map_comp_assoc, eq, L₂.map_id, id_comp, Iso.inv_hom_id_app]
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
eq : G.map (NatTrans.app adj.unit X₁) ≫ NatTrans.app adj.counit (G.obj X₁) = 𝟙 (G.obj X₁)
⊢ 𝟙 ((L₁ ⋙ G').obj ((𝟭 C₁).obj X₁)) = NatTrans.app (NatTrans.id (𝟭 D₁ ⋙ G')) (L₁.obj X₁)
[PROOFSTEP]
rfl
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ whiskerLeft F' (Localization.ε adj L₁ W₁ L₂ G' F') ≫
      (Functor.associator F' G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F' =
    NatTrans.id (F' ⋙ 𝟭 D₁)
[PROOFSTEP]
apply natTrans_ext L₂ W₂
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
⊢ ∀ (X : C₂),
    NatTrans.app
        (whiskerLeft F' (Localization.ε adj L₁ W₁ L₂ G' F') ≫
          (Functor.associator F' G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F')
        (L₂.obj X) =
      NatTrans.app (NatTrans.id (F' ⋙ 𝟭 D₁)) (L₂.obj X)
[PROOFSTEP]
intro X₂
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
⊢ NatTrans.app
      (whiskerLeft F' (Localization.ε adj L₁ W₁ L₂ G' F') ≫
        (Functor.associator F' G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F')
      (L₂.obj X₂) =
    NatTrans.app (NatTrans.id (F' ⋙ 𝟭 D₁)) (L₂.obj X₂)
[PROOFSTEP]
have eq := congr_app adj.right_triangle X₂
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : NatTrans.app (whiskerLeft F adj.unit ≫ whiskerRight adj.counit F) X₂ = NatTrans.app (𝟙 (F ⋙ 𝟭 C₁)) X₂
⊢ NatTrans.app
      (whiskerLeft F' (Localization.ε adj L₁ W₁ L₂ G' F') ≫
        (Functor.associator F' G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F')
      (L₂.obj X₂) =
    NatTrans.app (NatTrans.id (F' ⋙ 𝟭 D₁)) (L₂.obj X₂)
[PROOFSTEP]
dsimp at eq
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : NatTrans.app adj.unit (F.obj X₂) ≫ F.map (NatTrans.app adj.counit X₂) = 𝟙 (F.obj X₂)
⊢ NatTrans.app
      (whiskerLeft F' (Localization.ε adj L₁ W₁ L₂ G' F') ≫
        (Functor.associator F' G' F').inv ≫ whiskerRight (Localization.η adj L₁ L₂ W₂ G' F') F')
      (L₂.obj X₂) =
    NatTrans.app (NatTrans.id (F' ⋙ 𝟭 D₁)) (L₂.obj X₂)
[PROOFSTEP]
rw [NatTrans.comp_app, NatTrans.comp_app, whiskerLeft_app, whiskerRight_app, Localization.η_app,
  Functor.associator_inv_app, id_comp, F'.map_comp, F'.map_comp]
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : NatTrans.app adj.unit (F.obj X₂) ≫ F.map (NatTrans.app adj.counit X₂) = 𝟙 (F.obj X₂)
⊢ NatTrans.app (Localization.ε adj L₁ W₁ L₂ G' F') (F'.obj (L₂.obj X₂)) ≫
      F'.map (G'.map (NatTrans.app (CatCommSq.iso F L₂ L₁ F').inv X₂)) ≫
        F'.map (NatTrans.app (CatCommSq.iso G L₁ L₂ G').inv (F.obj X₂)) ≫ F'.map (L₂.map (NatTrans.app adj.counit X₂)) =
    NatTrans.app (NatTrans.id (F' ⋙ 𝟭 D₁)) (L₂.obj X₂)
[PROOFSTEP]
erw [← (Localization.ε _ _ _ _ _ _).naturality_assoc, Localization.ε_app, assoc, assoc, ← F'.map_comp_assoc,
  Iso.hom_inv_id_app, F'.map_id, id_comp, ← NatTrans.naturality, ← L₁.map_comp_assoc, eq, L₁.map_id, id_comp,
  Iso.inv_hom_id_app]
[GOAL]
case h
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{?u.24676, u_3} D₁
inst✝⁴ : Category.{?u.24680, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
eq : NatTrans.app adj.unit (F.obj X₂) ≫ F.map (NatTrans.app adj.counit X₂) = 𝟙 (F.obj X₂)
⊢ 𝟙 ((L₂ ⋙ F').obj X₂) = NatTrans.app (NatTrans.id (F' ⋙ 𝟭 D₁)) (L₂.obj X₂)
[PROOFSTEP]
rfl
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{u_5, u_3} D₁
inst✝⁴ : Category.{u_6, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₁ : C₁
⊢ NatTrans.app (localization adj L₁ W₁ L₂ W₂ G' F').unit (L₁.obj X₁) =
    L₁.map (NatTrans.app adj.unit X₁) ≫
      NatTrans.app (CatCommSq.iso F L₂ L₁ F').hom (G.obj X₁) ≫ F'.map (NatTrans.app (CatCommSq.iso G L₁ L₂ G').hom X₁)
[PROOFSTEP]
apply Localization.ε_app
[GOAL]
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{u_1, u_1} C₁
inst✝⁶ : Category.{u_2, u_2} C₂
inst✝⁵ : Category.{u_6, u_3} D₁
inst✝⁴ : Category.{u_5, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
W₁ : MorphismProperty C₁
inst✝³ : Functor.IsLocalization L₁ W₁
L₂ : C₂ ⥤ D₂
W₂ : MorphismProperty C₂
inst✝² : Functor.IsLocalization L₂ W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
inst✝¹ : CatCommSq G L₁ L₂ G'
inst✝ : CatCommSq F L₂ L₁ F'
X₂ : C₂
⊢ NatTrans.app (localization adj L₁ W₁ L₂ W₂ G' F').counit (L₂.obj X₂) =
    G'.map (NatTrans.app (CatCommSq.iso F L₂ L₁ F').inv X₂) ≫
      NatTrans.app (CatCommSq.iso G L₁ L₂ G').inv (F.obj X₂) ≫ L₂.map (NatTrans.app adj.counit X₂)
[PROOFSTEP]
apply Localization.η_app