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 : 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.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.map fj).hom ≫ s.ι.app j' = s.ι.app j
Tactic: simp only [Category.comp_id] 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 : 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 ≫ s.ι.app j ≫ 𝟙 s.pt
have 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
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 : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (obj uncurry F)
P : IsColimit c
s : Cocone D.coconePoints
j : 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
have 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 := sorry } } =
    (D.obj j).ι.app j_1 ≫ s.ι.app j
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 : 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 := ⋯ } }
have 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 := 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 : 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
⊢ 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))
have dsimp : c.ι.app (j, k) ≫ m = (D.obj j).ι.app k ≫ s.ι.app j
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
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 ≫ s.ι.app j
have rw : c.ι.app (j, k) ≫ m = (D.obj j).ι.app k ≫ (coconeOfCoconeUncurry Q c).ι.app j ≫ m
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 : 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
⊢ c.ι.app p ≫ P.desc (S s) = s.ι.app p
have h1 : 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
-- 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 (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
h1 :
  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)
⊢ c.ι.app p ≫ P.desc (S s) = s.ι.app p
have h1₁ : Eq (α := (F.obj p.1).obj p.2 ⟶ s.pt)
  (CategoryStruct.comp (Y := Cocone.pt (F := F.obj p.1) (D.obj p.1)) (NatTrans.app (Cocone.ι (D.obj p.1)) p.2)
      (desc (Q p.1)
        (obj (C := Cocone (Prod.sectR p.1 K ⋙ obj uncurry F))
          (Cocone.precompose (Iso.inv (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj p.1).obj x)) sorry)))
          (Cocone.whisker (Prod.sectR p.1 K) s))) :
    (F.obj p.1).obj p.2 ⟶ s.pt)
  (s.ι.app (p.1, p.2) : (obj uncurry F).obj (p.1, p.2) ⟶ obj (obj (const (J × K)) s.pt) (p.1, p.2))
Tactic: simp only [Functor.comp_obj, Prod.sectR_obj, uncurry_obj_obj,
        Cocone.precompose_obj_pt, Cocone.whisker_pt, Functor.const_obj_obj,
        Cocone.precompose_obj_ι, Cocone.whisker_ι, NatTrans.comp_app, NatIso.ofComponents_inv_app,
        Iso.refl_inv, whiskerLeft_app, Category.id_comp, 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 : 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
h1 :
  Eq (α := (F.obj p.1).obj p.2 ⟶ s.pt)
    (CategoryStruct.comp (Y := Cocone.pt (F := F.obj p.1) (D.obj p.1)) (NatTrans.app (Cocone.ι (D.obj p.1)) p.2)
        (desc (Q p.1)
          (obj (C := Cocone (Prod.sectR p.1 K ⋙ obj uncurry F))
            (Cocone.precompose (Iso.inv (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj p.1).obj x)) ⋯)))
            (Cocone.whisker (Prod.sectR p.1 K) s))) :
      (F.obj p.1).obj p.2 ⟶ s.pt)
    (s.ι.app (p.1, p.2) : (obj uncurry F).obj (p.1, p.2) ⟶ obj (obj (const (J × K)) s.pt) (p.1, p.2))
⊢ c.ι.app p ≫ P.desc (S s) = s.ι.app p
have h2 : Eq (α := D.coconePoints.obj p.1 ⟶ (S s).pt) ((coconeOfCoconeUncurry Q c).ι.app p.1 ≫ P.desc (S s)) ((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 : 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
h1 :
  Eq (α := (F.obj p.1).obj p.2 ⟶ s.pt)
    (CategoryStruct.comp (Y := Cocone.pt (F := F.obj p.1) (D.obj p.1)) (NatTrans.app (Cocone.ι (D.obj p.1)) p.2)
        (desc (Q p.1)
          (obj (C := Cocone (Prod.sectR p.1 K ⋙ obj uncurry F))
            (Cocone.precompose (Iso.inv (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj p.1).obj x)) ⋯)))
            (Cocone.whisker (Prod.sectR p.1 K) s))) :
      (F.obj p.1).obj p.2 ⟶ s.pt)
    (s.ι.app (p.1, p.2) : (obj uncurry F).obj (p.1, p.2) ⟶ obj (obj (const (J × K)) s.pt) (p.1, p.2))
h2 :
  Eq (α := D.coconePoints.obj p.1 ⟶ (S s).pt) ((coconeOfCoconeUncurry Q c).ι.app p.1 ≫ P.desc (S s)) ((S s).ι.app p.1)
⊢ c.ι.app p ≫ P.desc (S s) = s.ι.app p
have dsimp : c.ι.app p ≫
    P.desc
      { pt := s.pt,
        ι :=
          {
            app := fun (j : J) ↦
              (Q j).desc
                (obj (C := Cocone (Prod.sectR j K ⋙ obj uncurry F))
                  (Cocone.precompose (Iso.inv (NatIso.ofComponents (fun (x : K) ↦ Iso.refl ((F.obj j).obj x)) sorry)))
                  (Cocone.whisker (Prod.sectR j K) s)),
            naturality := sorry } } =
  s.ι.app p
Tactic: dsimp only [DiagramOfCocones.coconePoints_obj, Functor.comp_obj, Prod.sectR_obj,
        uncurry_obj_obj, NatTrans.id_app, Functor.const_obj_obj, DiagramOfCocones.coconePoints_map,
        Functor.const_obj_map, id_eq, Cocone.precompose_obj_pt, Cocone.whisker_pt,
        Cocone.precompose_obj_ι, Cocone.whisker_ι, NatTrans.comp_app, NatIso.ofComponents_inv_app,
        Iso.refl_inv, whiskerLeft_app, Prod.sectL_obj, Prod.sectL_map, eq_mp_eq_cast,
        eq_mpr_eq_cast, coconeOfCoconeUncurry_pt, coconeOfCoconeUncurry_ι_app, S, E] at h2 ⊢
-- 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
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
x y : J × K
x_1 : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
⊢ Eq.{v_3 + 1} (α := obj (obj (const (J × K)) (limit (obj curry G ⋙ lim))) x ⟶ G.obj y)
    (Functor.map (obj (const (J × K)) (limit (obj curry G ⋙ lim))) (f₁, f₂) ≫
      limit.π (obj curry G ⋙ lim) y.1 ≫ NatTrans.app (Cone.π (Q.obj y.1)) y.2)
    ((limit.π (obj curry G ⋙ lim) x.1 ≫ NatTrans.app (Cone.π (Q.obj x.1)) x.2) ≫ G.map (f₁, f₂))
have this : Eq (α := Cone.pt (F := (obj curry G).obj x.1) (Q.obj x.1) ⟶ ((obj curry G).obj x.1).obj y.2)
  (NatTrans.app (Cone.π (Q.obj x.1)) x.2 ≫ ((obj curry G).obj x.1).map f₂) (NatTrans.app (Cone.π (Q.obj x.1)) y.2)
Tactic: have := (Q.obj x.1).w 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
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
x y : J × K
x_1 : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this :
  Eq (α := Cone.pt (F := (obj curry G).obj x.1) (Q.obj x.1) ⟶ ((obj curry G).obj x.1).obj y.2)
    (NatTrans.app (Cone.π (Q.obj x.1)) x.2 ≫ ((obj curry G).obj x.1).map f₂) (NatTrans.app (Cone.π (Q.obj x.1)) y.2)
⊢ Eq.{v_3 + 1} (α := obj (obj (const (J × K)) (limit (obj curry G ⋙ lim))) x ⟶ G.obj y)
    (Functor.map (obj (const (J × K)) (limit (obj curry G ⋙ lim))) (f₁, f₂) ≫
      limit.π (obj curry G ⋙ lim) y.1 ≫ NatTrans.app (Cone.π (Q.obj y.1)) y.2)
    ((limit.π (obj curry G ⋙ lim) x.1 ≫ NatTrans.app (Cone.π (Q.obj x.1)) x.2) ≫ G.map (f₁, f₂))
have dsimp : 𝟙 (limit (obj curry G ⋙ lim)) ≫ limit.π (obj curry G ⋙ lim) y.1 ≫ limit.π ((obj curry G).obj y.1) y.2 =
  (limit.π (obj curry G ⋙ lim) x.1 ≫ limit.π ((obj curry G).obj x.1) x.2) ≫ G.map (f₁, f₂)
Tactic: dsimp [Q] at this ⊢
-- 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
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
x y : J × K
x_1 : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this :
  Eq (α := limit ((obj curry G).obj x.1) ⟶ G.obj (x.1, y.2))
    (limit.π ((obj curry G).obj x.1) x.2 ≫ G.map (Prod.mkHom (𝟙 x.1) f₂)) (limit.π ((obj curry G).obj x.1) y.2)
⊢ 𝟙 (limit (obj curry G ⋙ lim)) ≫ limit.π (obj curry G ⋙ lim) y.1 ≫ limit.π ((obj curry G).obj y.1) y.2 =
    (limit.π (obj curry G ⋙ lim) x.1 ≫ limit.π ((obj curry G).obj x.1) x.2) ≫ G.map (f₁, f₂)
have rw : 𝟙 (limit (obj curry G ⋙ lim)) ≫
    (limit.π (obj curry G ⋙ lim) x.1 ≫ (obj curry G ⋙ lim).map f₁) ≫ limit.π ((obj curry G).obj y.1) y.2 =
  (limit.π (obj curry G ⋙ lim) x.1 ≫ limit.π ((obj curry G).obj x.1) x.2) ≫ G.map (f₁, f₂)
Tactic: rw [← limit.w (F := curry.obj G ⋙ lim) (f := 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
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
x y : J × K
x_1 : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
this :
  Eq (α := limit ((obj curry G).obj x.1) ⟶ G.obj (x.1, y.2))
    (limit.π ((obj curry G).obj x.1) x.2 ≫ G.map (Prod.mkHom (𝟙 x.1) f₂)) (limit.π ((obj curry G).obj x.1) y.2)
⊢ 𝟙 (limit (obj curry G ⋙ lim)) ≫
      (limit.π (obj curry G ⋙ lim) x.1 ≫ (obj curry G ⋙ lim).map f₁) ≫ limit.π ((obj curry G).obj y.1) y.2 =
    (limit.π (obj curry G ⋙ lim) x.1 ≫ limit.π ((obj curry G).obj x.1) x.2) ≫ G.map (f₁, f₂)
have dsimp : 𝟙 (limit (obj curry G ⋙ lim)) ≫
    CategoryStruct.comp (Y := limit ((obj curry G).obj y.1))
      (limit.π (obj curry G ⋙ lim) x.1 ≫ limMap ((obj curry G).map f₁)) (limit.π ((obj curry G).obj y.1) y.2) =
  (limit.π (obj curry G ⋙ lim) x.1 ≫ limit.π ((obj curry G).obj x.1) x.2) ≫ G.map (f₁, f₂)
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
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj curry G ⋙ lim)
Q : DiagramOfCones (obj curry G) := DiagramOfCones.mkOfHasLimits (obj curry G)
Q' : (j : J) → IsLimit (Q.obj j) := fun (j : J) ↦ limit.isLimit ((obj curry G).obj j)
c' : Cone G
f : c'.pt ⟶ limit (obj curry G ⋙ lim)
h : ∀ (j : J × K), f ≫ limit.π (obj curry G ⋙ lim) j.1 ≫ limit.π ((obj curry G).obj j.1) j.2 = c'.π.app j
⊢ f = limit.lift (obj curry G ⋙ lim) (coneOfConeCurry G Q' c')
have refine : ∀ (j : J) (k : K),
  (f ≫ limit.π (obj curry G ⋙ lim) j) ≫ limit.π ((obj curry G).obj j) k =
    CategoryStruct.comp (Y := limit ((obj curry G).obj j))
      (CategoryStruct.comp (Y := limit (obj curry G ⋙ lim)) (limit.lift (obj curry G ⋙ lim) (coneOfConeCurry G Q' c'))
        (limit.π (obj curry G ⋙ lim) j))
      (limit.π ((obj curry G).obj j) k)
Tactic: refine limit.hom_ext (F := curry.obj G ⋙ lim) (fun j ↦ limit.hom_ext (fun 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_1 : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj uncurry F)
inst_5 : HasLimit (F ⋙ lim)
c : Cone (obj uncurry F) := limit.cone (obj uncurry F)
P : IsLimit c := limit.isLimit (obj uncurry F)
G : DiagramOfCones F := DiagramOfCones.mkOfHasLimits F
Q : (j : J) → IsLimit (G.obj j) := fun (j : J) ↦ limit.isLimit (F.obj j)
⊢ limit (obj uncurry F) ≅ limit (F ⋙ lim)
have have : (Q' : IsLimit (coneOfConeUncurry Q c)) → limit (obj uncurry F) ≅ limit (F ⋙ lim)
Tactic: have Q' := coneOfConeUncurryIsLimit Q P
-- 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_1 : J × K ⥤ C
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj uncurry F)
inst_5 : HasLimit (F ⋙ lim)
c : Cone (obj uncurry F) := limit.cone (obj uncurry F)
P : IsLimit c := limit.isLimit (obj uncurry F)
G : DiagramOfCones F := DiagramOfCones.mkOfHasLimits F
Q : (j : J) → IsLimit (G.obj j) := fun (j : J) ↦ limit.isLimit (F.obj j)
Q' : IsLimit (coneOfConeUncurry Q c)
⊢ limit (obj uncurry F) ≅ limit (F ⋙ lim)
have have : (Q'' : IsLimit (limit.cone (F ⋙ lim))) → limit (obj uncurry F) ≅ limit (F ⋙ lim)
Tactic: have Q'' := limit.isLimit (F ⋙ lim)
-- 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
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj uncurry F)
inst_5 : HasLimit (F ⋙ lim)
j : J
k : K
⊢ Eq (α := limit (obj uncurry F) ⟶ (F.obj j).obj k)
    (CategoryStruct.comp (Y := limit (F ⋙ lim)) (Iso.hom (limitUncurryIsoLimitCompLim F))
      (limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k))
    (limit.π (obj uncurry F) (j, k))
have dsimp : Eq (α := limit (obj uncurry F) ⟶ (F.obj j).obj k)
  (CategoryStruct.comp (Y := limit (F ⋙ lim))
      (limit.lift (F ⋙ lim) (coneOfConeUncurry (fun (j : J) ↦ limit.isLimit (F.obj j)) (limit.cone (obj uncurry F))))
      (limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k) :
    limit (obj uncurry F) ⟶ (F.obj j).obj k)
  (limit.π (obj uncurry F) (j, k) : limit (obj uncurry F) ⟶ (obj uncurry F).obj (j, k))
Tactic: dsimp [limitUncurryIsoLimitCompLim, IsLimit.conePointUniqueUpToIso, IsLimit.uniqueUpToIso]
-- 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
inst_3 : HasLimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasLimit (obj uncurry F)
inst_5 : HasLimit (F ⋙ lim)
j : J
k : K
⊢ Eq (α := limit (F ⋙ lim) ⟶ (obj uncurry F).obj (j, k))
    (CategoryStruct.comp (Y := limit (obj uncurry F)) (Iso.inv (limitUncurryIsoLimitCompLim F))
      (limit.π (obj uncurry F) (j, k)))
    (limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k)
have rw : Eq (α := limit (obj uncurry F) ⟶ (obj uncurry F).obj (j, k))
  (CategoryStruct.comp (Y := limit (F ⋙ lim)) (Iso.hom (limitUncurryIsoLimitCompLim F))
    (CategoryStruct.comp (Y := limit (obj uncurry F)) (Iso.inv (limitUncurryIsoLimitCompLim F))
      (limit.π (obj uncurry F) (j, k))))
  (CategoryStruct.comp (Y := limit (F ⋙ lim)) (Iso.hom (limitUncurryIsoLimitCompLim F))
    (limit.π (F ⋙ lim) j ≫ limit.π (F.obj j) k))
Tactic: rw [← cancel_epi (limitUncurryIsoLimitCompLim F).hom]
-- 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
inst_3 : HasColimitsOfShape.{v_2, u_2, v_3, u_3} K C
inst_4 : HasColimit (obj curry G ⋙ colim)
Q : DiagramOfCocones (obj curry G) := DiagramOfCocones.mkOfHasColimits (obj curry G)
x y : J × K
x_1 : x ⟶ y
f₁ : x.1 ⟶ y.1
f₂ : x.2 ⟶ y.2
⊢ Eq (α := G.obj x ⟶ obj (obj (const (J × K)) (colimit (obj curry G ⋙ colim))) y)
    (G.map (f₁, f₂) ≫ NatTrans.app (Cocone.ι (Q.obj y.1)) y.2 ≫ colimit.ι (obj curry G ⋙ colim) y.1)
    (CategoryStruct.comp (Y := obj (obj (const (J × K)) (colimit (obj curry G ⋙ colim))) x)
      (NatTrans.app (Cocone.ι (Q.obj x.1)) x.2 ≫ colimit.ι (obj curry G ⋙ colim) x.1)
      (Functor.map (obj (const (J × K)) (colimit (obj curry G ⋙ colim))) (f₁, f₂)))
have this : Eq (α := ((obj curry G).obj y.1).obj x.2 ⟶ Cocone.pt (F := (obj curry G).obj y.1) (Q.obj y.1))
  (((obj curry G).obj y.1).map f₂ ≫ NatTrans.app (Cocone.ι (Q.obj y.1)) y.2) (NatTrans.app (Cocone.ι (Q.obj y.1)) x.2)
Tactic: have := (Q.obj y.1).w f₂