awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
X : C
⊢ F.HasPointwiseRightDerivedFunctorAt W X ↔ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X)

Tactic:
exact ⟨fun h ↦ h.hasColimit', fun h ↦ ⟨h⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
X : C
inst_4 rwa rwa₁ rwa₂ rwa₃ : F.HasPointwiseRightDerivedFunctorAt W X
⊢ L.HasPointwiseLeftKanExtensionAt F (L.obj X)

Tactic:
rwa [← hasPointwiseRightDerivedFunctorAt_iff F L W]

Premises used: CategoryTheory.Functor.hasPointwiseRightDerivedFunctorAt_iff
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₃, u₃} H
F : Functor.{v₁, v₃, u₁, u₃} C H
W : MorphismProperty.{v₁, u₁} C
X Y : C
w : X ⟶ Y
hw : W w
simp : W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X) ↔ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj Y)
⊢ F.HasPointwiseRightDerivedFunctorAt W X ↔ F.HasPointwiseRightDerivedFunctorAt W Y

Tactic:
simp only [F.hasPointwiseRightDerivedFunctorAt_iff W.Q W]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.hasPointwiseRightDerivedFunctorAt_iff
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₃, u₃} H
F : Functor.{v₁, v₃, u₁, u₃} C H
W : MorphismProperty.{v₁, u₁} C
X Y : C
w : X ⟶ Y
hw : W w
⊢ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X) ↔ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj Y)

Tactic:
hasPointwiseLeftKanExtensionAt_iff_of_iso W.Q F (Localization.isoOfHom W.Q W w hw)

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.isoOfHom, CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₃, u₃} H
F : Functor.{v₁, v₃, u₁, u₃} C H
W : MorphismProperty.{v₁, u₁} C
X Y : C
w : X ⟶ Y
hw : W w
⊢ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X) ↔ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj Y)

Tactic:
exact hasPointwiseLeftKanExtensionAt_iff_of_iso W.Q F (Localization.isoOfHom W.Q W w hw)

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.isoOfHom, CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : F.HasPointwiseRightDerivedFunctor W
inst_4 : L.IsLocalization W
Y : D
⊢ L.EssSurj

Tactic:
have := Localization.essSurj L W
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : F.HasPointwiseRightDerivedFunctor W
inst_4 : L.IsLocalization W
Y : D
this : L.EssSurj
rw : F.HasPointwiseRightDerivedFunctorAt W (L.objPreimage Y)
⊢ L.HasPointwiseLeftKanExtensionAt F Y

Tactic:
rw [← hasPointwiseLeftKanExtensionAt_iff_of_iso _ F (L.objObjPreimageIso Y),
    ← F.hasPointwiseRightDerivedFunctorAt_iff L W]

Premises used: CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_iso, CategoryTheory.Functor.hasPointwiseRightDerivedFunctorAt_iff
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : F.HasPointwiseRightDerivedFunctor W
inst_4 : L.IsLocalization W
Y : D
this : L.EssSurj
⊢ F.HasPointwiseRightDerivedFunctorAt W (L.objPreimage Y)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₃, u₃} H
F : Functor.{v₁, v₃, u₁, u₃} C H
W : MorphismProperty.{v₁, u₁} C
inst_2 : F.HasPointwiseRightDerivedFunctor W
⊢ W.Q.HasPointwiseLeftKanExtension F

Tactic:
have := F.hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor W.Q W
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₃, u₃} H
F : Functor.{v₁, v₃, u₁, u₃} C H
W : MorphismProperty.{v₁, u₁} C
inst_2 : F.HasPointwiseRightDerivedFunctor W
this : W.Q.HasPointwiseLeftKanExtension F
⊢ W.Q.HasLeftKanExtension F

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
⊢ CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk (𝟙 (L.obj Y))))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk (𝟙 (L.obj Y))))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk φ))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk φ))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk φ)
⊢ Eq (α :=
    obj (CostructuredArrow.proj L (L.obj Y) ⋙ F) (CostructuredArrow.mk (L.map f ≫ φ)) ⟶
      obj (obj (const (CostructuredArrow L (L.obj Y))) s.pt) (CostructuredArrow.mk φ))
    (map (CostructuredArrow.proj L (L.obj Y) ⋙ F) (CostructuredArrow.homMk f ⋯) ≫ s.ι.app (CostructuredArrow.mk φ))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)) ≫
      map (obj (const (CostructuredArrow L (L.obj Y))) s.pt) (CostructuredArrow.homMk f ⋯))

Tactic:
have eq := s.ι.naturality
        (CostructuredArrow.homMk f : CostructuredArrow.mk (L.map f ≫ φ) ⟶ CostructuredArrow.mk φ)
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk φ))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk φ))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk φ)
eq :
  Eq (α :=
    obj (CostructuredArrow.proj L (L.obj Y) ⋙ F) (CostructuredArrow.mk (L.map f ≫ φ)) ⟶
      obj (obj (const (CostructuredArrow L (L.obj Y))) s.pt) (CostructuredArrow.mk φ))
    (map (CostructuredArrow.proj L (L.obj Y) ⋙ F) (CostructuredArrow.homMk f ⋯) ≫ s.ι.app (CostructuredArrow.mk φ))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)) ≫
      map (obj (const (CostructuredArrow L (L.obj Y))) s.pt) (CostructuredArrow.homMk f ⋯))
refine_1 :
  Eq (α := F.obj X₁ ⟶ s.pt)
    ((e.hom.app X₁ ≫ G.map (L.map f ≫ φ)) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
⊢ CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk (L.map f ≫ φ)))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk (L.map f ≫ φ)))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk (L.map f ≫ φ))

Tactic:
dsimp at eq hφ ⊢
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  Eq (α := F.obj X₂ ⟶ s.pt) ((e.hom.app X₂ ≫ G.map φ) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk φ))
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map f ≫ s.ι.app (CostructuredArrow.mk φ))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)) ≫ 𝟙 s.pt)
⊢ Eq (α := F.obj X₁ ⟶ s.pt) (F.map f ≫ s.ι.app (CostructuredArrow.mk φ)) (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))

Tactic:
rw [comp_id] at eq

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  Eq (α := F.obj X₂ ⟶ s.pt) ((e.hom.app X₂ ≫ G.map φ) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk φ))
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map f ≫ s.ι.app (CostructuredArrow.mk φ)) (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
⊢ Eq (α := F.obj X₂ ⟶ s.pt) (e.hom.app X₂ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk φ))

Tactic:
rw [assoc] at hφ

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  Eq (α := F.obj X₂ ⟶ s.pt) ((e.hom.app X₂ ≫ G.map φ) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk φ))
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map f ≫ s.ι.app (CostructuredArrow.mk φ)) (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
hφ₁ :
  Eq (α := F.obj X₂ ⟶ s.pt) (e.hom.app X₂ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk φ))
⊢ Eq (α := F.obj X₁ ⟶ s.pt) (F.map f ≫ s.ι.app (CostructuredArrow.mk φ)) (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))

Tactic:
rw [assoc] at hφ

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  Eq (α := F.obj X₂ ⟶ s.pt) (e.hom.app X₂ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk φ))
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map f ≫ s.ι.app (CostructuredArrow.mk φ)) (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
refine_1 :
  Eq (α := F.obj X₁ ⟶ s.pt)
    (e.hom.app X₁ ≫ G.map (L.map f ≫ φ) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
refine_1₁ :
  Eq (α := F.obj X₁ ⟶ s.pt)
    (e.hom.app X₁ ≫ G.map (L.map f) ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
refine_1₂ :
  Eq (α := F.obj X₁ ⟶ s.pt)
    (e.hom.app X₁ ≫ G.map (L.map f) ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (F.map f ≫ s.ι.app (CostructuredArrow.mk φ))
refine_1₃ :
  Eq (α := F.obj X₁ ⟶ s.pt)
    (e.hom.app X₁ ≫ G.map (L.map f) ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (F.map f ≫ e.hom.app X₂ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
refine_1₄ :
  Eq (α := F.obj X₁ ⟶ s.pt)
    (e.hom.app X₁ ≫ G.map (L.map f) ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (e.hom.app X₁ ≫ (L ⋙ G).map f ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
refine_1₅ refine_1₆ :
  Eq (α := F.obj X₁ ⟶ s.pt)
    (e.hom.app X₁ ≫ G.map (L.map f) ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (e.hom.app X₁ ≫ G.map (L.map f) ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
⊢ Eq (α := F.obj X₁ ⟶ s.pt)
    ((e.hom.app X₁ ≫ G.map (L.map f ≫ φ)) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))

Tactic:
rw [assoc, map_comp_assoc, ← eq, ← hφ, NatTrans.naturality_assoc, comp_map]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.comp_map, CategoryTheory.NatTrans.naturality_assoc
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk φ))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk φ))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk φ)
⊢ IsIso (L.map w)

Tactic:
have := Localization.inverts L W w hw
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk φ))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk φ))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk φ)
this : IsIso (L.map w)
rw : IsIso (e.hom.app X₁ ≫ (L ⋙ G).map w ≫ e.inv.app X₂)
⊢ IsIso (F.map w)

Tactic:
rw [← NatIso.naturality_2 e w]

Premises used: CategoryTheory.NatIso.naturality_2
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk φ))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk φ))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk φ)
this : IsIso (L.map w)
dsimp : IsIso (e.hom.app X₁ ≫ G.map (L.map w) ≫ e.inv.app X₂)
⊢ IsIso (e.hom.app X₁ ≫ (L ⋙ G).map w ≫ e.inv.app X₂)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk φ))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk φ))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk φ)
this : IsIso (L.map w)
⊢ IsIso (e.hom.app X₁ ≫ G.map (L.map w) ≫ e.inv.app X₂)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk φ))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk φ))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk φ)
⊢ IsIso (F.map w)

Tactic:
have : IsIso (F.map w) := by
        have := Localization.inverts L W w hw
        rw [← NatIso.naturality_2 e w]
        dsimp
        infer_instance
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived
Goal:
C : Type u₁
D : Type u₂
H : Type u₃
inst : Category.{v₁, u₁} C
inst_1 : Category.{v₂, u₂} D
inst_2 : Category.{v₃, u₃} H
F' : Functor.{v₂, v₃, u₂, u₃} D H
F : Functor.{v₁, v₃, u₁, u₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj X₁ ⟶ L.obj Y
hφ :
  CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk φ))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk φ))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk φ)
this : IsIso (F.map w)
⊢ Eq (α :=
    obj (CostructuredArrow.proj L (L.obj Y) ⋙ F) (CostructuredArrow.mk φ) ⟶
      obj (obj (const (CostructuredArrow L (L.obj Y))) s.pt)
        (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
    (map (CostructuredArrow.proj L (L.obj Y) ⋙ F) (CostructuredArrow.homMk w ⋯) ≫
      s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
    (s.ι.app (CostructuredArrow.mk φ) ≫
      map (obj (const (CostructuredArrow L (L.obj Y))) s.pt) (CostructuredArrow.homMk w ⋯))

Tactic:
have eq := s.ι.naturality
        (CostructuredArrow.homMk w : CostructuredArrow.mk φ ⟶ CostructuredArrow.mk
          ((Localization.isoOfHom L W w hw).inv ≫ φ))