awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
X : C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
inst_4 : IsIso (X := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (Y := limit F) (limMap c.π)
j : J
⊢ Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ F.obj j)
    (limit.π (Functor.obj (Functor.const J) c.pt) j ≫ c.π.app j)
    (Iso.hom
        (IsLimit.conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt))
          (isLimitConstCone J c.pt)) ≫
      c.π.app j)
have e_a : Eq.{v₂ + 1} (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ c.pt)
  (limit.π (Functor.obj (Functor.const J) c.pt) j)
  (Iso.hom
    (IsLimit.conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
hc : IsLimit c
this :
  Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ limit F) (limMap c.π)
    (Iso.hom
      (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
        hc.conePointUniqueUpToIso (limit.isLimit F)))
⊢ IsIso (X := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (Y := limit F) (limMap c.π)
have rw : IsIso (X := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (Y := limit F)
  (Iso.hom
    (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
      hc.conePointUniqueUpToIso (limit.isLimit F)))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
hc : IsLimit c
⊢ IsIso (X := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt)) (Y := limit F) (limMap c.π)
have suffices : Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ limit F) (limMap c.π)
  (Iso.hom
    (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
      hc.conePointUniqueUpToIso (limit.isLimit F)))
Tactic: suffices limMap c.π = ((limit.isLimit _).conePointUniqueUpToIso (isLimitConstCone J c.pt) ≪≫
      hc.conePointUniqueUpToIso (limit.isLimit _)).hom by
    rw [this]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
hc : IsLimit c
⊢ Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ limit F) (limMap c.π)
    (Iso.hom
      (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
        hc.conePointUniqueUpToIso (limit.isLimit F)))
have w : ∀ (j : J),
  Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ F.obj j)
    (CategoryStruct.comp (Y := limit F) (limMap c.π) (limit.π F j))
    (CategoryStruct.comp (Y := limit F)
      (Iso.hom
        (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
          hc.conePointUniqueUpToIso (limit.isLimit F)))
      (limit.π F j))
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
hc : IsLimit c
j : J
⊢ Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ F.obj j)
    (CategoryStruct.comp (Y := limit F) (limMap c.π) (limit.π F j))
    (CategoryStruct.comp (Y := limit F)
      (Iso.hom
        (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt) ≪≫
          hc.conePointUniqueUpToIso (limit.isLimit F)))
      (limit.π F j))
have w : Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ F.obj j)
  (limit.π (Functor.obj (Functor.const J) c.pt) j ≫ c.π.app j)
  (Iso.hom (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt)) ≫
    c.π.app j)
Tactic: simp only [limMap_π, Functor.const_obj_obj, limit.cone_x, constCone_pt, Iso.trans_hom, assoc,
    limit.conePointUniqueUpToIso_hom_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type u₁
inst : Category.{v₁, u₁} J
C : Type u₂
inst_1 : Category.{v₂, u₂} C
inst_2 : IsConnected.{v₁, u₁} J
F : Functor.{v₁, v₂, u₁, u₂} J C
inst_3 : HasLimit F
c : Cone F
hc : IsLimit c
j : J
⊢ Eq (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ F.obj j)
    (limit.π (Functor.obj (Functor.const J) c.pt) j ≫ c.π.app j)
    (Iso.hom (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt)) ≫
      c.π.app j)
have w : Eq.{v₂ + 1} (α := limit.{v₁, u₁, v₂, u₂} (Functor.obj (Functor.const J) c.pt) ⟶ c.pt)
  (limit.π (Functor.obj (Functor.const J) c.pt) j)
  (Iso.hom (conePointUniqueUpToIso (limit.isLimit (Functor.obj (Functor.const J) c.pt)) (isLimitConstCone J c.pt)))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type v₁
⊢ IsConnected.{v₁, v₁} (WidePullbackShape J)
have h : ∀ (p : Set (WidePullbackShape J)),
  none ∈ p → (∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : WidePullbackShape J), j ∈ p
Tactic: apply IsConnected.of_induct
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type v₁
h :
  ∀ (p : Set (WidePullbackShape J)),
    none ∈ p → (∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : WidePullbackShape J), j ∈ p
⊢ IsConnected.{v₁, v₁} (WidePullbackShape J)
have j₀ : WidePullbackShape J
Tactic: apply IsConnected.of_induct
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type v₁
p : Set (WidePullbackShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : WidePullbackShape J
h : none ∈ p
⊢ j ∈ p
have h₁ : ∀ (val : J), some val ∈ p
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type v₁
⊢ IsConnected.{v₁, v₁} (WidePushoutShape J)
have h : ∀ (p : Set (WidePushoutShape J)),
  none ∈ p → (∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : WidePushoutShape J), j ∈ p
Tactic: apply IsConnected.of_induct
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type v₁
h :
  ∀ (p : Set (WidePushoutShape J)),
    none ∈ p → (∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : WidePushoutShape J), j ∈ p
⊢ IsConnected.{v₁, v₁} (WidePushoutShape J)
have j₀ : WidePushoutShape J
Tactic: apply IsConnected.of_induct
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
J : Type v₁
p : Set (WidePushoutShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : WidePushoutShape J
h : none ∈ p
⊢ j ∈ p
have h₁ : ∀ (val : J), some val ∈ p
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
⊢ IsConnected WalkingParallelPair
have h : ∀ (p : Set WalkingParallelPair),
  WalkingParallelPair.one ∈ p →
    (∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : WalkingParallelPair), j ∈ p
Tactic: apply IsConnected.of_induct
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
h :
  ∀ (p : Set WalkingParallelPair),
    WalkingParallelPair.one ∈ p →
      (∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : WalkingParallelPair), j ∈ p
⊢ IsConnected WalkingParallelPair
have j₀ : WalkingParallelPair
Tactic: apply IsConnected.of_induct
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
p : Set WalkingParallelPair
h : WalkingParallelPair.one ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : WalkingParallelPair
⊢ j ∈ p
have h : WalkingParallelPair.zero ∈ p
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
inst_1 : HasBinaryProducts.{v₂, u₂} C
J : Type v₂
inst_2 : SmallCategory J
inst_3 : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ Functor.obj prod.functor X)
j : J
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := K ⋙ Functor.obj prod.functor X) (Functor.mapCone (Functor.obj prod.functor X) c))
      (prod.lift
        (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
          (s.π.app (Classical.arbitrary J)) prod.fst)
        (l.lift (forgetCone s)))
      (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj prod.functor X) c)) j) =
    s.π.app j
have h₁ : CategoryStruct.comp (Y := Limits.prod.{v₂, u₂} X (K.obj j))
    (CategoryStruct.comp (Y :=
      Cone.pt (F := K ⋙ Functor.obj prod.functor X) (Functor.mapCone (Functor.obj prod.functor X) c))
      (prod.lift
        (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
          (s.π.app (Classical.arbitrary J)) prod.fst)
        (l.lift (forgetCone s)))
      (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj prod.functor X) c)) j))
    prod.fst =
  s.π.app j ≫ prod.fst
Tactic: apply Limits.prod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
inst_1 : HasBinaryProducts.{v₂, u₂} C
J : Type v₂
inst_2 : SmallCategory J
inst_3 : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ Functor.obj prod.functor X)
j : J
h₁ :
  CategoryStruct.comp (Y := Limits.prod.{v₂, u₂} X (K.obj j))
      (CategoryStruct.comp (Y :=
        Cone.pt (F := K ⋙ Functor.obj prod.functor X) (Functor.mapCone (Functor.obj prod.functor X) c))
        (prod.lift
          (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
            (s.π.app (Classical.arbitrary J)) prod.fst)
          (l.lift (forgetCone s)))
        (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj prod.functor X) c)) j))
      prod.fst =
    s.π.app j ≫ prod.fst
⊢ CategoryStruct.comp (Y :=
      Cone.pt (F := K ⋙ Functor.obj prod.functor X) (Functor.mapCone (Functor.obj prod.functor X) c))
      (prod.lift
        (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
          (s.π.app (Classical.arbitrary J)) prod.fst)
        (l.lift (forgetCone s)))
      (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj prod.functor X) c)) j) =
    s.π.app j
have h₂ : CategoryStruct.comp (Y := Limits.prod.{v₂, u₂} X (K.obj j))
    (CategoryStruct.comp (Y :=
      Cone.pt (F := K ⋙ Functor.obj prod.functor X) (Functor.mapCone (Functor.obj prod.functor X) c))
      (prod.lift
        (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
          (s.π.app (Classical.arbitrary J)) prod.fst)
        (l.lift (forgetCone s)))
      (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj prod.functor X) c)) j))
    prod.snd =
  s.π.app j ≫ prod.snd
Tactic: apply Limits.prod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
inst_1 : HasBinaryProducts.{v₂, u₂} C
J : Type v₂
inst_2 : SmallCategory J
inst_3 : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ Functor.obj prod.functor X)
j : J
⊢ CategoryStruct.comp (Y := Limits.prod.{v₂, u₂} X (K.obj j))
      (CategoryStruct.comp (Y :=
        Cone.pt (F := K ⋙ Functor.obj prod.functor X) (Functor.mapCone (Functor.obj prod.functor X) c))
        (prod.lift
          (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
            (s.π.app (Classical.arbitrary J)) prod.fst)
          (l.lift (forgetCone s)))
        (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj prod.functor X) c)) j))
      prod.fst =
    s.π.app j ≫ prod.fst
have h₁ : NatTrans.app
    (Cone.π
      (BinaryFan.mk (P := s.pt)
        (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
            (s.π.app (Classical.arbitrary J)) prod.fst :
          s.pt ⟶ X)
        (l.lift (forgetCone s) : (forgetCone s).pt ⟶ c.pt)))
    { as := WalkingPair.left } =
  s.π.app j ≫ prod.fst
Tactic: erw [assoc, limMap_π, comp_id, limit.lift_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
inst_1 : HasBinaryProducts.{v₂, u₂} C
J : Type v₂
inst_2 : SmallCategory J
inst_3 : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ Functor.obj prod.functor X)
m : s.pt ⟶ Cone.pt (F := K ⋙ Functor.obj prod.functor X) (Functor.mapCone (Functor.obj prod.functor X) c)
L : ∀ (j : J), m ≫ NatTrans.app (Cone.π (Functor.mapCone (Functor.obj prod.functor X) c)) j = s.π.app j
⊢ m =
    prod.lift
      (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
        (s.π.app (Classical.arbitrary J)) prod.fst)
      (l.lift (forgetCone s))
have h₁ : m ≫ prod.fst =
  CategoryStruct.comp (Y := Limits.prod.{v₂, u₂} X c.pt)
    (prod.lift
      (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
        (s.π.app (Classical.arbitrary J)) prod.fst)
      (l.lift (forgetCone s)))
    prod.fst
Tactic: apply Limits.prod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
inst_1 : HasBinaryProducts.{v₂, u₂} C
J : Type v₂
inst_2 : SmallCategory J
inst_3 : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ Functor.obj prod.functor X)
m : s.pt ⟶ Cone.pt (F := K ⋙ Functor.obj prod.functor X) (Functor.mapCone (Functor.obj prod.functor X) c)
L : ∀ (j : J), m ≫ NatTrans.app (Cone.π (Functor.mapCone (Functor.obj prod.functor X) c)) j = s.π.app j
h₁ :
  m ≫ prod.fst =
    CategoryStruct.comp (Y := Limits.prod.{v₂, u₂} X c.pt)
      (prod.lift
        (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
          (s.π.app (Classical.arbitrary J)) prod.fst)
        (l.lift (forgetCone s)))
      prod.fst
⊢ m =
    prod.lift
      (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
        (s.π.app (Classical.arbitrary J)) prod.fst)
      (l.lift (forgetCone s))
have h₂ : m ≫ prod.snd =
  CategoryStruct.comp (Y := Limits.prod.{v₂, u₂} X c.pt)
    (prod.lift
      (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
        (s.π.app (Classical.arbitrary J)) prod.fst)
      (l.lift (forgetCone s)))
    prod.snd
Tactic: apply Limits.prod.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
inst_1 : HasBinaryProducts.{v₂, u₂} C
J : Type v₂
inst_2 : SmallCategory J
inst_3 : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ Functor.obj prod.functor X)
m : s.pt ⟶ Cone.pt (F := K ⋙ Functor.obj prod.functor X) (Functor.mapCone (Functor.obj prod.functor X) c)
L : ∀ (j : J), m ≫ NatTrans.app (Cone.π (Functor.mapCone (Functor.obj prod.functor X) c)) j = s.π.app j
⊢ m ≫ prod.snd =
    CategoryStruct.comp (Y := Limits.prod.{v₂, u₂} X c.pt)
      (prod.lift
        (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
          (s.π.app (Classical.arbitrary J)) prod.fst)
        (l.lift (forgetCone s)))
      prod.snd
have h₂ : m ≫ prod.snd =
  NatTrans.app
    (Cone.π
      (BinaryFan.mk (P := s.pt)
        (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
            (s.π.app (Classical.arbitrary J)) prod.fst :
          s.pt ⟶ X)
        (l.lift (forgetCone s) : (forgetCone s).pt ⟶ c.pt)))
    { as := WalkingPair.right }
Tactic: rw [limit.lift_π]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Connected (goal)
Goal:
C : Type u₂
inst : Category.{v₂, u₂} C
inst_1 : HasBinaryProducts.{v₂, u₂} C
J : Type v₂
inst_2 : SmallCategory J
inst_3 : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ Functor.obj prod.functor X)
m : s.pt ⟶ Cone.pt (F := K ⋙ Functor.obj prod.functor X) (Functor.mapCone (Functor.obj prod.functor X) c)
L : ∀ (j : J), m ≫ NatTrans.app (Cone.π (Functor.mapCone (Functor.obj prod.functor X) c)) j = s.π.app j
⊢ m ≫ prod.snd =
    NatTrans.app
      (Cone.π
        (BinaryFan.mk (P := s.pt)
          (CategoryStruct.comp (Y := (K ⋙ Functor.obj prod.functor X).obj (Classical.arbitrary J))
              (s.π.app (Classical.arbitrary J)) prod.fst :
            s.pt ⟶ X)
          (l.lift (forgetCone s) : (forgetCone s).pt ⟶ c.pt)))
      { as := WalkingPair.right }
have h₂ : ∀ (j : J), (m ≫ prod.snd) ≫ c.π.app j = (forgetCone s).π.app j
Tactic: apply l.uniq (forgetCone s)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cone F
X : C
hX : IsTerminal.{v, u} X
f : F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ X
g : F.obj { as := WalkingPair.right : Discrete WalkingPair } ⟶ X
hc :
  IsLimit (F := cospan f g)
    (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair }) (c.π.app { as := WalkingPair.right })
        ⋯ :
      PullbackCone f g)
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ c.π.app j = s.π.app j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ c.π.app { as := WalkingPair.right }) ⋯
⊢ m =
    hc.lift
      (PullbackCone.mk (s.π.app { as := WalkingPair.left : Discrete WalkingPair }) (s.π.app { as := WalkingPair.right })
        ⋯)
have dsimp : m =
  hc.lift
    (PullbackCone.mk (s.π.app { as := WalkingPair.left : Discrete WalkingPair }) (s.π.app { as := WalkingPair.right })
      sorry)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cone F
X : C
hX : IsTerminal.{v, u} X
f : F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ X
g : F.obj { as := WalkingPair.right : Discrete WalkingPair } ⟶ X
hc :
  IsLimit (F := cospan f g)
    (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair }) (c.π.app { as := WalkingPair.right })
        ⋯ :
      PullbackCone f g)
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ c.π.app j = s.π.app j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ c.π.app { as := WalkingPair.right }) ⋯
⊢ m =
    hc.lift
      (PullbackCone.mk (s.π.app { as := WalkingPair.left : Discrete WalkingPair }) (s.π.app { as := WalkingPair.right })
        ⋯)
have rw : m =
  hc.lift
    (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
      (m ≫ c.π.app { as := WalkingPair.right }) sorry)
Tactic: rw [← J, ← J]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cone F
X : C
hX : IsTerminal.{v, u} X
f : F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ X
g : F.obj { as := WalkingPair.right : Discrete WalkingPair } ⟶ X
hc :
  IsLimit (F := cospan f g)
    (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair }) (c.π.app { as := WalkingPair.right })
        ⋯ :
      PullbackCone f g)
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ c.π.app j = s.π.app j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ c.π.app { as := WalkingPair.right }) ⋯
⊢ m =
    hc.lift
      (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
        (m ≫ c.π.app { as := WalkingPair.right }) ⋯)
have apply : ∀ (j : WalkingCospan),
  Eq (α := s.pt ⟶ (cospan f g).obj j)
    (m ≫
      NatTrans.app
        (Cone.π
          (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair })
            (c.π.app { as := WalkingPair.right }) sorry))
        j)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := cospan f g)
        (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair })
            (c.π.app { as := WalkingPair.right }) sorry :
          PullbackCone f g))
      (hc.lift
        (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
          (m ≫ c.π.app { as := WalkingPair.right }) sorry))
      (NatTrans.app
        (Cone.π
          (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair })
            (c.π.app { as := WalkingPair.right }) sorry))
        j))
Tactic: apply hc.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u'
inst_1 : Category.{v', u'} D
F_1 : CategoryTheory.Functor.{v, v', u, u'} C D
F : CategoryTheory.Functor.{0, v, 0, u} (Discrete WalkingPair) C
c : Cone F
X : C
hX : IsTerminal.{v, u} X
f : F.obj { as := WalkingPair.left : Discrete WalkingPair } ⟶ X
g : F.obj { as := WalkingPair.right : Discrete WalkingPair } ⟶ X
hc :
  IsLimit (F := cospan f g)
    (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair }) (c.π.app { as := WalkingPair.right })
        ⋯ :
      PullbackCone f g)
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ c.π.app j = s.π.app j
c' : PullbackCone f g :=
  PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
    (m ≫ c.π.app { as := WalkingPair.right }) ⋯
⊢ Eq (α := s.pt ⟶ (cospan f g).obj none)
    (m ≫
      NatTrans.app
        (Cone.π
          (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair })
            (c.π.app { as := WalkingPair.right }) ⋯))
        none)
    (CategoryStruct.comp (Y :=
      Cone.pt (F := cospan f g)
        (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair })
            (c.π.app { as := WalkingPair.right }) ⋯ :
          PullbackCone f g))
      (hc.lift
        (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
          (m ≫ c.π.app { as := WalkingPair.right }) ⋯))
      (NatTrans.app
        (Cone.π
          (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair })
            (c.π.app { as := WalkingPair.right }) ⋯))
        none))
have none : m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair } ≫ f =
  hc.lift
      (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
        (m ≫ c.π.app { as := WalkingPair.right }) sorry) ≫
    c.π.app { as := WalkingPair.left : Discrete WalkingPair } ≫ f
Tactic: simp only [PullbackCone.mk_π_app]