awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} J
K : Functor.{v_3, v_1, u_3, u_1} J C
L L' : Functor.{v_1, v_2, u_1, u_2} C D
α : L ⟶ L'
inst_3 : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst_4 : PreservesColimit K L
inst_5 : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
⊢ IsIso (X := L.obj c.pt) (α.app c.pt)
have h : L.obj c.pt = (L.mapCocone c).pt → L'.obj c.pt = (L'.mapCocone c).pt → α.app c.pt = e.hom
Tactic: convert! (inferInstance : IsIso e.hom)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} J
K : Functor.{v_3, v_1, u_3, u_1} J C
L L' : Functor.{v_1, v_2, u_1, u_2} C D
α : L ⟶ L'
inst_3 : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst_4 : PreservesColimit K L
inst_5 : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
e_3 : L.obj c.pt = (L.mapCocone c).pt
e_4 : L'.obj c.pt = (L'.mapCocone c).pt
⊢ α.app c.pt = e.hom
have apply : ∀ (j : J), (L.mapCocone c).ι.app j ≫ α.app c.pt = (L.mapCocone c).ι.app j ≫ e.hom
Tactic: apply (isColimitOfPreserves L hc).hom_ext fun j ↦ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} J
K : Functor.{v_3, v_1, u_3, u_1} J C
L L' : Functor.{v_1, v_2, u_1, u_2} C D
α : L ⟶ L'
inst_3 : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst_4 : PreservesColimit K L
inst_5 : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
e_3 : L.obj c.pt = (L.mapCocone c).pt
e_4 : L'.obj c.pt = (L'.mapCocone c).pt
j : J
⊢ (L.mapCocone c).ι.app j ≫ α.app c.pt = (L.mapCocone c).ι.app j ≫ e.hom
have simp : α.app (K.obj j) ≫ L'.map (c.ι.app j) =
  L.map (c.ι.app j) ≫ (isColimitOfPreserves L hc).map (L'.mapCocone c) (K.whiskerLeft α)
Tactic: simp only [Functor.comp_obj, Functor.mapCocone_pt, Functor.const_obj_obj, Functor.mapCocone_ι_app,
    NatTrans.naturality, IsColimit.coconePointsIsoOfNatIso_hom, asIso_hom, e]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
J : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : Category.{v_3, u_3} J
K : Functor.{v_3, v_1, u_3, u_1} J C
L L' : Functor.{v_1, v_2, u_1, u_2} C D
α : L ⟶ L'
inst_3 : IsIso (K.whiskerLeft α)
c : Cocone K
hc : IsColimit c
inst_4 : PreservesColimit K L
inst_5 : PreservesColimit K L'
e : (L.mapCocone c).pt ≅ (L'.mapCocone c).pt :=
  (isColimitOfPreserves L hc).coconePointsIsoOfNatIso (isColimitOfPreserves L' hc) (asIso (K.whiskerLeft α))
e_3 : L.obj c.pt = (L.mapCocone c).pt
e_4 : L'.obj c.pt = (L'.mapCocone c).pt
j : J
⊢ α.app (K.obj j) ≫ L'.map (c.ι.app j) =
    L.map (c.ι.app j) ≫ (isColimitOfPreserves L hc).map (L'.mapCocone c) (K.whiskerLeft α)
have refine : (K.whiskerLeft α).app j ≫ (L'.mapCocone c).ι.app j = α.app (K.obj j) ≫ L'.map (c.ι.app j)
Tactic: refine (((isColimitOfPreserves L hc).ι_map (L'.mapCocone c) (whiskerLeft K α) j).trans ?_).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K_1 : Functor.{w', v₁, w, u₁} J_1 C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cone K
t : IsLimit (F.mapCone c)
⊢ ∀ (s : Cone K) (m : s ⟶ c),
    m = (Cone.functoriality K F).preimage (t.liftConeMorphism ((Cone.functoriality K F).obj s))
have apply : ∀ (s : Cone K) (m : s ⟶ c),
  (Cone.functoriality K F).map m =
    (Cone.functoriality K F).map
      ((Cone.functoriality K F).preimage (t.liftConeMorphism ((Cone.functoriality K F).obj s)))
Tactic: apply fun s m => (Cone.functoriality K F).map_injective _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K_1 : Functor.{w', v₁, w, u₁} J_1 C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cone K
t : IsLimit (F.mapCone c)
s : Cone K
m : s ⟶ c
⊢ (Cone.functoriality K F).map m =
    (Cone.functoriality K F).map
      ((Cone.functoriality K F).preimage (t.liftConeMorphism ((Cone.functoriality K F).obj s)))
have rw : (Cone.functoriality K F).map m = t.liftConeMorphism ((Cone.functoriality K F).obj s)
Tactic: rw [Functor.map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K_1 : Functor.{w', v₁, w, u₁} J_1 C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cocone K
t : IsColimit (F.mapCocone c)
⊢ ∀ (s : Cocone K) (m : c ⟶ s),
    m = (Cocone.functoriality K F).preimage (t.descCoconeMorphism ((Cocone.functoriality K F).obj s))
have apply : ∀ (s : Cocone K) (m : c ⟶ s),
  (Cocone.functoriality K F).map m =
    (Cocone.functoriality K F).map
      ((Cocone.functoriality K F).preimage (t.descCoconeMorphism ((Cocone.functoriality K F).obj s)))
Tactic: apply fun s m => (Cocone.functoriality K F).map_injective _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
J_1 : Type w
inst_2 : Category.{w', w} J_1
K_1 : Functor.{w', v₁, w, u₁} J_1 C
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_3 : F.Full
inst_4 : F.Faithful
J : Type w'
𝒥₁ : Category.{w, w'} J
K : Functor.{w, v₁, w', u₁} J C
c : Cocone K
t : IsColimit (F.mapCocone c)
s : Cocone K
m : c ⟶ s
⊢ (Cocone.functoriality K F).map m =
    (Cocone.functoriality K F).map
      ((Cocone.functoriality K F).preimage (t.descCoconeMorphism ((Cocone.functoriality K F).obj s)))
have rw : (Cocone.functoriality K F).map m = t.descCoconeMorphism ((Cocone.functoriality K F).obj s)
Tactic: rw [Functor.map_preimage]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Bifunctor (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
c₁ : Cocone K₁
c₂ : Cocone K₂
j₁ : J₁
j₂ : J₂
k₁ : J₁
k₂ : J₂
f₁ : (j₁, j₂).1 ⟶ (k₁, k₂).1
f₂ : (j₁, j₂).2 ⟶ (k₁, k₂).2
⊢ Eq (α :=
    (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj (j₁, j₂) ⟶
      obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) (k₁, k₂))
    ((obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).map (f₁, f₂) ≫
      match (motive :=
        (x : J₁ × J₂) →
          (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj x ⟶
            obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) x)
        (k₁, k₂) with
      | (j₁, j₂) =>
        (G.map (c₁.ι.app j₁)).app (K₂.obj (j₁, j₂).2) ≫
          (G.obj (obj.{v_1, v_3, u_1, u_3} (obj (const J₁) c₁.pt) j₁)).map (c₂.ι.app j₂))
    (CategoryStruct.comp (Y := obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) (j₁, j₂))
      (match (motive :=
        (x : J₁ × J₂) →
          (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj x ⟶
            obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) x)
        (j₁, j₂) with
      | (j₁, j₂) =>
        (G.map (c₁.ι.app j₁)).app (K₂.obj (j₁, j₂).2) ≫
          (G.obj (obj.{v_1, v_3, u_1, u_3} (obj (const J₁) c₁.pt) j₁)).map (c₂.ι.app j₂))
      (map (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) (f₁, f₂)))
have dsimp : ((G.map (K₁.map f₁)).app (K₂.obj j₂) ≫ (G.obj (K₁.obj k₁)).map (K₂.map f₂)) ≫
    (G.map (c₁.ι.app k₁)).app (K₂.obj k₂) ≫ (G.obj c₁.pt).map (c₂.ι.app k₂) =
  ((G.map (c₁.ι.app j₁)).app (K₂.obj j₂) ≫ (G.obj c₁.pt).map (c₂.ι.app j₂)) ≫ 𝟙 ((G.obj c₁.pt).obj c₂.pt)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Bifunctor (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
c₁ : Cone K₁
c₂ : Cone K₂
j₁ : J₁
j₂ : J₂
k₁ : J₁
k₂ : J₂
f₁ : (j₁, j₂).1 ⟶ (k₁, k₂).1
f₂ : (j₁, j₂).2 ⟶ (k₁, k₂).2
⊢ Eq.{v_5 + 1} (α :=
    obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) (j₁, j₂) ⟶
      (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj (k₁, k₂))
    (CategoryStruct.comp (Y := obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) (k₁, k₂))
      (map (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) (f₁, f₂))
      (match (motive :=
        (x : J₁ × J₂) →
          obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) x ⟶
            (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj x)
        (k₁, k₂) with
      | (j₁, j₂) => (G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)))
    ((match (motive :=
        (x : J₁ × J₂) →
          obj (obj (const (J₁ × J₂)) ((G.obj c₁.pt).obj c₂.pt)) x ⟶
            (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).obj x)
        (j₁, j₂) with
      | (j₁, j₂) => (G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)) ≫
      (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G)).map (f₁, f₂))
have dsimp : 𝟙 ((G.obj c₁.pt).obj c₂.pt) ≫ (G.map (c₁.π.app k₁)).app c₂.pt ≫ (G.obj (K₁.obj k₁)).map (c₂.π.app k₂) =
  ((G.map (c₁.π.app j₁)).app c₂.pt ≫ (G.obj (K₁.obj j₁)).map (c₂.π.app j₂)) ≫
    (G.map (K₁.map f₁)).app (K₂.obj j₂) ≫ (G.obj (K₁.obj k₁)).map (K₂.map f₂)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Bifunctor (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
c₃ : Cocone (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G))
hc₃ : IsColimit c₃
j : J₁ × J₂
⊢ c₃.ι.app j ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).inv =
    NatTrans.app (G.map (c₁.ι.app j.1)) (K₂.obj j.2) ≫ (G.obj c₁.pt).map (c₂.ι.app j.2)
have dsimp : c₃.ι.app j ≫ ((isColimitOfPreserves₂ G hc₁ hc₂).coconePointUniqueUpToIso hc₃).inv =
  NatTrans.app (G.map (c₁.ι.app j.1)) (K₂.obj j.2) ≫ (G.obj c₁.pt).map (c₂.ι.app j.2)
Tactic: dsimp [isoObjCoconePointsOfIsColimit, Functor.mapCocone₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Bifunctor (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
c₃ : Cocone (obj uncurry (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G))
hc₃ : IsColimit c₃
j : J₁ × J₂
⊢ NatTrans.app (G.map (c₁.ι.app j.1)) (K₂.obj j.2) ≫
      (G.obj c₁.pt).map (c₂.ι.app j.2) ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).hom =
    c₃.ι.app j
have rw : NatTrans.app (G.map (c₁.ι.app j.1)) (K₂.obj j.2) ≫ (G.obj c₁.pt).map (c₂.ι.app j.2) =
  c₃.ι.app j ≫ (isoObjCoconePointsOfIsColimit G hc₁ hc₂ hc₃).inv
Tactic: rw [← Category.assoc, ← Iso.eq_comp_inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Bifunctor (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
inst_6 : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst_7 : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G) :=
  { obj := fun (j₁ : J₁) ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j' : J₁} (f : j ⟶ j') ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun (j : J₁) ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun (x : J₁) ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
⊢ ((Cocone.precompose E₀.hom).obj (coconeOfCoconeUncurry P (G.mapCocone₂ c₁ c₂))).ι.app j₁ ≫
      Iso.hom (Iso.refl ((Cocone.precompose E₀.hom).obj (coconeOfCoconeUncurry P (G.mapCocone₂ c₁ c₂))).pt) =
    ((G.flip.obj c₂.pt).mapCocone c₁).ι.app j₁
have dsimp : CategoryStruct.comp (Y := (G.obj c₁.pt).obj c₂.pt)
    (𝟙 ((G.obj (K₁.obj j₁)).obj c₂.pt) ≫
        (P j₁).desc
          { pt := (G.obj c₁.pt).obj c₂.pt,
            ι :=
              { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
                naturality := sorry } } :
      (G.obj (K₁.obj j₁)).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt)
    (𝟙 ((G.obj c₁.pt).obj c₂.pt) : (G.obj c₁.pt).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt) =
  (G.map (c₁.ι.app j₁)).app c₂.pt
Tactic: dsimp [E₀, Q₀]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Bifunctor (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
inst_6 : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst_7 : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G) :=
  { obj := fun (j₁ : J₁) ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j' : J₁} (f : j ⟶ j') ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun (j : J₁) ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun (x : J₁) ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
⊢ CategoryStruct.comp (Y := (G.obj c₁.pt).obj c₂.pt)
      (𝟙 ((G.obj (K₁.obj j₁)).obj c₂.pt) ≫
          (P j₁).desc
            { pt := (G.obj c₁.pt).obj c₂.pt,
              ι :=
                { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
                  naturality := ⋯ } } :
        (G.obj (K₁.obj j₁)).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt)
      (𝟙 ((G.obj c₁.pt).obj c₂.pt) : (G.obj c₁.pt).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt) =
    (G.map (c₁.ι.app j₁)).app c₂.pt
have simp : Eq (α := (G.obj (K₁.obj j₁)).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt)
  ((P j₁).desc
      { pt := (G.obj c₁.pt).obj c₂.pt,
        ι :=
          { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
            naturality := sorry } } :
    ((G.obj (K₁.obj j₁)).mapCocone c₂).pt ⟶
      Cocone.pt.{v_2, v_5, u_2, u_5} (J := J₂) (F := (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G).obj j₁)
        { pt := (G.obj c₁.pt).obj c₂.pt,
          ι :=
            { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
              naturality := sorry } })
  ((G.map (c₁.ι.app j₁)).app c₂.pt)
Tactic: simp only [id_comp, comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Bifunctor (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
inst_6 : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst_7 : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G) :=
  { obj := fun (j₁ : J₁) ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j' : J₁} (f : j ⟶ j') ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun (j : J₁) ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun (x : J₁) ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
refine_2 :
  Eq (α := (G.obj (K₁.obj j₁)).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt)
    ((P j₁).desc
        { pt := (G.obj c₁.pt).obj c₂.pt,
          ι :=
            { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
              naturality := ⋯ } } :
      ((G.obj (K₁.obj j₁)).mapCocone c₂).pt ⟶
        Cocone.pt.{v_2, v_5, u_2, u_5} (J := J₂) (F := (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G).obj j₁)
          { pt := (G.obj c₁.pt).obj c₂.pt,
            ι :=
              { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
                naturality := ⋯ } })
    ((G.map (c₁.ι.app j₁)).app c₂.pt)
⊢ Eq (α := (G.obj (K₁.obj j₁)).obj c₂.pt ⟶ (G.obj c₁.pt).obj c₂.pt)
    ((P j₁).desc
        { pt := (G.obj c₁.pt).obj c₂.pt,
          ι :=
            { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
              naturality := ⋯ } } :
      ((G.obj (K₁.obj j₁)).mapCocone c₂).pt ⟶
        Cocone.pt.{v_2, v_5, u_2, u_5} (J := J₂) (F := (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G).obj j₁)
          { pt := (G.obj c₁.pt).obj c₂.pt,
            ι :=
              { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k),
                naturality := ⋯ } })
    ((G.map (c₁.ι.app j₁)).app c₂.pt)
have refine_1 : Cocone ((obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G).obj j₁)
Tactic: let s : Cocone (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G |>.obj j₁) := ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Bifunctor (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
inst_6 : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst_7 : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G) :=
  { obj := fun (j₁ : J₁) ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j' : J₁} (f : j ⟶ j') ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun (j : J₁) ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun (x : J₁) ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
s : Cocone ((obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G).obj j₁) :=
  { pt := (G.obj c₁.pt).obj c₂.pt,
    ι :=
      { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k), naturality := ⋯ } }
⊢ (P j₁).desc s = (G.map (c₁.ι.app j₁)).app c₂.pt
have refine_2 : (G.map (c₁.ι.app j₁)).app c₂.pt = (P j₁).desc s
Tactic: symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Bifunctor (goal)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
inst_6 : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst_7 : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G) :=
  { obj := fun (j₁ : J₁) ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j' : J₁} (f : j ⟶ j') ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun (j : J₁) ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun (x : J₁) ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
s : Cocone ((obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G).obj j₁) :=
  { pt := (G.obj c₁.pt).obj c₂.pt,
    ι :=
      { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k), naturality := ⋯ } }
⊢ (G.map (c₁.ι.app j₁)).app c₂.pt = (P j₁).desc s
have refine_2 : ∀ (j : J₂), (Q₀.obj j₁).ι.app j ≫ (G.map (c₁.ι.app j₁)).app c₂.pt = (Q₀.obj j₁).ι.app j ≫ (P j₁).desc s
Tactic: apply (P j₁).hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Bifunctor (hypothesis)
Goal:
J₁ : Type u_1
J₂ : Type u_2
inst : Category.{v_1, u_1} J₁
inst_1 : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst_2 : Category.{v_3, u_3} C₁
inst_3 : Category.{v_4, u_4} C₂
inst_4 : Category.{v_5, u_5} C
K₁ : Functor.{v_1, v_3, u_1, u_3} J₁ C₁
K₂ : Functor.{v_2, v_4, u_2, u_4} J₂ C₂
G : C₁ ⥤ Functor.{v_4, v_5, u_4, u_5} C₂ C
inst_5 : PreservesColimit₂ K₁ K₂ G
inst_6 : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst_7 : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones (obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G) :=
  { obj := fun (j₁ : J₁) ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j' : J₁} (f : j ⟶ j') ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun (j : J₁) ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun (x : J₁) ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
s : Cocone ((obj (obj (obj (whiskeringLeft₂ C) K₁) K₂) G).obj j₁) :=
  { pt := (G.obj c₁.pt).obj c₂.pt,
    ι :=
      { app := fun (k : J₂) ↦ (G.map (c₁.ι.app j₁)).app (K₂.obj k) ≫ (G.obj c₁.pt).map (c₂.ι.app k), naturality := ⋯ } }
j₂ : J₂
⊢ (Q₀.obj j₁).ι.app j₂ ≫ (G.map (c₁.ι.app j₁)).app c₂.pt = (Q₀.obj j₁).ι.app j₂ ≫ (P j₁).desc s
have this : (Q₀.obj j₁).ι.app j₂ ≫ (P j₁).desc s = s.ι.app j₂
Tactic: haveI := (P j₁).fac s j₂