awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (hypothesis)
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 c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.map fj).hom ≫ (D.obj j').π.app k' = (D.obj j).π.app k' ≫ (F.map fj).app k'
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.map fj).hom ≫ (D.obj j').π.app k'
have n : Functor.map (obj (const J) s.pt) fj ≫ s.π.app (j', k').1 = s.π.app (j, k).1 ≫ D.conePoints.map fj
Tactic: have n := s.π.naturality fj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (hypothesis)
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 c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.map fj).hom ≫ (D.obj j').π.app k' = (D.obj j).π.app k' ≫ (F.map fj).app k'
n : 𝟙 s.pt ≫ s.π.app j' = s.π.app j ≫ (D.map fj).hom
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.map fj).hom ≫ (D.obj j').π.app k'
have n₁ : s.π.app j' = s.π.app j ≫ (D.map fj).hom
Tactic: simp only [Category.id_comp] at n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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 c
s : Cone D.conePoints
j : J
k : K
j' : J
k' : K
fj : (j, k).1 ⟶ (j', k').1
fk : (j, k).2 ⟶ (j', k').2
w : (D.map fj).hom ≫ (D.obj j').π.app k' = (D.obj j).π.app k' ≫ (F.map fj).app k'
n : s.π.app j' = s.π.app j ≫ (D.map fj).hom
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.map fj).hom ≫ (D.obj j').π.app k'
have rw : (s.π.app j ≫ (D.map fj).hom) ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.map fj).hom ≫ (D.obj j').π.app k'
Tactic: rw [n]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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 c
s : Cone D.conePoints
j : J
⊢ P.lift
        { pt := s.pt,
          π := { app := fun (p : J × K) ↦ s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2, naturality := ⋯ } } ≫
      (coneOfConeUncurry Q c).π.app j =
    s.π.app j
have apply : ∀ (j_1 : K),
  (P.lift
          { pt := s.pt,
            π := { app := fun (p : J × K) ↦ s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2, naturality := sorry } } ≫
        (coneOfConeUncurry Q c).π.app j) ≫
      (D.obj j).π.app j_1 =
    s.π.app j ≫ (D.obj j).π.app j_1
Tactic: apply (Q j).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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 c
s : Cone D.conePoints
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ (coneOfConeUncurry Q c).π.app j = s.π.app j
⊢ m =
    P.lift
      { pt := s.pt,
        π := { app := fun (p : J × K) ↦ s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2, naturality := ⋯ } }
have refine : ∀ (j : J × K),
  m ≫ c.π.app j =
    NatTrans.app
      (Cone.π
        { pt := s.pt,
          π := { app := fun (p : J × K) ↦ s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2, naturality := sorry } })
      j
Tactic: refine P.uniq
      { pt := s.pt
        π := _ } m ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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 c
s : Cone D.conePoints
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ (coneOfConeUncurry Q c).π.app j = s.π.app j
j : J
k : K
⊢ Eq (α :=
    Cone.pt (J := J × K) (F := obj uncurry F)
        { pt := s.pt,
          π :=
            { app := fun (p : J × K) ↦ s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2, naturality := ⋯ :
              NatTrans (obj (const (J × K)) s.pt) (obj uncurry F) } :
          Cone (obj uncurry F) } ⟶
      (obj uncurry F).obj (j, k))
    (m ≫ c.π.app (j, k))
    (NatTrans.app
      (Cone.π
        { pt := s.pt,
          π := { app := fun (p : J × K) ↦ s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2, naturality := ⋯ } })
      (j, k))
have dsimp : m ≫ c.π.app (j, k) = s.π.app j ≫ (D.obj j).π.app k
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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 c
s : Cone D.conePoints
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ (coneOfConeUncurry Q c).π.app j = s.π.app j
j : J
k : K
⊢ m ≫ c.π.app (j, k) = s.π.app j ≫ (D.obj j).π.app k
have rw : m ≫ c.π.app (j, k) = (m ≫ (coneOfConeUncurry Q c).π.app j) ≫ (D.obj j).π.app k
Tactic: rw [← w j]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (hypothesis)
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)
p : J × K
⊢ P.lift (S s) ≫ c.π.app p = s.π.app p
have h1 : Eq (α :=
  Cone.pt (F := F.obj p.1) (obj (Cone.postcompose (Iso.hom (E p.1))) (Cone.whisker (Prod.sectR p.1 K) s)) ⟶
    (F.obj p.1).obj p.2)
  (lift (Q p.1) (obj (Cone.postcompose (Iso.hom (E p.1))) (Cone.whisker (Prod.sectR p.1 K) s)) ≫
    NatTrans.app (Cone.π (D.obj p.1)) p.2)
  (NatTrans.app (Cone.π (obj (Cone.postcompose (Iso.hom (E p.1))) (Cone.whisker (Prod.sectR p.1 K) s))) p.2)
Tactic: have h1 := (Q p.1).fac ((Cone.postcompose (E p.1).hom).obj <|
        s.whisker (Prod.sectR p.1 K)) p.2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (hypothesis)
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)
p : J × K
h1 :
  Eq (α :=
    Cone.pt (F := F.obj p.1) (obj (Cone.postcompose (Iso.hom (E p.1))) (Cone.whisker (Prod.sectR p.1 K) s)) ⟶
      (F.obj p.1).obj p.2)
    (lift (Q p.1) (obj (Cone.postcompose (Iso.hom (E p.1))) (Cone.whisker (Prod.sectR p.1 K) s)) ≫
      NatTrans.app (Cone.π (D.obj p.1)) p.2)
    (NatTrans.app (Cone.π (obj (Cone.postcompose (Iso.hom (E p.1))) (Cone.whisker (Prod.sectR p.1 K) s))) p.2)
⊢ P.lift (S s) ≫ c.π.app p = s.π.app p
have h1₁ : Eq (α := s.pt ⟶ (F.obj p.1).obj p.2)
  (CategoryStruct.comp (Y := Cone.pt (F := F.obj p.1) (D.obj p.1))
      (lift (Q p.1)
        (obj (C := Cone (Prod.sectR p.1 K ⋙ obj uncurry F))
          (Cone.postcompose (Iso.hom (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj p.1).obj x)) sorry)))
          (Cone.whisker (Prod.sectR p.1 K) s)))
      (NatTrans.app (Cone.π (D.obj p.1)) p.2) :
    s.pt ⟶ (F.obj p.1).obj p.2)
  (s.π.app (p.1, p.2) : obj (obj (const (J × K)) s.pt) (p.1, p.2) ⟶ (obj uncurry F).obj (p.1, p.2))
Tactic: simp only [Functor.comp_obj, Prod.sectR_obj, uncurry_obj_obj,
        Cone.postcompose_obj_pt, Cone.whisker_pt, Cone.postcompose_obj_π,
        Cone.whisker_π, NatTrans.comp_app, Functor.const_obj_obj, whiskerLeft_app,
        NatIso.ofComponents_hom_app, Iso.refl_hom, Category.comp_id, E] at h1
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (hypothesis)
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)
p : J × K
h1 :
  Eq (α := s.pt ⟶ (F.obj p.1).obj p.2)
    (CategoryStruct.comp (Y := Cone.pt (F := F.obj p.1) (D.obj p.1))
        (lift (Q p.1)
          (obj (C := Cone (Prod.sectR p.1 K ⋙ obj uncurry F))
            (Cone.postcompose (Iso.hom (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj p.1).obj x)) ⋯)))
            (Cone.whisker (Prod.sectR p.1 K) s)))
        (NatTrans.app (Cone.π (D.obj p.1)) p.2) :
      s.pt ⟶ (F.obj p.1).obj p.2)
    (s.π.app (p.1, p.2) : obj (obj (const (J × K)) s.pt) (p.1, p.2) ⟶ (obj uncurry F).obj (p.1, p.2))
⊢ P.lift (S s) ≫ c.π.app p = s.π.app p
have h2 : Eq (α := (S s).pt ⟶ D.conePoints.obj p.1) (P.lift (S s) ≫ (coneOfConeUncurry Q c).π.app p.1) ((S s).π.app p.1)
Tactic: have h2 := (P.fac (S s) p.1)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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)
p : J × K
h1 :
  Eq (α := s.pt ⟶ (F.obj p.1).obj p.2)
    (CategoryStruct.comp (Y := Cone.pt (F := F.obj p.1) (D.obj p.1))
        (lift (Q p.1)
          (obj (C := Cone (Prod.sectR p.1 K ⋙ obj uncurry F))
            (Cone.postcompose (Iso.hom (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj p.1).obj x)) ⋯)))
            (Cone.whisker (Prod.sectR p.1 K) s)))
        (NatTrans.app (Cone.π (D.obj p.1)) p.2) :
      s.pt ⟶ (F.obj p.1).obj p.2)
    (s.π.app (p.1, p.2) : obj (obj (const (J × K)) s.pt) (p.1, p.2) ⟶ (obj uncurry F).obj (p.1, p.2))
h2 : Eq (α := (S s).pt ⟶ D.conePoints.obj p.1) (P.lift (S s) ≫ (coneOfConeUncurry Q c).π.app p.1) ((S s).π.app p.1)
⊢ P.lift (S s) ≫ c.π.app p = s.π.app p
have dsimp : P.lift
      { pt := s.pt,
        π :=
          {
            app := fun (j : J) ↦
              (Q j).lift
                (obj (C := Cone (Prod.sectR j K ⋙ obj uncurry F))
                  (Cone.postcompose (Iso.hom (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj j).obj x)) sorry)))
                  (Cone.whisker (Prod.sectR j K) s)),
            naturality := sorry } } ≫
    c.π.app p =
  s.π.app p
Tactic: dsimp only [Functor.comp_obj, Prod.sectR_obj, uncurry_obj_obj, NatTrans.id_app,
        Functor.const_obj_obj, DiagramOfCones.conePoints_obj, DiagramOfCones.conePoints_map,
        Functor.const_obj_map, id_eq, Cone.postcompose_obj_pt, Cone.whisker_pt,
        Cone.postcompose_obj_π, Cone.whisker_π, NatTrans.comp_app, whiskerLeft_app,
        NatIso.ofComponents_hom_app, Iso.refl_hom, Prod.sectL_obj, Prod.sectL_map, eq_mp_eq_cast,
        eq_mpr_eq_cast, coneOfConeUncurry_pt, coneOfConeUncurry_π_app, S, E] at h2 ⊢
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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'
⊢ (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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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'
⊢ ((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
have 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
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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'
⊢ (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
have 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
Tactic: rcases p with ⟨j, k⟩
Cleared hypotheses: p, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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'
⊢ (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
have 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
Tactic: rcases p' with ⟨j', k'⟩
Cleared hypotheses: p', f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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')
⊢ (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
have 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
Tactic: rcases f with ⟨fj, fk⟩
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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
⊢ (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
have 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
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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
| (F.obj j').map fk ≫ (D.obj j').ι.app k'
have a : (D.obj j').ι.app k ≫ Functor.map (obj (const K) (D.obj j').pt) fk
Tactic: rw [(D.obj j').ι.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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
⊢ (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
have 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
Tactic: slice_lhs 2 3 => rw [(D.obj j').ι.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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
⊢ (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
have 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
Tactic: simp only [Functor.const_obj_map, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (hypothesis)
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
⊢ (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
have w : 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
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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
| (F.map fj).app k ≫ (D.obj j').ι.app k
have a : (D.obj j).ι.app k ≫ (D.map fj).hom
Tactic: rw [← w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (goal)
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
⊢ (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
have 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
Tactic: slice_lhs 1 2 => rw [← w]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Fubini (hypothesis)
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.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
have n : 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