awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_4 : L₁.IsLocalization W₁
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst_6 : G'.IsLeftDerivedFunctor α W₁
inst_7 : F'.IsRightDerivedFunctor β W₂
η : 𝟭 D₁ ⟶ G' ⋙ F'
ε : F' ⋙ G' ⟶ 𝟭 D₂
hη : ∀ (X₁ : C₁), η.app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)
hε : ∀ (X₂ : C₂), G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)
X₂ : C₂
eq₁ : β.app X₂ ≫ η.app (F'.obj (L₂.obj X₂)) = η.app (L₁.obj (F.obj X₂)) ≫ F'.map (G'.map (β.app X₂))
eq₂ : F'.map (G'.map (β.app X₂) ≫ ε.app (L₂.obj X₂)) = F'.map (α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂))
eq₃ : L₁.map (F.map (adj.counit.app X₂)) ≫ β.app X₂ = β.app (G.obj (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))
⊢ F'.map (G'.map (β.app X₂)) ≫ F'.map (ε.app (L₂.obj X₂)) =
    F'.map (α.app (F.obj X₂)) ≫ F'.map (L₂.map (adj.counit.app X₂))

Tactic:
simp only [Functor.map_comp] at eq₂

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst_5 : (G' ⋙ F').IsLeftDerivedFunctor ((L₁.associator G' F').inv ≫ whiskerRight α F') W₁
X₁ : C₁
⊢ (adj.derivedη W₁ α β).app (L₁.obj X₁) ≫ F'.map (α.app X₁) = L₁.map (adj.unit.app X₁) ≫ β.app (G.obj X₁)

Tactic:
simpa using ((G' ⋙ F').leftDerived_fac_app ((Functor.associator _ _ _).inv ≫
    whiskerRight α F') W₁ _ (L₁.rightUnitor.hom ≫ L₁.leftUnitor.inv ≫ whiskerRight adj.unit L₁ ≫
      (Functor.associator _ _ _).hom ≫ whiskerLeft G β ≫ (Functor.associator _ _ _).inv)) X₁

Premises used: CategoryTheory.Functor.leftDerived_fac_app, CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.unit, CategoryTheory.Functor.associator, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.leftUnitor, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_4 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst_5 : (F' ⋙ G').IsRightDerivedFunctor (whiskerRight β G' ≫ (L₂.associator F' G').hom) W₂
X₂ : C₂
⊢ G'.map (β.app X₂) ≫ (adj.derivedε W₂ α β).app (L₂.obj X₂) = α.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)

Tactic:
simpa using ((F' ⋙ G').rightDerived_fac_app
    (whiskerRight β G' ≫ (Functor.associator _ _ _).hom) W₂ _
    ((Functor.associator _ _ _).hom ≫ whiskerLeft F α ≫ (Functor.associator _ _ _).inv ≫
      whiskerRight adj.counit _ ≫ L₂.leftUnitor.hom ≫ L₂.rightUnitor.inv)) X₂

Premises used: CategoryTheory.Functor.rightDerived_fac_app, CategoryTheory.Functor.rightUnitor, CategoryTheory.Functor.comp, CategoryTheory.Functor.associator, CategoryTheory.Functor.whiskerLeft, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.whiskerRight, CategoryTheory.Functor.leftUnitor, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
LF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
mp : LF.IsLeftDerivedFunctor α W → LF.IsRightKanExtension α
mpr : LF.IsRightKanExtension α → LF.IsLeftDerivedFunctor α W
⊢ LF.IsLeftDerivedFunctor α W ↔ LF.IsRightKanExtension α

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

Tactic:
fun _ => IsLeftDerivedFunctor.isRightKanExtension LF α W

Premises used: CategoryTheory.Functor.IsLeftDerivedFunctor.isRightKanExtension
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
LF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
⊢ LF.IsLeftDerivedFunctor α W → LF.IsRightKanExtension α

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

Tactic:
fun h => ⟨h⟩

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

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

Tactic:
simp only [isLeftDerivedFunctor_iff_isRightKanExtension]

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

Tactic:
isRightKanExtension_iff_of_iso e _ _ comm

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

Tactic:
exact isRightKanExtension_iff_of_iso e _ _ comm

Premises used: CategoryTheory.Functor.isRightKanExtension_iff_of_iso
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
LF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : L ⋙ G ⟶ F
⊢ L.whiskerLeft (LF.leftDerivedLift α W G β) ≫ α = β

Tactic:
have := IsLeftDerivedFunctor.isRightKanExtension LF α W
  LF.liftOfIsRightKanExtension_fac α G β

Premises used: CategoryTheory.Functor.liftOfIsRightKanExtension_fac, CategoryTheory.Functor.leftDerivedLift, CategoryTheory.Functor.IsLeftDerivedFunctor.isRightKanExtension
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
LF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : L ⋙ G ⟶ F
X : C
⊢ (LF.leftDerivedLift α W G β).app (L.obj X) ≫ α.app X = β.app X

Tactic:
have := IsLeftDerivedFunctor.isRightKanExtension LF α W
  LF.liftOfIsRightKanExtension_fac_app α G β X

Premises used: CategoryTheory.Functor.liftOfIsRightKanExtension_fac_app, CategoryTheory.Functor.IsLeftDerivedFunctor.isRightKanExtension
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
LF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
γ₁ γ₂ : G ⟶ LF
hγ : L.whiskerLeft γ₁ ≫ α = L.whiskerLeft γ₂ ≫ α
⊢ γ₁ = γ₂

Tactic:
have := IsLeftDerivedFunctor.isRightKanExtension LF α W
  LF.hom_ext_of_isRightKanExtension α γ₁ γ₂ hγ

Premises used: CategoryTheory.Functor.hom_ext_of_isRightKanExtension, CategoryTheory.Functor.IsLeftDerivedFunctor.isRightKanExtension
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
LF' LF : Functor.{v_3, v_5, u_3, u_2} D H
F F' : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
α' : L ⋙ LF' ⟶ F'
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
τ : F' ⟶ F
⊢ L.whiskerLeft (LF.leftDerivedLift α W LF' (α' ≫ τ)) ≫ α = α' ≫ τ

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
LF' LF : Functor.{v_3, v_5, u_3, u_2} D H
F F' : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
α' : L ⋙ LF' ⟶ F'
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
τ : F' ⟶ F
X : C
dsimp : (LF.leftDerivedLift α W LF' (α' ≫ τ)).app (L.obj X) ≫ α.app X = α'.app X ≫ τ.app X
⊢ (LF'.leftDerivedNatTrans LF α' α W τ).app (L.obj X) ≫ α.app X = α'.app X ≫ τ.app X

Tactic:
dsimp only [leftDerivedNatTrans]

Premises used: CategoryTheory.Functor.leftDerivedNatTrans
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
LF' LF : Functor.{v_3, v_5, u_3, u_2} D H
F F' : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
α' : L ⋙ LF' ⟶ F'
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
τ : F' ⟶ F
X : C
⊢ (LF.leftDerivedLift α W LF' (α' ≫ τ)).app (L.obj X) ≫ α.app X = α'.app X ≫ τ.app X

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
LF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
⊢ L.whiskerLeft (LF.leftDerivedNatTrans LF α α W (𝟙 F)) ≫ α = L.whiskerLeft (𝟙 LF) ≫ α

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
LF'' LF' LF : Functor.{v_3, v_5, u_3, u_2} D H
F F' F'' : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
α'' : L ⋙ LF'' ⟶ F''
α' : L ⋙ LF' ⟶ F'
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
inst_5 : LF'.IsLeftDerivedFunctor α' W
τ' : F'' ⟶ F'
τ : F' ⟶ F
⊢ L.whiskerLeft (LF''.leftDerivedNatTrans LF' α'' α' W τ' ≫ LF'.leftDerivedNatTrans LF α' α W τ) ≫ α =
    L.whiskerLeft (LF''.leftDerivedNatTrans LF α'' α W (τ' ≫ τ)) ≫ α

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
LF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : L ⋙ G ⟶ F
rw : G.IsRightKanExtension β ↔ IsIso (LF.leftDerivedLift α W G β)
⊢ G.IsLeftDerivedFunctor β W ↔ IsIso (LF.leftDerivedLift α W G β)

Tactic:
rw [isLeftDerivedFunctor_iff_isRightKanExtension]

Premises used: CategoryTheory.Functor.isLeftDerivedFunctor_iff_isRightKanExtension
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
LF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : L ⋙ G ⟶ F
⊢ LF.IsRightKanExtension α

Tactic:
have := IsLeftDerivedFunctor.isRightKanExtension _ α W
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
LF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : L ⋙ G ⟶ F
this : LF.IsRightKanExtension α
⊢ L.whiskerLeft (LF.leftDerivedLift α W G β) ≫ α = β

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_3
D : Type u_1
H : Type u_2
inst : Category.{v_1, u_3} C
inst_1 : Category.{v_3, u_1} D
inst_2 : Category.{v_5, u_2} H
LF : Functor.{v_3, v_5, u_1, u_2} D H
F : Functor.{v_1, v_5, u_3, u_2} C H
L : Functor.{v_1, v_3, u_3, u_1} C D
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_3} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
G : Functor.{v_3, v_5, u_1, u_2} D H
β : L ⋙ G ⟶ F
this : LF.IsRightKanExtension α
⊢ G.IsRightKanExtension β ↔ IsIso (LF.leftDerivedLift α W G β)

Tactic:
exact isRightKanExtension_iff_isIso _ α _ (by simp)

Premises used: CategoryTheory.Functor.isRightKanExtension_iff_isIso
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
F : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
⊢ F.HasLeftDerivedFunctor W ↔ W.Q.HasRightKanExtension F

Tactic:
have : HasLeftDerivedFunctor F W ↔ HasRightKanExtension W.Q F :=
    ⟨fun h => h.hasRightKanExtension', fun h => ⟨h⟩⟩
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
F : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
this : F.HasLeftDerivedFunctor W ↔ W.Q.HasRightKanExtension F
rw : W.Q.HasRightKanExtension F ↔ L.HasRightKanExtension F
rw₁ rw₂ : W.Q.HasRightKanExtension F ↔ W.Q.HasRightKanExtension F
⊢ F.HasLeftDerivedFunctor W ↔ L.HasRightKanExtension F

Tactic:
rw [this, hasRightExtension_iff_postcomp₁ (Localization.compUniqFunctor W.Q L W) F]

Premises used: CategoryTheory.MorphismProperty.Q, CategoryTheory.Localization.compUniqFunctor, CategoryTheory.Functor.hasRightExtension_iff_postcomp₁
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_1
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_5, u_2} H
F F' : Functor.{v_1, v_5, u_1, u_2} C H
e : F ≅ F'
W : MorphismProperty.{v_1, u_1} C
rw : W.Q.HasRightKanExtension F ↔ F'.HasLeftDerivedFunctor W
rw₁ : W.Q.HasRightKanExtension F ↔ W.Q.HasRightKanExtension F'
rw₂ rw₃ : W.Q.HasRightKanExtension F' ↔ W.Q.HasRightKanExtension F'
⊢ F.HasLeftDerivedFunctor W ↔ F'.HasLeftDerivedFunctor W

Tactic:
rw [hasLeftDerivedFunctor_iff F W.Q W, hasLeftDerivedFunctor_iff F' W.Q W,
    hasRightExtension_iff_of_iso₂ W.Q e]

Premises used: CategoryTheory.Functor.hasLeftDerivedFunctor_iff, CategoryTheory.MorphismProperty.Q, CategoryTheory.Functor.hasRightExtension_iff_of_iso₂
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_1
D : Type u_3
H : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_3} D
inst_2 : Category.{v_5, u_2} H
F : Functor.{v_1, v_5, u_1, u_2} C H
L : Functor.{v_1, v_3, u_1, u_3} C D
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : F.HasLeftDerivedFunctor W
⊢ L.HasRightKanExtension F

Tactic:
simpa only [← hasLeftDerivedFunctor_iff F L W]

Premises used: CategoryTheory.Functor.hasLeftDerivedFunctor_iff
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
LF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
⊢ LF.IsRightKanExtension α

Tactic:
have := IsLeftDerivedFunctor.isRightKanExtension LF α W
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_1
D : Type u_2
H : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_3, u_2} D
inst_2 : Category.{v_5, u_3} H
LF : Functor.{v_3, v_5, u_2, u_3} D H
F : Functor.{v_1, v_5, u_1, u_3} C H
L : Functor.{v_1, v_3, u_1, u_2} C D
α : L ⋙ LF ⟶ F
W : MorphismProperty.{v_1, u_1} C
inst_3 : L.IsLocalization W
inst_4 : LF.IsLeftDerivedFunctor α W
this : LF.IsRightKanExtension α
⊢ F.HasLeftDerivedFunctor W

Tactic:
simpa only [hasLeftDerivedFunctor_iff F L W] using HasRightKanExtension.mk LF α

Premises used: CategoryTheory.Functor.HasRightKanExtension.mk, CategoryTheory.Functor.hasLeftDerivedFunctor_iff
-- Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived
Goal:
C : Type u_1
C' : Type ?u.110414
D : Type u_2
D' : Type ?u.110420
H : Type u_3
H' : Type ?u.110426
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, ?u.110414} C'
inst_2 : Category.{v_3, u_2} D
inst_3 : Category.{v_4, ?u.110420} D'
inst_4 : Category.{v_5, u_3} H
inst_5 : Category.{v_6, ?u.110426} H'
LF'' LF' LF : Functor.{v_3, v_5, u_2, u_3} D H
F F' F'' : Functor.{v_1, v_5, u_1, u_3} C H
e : F ≅ F'
L : Functor.{v_1, v_3, u_1, u_2} C D
α'' : L ⋙ LF'' ⟶ F''
α' : L ⋙ LF' ⟶ F'
α : L ⋙ LF ⟶ F
α'₂ : L ⋙ LF' ⟶ F
W : MorphismProperty.{v_1, u_1} C
inst_6 : L.IsLocalization W
inst_7 : F.HasLeftDerivedFunctor W
⊢ (L.rightKanExtension F).IsRightKanExtension (L.rightKanExtensionCounit F)

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
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.HasPointwiseLeftDerivedFunctorAt W X ↔ W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj X)
⊢ F.HasPointwiseLeftDerivedFunctorAt W X ↔ L.HasPointwiseRightKanExtensionAt F (L.obj X)

Tactic:
rw [← hasPointwiseRightKanExtensionAt_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.Localization.uniq, CategoryTheory.Localization.compUniqFunctor, CategoryTheory.Functor.hasPointwiseRightKanExtensionAt_iff_of_equivalence, CategoryTheory.Iso.app, CategoryTheory.Functor.obj
-- 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₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
X : C
⊢ F.HasPointwiseLeftDerivedFunctorAt W X ↔ W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj X)

Tactic:
⟨fun h ↦ h.hasLimit', fun h ↦ ⟨h⟩⟩

Premises used: CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorAt.hasLimit', Iff.intro, CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorAt.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₃} C H
L : Functor.{v₁, v₂, u₁, u₂} C D
W : MorphismProperty.{v₁, u₁} C
inst_3 : L.IsLocalization W
X : C
⊢ F.HasPointwiseLeftDerivedFunctorAt W X ↔ W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj X)

Tactic:
exact ⟨fun h ↦ h.hasLimit', fun h ↦ ⟨h⟩⟩