awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ m =
    (fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
        (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) ⋯ :
          s.pt ⟶ Over.mk (c.fst ≫ f)))
      s
have h : Over.Hom.left m =
  Over.Hom.left
    ((fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
        (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) sorry :
          s.pt ⟶ Over.mk (c.fst ≫ f)))
      s)
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
⊢ Over.Hom.left m =
    Over.Hom.left
      ((fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
          (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) ⋯ :
            s.pt ⟶ Over.mk (c.fst ≫ f)))
        s)
have h : Over.Hom.left m ≫ c.fst =
  Over.Hom.left
      ((fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
          (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) sorry :
            s.pt ⟶ Over.mk (c.fst ≫ f)))
        s) ≫
    c.fst
Tactic: apply PullbackCone.IsLimit.hom_ext hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : PullbackCone f g
hc : IsLimit c
s : BinaryFan (Over.mk f) (Over.mk g)
m : s.pt ⟶ Over.mk (c.fst ≫ f)
e₁ : m ≫ Over.homMk c.fst ⋯ = s.fst
e₂ : m ≫ Over.homMk c.snd ⋯ = s.snd
h :
  Over.Hom.left m ≫ c.fst =
    Over.Hom.left
        ((fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
            (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) ⋯ :
              s.pt ⟶ Over.mk (c.fst ≫ f)))
          s) ≫
      c.fst
⊢ Over.Hom.left m =
    Over.Hom.left
      ((fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
          (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) ⋯ :
            s.pt ⟶ Over.mk (c.fst ≫ f)))
        s)
have h₁ : Over.Hom.left m ≫ c.snd =
  Over.Hom.left
      ((fun (s : BinaryFan (Over.mk f) (Over.mk g)) ↦
          (Over.homMk (hc.lift (Functor.obj (Equivalence.inverse pullbackConeEquivBinaryFan) s)) sorry :
            s.pt ⟶ Over.mk (c.fst ≫ f)))
        s) ≫
    c.snd
Tactic: apply PullbackCone.IsLimit.hom_ext hc
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s :
  PullbackCone (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
    (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom
m :
  s.pt ⟶
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ m =
    (fun
          (s :
            PullbackCone
              (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
              (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
        (Over.Hom.left (hc.lift (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s)) :
          (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶ c.pt.left))
      s
have change : ∀ (s : PullbackCone f g)
  (m :
    s.pt ⟶
      (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
          { as := WalkingPair.left : Discrete WalkingPair }).left)
  (hm₁ : m ≫ Over.Hom.left c.fst = s.fst) (hm₂ : m ≫ Over.Hom.left c.snd = s.snd),
  m =
    (fun
          (s :
            PullbackCone
              (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
              (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
        (Over.Hom.left (hc.lift (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s)) :
          (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶ c.pt.left))
      s
Tactic: change PullbackCone f g at s
Cleared hypotheses: s, m, hm₁, hm₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m :
  s.pt ⟶
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Eq (α :=
    (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt ⟶
      Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair })
    (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair })
    ((Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).π.app { as := WalkingPair.left })
have left : Eq (α :=
  (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶
    (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).left)
  (Over.Hom.left (Over.homMk m sorry ≫ c.π.app { as := WalkingPair.left : Discrete WalkingPair }))
  (Over.Hom.left ((Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).π.app { as := WalkingPair.left }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m :
  s.pt ⟶
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ Eq (α :=
    (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt ⟶
      Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair })
    (Over.homMk m ⋯ ≫ c.π.app { as := WalkingPair.right : Discrete WalkingPair })
    ((Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).π.app { as := WalkingPair.right })
have right : Eq (α :=
  (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶
    (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).left)
  (Over.Hom.left (Over.homMk m sorry ≫ c.π.app { as := WalkingPair.right : Discrete WalkingPair }))
  (Over.Hom.left ((Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).π.app { as := WalkingPair.right }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (hypothesis)
Goal:
J : Type w
C : Type u
inst : Category.{v, u} C
X Y Z : C
f : Y ⟶ X
g : Z ⟶ X
c : BinaryFan (Over.mk f) (Over.mk g)
hc : IsLimit c
s : PullbackCone f g
m :
  s.pt ⟶
    (Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair }).left
hm₁ : m ≫ Over.Hom.left c.fst = s.fst
hm₂ : m ≫ Over.Hom.left c.snd = s.snd
⊢ m =
    (fun
          (s :
            PullbackCone
              (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.left : Discrete WalkingPair }).hom
              (Functor.obj (pair (Over.mk f) (Over.mk g)) { as := WalkingPair.right : Discrete WalkingPair }).hom) ↦
        (Over.Hom.left (hc.lift (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s)) :
          (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt.left ⟶ c.pt.left))
      s
have this : Eq (α := (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s).pt ⟶ c.pt) (Over.homMk m sorry)
  (hc.lift (Functor.obj (Equivalence.functor pullbackConeEquivBinaryFan) s))
Tactic: have := hc.uniq (pullbackConeEquivBinaryFan.functor.obj s) (Over.homMk m <| by
        simp [← hm₁, dsimp% c.fst.w])
        (by rintro (_ | _) <;> ext <;> simpa)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
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
        (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
have dsimp : (f ≫ Under.Hom.right X.inl) ≫ 𝟙 X.pt.right = X.pt.hom
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
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
⊢ 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
have 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) sorry)) sorry)
      s)
Tactic: ext1
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
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)
have 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) sorry)) sorry)
        s)
Tactic: refine PushoutCocone.IsColimit.hom_ext hc ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
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)
⊢ 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)
have 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) sorry)) sorry)
        s)
Tactic: refine PushoutCocone.IsColimit.hom_ext hc ?_ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
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
⊢ 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
have 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
Tactic: change PushoutCocone f g at s
Cleared hypotheses: s, m, hm₁, hm₂
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
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
⊢ 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 })
have 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 sorry))
  (Under.Hom.right
    ((Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).ι.app { as := WalkingPair.left }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
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
⊢ 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 })
have 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 sorry))
  (Under.Hom.right
    ((Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).ι.app { as := WalkingPair.right }))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (hypothesis)
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
⊢ 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
have this : Eq (α := c.pt ⟶ (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s).pt) (Under.homMk m sorry)
  (hc.desc (Functor.obj (Equivalence.functor pushoutCoconeEquivBinaryCofan) s))
Tactic: have := hc.uniq (pushoutCoconeEquivBinaryCofan.functor.obj s) (Under.homMk m <| by
        simp [← hm₁, dsimp% c.inl.w_assoc])
        (by rintro (_ | _) <;> ext <;> simpa)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
J_1 : Type w
C : Type u
inst : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over.{v, u} B
X_1 Y_1 : Cone F
f : X_1 ⟶ Y_1
j : WidePullbackShape J
⊢ Hom.left f.hom ≫ (conesEquivInverseObj B F Y_1).π.app j = (conesEquivInverseObj B F X_1).π.app j
have none : Eq (α := (conesEquivInverseObj B F X_1).pt ⟶ (widePullbackDiagramOfDiagramOver B F).obj none)
  (Hom.left f.hom ≫ (conesEquivInverseObj B F Y_1).π.app none) ((conesEquivInverseObj B F X_1).π.app none)
Tactic: obtain - | j := j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
J_1 : Type w
C : Type u
inst : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over.{v, u} B
X_1 Y_1 : Cone F
f : X_1 ⟶ Y_1
j : WidePullbackShape J
none :
  Eq (α := (conesEquivInverseObj B F X_1).pt ⟶ (widePullbackDiagramOfDiagramOver B F).obj Option.none)
    (Hom.left f.hom ≫ (conesEquivInverseObj B F Y_1).π.app Option.none)
    ((conesEquivInverseObj B F X_1).π.app Option.none)
⊢ Hom.left f.hom ≫ (conesEquivInverseObj B F Y_1).π.app j = (conesEquivInverseObj B F X_1).π.app j
have some : ∀ (j : J),
  Eq (α := (conesEquivInverseObj B F X_1).pt ⟶ (widePullbackDiagramOfDiagramOver B F).obj (some j))
    (Hom.left f.hom ≫ (conesEquivInverseObj B F Y_1).π.app (some j)) ((conesEquivInverseObj B F X_1).π.app (some j))
Tactic: obtain - | j := j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
J_1 : Type w
C : Type u
inst : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over.{v, u} B
X_1 Y_1 : Cone F
f : X_1 ⟶ Y_1
j : J
⊢ Eq (α := (conesEquivInverseObj B F X_1).pt ⟶ (widePullbackDiagramOfDiagramOver B F).obj (some j))
    (Hom.left f.hom ≫ (conesEquivInverseObj B F Y_1).π.app (some j)) ((conesEquivInverseObj B F X_1).π.app (some j))
have some : Eq (α := X_1.pt.left ⟶ (F.obj { as := j : Discrete J }).left) (Hom.left f.hom ≫ Hom.left (Y_1.π.app { as := j }))
  (Hom.left (X_1.π.app { as := j }))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
J_1 : Type w
C : Type u
inst : Category.{v, u} C
X Y Z B : C
J : Type w
F : Discrete J ⥤ Over.{v, u} B
X_1 Y_1 : Cone F
f : X_1 ⟶ Y_1
j : J
⊢ Eq (α := X_1.pt.left ⟶ (F.obj { as := j : Discrete J }).left) (Hom.left f.hom ≫ Hom.left (Y_1.π.app { as := j }))
    (Hom.left (X_1.π.app { as := j }))
have some : Eq (α := X_1.pt.left ⟶ (F.obj { as := j : Discrete J }).left) (Hom.left f.hom ≫ Hom.left (Y_1.π.app { as := j }))
  (Hom.left (f.hom ≫ Y_1.π.app { as := j }))
Tactic: rw [← f.w ⟨j⟩]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Constructions.Over.Products (goal)
Goal:
C : Type u
inst : Category.{v, u} C
B : C
F : Discrete PEmpty.{1} ⥤ Over.{v, u} B
s : Cone F
m :
  s.pt ⟶
    Cone.pt (J := Discrete PEmpty.{1}) (F := F)
      { pt := mk (𝟙 B), π := { app := fun (p : Discrete PEmpty.{1}) ↦ p.as.elim, naturality := ⋯ } }
h :
  ∀ (j : Discrete PEmpty.{1}),
    m ≫
        NatTrans.app
          (Cone.π { pt := mk (𝟙 B), π := { app := fun (p : Discrete PEmpty.{1}) ↦ p.as.elim, naturality := ⋯ } }) j =
      s.π.app j
⊢ m = homMk s.pt.hom ⋯
have h : Hom.left m = Hom.left (homMk s.pt.hom sorry)
Tactic: ext