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₃} 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 (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.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 (F.map w)
⊢ Eq (α :=
    obj (obj (const (StructuredArrow (L.obj Y) L)) s.pt)
        (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) ⟶
      (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk φ))
    (map (obj (const (StructuredArrow (L.obj Y) L)) s.pt) (StructuredArrow.homMk w ⋯) ≫ s.π.app (StructuredArrow.mk φ))
    (s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) ≫
      (StructuredArrow.proj (L.obj Y) L ⋙ F).map (StructuredArrow.homMk w ⋯))

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

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

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

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

Tactic:
simp only [← cancel_mono (F.map w), ← eq, comp_obj, comp_map, assoc,
        ← hφ, ← NatTrans.naturality, ← G.map_comp_assoc,
        Localization.isoOfHom_inv_hom_id, comp_id]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.Category.assoc, CategoryTheory.Localization.isoOfHom_inv_hom_id, CategoryTheory.cancel_mono, CategoryTheory.Category.comp_id, CategoryTheory.Functor.map, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.NatTrans.naturality, CategoryTheory.Functor.comp_map
-- 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)
m : s.pt ⟶ Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y))
hm :
  ∀ (j : StructuredArrow (L.obj Y) L),
    m ≫ NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y))) j = s.π.app j
⊢ Eq (α := s.pt ⟶ (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (𝟙 (L.obj Y))))
    (m ≫ NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y))) (StructuredArrow.mk (𝟙 (L.obj Y))))
    (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))))

Tactic:
have := hm (StructuredArrow.mk (𝟙 (L.obj Y)))
-- 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)
m : s.pt ⟶ Cone.pt (J := StructuredArrow (L.obj Y) L) ((RightExtension.mk G e.inv).coneAt (L.obj Y))
hm :
  ∀ (j : StructuredArrow (L.obj Y) L),
    m ≫ NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y))) j = s.π.app j
this :
  Eq (α := s.pt ⟶ (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (𝟙 (L.obj Y))))
    (m ≫ NatTrans.app (Cone.π ((RightExtension.mk G e.inv).coneAt (L.obj Y))) (StructuredArrow.mk (𝟙 (L.obj Y))))
    (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))))
dsimp : m = s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y
⊢ m = s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y

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

Tactic:
simp [← reassoc_of% this]
-- 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
hF : W.IsInvertedBy F
X : C
rw : W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj X)
⊢ F.HasPointwiseLeftDerivedFunctorAt W X

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

Tactic:
(isPointwiseRightKanExtensionOfIsoOfIsLocalization W
    (Localization.fac F hF W.Q).symm).hasPointwiseRightKanExtension _

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsoOfIsLocalization, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hasPointwiseRightKanExtension, CategoryTheory.Iso.symm, CategoryTheory.Localization.fac
-- 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
hF : W.IsInvertedBy F
X : C
⊢ W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj X)

Tactic:
exact (isPointwiseRightKanExtensionOfIsoOfIsLocalization W
    (Localization.fac F hF W.Q).symm).hasPointwiseRightKanExtension _

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsoOfIsLocalization, CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hasPointwiseRightKanExtension, CategoryTheory.Iso.symm, CategoryTheory.Localization.fac
-- 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
inst_3 : L.IsLocalization W
hF : W.IsInvertedBy F
⊢ (Localization.lift (W := W) F hF L).IsLeftDerivedFunctor (Iso.hom (Localization.fac (W := W) F hF L)) W

Tactic:
isLeftDerivedFunctor_of_inverts W _ _

Premises used: CategoryTheory.Functor.isLeftDerivedFunctor_of_inverts
-- 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
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
LF : Functor.{v₂, v₃, u₂, u₃} D H
α : L ⋙ LF ⟶ F
hF : W.IsInvertedBy F
inst_4 : LF.IsLeftDerivedFunctor α W
⊢ α =
    CategoryStruct.comp (Y := L ⋙ Localization.lift (W := W) F hF L)
      (L.whiskerLeft
        (Iso.inv
          (LF.leftDerivedUnique (Localization.lift (W := W) F hF L) (Iso.hom (Localization.fac (W := W) F hF L)) α W)))
      (Iso.hom (Localization.fac (W := W) F hF L))

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
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
LF : Functor.{v₂, v₃, u₂, u₃} D H
α : L ⋙ LF ⟶ F
hF : W.IsInvertedBy F
inst_4 : LF.IsLeftDerivedFunctor α W
⊢ α =
    CategoryStruct.comp (Y := L ⋙ Localization.lift (W := W) F hF L)
      (L.whiskerLeft
        (Iso.inv
          (LF.leftDerivedUnique (Localization.lift (W := W) F hF L) (Iso.hom (Localization.fac (W := W) F hF L)) α W)))
      (Iso.hom (Localization.fac (W := W) F hF L))

Tactic:
have : α = whiskerLeft _ (leftDerivedUnique _ _ (Localization.fac F hF L).hom α W).inv ≫
      (Localization.fac F hF L).hom := by 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
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
LF : Functor.{v₂, v₃, u₂, u₃} D H
α : L ⋙ LF ⟶ F
hF : W.IsInvertedBy F
inst_4 : LF.IsLeftDerivedFunctor α W
this :
  α =
    CategoryStruct.comp (Y := L ⋙ Localization.lift (W := W) F hF L)
      (L.whiskerLeft
        (Iso.inv
          (LF.leftDerivedUnique (Localization.lift (W := W) F hF L) (Iso.hom (Localization.fac (W := W) F hF L)) α W)))
      (Iso.hom (Localization.fac (W := W) F hF L))
rw :
  IsIso
    (CategoryStruct.comp (Y := L ⋙ Localization.lift (W := W) F hF L)
      (L.whiskerLeft
        (Iso.inv
          (LF.leftDerivedUnique (Localization.lift (W := W) F hF L) (Iso.hom (Localization.fac (W := W) F hF L)) α W)))
      (Iso.hom (Localization.fac (W := W) F hF L)))
⊢ IsIso α

Tactic:
rw [this]
-- 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
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
LF : Functor.{v₂, v₃, u₂, u₃} D H
α : L ⋙ LF ⟶ F
hF : W.IsInvertedBy F
inst_4 : LF.IsLeftDerivedFunctor α W
this :
  α =
    CategoryStruct.comp (Y := L ⋙ Localization.lift (W := W) F hF L)
      (L.whiskerLeft
        (Iso.inv
          (LF.leftDerivedUnique (Localization.lift (W := W) F hF L) (Iso.hom (Localization.fac (W := W) F hF L)) α W)))
      (Iso.hom (Localization.fac (W := W) F hF L))
⊢ IsIso
    (CategoryStruct.comp (Y := L ⋙ Localization.lift (W := W) F hF L)
      (L.whiskerLeft
        (Iso.inv
          (LF.leftDerivedUnique (Localization.lift (W := W) F hF L) (Iso.hom (Localization.fac (W := W) F hF L)) α W)))
      (Iso.hom (Localization.fac (W := W) F hF L)))

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
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
LF : Functor.{v₂, v₃, u₂, u₃} D H
α : L ⋙ LF ⟶ F
hF : W.IsInvertedBy F
⊢ LF.IsLeftDerivedFunctor α W ↔ IsIso α

Tactic:
⟨fun _ ↦ isIso_of_isLeftDerivedFunctor_of_inverts LF α hF, fun _ ↦
    isLeftDerivedFunctor_of_inverts W LF (asIso α)⟩

Premises used: CategoryTheory.Functor.isLeftDerivedFunctor_of_inverts, CategoryTheory.Functor.isIso_of_isLeftDerivedFunctor_of_inverts, Iff.intro, CategoryTheory.asIso
-- 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
rw : F.HasPointwiseRightDerivedFunctorAt W X ↔ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X)
⊢ F.HasPointwiseRightDerivedFunctorAt W X ↔ L.HasPointwiseLeftKanExtensionAt F (L.obj X)

Tactic:
rw [← hasPointwiseLeftKanExtensionAt_iff_of_equivalence W.Q L F
    (Localization.uniq W.Q L W) (Localization.compUniqFunctor W.Q L W) (W.Q.obj X) (L.obj X)
    ((Localization.compUniqFunctor W.Q L W).app X)]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.hasPointwiseLeftKanExtensionAt_iff_of_equivalence, CategoryTheory.Localization.uniq, CategoryTheory.Localization.compUniqFunctor, CategoryTheory.Iso.app, CategoryTheory.Functor.obj
-- 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:
⟨fun h ↦ h.hasColimit', fun h ↦ ⟨h⟩⟩

Premises used: CategoryTheory.Functor.HasPointwiseRightDerivedFunctorAt.mk, Iff.intro, CategoryTheory.Functor.HasPointwiseRightDerivedFunctorAt.hasColimit'