Module: Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc : IsLimit (PullbackCone.mk (c.π.app { as := WalkingPair.left }) (c.π.app { as := WalkingPair.right }) ⋯)
s : Cone F
m : s.pt ⟶ c.pt
J : ∀ (j : Discrete WalkingPair), m ≫ c.π.app j = s.π.app j
c' : PullbackCone f g := ⋯
⊢ ∀ (j : WalkingCospan),
    m ≫ (PullbackCone.mk (c.π.app { as := WalkingPair.left }) (c.π.app { as := WalkingPair.right }) ⋯).π.app j =
      hc.lift (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left }) (m ≫ c.π.app { as := WalkingPair.right }) ⋯) ≫
        (PullbackCone.mk (c.π.app { as := WalkingPair.left }) (c.π.app { as := WalkingPair.right }) ⋯).π.app j

Tactic:
rintro (_ | (_ | _)) <;> simp only [PullbackCone.mk_π_app]

Goal state after:
case none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc : IsLimit (PullbackCone.mk (c.π.app { as := WalkingPair.left }) (c.π.app { as := WalkingPair.right }) ⋯)
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 }) (m ≫ c.π.app { as := WalkingPair.right }) ⋯
⊢ m ≫ c.π.app { as := WalkingPair.left } ≫ f =
    hc.lift (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left }) (m ≫ c.π.app { as := WalkingPair.right }) ⋯) ≫
      c.π.app { as := WalkingPair.left } ≫ f

case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc : IsLimit (PullbackCone.mk (c.π.app { as := WalkingPair.left }) (c.π.app { as := WalkingPair.right }) ⋯)
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 }) (m ≫ c.π.app { as := WalkingPair.right }) ⋯
⊢ m ≫ c.π.app { as := WalkingPair.left } =
    hc.lift (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left }) (m ≫ c.π.app { as := WalkingPair.right }) ⋯) ≫
      c.π.app { as := WalkingPair.left }

case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ : C ⥤ D
F : Discrete WalkingPair ⥤ C
c : Cone F
X : C
hX : IsTerminal X
f : F.obj { as := WalkingPair.left } ⟶ X
g : F.obj { as := WalkingPair.right } ⟶ X
hc : IsLimit (PullbackCone.mk (c.π.app { as := WalkingPair.left }) (c.π.app { as := WalkingPair.right }) ⋯)
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 }) (m ≫ c.π.app { as := WalkingPair.right }) ⋯
⊢ m ≫ c.π.app { as := WalkingPair.right } =
    hc.lift (PullbackCone.mk (m ≫ c.π.app { as := WalkingPair.left }) (m ≫ c.π.app { as := WalkingPair.right }) ⋯) ≫
      c.π.app { as := WalkingPair.right }