awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsLimit c'
refine_1 :
  (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) →
    t.pt ⟶
      Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
        (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)
refine_2 :
  ∀ (s : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) (j : ι × ι'),
    CategoryStruct.comp (Y :=
        Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
          (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2))
        ((fun (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
            (lift hc' fun (i : ι) ↦ lift (hc i) fun (j : ι') ↦ t.proj (i, j) : t.pt ⟶ c'.pt))
          s)
        (proj (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2) j) =
      s.proj j
refine_3 :
  ∀ (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2)
    (m :
      t.pt ⟶
        Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
          (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2))
    (hm : ∀ (j : ι × ι'), m ≫ proj (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2) j = t.proj j),
    m =
      (fun (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
          (lift hc' fun (i : ι) ↦ lift (hc i) fun (j : ι') ↦ t.proj (i, j) : t.pt ⟶ c'.pt))
        t
⊢ IsLimit (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
    (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)

Tactic:
refine Fan.IsLimit.mk _ (fun t ↦ ?_) ?_ fun t m hm ↦ ?_

Premises used: CategoryTheory.Limits.Fan.IsLimit.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsLimit c'
t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2
⊢ t.pt ⟶
    Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)

Tactic:
exact Fan.IsLimit.lift hc' fun i ↦ Fan.IsLimit.lift (hc i) fun j ↦ t.proj (i, j)

Premises used: CategoryTheory.Limits.Fan.proj, Prod.mk, CategoryTheory.Limits.Fan.IsLimit.lift
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsLimit c'
⊢ ∀ (s : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) (j : ι × ι'),
    CategoryStruct.comp (Y :=
        Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
          (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2))
        ((fun (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
            (lift hc' fun (i : ι) ↦ lift (hc i) fun (j : ι') ↦ t.proj (i, j) : t.pt ⟶ c'.pt))
          s)
        (proj (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2) j) =
      s.proj j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsLimit c'
t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2
m :
  t.pt ⟶
    Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)
hm : ∀ (j : ι × ι'), m ≫ proj (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2) j = t.proj j
⊢ m =
    (fun (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
        (lift hc' fun (i : ι) ↦ lift (hc i) fun (j : ι') ↦ t.proj (i, j) : t.pt ⟶ c'.pt))
      t

Tactic:
Fan.IsLimit.hom_ext hc' _ _ fun i ↦ ?_

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.Fan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsLimit c'
t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2
m :
  t.pt ⟶
    Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)
hm : ∀ (j : ι × ι'), m ≫ proj (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2) j = t.proj j
refine_3 :
  ∀ (i : ι),
    m ≫ c'.proj i =
      (fun (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
            (lift hc' fun (i : ι) ↦ lift (hc i) fun (j : ι') ↦ t.proj (i, j) : t.pt ⟶ c'.pt))
          t ≫
        c'.proj i
⊢ m =
    (fun (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
        (lift hc' fun (i : ι) ↦ lift (hc i) fun (j : ι') ↦ t.proj (i, j) : t.pt ⟶ c'.pt))
      t

Tactic:
refine Fan.IsLimit.hom_ext hc' _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Fan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsLimit c'
t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2
m :
  t.pt ⟶
    Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)
hm : ∀ (j : ι × ι'), m ≫ proj (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2) j = t.proj j
i : ι
j : ι'
⊢ (m ≫ c'.proj i) ≫ (c i).proj j =
    ((fun (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
            (lift hc' fun (i : ι) ↦ lift (hc i) fun (j : ι') ↦ t.proj (i, j) : t.pt ⟶ c'.pt))
          t ≫
        c'.proj i) ≫
      (c i).proj j

Tactic:
simpa using hm (i, j)

Premises used: Prod.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsLimit c'
t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2
m :
  t.pt ⟶
    Cone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2)
hm : ∀ (j : ι × ι'), m ≫ proj (Fan.mk c'.pt fun (p : ι × ι') ↦ c'.proj p.1 ≫ proj (c p.1) p.2) j = t.proj j
i : ι
⊢ m ≫ c'.proj i =
    (fun (t : Fan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
          (lift hc' fun (i : ι) ↦ lift (hc i) fun (j : ι') ↦ t.proj (i, j) : t.pt ⟶ c'.pt))
        t ≫
      c'.proj i

Tactic:
exact Fan.IsLimit.hom_ext (hc i) _ _ fun j ↦ (by simpa using hm (i, j))

Premises used: CategoryTheory.Limits.Fan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsColimit c'
refine_1 :
  (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) →
    Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
        (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) ⟶
      t.pt
refine_2 :
  ∀ (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) (j : ι × ι'),
    CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
          (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1))
        (inj (f := fun (p : ι × ι') ↦ X p.1 p.2) (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) j)
        ((fun (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
            (desc hc' fun (i : ι) ↦ desc (hc i) fun (j : ι') ↦ t.inj (i, j) : c'.pt ⟶ t.pt))
          t) =
      t.inj j
refine_3 :
  ∀ (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2)
    (m :
      Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
          (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) ⟶
        t.pt)
    (hm :
      ∀ (j : ι × ι'),
        inj (f := fun (p : ι × ι') ↦ X p.1 p.2) (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) j ≫ m =
          t.inj j),
    m =
      (fun (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
          (desc hc' fun (i : ι) ↦ desc (hc i) fun (j : ι') ↦ t.inj (i, j) : c'.pt ⟶ t.pt))
        t
⊢ IsColimit (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
    (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1)

Tactic:
refine Cofan.IsColimit.mk _ (fun t ↦ ?_) ?_ fun t m hm ↦ ?_

Premises used: CategoryTheory.Limits.Cofan.IsColimit.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsColimit c'
t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2
⊢ Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) ⟶
    t.pt

Tactic:
exact Cofan.IsColimit.desc hc' fun i ↦ Cofan.IsColimit.desc (hc i) fun j ↦ t.inj (i, j)

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, Prod.mk, CategoryTheory.Limits.Cofan.inj
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsColimit c'
⊢ ∀ (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) (j : ι × ι'),
    CategoryStruct.comp (Y :=
        Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
          (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1))
        (inj (f := fun (p : ι × ι') ↦ X p.1 p.2) (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) j)
        ((fun (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
            (desc hc' fun (i : ι) ↦ desc (hc i) fun (j : ι') ↦ t.inj (i, j) : c'.pt ⟶ t.pt))
          t) =
      t.inj j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsColimit c'
t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2
m :
  Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) ⟶
    t.pt
hm :
  ∀ (j : ι × ι'),
    inj (f := fun (p : ι × ι') ↦ X p.1 p.2) (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) j ≫ m =
      t.inj j
⊢ m =
    (fun (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
        (desc hc' fun (i : ι) ↦ desc (hc i) fun (j : ι') ↦ t.inj (i, j) : c'.pt ⟶ t.pt))
      t

Tactic:
Cofan.IsColimit.hom_ext hc' _ _ fun i ↦ ?_

Premises used: CategoryTheory.Discrete.functor, CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsColimit c'
t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2
m :
  Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) ⟶
    t.pt
hm :
  ∀ (j : ι × ι'),
    inj (f := fun (p : ι × ι') ↦ X p.1 p.2) (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) j ≫ m =
      t.inj j
refine_3 :
  ∀ (i : ι),
    c'.inj i ≫ m =
      c'.inj i ≫
        (fun (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
            (desc hc' fun (i : ι) ↦ desc (hc i) fun (j : ι') ↦ t.inj (i, j) : c'.pt ⟶ t.pt))
          t
⊢ m =
    (fun (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
        (desc hc' fun (i : ι) ↦ desc (hc i) fun (j : ι') ↦ t.inj (i, j) : c'.pt ⟶ t.pt))
      t

Tactic:
refine Cofan.IsColimit.hom_ext hc' _ _ fun i ↦ ?_

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsColimit c'
t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2
m :
  Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) ⟶
    t.pt
hm :
  ∀ (j : ι × ι'),
    inj (f := fun (p : ι × ι') ↦ X p.1 p.2) (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) j ≫ m =
      t.inj j
i : ι
j : ι'
⊢ (c i).inj j ≫ c'.inj i ≫ m =
    (c i).inj j ≫
      c'.inj i ≫
        (fun (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
            (desc hc' fun (i : ι) ↦ desc (hc i) fun (j : ι') ↦ t.inj (i, j) : c'.pt ⟶ t.pt))
          t

Tactic:
simpa using hm (i, j)

Premises used: Prod.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
β : 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.{u_2, v, u} (C := C) fun (j : ι') ↦ X i j
hc : (i : ι) → IsColimit (c i)
c' : Cofan.{u_1, v, u} (C := C) fun (i : ι) ↦ (c i).pt
hc' : IsColimit c'
t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2
m :
  Cocone.pt (J := Discrete (ι × ι')) (F := Discrete.functor fun (p : ι × ι') ↦ X p.1 p.2)
      (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) ⟶
    t.pt
hm :
  ∀ (j : ι × ι'),
    inj (f := fun (p : ι × ι') ↦ X p.1 p.2) (Cofan.mk c'.pt fun (p : ι × ι') ↦ inj (c p.1) p.2 ≫ c'.inj p.1) j ≫ m =
      t.inj j
i : ι
⊢ c'.inj i ≫ m =
    c'.inj i ≫
      (fun (t : Cofan (C := C) fun (p : ι × ι') ↦ X p.1 p.2) ↦
          (desc hc' fun (i : ι) ↦ desc (hc i) fun (j : ι') ↦ t.inj (i, j) : c'.pt ⟶ t.pt))
        t

Tactic:
exact Cofan.IsColimit.hom_ext (hc i) _ _ fun j ↦ (by simpa using hm (i, j))

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Products
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproductsOfShape.{w₂, u, v} α C
⊢ Eq (α := (α → C) ⥤ C) (Equivalence.functor (piEquivalenceFunctorDiscrete α C) ⋙ colim) (Sigma.functor α)

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Discrete.functor, CategoryTheory.Limits.colimit, CategoryTheory.Discrete.natTrans, CategoryTheory.Limits.Sigma.functor, CategoryTheory.Limits.colimMap, CategoryTheory.Limits.Sigma.map, CategoryTheory.Limits.IsColimit.map, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
apply :
  IsLimit (F := cospan (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄)
    ((PullbackCone.mk («W» := Z₂) (pullback.fst f₃ f₄) (pullback.snd f₃ f₄) ⋯).pasteHoriz (i₂ :=
      (PullbackCone.mk («W» := Z₂) (pullback.fst f₃ f₄) (pullback.snd f₃ f₄) ⋯).fst)
      (PullbackCone.mk («W» := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄)
        (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄)
        (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
          (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
        ⋯)
      ⋯)
⊢ IsLimit (F := cospan (X := Z₁) (Y := Z₂) (pullback.snd f₁ f₂) (pullback.fst f₃ f₄))
    (PullbackCone.mk («W» := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄)
      (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      ⋯)

Tactic:
apply leftSquareIsPullback _ rfl (pullbackIsPullback f₃ f₄)

Premises used: CategoryTheory.Limits.leftSquareIsPullback, CategoryTheory.Limits.pullbackIsPullback, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
⊢ IsLimit (F := cospan (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄)
    ((PullbackCone.mk («W» := Z₂) (pullback.fst f₃ f₄) (pullback.snd f₃ f₄) ⋯).pasteHoriz (i₂ :=
      (PullbackCone.mk («W» := Z₂) (pullback.fst f₃ f₄) (pullback.snd f₃ f₄) ⋯).fst)
      (PullbackCone.mk («W» := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄)
        (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄)
        (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
          (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
        ⋯)
      ⋯)

Tactic:
simpa [PullbackCone.pasteHoriz] using PullbackCone.mkSelfIsLimit (pullbackIsPullback _ f₄)

Premises used: CategoryTheory.Limits.pullbackIsPullback, CategoryTheory.Limits.PullbackCone.mkSelfIsLimit, CategoryTheory.Limits.PullbackCone.pasteHoriz
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
rw :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂) ≫ f₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) ≫ f₂)
rw₁ :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂ ≫ f₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂) ≫ f₂)
rw₂ :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂ ≫ f₁)
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂ ≫ f₂)
rw₃ rw₄ :
  Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂ ≫ f₂)
    (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂ ≫ f₂)
⊢ Eq (α := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄ ⟶ Y₁)
    ((pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂) ≫ f₁)
    (CategoryStruct.comp (Y := Z₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      (pullback.fst f₃ f₄ ≫ f₂))

Tactic:
rw [pullback.lift_fst_assoc, Category.assoc, Category.assoc, pullback.condition]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.pullback.lift_fst_assoc, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
⊢ IsLimit (F := cospan (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂))
    (PullbackCone.mk («W» := pullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄)
      (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.fst f₁ f₂)
      (pullback.lift (pullback.fst (pullback.snd f₁ f₂ ≫ f₃) f₄ ≫ pullback.snd f₁ f₂)
        (pullback.snd (pullback.snd f₁ f₂ ≫ f₃) f₄) ⋯)
      ⋯)

Tactic:
simpa using pasteVertIsPullback rfl (pullbackIsPullback _ _)
    (pullbackPullbackLeftIsPullback f₁ f₂ f₃ f₄)

Premises used: CategoryTheory.Limits.pullbackPullbackLeftIsPullback, CategoryTheory.Limits.pullbackIsPullback, CategoryTheory.Limits.pasteVertIsPullback, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (X := Z₁) (pullback.snd f₁ f₂ ≫ f₃) f₄
⊢ HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)

Tactic:
⟨⟨⟨_, pullbackAssocIsPullback f₁ f₂ f₃ f₄⟩⟩⟩

Premises used: Nonempty.intro, CategoryTheory.Limits.pullbackAssocIsPullback, CategoryTheory.Limits.HasLimit.mk', CategoryTheory.Limits.LimitCone.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
Goal:
C : Type u
inst : Category.{v, u} C
X₁ X₂ X₃ Y₁ Y₂ : C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₁
f₃ : X₂ ⟶ Y₂
f₄ : X₃ ⟶ Y₂
inst_1 : HasPullback f₁ f₂
inst_2 : HasPullback f₃ f₄
inst_3 : HasPullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂)
apply :
  IsLimit (F := cospan (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂))
    ((PullbackCone.mk («W» := Z₁) (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ⋯).pasteVert (i₂ :=
      (PullbackCone.mk («W» := Z₁) (pullback.fst f₁ f₂) (pullback.snd f₁ f₂) ⋯).snd)
      (PullbackCone.mk («W» := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
          (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)) ⋯)
      ⋯)
⊢ IsLimit (F := cospan (X := Z₁) (Y := Z₂) (pullback.snd f₁ f₂) (pullback.fst f₃ f₄))
    (PullbackCone.mk («W» := pullback (Y := Z₂) f₁ (pullback.fst f₃ f₄ ≫ f₂))
      (pullback.lift (pullback.fst f₁ (pullback.fst f₃ f₄ ≫ f₂))
        (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂) ≫ pullback.fst f₃ f₄) ⋯)
      (pullback.snd f₁ (pullback.fst f₃ f₄ ≫ f₂)) ⋯)

Tactic:
apply topSquareIsPullback _ rfl (pullbackIsPullback f₁ f₂)

Premises used: CategoryTheory.Limits.topSquareIsPullback, CategoryTheory.Limits.pullbackIsPullback, rfl