awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
U : FormalCoproduct.{w, u} C
T : C
hT : IsTerminal.{v, u} T
n : SimplexCategoryᵒᵖ
i :
  ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC := fun (X : SimplexCategory) ↦
    Fin (X.len + 1)) (Opposite.unop n)
⊢ Eq (α := (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.obj n ⟶ U)
    (CategoryStruct.comp (Y := Functor.obj U.cech n) (Iso.inv (U.cechIsoCechNerveApp hT n)) (U.powerπ i) :
      (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.obj n ⟶ U)
    (WidePullback.π
        (fun
            (x :
              ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
          (isTerminalIncl T hT).from U)
        i :
      (widePullback (Functor.obj (incl C) T)
          (fun
              (x :
                ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                  fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
            U)
          fun
            (x :
              ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
          (isTerminalIncl T hT).from U) ⟶
        U)
have rw : Eq (α := (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.obj n ⟶ U)
  (CategoryStruct.comp (Y := Functor.obj U.cech n) (Iso.inv (U.cechIsoCechNerveApp hT n))
      (Iso.hom (U.cechIsoCechNerveApp hT n) ≫
        WidePullback.π
          (fun
              (x :
                ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                  fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
            (isTerminalIncl T hT).from U)
          i) :
    (Arrow.mk ((isTerminalIncl T hT).from U)).cechNerve.obj n ⟶ U)
  (WidePullback.π
      (fun
          (x :
            ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
        (isTerminalIncl T hT).from U)
      i :
    (widePullback (Functor.obj (incl C) T)
        (fun
            (x :
              ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
          U)
        fun
          (x :
            ToType (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (Opposite.unop n)) ↦
        (isTerminalIncl T hT).from U) ⟶
      U)
Tactic: rw [← U.cechIsoCechNerveApp_hom_π hT, Iso.inv_hom_id_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.FormalCoproducts.ExtraDegeneracy (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasFiniteProducts.{v, u} C
U : FormalCoproduct.{w, u} C
T : C
hT : IsTerminal.{v, u} T
⊢ Functor.map (𝟭 (SimplicialObject (FormalCoproduct.{w, u} C))) (Iso.hom (U.cechIsoCechNerve hT)) ≫
      (Arrow.mk ((isTerminalIncl T hT).from U)).augmentedCechNerve.hom =
    (SimplicialObject.augmentOfIsTerminal U.cech (isTerminalIncl T hT)).hom ≫
      Functor.map (SimplicialObject.const (FormalCoproduct.{w, u} C))
        (Iso.hom (Iso.refl (SimplicialObject.augmentOfIsTerminal U.cech (isTerminalIncl T hT)).right))
have h : ∀ (n : SimplexCategoryᵒᵖ),
  NatTrans.app
      (Functor.map (𝟭 (SimplicialObject (FormalCoproduct.{w, u} C))) (Iso.hom (U.cechIsoCechNerve hT)) ≫
        (Arrow.mk ((isTerminalIncl T hT).from U)).augmentedCechNerve.hom)
      n =
    ((SimplicialObject.augmentOfIsTerminal U.cech (isTerminalIncl T hT)).hom ≫
          Functor.map (SimplicialObject.const (FormalCoproduct.{w, u} C))
            (Iso.hom (Iso.refl (SimplicialObject.augmentOfIsTerminal U.cech (isTerminalIncl T hT)).right))).app
      n
Tactic: ext : 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)
j : J
k k' : K
f : k ⟶ k'
⊢ Eq (α := (F.obj j).obj k ⟶ obj.{v_2, v_3, u_2, u_3} (obj (const K) c.pt) k') ((F.obj j).map f ≫ c.ι.app (j, k'))
    (c.ι.app (j, k) ≫ Functor.map (obj (const K) c.pt) f)
have dsimp : Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.obj j).map f ≫ c.ι.app (j, k')) (c.ι.app (j, k) ≫ 𝟙 c.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)
j : J
k k' : K
f : k ⟶ k'
⊢ Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.obj j).map f ≫ c.ι.app (j, k')) (c.ι.app (j, k) ≫ 𝟙 c.pt)
have simp : Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.obj j).map f ≫ c.ι.app (j, k')) (c.ι.app (j, k))
Tactic: simp only [Category.comp_id]
-- 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)
j : J
k k' : K
f : k ⟶ k'
| (F.obj j).map f ≫ c.ι.app (j, k')
have arg : (F.obj j).map f
Tactic: arg 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)
j : J
k k' : K
f : k ⟶ k'
| (F.obj j).map f ≫ c.ι.app (j, k')
have arg : (F.obj j).map f
Tactic: arg 1; equals (F.map (𝟙 _)).app _ ≫ (F.obj j).map f =>
                      simp
-- 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)
j : J
k k' : K
f : k ⟶ k'
⊢ Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.obj j).map f ≫ c.ι.app (j, k')) (c.ι.app (j, k))
have conv_lhs : Eq (α := (F.obj j).obj k ⟶ c.pt) (((F.map (𝟙 j)).app k ≫ (F.obj j).map f) ≫ c.ι.app (j, k')) (c.ι.app (j, k))
Tactic: conv_lhs =>
                    arg 1; equals (F.map (𝟙 _)).app _ ≫ (F.obj j).map f =>
                      simp
-- 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)
j : J
k k' : K
f : k ⟶ k'
| ((F.map (𝟙 j)).app k ≫ (F.obj j).map f) ≫ c.ι.app (j, k')
have arg : (F.map (𝟙 j)).app k ≫ (F.obj j).map f
Tactic: arg 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)
j : J
k k' : K
f : k ⟶ k'
| (F.map (𝟙 j)).app k ≫ (F.obj j).map f
have rw : (obj uncurry F).map (𝟙 j ×ₘ f)
Tactic: rw [← uncurry_obj_map F (𝟙 j ×ₘ 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)
j : J
k k' : K
f : k ⟶ k'
| ((F.map (𝟙 j)).app k ≫ (F.obj j).map f) ≫ c.ι.app (j, k')
have arg : (obj uncurry F).map (𝟙 j ×ₘ f)
Tactic: arg 1; rw [← uncurry_obj_map F (𝟙 j ×ₘ 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)
j : J
k k' : K
f : k ⟶ k'
⊢ Eq (α := (F.obj j).obj k ⟶ c.pt) (((F.map (𝟙 j)).app k ≫ (F.obj j).map f) ≫ c.ι.app (j, k')) (c.ι.app (j, k))
have conv_lhs : (obj uncurry F).map (𝟙 j ×ₘ f) ≫ c.ι.app (j, k') = c.ι.app (j, k)
Tactic: conv_lhs => arg 1; rw [← uncurry_obj_map F (𝟙 j ×ₘ 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)
j : J
k k' : K
f : k ⟶ k'
⊢ (obj uncurry F).map (𝟙 j ×ₘ f) ≫ c.ι.app (j, k') = c.ι.app (j, k)
have rw : Eq (α := (F.obj j).obj k ⟶ c.pt) (c.ι.app (j, k) : (obj uncurry F).obj (j, k) ⟶ obj (obj (const (J × K)) c.pt) (j, k))
  (c.ι.app (j, k))
Tactic: rw [c.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)
j j' : J
f : j ⟶ j'
⊢ ∀ (j_1 : K),
    Eq (α := (F.obj j).obj j_1 ⟶ obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) j')
      ((D.obj j).ι.app j_1 ≫
          D.coconePoints.map f ≫
            (Q j').desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j', k), naturality := ⋯ } } :
        (F.obj j).obj j_1 ⟶ obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) j')
      ((D.obj j).ι.app j_1 ≫
          CategoryStruct.comp (Y := obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) j)
            ((Q j).desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := ⋯ } } :
              (D.obj j).pt ⟶
                Cocone.pt.{v_2, v_3, u_2, u_3} (J := K) (F := F.obj j)
                  { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := ⋯ } })
            (Functor.map (obj (const J) c.pt) f) :
        (F.obj j).obj j_1 ⟶ obj.{v_1, v_3, u_1, u_3} (obj (const J) c.pt) j')
have dsimp : ∀ (j_1 : K),
  Eq (α := (F.obj j).obj j_1 ⟶ c.pt)
    ((D.obj j).ι.app j_1 ≫
        (D.map f).hom ≫ (Q j').desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j', k), naturality := sorry } } :
      (F.obj j).obj j_1 ⟶ c.pt)
    ((D.obj j).ι.app j_1 ≫
        CategoryStruct.comp (Y := c.pt)
          ((Q j).desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := sorry } } :
            (D.obj j).pt ⟶
              Cocone.pt.{v_2, v_3, u_2, u_3} (J := K) (F := F.obj j)
                { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := sorry } })
          (𝟙 c.pt) :
      (F.obj j).obj j_1 ⟶ c.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)
j j' : J
f : j ⟶ j'
k : K
⊢ Eq (α := (F.obj j).obj k ⟶ c.pt)
    ((D.obj j).ι.app k ≫
        (D.map f).hom ≫ (Q j').desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j', k), naturality := ⋯ } } :
      (F.obj j).obj k ⟶ c.pt)
    ((D.obj j).ι.app k ≫
        CategoryStruct.comp (Y := c.pt)
          ((Q j).desc { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := ⋯ } } :
            (D.obj j).pt ⟶
              Cocone.pt.{v_2, v_3, u_2, u_3} (J := K) (F := F.obj j)
                { pt := c.pt, ι := { app := fun (k : K) ↦ c.ι.app (j, k), naturality := ⋯ } })
          (𝟙 c.pt) :
      (F.obj j).obj k ⟶ c.pt)
have simp : Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.map f).app k ≫ c.ι.app (j', k)) (c.ι.app (j, k))
Tactic: simp only [Limits.CoconeMorphism.w_assoc, Limits.Cocone.precompose_obj_ι,
              Limits.IsColimit.fac, NatTrans.comp_app, Category.comp_id,
              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)
j j' : J
f : j ⟶ j'
k : K
⊢ Eq (α := (F.obj j).obj k ⟶ c.pt) ((F.map f).app k ≫ c.ι.app (j', k)) (c.ι.app (j, k))
have this : Eq (α := (obj uncurry F).obj (j, k) ⟶ obj (obj (const (J × K)) c.pt) (j', k))
  ((obj uncurry F).map (f, 𝟙 k) ≫ c.ι.app (j', k)) (c.ι.app (j, k) ≫ Functor.map (obj (const (J × K)) c.pt) (f, 𝟙 k))
Tactic: have := @NatTrans.naturality _ _ _ _ _ _ c.ι (j, k) (j', k) (f, 𝟙 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 : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (obj uncurry F)
P : IsLimit c
s : Cone D.conePoints
p p' : J × K
f : p ⟶ p'
⊢ Functor.map (obj (const (J × K)) s.pt) f ≫ s.π.app p'.1 ≫ NatTrans.app (Cone.π (D.obj p'.1)) p'.2 =
    (s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2) ≫ (obj uncurry F).map f
have dsimp : 𝟙 s.pt ≫ s.π.app p'.1 ≫ NatTrans.app (Cone.π (D.obj p'.1)) p'.2 =
  (s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2) ≫ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2
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
p p' : J × K
f : p ⟶ p'
⊢ 𝟙 s.pt ≫ s.π.app p'.1 ≫ NatTrans.app (Cone.π (D.obj p'.1)) p'.2 =
    (s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2) ≫ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2
have simp : s.π.app p'.1 ≫ NatTrans.app (Cone.π (D.obj p'.1)) p'.2 =
  s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2 ≫ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2
Tactic: simp only [Category.id_comp, 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 : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (obj uncurry F)
P : IsLimit c
s : Cone D.conePoints
p p' : J × K
f : p ⟶ p'
⊢ s.π.app p'.1 ≫ NatTrans.app (Cone.π (D.obj p'.1)) p'.2 =
    s.π.app p.1 ≫ NatTrans.app (Cone.π (D.obj p.1)) p.2 ≫ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2
have rcases : ∀ (j : J) (k : K) (f : (j, k) ⟶ p'),
  s.π.app p'.1 ≫ NatTrans.app (Cone.π (D.obj p'.1)) p'.2 =
    s.π.app (j, k).1 ≫ NatTrans.app (Cone.π (D.obj (j, k).1)) (j, k).2 ≫ (F.map f.1).app (j, k).2 ≫ (F.obj p'.1).map f.2
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 : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (obj uncurry F)
P : IsLimit c
s : Cone D.conePoints
p' : J × K
j : J
k : K
f : (j, k) ⟶ p'
⊢ s.π.app p'.1 ≫ NatTrans.app (Cone.π (D.obj p'.1)) p'.2 =
    s.π.app (j, k).1 ≫ NatTrans.app (Cone.π (D.obj (j, k).1)) (j, k).2 ≫ (F.map f.1).app (j, k).2 ≫ (F.obj p'.1).map f.2
have rcases : ∀ (j' : J) (k' : K) (f : (j, k) ⟶ (j', k')),
  s.π.app (j', k').1 ≫ NatTrans.app (Cone.π (D.obj (j', k').1)) (j', k').2 =
    s.π.app (j, k).1 ≫
      NatTrans.app (Cone.π (D.obj (j, k).1)) (j, k).2 ≫ (F.map f.1).app (j, k).2 ≫ (F.obj (j', k').1).map f.2
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 : 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
f : (j, k) ⟶ (j', k')
⊢ s.π.app (j', k').1 ≫ NatTrans.app (Cone.π (D.obj (j', k').1)) (j', k').2 =
    s.π.app (j, k).1 ≫
      NatTrans.app (Cone.π (D.obj (j, k).1)) (j, k).2 ≫ (F.map f.1).app (j, k).2 ≫ (F.obj (j', k').1).map f.2
have rcases : ∀ (fj : (j, k).1 ⟶ (j', k').1) (fk : (j, k).2 ⟶ (j', k').2),
  s.π.app (j', k').1 ≫ NatTrans.app (Cone.π (D.obj (j', k').1)) (j', k').2 =
    s.π.app (j, k).1 ≫
      NatTrans.app (Cone.π (D.obj (j, k).1)) (j, k).2 ≫
        (F.map (fj, fk).1).app (j, k).2 ≫ (F.obj (j', k').1).map (fj, fk).2
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 : 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
⊢ s.π.app (j', k').1 ≫ NatTrans.app (Cone.π (D.obj (j', k').1)) (j', k').2 =
    s.π.app (j, k).1 ≫
      NatTrans.app (Cone.π (D.obj (j, k).1)) (j, k).2 ≫
        (F.map (fj, fk).1).app (j, k).2 ≫ (F.obj (j', k').1).map (fj, fk).2
have dsimp : s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.obj j).π.app k ≫ (F.map fj).app k ≫ (F.obj j').map fk
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
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
have a : (F.obj j).map fk ≫ (F.map fj).app k'
Tactic: rw [← NatTrans.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 : 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
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.obj j).π.app k ≫ (F.map fj).app k ≫ (F.obj j').map fk
have slice_rhs : s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.obj j).π.app k ≫ (F.obj j).map fk ≫ (F.map fj).app k'
Tactic: slice_rhs 3 4 => rw [← NatTrans.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 : 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
| (D.obj j).π.app k ≫ (F.obj j).map fk
have a : Functor.map (obj (const K) (D.obj j).pt) fk ≫ (D.obj j).π.app k'
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 : 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
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.obj j).π.app k ≫ (F.obj j).map fk ≫ (F.map fj).app k'
have slice_rhs : s.π.app j' ≫ (D.obj j').π.app k' =
  s.π.app j ≫ (Functor.map (obj (const K) (D.obj j).pt) fk ≫ (D.obj j).π.app k') ≫ (F.map fj).app k'
Tactic: slice_rhs 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 : 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
⊢ s.π.app j' ≫ (D.obj j').π.app k' =
    s.π.app j ≫ (Functor.map (obj (const K) (D.obj j).pt) fk ≫ (D.obj j).π.app k') ≫ (F.map fj).app k'
have simp : s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.obj j).π.app k' ≫ (F.map fj).app k'
Tactic: simp only [Functor.const_obj_map, Category.id_comp, 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 : 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
⊢ s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.obj j).π.app k' ≫ (F.map fj).app k'
have w : (D.map fj).hom ≫ NatTrans.app (Cone.π (D.obj (j', k').1)) k' =
  ((Cone.postcompose (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 : 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.obj j).π.app k' ≫ (F.map fj).app k'
have rw : s.π.app j' ≫ (D.obj j').π.app k' = s.π.app j ≫ (D.map fj).hom ≫ (D.obj j').π.app k'
Tactic: rw [← w]