-- Mathlib/CategoryTheory/Filtered/CostructuredArrow.lean
private lemma isFiltered_of_isFiltered_costructuredArrow_small (L : A ⥤ T) (R : B ⥤ T)
    [IsFiltered B] [Final R] [∀ b, IsFiltered (CostructuredArrow L (R.obj b))] : IsFiltered A

Proof state:
A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
b : B
⊢ PreservesLimitsOfShape J colim

Tactic:
exact filtered_colim_preservesFiniteLimits

Result:
no goals

Proof state:
A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
⊢ IsFiltered A

Tactic:
refine isFiltered_of_nonempty_limit_colimit_to_colimit_limit fun J {_ _} F => ⟨?_⟩

Result:
A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
⊢ limit (colimit F.flip) ⟶ colimit (limit F)

Proof state:
A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
⊢ limit (colimit F.flip) ⟶ colimit (limit F)

Tactic:
let R' := Grothendieck.pre (CostructuredArrow.functor L) R

Result:
A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
⊢ limit (colimit F.flip) ⟶ colimit (limit F)

Proof state:
A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
this : ∀ (b : B), PreservesLimitsOfShape J colim
⊢ limit (colimit F.flip) ⟶ colimit (limit F)

Tactic:
refine lim.map ((colimitIsoColimitGrothendieck L F.flip).hom ≫
  (inv (colimit.pre (CostructuredArrow.grothendieckProj L ⋙ F.flip) R'))) ≫
  (colimitLimitIso (R' ⋙ CostructuredArrow.grothendieckProj L ⋙ F.flip).flip).inv ≫
  colim.map ?_ ≫
  colimit.pre _ R' ≫
  (colimitIsoColimitGrothendieck L (limit F)).inv

Result:
A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
this : ∀ (b : B), PreservesLimitsOfShape J colim
⊢ limit (R' ⋙ CostructuredArrow.grothendieckProj L ⋙ F.flip).flip ⟶ R' ⋙ CostructuredArrow.grothendieckProj L ⋙ limit F

Proof state:
A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
this : ∀ (b : B), PreservesLimitsOfShape J colim
⊢ limit (R' ⋙ CostructuredArrow.grothendieckProj L ⋙ F.flip).flip ⟶ R' ⋙ CostructuredArrow.grothendieckProj L ⋙ limit F

Tactic:
exact (limitCompWhiskeringLeftIsoCompLimit F (R' ⋙ CostructuredArrow.grothendieckProj L)).hom

Result:
no goals

Proof state:
A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
⊢ limit (colimit F.flip) ⟶ colimit (limit F)

Tactic:
haveI : ∀ b, PreservesLimitsOfShape J
    (colim (J := (R ⋙ CostructuredArrow.functor L).obj b) (C := Type u₁)) := fun b => by
  simp only [comp_obj, CostructuredArrow.functor_obj, Cat.of_α]
  exact filtered_colim_preservesFiniteLimits

Result:
A : Type u₁
inst✝⁵ : SmallCategory A
B : Type u₁
inst✝⁴ : SmallCategory B
T : Type u₁
inst✝³ : SmallCategory T
L : A ⥤ T
R : B ⥤ T
inst✝² : IsFiltered B
inst✝¹ : R.Final
inst✝ : ∀ (b : B), IsFiltered (CostructuredArrow L (R.obj b))
J : Type u₁
x✝¹ : SmallCategory J
x✝ : FinCategory J
F : J ⥤ A ⥤ Type u₁
R' : Grothendieck (R ⋙ CostructuredArrow.functor L) ⥤ Grothendieck (CostructuredArrow.functor L) :=
  Grothendieck.pre (CostructuredArrow.functor L) R
this : ∀ (b : B), PreservesLimitsOfShape J colim
⊢ limit (colimit F.flip) ⟶ colimit (limit F)