awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
h :
  ∀ (p : Set WalkingParallelPair),
    WalkingParallelPair.one ∈ p →
      (∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p) → ∀ (j : WalkingParallelPair), j ∈ p
j₀ : WalkingParallelPair
⊢ IsConnected WalkingParallelPair

Tactic:
apply IsConnected.of_induct

Premises used: CategoryTheory.IsConnected.of_induct
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
p : Set WalkingParallelPair
h_1 : WalkingParallelPair.one ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
j : WalkingParallelPair
h : WalkingParallelPair.zero ∈ p
h₁ : WalkingParallelPair.one ∈ p
⊢ j ∈ p

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
p : Set WalkingParallelPair
h_1 : WalkingParallelPair.one ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
h h₁ h₂ h₃ : WalkingParallelPair.one ∈ p
⊢ WalkingParallelPair.zero ∈ p

Tactic:
rwa [t WalkingParallelPairHom.left]

Premises used: CategoryTheory.Limits.WalkingParallelPairHom.left
-- Module: Mathlib.CategoryTheory.Limits.Connected
Goal:
p : Set WalkingParallelPair
h : WalkingParallelPair.one ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair} (x : j₁ ⟶ j₂), j₁ ∈ p ↔ j₂ ∈ p
⊢ WalkingParallelPair.one ∈ p

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
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
⊢ 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

Tactic:
apply Limits.prod.hom_ext

Premises used: CategoryTheory.Limits.prod.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Connected
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₁ :
  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
⊢ 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:
erw [assoc, limMap_π, comp_id, limit.lift_π]

Premises used: CategoryTheory.Limits.limMap_π, CategoryTheory.Category.assoc, CategoryTheory.Category.comp_id, CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
⊢ 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:
(nat_trans_from_is_connected (s.π ≫ γ₁ X) j (Classical.arbitrary _)).symm

Premises used: CategoryTheory.Limits.limit.π, CategoryTheory.Limits.Cone.π, CategoryTheory.ProdPreservesConnectedLimits.γ₁, CategoryTheory.Limits.limit, Classical.arbitrary, CategoryTheory.CategoryStruct.comp, CategoryTheory.nat_trans_from_is_connected, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
⊢ 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:
exact (nat_trans_from_is_connected (s.π ≫ γ₁ X) j (Classical.arbitrary _)).symm

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ProdPreservesConnectedLimits.γ₁, Classical.arbitrary, CategoryTheory.CategoryStruct.comp, CategoryTheory.nat_trans_from_is_connected, Eq.symm
-- Module: Mathlib.CategoryTheory.Limits.Connected
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.snd =
    s.π.app j ≫ prod.snd

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
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
⊢ 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))

Tactic:
apply Limits.prod.hom_ext

Premises used: CategoryTheory.Limits.prod.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Connected
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.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:
simp [← L]
-- Module: Mathlib.CategoryTheory.Limits.Connected
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.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 }
⊢ 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:
rw [limit.lift_π]

Premises used: CategoryTheory.Limits.limit.lift_π
-- Module: Mathlib.CategoryTheory.Limits.Connected
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₂ : ∀ (j : J), (m ≫ prod.snd) ≫ c.π.app j = (forgetCone 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 }

Tactic:
apply l.uniq (forgetCone s)

Premises used: CategoryTheory.ProdPreservesConnectedLimits.forgetCone, CategoryTheory.Limits.IsLimit.uniq
-- Module: Mathlib.CategoryTheory.Limits.Connected
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
j : J
⊢ (m ≫ prod.snd) ≫ c.π.app j = (forgetCone s).π.app j

Tactic:
simp [← L j]
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
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 }) ⋯
dsimp :
  m =
    hc.lift
      (PullbackCone.mk (s.π.app { as := WalkingPair.left : Discrete WalkingPair }) (s.π.app { as := WalkingPair.right })
        ⋯)
⊢ m =
    hc.lift
      (PullbackCone.mk (s.π.app { as := WalkingPair.left : Discrete WalkingPair }) (s.π.app { as := WalkingPair.right })
        ⋯)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
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 }) ⋯
rw :
  m =
    hc.lift
      (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 })
        ⋯)

Tactic:
rw [← J, ← J]
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
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 }) ⋯
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 }) ⋯))
          j)
      (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 }) ⋯))
          j))
⊢ m =
    hc.lift
      (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
        (m ≫ c.π.app { as := WalkingPair.right }) ⋯)

Tactic:
apply hc.hom_ext

Premises used: CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
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 }) ⋯
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 }) ⋯) ≫
      c.π.app { as := WalkingPair.left : Discrete WalkingPair } ≫ f
⊢ Eq (α := s.pt ⟶ (cospan f g).obj Option.none)
    (m ≫
      NatTrans.app
        (Cone.π
          (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair })
            (c.π.app { as := WalkingPair.right }) ⋯))
        Option.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 }) ⋯))
        Option.none))

Tactic:
simp only [PullbackCone.mk_π_app]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
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 }) ⋯
some :
  Eq (α := s.pt ⟶ (cospan f g).obj (Option.some WalkingPair.left)) (m ≫ c.π.app { as := WalkingPair.left })
    (hc.lift
        (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
          (m ≫ c.π.app { as := WalkingPair.right }) ⋯) ≫
      c.π.app { as := WalkingPair.left : Discrete WalkingPair })
⊢ Eq (α := s.pt ⟶ (cospan f g).obj (Option.some WalkingPair.left))
    (m ≫
      NatTrans.app
        (Cone.π
          (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair })
            (c.π.app { as := WalkingPair.right }) ⋯))
        (Option.some WalkingPair.left))
    (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 }) ⋯))
        (Option.some WalkingPair.left)))

Tactic:
simp only [PullbackCone.mk_π_app]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app
-- Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
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 }) ⋯
some :
  Eq (α := s.pt ⟶ (cospan f g).obj (Option.some WalkingPair.right)) (m ≫ c.π.app { as := WalkingPair.right })
    (hc.lift
        (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
          (m ≫ c.π.app { as := WalkingPair.right }) ⋯) ≫
      c.π.app { as := WalkingPair.right : Discrete WalkingPair })
⊢ Eq (α := s.pt ⟶ (cospan f g).obj (Option.some WalkingPair.right))
    (m ≫
      NatTrans.app
        (Cone.π
          (PullbackCone.mk (c.π.app { as := WalkingPair.left : Discrete WalkingPair })
            (c.π.app { as := WalkingPair.right }) ⋯))
        (Option.some WalkingPair.right))
    (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 }) ⋯))
        (Option.some WalkingPair.right)))

Tactic:
simp only [PullbackCone.mk_π_app]

Premises used: CategoryTheory.Limits.PullbackCone.mk_π_app