Theorem: CategoryTheory.isSheafForDagurSieveIsIsoFork (Sieves/ExtensiveRegular.lean)

State before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
hS : S ∈ ExtensiveSieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
⊢ IsIso (Equalizer.forkMap F S)
Tactic:
rcases hS with ⟨α, _, Z, π, hS, HIso⟩
State after:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
⊢ IsIso (Equalizer.forkMap F S)

State before:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
⊢ IsIso (Equalizer.forkMap F S)
Tactic:
haveI : PreservesLimit (Discrete.functor fun a => op (Z a)) F := by
    haveI := (hF.preserves α); infer_instance
State after:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ IsIso (Equalizer.forkMap F S)

State before:
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ IsIso (Equalizer.forkMap F S)
Tactic:
refine' ⟨fromFirst hS hF HIso, _, _⟩
State after:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ Equalizer.forkMap F S ≫ fromFirst hS hF HIso = 𝟙 (F.obj X.op)

case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ fromFirst hS hF HIso ≫ Equalizer.forkMap F S = 𝟙 (Equalizer.FirstObj F S)

State before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
⊢ PreservesLimit (Discrete.functor fun a => (Z a).op) F
Tactic:
haveI := (hF.preserves α)
State after:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimitsOfShape (Discrete α) F
⊢ PreservesLimit (Discrete.functor fun a => (Z a).op) F

State before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimitsOfShape (Discrete α) F
⊢ PreservesLimit (Discrete.functor fun a => (Z a).op) F
Tactic:
infer_instance
State after:
no goals

State before:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ Equalizer.forkMap F S ≫ fromFirst hS hF HIso = 𝟙 (F.obj X.op)
Tactic:
unfold fromFirst
State after:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ Equalizer.forkMap F S ≫
      comparisoninv hS F ≫
        (PreservesProduct.iso F fun a => (Z a).op).inv ≫ F.map (CoprodToProd Z).inv ≫ F.map (inv (Sigma.desc π).op) =
    𝟙 (F.obj X.op)

State before:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ Equalizer.forkMap F S ≫
      comparisoninv hS F ≫
        (PreservesProduct.iso F fun a => (Z a).op).inv ≫ F.map (CoprodToProd Z).inv ≫ F.map (inv (Sigma.desc π).op) =
    𝟙 (F.obj X.op)
Tactic:
simp only [← Category.assoc]
State after:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ (((Equalizer.forkMap F S ≫ comparisoninv hS F) ≫ (PreservesProduct.iso F fun a => (Z a).op).inv) ≫
        F.map (CoprodToProd Z).inv) ≫
      F.map (inv (Sigma.desc π).op) =
    𝟙 (F.obj X.op)

State before:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ (((Equalizer.forkMap F S ≫ comparisoninv hS F) ≫ (PreservesProduct.iso F fun a => (Z a).op).inv) ≫
        F.map (CoprodToProd Z).inv) ≫
      F.map (inv (Sigma.desc π).op) =
    𝟙 (F.obj X.op)
Tactic:
rw [Functor.map_inv, IsIso.comp_inv_eq, Category.id_comp, ← Functor.mapIso_inv,
  Iso.comp_inv_eq, Functor.mapIso_hom, Iso.comp_inv_eq, ← Functor.map_comp, descOpCompCoprodToProd]
State after:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ Equalizer.forkMap F S ≫ comparisoninv hS F =
    F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom

State before:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ Equalizer.forkMap F S ≫ comparisoninv hS F =
    F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom
Tactic:
have : F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => op (Z a)).hom =
  Pi.lift (fun a => F.map ((Sigma.ι Z a ≫ (Sigma.desc π)).op)) := by simp
State after:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
⊢ Equalizer.forkMap F S ≫ comparisoninv hS F =
    F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom

State before:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
⊢ Equalizer.forkMap F S ≫ comparisoninv hS F =
    F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom
Tactic:
erw [this]
State after:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
⊢ Equalizer.forkMap F S ≫ comparisoninv hS F = Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op

State before:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
⊢ Equalizer.forkMap F S ≫ comparisoninv hS F = Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
Tactic:
refine' funext (fun s => _)
State after:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
⊢ (Equalizer.forkMap F S ≫ comparisoninv hS F) s = Pi.lift (fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op) s

State before:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
⊢ (Equalizer.forkMap F S ≫ comparisoninv hS F) s = Pi.lift (fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op) s
Tactic:
simp only [types_comp_apply, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
State after:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
⊢ comparisoninv hS F (Equalizer.forkMap F S s) = Pi.lift (fun a => F.map (π a).op) s

State before:
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
⊢ comparisoninv hS F (Equalizer.forkMap F S s) = Pi.lift (fun a => F.map (π a).op) s
Tactic:
ext a
State after:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a (comparisoninv hS F (Equalizer.forkMap F S s)) =
    limit.π (Discrete.functor fun a => F.obj (Z a).op) a (Pi.lift (fun a => F.map (π a).op) s)

State before:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a (comparisoninv hS F (Equalizer.forkMap F S s)) =
    limit.π (Discrete.functor fun a => F.obj (Z a).op) a (Pi.lift (fun a => F.map (π a).op) s)
Tactic:
rw [Types.Limit.lift_π_apply]
State after:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a (comparisoninv hS F (Equalizer.forkMap F S s)) =
    (Fan.mk (F.obj X.op) fun a => F.map (π a).op).π.app a s

State before:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a (comparisoninv hS F (Equalizer.forkMap F S s)) =
    (Fan.mk (F.obj X.op) fun a => F.map (π a).op).π.app a s
Tactic:
dsimp [comparisoninv]
State after:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a
      (Pi.lift (fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a) ≫ F.map (𝟙 (v hS a).fst.op))
        (Equalizer.forkMap F S s)) =
    F.map (π a.as).op s

State before:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a
      (Pi.lift (fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a) ≫ F.map (𝟙 (v hS a).fst.op))
        (Equalizer.forkMap F S s)) =
    F.map (π a.as).op s
Tactic:
simp_rw [v.fst]
State after:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a
      (Pi.lift (fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a) ≫ F.map (𝟙 (Z a).op)) (Equalizer.forkMap F S s)) =
    F.map (π a.as).op s

State before:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a
      (Pi.lift (fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a) ≫ F.map (𝟙 (Z a).op)) (Equalizer.forkMap F S s)) =
    F.map (π a.as).op s
Tactic:
simp only [Functor.map_id, Category.comp_id]
State after:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a
      (Pi.lift (fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a)) (Equalizer.forkMap F S s)) =
    F.map (π a.as).op s

State before:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ limit.π (Discrete.functor fun a => F.obj (Z a).op) a
      (Pi.lift (fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a)) (Equalizer.forkMap F S s)) =
    F.map (π a.as).op s
Tactic:
rw [Types.Limit.lift_π_apply]
State after:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ (Fan.mk (∏ fun f => F.obj f.fst.op) fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a)).π.app a
      (Equalizer.forkMap F S s) =
    F.map (π a.as).op s

State before:
case intro.intro.intro.intro.intro.refine'_1.w
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this✝ : PreservesLimit (Discrete.functor fun a => (Z a).op) F
this :
  F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
s : F.obj X.op
a : Discrete α
⊢ (Fan.mk (∏ fun f => F.obj f.fst.op) fun a => Pi.π (fun f => F.obj f.fst.op) (v hS a)).π.app a
      (Equalizer.forkMap F S s) =
    F.map (π a.as).op s
Tactic:
simp only [Fan.mk_pt, Equalizer.forkMap, Fan.mk_π_app, Types.pi_lift_π_apply, v.snd]
State after:
no goals

State before:
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ F.map (Pi.lift fun a => (π a).op) ≫ (PreservesProduct.iso F fun a => (Z a).op).hom =
    Pi.lift fun a => F.map (Sigma.ι Z a ≫ Sigma.desc π).op
Tactic:
simp
State after:
no goals

State before:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
⊢ fromFirst hS hF HIso ≫ Equalizer.forkMap F S = 𝟙 (Equalizer.FirstObj F S)
Tactic:
refine' Limits.Pi.hom_ext _ _ (fun f => _)
State after:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ (fromFirst hS hF HIso ≫ Equalizer.forkMap F S) ≫ Pi.π (fun f => F.obj f.fst.op) f =
    𝟙 (Equalizer.FirstObj F S) ≫ Pi.π (fun f => F.obj f.fst.op) f

State before:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ (fromFirst hS hF HIso ≫ Equalizer.forkMap F S) ≫ Pi.π (fun f => F.obj f.fst.op) f =
    𝟙 (Equalizer.FirstObj F S) ≫ Pi.π (fun f => F.obj f.fst.op) f
Tactic:
dsimp [Equalizer.forkMap]
State after:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ (fromFirst hS hF HIso ≫ Pi.lift fun f => F.map (↑f.snd).op) ≫ Pi.π (fun f => F.obj f.fst.op) f =
    𝟙 (Equalizer.FirstObj F S) ≫ Pi.π (fun f => F.obj f.fst.op) f

State before:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ (fromFirst hS hF HIso ≫ Pi.lift fun f => F.map (↑f.snd).op) ≫ Pi.π (fun f => F.obj f.fst.op) f =
    𝟙 (Equalizer.FirstObj F S) ≫ Pi.π (fun f => F.obj f.fst.op) f
Tactic:
rw [Category.id_comp, Category.assoc, limit.lift_π, Limits.Fan.mk_π_app]
State after:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ fromFirst hS hF HIso ≫ F.map (↑{ as := f }.as.snd).op = Pi.π (fun f => F.obj f.fst.op) f

State before:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ fromFirst hS hF HIso ≫ F.map (↑{ as := f }.as.snd).op = Pi.π (fun f => F.obj f.fst.op) f
Tactic:
simp only
State after:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ fromFirst hS hF HIso ≫ F.map (↑f.snd).op = Pi.π (fun f => F.obj f.fst.op) f

State before:
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
⊢ fromFirst hS hF HIso ≫ F.map (↑f.snd).op = Pi.π (fun f => F.obj f.fst.op) f
Tactic:
obtain ⟨a, ha⟩ := vsurj hS f
State after:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ fromFirst hS hF HIso ≫ F.map (↑f.snd).op = Pi.π (fun f => F.obj f.fst.op) f

State before:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ fromFirst hS hF HIso ≫ F.map (↑f.snd).op = Pi.π (fun f => F.obj f.fst.op) f
Tactic:
unfold fromFirst
State after:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ (comparisoninv hS F ≫
        (PreservesProduct.iso F fun a => (Z a).op).inv ≫ F.map (CoprodToProd Z).inv ≫ F.map (inv (Sigma.desc π).op)) ≫
      F.map (↑f.snd).op =
    Pi.π (fun f => F.obj f.fst.op) f

State before:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ (comparisoninv hS F ≫
        (PreservesProduct.iso F fun a => (Z a).op).inv ≫ F.map (CoprodToProd Z).inv ≫ F.map (inv (Sigma.desc π).op)) ≫
      F.map (↑f.snd).op =
    Pi.π (fun f => F.obj f.fst.op) f
Tactic:
simp only [Category.assoc]
State after:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ comparisoninv hS F ≫
      (PreservesProduct.iso F fun a => (Z a).op).inv ≫
        F.map (CoprodToProd Z).inv ≫ F.map (inv (Sigma.desc π).op) ≫ F.map (↑f.snd).op =
    Pi.π (fun f => F.obj f.fst.op) f

State before:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ comparisoninv hS F ≫
      (PreservesProduct.iso F fun a => (Z a).op).inv ≫
        F.map (CoprodToProd Z).inv ≫ F.map (inv (Sigma.desc π).op) ≫ F.map (↑f.snd).op =
    Pi.π (fun f => F.obj f.fst.op) f
Tactic:
rw [← Functor.map_comp, ← op_inv, ← op_comp, ← ha, v.snd hS, piCompInvdesc,
  ← Functor.map_comp, CoprodToProdInvComp.ι, @PreservesProduct.isoInvCompMap _ _ _ _ F _ _ _ _ (_) a]
State after:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ comparisoninv hS F ≫ Pi.π (fun j => F.obj (Z j).op) a = Pi.π (fun f => F.obj f.fst.op) (v hS a)

State before:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ comparisoninv hS F ≫ Pi.π (fun j => F.obj (Z j).op) a = Pi.π (fun f => F.obj f.fst.op) (v hS a)
Tactic:
simp only [comparisoninv, op_id, limit.lift_π, Fan.mk_pt, Fan.mk_π_app]
State after:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ Pi.π (fun f => F.obj f.fst.op) (v hS a) ≫ F.map (𝟙 (v hS a).fst.op) = Pi.π (fun f => F.obj f.fst.op) (v hS a)

State before:
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝² : Category C
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasPullbackOfIsIsodesc C
X : C
S : Presieve X
F : Cᵒᵖ ⥤ Type (max u v)
hF : PreservesFiniteProducts F
α : Type
w✝ : Fintype α
Z : α → C
π : (a : α) → Z a ⟶ X
hS : S = Presieve.ofArrows Z π
HIso : IsIso (Sigma.desc π)
this : PreservesLimit (Discrete.functor fun a => (Z a).op) F
f : (Y : C) × { f // S f }
a : α
ha : v hS a = f
⊢ Pi.π (fun f => F.obj f.fst.op) (v hS a) ≫ F.map (𝟙 (v hS a).fst.op) = Pi.π (fun f => F.obj f.fst.op) (v hS a)
Tactic:
erw [F.map_id, Category.comp_id]
State after:
no goals