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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : Discrete WalkingPair ⥤ C
f : F.obj { as := left } ⟶ G.obj { as := left }
g : F.obj { as := right } ⟶ G.obj { as := right }
x✝² x✝¹ : Discrete WalkingPair
X Y : WalkingPair
x✝ : { as := X } ⟶ { as := Y }
u : { as := X }.as = { as := Y }.as
⊢ (F.map { down := { down := u } } ≫
      match { as := Y } with
      | { as := left } => f
      | { as := right } => g) =
    (match { as := X } with
      | { as := left } => f
      | { as := right } => g) ≫
      G.map { down := { down := u } }

Tactic:
by

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)
⊢ map q ≫ map' p q' = map' p fun a ↦ q a ≫ q' a

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F G : Discrete WalkingPair ⥤ C
f✝ : F.obj { as := left } ⟶ G.obj { as := left }
g✝ : F.obj { as := right } ⟶ G.obj { as := right }
f : F.obj { as := left } ≅ G.obj { as := left }
g : F.obj { as := right } ≅ G.obj { as := right }
X✝ Y✝ : Discrete WalkingPair
x✝ : X✝ ⟶ Y✝
u : X✝.as = Y✝.as
⊢ F.map { down := { down := u } } ≫
      (match Y✝ with
        | { as := left } => f
        | { as := right } => g).hom =
    (match X✝ with
        | { as := left } => f
        | { as := right } => g).hom ≫
      G.map { down := { down := u } }

Tactic:
by

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 : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct g
p p' : α → β
q : (a : α) → f a ⟶ g (p a)
q' : (a : α) → f a ⟶ g (p' a)
hp : p = p'
hq : ∀ (a : α), q a ≫ eqToHom ⋯ = q' a
⊢ map' p q = map' p' q'

Tactic:
by

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:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryFan A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
j : Discrete WalkingPair
⊢ c.π.app j = e.hom ≫ c'.π.app j

Tactic:
by

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
m : (Sigma.cocone X).pt ⟶ s.pt
hm : ∀ (j : Discrete α), (Sigma.cocone X).ι.app j ≫ m = s.ι.app j
⊢ m = Sigma.desc fun j ↦ s.ι.app { as := j }

Tactic:
by

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:
by

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:
by

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:
by

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)
    (m : s.pt ⟶ (Fan.mk (∏ᶜ fun i ↦ ∏ᶜ g i) fun X ↦ Pi.π (fun i ↦ ∏ᶜ g i) X.fst ≫ Pi.π (g X.fst) X.snd).pt),
    (∀ (j : (i : ι) × f i),
        m ≫ (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) →
      m = Pi.lift fun b ↦ Pi.lift fun c ↦ s.proj ⟨b, c⟩

Tactic:
by

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:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryFan X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
⊢ ∀ (s_1 : Cone (pair X Y)) (j : Discrete WalkingPair), lift (fst s_1) (snd s_1) ≫ s.π.app j = s_1.π.app j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
A B : C
c c' : BinaryCofan A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
j : Discrete WalkingPair
⊢ c.ι.app j ≫ e.hom = c'.ι.app j

Tactic:
by

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)
    (m : (Cofan.mk (∐ fun i ↦ ∐ g i) fun X ↦ Sigma.ι (g X.fst) X.snd ≫ Sigma.ι (fun i ↦ ∐ g i) X.fst).pt ⟶ t.pt),
    (∀ (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 ≫ m =
          t.inj j) →
      m = Sigma.desc fun b ↦ Sigma.desc fun c ↦ t.inj ⟨b, c⟩

Tactic:
by

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

Goal state before:
pp: β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct fun b ↦ G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
⊢ G.map (Pi.lift g) ≫ piComparison G f = Pi.lift fun j ↦ G.map (g j)

Tactic:
by

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

Goal state before:
pp: β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun b ↦ G.obj (f b)
P : C
g : (j : β) → f j ⟶ P
⊢ sigmaComparison G f ≫ G.map (Sigma.desc g) = Sigma.desc fun j ↦ G.map (g j)

Tactic:
by

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

Goal state before:
pp: β : Type w
C : Type u
inst✝³ : Category.{v, u} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct fun b ↦ G.obj (f b)
P : C
g : (j : β) → f j ⟶ P
⊢ sigmaComparison G f ≫ G.map (Sigma.desc g) = Sigma.desc fun j ↦ G.map (g j)

Tactic:
by
  ext j
  simp only [ι_comp_sigmaComparison_assoc, ← G.map_comp, colimit.ι_desc, Cofan.mk_ι_app]

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✝ : HasProducts C
X : C
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (yoneda.obj X ⋙ (piConst.obj X).rightOp).map x✝ ≫ (Pi.lift id).op = (Pi.lift id).op ≫ (𝟭 Cᵒᵖ).map x✝

Tactic:
by

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✝ : HasProducts C
X : C
x✝ : Type v
⊢ (piConst.obj X).rightOp.map ({ app := fun n ↦ ↾fun i ↦ Pi.π (fun x ↦ X) i, naturality := ⋯ }.app x✝) ≫
      { app := fun Y ↦ (Pi.lift id).op, naturality := ⋯ }.app ((piConst.obj X).rightOp.obj x✝) =
    𝟙 ((piConst.obj X).rightOp.obj x✝)

Tactic:
by

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
x✝ : Discrete β
j : β
⊢ ((Functor.const (Discrete β)).obj (f default)).obj { as := j } = (Discrete.functor f).obj { as := j }

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
⊢ ∀ (s_1 : Cocone (pair X Y)) (j : Discrete WalkingPair), s.ι.app j ≫ desc (inl s_1) (inr s_1) = s_1.ι.app j

Tactic:
by

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)
j : Discrete β
⊢ s.π.app default ≫
      { pt := f default,
              π :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.π.app
        j =
    s.π.app j

Tactic:
by

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)
m :
  s.pt ⟶
    { pt := f default,
        π :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => eqToHom ⋯ }.pt
w :
  ∀ (j : Discrete β),
    m ≫
        { pt := f default,
                π :=
                  Discrete.natTrans fun x ↦
                    match x with
                    | { as := j } => eqToHom ⋯ }.π.app
          j =
      s.π.app j
⊢ m = s.π.app default

Tactic:
by

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

Goal state before:
pp: β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
b : β
⊢ (productUniqueIso f).inv ≫ Pi.π f b = eqToHom ⋯

Tactic:
by

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

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

Tactic:
by

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 Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
⊢ IsLimit (mk X fun x ↦ e.hom)

Tactic:
by

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
x✝ : Discrete β
j : β
⊢ (Discrete.functor f).obj { as := j } = ((Functor.const (Discrete β)).obj (f default)).obj { as := j }

Tactic:
by

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 : Cocone (Discrete.functor f)
j : Discrete β
⊢ { pt := f default,
              ι :=
                Discrete.natTrans fun x ↦
                  match x with
                  | { as := j } => eqToHom ⋯ }.ι.app
        j ≫
      s.ι.app default =
    s.ι.app j

Tactic:
by

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

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

Tactic:
by

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 : Cocone (Discrete.functor f)
m :
  { pt := f default,
        ι :=
          Discrete.natTrans fun x ↦
            match x with
            | { as := j } => eqToHom ⋯ }.pt ⟶
    s.pt
w :
  ∀ (j : Discrete β),
    { pt := f default,
                ι :=
                  Discrete.natTrans fun x ↦
                    match x with
                    | { as := j } => eqToHom ⋯ }.ι.app
          j ≫
        m =
      s.ι.app j
⊢ m = s.ι.app default

Tactic:
by

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

Goal state before:
pp: β : Type w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Unique β
f : β → C
b : β
⊢ Sigma.ι f b ≫ (coproductUniqueIso f).hom = eqToHom ⋯

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y W : C
fst : W ⟶ X
snd : W ⟶ Y
lift : (s : BinaryFan X Y) → s.pt ⟶ W
fac_left : ∀ (s : BinaryFan X Y), lift s ≫ fst = s.fst
fac_right : ∀ (s : BinaryFan X Y), lift s ≫ snd = s.snd
uniq : ∀ (s : BinaryFan X Y) (m : s.pt ⟶ W), m ≫ fst = s.fst → m ≫ snd = s.snd → m = lift s
s : Cone (pair X Y)
j : Discrete WalkingPair
⊢ lift s ≫ (mk fst snd).π.app j = s.π.app j

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y W : C
inl : X ⟶ W
inr : Y ⟶ W
desc : (s : BinaryCofan X Y) → W ⟶ s.pt
fac_left : ∀ (s : BinaryCofan X Y), inl ≫ desc s = s.inl
fac_right : ∀ (s : BinaryCofan X Y), inr ≫ desc s = s.inr
uniq : ∀ (s : BinaryCofan X Y) (m : W ⟶ s.pt), inl ≫ m = s.inl → inr ≫ m = s.inr → m = desc s
s : Cocone (pair X Y)
j : Discrete WalkingPair
⊢ (mk inl inr).ι.app j ≫ desc s = s.ι.app j

Tactic:
by

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
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ c.fst = 𝟙 X
⊢ (c.fst ≫ l) ≫ c.fst = 𝟙 (((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }) ≫ c.fst

Tactic:
by

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 Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
⊢ IsColimit (mk Y fun x ↦ e.hom)

Tactic:
by

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:
by

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✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ⇑ε)
b : β
⊢ (reindex ε f).hom ≫ π f (ε b) = π (f ∘ ⇑ε) b

Tactic:
by

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✝¹ : T✝ ⟶ c.pt
e : x✝¹ ≫ c.fst = x✝³
x✝ : x✝¹ ≫ c.snd = x✝²
⊢ x✝¹ = x✝³ ≫ inv c.fst

Tactic:
by

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✝¹ : HasProduct f
inst✝ : HasProduct (f ∘ ⇑ε)
b : β
⊢ (reindex ε f).inv ≫ π (f ∘ ⇑ε) b = π f (ε b)

Tactic:
by

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
⊢ Nonempty (IsLimit c) ↔ IsIso c.fst

Tactic:
by

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 X
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) ↔ IsIso c.snd

Tactic:
by

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 : β
⊢ ι (f ∘ ⇑ε) b ≫ (reindex ε f).hom = ι f (ε b)

Tactic:
by

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 : β
⊢ ι f (ε b) ≫ (reindex ε f).inv = ι (f ∘ ⇑ε) b

Tactic:
by

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₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ C
inst✝¹ : HasLimit F
inst✝ : HasProduct F.obj
Z✝ : C
x✝¹ x✝ : Z✝ ⟶ limit F
h : x✝¹ ≫ Pi.lift (limit.π F) = x✝ ≫ Pi.lift (limit.π F)
⊢ x✝¹ = x✝

Tactic:
by

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₂
inst✝² : Category.{v₂, u₂} J
F : J ⥤ C
inst✝¹ : HasColimit F
inst✝ : HasCoproduct F.obj
Z✝ : C
x✝¹ x✝ : colimit F ⟶ Z✝
h : Sigma.desc (colimit.ι F) ≫ x✝¹ = Sigma.desc (colimit.ι F) ≫ x✝
⊢ x✝¹ = x✝

Tactic:
by

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✝¹ : Quiver.IsThin C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ ∀ (s : Fan K.obj) (j : J),
    hc.lift { pt := s.pt, π := { app := fun j ↦ s.proj j, naturality := ⋯ } } ≫ (Fan.mk c.pt c.π.app).proj j = s.proj j

Tactic:
by

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✝¹ : Quiver.IsThin C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c : Cone K
hc : IsLimit c
⊢ ∀ (s : Fan K.obj) (m : s.pt ⟶ (Fan.mk c.pt c.π.app).pt),
    (∀ (j : J), m ≫ (Fan.mk c.pt c.π.app).proj j = s.proj j) →
      m = hc.lift { pt := s.pt, π := { app := fun j ↦ s.proj j, naturality := ⋯ } }

Tactic:
by

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✝¹ : Quiver.IsThin C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c : Cocone K
hc : IsColimit c
⊢ ∀ (t : Cofan K.obj) (j : J),
    (Cofan.mk c.pt c.ι.app).inj j ≫ hc.desc { pt := t.pt, ι := { app := fun j ↦ t.inj j, naturality := ⋯ } } = t.inj j

Tactic:
by

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✝¹ : Quiver.IsThin C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
K : J ⥤ C
c : Cocone K
hc : IsColimit c
⊢ ∀ (t : Cofan K.obj) (m : (Cofan.mk c.pt c.ι.app).pt ⟶ t.pt),
    (∀ (j : J), (Cofan.mk c.pt c.ι.app).inj j ≫ m = t.inj j) →
      m = hc.desc { pt := t.pt, ι := { app := fun j ↦ t.inj j, naturality := ⋯ } }

Tactic:
by

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

Goal state before:
pp: 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
⊢ IsLimit (mk (c.fst ≫ f) c.snd)

Tactic:
by

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 : IsInitial Y
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ IsIso c.inl

Tactic:
by

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 : IsInitial X
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) ↔ IsIso c.inr

Tactic:
by

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
ι' : 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'
t : Fan fun p ↦ X p.1 p.2
m : t.pt ⟶ (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).pt
hm : ∀ (j : ι × ι'), m ≫ (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).proj j = t.proj j
i : ι
j : ι'
⊢ (m ≫ c'.proj i) ≫ (c i).proj j = ((lift hc' fun i ↦ lift (hc i) fun j ↦ t.proj (i, j)) ≫ c'.proj i) ≫ (c i).proj j

Tactic:
by

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
ι' : 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'
⊢ IsLimit (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2)

Tactic:
by

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

Goal state before:
pp: 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
⊢ IsColimit (mk (f ≫ c.inl) c.inr)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: 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 = lift (f ≫ g) (f ≫ h)

Tactic:
by

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:
by

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 X Y
⊢ map (𝟙 X) (𝟙 Y) = 𝟙 (X ⨯ Y)

Tactic:
by

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 X Y
⊢ lift fst snd = 𝟙 (X ⨯ Y)

Tactic:
by

Goal state after: