awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasColimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasCoequalizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesColimitsOfShape WalkingParallelPair G
inst_7 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := sigmaObj.{w, v, u} K.obj
Q : C := sigmaObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
s : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
      colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
t : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
⊢ IsColimit (F := parallelPair (G.map s) (G.map t)) (Cofork.ofπ (G.map i) ⋯ : Cofork (G.map s) (G.map t))
have l : IsColimit (Cofork.ofπ i sorry)
Tactic: apply isColimitCoforkMapOfIsColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : SmallCategory J
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : HasColimitsOfShape.{w, w, v, u} (Discrete J) C
inst_4 : HasColimitsOfShape.{w, w, v, u} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) C
inst_5 : HasCoequalizers.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_6 : PreservesColimitsOfShape WalkingParallelPair G
inst_7 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete J) G
inst_8 : PreservesColimitsOfShape.{w, w, v, v₂, u, u₂} (Discrete ((p : J × J) × (p.1 ⟶ p.2))) G
K : Functor.{w, v, w, u} J C
P : C := sigmaObj.{w, v, u} K.obj
Q : C := sigmaObj.{w, v, u} fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦ K.obj f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1
s : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    K.map (f.snd (β := fun (p : J × J) ↦ p.1 ⟶ p.2)) ≫
      colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).2 }
t : Q ⟶ P :=
  Sigma.desc fun (f : (p : J × J) × (p.1 ⟶ p.2)) ↦
    colimit.ι (Discrete.functor K.obj) { as := f.fst (β := fun (p : J × J) ↦ p.1 ⟶ p.2).1 }
I : C := coequalizer s t
i : P ⟶ I := coequalizer.π s t
l : IsColimit (Cofork.ofπ i ⋯)
⊢ IsColimit (F := parallelPair (G.map s) (G.map t)) (Cofork.ofπ (G.map i) ⋯ : Cofork (G.map s) (G.map t))
have w : s ≫ i = t ≫ i
Tactic: apply isColimitCoforkMapOfIsColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
⊢ PreservesFiniteColimits G
have this : HasFiniteColimits.{v, u} C
Tactic: haveI : HasFiniteColimits C := hasFiniteColimits_of_hasInitial_and_pushouts
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
this : HasFiniteColimits.{v, u} C
⊢ PreservesFiniteColimits G
have this₁ : PreservesColimitsOfShape (Discrete WalkingPair) G
Tactic: haveI : PreservesColimitsOfShape (Discrete WalkingPair) G :=
    preservesBinaryCoproducts_of_preservesInitial_and_pushouts G
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
this_1 : HasFiniteColimits.{v, u} C
this : PreservesColimitsOfShape (Discrete WalkingPair) G
⊢ PreservesFiniteColimits G
have this₁ : PreservesColimitsOfShape WalkingParallelPair G
Tactic: haveI : PreservesColimitsOfShape (WalkingParallelPair) G :=
      (preservesCoequalizers_of_preservesPushouts_and_binaryCoproducts G)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
this_1 : HasFiniteColimits.{v, u} C
this_2 : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteColimits G
have _ : PreservesFiniteCoproducts G
Tactic: refine
    @preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts _ _ _ _ _ _ G _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasInitial.{v, u} C
inst_3 : HasPushouts.{v, u} C
G : Functor.{v, v₂, u, u₂} C D
inst_4 : PreservesColimitsOfShape (Discrete PEmpty.{1}) G
inst_5 : PreservesColimitsOfShape WalkingSpan G
this_1 : HasFiniteColimits.{v, u} C
this_2 : PreservesColimitsOfShape (Discrete WalkingPair) G
this : PreservesColimitsOfShape WalkingParallelPair G
⊢ PreservesFiniteCoproducts G
have refine : ∀ (x : ℕ), PreservesColimitsOfShape (Discrete (Fin x)) G
Tactic: refine ⟨fun _ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasFiniteWidePullbacks.{v, u} C
⊢ HasFiniteLimits (Over.{v, u} B)
have this : HasFiniteProducts (Over.{v, u} B)
Tactic: have := ConstructProducts.over_finiteProducts_of_finiteWidePullbacks (B := B)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasFiniteWidePullbacks.{v, u} C
this : HasFiniteProducts (Over.{v, u} B)
⊢ HasFiniteLimits (Over.{v, u} B)
have this₁ : HasEqualizers (Over.{v, u} B)
Tactic: have := hasEqualizers_of_hasPullbacks_and_binary_products (C := Over B)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasWidePullbacks.{w, v, u} C
⊢ HasLimitsOfSize.{w, w, v, max u v} (Over.{v, u} B)
have this : HasBinaryProducts (Over.{v, u} B)
Tactic: have := ConstructProducts.over_binaryProduct_of_pullback (B := B)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasWidePullbacks.{w, v, u} C
this : HasBinaryProducts (Over.{v, u} B)
⊢ HasLimitsOfSize.{w, w, v, max u v} (Over.{v, u} B)
have this₁ : HasEqualizers (Over.{v, u} B)
Tactic: have := hasEqualizers_of_hasPullbacks_and_binary_products (C := Over B)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasWidePullbacks.{w, v, u} C
this_1 : HasBinaryProducts (Over.{v, u} B)
this : HasEqualizers (Over.{v, u} B)
⊢ HasLimitsOfSize.{w, w, v, max u v} (Over.{v, u} B)
have this₁ : HasProducts (Over.{v, u} B)
Tactic: have := ConstructProducts.over_products_of_widePullbacks (B := B)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasFiniteWidePushouts.{v, u} C
⊢ HasFiniteColimits (Under.{v, u} B)
have rw : HasFiniteLimits (Under.{v, u} B)ᵒᵖ
Tactic: rw [← hasFiniteLimits_opposite_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X B : C
inst_1 : HasWidePushouts.{w, v, u} C
⊢ HasColimitsOfSize.{w, w, v, max u v} (Under.{v, u} B)
have rw : HasLimitsOfSize.{w, w, v, max u v} (Under.{v, u} B)ᵒᵖ
Tactic: rw [← hasLimitsOfSize_opposite_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (goal)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
j : J
z : Quiver.Hom (V := Functor.{v', v_1, u', u_1} J D) (Functor.obj (Functor.const J) (K.obj c.pt))
  (Functor.obj (Functor.const J) B) :=
  Iso.inv (Functor.constComp J c.pt K) ≫ Functor.whiskerRight c.π K ≫ natTransInCostructuredArrow F
⊢ K.map (c.π.app j) ≫ (F.obj j).hom =
    (Functor.obj
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        j).hom
have h : (K.obj
        (Functor.obj
            (Functor.obj (Functor.const J)
              (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
            j).left ⟶
      B) =
    (Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) (K.obj c.pt)) j ⟶
      Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) B) j) →
  K.map (c.π.app j) ≫ (F.obj j).hom = z.app j
Tactic: convert! (nat_trans_from_is_connected z j (Classical.arbitrary J))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (goal)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
j : J
z : Quiver.Hom (V := Functor.{v', v_1, u', u_1} J D) (Functor.obj (Functor.const J) (K.obj c.pt))
  (Functor.obj (Functor.const J) B) :=
  Iso.inv (Functor.constComp J c.pt K) ≫ Functor.whiskerRight c.π K ≫ natTransInCostructuredArrow F
h :
  (K.obj
          (Functor.obj
              (Functor.obj (Functor.const J)
                (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
              j).left ⟶
        B) =
      (Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) (K.obj c.pt)) j ⟶
        Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) B) j) →
    K.map (c.π.app j) ≫ (F.obj j).hom = z.app j
⊢ K.map (c.π.app j) ≫ (F.obj j).hom =
    (Functor.obj
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        j).hom
have h₁ : (K.obj
        (Functor.obj
            (Functor.obj (Functor.const J)
              (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
            j).left ⟶
      B) =
    (Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) (K.obj c.pt)) j ⟶
      Functor.obj.{v', v_1, u', u_1} (Functor.obj (Functor.const J) B) j) →
  (Functor.obj
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        j).hom =
    z.app (Classical.arbitrary J)
Tactic: convert! (nat_trans_from_is_connected z j (Classical.arbitrary J))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (goal)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X_1 : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
X Y : J
f : X ⟶ Y
⊢ Eq (α :=
    Functor.obj
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        X ⟶
      F.obj Y)
    (Functor.map
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        f ≫
      homMk (c.π.app Y) ⋯)
    (homMk (c.π.app X) ⋯ ≫ F.map f)
have left : Eq (α :=
  (Functor.obj
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        X).left ⟶
    (F.obj Y).left)
  (CommaMorphism.left
    (Functor.map
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        f ≫
      homMk (c.π.app Y) sorry))
  (CommaMorphism.left (homMk (c.π.app X) sorry ≫ F.map f))
Tactic: apply CommaMorphism.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (goal)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X_1 : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K B
c : Cone (F ⋙ proj K B)
X Y : J
f : X ⟶ Y
left :
  Eq (α :=
    (Functor.obj
          (Functor.obj (Functor.const J)
            (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
          X).left ⟶
      (F.obj Y).left)
    (CommaMorphism.left
      (Functor.map
          (Functor.obj (Functor.const J)
            (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
          f ≫
        homMk (c.π.app Y) ⋯))
    (CommaMorphism.left (homMk (c.π.app X) ⋯ ≫ F.map f))
⊢ Eq (α :=
    Functor.obj
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        X ⟶
      F.obj Y)
    (Functor.map
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        f ≫
      homMk (c.π.app Y) ⋯)
    (homMk (c.π.app X) ⋯ ≫ F.map f)
have right : Eq (α :=
  (Functor.obj
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        X).right ⟶
    (F.obj Y).right)
  (CommaMorphism.right
    (Functor.map
        (Functor.obj (Functor.const J)
          (mk (K.map (c.π.app (Classical.arbitrary J)) ≫ (F.obj (Classical.arbitrary J)).hom)))
        f ≫
      homMk (c.π.app Y) sorry))
  (CommaMorphism.right (homMk (c.π.app X) sorry ≫ F.map f))
Tactic: apply CommaMorphism.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (goal)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K_1 : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K_1 B
c : Cone (F ⋙ proj K_1 B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ (raiseCone c).π.app j = s.π.app j
⊢ m = homMk (t.lift ((proj K_1 B).mapCone s)) ⋯
have h : m.left = CommaMorphism.left (homMk (t.lift ((proj K_1 B).mapCone s)) sorry)
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (goal)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K_1 : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
F : J ⥤ CostructuredArrow K_1 B
c : Cone (F ⋙ proj K_1 B)
t : IsLimit c
s : Cone F
m : s.pt ⟶ (raiseCone c).pt
K : ∀ (j : J), m ≫ (raiseCone c).π.app j = s.π.app j
⊢ m.left = CommaMorphism.left (homMk (t.lift ((proj K_1 B).mapCone s)) ⋯)
have h : ∀ (j : J), m.left ≫ c.π.app j = CommaMorphism.left (homMk (t.lift ((proj K_1 B).mapCone s)) sorry) ≫ c.π.app j
Tactic: apply t.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (goal)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
K_1 : J ⥤ CostructuredArrow K B
c : Cone K_1
hc : IsLimit c
x : Cone (K_1 ⋙ proj K B)
x_1 : J
⊢ (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ ((proj K B).mapCone c).π.app x_1 = x.π.app x_1
have rw : (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ (proj K B).map (c.π.app x_1) = x.π.app x_1
Tactic: rw [Functor.mapCone_π_app, ← Functor.map_comp, hc.fac,
        CreatesConnected.raiseCone_π_app, CostructuredArrow.proj_map,
        CostructuredArrow.homMk_left _ _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (goal)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
K_1 : J ⥤ CostructuredArrow K B
c : Cone K_1
hc : IsLimit c
x : Cone (K_1 ⋙ proj K B)
x_1 : J
rw : (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ (proj K B).map (c.π.app x_1) = x.π.app x_1
⊢ (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ ((proj K B).mapCone c).π.app x_1 = x.π.app x_1
have rw₁ : (proj K B).map (hc.lift (CreatesConnected.raiseCone x) ≫ c.π.app x_1) = x.π.app x_1
Tactic: rw [Functor.mapCone_π_app, ← Functor.map_comp, hc.fac,
        CreatesConnected.raiseCone_π_app, CostructuredArrow.proj_map,
        CostructuredArrow.homMk_left _ _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (goal)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
K_1 : J ⥤ CostructuredArrow K B
c : Cone K_1
hc : IsLimit c
x : Cone (K_1 ⋙ proj K B)
x_1 : J
rw : (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ (proj K B).map (c.π.app x_1) = x.π.app x_1
rw₁ : (proj K B).map (hc.lift (CreatesConnected.raiseCone x) ≫ c.π.app x_1) = x.π.app x_1
⊢ (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ ((proj K B).mapCone c).π.app x_1 = x.π.app x_1
have rw₂ : (proj K B).map ((CreatesConnected.raiseCone x).π.app x_1) = x.π.app x_1
Tactic: rw [Functor.mapCone_π_app, ← Functor.map_comp, hc.fac,
        CreatesConnected.raiseCone_π_app, CostructuredArrow.proj_map,
        CostructuredArrow.homMk_left _ _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (goal)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
K_1 : J ⥤ CostructuredArrow K B
c : Cone K_1
hc : IsLimit c
x : Cone (K_1 ⋙ proj K B)
x_1 : J
rw : (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ (proj K B).map (c.π.app x_1) = x.π.app x_1
rw₁ : (proj K B).map (hc.lift (CreatesConnected.raiseCone x) ≫ c.π.app x_1) = x.π.app x_1
rw₂ : (proj K B).map ((CreatesConnected.raiseCone x).π.app x_1) = x.π.app x_1
⊢ (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ ((proj K B).mapCone c).π.app x_1 = x.π.app x_1
have rw₃ : (proj K B).map (homMk (x.π.app x_1) sorry) = x.π.app x_1
Tactic: rw [Functor.mapCone_π_app, ← Functor.map_comp, hc.fac,
        CreatesConnected.raiseCone_π_app, CostructuredArrow.proj_map,
        CostructuredArrow.homMk_left _ _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (goal)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
K_1 : J ⥤ CostructuredArrow K B
c : Cone K_1
hc : IsLimit c
x : Cone (K_1 ⋙ proj K B)
x_1 : J
rw : (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ (proj K B).map (c.π.app x_1) = x.π.app x_1
rw₁ : (proj K B).map (hc.lift (CreatesConnected.raiseCone x) ≫ c.π.app x_1) = x.π.app x_1
rw₂ : (proj K B).map ((CreatesConnected.raiseCone x).π.app x_1) = x.π.app x_1
rw₃ : (proj K B).map (homMk (x.π.app x_1) ⋯) = x.π.app x_1
⊢ (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ ((proj K B).mapCone c).π.app x_1 = x.π.app x_1
have rw₄ : CommaMorphism.left (homMk (x.π.app x_1) sorry) = x.π.app x_1
Tactic: rw [Functor.mapCone_π_app, ← Functor.map_comp, hc.fac,
        CreatesConnected.raiseCone_π_app, CostructuredArrow.proj_map,
        CostructuredArrow.homMk_left _ _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (goal)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
K_1 : J ⥤ CostructuredArrow K B
c : Cone K_1
hc : IsLimit c
x : Cone (K_1 ⋙ proj K B)
x_1 : J
rw : (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ (proj K B).map (c.π.app x_1) = x.π.app x_1
rw₁ : (proj K B).map (hc.lift (CreatesConnected.raiseCone x) ≫ c.π.app x_1) = x.π.app x_1
rw₂ : (proj K B).map ((CreatesConnected.raiseCone x).π.app x_1) = x.π.app x_1
rw₃ : (proj K B).map (homMk (x.π.app x_1) ⋯) = x.π.app x_1
rw₄ : CommaMorphism.left (homMk (x.π.app x_1) ⋯) = x.π.app x_1
⊢ (proj K B).map (hc.lift (CreatesConnected.raiseCone x)) ≫ ((proj K B).mapCone c).π.app x_1 = x.π.app x_1
have rw₅ : x.π.app x_1 = x.π.app x_1
Tactic: rw [Functor.mapCone_π_app, ← Functor.map_comp, hc.fac,
        CreatesConnected.raiseCone_π_app, CostructuredArrow.proj_map,
        CostructuredArrow.homMk_left _ _]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (hypothesis)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u_1
inst_2 : Category.{v_1, u_1} D
K : Functor.{v, v_1, u, u_1} C D
X : C
inst_3 : IsConnected.{v', u'} J
B : D
⊢ PreservesColimitsOfShape J (proj B K)
have this : PreservesLimitsOfShape Jᵒᵖ (proj B K).op
Tactic: have : PreservesLimitsOfShape Jᵒᵖ (proj B K).op :=
    inferInstanceAs <| PreservesLimitsOfShape Jᵒᵖ <|
      (structuredArrowOpEquivalence K B).functor ⋙ CostructuredArrow.proj K.op (.op B)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (hypothesis)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u_1
inst_2 : Category.{v_1, u_1} D_1
K : Functor.{v, v_1, u, u_1} C D_1
X : C
B : D_1
inst_3 : IsConnected.{v', u'} J
inst_4 : HasLimitsOfShape.{v', u', v, u} J C
inst_5 : PreservesLimitsOfShape.{v', u', v, v_1, u, u_1} J K
D : J ⥤ CostructuredArrow K B
⊢ PreservesLimit D (CostructuredArrow.toOver K B)
have this : PreservesLimit D (CostructuredArrow.toOver K B ⋙ Over.forget B)
Tactic: have : PreservesLimit D (CostructuredArrow.toOver K B ⋙ Over.forget B) :=
      inferInstanceAs <| PreservesLimit D (CostructuredArrow.proj K B ⋙ K)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Connected (hypothesis)
Goal:
J : Type u'
inst : Category.{v', u'} J
C : Type u
inst_1 : Category.{v, u} C
D_1 : Type u_1
inst_2 : Category.{v_1, u_1} D_1
K : Functor.{v, v_1, u, u_1} C D_1
X : C
B : D_1
inst_3 : IsConnected.{v', u'} J
inst_4 : HasColimitsOfShape.{v', u', v, u} J C
inst_5 : PreservesColimitsOfShape.{v', u', v, v_1, u, u_1} J K
D : J ⥤ StructuredArrow B K
⊢ PreservesColimit D (StructuredArrow.toUnder B K)
have this : PreservesColimit D (StructuredArrow.toUnder B K ⋙ Under.forget B)
Tactic: have : PreservesColimit D (StructuredArrow.toUnder B K ⋙ Under.forget B) :=
      inferInstanceAs <| PreservesColimit D (StructuredArrow.proj B K ⋙ K)