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₃} 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 :
  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 ⋯))
refine_2 :
  Eq (α := F.obj X₂ ⟶ s.pt)
    ((e.hom.app X₂ ≫ G.map ((Localization.isoOfHom L W w hw).inv ≫ φ)) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
⊢ 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 ((Localization.isoOfHom L W w hw).inv ≫ φ)))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)))
        (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ))

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
w : X₁ ⟶ X₂
hw : W w
φ : 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 φ))
this : IsIso (F.map w)
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
    (s.ι.app (CostructuredArrow.mk φ) ≫ 𝟙 s.pt)
⊢ Eq (α := F.obj X₁ ⟶ s.pt) (F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
    (s.ι.app (CostructuredArrow.mk φ))

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
w : X₁ ⟶ X₂
hw : W w
φ : 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 φ))
this : IsIso (F.map w)
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
    (s.ι.app (CostructuredArrow.mk φ))
⊢ 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
w : X₁ ⟶ X₂
hw : W w
φ : 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 φ))
this : IsIso (F.map w)
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
    (s.ι.app (CostructuredArrow.mk φ))
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 φ))
⊢ IsIso (F.map w)

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
w : X₁ ⟶ X₂
hw : W w
φ : 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 φ))
this : IsIso (F.map w)
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
    (s.ι.app (CostructuredArrow.mk φ))
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 φ))
this₁ : IsIso (F.map w)
⊢ Eq (α := F.obj X₁ ⟶ s.pt) (F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
    (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
w : X₁ ⟶ X₂
hw : W w
φ : 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 φ))
this : IsIso (F.map w)
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
    (s.ι.app (CostructuredArrow.mk φ))
refine_2 :
  Eq (α := F.obj X₁ ⟶ s.pt)
    (e.hom.app X₁ ≫
      G.map (L.map w ≫ (Localization.isoOfHom L W w hw).inv) ≫
        G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (e.hom.app X₁ ≫ 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 ((Localization.isoOfHom L W w hw).inv ≫ φ)) ≫
      e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))

Tactic:
rw [map_comp, assoc, assoc, ← cancel_epi (F.map w), eq, ← hφ,
        NatTrans.naturality_assoc, comp_map, ← G.map_comp_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.cancel_epi, 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φ :
  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 φ))
this : IsIso (F.map w)
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map w ≫ s.ι.app (CostructuredArrow.mk ((Localization.isoOfHom L W w hw).inv ≫ φ)))
    (s.ι.app (CostructuredArrow.mk φ))
⊢ Eq (α := F.obj X₁ ⟶ s.pt)
    (e.hom.app X₁ ≫
      G.map (L.map w ≫ (Localization.isoOfHom L W w hw).inv) ≫
        G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (e.hom.app X₁ ≫ G.map φ ≫ e.inv.app 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)
m : Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)) ⟶ s.pt
hm :
  ∀ (j : CostructuredArrow L (L.obj Y)),
    NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) j ≫ m = s.ι.app j
⊢ NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk (𝟙 (L.obj Y))) ≫ m =
    s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))

Tactic:
have := hm (CostructuredArrow.mk (𝟙 (L.obj Y)))
-- 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)
m : Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y)) ⟶ s.pt
hm :
  ∀ (j : CostructuredArrow L (L.obj Y)),
    NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) j ≫ m = s.ι.app j
this :
  NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk (𝟙 (L.obj Y))) ≫ m =
    s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))
dsimp : m = e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))
⊢ m = e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))

Tactic:
dsimp at this m hm ⊢
-- 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)
m : G.obj (L.obj Y) ⟶ s.pt
hm : ∀ (j : CostructuredArrow L (L.obj Y)), (e.hom.app j.left ≫ G.map j.hom) ≫ m = s.ι.app j
this : (e.hom.app Y ≫ G.map (𝟙 (L.obj Y))) ≫ m = s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))
⊢ m = e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))

Tactic:
simp only [← this, map_id, comp_id, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.Category.comp_id, CategoryTheory.Functor.map_id, CategoryTheory.Iso.inv_hom_id_app_assoc
-- 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
hF : W.IsInvertedBy F
X : C
rw : W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X)
⊢ F.HasPointwiseRightDerivedFunctorAt W X

Tactic:
rw [hasPointwiseRightDerivedFunctorAt_iff F 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
hF : W.IsInvertedBy F
X : C
⊢ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X)

Tactic:
(isPointwiseLeftKanExtensionOfIsoOfIsLocalization W
    (Localization.fac F hF W.Q).symm).hasPointwiseLeftKanExtension _

Premises used: CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsoOfIsLocalization, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension, CategoryTheory.Iso.symm, CategoryTheory.Localization.fac
-- 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
hF : W.IsInvertedBy F
X : C
⊢ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X)

Tactic:
exact (isPointwiseLeftKanExtensionOfIsoOfIsLocalization W
    (Localization.fac F hF W.Q).symm).hasPointwiseLeftKanExtension _

Premises used: CategoryTheory.Functor.isPointwiseLeftKanExtensionOfIsoOfIsLocalization, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hasPointwiseLeftKanExtension, CategoryTheory.Iso.symm, CategoryTheory.Localization.fac
-- 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
inst_3 : L.IsLocalization W
hF : W.IsInvertedBy F
⊢ (Localization.lift (W := W) F hF L).IsRightDerivedFunctor (Iso.inv (Localization.fac (W := W) F hF L)) W

Tactic:
isRightDerivedFunctor_of_inverts W _ _

Premises used: CategoryTheory.Functor.isRightDerivedFunctor_of_inverts
-- 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
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
F : Functor.{v₁, v₃, u₁, u₃} C H
RF : Functor.{v₂, v₃, u₂, u₃} D H
α : F ⟶ L ⋙ RF
hF : W.IsInvertedBy F
inst_4 : RF.IsRightDerivedFunctor α W
⊢ α =
    Iso.inv (Localization.fac (W := W) F hF L) ≫
      L.whiskerLeft
        ((Localization.lift (W := W) F hF L).rightDerivedUnique RF (Iso.inv (Localization.fac (W := W) F hF L)) α W).hom

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
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
F : Functor.{v₁, v₃, u₁, u₃} C H
RF : Functor.{v₂, v₃, u₂, u₃} D H
α : F ⟶ L ⋙ RF
hF : W.IsInvertedBy F
inst_4 : RF.IsRightDerivedFunctor α W
⊢ α =
    Iso.inv (Localization.fac (W := W) F hF L) ≫
      L.whiskerLeft
        ((Localization.lift (W := W) F hF L).rightDerivedUnique RF (Iso.inv (Localization.fac (W := W) F hF L)) α W).hom

Tactic:
have : α = (Localization.fac F hF L).inv ≫
    whiskerLeft _ (rightDerivedUnique _ _ (Localization.fac F hF L).inv α W).hom := by 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
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
F : Functor.{v₁, v₃, u₁, u₃} C H
RF : Functor.{v₂, v₃, u₂, u₃} D H
α : F ⟶ L ⋙ RF
hF : W.IsInvertedBy F
inst_4 : RF.IsRightDerivedFunctor α W
this :
  α =
    Iso.inv (Localization.fac (W := W) F hF L) ≫
      L.whiskerLeft
        ((Localization.lift (W := W) F hF L).rightDerivedUnique RF (Iso.inv (Localization.fac (W := W) F hF L)) α W).hom
rw :
  IsIso
    (Iso.inv (Localization.fac (W := W) F hF L) ≫
      L.whiskerLeft
        ((Localization.lift (W := W) F hF L).rightDerivedUnique RF (Iso.inv (Localization.fac (W := W) F hF L)) α
            W).hom)
⊢ IsIso α

Tactic:
rw [this]
-- 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
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
F : Functor.{v₁, v₃, u₁, u₃} C H
RF : Functor.{v₂, v₃, u₂, u₃} D H
α : F ⟶ L ⋙ RF
hF : W.IsInvertedBy F
inst_4 : RF.IsRightDerivedFunctor α W
this :
  α =
    Iso.inv (Localization.fac (W := W) F hF L) ≫
      L.whiskerLeft
        ((Localization.lift (W := W) F hF L).rightDerivedUnique RF (Iso.inv (Localization.fac (W := W) F hF L)) α W).hom
⊢ IsIso
    (Iso.inv (Localization.fac (W := W) F hF L) ≫
      L.whiskerLeft
        ((Localization.lift (W := W) F hF L).rightDerivedUnique RF (Iso.inv (Localization.fac (W := W) F hF L)) α
            W).hom)

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
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
F : Functor.{v₁, v₃, u₁, u₃} C H
RF : Functor.{v₂, v₃, u₂, u₃} D H
α : F ⟶ L ⋙ RF
hF : W.IsInvertedBy F
⊢ RF.IsRightDerivedFunctor α W ↔ IsIso α

Tactic:
⟨fun _ ↦ isIso_of_isRightDerivedFunctor_of_inverts RF α hF, fun _ ↦
    isRightDerivedFunctor_of_inverts W RF (asIso α).symm⟩

Premises used: CategoryTheory.Functor.isIso_of_isRightDerivedFunctor_of_inverts, Iff.intro, CategoryTheory.Iso.symm, CategoryTheory.Functor.isRightDerivedFunctor_of_inverts, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
RF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
mp : RF.IsRightDerivedFunctor α W → RF.IsLeftKanExtension α
mpr : RF.IsLeftKanExtension α → RF.IsRightDerivedFunctor α W
⊢ RF.IsRightDerivedFunctor α W ↔ RF.IsLeftKanExtension α

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
RF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
⊢ RF.IsRightDerivedFunctor α W → RF.IsLeftKanExtension α

Tactic:
fun _ => IsRightDerivedFunctor.isLeftKanExtension RF α W

Premises used: CategoryTheory.Functor.IsRightDerivedFunctor.isLeftKanExtension
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
RF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
⊢ RF.IsRightDerivedFunctor α W → RF.IsLeftKanExtension α

Tactic:
exact fun _ => IsRightDerivedFunctor.isLeftKanExtension RF α W
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
RF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
⊢ RF.IsLeftKanExtension α → RF.IsRightDerivedFunctor α W

Tactic:
fun h => ⟨h⟩

Premises used: CategoryTheory.Functor.IsRightDerivedFunctor.mk
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
RF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : F ⟶ L ⋙ RF
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
⊢ RF.IsLeftKanExtension α → RF.IsRightDerivedFunctor α W

Tactic:
exact fun h => ⟨h⟩
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
RF RF' : Functor.{v_3, v_5, u_3, u_2} D H
F : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
α : F ⟶ L ⋙ RF
α' : F ⟶ L ⋙ RF'
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
e : RF ≅ RF'
comm : α ≫ L.whiskerLeft e.hom = α'
simp : RF.IsLeftKanExtension α ↔ RF'.IsLeftKanExtension α'
⊢ RF.IsRightDerivedFunctor α W ↔ RF'.IsRightDerivedFunctor α' W

Tactic:
simp only [isRightDerivedFunctor_iff_isLeftKanExtension]

Premises used: CategoryTheory.Functor.isRightDerivedFunctor_iff_isLeftKanExtension
-- Module: Mathlib.CategoryTheory.Functor.Derived.RightDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
RF RF' : Functor.{v_3, v_5, u_3, u_2} D H
F : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
α : F ⟶ L ⋙ RF
α' : F ⟶ L ⋙ RF'
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
e : RF ≅ RF'
comm : α ≫ L.whiskerLeft e.hom = α'
⊢ RF.IsLeftKanExtension α ↔ RF'.IsLeftKanExtension α'

Tactic:
isLeftKanExtension_iff_of_iso e _ _ comm

Premises used: CategoryTheory.Functor.isLeftKanExtension_iff_of_iso