awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (obj uncurry F)
P : IsLimit (coneOfConeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ obj uncurry F ≅ F.obj j :=
  fun (j : J) ↦ NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((Prod.sectR j K ⋙ obj uncurry F).obj x)) ⋯
S : (s : Cone (obj uncurry F)) → Cone D.conePoints :=
  fun (s : Cone (obj uncurry F)) ↦
    { pt := s.pt,
      π :=
        { app := fun (j : J) ↦ (Q j).lift ((Cone.postcompose (E j).hom).obj (Cone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cone (obj uncurry F)
f : s.pt ⟶ c.pt
hf : ∀ (j : J × K), f ≫ c.π.app j = s.π.app j
j : J
k : K
⊢ (f ≫ (coneOfConeUncurry Q c).π.app j) ≫ (D.obj j).π.app k = (S s).π.app j ≫ (D.obj j).π.app k

Tactic:
simpa [S, E] using hf (j, k)

Premises used: Prod.mk
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
p p' : J × K
f : p ⟶ p'
dsimp :
  ((F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2) ≫ NatTrans.app (Cocone.ι (D.obj p'.1)) p'.2 ≫ s.ι.app p'.1 =
    (NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫ s.ι.app p.1) ≫ 𝟙 s.pt
⊢ (obj uncurry F).map f ≫ NatTrans.app (Cocone.ι (D.obj p'.1)) p'.2 ≫ s.ι.app p'.1 =
    (NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫ s.ι.app p.1) ≫ Functor.map (obj (const (J × K)) s.pt) f

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
p p' : J × K
f : p ⟶ p'
simp :
  (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2 ≫ NatTrans.app (Cocone.ι (D.obj p'.1)) p'.2 ≫ s.ι.app p'.1 =
    NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫ s.ι.app p.1 ≫ 𝟙 s.pt
⊢ ((F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2) ≫ NatTrans.app (Cocone.ι (D.obj p'.1)) p'.2 ≫ s.ι.app p'.1 =
    (NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫ s.ι.app p.1) ≫ 𝟙 s.pt

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
p p' : J × K
f : p ⟶ p'
rcases :
  ∀ (j : J) (k : K) (f : (j, k) ⟶ p'),
    (F.map f.1).app (j, k).2 ≫ (F.obj p'.1).map f.2 ≫ NatTrans.app (Cocone.ι (D.obj p'.1)) p'.2 ≫ s.ι.app p'.1 =
      NatTrans.app (Cocone.ι (D.obj (j, k).1)) (j, k).2 ≫ s.ι.app (j, k).1 ≫ 𝟙 s.pt
⊢ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2 ≫ NatTrans.app (Cocone.ι (D.obj p'.1)) p'.2 ≫ s.ι.app p'.1 =
    NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫ s.ι.app p.1 ≫ 𝟙 s.pt

Tactic:
rcases p with ⟨j, k⟩
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
p' : J × K
j : J
k : K
f : (j, k) ⟶ p'
rcases :
  ∀ (j' : J) (k' : K) (f : (j, k) ⟶ (j', k')),
    (F.map f.1).app (j, k).2 ≫
        (F.obj (j', k').1).map f.2 ≫ NatTrans.app (Cocone.ι (D.obj (j', k').1)) (j', k').2 ≫ s.ι.app (j', k').1 =
      NatTrans.app (Cocone.ι (D.obj (j, k).1)) (j, k).2 ≫ s.ι.app (j, k).1 ≫ 𝟙 s.pt
⊢ (F.map f.1).app (j, k).2 ≫ (F.obj p'.1).map f.2 ≫ NatTrans.app (Cocone.ι (D.obj p'.1)) p'.2 ≫ s.ι.app p'.1 =
    NatTrans.app (Cocone.ι (D.obj (j, k).1)) (j, k).2 ≫ s.ι.app (j, k).1 ≫ 𝟙 s.pt

Tactic:
rcases p' with ⟨j', k'⟩
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
f : (j, k) ⟶ (j', k')
rcases :
  ∀ (fj : (j, k).1 ⟶ (j', k').1) (fk : (j, k).2 ⟶ (j', k').2),
    (F.map (fj, fk).1).app (j, k).2 ≫
        (F.obj (j', k').1).map (fj, fk).2 ≫ NatTrans.app (Cocone.ι (D.obj (j', k').1)) (j', k').2 ≫ s.ι.app (j', k').1 =
      NatTrans.app (Cocone.ι (D.obj (j, k).1)) (j, k).2 ≫ s.ι.app (j, k).1 ≫ 𝟙 s.pt
⊢ (F.map f.1).app (j, k).2 ≫
      (F.obj (j', k').1).map f.2 ≫ NatTrans.app (Cocone.ι (D.obj (j', k').1)) (j', k').2 ≫ s.ι.app (j', k').1 =
    NatTrans.app (Cocone.ι (D.obj (j, k).1)) (j, k).2 ≫ s.ι.app (j, k).1 ≫ 𝟙 s.pt

Tactic:
rcases f with ⟨fj, fk⟩
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
dsimp : (F.map fj).app k ≫ (F.obj j').map fk ≫ (D.obj j').ι.app k' ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt
⊢ (F.map (fj, fk).1).app (j, k).2 ≫
      (F.obj (j', k').1).map (fj, fk).2 ≫ NatTrans.app (Cocone.ι (D.obj (j', k').1)) (j', k').2 ≫ s.ι.app (j', k').1 =
    NatTrans.app (Cocone.ι (D.obj (j, k).1)) (j, k).2 ≫ s.ι.app (j, k).1 ≫ 𝟙 s.pt

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
a : (D.obj j').ι.app k ≫ Functor.map (obj (const K) (D.obj j').pt) fk
| (F.obj j').map fk ≫ (D.obj j').ι.app k'

Tactic:
rw [(D.obj j').ι.naturality]

Premises used: CategoryTheory.Limits.DiagramOfCocones.obj, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
slice_lhs :
  (F.map fj).app k ≫ ((D.obj j').ι.app k ≫ Functor.map (obj (const K) (D.obj j').pt) fk) ≫ s.ι.app j' =
    (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt
⊢ (F.map fj).app k ≫ (F.obj j').map fk ≫ (D.obj j').ι.app k' ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt

Tactic:
slice_lhs 2 3 => rw [(D.obj j').ι.naturality]

Premises used: CategoryTheory.Limits.DiagramOfCocones.obj, CategoryTheory.Limits.Cocone.ι, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
simp : (F.map fj).app k ≫ (D.obj j').ι.app k ≫ 𝟙 (D.obj j').pt ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt
⊢ (F.map fj).app k ≫ ((D.obj j').ι.app k ≫ Functor.map (obj (const K) (D.obj j').pt) fk) ≫ s.ι.app j' =
    (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt

Tactic:
simp only [Functor.const_obj_map, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Functor.const_obj_map
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
⊢ NatTrans.app (Cocone.ι (D.obj (j, k).1)) k ≫ (D.map fj).hom =
    ((Cocone.precompose (F.map fj)).obj (D.obj (j', k').1)).ι.app k

Tactic:
have w := (D.map fj).w k
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
a : (D.obj j).ι.app k ≫ (D.map fj).hom
| (F.map fj).app k ≫ (D.obj j').ι.app k

Tactic:
rw [← w]
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
slice_lhs :
  (((D.obj j).ι.app k ≫ (D.map fj).hom) ≫ 𝟙 (D.obj j').pt) ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt
⊢ (F.map fj).app k ≫ (D.obj j').ι.app k ≫ 𝟙 (D.obj j').pt ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt

Tactic:
slice_lhs 1 2 => rw [← w]
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
⊢ D.coconePoints.map fj ≫ s.ι.app (j', k').1 = s.ι.app (j, k).1 ≫ Functor.map (obj (const J) s.pt) fj

Tactic:
have n := s.ι.naturality fj
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
n : (D.map fj).hom ≫ s.ι.app j' = s.ι.app j ≫ 𝟙 s.pt
⊢ (D.map fj).hom ≫ s.ι.app j' = s.ι.app j

Tactic:
simp only [Category.comp_id] at n

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
n : (D.map fj).hom ≫ s.ι.app j' = s.ι.app j
rw :
  (((D.obj j).ι.app k ≫ (D.map fj).hom) ≫ 𝟙 (D.obj j').pt) ≫ s.ι.app j' =
    (D.obj j).ι.app k ≫ ((D.map fj).hom ≫ s.ι.app j') ≫ 𝟙 s.pt
⊢ (((D.obj j).ι.app k ≫ (D.map fj).hom) ≫ 𝟙 (D.obj j').pt) ≫ s.ι.app j' = (D.obj j).ι.app k ≫ s.ι.app j ≫ 𝟙 s.pt

Tactic:
rw [← n]
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.obj j).ι.app k ≫ (D.map fj).hom = (F.map fj).app k ≫ (D.obj j').ι.app k
n : (D.map fj).hom ≫ s.ι.app j' = s.ι.app j
⊢ (((D.obj j).ι.app k ≫ (D.map fj).hom) ≫ 𝟙 (D.obj j').pt) ≫ s.ι.app j' =
    (D.obj j).ι.app k ≫ ((D.map fj).hom ≫ s.ι.app j') ≫ 𝟙 s.pt

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
apply :
  ∀ (j_1 : K),
    (D.obj j).ι.app j_1 ≫
        (coconeOfCoconeUncurry Q c).ι.app j ≫
          P.desc
            { pt := s.pt,
              ι :=
                { app := fun (p : J × K) ↦ NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫ s.ι.app p.1, naturality := ⋯ } } =
      (D.obj j).ι.app j_1 ≫ s.ι.app j
⊢ (coconeOfCoconeUncurry Q c).ι.app j ≫
      P.desc
        { pt := s.pt,
          ι := { app := fun (p : J × K) ↦ NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫ s.ι.app p.1, naturality := ⋯ } } =
    s.ι.app j

Tactic:
apply (Q j).hom_ext

Premises used: CategoryTheory.Limits.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : J
k : K
⊢ (D.obj j).ι.app k ≫
      (coconeOfCoconeUncurry Q c).ι.app j ≫
        P.desc
          { pt := s.pt,
            ι := { app := fun (p : J × K) ↦ NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫ s.ι.app p.1, naturality := ⋯ } } =
    (D.obj j).ι.app k ≫ s.ι.app j

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
m : (coconeOfCoconeUncurry Q c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeUncurry Q c).ι.app j ≫ m = s.ι.app j
⊢ m =
    P.desc
      { pt := s.pt,
        ι := { app := fun (p : J × K) ↦ NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫ s.ι.app p.1, naturality := ⋯ } }

Tactic:
P.uniq
      { pt := s.pt
        ι := _ } m ?_

Premises used: CategoryTheory.Limits.Cocone.mk, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Limits.DiagramOfCocones.coconePoints, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
m : (coconeOfCoconeUncurry Q c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeUncurry Q c).ι.app j ≫ m = s.ι.app j
refine :
  ∀ (j : J × K),
    c.ι.app j ≫ m =
      NatTrans.app
        (Cocone.ι
          { pt := s.pt,
            ι := { app := fun (p : J × K) ↦ NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫ s.ι.app p.1, naturality := ⋯ } })
        j
⊢ m =
    P.desc
      { pt := s.pt,
        ι := { app := fun (p : J × K) ↦ NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫ s.ι.app p.1, naturality := ⋯ } }

Tactic:
refine P.uniq
      { pt := s.pt
        ι := _ } m ?_

Premises used: CategoryTheory.Limits.Cocone.mk, CategoryTheory.Limits.IsColimit.uniq, CategoryTheory.Limits.Cocone.pt
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
m : (coconeOfCoconeUncurry Q c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeUncurry Q c).ι.app j ≫ m = s.ι.app j
j : J
k : K
dsimp : c.ι.app (j, k) ≫ m = (D.obj j).ι.app k ≫ s.ι.app j
⊢ Eq (α :=
    (obj uncurry F).obj (j, k) ⟶
      Cocone.pt (J := J × K) (F := obj uncurry F)
        { pt := s.pt,
          ι := { app := fun (p : J × K) ↦ NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫ s.ι.app p.1, naturality := ⋯ } })
    (c.ι.app (j, k) ≫ m)
    (NatTrans.app
      (Cocone.ι
        { pt := s.pt,
          ι := { app := fun (p : J × K) ↦ NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫ s.ι.app p.1, naturality := ⋯ } })
      (j, k))

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
m : (coconeOfCoconeUncurry Q c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeUncurry Q c).ι.app j ≫ m = s.ι.app j
j : J
k : K
rw : c.ι.app (j, k) ≫ m = (D.obj j).ι.app k ≫ (coconeOfCoconeUncurry Q c).ι.app j ≫ m
⊢ c.ι.app (j, k) ≫ m = (D.obj j).ι.app k ≫ s.ι.app j

Tactic:
rw [← w j]
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
m : (coconeOfCoconeUncurry Q c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeUncurry Q c).ι.app j ≫ m = s.ι.app j
j : J
k : K
⊢ c.ι.app (j, k) ≫ m = (D.obj j).ι.app k ≫ (coconeOfCoconeUncurry Q c).ι.app j ≫ m

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit (coconeOfCoconeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ obj uncurry F ≅ F.obj j :=
  fun (j : J) ↦ NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((Prod.sectR j K ⋙ obj uncurry F).obj x)) ⋯
s : Cocone (obj uncurry F)
j j' : J
f : j ⟶ j'
k : K
⊢ Eq (α := (F.obj j).obj k ⟶ obj.{v_1, v_3, u_1, u_3} (obj (const J) s.pt) j')
    ((D.obj j).ι.app k ≫
        D.coconePoints.map f ≫ (Q j').desc ((Cocone.precompose (E j').inv).obj (Cocone.whisker (Prod.sectR j' K) s)) :
      (F.obj j).obj k ⟶ obj.{v_1, v_3, u_1, u_3} (obj (const J) s.pt) j')
    ((D.obj j).ι.app k ≫
        CategoryStruct.comp (Y := obj.{v_1, v_3, u_1, u_3} (obj (const J) s.pt) j)
          ((Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)) :
            (D.obj j).pt ⟶ ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)).pt)
          (Functor.map (obj (const J) s.pt) f) :
      (F.obj j).obj k ⟶ obj.{v_1, v_3, u_1, u_3} (obj (const J) s.pt) j')

Tactic:
simpa [E] using s.ι.naturality ((Prod.sectL J k).map f)

Premises used: CategoryTheory.Functor.map, CategoryTheory.Limits.Cocone.ι, CategoryTheory.Prod.sectL, CategoryTheory.NatTrans.naturality
-- Module: Mathlib.CategoryTheory.Limits.Fubini
Goal:
J : Type u_1
K : Type u_2
inst : Category.{v_1, u_1} J
inst_1 : Category.{v_2, u_2} K
C : Type u_3
inst_2 : Category.{v_3, u_3} C
F : J ⥤ Functor.{v_2, v_3, u_2, u_3} K C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit (coconeOfCoconeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ obj uncurry F ≅ F.obj j :=
  fun (j : J) ↦ NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((Prod.sectR j K ⋙ obj uncurry F).obj x)) ⋯
S : (s : Cocone (obj uncurry F)) → Cocone D.coconePoints :=
  fun (s : Cocone (obj uncurry F)) ↦
    { pt := s.pt,
      ι :=
        { app := fun (j : J) ↦ (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cocone (obj uncurry F)
p : J × K
⊢ Eq (α :=
    (F.obj p.1).obj p.2 ⟶
      Cocone.pt (F := F.obj p.1) (obj (Cocone.precompose (Iso.inv (E p.1))) (Cocone.whisker (Prod.sectR p.1 K) s)))
    (NatTrans.app (Cocone.ι (D.obj p.1)) p.2 ≫
      desc (Q p.1) (obj (Cocone.precompose (Iso.inv (E p.1))) (Cocone.whisker (Prod.sectR p.1 K) s)))
    (NatTrans.app (Cocone.ι (obj (Cocone.precompose (Iso.inv (E p.1))) (Cocone.whisker (Prod.sectR p.1 K) s))) p.2)

Tactic:
have h1 := (Q p.1).fac ((Cocone.precompose (E p.1).inv).obj <|
        s.whisker (Prod.sectR p.1 K)) p.2