mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ ψ ≫ map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ) = τ

pp: case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ ∀ (y : c ⟶ c'), (fun χ ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)

Tactic:
·

Goal state after:
case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ ψ ≫ map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ) = τ
Module: Mathlib.CategoryTheory.FiberedCategory.Cocartesian

Goal state before:
pp: case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ ∀ (y : c ⟶ c'), (fun χ ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)

Tactic:
·

Goal state after:
case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝⁴ : Category.{v₁, u₁} 𝒮
inst✝³ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
R S T : 𝒮
a b c : 𝒳
f : R ⟶ S
g : S ⟶ T
φ : a ⟶ b
ψ : b ⟶ c
inst✝² : p.IsStronglyCocartesian f φ
inst✝¹ : p.IsStronglyCocartesian (f ≫ g) (φ ≫ ψ)
inst✝ : p.IsHomLift g ψ
c' : 𝒳
h : T ⟶ p.obj c'
τ : b ⟶ c'
hτ : p.IsHomLift (g ≫ h) τ
⊢ ∀ (y : c ⟶ c'), (fun χ ↦ p.IsHomLift h χ ∧ ψ ≫ χ = τ) y → y = map p (f ≫ g) (φ ≫ ψ) ⋯ (φ ≫ τ)
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: case refine_1
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ homCartesianLift f g φ' ≫ cartesianLift a f = φ'

pp: case refine_2
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ ∀ (y : a' ⟶ domainCartesianLift a f),
    (fun χ ↦ (forget F).IsHomLift g χ ∧ χ ≫ cartesianLift a f = φ') y → y = homCartesianLift f g φ'

Tactic:
·

Goal state after:
case refine_1
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
R S : 𝒮
a : ↑(F.obj { as := op S })
f : R ⟶ S
a' : ∫ᶜ F
g : (forget F).obj a' ⟶ R
φ' : a' ⟶ { base := S, fiber := a }
hφ' : (forget F).IsHomLift (g ≫ f) φ'
⊢ homCartesianLift f g φ' ≫ cartesianLift a f = φ'
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: case hfg₁
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : ↑(F.obj { as := op S })
φ : a ⟶ b
ψ : b ⟶ c
⊢ { base := 𝟙 S, fiber := (φ ≫ ψ) ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }.base =
    ({ base := 𝟙 S, fiber := φ ≫ (F.mapId { as := op S }).inv.toNatTrans.app b } ≫
        { base := 𝟙 S, fiber := ψ ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }).base

pp: case hfg₂
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : ↑(F.obj { as := op S })
φ : a ⟶ b
ψ : b ⟶ c
⊢ { base := 𝟙 S, fiber := (φ ≫ ψ) ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }.fiber =
    ({ base := 𝟙 S, fiber := φ ≫ (F.mapId { as := op S }).inv.toNatTrans.app b } ≫
          { base := 𝟙 S, fiber := ψ ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }).fiber ≫
      eqToHom ⋯

Tactic:
·

Goal state after:
case hfg₁
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : ↑(F.obj { as := op S })
φ : a ⟶ b
ψ : b ⟶ c
⊢ { base := 𝟙 S, fiber := (φ ≫ ψ) ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }.base =
    ({ base := 𝟙 S, fiber := φ ≫ (F.mapId { as := op S }).inv.toNatTrans.app b } ≫
        { base := 𝟙 S, fiber := ψ ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }).base
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: case hfg₂
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : ↑(F.obj { as := op S })
φ : a ⟶ b
ψ : b ⟶ c
⊢ { base := 𝟙 S, fiber := (φ ≫ ψ) ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }.fiber =
    ({ base := 𝟙 S, fiber := φ ≫ (F.mapId { as := op S }).inv.toNatTrans.app b } ≫
          { base := 𝟙 S, fiber := ψ ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }).fiber ≫
      eqToHom ⋯

Tactic:
·

Goal state after:
case hfg₂
𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : ↑(F.obj { as := op S })
φ : a ⟶ b
ψ : b ⟶ c
⊢ { base := 𝟙 S, fiber := (φ ≫ ψ) ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }.fiber =
    ({ base := 𝟙 S, fiber := φ ≫ (F.mapId { as := op S }).inv.toNatTrans.app b } ≫
          { base := 𝟙 S, fiber := ψ ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }).fiber ≫
      eqToHom ⋯
Module: Mathlib.CategoryTheory.FiberedCategory.Grothendieck

Goal state before:
pp: 𝒮 : Type u_1
inst✝ : Category.{v_1, u_1} 𝒮
F : LocallyDiscrete 𝒮ᵒᵖ ⥤ᵖ Cat
S : 𝒮
a b c : ↑(F.obj { as := op S })
φ : a ⟶ b
ψ : b ⟶ c
⊢ { base := 𝟙 S, fiber := (φ ≫ ψ) ≫ (F.mapId { as := op S }).inv.toNatTrans.app c } =
    { base := 𝟙 S, fiber := φ ≫ (F.mapId { as := op S }).inv.toNatTrans.app b } ≫
      { base := 𝟙 S, fiber := ψ ≫ (F.mapId { as := op S }).inv.toNatTrans.app c }

Tactic:
ext
    · simp
    · simp [← (F.mapId ⟨op S⟩).inv.toNatTrans.naturality_assoc ψ, F.whiskerRight_mapId_inv_app,
        Strict.leftUnitor_eqToIso, ← Cat.Hom₂.comp_app]

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: case refine_1
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ ∀ (X Y : Grothendieck F), ∃ Z x x, True

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ ∀ ⦃X Y : Grothendieck F⦄ (f g : X ⟶ Y), ∃ Z h, f ≫ h = g ≫ h

Tactic:
·

Goal state after:
case refine_1
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ ∀ (X Y : Grothendieck F), ∃ Z x x, True
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ ∀ ⦃X Y : Grothendieck F⦄ (f g : X ⟶ Y), ∃ Z h, f ≫ h = g ≫ h

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
⊢ ∀ ⦃X Y : Grothendieck F⦄ (f g : X ⟶ Y), ∃ Z h, f ≫ h = g ≫ h
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
c : C
f : ↑(F.obj c)
d : C
g : ↑(F.obj d)
u : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
⊢ (F.map (coeqHom u v)).toFunctor.obj ((F.map v).toFunctor.obj { base := c, fiber := f }.fiber) =
    (F.map (coeqHom u v)).toFunctor.obj ((F.map u).toFunctor.obj { base := c, fiber := f }.fiber)

pp: case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
c : C
f : ↑(F.obj c)
d : C
g : ↑(F.obj d)
u : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
⊢ { base := u, fiber := x } ≫
      { base := coeqHom u v,
        fiber :=
          coeqHom (eqToHom ?refine_2.refine_1 ≫ (F.map (coeqHom u v)).toFunctor.map x)
            ((F.map (coeqHom u v)).toFunctor.map y) } =
    { base := v, fiber := y } ≫
      { base := coeqHom u v,
        fiber :=
          coeqHom (eqToHom ?refine_2.refine_1 ≫ (F.map (coeqHom u v)).toFunctor.map x)
            ((F.map (coeqHom u v)).toFunctor.map y) }

Tactic:
·

Goal state after:
case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
c : C
f : ↑(F.obj c)
d : C
g : ↑(F.obj d)
u : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
⊢ (F.map (coeqHom u v)).toFunctor.obj ((F.map v).toFunctor.obj { base := c, fiber := f }.fiber) =
    (F.map (coeqHom u v)).toFunctor.obj ((F.map u).toFunctor.obj { base := c, fiber := f }.fiber)
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
c : C
f : ↑(F.obj c)
d : C
g : ↑(F.obj d)
u : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
| (F.map v ≫ F.map (coeqHom u v)).toFunctor.obj { base := c, fiber := f }.fiber

Tactic:
Cat.Hom.comp_obj

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
c : C
f : ↑(F.obj c)
d : C
g : ↑(F.obj d)
u : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
| (F.map (coeqHom u v)).toFunctor.obj ((F.map v).toFunctor.obj { base := c, fiber := f }.fiber)
Module: Mathlib.CategoryTheory.Filtered.Grothendieck

Goal state before:
pp: case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
c : C
f : ↑(F.obj c)
d : C
g : ↑(F.obj d)
u : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
⊢ { base := u, fiber := x } ≫
      { base := coeqHom u v,
        fiber := coeqHom (eqToHom ⋯ ≫ (F.map (coeqHom u v)).toFunctor.map x) ((F.map (coeqHom u v)).toFunctor.map y) } =
    { base := v, fiber := y } ≫
      { base := coeqHom u v,
        fiber := coeqHom (eqToHom ⋯ ≫ (F.map (coeqHom u v)).toFunctor.map x) ((F.map (coeqHom u v)).toFunctor.map y) }

Tactic:
·

Goal state after:
case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
F : C ⥤ Cat
inst✝¹ : IsFilteredOrEmpty C
inst✝ : ∀ (c : C), IsFilteredOrEmpty ↑(F.obj c)
c : C
f : ↑(F.obj c)
d : C
g : ↑(F.obj d)
u : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
x : (F.map u).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
v : { base := c, fiber := f }.base ⟶ { base := d, fiber := g }.base
y : (F.map v).toFunctor.obj { base := c, fiber := f }.fiber ⟶ { base := d, fiber := g }.fiber
⊢ { base := u, fiber := x } ≫
      { base := coeqHom u v,
        fiber := coeqHom (eqToHom ⋯ ≫ (F.map (coeqHom u v)).toFunctor.map x) ((F.map (coeqHom u v)).toFunctor.map y) } =
    { base := v, fiber := y } ≫
      { base := coeqHom u v,
        fiber := coeqHom (eqToHom ⋯ ≫ (F.map (coeqHom u v)).toFunctor.map x) ((F.map (coeqHom u v)).toFunctor.map y) }
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ LF.IsLeftDerivedFunctor α W → LF.IsRightKanExtension α

pp: case mpr
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ LF.IsRightKanExtension α → LF.IsLeftDerivedFunctor α W

Tactic:
·

Goal state after:
case mp
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ LF.IsLeftDerivedFunctor α W → LF.IsRightKanExtension α
Module: Mathlib.CategoryTheory.Functor.Derived.LeftDerived

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ LF.IsRightKanExtension α → LF.IsLeftDerivedFunctor α W

Tactic:
·

Goal state after:
case mpr
C : Type u_1
D : Type u_2
H : Type u_3
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_2} D
inst✝¹ : Category.{v_5, u_3} H
LF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ LF ⟶ F
W : MorphismProperty C
inst✝ : L.IsLocalization W
⊢ LF.IsRightKanExtension α → LF.IsLeftDerivedFunctor α W
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: case refine_1
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : 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φ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk φ)
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk (φ ≫ L.map f)) =
    s.π.app (StructuredArrow.mk (φ ≫ L.map f))

pp: case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : 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φ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk φ)
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app
        (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))

Tactic:
·

Goal state after:
case refine_1
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : 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φ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk φ)
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk (φ ≫ L.map f)) =
    s.π.app (StructuredArrow.mk (φ ≫ L.map f))
Module: Mathlib.CategoryTheory.Functor.Derived.Adjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : 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₂)
⊢ L₁.whiskerLeft
        (G'.leftUnitor.inv ≫ whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom) ≫
      α =
    L₁.whiskerLeft (𝟙 G') ≫ α

Tactic:
ext X₁

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst✝⁷ : Category.{v_1, u_1} C₁
inst✝⁶ : Category.{v_2, u_2} C₂
inst✝⁵ : Category.{v_3, u_3} D₁
inst✝⁴ : Category.{v_4, u_4} D₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
L₁ : C₁ ⥤ D₁
L₂ : C₂ ⥤ D₂
W₁ : MorphismProperty C₁
W₂ : MorphismProperty C₂
inst✝³ : L₁.IsLocalization W₁
inst✝² : L₂.IsLocalization W₂
G' : D₁ ⥤ D₂
F' : D₂ ⥤ D₁
α : L₁ ⋙ G' ⟶ G ⋙ L₂
β : F ⋙ L₁ ⟶ L₂ ⋙ F'
inst✝¹ : G'.IsLeftDerivedFunctor α W₁
inst✝ : 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₁
⊢ (L₁.whiskerLeft
            (G'.leftUnitor.inv ≫
              whiskerRight η G' ≫ (G'.associator F' G').hom ≫ G'.whiskerLeft ε ≫ G'.rightUnitor.hom) ≫
          α).app
      X₁ =
    (L₁.whiskerLeft (𝟙 G') ≫ α).app X₁
Module: Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived

Goal state before:
pp: case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : 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φ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk φ)
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app
        (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))

Tactic:
·

Goal state after:
case refine_2
C : Type u₁
D : Type u₂
H : Type u₃
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Category.{v₃, u₃} H
F' : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : L ⋙ F' ⟶ F
W : MorphismProperty C
G : D ⥤ H
e : F ≅ L ⋙ G
inst✝ : 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φ :
  (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app (StructuredArrow.mk φ) =
    s.π.app (StructuredArrow.mk φ)
⊢ (s.π.app (StructuredArrow.mk (𝟙 (L.obj Y))) ≫ e.hom.app Y) ≫
      ((RightExtension.mk G e.inv).coneAt (L.obj Y)).π.app
        (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv)) =
    s.π.app (StructuredArrow.mk (φ ≫ (Localization.isoOfHom L W w hw).inv))
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁴ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝³ : HasZeroMorphisms C
inst✝² : (i : I) → HasZeroMorphisms (D i)
inst✝¹ : ∀ (i : I), (F i).PreservesZeroMorphisms
inst✝ : HasZeroObject C
X : C
⊢ IsZero X ↔ ∀ (i : I), IsZero ((F i).obj X)

Tactic:
by
  refine ⟨fun hX _ ↦ Functor.map_isZero _ hX, fun hX ↦ ?_⟩
  let φ : 0 ⟶ X := 0
  have : IsIso φ := by
    rw [hP.isIso_iff]
    exact fun i ↦ (Functor.map_isZero _ (isZero_zero _)).isIso (hX i) _
  exact (isZero_zero C).of_iso (asIso φ).symm

Goal state after:
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : S.ShortExact
i : I
⊢ (S.map (F i)).ShortExact

pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).ShortExact
⊢ S.ShortExact

Tactic:
·

Goal state after:
case refine_1
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : S.ShortExact
i : I
⊢ (S.map (F i)).ShortExact
Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact

Goal state before:
pp: case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).ShortExact
⊢ S.ShortExact

Tactic:
·

Goal state after:
case refine_2
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst✝⁵ : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → C ⥤ D i
hP : JointlyReflectIsomorphisms F
inst✝⁴ : Abelian C
inst✝³ : (i : I) → Abelian (D i)
inst✝² : CategoryWithHomology C
inst✝¹ : ∀ (i : I), PreservesFiniteLimits (F i)
inst✝ : ∀ (i : I), PreservesFiniteColimits (F i)
S : ShortComplex C
hS : ∀ (i : I), (S.map (F i)).ShortExact
⊢ S.ShortExact