awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
f g h : α → C
inst_1 : HasProduct.{w₂, v, u} f
inst_2 : HasProduct.{w₂, v, u} g
inst_3 : HasProduct.{w₂, v, u} h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
⊢ Eq (α := piObj.{w₂, v, u} f ⟶ piObj.{w₂, v, u} h) (CategoryStruct.comp (Y := piObj.{w₂, v, u} g) (map q) (map q'))
    (map fun (a : α) ↦ q a ≫ q' a)
have h₁ : ∀ (b : α),
  Eq (α := piObj.{w₂, v, u} f ⟶ h b)
    (CategoryStruct.comp (Y := piObj.{w₂, v, u} h) (CategoryStruct.comp (Y := piObj.{w₂, v, u} g) (map q) (map q'))
      (π h b))
    (CategoryStruct.comp (Y := piObj.{w₂, v, u} h) (map fun (a : α) ↦ q a ≫ q' a) (π h b))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f g : β → C
inst_1 : HasProduct.{w, v, u} f
inst_2 : HasProduct.{w, v, u} g
p : (b : β) → f b ⟶ g b
inst_3 : ∀ (i : β), Mono (p i)
⊢ ∀ (j : Discrete β),
    Mono.{v, u} (C := C) (X := Functor.obj.{w, v, w, u} (Discrete.functor f) j) (Y :=
      Functor.obj.{w, v, w, u} (Discrete.functor g) j)
      (NatTrans.app (Discrete.natTrans fun (X : Discrete β) ↦ p X.as) j)
have dsimp : ∀ (j : Discrete β), Mono (X := f j.as) (p j.as)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
inst_1 : HasProduct.{w₂, v, u} f
⊢ (map' id fun (a : α) ↦ 𝟙 (f a)) = 𝟙 (piObj.{w₂, v, u} f)
have h : ∀ (b : α),
  CategoryStruct.comp (Y := piObj.{w₂, v, u} f) (map' id fun (a : α) ↦ 𝟙 (f a)) (π f b) = 𝟙 (piObj.{w₂, v, u} f) ≫ π f b
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst_1 : HasProduct.{w₂, v, u} f
inst_2 : HasProduct.{w, v, u} g
inst_3 : HasProduct.{w₃, v, u} h
p : β → α
p' : γ → β
q : (b : β) → f (p b) ⟶ g b
q' : (c : γ) → g (p' c) ⟶ h c
⊢ Eq (α := piObj.{w₂, v, u} f ⟶ piObj.{w₃, v, u} h)
    (CategoryStruct.comp (Y := piObj.{w, v, u} g) (map' p q) (map' p' q')) (map' (p ∘ p') fun (c : γ) ↦ q (p' c) ≫ q' c)
have h₁ : ∀ (b : γ),
  Eq (α := piObj.{w₂, v, u} f ⟶ h b)
    (CategoryStruct.comp (Y := piObj.{w₃, v, u} h)
      (CategoryStruct.comp (Y := piObj.{w, v, u} g) (map' p q) (map' p' q')) (π h b))
    (CategoryStruct.comp (Y := piObj.{w₃, v, u} h) (map' (p ∘ p') fun (c : γ) ↦ q (p' c) ≫ q' c) (π h b))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
g h : β → C
inst_1 : HasProduct.{w₂, v, u} f
inst_2 : HasProduct.{w, v, u} g
inst_3 : HasProduct.{w, v, u} h
p : β → α
q : (b : β) → f (p b) ⟶ g b
q' : (b : β) → g b ⟶ h b
⊢ Eq (α := piObj.{w₂, v, u} f ⟶ piObj.{w, v, u} h) (CategoryStruct.comp (Y := piObj.{w, v, u} g) (map' p q) (map q'))
    (map' p fun (b : β) ↦ q b ≫ q' b)
have h₁ : ∀ (b : β),
  Eq (α := piObj.{w₂, v, u} f ⟶ h b)
    (CategoryStruct.comp (Y := piObj.{w, v, u} h) (CategoryStruct.comp (Y := piObj.{w, v, u} g) (map' p q) (map q'))
      (π h b))
    (CategoryStruct.comp (Y := piObj.{w, v, u} h) (map' p fun (b : β) ↦ q b ≫ q' b) (π h b))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
C : Type u
inst : Category.{v, u} C
f g : α → C
h : β → C
inst_1 : HasProduct.{w₂, v, u} f
inst_2 : HasProduct.{w₂, v, u} g
inst_3 : HasProduct.{w, v, u} h
p : β → α
q : (a : α) → f a ⟶ g a
q' : (b : β) → g (p b) ⟶ h b
⊢ Eq (α := piObj.{w₂, v, u} f ⟶ piObj.{w, v, u} h) (CategoryStruct.comp (Y := piObj.{w₂, v, u} g) (map q) (map' p q'))
    (map' p fun (b : β) ↦ q (p b) ≫ q' b)
have h₁ : ∀ (b : β),
  Eq (α := piObj.{w₂, v, u} f ⟶ h b)
    (CategoryStruct.comp (Y := piObj.{w, v, u} h) (CategoryStruct.comp (Y := piObj.{w₂, v, u} g) (map q) (map' p q'))
      (π h b))
    (CategoryStruct.comp (Y := piObj.{w, v, u} h) (map' p fun (b : β) ↦ q (p b) ≫ q' b) (π h b))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasProduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cone X
m : s.pt ⟶ (Pi.cone X).pt
hm : ∀ (j : Discrete α), m ≫ (Pi.cone X).π.app j = s.π.app j
⊢ m = Pi.lift fun (j : α) ↦ s.π.app { as := j }
have h : ∀ (b : α),
  m ≫ Pi.π (fun (j : α) ↦ X.obj { as := j : Discrete α }) b =
    CategoryStruct.comp (Y := piObj.{w₂, v, u} fun (j : α) ↦ X.obj { as := j })
      (Pi.lift fun (j : α) ↦ s.π.app { as := j }) (Pi.π (fun (j : α) ↦ X.obj { as := j }) b)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasProduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cone X
m : s.pt ⟶ (Pi.cone X).pt
hm : ∀ (j : Discrete α), m ≫ (Pi.cone X).π.app j = s.π.app j
b : α
⊢ m ≫ Pi.π (fun (j : α) ↦ X.obj { as := j : Discrete α }) b =
    CategoryStruct.comp (Y := piObj.{w₂, v, u} fun (j : α) ↦ X.obj { as := j })
      (Pi.lift fun (j : α) ↦ s.π.app { as := j }) (Pi.π (fun (j : α) ↦ X.obj { as := j }) b)
have h : m ≫ Pi.π (fun (j : α) ↦ X.obj { as := j : Discrete α }) b = s.π.app { as := b }
Tactic: simp only [limit.lift_π, Fan.mk_pt, Fan.mk_π_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
inst_1 : HasCoproduct.{w₂, v, u} f
⊢ (map fun (a : α) ↦ 𝟙 (f a)) = 𝟙 (sigmaObj.{w₂, v, u} f)
have h : ∀ (b : α),
  CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map fun (a : α) ↦ 𝟙 (f a)) =
    ι f b ≫ 𝟙 (sigmaObj.{w₂, v, u} f)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
f g h : α → C
inst_1 : HasCoproduct.{w₂, v, u} f
inst_2 : HasCoproduct.{w₂, v, u} g
inst_3 : HasCoproduct.{w₂, v, u} h
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h a
⊢ Eq (α := sigmaObj.{w₂, v, u} f ⟶ sigmaObj.{w₂, v, u} h)
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} g) (map q) (map q')) (map fun (a : α) ↦ q a ≫ q' a)
have h₁ : ∀ (b : α),
  Eq (α := f b ⟶ sigmaObj.{w₂, v, u} h)
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b)
      (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} g) (map q) (map q')))
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map fun (a : α) ↦ q a ≫ q' a))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f g : β → C
inst_1 : HasCoproduct.{w, v, u} f
inst_2 : HasCoproduct.{w, v, u} g
p : (b : β) → f b ⟶ g b
inst_3 : ∀ (i : β), Epi (p i)
⊢ ∀ (j : Discrete β),
    Epi.{v, u} (C := C) (X := Functor.obj.{w, v, w, u} (Discrete.functor f) j) (Y :=
      Functor.obj.{w, v, w, u} (Discrete.functor g) j)
      (NatTrans.app (Discrete.natTrans fun (X : Discrete β) ↦ p X.as) j)
have dsimp : ∀ (j : Discrete β), Epi (X := f j.as) (p j.as)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
inst_1 : HasCoproduct.{w₂, v, u} f
⊢ (map' id fun (a : α) ↦ 𝟙 (f a)) = 𝟙 (sigmaObj.{w₂, v, u} f)
have h : ∀ (b : α),
  CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map' id fun (a : α) ↦ 𝟙 (f a)) =
    ι f b ≫ 𝟙 (sigmaObj.{w₂, v, u} f)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
f : α → C
g : β → C
h : γ → C
inst_1 : HasCoproduct.{w₂, v, u} f
inst_2 : HasCoproduct.{w, v, u} g
inst_3 : HasCoproduct.{w₃, v, u} h
p : α → β
p' : β → γ
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h (p' b)
⊢ Eq (α := sigmaObj.{w₂, v, u} f ⟶ sigmaObj.{w₃, v, u} h)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} g) (map' p q) (map' p' q'))
    (map' (p' ∘ p) fun (a : α) ↦ q a ≫ q' (p a))
have h₁ : ∀ (b : α),
  Eq (α := f b ⟶ sigmaObj.{w₃, v, u} h)
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b)
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} g) (map' p q) (map' p' q')))
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map' (p' ∘ p) fun (a : α) ↦ q a ≫ q' (p a)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
C : Type u
inst : Category.{v, u} C
f : α → C
g h : β → C
inst_1 : HasCoproduct.{w₂, v, u} f
inst_2 : HasCoproduct.{w, v, u} g
inst_3 : HasCoproduct.{w, v, u} h
p : α → β
q : (a : α) → f a ⟶ g (p a)
q' : (b : β) → g b ⟶ h b
⊢ Eq (α := sigmaObj.{w₂, v, u} f ⟶ sigmaObj.{w, v, u} h)
    (CategoryStruct.comp (Y := sigmaObj.{w, v, u} g) (map' p q) (map q')) (map' p fun (a : α) ↦ q a ≫ q' (p a))
have h₁ : ∀ (b : α),
  Eq (α := f b ⟶ sigmaObj.{w, v, u} h)
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b)
      (CategoryStruct.comp (Y := sigmaObj.{w, v, u} g) (map' p q) (map q')))
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map' p fun (a : α) ↦ q a ≫ q' (p a)))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
C : Type u
inst : Category.{v, u} C
f g : α → C
h : β → C
inst_1 : HasCoproduct.{w₂, v, u} f
inst_2 : HasCoproduct.{w₂, v, u} g
inst_3 : HasCoproduct.{w, v, u} h
p : α → β
q : (a : α) → f a ⟶ g a
q' : (a : α) → g a ⟶ h (p a)
⊢ Eq (α := sigmaObj.{w₂, v, u} f ⟶ sigmaObj.{w, v, u} h)
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} g) (map q) (map' p q')) (map' p fun (a : α) ↦ q a ≫ q' a)
have h₁ : ∀ (b : α),
  Eq (α := f b ⟶ sigmaObj.{w, v, u} h)
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b)
      (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} g) (map q) (map' p q')))
    (CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} f) (ι f b) (map' p fun (a : α) ↦ q a ≫ q' a))
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasCoproduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cocone X
m : (Sigma.cocone X).pt ⟶ s.pt
hm : ∀ (j : Discrete α), (Sigma.cocone X).ι.app j ≫ m = s.ι.app j
⊢ m = Sigma.desc fun (j : α) ↦ s.ι.app { as := j }
have h : ∀ (b : α),
  Sigma.ι.{w₂, v, u} (C := C) (fun (j : α) ↦ X.obj { as := j : Discrete α }) b ≫ m =
    CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} fun (j : α) ↦ X.obj { as := j })
      (Sigma.ι.{w₂, v, u} (C := C) (fun (j : α) ↦ X.obj { as := j }) b) (Sigma.desc fun (j : α) ↦ s.ι.app { as := j })
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
X : Functor.{w₂, v, w₂, u} (Discrete α) C
inst_1 : HasCoproduct.{w₂, v, u} (C := C) fun (j : α) ↦ X.obj { as := j }
s : Cocone X
m : (Sigma.cocone X).pt ⟶ s.pt
hm : ∀ (j : Discrete α), (Sigma.cocone X).ι.app j ≫ m = s.ι.app j
b : α
⊢ Sigma.ι.{w₂, v, u} (C := C) (fun (j : α) ↦ X.obj { as := j : Discrete α }) b ≫ m =
    CategoryStruct.comp (Y := sigmaObj.{w₂, v, u} fun (j : α) ↦ X.obj { as := j })
      (Sigma.ι.{w₂, v, u} (C := C) (fun (j : α) ↦ X.obj { as := j }) b) (Sigma.desc fun (j : α) ↦ s.ι.app { as := j })
have h : Sigma.ι.{w₂, v, u} (C := C) (fun (j : α) ↦ X.obj { as := j : Discrete α }) b ≫ m = s.ι.app { as := b }
Tactic: simp only [colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
ι : Type u_1
f : ι → Type u_2
g : (i : ι) → f i → C
inst_1 : ∀ (i : ι), HasProduct.{u_2, v, u} (g i)
inst_2 : HasProduct.{u_1, v, u} (C := C) fun (i : ι) ↦ piObj.{u_2, v, u} (g i)
s : Fan (C := C) fun (p : (i : ι) × f i) ↦ g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i))
⊢ ∀
    (m :
      s.pt ⟶
        Cone.pt (J := Discrete ((i : ι) × f i)) (F :=
          Discrete.functor fun (p : (i : ι) × f i) ↦
            g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i)))
          (Fan.mk (piObj.{u_1, v, u} fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
            Pi.π (fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) (X.fst (β := fun (i : ι) ↦ f i)) ≫
              Pi.π (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i)))),
    (∀ (j : (i : ι) × f i),
        m ≫
            Fan.proj
              (Fan.mk (piObj.{u_1, v, u} fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
                Pi.π (fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) (X.fst (β := fun (i : ι) ↦ f i)) ≫
                  Pi.π (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i)))
              j =
          s.proj j) →
      m =
        (fun
              (s :
                Fan (C := C) fun (p : (i : ι) × f i) ↦
                  g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i))) ↦
            (Pi.lift fun (b : ι) ↦ Pi.lift fun (c : f b) ↦ s.proj (Sigma.mk (β := fun (i : ι) ↦ f i) b c) :
              s.pt ⟶
                piObj.{u_1, v, u} fun (b : ι) ↦
                  piObj.{u_2, v, u} fun (c : f b) ↦
                    g ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).fst (β := fun (i : ι) ↦ f i))
                      ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).snd (β := fun (i : ι) ↦ f i))))
          s
have _ : ∀ (m : s.pt ⟶ piObj.{u_1, v, u} fun (i : ι) ↦ piObj.{u_2, v, u} (g i)),
  (∀ (j : (i : ι) × f i),
      m ≫
          Fan.proj
            (Fan.mk (piObj.{u_1, v, u} fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) fun (X : (i : ι) × f i) ↦
              Pi.π (fun (i : ι) ↦ piObj.{u_2, v, u} (g i)) (X.fst (β := fun (i : ι) ↦ f i)) ≫
                Pi.π (g (X.fst (β := fun (i : ι) ↦ f i))) (X.snd (β := fun (i : ι) ↦ f i)))
            j =
        s.proj j) →
    m =
      (fun
            (s :
              Fan (C := C) fun (p : (i : ι) × f i) ↦
                g (p.fst (β := fun (i : ι) ↦ f i)) (p.snd (β := fun (i : ι) ↦ f i))) ↦
          (Pi.lift fun (b : ι) ↦ Pi.lift fun (c : f b) ↦ s.proj (Sigma.mk (β := fun (i : ι) ↦ f i) b c) :
            s.pt ⟶
              piObj.{u_1, v, u} fun (b : ι) ↦
                piObj.{u_2, v, u} fun (c : f b) ↦
                  g ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).fst (β := fun (i : ι) ↦ f i))
                    ((Sigma.mk (β := fun (i : ι) ↦ f i) b c).snd (β := fun (i : ι) ↦ f i))))
        s
Tactic: (m : _ ⟶ (∏ᶜ fun i ↦ ∏ᶜ g i))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : β → C
inst_2 : HasProduct.{w, v, u} f
inst_3 : HasProduct.{w, v₂, u₂} (C := D) fun (b : β) ↦ G.obj (f b)
P : C
g : (j : β) → P ⟶ f j
⊢ Eq (α := G.obj P ⟶ piObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b))
    (CategoryStruct.comp (Y := G.obj (piObj.{w, v, u} f)) (G.map (Pi.lift g)) (piComparison G f))
    (Pi.lift fun (j : β) ↦ G.map (g j))
have h : ∀ (j : β),
  CategoryStruct.comp (Y := piObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b))
      (CategoryStruct.comp (Y := G.obj (piObj.{w, v, u} f)) (G.map (Pi.lift g)) (piComparison G f))
      (Pi.π (fun (b : β) ↦ G.obj (f b)) j) =
    CategoryStruct.comp (Y := piObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b)) (Pi.lift fun (j : β) ↦ G.map (g j))
      (Pi.π (fun (b : β) ↦ G.obj (f b)) j)
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v, v₂, u, u₂} C D
f : β → C
inst_2 : HasCoproduct.{w, v, u} f
inst_3 : HasCoproduct.{w, v₂, u₂} (C := D) fun (b : β) ↦ G.obj (f b)
P : C
g : (j : β) → f j ⟶ P
⊢ Eq (α := (sigmaObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b)) ⟶ G.obj P)
    (CategoryStruct.comp (Y := G.obj (sigmaObj.{w, v, u} f)) (sigmaComparison G f) (G.map (Sigma.desc g)))
    (Sigma.desc fun (j : β) ↦ G.map (g j))
have h : ∀ (j : β),
  CategoryStruct.comp (Y := sigmaObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b))
      (Sigma.ι.{w, v₂, u₂} (C := D) (fun (b : β) ↦ G.obj (f b)) j)
      (CategoryStruct.comp (Y := G.obj (sigmaObj.{w, v, u} f)) (sigmaComparison G f) (G.map (Sigma.desc g))) =
    CategoryStruct.comp (Y := sigmaObj.{w, v₂, u₂} fun (b : β) ↦ G.obj (f b))
      (Sigma.ι.{w, v₂, u₂} (C := D) (fun (b : β) ↦ G.obj (f b)) j) (Sigma.desc fun (j : β) ↦ G.map (g j))
Tactic: ext j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v, v, u} C
X : C
x x_1 : Cᵒᵖ
x_2 : x ⟶ x_1
⊢ Eq (α :=
    Functor.obj.{v, v, u, u} (Functor.obj yoneda X ⋙ Functor.rightOp (Functor.obj piConst X)) x ⟶
      Functor.obj.{v, v, u, u} (𝟭 Cᵒᵖ) x_1)
    (Functor.map (Functor.obj yoneda X ⋙ Functor.rightOp (Functor.obj piConst X)) x_2 ≫ Quiver.Hom.op (Pi.lift id))
    (Quiver.Hom.op (Pi.lift id) ≫ Functor.map (𝟭 Cᵒᵖ) x_2)
have a : Eq (α :=
  Opposite.unop (Functor.obj.{v, v, u, u} (𝟭 Cᵒᵖ) x_1) ⟶
    Opposite.unop (Functor.obj.{v, v, u, u} (Functor.obj yoneda X ⋙ Functor.rightOp (Functor.obj piConst X)) x))
  (Quiver.Hom.unop
    (Functor.map (Functor.obj yoneda X ⋙ Functor.rightOp (Functor.obj piConst X)) x_2 ≫ Quiver.Hom.op (Pi.lift id)))
  (Quiver.Hom.unop (Quiver.Hom.op (Pi.lift id) ≫ Functor.map (𝟭 Cᵒᵖ) x_2))
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : HasProducts.{v, v, u} C
X : C
x : Type v
⊢ CategoryStruct.comp (Y :=
      Functor.obj (Functor.rightOp (Functor.obj piConst X))
        (Functor.obj (Functor.obj yoneda X) (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x)))
      (Functor.map (Functor.rightOp (Functor.obj piConst X))
        (NatTrans.app
          { app := fun (n : Type v) ↦ ↾fun (i : Functor.obj (𝟭 (Type v)) n) ↦ Pi.π (fun (x : n) ↦ X) i,
            naturality := ⋯ }
          x))
      (NatTrans.app { app := fun (Y : Cᵒᵖ) ↦ Quiver.Hom.op (Pi.lift id), naturality := ⋯ }
        (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x)) =
    𝟙 (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x)
have a : Eq (α :=
  Opposite.unop (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x) ⟶
    Opposite.unop (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x))
  (Quiver.Hom.unop
    (CategoryStruct.comp (Y :=
      Functor.obj (Functor.rightOp (Functor.obj piConst X))
        (Functor.obj (Functor.obj yoneda X) (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x)))
      (Functor.map (Functor.rightOp (Functor.obj piConst X))
        (NatTrans.app
          { app := fun (n : Type v) ↦ ↾fun (i : Functor.obj (𝟭 (Type v)) n) ↦ Pi.π (fun (x : n) ↦ X) i,
            naturality := sorry }
          x))
      (NatTrans.app { app := fun (Y : Cᵒᵖ) ↦ Quiver.Hom.op (Pi.lift id), naturality := sorry }
        (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x))))
  (Quiver.Hom.unop (𝟙 (Functor.obj (Functor.rightOp (Functor.obj piConst X)) x)))
Tactic: apply Quiver.Hom.unop_inj
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
x : Discrete β
j : β
⊢ Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) { as := j : Discrete β } =
    Functor.obj.{w, v, w, u} (Discrete.functor f) { as := j : Discrete β }
have dsimp : f default = f j
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
x : Discrete β
j : β
⊢ f default = f j
have e_a : default = j
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Products (goal)
Goal:
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst : Category.{v, u} C
inst_1 : Unique β
f : β → C
s : Cone.{w, v, w, u} (Discrete.functor f)
j : Discrete β
⊢ CategoryStruct.comp (Y :=
      Cone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
        { pt := f default,
          π :=
            Discrete.natTrans fun (x : Discrete β) ↦
              match (motive :=
                (x : Discrete β) →
                  Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                    Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                x with
              | { as := j } => eqToHom ⋯ })
      (s.π.app default)
      (NatTrans.app
        (Cone.π
          { pt := f default,
            π :=
              Discrete.natTrans fun (x : Discrete β) ↦
                match (motive :=
                  (x : Discrete β) →
                    Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                      Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                  x with
                | { as := j } => eqToHom ⋯ })
        j) =
    s.π.app j
have obtain : Eq (α := s.pt ⟶ Functor.obj.{w, v, w, u} (Discrete.functor f) default)
  (CategoryStruct.comp (Y :=
    Cone.pt.{w, v, w, u} (J := Discrete β) (F := Discrete.functor f)
      { pt := f default,
        π :=
          Discrete.natTrans fun (x : Discrete β) ↦
            match (motive :=
              (x : Discrete β) →
                Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                  Functor.obj.{w, v, w, u} (Discrete.functor f) x)
              x with
            | { as := j } => eqToHom sorry })
    (s.π.app default)
    (NatTrans.app
      (Cone.π
        { pt := f default,
          π :=
            Discrete.natTrans fun (x : Discrete β) ↦
              match (motive :=
                (x : Discrete β) →
                  Functor.obj.{w, v, w, u} (Functor.obj (Functor.const (Discrete β)) (f default)) x ⟶
                    Functor.obj.{w, v, w, u} (Discrete.functor f) x)
                x with
              | { as := j } => eqToHom sorry })
      default))
  (s.π.app default)
Tactic: obtain rfl := Subsingleton.elim j default
Cleared hypotheses: j