awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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.HasPointwiseLeftDerivedFunctorAt W X
⊢ L.HasPointwiseRightKanExtensionAt F (L.obj X)

Tactic:
rwa [← hasPointwiseLeftDerivedFunctorAt_iff F L W]

Premises used: CategoryTheory.Functor.hasPointwiseLeftDerivedFunctorAt_iff
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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.HasPointwiseRightKanExtensionAt F (W.Q.obj X) ↔ W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj Y)
⊢ F.HasPointwiseLeftDerivedFunctorAt W X ↔ F.HasPointwiseLeftDerivedFunctorAt W Y

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

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.hasPointwiseLeftDerivedFunctorAt_iff
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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.HasPointwiseRightKanExtensionAt F (W.Q.obj X) ↔ W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj Y)

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

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.isoOfHom, CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_iso
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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.HasPointwiseRightKanExtensionAt F (W.Q.obj X) ↔ W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj Y)

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

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.isoOfHom, CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_iso
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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.HasPointwiseLeftDerivedFunctor W
inst_4 : L.IsLocalization W
Y : D
⊢ L.EssSurj

Tactic:
have := Localization.essSurj L W
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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.HasPointwiseLeftDerivedFunctor W
inst_4 : L.IsLocalization W
Y : D
this : L.EssSurj
rw : F.HasPointwiseLeftDerivedFunctorAt W (L.objPreimage Y)
⊢ L.HasPointwiseRightKanExtensionAt F Y

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

Premises used: CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_iso, CategoryTheory.Functor.hasPointwiseLeftDerivedFunctorAt_iff, CategoryTheory.Functor.objObjPreimageIso
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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.HasPointwiseLeftDerivedFunctor W
inst_4 : L.IsLocalization W
Y : D
this : L.EssSurj
⊢ F.HasPointwiseLeftDerivedFunctorAt W (L.objPreimage Y)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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.HasPointwiseLeftDerivedFunctor W
⊢ W.Q.HasPointwiseRightKanExtension F

Tactic:
have := F.hasPointwiseRightKanExtension_of_hasPointwiseLeftDerivedFunctor W.Q W
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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.HasPointwiseLeftDerivedFunctor W
this : W.Q.HasPointwiseRightKanExtension F
⊢ W.Q.HasRightKanExtension F

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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
α : L ⋙ F' ⟶ 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 : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
⊢ CategoryStruct.comp (Y := Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y :
        s.pt ⟶ Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y))) (StructuredArrow.mk (𝟙 (L.obj Y))) :
        obj
            (obj (const (StructuredArrow (L.obj Y) L))
              (Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y))))
            (StructuredArrow.mk (𝟙 (L.obj Y))) ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.π.app (StructuredArrow.mk (𝟙 (L.obj Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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
α : L ⋙ F' ⟶ 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 : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj Y ⟶ L.obj X₁
hφ :
  CategoryStruct.comp (Y := Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y :
        s.pt ⟶ Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y))) (StructuredArrow.mk φ) :
        obj
            (obj (const (StructuredArrow (L.obj Y) L))
              (Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y))))
            (StructuredArrow.mk φ) ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ)) =
    s.π.app (StructuredArrow.mk φ)
⊢ Eq (α :=
    obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk φ) ⟶
      (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ L.map f)))
    (map (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.homMk f ⋯) ≫
      s.π.app (StructuredArrow.mk (φ ≫ L.map f)))
    (s.π.app (StructuredArrow.mk φ) ≫ (StructuredArrow.proj (L.obj Y) L ⋙ F).map (StructuredArrow.homMk f ⋯))

Tactic:
have eq := s.π.naturality
        (StructuredArrow.homMk f : StructuredArrow.mk φ ⟶ StructuredArrow.mk (φ ≫ L.map f))
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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
α : L ⋙ F' ⟶ 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 : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj Y ⟶ L.obj X₁
hφ :
  CategoryStruct.comp (Y := Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y :
        s.pt ⟶ Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y))) (StructuredArrow.mk φ) :
        obj
            (obj (const (StructuredArrow (L.obj Y) L))
              (Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y))))
            (StructuredArrow.mk φ) ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ)) =
    s.π.app (StructuredArrow.mk φ)
eq :
  Eq (α :=
    obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk φ) ⟶
      (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ L.map f)))
    (map (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.homMk f ⋯) ≫
      s.π.app (StructuredArrow.mk (φ ≫ L.map f)))
    (s.π.app (StructuredArrow.mk φ) ≫ (StructuredArrow.proj (L.obj Y) L ⋙ F).map (StructuredArrow.homMk f ⋯))
refine_1 :
  Eq (α := s.pt ⟶ F.obj X₂)
    ((s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫ G.map (φ ≫ L.map f) ≫ e.inv.app X₂ : s.pt ⟶ F.obj X₂)
    (s.π.app (StructuredArrow.mk (φ ≫ L.map f)) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk (φ ≫ L.map f)) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ L.map f)))
⊢ CategoryStruct.comp (Y := Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y :
        s.pt ⟶ Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y))) (StructuredArrow.mk (φ ≫ L.map f)) :
        obj
            (obj (const (StructuredArrow (L.obj Y) L))
              (Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y))))
            (StructuredArrow.mk (φ ≫ L.map f)) ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ L.map f))) =
    s.π.app (StructuredArrow.mk (φ ≫ L.map f))

Tactic:
dsimp at eq hφ ⊢
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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
α : L ⋙ F' ⟶ 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 : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj Y ⟶ L.obj X₁
hφ :
  Eq (α := s.pt ⟶ F.obj X₁)
    ((s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫ G.map φ ≫ e.inv.app X₁ : s.pt ⟶ F.obj X₁)
    (s.π.app (StructuredArrow.mk φ) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk φ) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ))
eq :
  Eq (α := s.pt ⟶ F.obj X₂) (𝟙 s.pt ≫ s.π.app (StructuredArrow.mk (φ ≫ L.map f)) : s.pt ⟶ F.obj X₂)
    (s.π.app (StructuredArrow.mk φ) ≫ F.map f : s.pt ⟶ F.obj X₂)
⊢ Eq (α := s.pt ⟶ F.obj X₂)
    (s.π.app (StructuredArrow.mk (φ ≫ L.map f)) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk (φ ≫ L.map f)) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ L.map f)))
    (s.π.app (StructuredArrow.mk φ) ≫ F.map f)

Tactic:
rw [id_comp] at eq

Premises used: CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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
α : L ⋙ F' ⟶ 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 : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj Y ⟶ L.obj X₁
hφ :
  Eq (α := s.pt ⟶ F.obj X₁)
    ((s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫ G.map φ ≫ e.inv.app X₁ : s.pt ⟶ F.obj X₁)
    (s.π.app (StructuredArrow.mk φ) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk φ) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ))
eq :
  Eq (α := s.pt ⟶ F.obj X₂)
    (s.π.app (StructuredArrow.mk (φ ≫ L.map f)) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk (φ ≫ L.map f)) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ L.map f)))
    (s.π.app (StructuredArrow.mk φ) ≫ F.map f)
⊢ Eq (α := s.pt ⟶ F.obj X₁)
    (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y ≫ G.map φ ≫ e.inv.app X₁ : s.pt ⟶ F.obj X₁)
    (s.π.app (StructuredArrow.mk φ) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk φ) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ))

Tactic:
rw [assoc] at hφ

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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
α : L ⋙ F' ⟶ 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 : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj Y ⟶ L.obj X₁
hφ :
  Eq (α := s.pt ⟶ F.obj X₁)
    ((s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫ G.map φ ≫ e.inv.app X₁ : s.pt ⟶ F.obj X₁)
    (s.π.app (StructuredArrow.mk φ) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk φ) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ))
eq :
  Eq (α := s.pt ⟶ F.obj X₂)
    (s.π.app (StructuredArrow.mk (φ ≫ L.map f)) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk (φ ≫ L.map f)) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ L.map f)))
    (s.π.app (StructuredArrow.mk φ) ≫ F.map f)
hφ₁ :
  Eq (α := s.pt ⟶ F.obj X₁)
    (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y ≫ G.map φ ≫ e.inv.app X₁ : s.pt ⟶ F.obj X₁)
    (s.π.app (StructuredArrow.mk φ) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk φ) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ))
⊢ Eq (α := s.pt ⟶ F.obj X₂)
    (s.π.app (StructuredArrow.mk (φ ≫ L.map f)) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk (φ ≫ L.map f)) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ L.map f)))
    (s.π.app (StructuredArrow.mk φ) ≫ F.map f)

Tactic:
rw [assoc] at hφ

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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
α : L ⋙ F' ⟶ 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 : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj Y ⟶ L.obj X₁
hφ :
  Eq (α := s.pt ⟶ F.obj X₁)
    (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y ≫ G.map φ ≫ e.inv.app X₁ : s.pt ⟶ F.obj X₁)
    (s.π.app (StructuredArrow.mk φ) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk φ) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ))
eq :
  Eq (α := s.pt ⟶ F.obj X₂)
    (s.π.app (StructuredArrow.mk (φ ≫ L.map f)) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk (φ ≫ L.map f)) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ L.map f)))
    (s.π.app (StructuredArrow.mk φ) ≫ F.map f)
⊢ Eq (α := s.pt ⟶ F.obj X₂)
    ((s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫ G.map (φ ≫ L.map f) ≫ e.inv.app X₂ : s.pt ⟶ F.obj X₂)
    (s.π.app (StructuredArrow.mk (φ ≫ L.map f)) :
      obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.mk (φ ≫ L.map f)) ⟶
        (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ L.map f)))

Tactic:
simp [eq, ← reassoc_of% hφ, ← e.inv.naturality f]

Premises used: CategoryTheory.NatTrans.naturality, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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
α : L ⋙ F' ⟶ 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 : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj Y ⟶ L.obj X₂
hφ :
  CategoryStruct.comp (Y := Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y :
        s.pt ⟶ Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y))) (StructuredArrow.mk φ) :
        obj
            (obj (const (StructuredArrow (L.obj Y) L))
              (Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y))))
            (StructuredArrow.mk φ) ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ)) =
    s.π.app (StructuredArrow.mk φ)
⊢ IsIso (L.map w)

Tactic:
have := Localization.inverts L W w hw
-- Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
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
α : L ⋙ F' ⟶ 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 : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj Y ⟶ L.obj X₂
hφ :
  CategoryStruct.comp (Y := Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y :
        s.pt ⟶ Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y))) (StructuredArrow.mk φ) :
        obj
            (obj (const (StructuredArrow (L.obj Y) L))
              (Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y))))
            (StructuredArrow.mk φ) ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ)) =
    s.π.app (StructuredArrow.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.PointwiseLeftDerived
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
α : L ⋙ F' ⟶ 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 : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj Y ⟶ L.obj X₂
hφ :
  CategoryStruct.comp (Y := Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y :
        s.pt ⟶ Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y))) (StructuredArrow.mk φ) :
        obj
            (obj (const (StructuredArrow (L.obj Y) L))
              (Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y))))
            (StructuredArrow.mk φ) ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ)) =
    s.π.app (StructuredArrow.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.PointwiseLeftDerived
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
α : L ⋙ F' ⟶ 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 : Cone (StructuredArrow.proj (L.obj Y) L ⋙ F)
j : StructuredArrow (L.obj Y) L
X₁ X₂ : C
w : X₁ ⟶ X₂
hw : W w
φ : L.obj Y ⟶ L.obj X₂
hφ :
  CategoryStruct.comp (Y := Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y :
        s.pt ⟶ Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y)))
      (NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y))) (StructuredArrow.mk φ) :
        obj
            (obj (const (StructuredArrow (L.obj Y) L))
              (Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y))))
            (StructuredArrow.mk φ) ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ)) =
    s.π.app (StructuredArrow.mk φ)
this : IsIso (L.map w)
⊢ IsIso (e.hom.app X₁ ≫ G.map (L.map w) ≫ e.inv.app X₂)

Tactic:
infer_instance