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₃} 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 (𝟙 (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)))
have 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)
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
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)))
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φ, this, 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)
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
⊢ m = s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y
have 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))))
Tactic: have := hm (StructuredArrow.mk (𝟙 (L.obj Y)))
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived (goal)
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
⊢ F.HasPointwiseLeftDerivedFunctorAt W X
have rw : W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj X)
Tactic: rw [hasPointwiseLeftDerivedFunctorAt_iff F W.Q W]
-- 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
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
⊢ IsIso α
have 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))
Tactic: have : α = whiskerLeft _ (leftDerivedUnique _ _ (Localization.fac F hF L).hom α W).inv ≫
      (Localization.fac F hF L).hom := by simp
-- 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
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 α
have 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)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (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 : L.IsLocalization W
X : C
⊢ F.HasPointwiseRightDerivedFunctorAt W X ↔ L.HasPointwiseLeftKanExtensionAt F (L.obj X)
have rw : F.HasPointwiseRightDerivedFunctorAt W X ↔ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.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)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (goal)
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
⊢ F.HasPointwiseRightDerivedFunctorAt W X ↔ F.HasPointwiseRightDerivedFunctorAt W Y
have simp : W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X) ↔ W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj Y)
Tactic: simp only [F.hasPointwiseRightDerivedFunctorAt_iff W.Q W]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (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.HasPointwiseRightDerivedFunctor W
inst_4 : L.IsLocalization W
Y : D
⊢ L.HasPointwiseLeftKanExtensionAt F Y
have this : L.EssSurj
Tactic: have := Localization.essSurj L W
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (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.HasPointwiseRightDerivedFunctor W
inst_4 : L.IsLocalization W
Y : D
this : L.EssSurj
⊢ L.HasPointwiseLeftKanExtensionAt F Y
have rw : F.HasPointwiseRightDerivedFunctorAt W (L.objPreimage Y)
Tactic: rw [← hasPointwiseLeftKanExtensionAt_iff_of_iso _ F (L.objObjPreimageIso Y),
    ← F.hasPointwiseRightDerivedFunctorAt_iff L W]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (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.HasPointwiseRightDerivedFunctor W
⊢ W.Q.HasLeftKanExtension F
have this : W.Q.HasPointwiseLeftKanExtension F
Tactic: have := F.hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor W.Q W
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (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
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
⊢ CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        j)
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) j)
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app j
have refine_1 : ∀ (X₁ X₂ : C) (f : X₁ ⟶ X₂) (φ : L.obj X₂ ⟶ L.obj Y)
  (hφ :
    CategoryStruct.comp (Y :=
        obj
          (obj (const (CostructuredArrow L (L.obj Y)))
            (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
          (CostructuredArrow.mk φ))
        (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk φ))
        (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
      s.ι.app (CostructuredArrow.mk φ)),
  CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk (L.map f ≫ φ)))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk (L.map f ≫ φ)))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk (L.map f ≫ φ))
Tactic: refine Localization.induction_costructuredArrow 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.PointwiseRightDerived (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
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk φ))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk φ))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk φ)
⊢ CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk (L.map f ≫ φ)))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk (L.map f ≫ φ)))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk (L.map f ≫ φ))
have eq : Eq (α :=
  obj (CostructuredArrow.proj L (L.obj Y) ⋙ F) (CostructuredArrow.mk (L.map f ≫ φ)) ⟶
    obj (obj (const (CostructuredArrow L (L.obj Y))) s.pt) (CostructuredArrow.mk φ))
  (map (CostructuredArrow.proj L (L.obj Y) ⋙ F) (CostructuredArrow.homMk f sorry) ≫ s.ι.app (CostructuredArrow.mk φ))
  (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)) ≫
    map (obj (const (CostructuredArrow L (L.obj Y))) s.pt) (CostructuredArrow.homMk f sorry))
Tactic: have eq := s.ι.naturality
        (CostructuredArrow.homMk f : CostructuredArrow.mk (L.map f ≫ φ) ⟶ CostructuredArrow.mk φ)
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (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
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk φ))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk φ))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk φ)
eq :
  Eq (α :=
    obj (CostructuredArrow.proj L (L.obj Y) ⋙ F) (CostructuredArrow.mk (L.map f ≫ φ)) ⟶
      obj (obj (const (CostructuredArrow L (L.obj Y))) s.pt) (CostructuredArrow.mk φ))
    (map (CostructuredArrow.proj L (L.obj Y) ⋙ F) (CostructuredArrow.homMk f ⋯) ≫ s.ι.app (CostructuredArrow.mk φ))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)) ≫
      map (obj (const (CostructuredArrow L (L.obj Y))) s.pt) (CostructuredArrow.homMk f ⋯))
⊢ CategoryStruct.comp (Y :=
      obj
        (obj (const (CostructuredArrow L (L.obj Y)))
          (Cocone.pt (J := CostructuredArrow L (L.obj Y)) ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))))
        (CostructuredArrow.mk (L.map f ≫ φ)))
      (NatTrans.app (Cocone.ι ((LeftExtension.mk G e.hom).coconeAt (L.obj Y))) (CostructuredArrow.mk (L.map f ≫ φ)))
      (e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))) =
    s.ι.app (CostructuredArrow.mk (L.map f ≫ φ))
have refine_1 : Eq (α := F.obj X₁ ⟶ s.pt)
  ((e.hom.app X₁ ≫ G.map (L.map f ≫ φ)) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
  (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
Tactic: dsimp at eq hφ ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (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
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  Eq (α := F.obj X₂ ⟶ s.pt) ((e.hom.app X₂ ≫ G.map φ) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk φ))
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map f ≫ s.ι.app (CostructuredArrow.mk φ))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)) ≫ 𝟙 s.pt)
⊢ Eq (α := F.obj X₁ ⟶ s.pt)
    ((e.hom.app X₁ ≫ G.map (L.map f ≫ φ)) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
have eq₁ : Eq (α := F.obj X₁ ⟶ s.pt) (F.map f ≫ s.ι.app (CostructuredArrow.mk φ)) (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
Tactic: rw [comp_id] at eq
Cleared hypotheses: eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (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
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  Eq (α := F.obj X₂ ⟶ s.pt) ((e.hom.app X₂ ≫ G.map φ) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk φ))
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map f ≫ s.ι.app (CostructuredArrow.mk φ)) (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
⊢ Eq (α := F.obj X₁ ⟶ s.pt)
    ((e.hom.app X₁ ≫ G.map (L.map f ≫ φ)) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
have 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 φ))
Tactic: rw [assoc] at hφ
Cleared hypotheses: hφ, eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (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
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  Eq (α := F.obj X₂ ⟶ s.pt) (e.hom.app X₂ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk φ))
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map f ≫ s.ι.app (CostructuredArrow.mk φ)) (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
⊢ Eq (α := F.obj X₁ ⟶ s.pt)
    ((e.hom.app X₁ ≫ G.map (L.map f ≫ φ)) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
have refine_1 : Eq (α := F.obj X₁ ⟶ s.pt)
  (e.hom.app X₁ ≫ G.map (L.map f ≫ φ) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
  (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
Tactic: rw [assoc, map_comp_assoc, ← eq, ← hφ, NatTrans.naturality_assoc, comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (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
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  Eq (α := F.obj X₂ ⟶ s.pt) (e.hom.app X₂ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk φ))
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map f ≫ s.ι.app (CostructuredArrow.mk φ)) (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
refine_1 :
  Eq (α := F.obj X₁ ⟶ s.pt)
    (e.hom.app X₁ ≫ G.map (L.map f ≫ φ) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
⊢ Eq (α := F.obj X₁ ⟶ s.pt)
    ((e.hom.app X₁ ≫ G.map (L.map f ≫ φ)) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
have refine_1₁ : Eq (α := F.obj X₁ ⟶ s.pt)
  (e.hom.app X₁ ≫ G.map (L.map f) ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
  (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
Tactic: rw [assoc, map_comp_assoc, ← eq, ← hφ, NatTrans.naturality_assoc, comp_map]
-- Lean 4 proof step from Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (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
α : F ⟶ L ⋙ F'
W : MorphismProperty.{v₁, u₁} C
G : Functor.{v₂, v₃, u₂, u₃} D H
e : F ≅ L ⋙ G
inst_3 : L.IsLocalization W
Y : C
s : Cocone (J := CostructuredArrow L (L.obj Y)) (CostructuredArrow.proj L (L.obj Y) ⋙ F)
j : CostructuredArrow L (L.obj Y)
X₁ X₂ : C
f : X₁ ⟶ X₂
φ : L.obj X₂ ⟶ L.obj Y
hφ :
  Eq (α := F.obj X₂ ⟶ s.pt) (e.hom.app X₂ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk φ))
eq :
  Eq (α := F.obj X₁ ⟶ s.pt) (F.map f ≫ s.ι.app (CostructuredArrow.mk φ)) (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
refine_1 :
  Eq (α := F.obj X₁ ⟶ s.pt)
    (e.hom.app X₁ ≫ G.map (L.map f ≫ φ) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
refine_1₁ :
  Eq (α := F.obj X₁ ⟶ s.pt)
    (e.hom.app X₁ ≫ G.map (L.map f) ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
⊢ Eq (α := F.obj X₁ ⟶ s.pt)
    ((e.hom.app X₁ ≫ G.map (L.map f ≫ φ)) ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
    (s.ι.app (CostructuredArrow.mk (L.map f ≫ φ)))
have refine_1₂ : Eq (α := F.obj X₁ ⟶ s.pt)
  (e.hom.app X₁ ≫ G.map (L.map f) ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
  (F.map f ≫ s.ι.app (CostructuredArrow.mk φ))
Tactic: rw [assoc, map_comp_assoc, ← eq, ← hφ, NatTrans.naturality_assoc, comp_map]