mathlib-initiative/mathlib-tactics huggingface dataset:
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:
by

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:
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
e : β ≃ α
iso : (j : β) → g j ≅ f (e j)
⊢ HasCoproduct g

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✝ : HasProduct f
e : β ≃ α
iso : (j : β) → g j ≅ f (e j)
⊢ HasProduct g

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
f : J → C
inst✝ : HasProduct f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
f : J → C
inst✝ : HasProduct f
j j' : J
w : j = j'
⊢ π f j ≫ eqToHom ⋯ = π f 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
f : J → C
inst✝ : HasCoproduct f
j j' : J
w : j = j'
⊢ f j = f j'

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
β : Type w
f : β → C
inst✝ : HasProduct f
P : C
p : (b : β) → P ⟶ f b
b : β
⊢ lift p ≫ π f b = p b

Tactic:
by

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)).map
        (WidePullbackShape.Hom.term i) ≫
      (Iso.refl X).hom =
    (eqToIso ⋯).hom ≫ (WidePullbackShape.wideCospan X Y f).map (WidePullbackShape.Hom.term i)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
β : Type w
f : β → C
inst✝ : HasCoproduct f
P : C
p : (b : β) → f b ⟶ P
b : β
⊢ ι f b ≫ desc p = p 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
f : β → C
inst✝ : HasCoproduct f
⊢ IsIso (Sigma.desc fun a ↦ Sigma.ι f a)

Tactic:
by

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 : ι' ≃ ι
⊢ (Iso.refl
          ((Cone.postcompose (WidePullbackShape.functorExt (Iso.refl X) (fun i ↦ eqToIso ⋯) ⋯).hom).obj
              (Cone.whisker (WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e))).pt).hom ≫
      s.base =
    base
      ((Cone.postcompose (WidePullbackShape.functorExt (Iso.refl X) (fun i ↦ eqToIso ⋯) ⋯).hom).obj
        (Cone.whisker (WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e)))

Tactic:
by

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 : ι
⊢ (Iso.refl
          ((Cone.postcompose (WidePullbackShape.functorExt (Iso.refl X) (fun i ↦ eqToIso ⋯) ⋯).hom).obj
              (Cone.whisker (WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e))).pt).hom ≫
      s.π i =
    π
      ((Cone.postcompose (WidePullbackShape.functorExt (Iso.refl X) (fun i ↦ eqToIso ⋯) ⋯).hom).obj
        (Cone.whisker (WidePullbackShape.equivalenceOfEquiv ι' e.symm).functor (s.reindex e)))
      i

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: J : Type w
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
j : J
⊢ ι arrows j ≫ desc f fs w = fs j

Tactic:
by

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

Goal state before:
pp: J : Type w
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
⊢ head arrows ≫ desc f fs w = f

Tactic:
by

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

Goal state before:
pp: J : Type w
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 ≫ g = fs j) → head arrows ≫ g = f → g = desc f fs w

Tactic:
intro h1 h2

Goal state after:
J : Type w
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
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
⊢ g = desc f fs w
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: J : Type w
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 ≫ g = fs j) → head arrows ≫ g = f → g = desc f fs w

Tactic:
by

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

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

Goal state before:
pp: J : Type w
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
g : widePushout B objs arrows ⟶ X
⊢ g = desc (head arrows ≫ g) (fun j ↦ ι arrows j ≫ g) ⋯

Tactic:
by

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

Goal state before:
pp: J : Type w
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
g1 g2 : widePushout B objs arrows ⟶ X
⊢ (∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2) → head arrows ≫ g1 = head arrows ≫ g2 → g1 = g2

Tactic:
intro h1 h2

Goal state after:
J : Type w
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
g1 g2 : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
⊢ g1 = g2
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 : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ IsColimit
    (mk c.pt fun x ↦
      match x with
      | ⟨a, b⟩ => π a b ≫ c.inj a)

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
f g : β → C
inst✝¹ : HasProduct f
inst✝ : HasProduct g
p : (b : β) → f b ⟶ g b
b : β
⊢ map p ≫ π g b = π f b ≫ p 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
f : α → C
inst✝ : HasProduct f
⊢ (map fun a ↦ 𝟙 (f a)) = 𝟙 (∏ᶜ f)

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

Tactic:
by

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

Goal state before:
pp: J : Type w
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
g1 g2 : widePushout B objs arrows ⟶ X
⊢ (∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2) → head arrows ≫ g1 = head arrows ≫ g2 → g1 = g2

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
f g : β → C
inst✝² : HasProduct f
inst✝¹ : HasProduct g
p : (b : β) → f b ⟶ g b
inst✝ : ∀ (i : β), Mono (p i)
⊢ ∀ (j : Discrete β), Mono ((Discrete.natTrans fun X ↦ p X.as).app 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
f : α → C
inst✝ : HasProduct f
⊢ (map' id fun a ↦ 𝟙 (f a)) = 𝟙 (∏ᶜ f)

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

Tactic:
by

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 : Discrete PEmpty.{w' + 1}) → ((Functor.const (Discrete PEmpty.{w' + 1})).obj (limit F₁)).obj X ⟶ F₂.obj X

Tactic:
by

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

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 : Discrete PEmpty.{w' + 1}) → F₂.obj X ⟶ ((Functor.const (Discrete PEmpty.{w' + 1})).obj (colimit F₁)).obj X

Tactic:
by

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

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 : Discrete PEmpty.{1}) → ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1 ⟶ F.obj X_1

Tactic:
by

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

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 : Discrete PEmpty.{1}) → F.obj X_1 ⟶ ((Functor.const (Discrete PEmpty.{1})).obj X).obj X_1

Tactic:
by

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

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasTerminal C
P : C
f g : P ⟶ ⊤_ C
⊢ f = g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasInitial C
P : C
f g : ⊥_ C ⟶ P
⊢ f = g

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasTerminal C
P Q : C
f : P ⟶ Q
⊢ f ≫ «from» Q = «from» P

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : HasInitial C
P Q : C
f : P ⟶ Q
⊢ «to» P ≫ f = «to» Q

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasTerminal C
j : J
⊢ limitConstTerminal.inv ≫ limit.π ((Functor.const J).obj (⊤_ C)) j = terminal.from (⊤_ C)

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✝² : HasProduct f
inst✝¹ : HasProduct g
inst✝ : HasProduct h
p : β → α
q : (a : α) → f a ⟶ g a
q' : (b : β) → g (p b) ⟶ h b
⊢ map q ≫ map' p q' = map' p fun b ↦ q (p b) ≫ q' b

Tactic:
by

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

Goal state before:
pp: J : Type u_1
inst✝² : Category.{v_1, u_1} J
C : Type u_2
inst✝¹ : Category.{v_2, u_2} C
inst✝ : HasInitial C
j : J
⊢ colimit.ι ((Functor.const J).obj (⊥_ C)) j ≫ colimitConstInitial.hom = initial.to (⊥_ C)

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

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.π F j ≫ limit.lift F (coneOfDiagramInitial I F) = 𝟙 (limit F)

Tactic:
by

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

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.π F j ≫ limit.lift F (coneOfDiagramTerminal I F) = 𝟙 (limit F)

Tactic:
by

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

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:
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✝ : HasProduct fun j ↦ X.obj { as := j }
s : Cone X
m : s.pt ⟶ (Pi.cone X).pt
hm : ∀ (j : Discrete α), m ≫ (Pi.cone X).π.app j = s.π.app j
⊢ m = Pi.lift fun j ↦ s.π.app { as := 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
f g : β → C
inst✝¹ : HasCoproduct f
inst✝ : HasCoproduct g
p : (b : β) → f b ⟶ g b
b : β
⊢ ι f b ≫ map p = p b ≫ ι g 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
f : α → C
inst✝ : HasCoproduct f
⊢ (map fun a ↦ 𝟙 (f a)) = 𝟙 (∐ f)

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

Tactic:
by

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.desc F (coconeOfDiagramTerminal I F) ≫ colimit.ι F j = 𝟙 (colimit F)

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
f g : β → C
inst✝² : HasCoproduct f
inst✝¹ : HasCoproduct g
p : (b : β) → f b ⟶ g b
inst✝ : ∀ (i : β), Epi (p i)
⊢ ∀ (j : Discrete β), Epi ((Discrete.natTrans fun X ↦ p X.as).app j)

Tactic:
by

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)
⊢ colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = 𝟙 (colimit F)

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
f : α → C
inst✝ : HasCoproduct f
⊢ (map' id fun a ↦ 𝟙 (f a)) = 𝟙 (∐ f)

Tactic:
by

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)
⊢ colimit.ι F j ≫ colimit.desc F (coconeOfDiagramInitial I F) = 𝟙 (F.obj j) ∧
    colimit.desc F (coconeOfDiagramInitial I F) ≫ colimit.ι F j = 𝟙 (colimit F)

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

Tactic:
by

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

Goal state before:
pp: j : WalkingPair
⊢ (fun x ↦
        match x with
        | left => right
        | right => left)
      ((fun x ↦
          match x with
          | left => right
          | right => left)
        j) =
    j

Tactic:
by

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

Goal state before:
pp: j : WalkingPair
⊢ (fun b ↦ Bool.recOn b right left)
      ((fun x ↦
          match x with
          | left => true
          | right => false)
        j) =
    j

Tactic:
by

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

Goal state before:
pp: b : Bool
⊢ (fun x ↦
        match x with
        | left => true
        | right => false)
      ((fun b ↦ Bool.recOn b right left) b) =
    b

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

Tactic:
by

Goal state after: