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

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : t.unop.pt ⟶ s.pt
w : ∀ (j : J), t.unop.ι.app j ≫ m = s.ι.app j
⊢ ∀ (j : Jᵒᵖ), m.op ≫ t.π.app j = (s.ι.app (Opposite.unop j)).op

Tactic:
intro j

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cone F.op
P : IsLimit t
s : Cocone F
m : t.unop.pt ⟶ s.pt
w : ∀ (j : J), t.unop.ι.app j ≫ m = s.ι.app j
j : Jᵒᵖ
⊢ m.op ≫ t.π.app j = (s.ι.app (Opposite.unop j)).op
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ (𝟭 (WidePushoutShape J)).obj none =
    ((wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)) ⋙
          wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)).obj
      none

Tactic:
simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J
⊢ (𝟭 (WidePushoutShape J)).obj (some val✝) =
    ((wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)) ⋙
          wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)).obj
      (some val✝)

Tactic:
simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      none =
    (𝟭 (WidePushoutShape J')).obj none

Tactic:
simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
J' : Type w'
h : J ≃ J'
val✝ : J'
⊢ ((wideSpan none (fun j ↦ some (h.invFun j)) fun j ↦ Hom.init (h.invFun j)) ⋙
          wideSpan none (fun j ↦ some (h j)) fun j ↦ Hom.init (h j)).obj
      (some val✝) =
    (𝟭 (WidePushoutShape J')).obj (some val✝)

Tactic:
simp

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

Goal state before:
pp: J : Type w
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
⊢ ∀ (j : J), (g ≫ π arrows j) ≫ arrows j = g ≫ base arrows

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.HasLimits

Goal state before:
pp: J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ t.unop.pt
w : ∀ (j : J), m ≫ t.unop.π.app j = s.π.app j
⊢ ∀ (j : Jᵒᵖ), t.ι.app j ≫ m.op = (s.π.app (Opposite.unop j)).op

Tactic:
intro j

Goal state after:
J : Type u₁
inst✝² : Category.{v₁, u₁} J
K : Type u₂
inst✝¹ : Category.{v₂, u₂} K
C : Type u
inst✝ : Category.{v, u} C
F : J ⥤ C
t : Cocone F.op
P : IsColimit t
s : Cone F
m : s.pt ⟶ t.unop.pt
w : ∀ (j : J), m ≫ t.unop.π.app j = s.π.app j
j : Jᵒᵖ
⊢ t.ι.app j ≫ m.op = (s.π.app (Opposite.unop j)).op
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
⊢ ∀ (i : ι'), s.π (e i) ≫ f (e i) = s.base

Tactic:
simp

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

Goal state before:
pp: J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
ι' : Type u_3
e : ι' ≃ ι
i : ι
⊢ ((WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor ⋙
          WidePullbackShape.wideCospan X (fun i ↦ Y (e i)) fun i ↦ f (e i)).obj
      (some i) =
    (WidePullbackShape.wideCospan X Y f).obj (some i)

Tactic:
simp

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

Goal state before:
pp: case refl
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasCoproduct f
j : J
⊢ eqToHom ⋯ ≫ ι f j = ι f j

Tactic:
simp

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

Goal state before:
pp: case e'_5
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
b✝ : β
⊢ (Sigma.ι f b✝ ≫ Sigma.desc fun a ↦ Sigma.ι f a) = Sigma.ι f b✝ ≫ 𝟙 (∐ f)

Tactic:
simp

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

Goal state before:
pp: J : Type w
C✝ : Type u
inst✝² : Category.{v, u} C✝
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
j : J
⊢ (arrows j ≫ ι arrows j) ≫ g = head arrows ≫ g

Tactic:
simp

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
b✝ : α
⊢ (map fun a ↦ 𝟙 (f a)) ≫ π f b✝ = 𝟙 (∏ᶜ f) ≫ π f b✝

Tactic:
simp

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
b✝ : α
⊢ (map q ≫ map q') ≫ π h b✝ = (map fun a ↦ q a ≫ q' a) ≫ π h b✝

Tactic:
simp

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasProduct f
b✝ : α
⊢ (map' id fun a ↦ 𝟙 (f a)) ≫ π f b✝ = 𝟙 (∏ᶜ f) ≫ π f b✝

Tactic:
simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
p' : γ → β
q : (b : β) → f (p b) ⟶ g b
q' : (c : γ) → g (p' c) ⟶ h c
b✝ : γ
⊢ (map' p q ≫ map' p' q') ≫ π h b✝ = (map' (p ∘ p') fun c ↦ q (p' c) ≫ q' c) ≫ π h b✝

Tactic:
simp

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (b : β) → f (p b) ⟶ g b
q' : (b : β) → g b ⟶ h b
b✝ : β
⊢ (map' p q ≫ map q') ≫ π h b✝ = (map' p fun b ↦ q b ≫ q' b) ≫ π h b✝

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
h : HasLimit F₁
⊢ ∀ ⦃X Y : Discrete PEmpty.{w' + 1}⦄ (f : X ⟶ Y),
    ((Functor.const (Discrete PEmpty.{w' + 1})).obj (limit F₁)).map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X fun as ↦ ⋯.elim) ≫ F₂.map f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
F₁ : Discrete PEmpty.{w + 1} ⥤ C
F₂ : Discrete PEmpty.{w' + 1} ⥤ C
h : HasColimit F₁
⊢ ∀ ⦃X Y : Discrete PEmpty.{w' + 1}⦄ (f : X ⟶ Y),
    F₂.map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X fun as ↦ ⋯.elim) ≫ ((Functor.const (Discrete PEmpty.{w' + 1})).obj (colimit F₁)).map f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsTerminal X
F : Discrete PEmpty.{1} ⥤ C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    ((Functor.const (Discrete PEmpty.{1})).obj X).map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X_1 fun as ↦ ⋯.elim) ≫ F.map f

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
h : IsInitial X
F : Discrete PEmpty.{1} ⥤ C
⊢ ∀ ⦃X_1 Y : Discrete PEmpty.{1}⦄ (f : X_1 ⟶ Y),
    F.map f ≫ id (Discrete.casesOn Y fun as ↦ ⋯.elim) =
      id (Discrete.casesOn X_1 fun as ↦ ⋯.elim) ≫ ((Functor.const (Discrete PEmpty.{1})).obj X).map f

Tactic:
simp

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g : α → C
h : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (a : α) → f a ⟶ g a
q' : (b : β) → g (p b) ⟶ h b
b✝ : β
⊢ (map q ≫ map' p q') ≫ π h b✝ = (map' p fun b ↦ q (p b) ≫ q' b) ≫ π h b✝

Tactic:
simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X : Discrete α ⥤ C
inst✝ : HasProduct fun j ↦ X.obj { as := j }
s : Cone X
⊢ ∀ (j : Discrete α), (Pi.lift fun j ↦ s.π.app { as := j }) ≫ (Pi.cone X).π.app j = s.π.app j

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramInitial I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝ : HasLimit F
⊢ limit.lift F (coneOfDiagramInitial I F) ≫ limit.π F j = 𝟙 (F.obj j)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j✝ : J
⊢ (limit.π F j ≫ limit.lift F (coneOfDiagramTerminal I F)) ≫ limit.π F j✝ = 𝟙 (limit F) ≫ limit.π F j✝

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
⊢ limit.lift F (coneOfDiagramTerminal I F) ≫ limit.π F j = 𝟙 (F.obj j)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝ : HasColimit F
⊢ colimit.ι F j ≫ colimit.desc F (coconeOfDiagramTerminal I F) = 𝟙 (F.obj j)

Tactic:
simp

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
b✝ : α
⊢ (ι f b✝ ≫ map fun a ↦ 𝟙 (f a)) = ι f b✝ ≫ 𝟙 (∐ f)

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u
inst✝¹ : Category.{v, u} J
j : J
I : IsTerminal j
F : J ⥤ C
inst✝ : HasColimit F
j✝ : J
⊢ colimit.ι F j✝ ≫ colimit.desc F (coconeOfDiagramTerminal I F) ≫ colimit.ι F j = colimit.ι F j✝ ≫ 𝟙 (colimit F)

Tactic:
simp

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g h : α → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
b✝ : α
⊢ ι f b✝ ≫ map q ≫ map q' = ι f b✝ ≫ map fun a ↦ q a ≫ q' a

Tactic:
simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
J : Type u
inst✝² : Category.{v, u} J
j : J
I : IsInitial j
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : ∀ (i j : J) (f : i ⟶ j), IsIso (F.map f)
j✝ : J
⊢ colimit.ι F j✝ ≫ colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = colimit.ι F j✝ ≫ 𝟙 (colimit F)

Tactic:
simp

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

Goal state before:
pp: α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
b✝ : α
⊢ (ι f b✝ ≫ map' id fun a ↦ 𝟙 (f a)) = ι f b✝ ≫ 𝟙 (∐ f)

Tactic:
simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
p' : β → γ
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h (p' b)
b✝ : α
⊢ ι f b✝ ≫ map' p q ≫ map' p' q' = ι f b✝ ≫ map' (p' ∘ p) fun a ↦ q a ≫ q' (p a)

Tactic:
simp

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f : α → C
g h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h b
b✝ : α
⊢ ι f b✝ ≫ map' p q ≫ map q' = ι f b✝ ≫ map' p fun a ↦ q a ≫ q' (p a)

Tactic:
simp

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

Goal state before:
pp: β : Type w
α : Type w₂
C : Type u
inst✝³ : Category.{v, u} C
f g : α → C
h : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
inst✝ : HasCoproduct h
p : α → β
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h (p a)
b✝ : α
⊢ ι f b✝ ≫ map q ≫ map' p q' = ι f b✝ ≫ map' p fun a ↦ q a ≫ q' a

Tactic:
simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X : Discrete α ⥤ C
inst✝ : HasCoproduct fun j ↦ X.obj { as := j }
s : Cocone X
⊢ ∀ (j : Discrete α), ((Sigma.cocone X).ι.app j ≫ Sigma.desc fun j ↦ s.ι.app { as := j }) = s.ι.app j

Tactic:
simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
J : Type u_1
K : Type u_2
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasProduct f
inst✝ : HasProduct g
k : K
⊢ g (e (e.symm k)) = g k

Tactic:
simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
J : Type u_1
K : Type u_2
f : J → C
g : K → C
e : J ≃ K
w : (j : J) → g (e j) ≅ f j
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct g
k : K
⊢ g k = g (e (e.symm k))

Tactic:
simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasProduct (g i)
inst✝ : HasProduct fun i ↦ ∏ᶜ g i
⊢ ∀ (s : Fan fun p ↦ g p.fst p.snd) (j : (i : ι) × f i),
    (Pi.lift fun b ↦ Pi.lift fun c ↦ s.proj ⟨b, c⟩) ≫
        (Fan.mk (∏ᶜ fun i ↦ ∏ᶜ g i) fun X ↦ Pi.π (fun i ↦ ∏ᶜ g i) X.fst ≫ Pi.π (g X.fst) X.snd).proj j =
      s.proj j

Tactic:
simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝² : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst✝¹ : ∀ (i : ι), HasCoproduct (g i)
inst✝ : HasCoproduct fun i ↦ ∐ g i
⊢ ∀ (t : Cofan fun p ↦ g p.fst p.snd) (j : (i : ι) × f i),
    ((Cofan.mk (∐ fun i ↦ ∐ g i) fun X ↦ Sigma.ι (g X.fst) X.snd ≫ Sigma.ι (fun i ↦ ∐ g i) X.fst).inj j ≫
        Sigma.desc fun b ↦ Sigma.desc fun c ↦ t.inj ⟨b, c⟩) =
      t.inj j

Tactic:
simp

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

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
s : Cone (Discrete.functor f)
⊢ s.π.app default ≫
      { pt := f default,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.π.app
        default =
    s.π.app default

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
x✝ : Discrete WalkingPair
⊢ c.π.app { as := left } = (Iso.refl c.pt).hom ≫ (BinaryFan.mk c.fst c.snd).π.app { as := left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
x✝ : Discrete WalkingPair
⊢ c.π.app { as := right } = (Iso.refl c.pt).hom ≫ (BinaryFan.mk c.fst c.snd).π.app { as := right }

Tactic:
simp

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
x✝ : Discrete WalkingPair
⊢ c.π.app { as := right } = (Iso.refl c.pt).hom ≫ (BinaryFan.mk c.fst c.snd).π.app { as := right }
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_1
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Fan fun x ↦ Y
⊢ (s.proj default ≫ e.inv) ≫ (mk X fun x ↦ e.hom).proj default = s.proj default

Tactic:
simp

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

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryFan X Y
x✝ : Discrete WalkingPair
⊢ c.π.app { as := right } = (Iso.refl c.pt).hom ≫ (BinaryFan.mk c.fst c.snd).π.app { as := right }

Tactic:
simp

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

Goal state before:

Tactic:
simp

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

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
x✝ : Discrete WalkingPair
⊢ c.ι.app { as := left } ≫ (Iso.refl c.pt).hom = (BinaryCofan.mk c.inl c.inr).ι.app { as := left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
x✝ : Discrete WalkingPair
⊢ c.ι.app { as := right } ≫ (Iso.refl c.pt).hom = (BinaryCofan.mk c.inl c.inr).ι.app { as := right }

Tactic:
simp

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
x✝ : Discrete WalkingPair
⊢ c.ι.app { as := right } ≫ (Iso.refl c.pt).hom = (BinaryCofan.mk c.inl c.inr).ι.app { as := right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ X Y : C
c : BinaryCofan X Y
x✝ : Discrete WalkingPair
⊢ c.ι.app { as := right } ≫ (Iso.refl c.pt).hom = (BinaryCofan.mk c.inl c.inr).ι.app { as := right }

Tactic:
simp

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

Goal state before:
pp: case refine_1
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Cofan fun x ↦ X
⊢ (mk Y fun x ↦ e.hom).inj default ≫ e.inv ≫ s.inj default = s.inj default

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
a✝ : IsIso c.fst
T✝ : C
x✝¹ : T✝ ⟶ X
x✝ : T✝ ⟶ Y
⊢ (x✝¹ ≫ inv c.fst) ≫ c.fst = x✝¹

Tactic:
simp

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

Goal state before:
pp: case fac_left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right })), IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst ≫ f = s.fst

Tactic:
simp

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

Goal state before:
pp: case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right })), IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd = s.snd

Tactic:
simp

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

Goal state before:
pp: β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ⇑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' ⋯) ≫ colimit.ι (Discrete.functor f) { as := ε b } =
    colimit.ι (Discrete.functor f) { as := ε (ε.symm (ε b)) }
⊢ eqToHom ⋯ ≫ colimit.ι (Discrete.functor f) { as := ε b } = ι f (ε b)

Tactic:
simp

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

Goal state before:
pp: case p
β : Type w
C : Type u
inst✝² : Category.{v, u} C
γ : Type w'
ε : β ≃ γ
f : γ → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct (f ∘ ⇑ε)
b : β
h :
  (Discrete.functor f).map (Discrete.eqToHom' ⋯) ≫ colimit.ι (Discrete.functor f) { as := ε b } =
    colimit.ι (Discrete.functor f) { as := ε (ε.symm (ε b)) }
⊢ { as := b } = { as := ε.symm (ε b) }

Tactic:
simp

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

Goal state before:
pp: case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan fun j ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan fun i ↦ (c i).pt
hc' : IsLimit c'
⊢ ∀ (s : Fan fun p ↦ X p.1 p.2) (j : ι × ι'),
    (lift hc' fun i ↦ lift (hc i) fun j ↦ s.proj (i, j)) ≫
        (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).proj j =
      s.proj j

Tactic:
simp

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

Goal state before:
pp: case fac_left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right })), (f ≫ c.inl) ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr = s.inl

Tactic:
simp

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

Goal state before:
pp: case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right })), c.inr ≫ IsColimit.desc h (inv f ≫ s.inl) s.inr = s.inr

Tactic:
simp

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

Goal state before:
pp: case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Cofan fun j ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan fun i ↦ (c i).pt
hc' : IsColimit c'
⊢ ∀ (t : Cofan fun p ↦ X p.1 p.2) (j : ι × ι'),
    ((Cofan.mk c'.pt fun p ↦ (c p.1).inj p.2 ≫ c'.inj p.1).inj j ≫ desc hc' fun i ↦ desc (hc i) fun j ↦ t.inj (i, j)) =
      t.inj j

Tactic:
simp

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

Goal state before:
pp: case h₁
C : Type u
inst✝¹ : Category.{v, u} C
V W X Y : C
inst✝ : HasBinaryProduct X Y
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ fst = lift (f ≫ g) (f ≫ h) ≫ fst

Tactic:
simp

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

Goal state before:
pp: case h₂
C : Type u
inst✝¹ : Category.{v, u} C
V W X Y : C
inst✝ : HasBinaryProduct X Y
f : V ⟶ W
g : W ⟶ X
h : W ⟶ Y
⊢ (f ≫ lift g h) ≫ snd = lift (f ≫ g) (f ≫ h) ≫ snd

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
inst✝ : HasBinaryProduct Y Y
f : X ⟶ Y
⊢ f ≫ diag Y = lift f f

Tactic:
simp

Goal state after: