awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
f : J → C
inst_10 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
rw :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f)))
      (desc b.ι) =
    𝟙 b.pt
rw₁ :
  CategoryStruct.comp (Y := biproduct.{w, v, u} f) (Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f)))
      (Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f))) =
    𝟙 b.pt
⊢ CategoryStruct.comp (Y := biproduct.{w, v, u} f) (lift b.π) (desc b.ι) = 𝟙 b.pt
have rw₂ : Eq.{v + 1} (α := b.pt ⟶ b.pt) (𝟙 b.pt) (𝟙 b.pt)
Tactic: rw [← biproduct.conePointUniqueUpToIso_hom f hb, ←
      biproduct.conePointUniqueUpToIso_inv f hb, Iso.hom_inv_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
f : J → C
inst_10 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
⊢ desc b.ι ≫ lift b.π = 𝟙 (biproduct.{w, v, u} f)
have rw : desc b.ι ≫ Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f)) = 𝟙 (biproduct.{w, v, u} f)
Tactic: rw [← biproduct.conePointUniqueUpToIso_hom f hb, ←
      biproduct.conePointUniqueUpToIso_inv f hb, Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
f : J → C
inst_10 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
rw : desc b.ι ≫ Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f)) = 𝟙 (biproduct.{w, v, u} f)
⊢ desc b.ι ≫ lift b.π = 𝟙 (biproduct.{w, v, u} f)
have rw₁ : Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f)) ≫ Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f)) =
  𝟙 (biproduct.{w, v, u} f)
Tactic: rw [← biproduct.conePointUniqueUpToIso_hom f hb, ←
      biproduct.conePointUniqueUpToIso_inv f hb, Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
f : J → C
inst_10 : HasBiproduct.{w, v, u} f
b : Bicone.{w, v, u} f
hb : b.IsBilimit
rw : desc b.ι ≫ Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f)) = 𝟙 (biproduct.{w, v, u} f)
rw₁ :
  Iso.inv (hb.isLimit.conePointUniqueUpToIso (isLimit f)) ≫ Iso.hom (hb.isLimit.conePointUniqueUpToIso (isLimit f)) =
    𝟙 (biproduct.{w, v, u} f)
⊢ desc b.ι ≫ lift b.π = 𝟙 (biproduct.{w, v, u} f)
have rw₂ : Eq.{v + 1} (α := biproduct.{w, v, u} f ⟶ biproduct.{w, v, u} f) (𝟙 (biproduct.{w, v, u} f)) (𝟙 (biproduct.{w, v, u} f))
Tactic: rw [← biproduct.conePointUniqueUpToIso_hom f hb, ←
      biproduct.conePointUniqueUpToIso_inv f hb, Iso.inv_hom_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : HasFiniteBiproducts.{v, u} C
⊢ HasZeroObject.{v, u} C
have refine_1 : ∀ (X : C) (a : biproduct.{0, v, u} Empty.elim ⟶ X), a = default
Tactic: refine ⟨⟨biproduct Empty.elim, fun X => ⟨⟨⟨0⟩, ?_⟩⟩, fun X => ⟨⟨⟨0⟩, ?_⟩⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : HasFiniteBiproducts.{v, u} C
refine_1 : ∀ (X : C) (a : biproduct.{0, v, u} Empty.elim ⟶ X), a = default
⊢ HasZeroObject.{v, u} C
have refine_2 : ∀ (X : C) (a : X ⟶ biproduct.{0, v, u} Empty.elim), a = default
Tactic: refine ⟨⟨biproduct Empty.elim, fun X => ⟨⟨⟨0⟩, ?_⟩⟩, fun X => ⟨⟨⟨0⟩, ?_⟩⟩⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : HasFiniteBiproducts.{v, u} C
X : C
a : biproduct.{0, v, u} Empty.elim ⟶ X
⊢ a = default
have refine_1 : ∀ (j : Empty),
  biproduct.ι Empty.elim j ≫ a =
    CategoryStruct.comp (Y := biproduct.{0, v, u} Empty.elim) (biproduct.ι Empty.elim j) default
Tactic: apply biproduct.hom_ext'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : HasFiniteBiproducts.{v, u} C
X : C
a : X ⟶ biproduct.{0, v, u} Empty.elim
⊢ a = default
have refine_2 : ∀ (j : Empty),
  a ≫ biproduct.π Empty.elim j =
    CategoryStruct.comp (Y := biproduct.{0, v, u} Empty.elim) default (biproduct.π Empty.elim j)
Tactic: apply biproduct.hom_ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : Unique J
f : J → C
j : J
⊢ f default = f j
have e_a : default = j
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : Unique J
f : J → C
j : J
⊢ default = j
have e_a : j = j
Tactic: rw [← Unique.uniq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : Unique J
f : J → C
j : J
⊢ f j = f default
have e_a : j = default
Tactic: congr
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Biproducts (goal)
Goal:
J_1 : Type w
C_1 : Type uC
inst : Category.{uC', uC} C_1
inst_1 : HasZeroMorphisms.{uC', uC} C_1
D_1 : Type uD
inst_2 : Category.{uD', uD} D_1
inst_3 : HasZeroMorphisms.{uD', uD} D_1
F : J_1 → C_1
J_2 : Type w
K : Type u_1
C_2 : Type u
inst_4 : Category.{v, u} C_2
inst_5 : HasZeroMorphisms.{v, u} C_2
J : Type w
C : Type u
inst_6 : Category.{v, u} C
inst_7 : HasZeroMorphisms.{v, u} C
D : Type uD
inst_8 : Category.{uD', uD} D
inst_9 : HasZeroMorphisms.{uD', uD} D
inst_10 : Unique J
f : J → C
j : J
⊢ j = default
have e_a : j = j
Tactic: rw [← Unique.uniq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan.{u_1, u₂, u₁} f₁
c₂ : Fan.{u_2, u₂, u₁} f₂
bc : BinaryFan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
i : WalkingPair
⊢ s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt
have left : s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.left c₁.pt c₂.pt
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan.{u_1, u₂, u₁} f₁
c₂ : Fan.{u_2, u₂, u₁} f₂
bc : BinaryFan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
i : WalkingPair
left : s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.left c₁.pt c₂.pt
⊢ s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt
have right : s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.right c₁.pt c₂.pt
Tactic: cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan.{u_1, u₂, u₁} f₁
c₂ : Fan.{u_2, u₂, u₁} f₂
bc : BinaryFan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
w : ι₁ ⊕ ι₂
⊢ (fun (s : Fan (Sum.elim f₁ f₂)) ↦
          (IsLimit.lift h fun (i : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                (h : i = t) → s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt) i
                (fun (h : i = WalkingPair.left) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                    (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                    (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
                ⋯ :
            s.pt ⟶ bc.pt))
        s ≫
      (mk bc.pt (c₁.combPairHoms c₂ bc)).proj w =
    s.proj w
have inl : ∀ (val : ι₁),
  Eq (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
    ((fun (s : Fan (Sum.elim f₁ f₂)) ↦
          (IsLimit.lift h fun (i : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                (h : i = t) → s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt) i
                (fun (h : i = WalkingPair.left) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                    (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) sorry)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                    (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) sorry)
                sorry :
            s.pt ⟶ bc.pt))
        s ≫
      (mk bc.pt (c₁.combPairHoms c₂ bc)).proj (Sum.inl val))
    (s.proj (Sum.inl val))
Tactic: cases w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan.{u_1, u₂, u₁} f₁
c₂ : Fan.{u_2, u₂, u₁} f₂
bc : BinaryFan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val : ι₁
⊢ Eq (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
    ((fun (s : Fan (Sum.elim f₁ f₂)) ↦
          (IsLimit.lift h fun (i : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                (h : i = t) → s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt) i
                (fun (h : i = WalkingPair.left) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                    (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                    (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
                ⋯ :
            s.pt ⟶ bc.pt))
        s ≫
      (mk bc.pt (c₁.combPairHoms c₂ bc)).proj (Sum.inl val))
    (s.proj (Sum.inl val))
have inl : Eq (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
  ((IsLimit.lift h fun (i : WalkingPair) ↦
      WalkingPair.rec (motive := fun (t : WalkingPair) ↦
        (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
        (fun (h : i = WalkingPair.left) ↦
          Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
            s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
            (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) sorry)
        (fun (h : i = WalkingPair.right) ↦
          Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
            s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
            (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) sorry)
        i sorry) ≫
    bc.fst ≫ c₁.proj val)
  (s.proj (Sum.inl val))
Tactic: simp only [fan_mk_proj, combPairHoms]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan.{u_1, u₂, u₁} f₁
c₂ : Fan.{u_2, u₂, u₁} f₂
bc : BinaryFan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val : ι₁
⊢ Eq (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
    ((IsLimit.lift h fun (i : WalkingPair) ↦
        WalkingPair.rec (motive := fun (t : WalkingPair) ↦
          (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
          (fun (h : i = WalkingPair.left) ↦
            Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
              s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
              (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
          (fun (h : i = WalkingPair.right) ↦
            Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
              s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
              (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
          i ⋯) ≫
      bc.fst ≫ c₁.proj val)
    (s.proj (Sum.inl val))
have inl : Eq.{u₂ + 1} (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
  (NatTrans.app
        (Cone.π
          (mk s.pt fun (i : WalkingPair) ↦
            WalkingPair.rec (motive := fun (t : WalkingPair) ↦
              (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
              (fun (h : i = WalkingPair.left) ↦
                Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                  s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
                  (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) sorry)
              (fun (h : i = WalkingPair.right) ↦
                Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                  s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
                  (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) sorry)
              i sorry))
        { as := WalkingPair.left } ≫
      c₁.proj val :
    s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
  (s.proj (Sum.inl val) : s.pt ⟶ Sum.elim f₁ f₂ (Sum.inl val))
Tactic: erw [← Category.assoc, h.fac]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan.{u_1, u₂, u₁} f₁
c₂ : Fan.{u_2, u₂, u₁} f₂
bc : BinaryFan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val : ι₂
⊢ Eq (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
    ((fun (s : Fan (Sum.elim f₁ f₂)) ↦
          (IsLimit.lift h fun (i : WalkingPair) ↦
              WalkingPair.casesOn (motive := fun (t : WalkingPair) ↦
                (h : i = t) → s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt) i
                (fun (h : i = WalkingPair.left) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                    (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
                (fun (h : i = WalkingPair.right) ↦
                  Eq.ndrec (motive := fun (i : WalkingPair) ↦
                    s.pt ⟶ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) i c₁.pt c₂.pt)
                    (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
                ⋯ :
            s.pt ⟶ bc.pt))
        s ≫
      (mk bc.pt (c₁.combPairHoms c₂ bc)).proj (Sum.inr val))
    (s.proj (Sum.inr val))
have inr : Eq (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
  ((IsLimit.lift h fun (i : WalkingPair) ↦
      WalkingPair.rec (motive := fun (t : WalkingPair) ↦
        (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
        (fun (h : i = WalkingPair.left) ↦
          Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
            s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
            (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) sorry)
        (fun (h : i = WalkingPair.right) ↦
          Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
            s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
            (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) sorry)
        i sorry) ≫
    bc.snd ≫ c₂.proj val)
  (s.proj (Sum.inr val))
Tactic: simp only [fan_mk_proj, combPairHoms]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts (goal)
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
ι₁ : Type u_1
ι₂ : Type u_2
X : C
f₁ : ι₁ → C
f₂ : ι₂ → C
c₁ : Fan.{u_1, u₂, u₁} f₁
c₂ : Fan.{u_2, u₂, u₁} f₂
bc : BinaryFan.{u₂, u₁} c₁.pt c₂.pt
h₁ : IsLimit c₁
h₂ : IsLimit c₂
h : IsLimit bc
s : Fan (Sum.elim f₁ f₂)
val : ι₂
⊢ Eq (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
    ((IsLimit.lift h fun (i : WalkingPair) ↦
        WalkingPair.rec (motive := fun (t : WalkingPair) ↦
          (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
          (fun (h : i = WalkingPair.left) ↦
            Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
              s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
              (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) ⋯)
          (fun (h : i = WalkingPair.right) ↦
            Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
              s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
              (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) ⋯)
          i ⋯) ≫
      bc.snd ≫ c₂.proj val)
    (s.proj (Sum.inr val))
have inr : Eq.{u₂ + 1} (α := s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
  (NatTrans.app
        (Cone.π
          (mk s.pt fun (i : WalkingPair) ↦
            WalkingPair.rec (motive := fun (t : WalkingPair) ↦
              (h : i = t) → s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt i)
              (fun (h : i = WalkingPair.left) ↦
                Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.left = x) ↦
                  s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
                  (IsLimit.lift h₁ fun (a : ι₁) ↦ s.proj (Sum.inl a)) sorry)
              (fun (h : i = WalkingPair.right) ↦
                Eq.rec (motive := fun (x : WalkingPair) (x_1 : WalkingPair.right = x) ↦
                  s.pt ⟶ WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) c₁.pt c₂.pt x)
                  (IsLimit.lift h₂ fun (a : ι₂) ↦ s.proj (Sum.inr a)) sorry)
              i sorry))
        { as := WalkingPair.right } ≫
      c₂.proj val :
    s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
  (s.proj (Sum.inr val) : s.pt ⟶ Sum.elim f₁ f₂ (Sum.inr val))
Tactic: erw [← Category.assoc, h.fac]