mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case e'_2.e'_6.e'_5
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
e_1✝ : (op X ⟶ ∏ᶜ fun x ↦ op (Z x)) = (op (Cofan.mk X π).pt ⟶ (Fan.mk (∏ᶜ fun x ↦ op (Z x)) (Pi.π fun x ↦ op (Z x))).pt)
e_3✝¹ : op X = op (Cofan.mk X π).pt
e_4✝¹ : op (∐ Z) = op (Cofan.mk (∐ Z) (Sigma.ι Z)).pt
e_3✝ : ∐ Z = (Cofan.mk (∐ Z) (Sigma.ι Z)).pt
e_4✝ : X = (Cofan.mk X π).pt
⊢ Sigma.desc π = (coproductIsCoproduct Z).desc (Cofan.mk X π)

pp: case e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
e_1✝ : (op X ⟶ ∏ᶜ fun x ↦ op (Z x)) = (op (Cofan.mk X π).pt ⟶ (Fan.mk (∏ᶜ fun x ↦ op (Z x)) (Pi.π fun x ↦ op (Z x))).pt)
⊢ (Pi.lift fun a ↦ (π a).op) = (productIsProduct fun x ↦ op (Z x)).lift (Cofan.mk X π).op

Tactic:
·

Goal state after:
case e'_2.e'_6.e'_5
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
e_1✝ : (op X ⟶ ∏ᶜ fun x ↦ op (Z x)) = (op (Cofan.mk X π).pt ⟶ (Fan.mk (∏ᶜ fun x ↦ op (Z x)) (Pi.π fun x ↦ op (Z x))).pt)
e_3✝¹ : op X = op (Cofan.mk X π).pt
e_4✝¹ : op (∐ Z) = op (Cofan.mk (∐ Z) (Sigma.ι Z)).pt
e_3✝ : ∐ Z = (Cofan.mk (∐ Z) (Sigma.ι Z)).pt
e_4✝ : X = (Cofan.mk X π).pt
⊢ Sigma.desc π = (coproductIsCoproduct Z).desc (Cofan.mk X π)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
e_1✝ : (op X ⟶ ∏ᶜ fun x ↦ op (Z x)) = (op (Cofan.mk X π).pt ⟶ (Fan.mk (∏ᶜ fun x ↦ op (Z x)) (Pi.π fun x ↦ op (Z x))).pt)
⊢ (Pi.lift fun a ↦ (π a).op) = (productIsProduct fun x ↦ op (Z x)).lift (Cofan.mk X π).op

Tactic:
·

Goal state after:
case e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasCoproduct Z
X : C
π : (a : α) → Z a ⟶ X
e_1✝ : (op X ⟶ ∏ᶜ fun x ↦ op (Z x)) = (op (Cofan.mk X π).pt ⟶ (Fan.mk (∏ᶜ fun x ↦ op (Z x)) (Pi.π fun x ↦ op (Z x))).pt)
⊢ (Pi.lift fun a ↦ (π a).op) = (productIsProduct fun x ↦ op (Z x)).lift (Cofan.mk X π).op
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
j : α
⊢ ((opProductIsoCoproduct' hf hc).hom ≫ (opProductIsoCoproduct' hf' hc).inv).unop ≫ f.proj j =
    (hf.conePointUniqueUpToIso hf').op.inv.unop ≫ f.π.app { as := j }

Tactic:
simp only [unop_op, unop_comp, Category.assoc, Discrete.functor_obj, Iso.op_inv,
    Quiver.Hom.unop_op, IsLimit.conePointUniqueUpToIso_inv_comp]

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
f f' : Fan Z
c : Cofan fun x ↦ op (Z x)
hf : IsLimit f
hf' : IsLimit f'
hc : IsColimit c
j : α
⊢ (opProductIsoCoproduct' hf' hc).inv.unop ≫ (opProductIsoCoproduct' hf hc).hom.unop ≫ f.proj j = f'.π.app { as := j }
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case e'_2.e'_7.e'_5
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x ↦ op (Z x)) ⟶ op X) = ((Cofan.mk (∐ fun x ↦ op (Z x)) (Sigma.ι fun x ↦ op (Z x))).pt ⟶ op (Fan.mk X π).pt)
e_4✝¹ : op (∏ᶜ Z) = op (Fan.mk (∏ᶜ Z) (Pi.π Z)).pt
e_5✝ : op X = op (Fan.mk X π).pt
e_3✝ : X = (Fan.mk X π).pt
e_4✝ : ∏ᶜ Z = (Fan.mk (∏ᶜ Z) (Pi.π Z)).pt
⊢ Pi.lift π = (productIsProduct Z).lift (Fan.mk X π)

pp: case e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x ↦ op (Z x)) ⟶ op X) = ((Cofan.mk (∐ fun x ↦ op (Z x)) (Sigma.ι fun x ↦ op (Z x))).pt ⟶ op (Fan.mk X π).pt)
⊢ (Sigma.desc fun a ↦ (π a).op) = (coproductIsCoproduct fun x ↦ op (Z x)).desc (Fan.mk X π).op

Tactic:
·

Goal state after:
case e'_2.e'_7.e'_5
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x ↦ op (Z x)) ⟶ op X) = ((Cofan.mk (∐ fun x ↦ op (Z x)) (Sigma.ι fun x ↦ op (Z x))).pt ⟶ op (Fan.mk X π).pt)
e_4✝¹ : op (∏ᶜ Z) = op (Fan.mk (∏ᶜ Z) (Pi.π Z)).pt
e_5✝ : op X = op (Fan.mk X π).pt
e_3✝ : X = (Fan.mk X π).pt
e_4✝ : ∏ᶜ Z = (Fan.mk (∏ᶜ Z) (Pi.π Z)).pt
⊢ Pi.lift π = (productIsProduct Z).lift (Fan.mk X π)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x ↦ op (Z x)) ⟶ op X) = ((Cofan.mk (∐ fun x ↦ op (Z x)) (Sigma.ι fun x ↦ op (Z x))).pt ⟶ op (Fan.mk X π).pt)
⊢ (Sigma.desc fun a ↦ (π a).op) = (coproductIsCoproduct fun x ↦ op (Z x)).desc (Fan.mk X π).op

Tactic:
·

Goal state after:
case e'_3
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
α : Type u_1
Z : α → C
inst✝ : HasProduct Z
X : C
π : (a : α) → X ⟶ Z a
e_1✝ :
  ((∐ fun x ↦ op (Z x)) ⟶ op X) = ((Cofan.mk (∐ fun x ↦ op (Z x)) (Sigma.ι fun x ↦ op (Z x))).pt ⟶ op (Fan.mk X π).pt)
⊢ (Sigma.desc fun a ↦ (π a).op) = (coproductIsCoproduct fun x ↦ op (Z x)).desc (Fan.mk X π).op
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.fst =
    (𝟙 (op (A ⨯ B))).unop ≫ prod.fst

Tactic:
·

Goal state after:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.fst =
    (𝟙 (op (A ⨯ B))).unop ≫ prod.fst
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.snd =
    (𝟙 (op (A ⨯ B))).unop ≫ prod.snd

Tactic:
·

Goal state after:
case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ ((prod.lift coprod.inl.unop coprod.inr.unop).op ≫ coprod.desc prod.fst.op prod.snd.op).unop ≫ prod.snd =
    (𝟙 (op (A ⨯ B))).unop ≫ prod.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inl ≫ coprod.desc prod.fst.op prod.snd.op ≫ (prod.lift coprod.inl.unop coprod.inr.unop).op =
    coprod.inl ≫ 𝟙 (op A ⨿ op B)

Tactic:
·

Goal state after:
case h₁
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inl ≫ coprod.desc prod.fst.op prod.snd.op ≫ (prod.lift coprod.inl.unop coprod.inr.unop).op =
    coprod.inl ≫ 𝟙 (op A ⨿ op B)
Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products

Goal state before:
pp: case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inr ≫ coprod.desc prod.fst.op prod.snd.op ≫ (prod.lift coprod.inl.unop coprod.inr.unop).op =
    coprod.inr ≫ 𝟙 (op A ⨿ op B)

Tactic:
·

Goal state after:
case h₂
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
X : Type v₂
A B : C
inst✝ : HasBinaryProduct A B
⊢ coprod.inr ≫ coprod.desc prod.fst.op prod.snd.op ≫ (prod.lift coprod.inl.unop coprod.inr.unop).op =
    coprod.inr ≫ 𝟙 (op A ⨿ op B)
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: case e'_3
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasColimitsOfShape (Finset (Discrete α)) C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinsetObj F),
        ι := Discrete.natTrans fun j ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    { pt := colimit (liftToFinsetObj F),
                ι :=
                  Discrete.natTrans fun j ↦
                    Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.ι.app
          j ≫
        m =
      s.ι.app j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
e_1✝ : ((Discrete.functor fun x ↦ F.obj ↑x).obj { as := ⟨j, hj⟩ } ⟶ s.pt) = (F.obj j ⟶ s.pt)
⊢ colimit.ι (Discrete.functor fun x ↦ F.obj ↑x) { as := ⟨j, hj⟩ } ≫
      colimit.ι
          { obj := fun s ↦ ∐ fun x ↦ F.obj ↑x,
            map := fun {x Y} h ↦ Sigma.desc fun y ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩, map_id := ⋯, map_comp := ⋯ }
          t ≫
        colimit.desc
          { obj := fun s ↦ ∐ fun x ↦ F.obj ↑x,
            map := fun {x Y} h ↦ Sigma.desc fun y ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩, map_id := ⋯, map_comp := ⋯ }
          { pt := s.pt, ι := { app := fun x ↦ Sigma.desc fun x_1 ↦ s.ι.app ↑x_1, naturality := ⋯ } } =
    s.ι.app j

Tactic:
·

Goal state after:
case e'_3
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteCoproducts C
inst✝ : HasColimitsOfShape (Finset (Discrete α)) C
F : Discrete α ⥤ C
s : Cocone F
m :
  { pt := colimit (liftToFinsetObj F),
        ι := Discrete.natTrans fun j ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.pt ⟶
    s.pt
h :
  ∀ (j : Discrete α),
    { pt := colimit (liftToFinsetObj F),
                ι :=
                  Discrete.natTrans fun j ↦
                    Sigma.ι (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ ≫ colimit.ι (liftToFinsetObj F) {j} }.ι.app
          j ≫
        m =
      s.ι.app j
t : Finset (Discrete α)
j : Discrete α
hj : j ∈ t
e_1✝ : ((Discrete.functor fun x ↦ F.obj ↑x).obj { as := ⟨j, hj⟩ } ⟶ s.pt) = (F.obj j ⟶ s.pt)
⊢ colimit.ι (Discrete.functor fun x ↦ F.obj ↑x) { as := ⟨j, hj⟩ } ≫
      colimit.ι
          { obj := fun s ↦ ∐ fun x ↦ F.obj ↑x,
            map := fun {x Y} h ↦ Sigma.desc fun y ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩, map_id := ⋯, map_comp := ⋯ }
          t ≫
        colimit.desc
          { obj := fun s ↦ ∐ fun x ↦ F.obj ↑x,
            map := fun {x Y} h ↦ Sigma.desc fun y ↦ Sigma.ι (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩, map_id := ⋯, map_comp := ⋯ }
          { pt := s.pt, ι := { app := fun x ↦ Sigma.desc fun x_1 ↦ s.ι.app ↑x_1, naturality := ⋯ } } =
    s.ι.app j
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: case e'_2.e'_6
C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
j : ↥S
e_1✝ : (f (↑j).as ⟶ ∐ f) = ((Discrete.functor f).obj ↑j ⟶ (colimit.cocone (Discrete.functor f)).pt)
e_3✝ : f (↑j).as = (Discrete.functor f).obj ↑j
e_4✝ : colimit (liftToFinsetObj (Discrete.functor f)) = (liftToFinsetColimitCocone (Discrete.functor f)).cocone.pt
⊢ Sigma.ι (fun x ↦ f (↑x).as) j ≫ colimit.ι (liftToFinsetObj (Discrete.functor f)) S =
    (liftToFinsetColimitCocone (Discrete.functor f)).cocone.ι.app ↑j

pp: case e'_3
C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
j : ↥S
e_1✝ : (f (↑j).as ⟶ ∐ f) = ((Discrete.functor f).obj ↑j ⟶ (colimit.cocone (Discrete.functor f)).pt)
⊢ (Sigma.ι (fun x ↦ f (↑x).as) j ≫ Sigma.desc fun s ↦ Sigma.ι f (↑s).as) =
    (colimit.cocone (Discrete.functor f)).ι.app ↑j

Tactic:
·

Goal state after:
case e'_2.e'_6
C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
j : ↥S
e_1✝ : (f (↑j).as ⟶ ∐ f) = ((Discrete.functor f).obj ↑j ⟶ (colimit.cocone (Discrete.functor f)).pt)
e_3✝ : f (↑j).as = (Discrete.functor f).obj ↑j
e_4✝ : colimit (liftToFinsetObj (Discrete.functor f)) = (liftToFinsetColimitCocone (Discrete.functor f)).cocone.pt
⊢ Sigma.ι (fun x ↦ f (↑x).as) j ≫ colimit.ι (liftToFinsetObj (Discrete.functor f)) S =
    (liftToFinsetColimitCocone (Discrete.functor f)).cocone.ι.app ↑j
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: case e'_3
C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
j : ↥S
e_1✝ : (f (↑j).as ⟶ ∐ f) = ((Discrete.functor f).obj ↑j ⟶ (colimit.cocone (Discrete.functor f)).pt)
⊢ (Sigma.ι (fun x ↦ f (↑x).as) j ≫ Sigma.desc fun s ↦ Sigma.ι f (↑s).as) =
    (colimit.cocone (Discrete.functor f)).ι.app ↑j

Tactic:
·

Goal state after:
case e'_3
C : Type u
inst✝³ : Category.{v, u} C
α : Type w
inst✝² : HasFiniteCoproducts C
f : α → C
inst✝¹ : HasColimitsOfShape (Finset (Discrete α)) C
inst✝ : HasCoproduct f
S : Finset (Discrete α)
j : ↥S
e_1✝ : (f (↑j).as ⟶ ∐ f) = ((Discrete.functor f).obj ↑j ⟶ (colimit.cocone (Discrete.functor f)).pt)
⊢ (Sigma.ι (fun x ↦ f (↑x).as) j ≫ Sigma.desc fun s ↦ Sigma.ι f (↑s).as) =
    (colimit.cocone (Discrete.functor f)).ι.app ↑j
Module: Mathlib.CategoryTheory.Limits.Constructions.Filtered

Goal state before:
pp: case e'_3
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
t : (Finset (Discrete α))ᵒᵖ
j : Discrete α
hj : j ∈ unop t
e_1✝ : (s.pt ⟶ (Discrete.functor fun x ↦ F.obj ↑x).obj { as := ⟨j, hj⟩ }) = (s.pt ⟶ F.obj j)
⊢ (limit.lift
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          { pt := s.pt, π := { app := fun x ↦ Pi.lift fun x_1 ↦ s.π.app ↑x_1, naturality := ⋯ } } ≫
        limit.π
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          t) ≫
      limit.π (Discrete.functor fun x ↦ F.obj ↑x) { as := ⟨j, hj⟩ } =
    s.π.app j

Tactic:
·

Goal state after:
case e'_3
C : Type u
inst✝² : Category.{v, u} C
α : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C
F : Discrete α ⥤ C
s : Cone F
m :
  s.pt ⟶
    { pt := limit (liftToFinsetObj F),
        π := Discrete.natTrans fun j ↦ limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.pt
h :
  ∀ (j : Discrete α),
    m ≫
        { pt := limit (liftToFinsetObj F),
                π :=
                  Discrete.natTrans fun j ↦
                    limit.π (liftToFinsetObj F) (op {j}) ≫ Pi.π (fun x ↦ F.obj ↑x) ⟨j, ⋯⟩ }.π.app
          j =
      s.π.app j
t : (Finset (Discrete α))ᵒᵖ
j : Discrete α
hj : j ∈ unop t
e_1✝ : (s.pt ⟶ (Discrete.functor fun x ↦ F.obj ↑x).obj { as := ⟨j, hj⟩ }) = (s.pt ⟶ F.obj j)
⊢ (limit.lift
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          { pt := s.pt, π := { app := fun x ↦ Pi.lift fun x_1 ↦ s.π.app ↑x_1, naturality := ⋯ } } ≫
        limit.π
          { obj := fun s ↦ ∏ᶜ fun x ↦ F.obj ↑x, map := fun {Y x} h ↦ Pi.lift fun y ↦ Pi.π (fun x ↦ F.obj ↑x) ⟨↑y, ⋯⟩,
            map_id := ⋯, map_comp := ⋯ }
          t) ≫
      limit.π (Discrete.functor fun x ↦ F.obj ↑x) { as := ⟨j, hj⟩ } =
    s.π.app j
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L.HasPointwiseLeftKanExtensionAt F Y → L'.HasPointwiseLeftKanExtensionAt F Y'

pp: case mpr
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L'.HasPointwiseLeftKanExtensionAt F Y' → L.HasPointwiseLeftKanExtensionAt F Y

Tactic:
·

Goal state after:
case mp
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L.HasPointwiseLeftKanExtensionAt F Y → L'.HasPointwiseLeftKanExtensionAt F Y'
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L'.HasPointwiseLeftKanExtensionAt F Y' → L.HasPointwiseLeftKanExtensionAt F Y

Tactic:
·

Goal state after:
case mpr
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L'.HasPointwiseLeftKanExtensionAt F Y' → L.HasPointwiseLeftKanExtensionAt F Y
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: case mp
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L.HasPointwiseRightKanExtensionAt F Y → L'.HasPointwiseRightKanExtensionAt F Y'

pp: case mpr
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L'.HasPointwiseRightKanExtensionAt F Y' → L.HasPointwiseRightKanExtensionAt F Y

Tactic:
·

Goal state after:
case mp
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L.HasPointwiseRightKanExtensionAt F Y → L'.HasPointwiseRightKanExtensionAt F Y'
Module: Mathlib.CategoryTheory.Functor.KanExtension.Pointwise

Goal state before:
pp: case mpr
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L'.HasPointwiseRightKanExtensionAt F Y' → L.HasPointwiseRightKanExtensionAt F Y

Tactic:
·

Goal state after:
case mpr
C : Type u_1
D : Type u_2
D' : Type u_3
H : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Category.{v_3, u_3} D'
inst✝ : Category.{v_4, u_4} H
L : C ⥤ D
L' : C ⥤ D'
F : C ⥤ H
E : D ≌ D'
eL : L ⋙ E.functor ≅ L'
Y : D
Y' : D'
e : E.functor.obj Y ≅ Y'
⊢ L'.HasPointwiseRightKanExtensionAt F Y' → L.HasPointwiseRightKanExtensionAt F Y
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
⊢ F'.IsRightKanExtension α → F''.IsRightKanExtension α'

pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
⊢ F''.IsRightKanExtension α' → F'.IsRightKanExtension α

Tactic:
·

Goal state after:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
⊢ F'.IsRightKanExtension α → F''.IsRightKanExtension α'
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
⊢ F''.IsRightKanExtension α' → F'.IsRightKanExtension α

Tactic:
·

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Category.{v_3, u_3} H
inst✝ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
e : F' ≅ F''
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft e.hom ≫ α' = α
⊢ F''.IsRightKanExtension α' → F'.IsRightKanExtension α
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α' → IsIso φ

pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ IsIso φ → F''.IsRightKanExtension α'

Tactic:
·

Goal state after:
case mp
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ F''.IsRightKanExtension α' → IsIso φ
Module: Mathlib.CategoryTheory.Functor.KanExtension.Basic

Goal state before:
pp: case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ IsIso φ → F''.IsRightKanExtension α'

Tactic:
·

Goal state after:
case mpr
C : Type u_1
H : Type u_3
D : Type u_4
inst✝³ : Category.{v_1, u_1} C
inst✝² : Category.{v_3, u_3} H
inst✝¹ : Category.{v_4, u_4} D
F' F'' : D ⥤ H
φ : F'' ⟶ F'
L : C ⥤ D
F : C ⥤ H
α : L ⋙ F' ⟶ F
α' : L ⋙ F'' ⟶ F
comm : L.whiskerLeft φ ≫ α = α'
inst✝ : F'.IsRightKanExtension α
⊢ IsIso φ → F''.IsRightKanExtension α'