awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 ≫ φ)))
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 φ))
⊢ 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 ≫ e.hom.app X₂ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
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 ≫ φ)))
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 φ))
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 ≫ 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 (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))))
  (e.hom.app X₁ ≫ (L ⋙ G).map f ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
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 ≫ φ)))
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 φ))
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 ≫ e.hom.app X₂ ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
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))))
    (e.hom.app X₁ ≫ (L ⋙ G).map f ≫ 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 (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))))
  (e.hom.app X₁ ≫ G.map (L.map f) ≫ G.map φ ≫ e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y))))
Tactic: rw [assoc, map_comp_assoc, ← eq, ← hφ, NatTrans.naturality_assoc, comp_map]
-- 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
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 φ)
⊢ 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.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
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 (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.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
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 (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.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
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 φ)
⊢ 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 ≫ φ))
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.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
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)
⊢ 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 ≫ φ))
have 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 sorry) ≫
    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 sorry))
Tactic: have eq := s.ι.naturality
        (CostructuredArrow.homMk w : CostructuredArrow.mk φ ⟶ CostructuredArrow.mk
          ((Localization.isoOfHom L W w hw).inv ≫ φ))
-- 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
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 ⋯))
⊢ 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 ≫ φ))
have 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 ≫ φ)))
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
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)
    ((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 ≫ φ)))
have 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 φ))
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
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 ((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 ≫ φ)))
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φ, this, 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
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 ((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 ≫ φ)))
have 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))))
Tactic: rw [map_comp, assoc, assoc, ← cancel_epi (F.map w), eq, ← hφ,
        NatTrans.naturality_assoc, comp_map, ← G.map_comp_assoc]
-- 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)
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
⊢ m = e.inv.app Y ≫ s.ι.app (CostructuredArrow.mk (𝟙 (L.obj Y)))
have 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)))
Tactic: have := hm (CostructuredArrow.mk (𝟙 (L.obj Y)))
-- 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
hF : W.IsInvertedBy F
X : C
⊢ F.HasPointwiseRightDerivedFunctorAt W X
have rw : W.Q.HasPointwiseLeftKanExtensionAt F (W.Q.obj X)
Tactic: rw [hasPointwiseRightDerivedFunctorAt_iff F 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
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
⊢ IsIso α
have 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
Tactic: have : α = (Localization.fac F hF L).inv ≫
    whiskerLeft _ (rightDerivedUnique _ _ (Localization.fac F hF L).inv α W).hom := by simp