awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
hA : IsZero.{uC', uC} A
hB : IsZero.{uC', uC} B
mpr : 𝟙 (biprod.{uC', uC} A B) ≫ biprod.fst = CategoryStruct.comp (Y := biprod.{uC', uC} A B) 0 biprod.fst
mpr₁ : 𝟙 (biprod.{uC', uC} A B) ≫ biprod.snd = CategoryStruct.comp (Y := biprod.{uC', uC} A B) 0 biprod.snd
⊢ Eq.{uC' + 1} (α := biprod.{uC', uC} A B ⟶ biprod.{uC', uC} A B) (𝟙 (biprod.{uC', uC} A B)) 0

Tactic:
apply biprod.hom_ext

Premises used: CategoryTheory.Limits.biprod.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
hA : IsZero.{uC', uC} A
hB : IsZero.{uC', uC} B
⊢ 𝟙 (biprod.{uC', uC} A B) ≫ biprod.fst = CategoryStruct.comp (Y := biprod.{uC', uC} A B) 0 biprod.fst

Tactic:
apply hA.eq_of_tgt

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
A B : C
inst_2 : HasBinaryBiproduct.{uC', uC} A B
hA : IsZero.{uC', uC} A
hB : IsZero.{uC', uC} B
⊢ 𝟙 (biprod.{uC', uC} A B) ≫ biprod.snd = CategoryStruct.comp (Y := biprod.{uC', uC} A B) 0 biprod.snd

Tactic:
apply hB.eq_of_tgt

Premises used: CategoryTheory.Limits.IsZero.eq_of_tgt
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type uC
inst : Category.{uC', uC} C
inst_1 : HasZeroMorphisms.{uC', uC} C
inst_2 : HasBinaryBiproducts.{uC', uC} C
P Q : C
⊢ Eq (α := biprod.{uC', uC} P Q ⟶ biprod.{uC', uC} P Q)
    (CategoryStruct.comp (Y := biprod.{uC', uC} Q P)
        (Iso.hom (braiding P Q) : biprod.{uC', uC} P Q ⟶ biprod.{uC', uC} Q P)
        (Iso.hom (braiding Q P) : biprod.{uC', uC} Q P ⟶ biprod.{uC', uC} P Q) :
      biprod.{uC', uC} P Q ⟶ biprod.{uC', uC} P Q)
    (𝟙 (biprod.{uC', uC} P Q) : biprod.{uC', uC} P Q ⟶ biprod.{uC', uC} P Q)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
⊢ Eq.{v + 1} (α := W ⟶ W)
    ((fun (p : biprod.{v, u} W X ⟶ biprod.{v, u} W X) ↦ biprod.inl ≫ p ≫ biprod.fst)
      (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.map f g) (inv (biprod.map f g))))
    ((fun (p : biprod.{v, u} W X ⟶ biprod.{v, u} W X) ↦ biprod.inl ≫ p ≫ biprod.fst) (𝟙 (biprod.{v, u} W X)))

Tactic:
have t := congrArg (fun p : W ⊞ X ⟶ W ⊞ X => biprod.inl ≫ p ≫ biprod.fst)
          (IsIso.hom_inv_id (biprod.map f g))
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
t :
  Eq.{v + 1} (α := W ⟶ W)
    ((fun (p : biprod.{v, u} W X ⟶ biprod.{v, u} W X) ↦ biprod.inl ≫ p ≫ biprod.fst)
      (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.map f g) (inv (biprod.map f g))))
    ((fun (p : biprod.{v, u} W X ⟶ biprod.{v, u} W X) ↦ biprod.inl ≫ p ≫ biprod.fst) (𝟙 (biprod.{v, u} W X)))
⊢ f ≫
      CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
        (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) biprod.fst) =
    CategoryStruct.comp (Y := biprod.{v, u} W X) biprod.inl biprod.fst

Tactic:
simp only [Category.id_comp, Category.assoc, biprod.inl_map_assoc] at t

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.inl_map_assoc, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
t :
  f ≫
      CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
        (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) biprod.fst) =
    CategoryStruct.comp (Y := biprod.{v, u} W X) biprod.inl biprod.fst
⊢ f ≫
      CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
        (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) biprod.fst) =
    𝟙 W

Tactic:
simp [t]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
⊢ Eq.{v + 1} (α := Y ⟶ Y)
    ((fun (p : biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) ↦ biprod.inl ≫ p ≫ biprod.fst)
      (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) (biprod.map f g)))
    ((fun (p : biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) ↦ biprod.inl ≫ p ≫ biprod.fst) (𝟙 (biprod.{v, u} Y Z)))

Tactic:
have t := congrArg (fun p : Y ⊞ Z ⟶ Y ⊞ Z => biprod.inl ≫ p ≫ biprod.fst)
          (IsIso.inv_hom_id (biprod.map f g))
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
t :
  Eq.{v + 1} (α := Y ⟶ Y)
    ((fun (p : biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) ↦ biprod.inl ≫ p ≫ biprod.fst)
      (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) (biprod.map f g)))
    ((fun (p : biprod.{v, u} Y Z ⟶ biprod.{v, u} Y Z) ↦ biprod.inl ≫ p ≫ biprod.fst) (𝟙 (biprod.{v, u} Y Z)))
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
      (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) (biprod.fst ≫ f)) =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl biprod.fst

Tactic:
simp only [Category.id_comp, Category.assoc, biprod.map_fst] at t

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.biprod.map_fst, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
t :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
      (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) (biprod.fst ≫ f)) =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl biprod.fst
simp :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
      (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) (biprod.fst ≫ f)) =
    𝟙 Y
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
        (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) biprod.fst) ≫
      f =
    𝟙 Y

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
t :
  CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
      (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) (biprod.fst ≫ f)) =
    CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl biprod.fst
⊢ CategoryStruct.comp (Y := biprod.{v, u} Y Z) biprod.inl
      (CategoryStruct.comp (Y := biprod.{v, u} W X) (inv (biprod.map f g)) (biprod.fst ≫ f)) =
    𝟙 Y

Tactic:
simp [t]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
rw :
  IsIso (X := biprod.{v, u} X W) (Y := biprod.{v, u} Z Y)
    (CategoryStruct.comp (Y := biprod.{v, u} W X)
        (Iso.hom (biprod.braiding X W) : biprod.{v, u} X W ⟶ biprod.{v, u} W X)
        (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.map f g : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z)
            (Iso.hom (biprod.braiding Y Z) : biprod.{v, u} Y Z ⟶ biprod.{v, u} Z Y) :
          biprod.{v, u} W X ⟶ biprod.{v, u} Z Y) :
      biprod.{v, u} X W ⟶ biprod.{v, u} Z Y)
⊢ IsIso (X := biprod.{v, u} X W) (Y := biprod.{v, u} Z Y) (biprod.map g f)

Tactic:
rw [← biprod.braiding_map_braiding]

Premises used: CategoryTheory.Limits.biprod.braiding_map_braiding
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasZeroMorphisms.{v, u} C
inst_2 : HasBinaryBiproducts.{v, u} C
W X Y Z : C
f : W ⟶ Y
g : X ⟶ Z
inst_3 : IsIso (X := biprod.{v, u} W X) (Y := biprod.{v, u} Y Z) (biprod.map f g)
⊢ IsIso (X := biprod.{v, u} X W) (Y := biprod.{v, u} Z Y)
    (CategoryStruct.comp (Y := biprod.{v, u} W X)
        (Iso.hom (biprod.braiding X W) : biprod.{v, u} X W ⟶ biprod.{v, u} W X)
        (CategoryStruct.comp (Y := biprod.{v, u} Y Z) (biprod.map f g : biprod.{v, u} W X ⟶ biprod.{v, u} Y Z)
            (Iso.hom (biprod.braiding Y Z) : biprod.{v, u} Y Z ⟶ biprod.{v, u} Z Y) :
          biprod.{v, u} W X ⟶ biprod.{v, u} Z Y) :
      biprod.{v, u} X W ⟶ biprod.{v, u} Z Y)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
j : WalkingPair
left :
  (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → WalkingPair) x with
          | WalkingPair.left => WalkingPair.right
          | WalkingPair.right => WalkingPair.left :
          WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → WalkingPair) x with
            | WalkingPair.left => WalkingPair.right
            | WalkingPair.right => WalkingPair.left :
            WalkingPair))
        WalkingPair.left) =
    WalkingPair.left
right :
  (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → WalkingPair) x with
          | WalkingPair.left => WalkingPair.right
          | WalkingPair.right => WalkingPair.left :
          WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → WalkingPair) x with
            | WalkingPair.left => WalkingPair.right
            | WalkingPair.right => WalkingPair.left :
            WalkingPair))
        WalkingPair.right) =
    WalkingPair.right
⊢ (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → WalkingPair) x with
          | WalkingPair.left => WalkingPair.right
          | WalkingPair.right => WalkingPair.left :
          WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → WalkingPair) x with
            | WalkingPair.left => WalkingPair.right
            | WalkingPair.right => WalkingPair.left :
            WalkingPair))
        j) =
    j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → WalkingPair) x with
          | left => right
          | right => left :
          WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → WalkingPair) x with
            | left => right
            | right => left :
            WalkingPair))
        left) =
    left

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → WalkingPair) x with
          | left => right
          | right => left :
          WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → WalkingPair) x with
            | left => right
            | right => left :
            WalkingPair))
        right) =
    right

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (swap : (a : WalkingPair) → WalkingPair) left = right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (swap : (a : WalkingPair) → WalkingPair) right = left

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (swap.symm : (a : WalkingPair) → WalkingPair) left = right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (swap.symm : (a : WalkingPair) → WalkingPair) right = left

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
j : WalkingPair
left :
  (fun (b : Bool) ↦
        (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b WalkingPair.right WalkingPair.left : WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → Bool) x with
            | WalkingPair.left => true
            | WalkingPair.right => false :
            Bool))
        WalkingPair.left) =
    WalkingPair.left
right :
  (fun (b : Bool) ↦
        (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b WalkingPair.right WalkingPair.left : WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → Bool) x with
            | WalkingPair.left => true
            | WalkingPair.right => false :
            Bool))
        WalkingPair.right) =
    WalkingPair.right
⊢ (fun (b : Bool) ↦
        (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b WalkingPair.right WalkingPair.left : WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → Bool) x with
            | WalkingPair.left => true
            | WalkingPair.right => false :
            Bool))
        j) =
    j

Tactic:
cases j
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (fun (b : Bool) ↦ (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b right left : WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → Bool) x with
            | left => true
            | right => false :
            Bool))
        left) =
    left

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (fun (b : Bool) ↦ (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b right left : WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → Bool) x with
            | left => true
            | right => false :
            Bool))
        right) =
    right

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
b : Bool
false :
  (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → Bool) x with
          | left => Bool.true
          | right => Bool.false :
          Bool))
      ((fun (b : Bool) ↦ (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b right left : WalkingPair)) Bool.false) =
    Bool.false
true :
  (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → Bool) x with
          | left => Bool.true
          | right => Bool.false :
          Bool))
      ((fun (b : Bool) ↦ (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b right left : WalkingPair)) Bool.true) =
    Bool.true
⊢ (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → Bool) x with
          | left => Bool.true
          | right => Bool.false :
          Bool))
      ((fun (b : Bool) ↦ (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b right left : WalkingPair)) b) =
    b

Tactic:
cases b
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → Bool) x with
          | left => true
          | right => false :
          Bool))
      ((fun (b : Bool) ↦ (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b right left : WalkingPair)) false) =
    false

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → Bool) x with
          | left => true
          | right => false :
          Bool))
      ((fun (b : Bool) ↦ (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b right left : WalkingPair)) true) =
    true

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (equivBool : (a : WalkingPair) → Bool) left = true

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (equivBool : (a : WalkingPair) → Bool) right = false

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (equivBool.symm : (a : Bool) → WalkingPair) true = left

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
⊢ (equivBool.symm : (a : Bool) → WalkingPair) false = right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
X Y : C
⊢ pairFunction X Y left = X

Tactic:
rfl

Premises used: CategoryTheory.Limits.pairFunction, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
X Y : C
⊢ pairFunction X Y right = Y

Tactic:
rfl

Premises used: CategoryTheory.Limits.pairFunction, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
⊢ Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair } = X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
⊢ Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair } = Y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} (Discrete WalkingPair) C
f : F.obj { as := left : Discrete WalkingPair } ⟶ G.obj { as := left }
g : F.obj { as := right : Discrete WalkingPair } ⟶ G.obj { as := right }
⊢ (mapPair f g).app { as := left } = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
F G : Functor.{0, v, 0, u} (Discrete WalkingPair) C
f : F.obj { as := left : Discrete WalkingPair } ⟶ G.obj { as := left }
g : F.obj { as := right : Discrete WalkingPair } ⟶ G.obj { as := right }
⊢ (mapPair f g).app { as := right } = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryFan.{v, u} X Y
⊢ s.π.app { as := left } = s.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryFan.{v, u} X Y
⊢ s.π.app { as := right } = s.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
c c' : BinaryFan.{v, u} A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
j : Discrete WalkingPair
left :
  Eq (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.left : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair A B) { as := WalkingPair.left : Discrete WalkingPair })
    (c.π.app { as := WalkingPair.left }) (e.hom ≫ c'.π.app { as := WalkingPair.left })
right :
  Eq (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := WalkingPair.right : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair A B) { as := WalkingPair.right : Discrete WalkingPair })
    (c.π.app { as := WalkingPair.right }) (e.hom ≫ c'.π.app { as := WalkingPair.right })
⊢ c.π.app j = e.hom ≫ c'.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
c c' : BinaryFan.{v, u} A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair A B) { as := left : Discrete WalkingPair })
    (c.π.app { as := left }) (e.hom ≫ c'.π.app { as := left })

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
c c' : BinaryFan.{v, u} A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := right : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair A B) { as := right : Discrete WalkingPair })
    (c.π.app { as := right }) (e.hom ≫ c'.π.app { as := right })

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
c c' : BinaryFan.{v, u} A B
e : c.pt ≅ c'.pt
h₁ : c.fst = e.hom ≫ c'.fst
h₂ : c.snd = e.hom ≫ c'.snd
⊢ (ext e h₁ h₂).hom.hom = e.hom

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryFan.{v, u} X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
t : Cone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair })
    ((fun (t : Cone.{0, v, 0, u} (pair X Y)) ↦ lift (fst t) (snd t)) t ≫ s.π.app { as := left : Discrete WalkingPair })
    (t.π.app { as := left })

Tactic:
hl₁ _ _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryFan.{v, u} X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
t : Cone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair })
    ((fun (t : Cone.{0, v, 0, u} (pair X Y)) ↦ lift (fst t) (snd t)) t ≫ s.π.app { as := left : Discrete WalkingPair })
    (t.π.app { as := left })

Tactic:
exact hl₁ _ _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryFan.{v, u} X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
t : Cone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
    ((fun (t : Cone.{0, v, 0, u} (pair X Y)) ↦ lift (fst t) (snd t)) t ≫ s.π.app { as := right : Discrete WalkingPair })
    (t.π.app { as := right })

Tactic:
hl₂ _ _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryFan.{v, u} X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
t : Cone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := t.pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
    ((fun (t : Cone.{0, v, 0, u} (pair X Y)) ↦ lift (fst t) (snd t)) t ≫ s.π.app { as := right : Discrete WalkingPair })
    (t.π.app { as := right })

Tactic:
exact hl₂ _ _