awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
X_1 Y_1 : PushoutCocone f_1 g
f : X_1 ⟶ Y_1
⊢ Eq (α :=
    (Functor.obj (𝟭 (PushoutCocone f_1 g)) X_1).pt ⟶
      Cocone.pt.{0, v, 0, u} (J := WalkingSpan) (F := span f_1 g)
        (Functor.obj
          (Functor.comp (D := BinaryCofan (Under.mk f_1) (Under.mk g))
            {
              obj := fun (c : PushoutCocone f_1 g) ↦
                BinaryCofan.mk (P := Under.mk (f_1 ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
              map := fun {c₁ c₂ : PushoutCocone f_1 g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ },
              map_id := ⋯, map_comp := ⋯ }
            {
              obj := fun (c : BinaryCofan (Under.mk f_1) (Under.mk g)) ↦
                PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
              map := fun {c₁ c₂ : BinaryCofan (Under.mk f_1) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
                { hom := Under.Hom.right a.hom, w := ⋯ },
              map_id := ⋯, map_comp := ⋯ })
          Y_1))
    (CoconeMorphism.hom
      (Functor.map (𝟭 (PushoutCocone f_1 g)) f ≫ Iso.hom ((fun (c : PushoutCocone f_1 g) ↦ c.eta) Y_1)))
    (CoconeMorphism.hom
      (Iso.hom ((fun (c : PushoutCocone f_1 g) ↦ c.eta) X_1) ≫
        Functor.map
          (Functor.comp (D := BinaryCofan (Under.mk f_1) (Under.mk g))
            {
              obj := fun (c : PushoutCocone f_1 g) ↦
                BinaryCofan.mk (P := Under.mk (f_1 ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
              map := fun {c₁ c₂ : PushoutCocone f_1 g} (a : c₁ ⟶ c₂) ↦
                { hom := Under.homMk a.hom ⋯, w := ⋯ :
                  CoconeMorphism (C := Under.{v, u} X) (F := pair (Under.mk f_1) (Under.mk g))
                    (BinaryCofan.mk (P := Under.mk (f_1 ≫ c₁.inl)) (Under.homMk c₁.inl ⋯) (Under.homMk c₁.inr ⋯))
                    (BinaryCofan.mk (P := Under.mk (f_1 ≫ c₂.inl)) (Under.homMk c₂.inl ⋯) (Under.homMk c₂.inr ⋯)) },
              map_id := ⋯, map_comp := ⋯ : PushoutCocone f_1 g ⥤ BinaryCofan (Under.mk f_1) (Under.mk g) }
            {
              obj := fun (c : BinaryCofan (Under.mk f_1) (Under.mk g)) ↦
                PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
              map := fun {c₁ c₂ : BinaryCofan (Under.mk f_1) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
                { hom := Under.Hom.right a.hom, w := ⋯ :
                  CoconeMorphism (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯)
                    (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯) },
              map_id := ⋯, map_comp := ⋯ : BinaryCofan (Under.mk f_1) (Under.mk g) ⥤ PushoutCocone f_1 g })
          f))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
f : X_1 ⟶ Y
g : X_1 ⟶ Z
X : BinaryCofan (Under.mk f) (Under.mk g)
dsimp : (f ≫ Under.Hom.right X.inl) ≫ 𝟙 X.pt.right = X.pt.hom
⊢ Under.hom
        (Cocone.pt (J := Discrete WalkingPair) (F := pair (Under.mk f) (Under.mk g))
          (Functor.obj
            (Functor.comp (D := PushoutCocone f g)
              {
                obj := fun (c : BinaryCofan (Under.mk f) (Under.mk g)) ↦
                  PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
                  { hom := Under.Hom.right a.hom, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }
              {
                obj := fun (c : PushoutCocone f g) ↦
                  BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ })
            X)) ≫
      Iso.hom
        (Iso.refl
          (Under.right.{v, u} (X := X_1)
            (Cocone.pt (J := Discrete WalkingPair) (F := pair (Under.mk f) (Under.mk g))
              (Functor.obj
                (Functor.comp (D := PushoutCocone f g)
                  {
                    obj := fun (c : BinaryCofan (Under.mk f) (Under.mk g)) ↦
                      PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                    map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
                      { hom := Under.Hom.right a.hom, w := ⋯ :
                        CoconeMorphism (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯)
                          (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯) },
                    map_id := ⋯, map_comp := ⋯ : BinaryCofan (Under.mk f) (Under.mk g) ⥤ PushoutCocone f g }
                  {
                    obj := fun (c : PushoutCocone f g) ↦
                      BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                    map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦
                      { hom := Under.homMk a.hom ⋯, w := ⋯ :
                        CoconeMorphism (C := Under.{v, u} X_1) (F := pair (Under.mk f) (Under.mk g))
                          (BinaryCofan.mk (P := Under.mk (f ≫ c₁.inl)) (Under.homMk c₁.inl ⋯) (Under.homMk c₁.inr ⋯))
                          (BinaryCofan.mk (P := Under.mk (f ≫ c₂.inl)) (Under.homMk c₂.inl ⋯) (Under.homMk c₂.inr ⋯)) },
                    map_id := ⋯, map_comp := ⋯ : PushoutCocone f g ⥤ BinaryCofan (Under.mk f) (Under.mk g) })
                X)))) =
    (Functor.obj (𝟭 (BinaryCofan (Under.mk f) (Under.mk g))) X).pt.hom

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
f : X_1 ⟶ Y
g : X_1 ⟶ Z
X : BinaryCofan (Under.mk f) (Under.mk g)
⊢ (f ≫ Under.Hom.right X.inl) ≫ 𝟙 X.pt.right = X.pt.hom

Tactic:
simpa using X.inl.w

Premises used: CategoryTheory.Under.Hom.w, CategoryTheory.Limits.BinaryCofan.inl
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
f : X_1 ⟶ Y
g : X_1 ⟶ Z
X : BinaryCofan (Under.mk f) (Under.mk g)
⊢ Under.Hom.right
      (BinaryCofan.inl
          (Functor.obj
            (Functor.comp (D := PushoutCocone f g)
              {
                obj := fun (c : BinaryCofan (Under.mk f) (Under.mk g)) ↦
                  PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
                  { hom := Under.Hom.right a.hom, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }
              {
                obj := fun (c : PushoutCocone f g) ↦
                  BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ })
            X) ≫
        Iso.hom
          (Under.isoMk
            (Iso.refl
              (Under.right.{v, u} (X := X_1)
                (Cocone.pt (J := Discrete WalkingPair) (F := pair (Under.mk f) (Under.mk g))
                  (Functor.obj
                    (Functor.comp (D := PushoutCocone f g)
                      {
                        obj := fun (c : BinaryCofan (Under.mk f) (Under.mk g)) ↦
                          PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                        map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
                          { hom := Under.Hom.right a.hom, w := ⋯ :
                            CoconeMorphism (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯)
                              (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯) },
                        map_id := ⋯, map_comp := ⋯ : BinaryCofan (Under.mk f) (Under.mk g) ⥤ PushoutCocone f g }
                      {
                        obj := fun (c : PushoutCocone f g) ↦
                          BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                        map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦
                          { hom := Under.homMk a.hom ⋯, w := ⋯ :
                            CoconeMorphism (C := Under.{v, u} X_1) (F := pair (Under.mk f) (Under.mk g))
                              (BinaryCofan.mk (P := Under.mk (f ≫ c₁.inl)) (Under.homMk c₁.inl ⋯)
                                (Under.homMk c₁.inr ⋯))
                              (BinaryCofan.mk (P := Under.mk (f ≫ c₂.inl)) (Under.homMk c₂.inl ⋯)
                                (Under.homMk c₂.inr ⋯)) },
                        map_id := ⋯, map_comp := ⋯ : PushoutCocone f g ⥤ BinaryCofan (Under.mk f) (Under.mk g) })
                    X))))
            ⋯)) =
    Under.Hom.right (Functor.obj (𝟭 (BinaryCofan (Under.mk f) (Under.mk g))) X).inl

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X_1 Y Z : C
f : X_1 ⟶ Y
g : X_1 ⟶ Z
X : BinaryCofan (Under.mk f) (Under.mk g)
⊢ Under.Hom.right
      (BinaryCofan.inr
          (Functor.obj
            (Functor.comp (D := PushoutCocone f g)
              {
                obj := fun (c : BinaryCofan (Under.mk f) (Under.mk g)) ↦
                  PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
                  { hom := Under.Hom.right a.hom, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ }
              {
                obj := fun (c : PushoutCocone f g) ↦
                  BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦ { hom := Under.homMk a.hom ⋯, w := ⋯ },
                map_id := ⋯, map_comp := ⋯ })
            X) ≫
        Iso.hom
          (Under.isoMk
            (Iso.refl
              (Under.right.{v, u} (X := X_1)
                (Cocone.pt (J := Discrete WalkingPair) (F := pair (Under.mk f) (Under.mk g))
                  (Functor.obj
                    (Functor.comp (D := PushoutCocone f g)
                      {
                        obj := fun (c : BinaryCofan (Under.mk f) (Under.mk g)) ↦
                          PushoutCocone.mk (Under.Hom.right c.inl) (Under.Hom.right c.inr) ⋯,
                        map := fun {c₁ c₂ : BinaryCofan (Under.mk f) (Under.mk g)} (a : c₁ ⟶ c₂) ↦
                          { hom := Under.Hom.right a.hom, w := ⋯ :
                            CoconeMorphism (PushoutCocone.mk (Under.Hom.right c₁.inl) (Under.Hom.right c₁.inr) ⋯)
                              (PushoutCocone.mk (Under.Hom.right c₂.inl) (Under.Hom.right c₂.inr) ⋯) },
                        map_id := ⋯, map_comp := ⋯ : BinaryCofan (Under.mk f) (Under.mk g) ⥤ PushoutCocone f g }
                      {
                        obj := fun (c : PushoutCocone f g) ↦
                          BinaryCofan.mk (P := Under.mk (f ≫ c.inl)) (Under.homMk c.inl ⋯) (Under.homMk c.inr ⋯),
                        map := fun {c₁ c₂ : PushoutCocone f g} (a : c₁ ⟶ c₂) ↦
                          { hom := Under.homMk a.hom ⋯, w := ⋯ :
                            CoconeMorphism (C := Under.{v, u} X_1) (F := pair (Under.mk f) (Under.mk g))
                              (BinaryCofan.mk (P := Under.mk (f ≫ c₁.inl)) (Under.homMk c₁.inl ⋯)
                                (Under.homMk c₁.inr ⋯))
                              (BinaryCofan.mk (P := Under.mk (f ≫ c₂.inl)) (Under.homMk c₂.inl ⋯)
                                (Under.homMk c₂.inr ⋯)) },
                        map_id := ⋯, map_comp := ⋯ : PushoutCocone f g ⥤ BinaryCofan (Under.mk f) (Under.mk g) })
                    X))))
            ⋯)) =
    Under.Hom.right (Functor.obj (𝟭 (BinaryCofan (Under.mk f) (Under.mk g))) X).inr

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
⊢ (Under.mk (f ≫ c.inl)).hom ≫ hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯) = s.pt.hom

Tactic:
simpa using s.inl.w

Premises used: CategoryTheory.Under.Hom.w, CategoryTheory.Limits.BinaryCofan.inl
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
h :
  Under.Hom.right m =
    Under.Hom.right
      ((fun (s : BinaryCofan (Under.mk f) (Under.mk g)) ↦
          Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)
        s)
⊢ m =
    (fun (s : BinaryCofan (Under.mk f) (Under.mk g)) ↦
        Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)
      s

Tactic:
ext1
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ Under.Hom.right m =
    Under.Hom.right
      ((fun (s : BinaryCofan (Under.mk f) (Under.mk g)) ↦
          Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)
        s)

Tactic:
PushoutCocone.IsColimit.hom_ext hc ?_ ?_

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
h :
  c.inl ≫ Under.Hom.right m =
    c.inl ≫
      Under.Hom.right
        ((fun (s : BinaryCofan (Under.mk f) (Under.mk g)) ↦
            Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)
          s)
h₁ :
  c.inr ≫ Under.Hom.right m =
    c.inr ≫
      Under.Hom.right
        ((fun (s : BinaryCofan (Under.mk f) (Under.mk g)) ↦
            Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)
          s)
⊢ Under.Hom.right m =
    Under.Hom.right
      ((fun (s : BinaryCofan (Under.mk f) (Under.mk g)) ↦
          Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)
        s)

Tactic:
refine PushoutCocone.IsColimit.hom_ext hc ?_ ?_

Premises used: CategoryTheory.Limits.PushoutCocone.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ c.inl ≫ Under.Hom.right m =
    c.inl ≫
      Under.Hom.right
        ((fun (s : BinaryCofan (Under.mk f) (Under.mk g)) ↦
            Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)
          s)

Tactic:
simpa using congr(($e₁).right)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : PushoutCocone f g
hc : IsColimit c
s : BinaryCofan (Under.mk f) (Under.mk g)
m : Under.mk (f ≫ c.inl) ⟶ s.pt
e₁ : Under.homMk c.inl ⋯ ≫ m = s.inl
e₂ : Under.homMk c.inr ⋯ ≫ m = s.inr
⊢ c.inr ≫ Under.Hom.right m =
    c.inr ≫
      Under.Hom.right
        ((fun (s : BinaryCofan (Under.mk f) (Under.mk g)) ↦
            Under.homMk (hc.desc (PushoutCocone.mk (Under.Hom.right s.inl) (Under.Hom.right s.inr) ⋯)) ⋯)
          s)

Tactic:
simpa using congr(($e₂).right)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s :
  PushoutCocone (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
    (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom
⊢ Under.Hom.right c.inl ≫
      (fun
            (s :
              PushoutCocone
                (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
                (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
          (Under.Hom.right (hc.desc (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s)) :
            c.pt.right ⟶ (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt.right))
        s =
    s.inl

Tactic:
simpa only using congr($(hc.fac _ _).right)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s :
  PushoutCocone (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
    (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom
⊢ Under.Hom.right c.inr ≫
      (fun
            (s :
              PushoutCocone
                (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
                (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
          (Under.Hom.right (hc.desc (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s)) :
            c.pt.right ⟶ (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt.right))
        s =
    s.inr

Tactic:
simpa only using congr($(hc.fac _ _).right)
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s :
  PushoutCocone (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
    (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom
m :
  (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).right ⟶
    s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
change :
  ∀ (s : PushoutCocone f g)
    (m :
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
            { as := WalkingPair.left : Discrete WalkingPair }).right ⟶
        s.pt)
    (hm₁ : Under.Hom.right c.inl ≫ m = s.inl) (hm₂ : Under.Hom.right c.inr ≫ m = s.inr),
    m =
      (fun
            (s :
              PushoutCocone
                (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
                (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
          (Under.Hom.right (hc.desc (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s)) :
            c.pt.right ⟶ (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt.right))
        s
⊢ m =
    (fun
          (s :
            PushoutCocone
              (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
              (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
        (Under.Hom.right (hc.desc (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s)) :
          c.pt.right ⟶ (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt.right))
      s

Tactic:
change PushoutCocone f g at s

Premises used: CategoryTheory.Limits.PushoutCocone
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m :
  (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).right ⟶
    s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
⊢ c.pt.hom ≫ m = (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt.hom

Tactic:
simp [← hm₁, dsimp% c.inl.w_assoc]

Premises used: CategoryTheory.Limits.BinaryCofan.inl, CategoryTheory.Under.Hom.w_assoc
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m :
  (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).right ⟶
    s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
left :
  Eq (α :=
    (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).right ⟶
      (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt.right)
    (Under.Hom.right (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ Under.homMk m ⋯))
    (Under.Hom.right
      ((Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).ι.app { as := WalkingPair.left }))
⊢ Eq (α :=
    Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt)
    (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ Under.homMk m ⋯)
    ((Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).ι.app { as := WalkingPair.left })

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Limits.Constructions.Over.Products
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
c : BinaryCofan (Under.mk f) (Under.mk g)
hc : IsColimit c
s : PushoutCocone f g
m :
  (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).right ⟶
    s.pt
hm₁ : Under.Hom.right c.inl ≫ m = s.inl
hm₂ : Under.Hom.right c.inr ≫ m = s.inr
right :
  Eq (α :=
    (Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).right ⟶
      (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt.right)
    (Under.Hom.right (c.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫ Under.homMk m ⋯))
    (Under.Hom.right
      ((Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).ι.app { as := WalkingPair.right }))
⊢ Eq (α :=
    Functor.obj (pair (Under.mk f) (Under.mk g)) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt)
    (c.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫ Under.homMk m ⋯)
    ((Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).ι.app { as := WalkingPair.right })

Tactic:
ext