mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
A : Type u₁
inst✝ : Category.{v₁, u₁} A
X Y Z : FormalCoproduct C
f : X ⟶ Z
g : Y ⟶ Z
pb :
  (i : Function.Pullback f.f g.f) → PullbackCone (f.φ (↑i).1 ≫ eqToHom (@_proof_107 C inst✝¹ X Y Z f g i)) (g.φ (↑i).2)
hpb : (i : Function.Pullback f.f g.f) → IsLimit (pb i)
T : FormalCoproduct C
⊢ IsLimit (pullbackCone f g pb)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
X : C
F : C ⥤ D
inst✝ : PreservesLimitsOfShape (WithTerminal J) F
K✝ : J ⥤ Over X
coneK : Cone K✝
isLimitConeK : IsLimit coneK
isLimitConeD : IsLimit ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK)))
⊢ ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK))).π.app WithTerminal.star =
    (Iso.refl ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK))).pt).hom ≫
      (coneEquiv.functor.obj ((Over.post F).mapCone coneK)).π.app WithTerminal.star

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
X : C
F : C ⥤ D
inst✝ : PreservesLimitsOfShape (WithTerminal J) F
K✝ : J ⥤ Over X
coneK : Cone K✝
isLimitConeK : IsLimit coneK
isLimitConeD : IsLimit ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK)))
a : J
⊢ ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK))).π.app (of a) =
    (Iso.refl ((Cone.postcompose liftFromOverComp.symm.hom).obj (F.mapCone (coneEquiv.functor.obj coneK))).pt).hom ≫
      (coneEquiv.functor.obj ((Over.post F).mapCone coneK)).π.app (of a)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasCoproducts A
J : Type w
f : J → FormalCoproduct C
F✝ F : C ⥤ A
X✝ Y✝ Z✝ : FormalCoproduct C
x✝² : X✝ ⟶ Y✝
x✝¹ : Y✝ ⟶ Z✝
x✝ : X✝.I
⊢ (Sigma.ι (fun i ↦ F.obj (X✝.obj i)) x✝ ≫
      Sigma.desc fun i ↦ F.map ((x✝² ≫ x✝¹).φ i) ≫ Sigma.ι (F.obj ∘ Z✝.obj) ((x✝² ≫ x✝¹).f i)) =
    Sigma.ι (fun i ↦ F.obj (X✝.obj i)) x✝ ≫
      (Sigma.desc fun i ↦ F.map (x✝².φ i) ≫ Sigma.ι (F.obj ∘ Y✝.obj) (x✝².f i)) ≫
        Sigma.desc fun i ↦ F.map (x✝¹.φ i) ≫ Sigma.ι (F.obj ∘ Z✝.obj) (x✝¹.f i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
X : C
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (WithInitial J) F
K✝ : J ⥤ Under X
coconeK : Cocone K✝
isColimitCoconeK : IsColimit coconeK
isColimitCoconeD :
  IsColimit ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK)))
⊢ ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK))).ι.app
        WithInitial.star ≫
      (Iso.refl
          ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK))).pt).hom =
    (coconeEquiv.functor.obj ((Under.post F).mapCocone coconeK)).ι.app WithInitial.star

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasCoproducts A
J : Type w
f : J → FormalCoproduct C
F✝ F : C ⥤ A
x : C
⊢ (Sigma.desc fun x_1 ↦ 𝟙 (F.obj (((incl C).obj x).obj x_1))) ≫ Sigma.ι (fun x_1 ↦ F.obj x) PUnit.unit =
    𝟙 (((eval C A ⋙ (whiskeringLeft C (FormalCoproduct C) A).obj (incl C)).obj F).obj x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasCoproducts A
J : Type w
f : J → FormalCoproduct C
F✝ F : C ⥤ A
x : C
⊢ (Sigma.ι (fun x_1 ↦ F.obj x) PUnit.unit ≫ Sigma.desc fun x_1 ↦ 𝟙 (F.obj (((incl C).obj x).obj x_1))) =
    𝟙 (((𝟭 (C ⥤ A)).obj F).obj x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Over

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
J : Type w
inst✝¹ : Category.{w', w} J
X : C
F : C ⥤ D
inst✝ : PreservesColimitsOfShape (WithInitial J) F
K✝ : J ⥤ Under X
coconeK : Cocone K✝
isColimitCoconeK : IsColimit coconeK
isColimitCoconeD :
  IsColimit ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK)))
a : J
⊢ ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK))).ι.app (of a) ≫
      (Iso.refl
          ((Cocone.precompose liftFromUnderComp.hom).obj (F.mapCocone (coconeEquiv.functor.obj coconeK))).pt).hom =
    (coconeEquiv.functor.obj ((Under.post F).mapCocone coconeK)).ι.app (of a)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasCoproducts A
J : Type w
f✝ : J → FormalCoproduct C
F✝ F : C ⥤ A
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ ∀ (b : ((incl C).obj X✝).I),
    Sigma.ι (fun i ↦ F.obj (((incl C).obj X✝).obj i)) b ≫
        ((eval C A ⋙ (whiskeringLeft C (FormalCoproduct C) A).obj (incl C)).obj F).map f ≫
          { hom := Sigma.desc fun x ↦ 𝟙 (F.obj (((incl C).obj Y✝).obj x)), inv := Sigma.ι (fun x ↦ F.obj Y✝) PUnit.unit,
              hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom =
      Sigma.ι (fun i ↦ F.obj (((incl C).obj X✝).obj i)) b ≫
        { hom := Sigma.desc fun x ↦ 𝟙 (F.obj (((incl C).obj X✝).obj x)), inv := Sigma.ι (fun x ↦ F.obj X✝) PUnit.unit,
              hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
          ((𝟭 (C ⥤ A)).obj F).map f

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasCoproducts A
J : Type w
f : J → FormalCoproduct C
F : C ⥤ A
s : Cocone (Discrete.functor f ⋙ (eval C A).obj F)
i✝ : Discrete J
i : ((Discrete.functor f).obj i✝).I
⊢ (Sigma.ι (fun i ↦ F.obj (((Discrete.functor f).obj i✝).obj i)) i ≫
      (((eval C A).obj F).mapCocone (cofan J f)).ι.app i✝ ≫
        Sigma.desc fun i ↦ Sigma.ι (F.obj ∘ (f i.fst).obj) i.snd ≫ s.ι.app { as := i.fst }) =
    Sigma.ι (fun i ↦ F.obj (((Discrete.functor f).obj i✝).obj i)) i ≫ s.ι.app i✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasCoproducts A
J : Type w
f : J → FormalCoproduct C
F : C ⥤ A
s : Cocone (Discrete.functor f ⋙ (eval C A).obj F)
m : (((eval C A).obj F).mapCocone (cofan J f)).pt ⟶ s.pt
h : ∀ (j : Discrete J), (((eval C A).obj F).mapCocone (cofan J f)).ι.app j ≫ m = s.ι.app j
x✝ : (cofan J f).pt.I
i₁ : J
i₂ : (f i₁).I
⊢ Sigma.ι (fun i ↦ F.obj ((cofan J f).pt.obj i)) ⟨i₁, i₂⟩ ≫ m =
    Sigma.ι (fun i ↦ F.obj ((cofan J f).pt.obj i)) ⟨i₁, i₂⟩ ≫
      Sigma.desc fun i ↦ Sigma.ι (F.obj ∘ (f i.fst).obj) i.snd ≫ s.ι.app { as := i.fst }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasProducts A
J : Type w
f : J → FormalCoproduct C
F✝ F : Cᵒᵖ ⥤ A
x : Cᵒᵖ
⊢ (Pi.π (fun i ↦ F.obj (op ((unop ((incl C).op.obj x)).obj i))) PUnit.unit ≫
      Pi.lift fun x_1 ↦ 𝟙 (((𝟭 (Cᵒᵖ ⥤ A)).obj F).obj x)) =
    𝟙 (((evalOp C A ⋙ (whiskeringLeft Cᵒᵖ (FormalCoproduct C)ᵒᵖ A).obj (incl C).op).obj F).obj x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasProducts A
J : Type w
f : J → FormalCoproduct C
F✝ F : Cᵒᵖ ⥤ A
x : Cᵒᵖ
⊢ (Pi.lift fun x_1 ↦ 𝟙 (((𝟭 (Cᵒᵖ ⥤ A)).obj F).obj x)) ≫
      Pi.π (fun i ↦ F.obj (op ((unop ((incl C).op.obj x)).obj i))) PUnit.unit =
    𝟙 (((𝟭 (Cᵒᵖ ⥤ A)).obj F).obj x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasProducts A
J : Type w
f : J → FormalCoproduct C
F : Cᵒᵖ ⥤ A
s : Cone ((Discrete.functor fun x ↦ op (f x)) ⋙ (evalOp C A).obj F)
i✝ : Discrete J
i : (unop ((Discrete.functor fun x ↦ op (f x)).obj i✝)).I
⊢ ((Pi.lift fun i ↦
          s.π.app { as := i.fst } ≫
            Pi.π (fun i_1 ↦ F.obj (op ((unop ((Discrete.functor fun x ↦ op (f x)).obj { as := i.fst })).obj i_1)))
              i.snd) ≫
        (((evalOp C A).obj F).mapCone (cofan J f).op).π.app i✝) ≫
      Pi.π (fun i ↦ F.obj (op ((unop ((Discrete.functor fun x ↦ op (f x)).obj i✝)).obj i))) i =
    s.π.app i✝ ≫ Pi.π (fun i ↦ F.obj (op ((unop ((Discrete.functor fun x ↦ op (f x)).obj i✝)).obj i))) i

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
A : Type u₁
inst✝¹ : Category.{v₁, u₁} A
inst✝ : HasProducts A
J : Type w
f : J → FormalCoproduct C
F : Cᵒᵖ ⥤ A
s : Cone ((Discrete.functor fun x ↦ op (f x)) ⋙ (evalOp C A).obj F)
m : s.pt ⟶ (((evalOp C A).obj F).mapCone (cofan J f).op).pt
h : ∀ (j : Discrete J), m ≫ (((evalOp C A).obj F).mapCone (cofan J f).op).π.app j = s.π.app j
x✝ : (unop (cofan J f).op.pt).I
i₁ : J
i₂ : (f i₁).I
⊢ m ≫ Pi.π (fun i ↦ F.obj (op ((unop (cofan J f).op.pt).obj i))) ⟨i₁, i₂⟩ =
    (Pi.lift fun i ↦
        s.π.app { as := i.fst } ≫
          Pi.π (fun i_1 ↦ F.obj (op ((unop ((Discrete.functor fun x ↦ op (f x)).obj { as := i.fst })).obj i_1)))
            i.snd) ≫
      Pi.π (fun i ↦ F.obj (op ((unop (cofan J f).op.pt).obj i))) ⟨i₁, i₂⟩

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ ∀ (s : BinaryFan (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)),
    ((lift fun b ↦
          if h : P b then s.π.app { as := WalkingPair.left } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩
          else s.π.app { as := WalkingPair.right } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩) ≫
        map' Subtype.val fun x ↦ 𝟙 (X ↑x)) =
      s.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ ∀ (s : BinaryFan (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)),
    ((lift fun b ↦
          if h : P b then s.π.app { as := WalkingPair.left } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩
          else s.π.app { as := WalkingPair.right } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩) ≫
        map' Subtype.val fun x ↦ 𝟙 (X ↑x)) =
      s.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
x✝¹ : BinaryFan (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)
x✝ : x✝¹.pt ⟶ ∏ᶜ X
h₁ : (x✝ ≫ map' Subtype.val fun x ↦ 𝟙 (X ↑x)) = x✝¹.fst
h₂ : (x✝ ≫ map' Subtype.val fun x ↦ 𝟙 (X ↑x)) = x✝¹.snd
b : I
⊢ x✝ ≫ π X b =
    (lift fun b ↦
        if h : P b then x✝¹.π.app { as := WalkingPair.left } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩
        else x✝¹.π.app { as := WalkingPair.right } ≫ π (fun i ↦ X ↑i) ⟨b, h⟩) ≫
      π X b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝³ : Category.{v_1, u_1} C
X : I → C
P : I → Prop
inst✝² : HasProduct X
inst✝¹ : HasProduct fun i ↦ X ↑i
inst✝ : HasProduct fun i ↦ X ↑i
⊢ HasBinaryProduct (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.PiProd

Goal state before:
pp: C : Type u_1
I : Type u_2
inst✝⁷ : Category.{v_1, u_1} C
X Y : I → C
f : (i : I) → X i ⟶ Y i
P : I → Prop
inst✝⁶ : HasProduct X
inst✝⁵ : HasProduct Y
inst✝⁴ : HasProduct fun i ↦ X ↑i
inst✝³ : HasProduct fun i ↦ X ↑i
inst✝² : HasProduct fun i ↦ Y ↑i
inst✝¹ : HasProduct fun i ↦ Y ↑i
inst✝ : (i : I) → Decidable (P i)
⊢ map f =
    ((binaryFanOfPropIsLimit X P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i ↦ X ↑i) (∏ᶜ fun i ↦ X ↑i))).hom ≫
      prod.map (map fun i ↦ f ↑i) (map fun i ↦ f ↑i) ≫
        ((binaryFanOfPropIsLimit Y P).conePointUniqueUpToIso (prodIsProd (∏ᶜ fun i ↦ Y ↑i) (∏ᶜ fun i ↦ Y ↑i))).inv

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝¹ : Cone (pair F G)
x✝ : x✝¹.pt ⟶ (binaryProductCone F G).pt
h : ∀ (j : Discrete WalkingPair), x✝ ≫ (binaryProductCone F G).π.app j = x✝¹.π.app j
⊢ x✝ = prod.lift (BinaryFan.fst x✝¹) (BinaryFan.snd x✝¹)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ (binaryProductIso F G).inv ≫ Limits.prod.fst = prod.fst

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ (binaryProductIso F G).inv ≫ Limits.prod.snd = prod.snd

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
x : F.obj a
y : G.obj a
⊢ (hom (Limits.prod.fst.app a)) (prodMk x y) = x

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
x : F.obj a
y : G.obj a
⊢ (hom (Limits.prod.snd.app a)) (prodMk x y) = y

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
x✝ : (F ⨯ G).obj a
⊢ (fun z ↦ prodMk z.1 z.2)
      ((fun z ↦ (((hom ((binaryProductIso F G).hom.app a)) z).1, ((hom ((binaryProductIso F G).hom.app a)) z).2)) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
x✝ : F.obj a × G.obj a
⊢ (fun z ↦ (((hom ((binaryProductIso F G).hom.app a)) z).1, ((hom ((binaryProductIso F G).hom.app a)) z).2))
      ((fun z ↦ prodMk z.1 z.2) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
z w : (F ⨯ G).obj a
h1 : (hom (Limits.prod.fst.app a)) z = (hom (Limits.prod.fst.app a)) w
h2 : (hom (Limits.prod.snd.app a)) z = (hom (Limits.prod.snd.app a)) w
⊢ z = w

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝ : C
⊢ ↾Sum.map ⇑(hom (F.map (𝟙 x✝))) ⇑(hom (G.map (𝟙 x✝))) = 𝟙 (F.obj x✝ ⊕ G.obj x✝)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
X✝ Y✝ Z✝ : C
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ↾Sum.map ⇑(hom (F.map (x✝¹ ≫ x✝))) ⇑(hom (G.map (x✝¹ ≫ x✝))) =
    ↾Sum.map ⇑(hom (F.map x✝¹)) ⇑(hom (G.map x✝¹)) ≫ ↾Sum.map ⇑(hom (F.map x✝)) ⇑(hom (G.map x✝))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G F₁ F₂ : C ⥤ Type w
τ₁ : F₁ ⟶ F
τ₂ : F₂ ⟶ F
x✝² x✝¹ : C
x✝ : x✝² ⟶ x✝¹
⊢ (coprod F₁ F₂).map x✝ ≫ ↾Sum.elim ⇑(hom (τ₁.app x✝¹)) ⇑(hom (τ₂.app x✝¹)) =
    ↾Sum.elim ⇑(hom (τ₁.app x✝²)) ⇑(hom (τ₂.app x✝²)) ≫ F.map x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
x✝¹ : Cocone (pair F G)
x✝ : (binaryCoproductCocone F G).pt ⟶ x✝¹.pt
h : ∀ (j : Discrete WalkingPair), (binaryCoproductCocone F G).ι.app j ≫ x✝ = x✝¹.ι.app j
⊢ x✝ = coprod.desc (BinaryCofan.inl x✝¹) (BinaryCofan.inr x✝¹)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ Limits.coprod.inl ≫ (binaryCoproductIso F G).hom = coprod.inl

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
⊢ Limits.coprod.inr ≫ (binaryCoproductIso F G).hom = coprod.inr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
x✝ : (F ⨿ G).obj a
⊢ (fun z ↦ (hom ((binaryCoproductIso F G).inv.app a)) z) ((fun z ↦ (hom ((binaryCoproductIso F G).hom.app a)) z) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : C ⥤ Type w
a : C
x✝ : F.obj a ⊕ G.obj a
⊢ (fun z ↦ (hom ((binaryCoproductIso F G).hom.app a)) z) ((fun z ↦ (hom ((binaryCoproductIso F G).inv.app a)) z) x✝) =
    x✝

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
⊢ h.p₂ ≫ f₂ = h.p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
l : h.LiftStruct g₁ g₂ b
⊢ g₁ ≫ f₁ = g₂ ≫ f₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
f : Y ⟶ h.pullback
f_p₁ : f ≫ h.p₁ = g₁
f_p₂ : f ≫ h.p₂ = g₂
f_p✝¹ : f ≫ h.p = b
f' : Y ⟶ h.pullback
f'_p₁ : f' ≫ h.p₁ = g₁
f'_p₂ : f' ≫ h.p₂ = g₂
f_p✝ : f' ≫ h.p = b
⊢ f = f'

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
⊢ ∀ (a b_1 : h.LiftStruct g₁ g₂ b), a = b_1

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
w : g₁ ≫ f₁ = g₂ ≫ f₂
hf₁ : g₁ ≫ f₁ = b
l : Y ⟶ h.pullback
h₁ : l ≫ h.p₁ = g₁
h₂ : l ≫ h.p₂ = g₂
⊢ l ≫ h.p = b

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
h : ChosenPullback f₁ f₂
Y : C
g₁ : Y ⟶ X₁
g₂ : Y ⟶ X₂
b : Y ⟶ S
w : g₁ ≫ f₁ = g₂ ≫ f₂
hf₁ : g₁ ≫ f₁ = b
⊢ Nonempty (h.LiftStruct g₁ g₂ b)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X S : C
f : X ⟶ S
h : ChosenPullback f f
⊢ Nonempty h.Diagonal

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₂ ≫ h₁₂.p₁ = h.p₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₂ ≫ h₁₂.p₂ = h.p₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂₃ ≫ h₂₃.p₁ = h.p₂

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂₃ ≫ h₂₃.p₂ = h.p₃

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₃ ≫ h₁₃.p₁ = h.p₁

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₃ ≫ h₁₃.p₂ = h.p₃

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁ ≫ f₁ = h.p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₃ ≫ f₃ = h.p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₂ ≫ f₂ = h.p

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₁ X₂ X₃ S : C
f₁ : X₁ ⟶ S
f₂ : X₂ ⟶ S
f₃ : X₃ ⟶ S
h₁₂ : ChosenPullback f₁ f₂
h₂₃ : ChosenPullback f₂ f₃
h₁₃ : ChosenPullback f₁ f₃
h : ChosenPullback₃ h₁₂ h₂₃ h₁₃
⊢ h.p₁₂ ≫ h₁₂.p = h.p

Tactic:
by

Goal state after: