awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (hypothesis)
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.HasPointwiseRightKanExtensionAt F Y
have this : L.EssSurj
Tactic: have := Localization.essSurj L W
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (goal)
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
⊢ L.HasPointwiseRightKanExtensionAt F Y
have rw : F.HasPointwiseLeftDerivedFunctorAt W (L.objPreimage Y)
Tactic: rw [← hasPointwiseRightKanExtensionAt_iff_of_iso _ F (L.objObjPreimageIso Y),
    ← F.hasPointwiseLeftDerivedFunctorAt_iff L W]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (hypothesis)
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.HasRightKanExtension F
have this : W.Q.HasPointwiseRightKanExtension F
Tactic: have := F.hasPointwiseRightKanExtension_of_hasPointwiseLeftDerivedFunctor W.Q W
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (goal)
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))) j :
        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))))
            j ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj j) =
    s.π.app j
have refine_1 : ∀ (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 φ)),
  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: refine Localization.induction_structuredArrow L W _ (by simp)
      (fun X₁ X₂ f φ hφ ↦ ?_) (fun X₁ X₂ w hw φ hφ ↦ ?_) j
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (hypothesis)
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 φ)
⊢ 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))
have 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 sorry) ≫
    s.π.app (StructuredArrow.mk (φ ≫ L.map f)))
  (s.π.app (StructuredArrow.mk φ) ≫ (StructuredArrow.proj (L.obj Y) L ⋙ F).map (StructuredArrow.homMk f sorry))
Tactic: have eq := s.π.naturality
        (StructuredArrow.homMk f : StructuredArrow.mk φ ⟶ StructuredArrow.mk (φ ≫ L.map f))
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (goal)
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 ⋯))
⊢ 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))
have 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)))
Tactic: dsimp at eq hφ ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (hypothesis)
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.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)))
have 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)
Tactic: rw [id_comp] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (hypothesis)
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)))
have 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 φ))
Tactic: rw [assoc] at hφ
Cleared hypotheses: hφ, eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (hypothesis)
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)
have this : IsIso (L.map w)
Tactic: have := Localization.inverts L W w hw
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (goal)
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 (F.map w)
have rw : IsIso (e.hom.app X₁ ≫ (L ⋙ G).map w ≫ e.inv.app X₂)
Tactic: rw [← NatIso.naturality_2 e w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (goal)
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₁ ≫ (L ⋙ G).map w ≫ e.inv.app X₂)
have dsimp : IsIso (e.hom.app X₁ ≫ G.map (L.map w) ≫ e.inv.app X₂)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (hypothesis)
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 φ)
⊢ 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 (φ ≫ (Localization.isoOfHom L W w hw).inv)) :
        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 (φ ≫ (Localization.isoOfHom L W w hw).inv)) ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))) =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))
have this : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (hypothesis)
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)
⊢ 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 (φ ≫ (Localization.isoOfHom L W w hw).inv)) :
        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 (φ ≫ (Localization.isoOfHom L W w hw).inv)) ⟶
          (StructuredArrow.proj (L.obj Y) L ⋙ F).obj (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))) =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))
have eq : 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 sorry) ≫ 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 sorry))
Tactic: have eq := s.π.naturality (StructuredArrow.homMk w :
          StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv) ⟶
            StructuredArrow.mk φ)