awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
j' : WalkingPair
⊢ Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.left b.inl b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
    (if h : WalkingPair.left = j' then eqToHom ⋯ else 0 : pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
have left : Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.left)
  (CategoryStruct.comp (Y := b.pt)
      (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.left b.inl b.inr)
      (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.left b.fst b.snd) :
    pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.left)
  (if h : WalkingPair.left = WalkingPair.left then eqToHom sorry else 0 :
    pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.left)
Tactic: rcases j' with ⟨⟩
Cleared hypotheses: j'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
j' : WalkingPair
left :
  Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.left)
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.left b.inl b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.left b.fst
          b.snd) :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.left)
    (if h : WalkingPair.left = WalkingPair.left then eqToHom ⋯ else 0 :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.left)
⊢ Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.left b.inl b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
      pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
    (if h : WalkingPair.left = j' then eqToHom ⋯ else 0 : pairFunction X Y WalkingPair.left ⟶ pairFunction X Y j')
have left₁ : Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.right)
  (CategoryStruct.comp (Y := b.pt)
      (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.left b.inl b.inr)
      (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.right b.fst
        b.snd) :
    pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.right)
  (if h : WalkingPair.left = WalkingPair.right then eqToHom sorry else 0 :
    pairFunction X Y WalkingPair.left ⟶ pairFunction X Y WalkingPair.right)
Tactic: rcases j' with ⟨⟩
Cleared hypotheses: j'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
j' : WalkingPair
⊢ Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.right b.inl
          b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
    (if h : WalkingPair.right = j' then eqToHom ⋯ else 0 : pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
have right : Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.left)
  (CategoryStruct.comp (Y := b.pt)
      (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.right b.inl b.inr)
      (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.left b.fst b.snd) :
    pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.left)
  (if h : WalkingPair.right = WalkingPair.left then eqToHom sorry else 0 :
    pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.left)
Tactic: rcases j' with ⟨⟩
Cleared hypotheses: j'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
j' : WalkingPair
right :
  Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.left)
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.right b.inl
          b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.left b.fst
          b.snd) :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.left)
    (if h : WalkingPair.right = WalkingPair.left then eqToHom ⋯ else 0 :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.left)
⊢ Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
    (CategoryStruct.comp (Y := b.pt)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.right b.inl
          b.inr)
        (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) j' b.fst b.snd) :
      pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
    (if h : WalkingPair.right = j' then eqToHom ⋯ else 0 : pairFunction X Y WalkingPair.right ⟶ pairFunction X Y j')
have right₁ : Eq.{uC' + 1} (α := pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.right)
  (CategoryStruct.comp (Y := b.pt)
      (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ pairFunction X Y x ⟶ b.pt) WalkingPair.right b.inl b.inr)
      (WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ b.pt ⟶ pairFunction X Y x) WalkingPair.right b.fst
        b.snd) :
    pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.right)
  (if h : WalkingPair.right = WalkingPair.right then eqToHom sorry else 0 :
    pairFunction X Y WalkingPair.right ⟶ pairFunction X Y WalkingPair.right)
Tactic: rcases j' with ⟨⟩
Cleared hypotheses: j'
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
x : Discrete WalkingPair
as : WalkingPair
⊢ Eq (α :=
    obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBicone.toCone.pt) { as := as : Discrete WalkingPair } ⟶
      obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := as : Discrete WalkingPair })
    (b.toBicone.toCone.π.app { as := as }) (Iso.hom (Iso.refl b.toBicone.toCone.pt) ≫ b.toCone.π.app { as := as })
have left : Eq (α :=
  obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBicone.toCone.pt)
      { as := WalkingPair.left : Discrete WalkingPair } ⟶
    obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.left : Discrete WalkingPair })
  (b.toBicone.toCone.π.app { as := WalkingPair.left })
  (Iso.hom (Iso.refl b.toBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.left })
Tactic: cases as
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
x : Discrete WalkingPair
as : WalkingPair
left :
  Eq (α :=
    obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBicone.toCone.pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.left : Discrete WalkingPair })
    (b.toBicone.toCone.π.app { as := WalkingPair.left })
    (Iso.hom (Iso.refl b.toBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.left })
⊢ Eq (α :=
    obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBicone.toCone.pt) { as := as : Discrete WalkingPair } ⟶
      obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := as : Discrete WalkingPair })
    (b.toBicone.toCone.π.app { as := as }) (Iso.hom (Iso.refl b.toBicone.toCone.pt) ≫ b.toCone.π.app { as := as })
have right : Eq (α :=
  obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBicone.toCone.pt)
      { as := WalkingPair.right : Discrete WalkingPair } ⟶
    obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.right : Discrete WalkingPair })
  (b.toBicone.toCone.π.app { as := WalkingPair.right })
  (Iso.hom (Iso.refl b.toBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.right })
Tactic: cases as
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
x : Discrete WalkingPair
as : WalkingPair
⊢ Eq (α :=
    obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := as : Discrete WalkingPair } ⟶ b.toCocone.pt)
    (b.toBicone.toCocone.ι.app { as := as : Discrete WalkingPair } ≫ Iso.hom (Iso.refl b.toBicone.toCocone.pt))
    (b.toCocone.ι.app { as := as })
have left : Eq (α :=
  obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.left : Discrete WalkingPair } ⟶
    b.toCocone.pt)
  (b.toBicone.toCocone.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
    Iso.hom (Iso.refl b.toBicone.toCocone.pt))
  (b.toCocone.ι.app { as := WalkingPair.left })
Tactic: cases as
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P P' Q Q' X Y : C
b : BinaryBicone.{uC', uC} X Y
x : Discrete WalkingPair
as : WalkingPair
left :
  Eq (α :=
    obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      b.toCocone.pt)
    (b.toBicone.toCocone.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl b.toBicone.toCocone.pt))
    (b.toCocone.ι.app { as := WalkingPair.left })
⊢ Eq (α :=
    obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := as : Discrete WalkingPair } ⟶ b.toCocone.pt)
    (b.toBicone.toCocone.ι.app { as := as : Discrete WalkingPair } ≫ Iso.hom (Iso.refl b.toBicone.toCocone.pt))
    (b.toCocone.ι.app { as := as })
have right : Eq (α :=
  obj.{0, uC', 0, uC} (Discrete.functor (pairFunction X Y)) { as := WalkingPair.right : Discrete WalkingPair } ⟶
    b.toCocone.pt)
  (b.toBicone.toCocone.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫
    Iso.hom (Iso.refl b.toBicone.toCocone.pt))
  (b.toCocone.ι.app { as := WalkingPair.right })
Tactic: cases as
Cleared hypotheses: as
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
j : Discrete WalkingPair
⊢ b.toBinaryBicone.toCone.π.app j = Iso.hom (Iso.refl b.toBinaryBicone.toCone.pt) ≫ b.toCone.π.app j
have left : Eq (α :=
  obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBinaryBicone.toCone.pt)
      { as := WalkingPair.left : Discrete WalkingPair } ⟶
    obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
  (b.toBinaryBicone.toCone.π.app { as := WalkingPair.left })
  (Iso.hom (Iso.refl b.toBinaryBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.left })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
j : Discrete WalkingPair
left :
  Eq (α :=
    obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBinaryBicone.toCone.pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (b.toBinaryBicone.toCone.π.app { as := WalkingPair.left })
    (Iso.hom (Iso.refl b.toBinaryBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.left })
⊢ b.toBinaryBicone.toCone.π.app j = Iso.hom (Iso.refl b.toBinaryBicone.toCone.pt) ≫ b.toCone.π.app j
have right : Eq (α :=
  obj.{0, uC', 0, uC} (obj (const (Discrete WalkingPair)) b.toBinaryBicone.toCone.pt)
      { as := WalkingPair.right : Discrete WalkingPair } ⟶
    obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
  (b.toBinaryBicone.toCone.π.app { as := WalkingPair.right })
  (Iso.hom (Iso.refl b.toBinaryBicone.toCone.pt) ≫ b.toCone.π.app { as := WalkingPair.right })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
j : Discrete WalkingPair
⊢ b.toBinaryBicone.toCocone.ι.app j ≫ Iso.hom (Iso.refl b.toBinaryBicone.toCocone.pt) = b.toCocone.ι.app j
have left : Eq (α := obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ b.toCocone.pt)
  (b.toBinaryBicone.toCocone.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
    Iso.hom (Iso.refl b.toBinaryBicone.toCocone.pt))
  (b.toCocone.ι.app { as := WalkingPair.left })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
j : Discrete WalkingPair
left :
  Eq (α := obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ b.toCocone.pt)
    (b.toBinaryBicone.toCocone.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫
      Iso.hom (Iso.refl b.toBinaryBicone.toCocone.pt))
    (b.toCocone.ι.app { as := WalkingPair.left })
⊢ b.toBinaryBicone.toCocone.ι.app j ≫ Iso.hom (Iso.refl b.toBinaryBicone.toCocone.pt) = b.toCocone.ι.app j
have right : Eq (α := obj.{0, uC', 0, uC} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶ b.toCocone.pt)
  (b.toBinaryBicone.toCocone.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫
    Iso.hom (Iso.refl b.toBinaryBicone.toCocone.pt))
  (b.toCocone.ι.app { as := WalkingPair.right })
Tactic: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q P' Q' : C
b : BinaryBicone.{uC', uC} P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ IsLimit (b.ofIso eP eQ).toCone
have refine : obj (Cone.postcompose (Iso.hom (mapPairIso eP eQ))) b.toCone ≅ (b.ofIso eP eQ).toCone
Tactic: refine (IsLimit.equivOfNatIsoOfIso (mapPairIso eP eQ) _ _ ?_).1 hb.isLimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
P Q P' Q' : C
b : BinaryBicone.{uC', uC} P Q
hb : b.IsBilimit
eP : P ≅ P'
eQ : Q ≅ Q'
⊢ IsColimit (b.ofIso eP eQ).toCocone
have refine : obj (Cocone.precompose (Iso.inv (mapPairIso eP eQ))) b.toCocone ≅ (b.ofIso eP eQ).toCocone
Tactic: refine (IsColimit.equivOfNatIsoOfIso (mapPairIso eP eQ) _ _ ?_).1 hb.isColimit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : BinaryBicone.{uC', uC} X Y
x : b.toBicone.IsBilimit
h : IsLimit b.toBicone.toCone
h' : IsColimit b.toBicone.toCocone
⊢ (fun (h : b.IsBilimit) ↦
        ({ isLimit := (b.toBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBicone.toCone) h.isLimit,
            isColimit :=
              (b.toBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBicone.toCocone) h.isColimit } :
          b.toBicone.IsBilimit))
      ((fun (h : b.toBicone.IsBilimit) ↦
          ({ isLimit := (b.toBiconeIsLimit : (a : IsLimit b.toBicone.toCone) → IsLimit b.toCone) h.isLimit,
              isColimit :=
                (b.toBiconeIsColimit : (a : IsColimit b.toBicone.toCocone) → IsColimit b.toCocone) h.isColimit } :
            b.IsBilimit))
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' : b.toBicone.IsBilimit }
have dsimp : {
    isLimit :=
      (b.toBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBicone.toCone)
        ((b.toBiconeIsLimit : (a : IsLimit b.toBicone.toCone) → IsLimit b.toCone) h),
    isColimit :=
      (b.toBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBicone.toCocone)
        ((b.toBiconeIsColimit : (a : IsColimit b.toBicone.toCocone) → IsColimit b.toCocone) h') } =
  { isLimit := h, isColimit := h' : b.toBicone.IsBilimit }
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : BinaryBicone.{uC', uC} X Y
x : b.IsBilimit
h : IsLimit b.toCone
h' : IsColimit b.toCocone
⊢ (fun (h : b.toBicone.IsBilimit) ↦
        ({ isLimit := (b.toBiconeIsLimit : (a : IsLimit b.toBicone.toCone) → IsLimit b.toCone) h.isLimit,
            isColimit :=
              (b.toBiconeIsColimit : (a : IsColimit b.toBicone.toCocone) → IsColimit b.toCocone) h.isColimit } :
          b.IsBilimit))
      ((fun (h : b.IsBilimit) ↦
          ({ isLimit := (b.toBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBicone.toCone) h.isLimit,
              isColimit :=
                (b.toBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBicone.toCocone) h.isColimit } :
            b.toBicone.IsBilimit))
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' : b.IsBilimit }
have dsimp : {
    isLimit :=
      (b.toBiconeIsLimit : (a : IsLimit b.toBicone.toCone) → IsLimit b.toCone)
        ((b.toBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBicone.toCone) h),
    isColimit :=
      (b.toBiconeIsColimit : (a : IsColimit b.toBicone.toCocone) → IsColimit b.toCocone)
        ((b.toBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBicone.toCocone) h') } =
  { isLimit := h, isColimit := h' : b.IsBilimit }
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
x : b.toBinaryBicone.IsBilimit
h : IsLimit b.toBinaryBicone.toCone
h' : IsColimit b.toBinaryBicone.toCocone
⊢ (fun (h : b.IsBilimit) ↦
        ({
            isLimit :=
              (b.toBinaryBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBinaryBicone.toCone) h.isLimit,
            isColimit :=
              (b.toBinaryBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBinaryBicone.toCocone)
                h.isColimit } :
          b.toBinaryBicone.IsBilimit))
      ((fun (h : b.toBinaryBicone.IsBilimit) ↦
          ({ isLimit := (b.toBinaryBiconeIsLimit : (a : IsLimit b.toBinaryBicone.toCone) → IsLimit b.toCone) h.isLimit,
              isColimit :=
                (b.toBinaryBiconeIsColimit : (a : IsColimit b.toBinaryBicone.toCocone) → IsColimit b.toCocone)
                  h.isColimit } :
            b.IsBilimit))
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' : b.toBinaryBicone.IsBilimit }
have dsimp : {
    isLimit :=
      (b.toBinaryBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBinaryBicone.toCone)
        ((b.toBinaryBiconeIsLimit : (a : IsLimit b.toBinaryBicone.toCone) → IsLimit b.toCone) h),
    isColimit :=
      (b.toBinaryBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBinaryBicone.toCocone)
        ((b.toBinaryBiconeIsColimit : (a : IsColimit b.toBinaryBicone.toCocone) → IsColimit b.toCocone) h') } =
  { isLimit := h, isColimit := h' : b.toBinaryBicone.IsBilimit }
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts (goal)
Goal:
J : Type w
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
D : Type uD
inst_2 : Category.{uD', uD} D
inst_3 : HasZeroMorphisms.{uD', uD} D
X Y : C
b : Bicone.{0, uC', uC} (pairFunction X Y)
x : b.IsBilimit
h : IsLimit b.toCone
h' : IsColimit b.toCocone
⊢ (fun (h : b.toBinaryBicone.IsBilimit) ↦
        ({ isLimit := (b.toBinaryBiconeIsLimit : (a : IsLimit b.toBinaryBicone.toCone) → IsLimit b.toCone) h.isLimit,
            isColimit :=
              (b.toBinaryBiconeIsColimit : (a : IsColimit b.toBinaryBicone.toCocone) → IsColimit b.toCocone)
                h.isColimit } :
          b.IsBilimit))
      ((fun (h : b.IsBilimit) ↦
          ({
              isLimit :=
                (b.toBinaryBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBinaryBicone.toCone) h.isLimit,
              isColimit :=
                (b.toBinaryBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBinaryBicone.toCocone)
                  h.isColimit } :
            b.toBinaryBicone.IsBilimit))
        { isLimit := h, isColimit := h' }) =
    { isLimit := h, isColimit := h' : b.IsBilimit }
have dsimp : {
    isLimit :=
      (b.toBinaryBiconeIsLimit : (a : IsLimit b.toBinaryBicone.toCone) → IsLimit b.toCone)
        ((b.toBinaryBiconeIsLimit.symm : (a : IsLimit b.toCone) → IsLimit b.toBinaryBicone.toCone) h),
    isColimit :=
      (b.toBinaryBiconeIsColimit : (a : IsColimit b.toBinaryBicone.toCocone) → IsColimit b.toCocone)
        ((b.toBinaryBiconeIsColimit.symm : (a : IsColimit b.toCocone) → IsColimit b.toBinaryBicone.toCocone) h') } =
  { isLimit := h, isColimit := h' : b.IsBilimit }
Tactic: dsimp only