awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y : C
s : BinaryFan.{v, u} X Y
h : IsLimit s
f g : W ⟶ s.pt
h₁ : f ≫ s.fst = g ≫ s.fst
h₂ : f ≫ s.snd = g ≫ s.snd
⊢ f = g

Tactic:
h.hom_ext fun j => Discrete.recOn j fun j => WalkingPair.casesOn j h₁ h₂

Premises used: CategoryTheory.Discrete.recOn, CategoryTheory.Limits.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
A B : C
c c' : BinaryCofan.{v, u} A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
j : Discrete WalkingPair
left :
  Eq (α := Functor.obj.{0, v, 0, u} (pair A B) { as := WalkingPair.left : Discrete WalkingPair } ⟶ c'.pt)
    (c.ι.app { as := WalkingPair.left } ≫ e.hom) (c'.ι.app { as := WalkingPair.left })
right :
  Eq (α := Functor.obj.{0, v, 0, u} (pair A B) { as := WalkingPair.right : Discrete WalkingPair } ⟶ c'.pt)
    (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' : BinaryCofan.{v, u} A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair A B) { as := left : Discrete WalkingPair } ⟶ c'.pt)
    (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' : BinaryCofan.{v, u} A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair A B) { as := right : Discrete WalkingPair } ⟶ c'.pt)
    (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' : BinaryCofan.{v, u} A B
e : c.pt ≅ c'.pt
h₁ : c.inl ≫ e.hom = c'.inl
h₂ : c.inr ≫ e.hom = c'.inr
⊢ (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 : BinaryCofan.{v, u} X Y
⊢ s.ι.app { as := left } = s.inl

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryCofan.{v, u} X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair } ⟶ t.pt)
    (s.ι.app { as := left : Discrete WalkingPair } ≫
      (fun (t : Cocone.{0, v, 0, u} (pair X Y)) ↦ desc (inl t) (inr t)) t)
    (t.ι.app { as := left })

Tactic:
hd₁ _ _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryCofan.{v, u} X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair } ⟶ t.pt)
    (s.ι.app { as := left : Discrete WalkingPair } ≫
      (fun (t : Cocone.{0, v, 0, u} (pair X Y)) ↦ desc (inl t) (inr t)) t)
    (t.ι.app { as := left })

Tactic:
exact hd₁ _ _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryCofan.{v, u} X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair } ⟶ t.pt)
    (s.ι.app { as := right : Discrete WalkingPair } ≫
      (fun (t : Cocone.{0, v, 0, u} (pair X Y)) ↦ desc (inl t) (inr t)) t)
    (t.ι.app { as := right })

Tactic:
hd₂ _ _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
s : BinaryCofan.{v, u} X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair } ⟶ t.pt)
    (s.ι.app { as := right : Discrete WalkingPair } ≫
      (fun (t : Cocone.{0, v, 0, u} (pair X Y)) ↦ desc (inl t) (inr t)) t)
    (t.ι.app { as := right })

Tactic:
exact hd₂ _ _
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
W X Y : C
s : BinaryCofan.{v, u} X Y
h : IsColimit s
f g : s.pt ⟶ W
h₁ : s.inl ≫ f = s.inl ≫ g
h₂ : s.inr ≫ f = s.inr ≫ g
⊢ f = g

Tactic:
h.hom_ext fun j => Discrete.recOn j fun j => WalkingPair.casesOn j h₁ h₂

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.Discrete.recOn
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y P : C
π₁ : P ⟶ X
π₂ : P ⟶ Y
⊢ (mk π₁ π₂).fst = π₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y P : C
π₁ : P ⟶ X
π₂ : P ⟶ Y
⊢ (mk π₁ π₂).snd = π₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y P : C
ι₁ : X ⟶ P
ι₂ : Y ⟶ P
⊢ (mk ι₁ ι₂).inl = ι₁

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y P : C
ι₁ : X ⟶ P
ι₂ : Y ⟶ P
⊢ (mk ι₁ ι₂).inr = ι₂

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
c : BinaryFan.{v, u} X Y
x : Discrete WalkingPair
l : 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 X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (c.π.app { as := WalkingPair.left })
    (Iso.hom (Iso.refl c.pt) ≫ (BinaryFan.mk c.fst c.snd).π.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 X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (c.π.app { as := WalkingPair.right })
    (Iso.hom (Iso.refl c.pt) ≫ (BinaryFan.mk c.fst c.snd).π.app { as := WalkingPair.right })
⊢ Eq (α :=
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := l : Discrete WalkingPair } ⟶
      Functor.obj.{0, v, 0, u} (pair X Y) { as := l : Discrete WalkingPair })
    (c.π.app { as := l }) (Iso.hom (Iso.refl c.pt) ≫ (BinaryFan.mk c.fst c.snd).π.app { as := l })

Tactic:
cases l
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
c : BinaryFan.{v, u} X Y
x : Discrete WalkingPair
⊢ 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 X Y) { as := left : Discrete WalkingPair })
    (c.π.app { as := left }) (Iso.hom (Iso.refl c.pt) ≫ (BinaryFan.mk c.fst c.snd).π.app { as := left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
c : BinaryFan.{v, u} X Y
x : Discrete WalkingPair
⊢ 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 X Y) { as := right : Discrete WalkingPair })
    (c.π.app { as := right }) (Iso.hom (Iso.refl c.pt) ≫ (BinaryFan.mk c.fst c.snd).π.app { as := right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
c : BinaryFan.{v, u} X Y
x : Discrete WalkingPair
⊢ 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 X Y) { as := left : Discrete WalkingPair })
    (c.π.app { as := left }) (Iso.hom (Iso.refl c.pt) ≫ (BinaryFan.mk c.fst c.snd).π.app { as := left })

Tactic:
repeat simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
c : BinaryCofan.{v, u} X Y
x : Discrete WalkingPair
l : WalkingPair
left :
  Eq (α :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶
      (BinaryCofan.mk c.inl c.inr).pt)
    (c.ι.app { as := WalkingPair.left : Discrete WalkingPair } ≫ Iso.hom (Iso.refl c.pt))
    ((BinaryCofan.mk c.inl c.inr).ι.app { as := WalkingPair.left })
right :
  Eq (α :=
    Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶
      (BinaryCofan.mk c.inl c.inr).pt)
    (c.ι.app { as := WalkingPair.right : Discrete WalkingPair } ≫ Iso.hom (Iso.refl c.pt))
    ((BinaryCofan.mk c.inl c.inr).ι.app { as := WalkingPair.right })
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := l : Discrete WalkingPair } ⟶ (BinaryCofan.mk c.inl c.inr).pt)
    (c.ι.app { as := l : Discrete WalkingPair } ≫ Iso.hom (Iso.refl c.pt))
    ((BinaryCofan.mk c.inl c.inr).ι.app { as := l })

Tactic:
cases l
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
c : BinaryCofan.{v, u} X Y
x : Discrete WalkingPair
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair } ⟶ (BinaryCofan.mk c.inl c.inr).pt)
    (c.ι.app { as := left : Discrete WalkingPair } ≫ Iso.hom (Iso.refl c.pt))
    ((BinaryCofan.mk c.inl c.inr).ι.app { as := left })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
c : BinaryCofan.{v, u} X Y
x : Discrete WalkingPair
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair } ⟶ (BinaryCofan.mk c.inl c.inr).pt)
    (c.ι.app { as := right : Discrete WalkingPair } ≫ Iso.hom (Iso.refl c.pt))
    ((BinaryCofan.mk c.inl c.inr).ι.app { as := right })

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y : C
c : BinaryCofan.{v, u} X Y
x : Discrete WalkingPair
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair } ⟶ (BinaryCofan.mk c.inl c.inr).pt)
    (c.ι.app { as := left : Discrete WalkingPair } ≫ Iso.hom (Iso.refl c.pt))
    ((BinaryCofan.mk c.inl c.inr).ι.app { as := left })

Tactic:
repeat simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
fst : W ⟶ X
snd : W ⟶ Y
lift : (s : BinaryFan.{v, u} X Y) → s.pt ⟶ W
fac_left : ∀ (s : BinaryFan.{v, u} X Y), lift s ≫ fst = s.fst
fac_right : ∀ (s : BinaryFan.{v, u} X Y), lift s ≫ snd = s.snd
uniq : ∀ (s : BinaryFan.{v, u} X Y) (m : s.pt ⟶ W), m ≫ fst = s.fst → m ≫ snd = s.snd → m = lift s
s : Cone.{0, v, 0, u} (pair X Y)
j : Discrete WalkingPair
left :
  Eq (α := s.pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair })
    (lift s ≫ (mk fst snd).π.app { as := WalkingPair.left }) (s.π.app { as := WalkingPair.left })
right :
  Eq (α := s.pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair })
    (lift s ≫ (mk fst snd).π.app { as := WalkingPair.right }) (s.π.app { as := WalkingPair.right })
⊢ lift s ≫ (mk fst snd).π.app j = s.π.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
fst : W ⟶ X
snd : W ⟶ Y
lift : (s : BinaryFan.{v, u} X Y) → s.pt ⟶ W
fac_left : ∀ (s : BinaryFan.{v, u} X Y), lift s ≫ fst = s.fst
fac_right : ∀ (s : BinaryFan.{v, u} X Y), lift s ≫ snd = s.snd
uniq : ∀ (s : BinaryFan.{v, u} X Y) (m : s.pt ⟶ W), m ≫ fst = s.fst → m ≫ snd = s.snd → m = lift s
s : Cone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := s.pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair })
    (lift s ≫ (mk fst snd).π.app { as := left }) (s.π.app { as := left })

Tactic:
fac_left s
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
fst : W ⟶ X
snd : W ⟶ Y
lift : (s : BinaryFan.{v, u} X Y) → s.pt ⟶ W
fac_left : ∀ (s : BinaryFan.{v, u} X Y), lift s ≫ fst = s.fst
fac_right : ∀ (s : BinaryFan.{v, u} X Y), lift s ≫ snd = s.snd
uniq : ∀ (s : BinaryFan.{v, u} X Y) (m : s.pt ⟶ W), m ≫ fst = s.fst → m ≫ snd = s.snd → m = lift s
s : Cone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := s.pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
    (lift s ≫ (mk fst snd).π.app { as := right }) (s.π.app { as := right })

Tactic:
fac_right s
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
fst : W ⟶ X
snd : W ⟶ Y
lift : (s : BinaryFan.{v, u} X Y) → s.pt ⟶ W
fac_left : ∀ (s : BinaryFan.{v, u} X Y), lift s ≫ fst = s.fst
fac_right : ∀ (s : BinaryFan.{v, u} X Y), lift s ≫ snd = s.snd
uniq : ∀ (s : BinaryFan.{v, u} X Y) (m : s.pt ⟶ W), m ≫ fst = s.fst → m ≫ snd = s.snd → m = lift s
s : Cone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := s.pt ⟶ Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair })
    (lift s ≫ (mk fst snd).π.app { as := left }) (s.π.app { as := left })

Tactic:
exacts [fac_left s, fac_right s]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
inl : X ⟶ W
inr : Y ⟶ W
desc : (s : BinaryCofan.{v, u} X Y) → W ⟶ s.pt
fac_left : ∀ (s : BinaryCofan.{v, u} X Y), inl ≫ desc s = s.inl
fac_right : ∀ (s : BinaryCofan.{v, u} X Y), inr ≫ desc s = s.inr
uniq : ∀ (s : BinaryCofan.{v, u} X Y) (m : W ⟶ s.pt), inl ≫ m = s.inl → inr ≫ m = s.inr → m = desc s
s : Cocone.{0, v, 0, u} (pair X Y)
j : Discrete WalkingPair
left :
  Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.left : Discrete WalkingPair } ⟶ s.pt)
    ((mk inl inr).ι.app { as := WalkingPair.left } ≫ desc s) (s.ι.app { as := WalkingPair.left })
right :
  Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := WalkingPair.right : Discrete WalkingPair } ⟶ s.pt)
    ((mk inl inr).ι.app { as := WalkingPair.right } ≫ desc s) (s.ι.app { as := WalkingPair.right })
⊢ (mk inl inr).ι.app j ≫ desc s = s.ι.app j

Tactic:
rcases j with ⟨⟨⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
inl : X ⟶ W
inr : Y ⟶ W
desc : (s : BinaryCofan.{v, u} X Y) → W ⟶ s.pt
fac_left : ∀ (s : BinaryCofan.{v, u} X Y), inl ≫ desc s = s.inl
fac_right : ∀ (s : BinaryCofan.{v, u} X Y), inr ≫ desc s = s.inr
uniq : ∀ (s : BinaryCofan.{v, u} X Y) (m : W ⟶ s.pt), inl ≫ m = s.inl → inr ≫ m = s.inr → m = desc s
s : Cocone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair } ⟶ s.pt)
    ((mk inl inr).ι.app { as := left } ≫ desc s) (s.ι.app { as := left })

Tactic:
fac_left s
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
inl : X ⟶ W
inr : Y ⟶ W
desc : (s : BinaryCofan.{v, u} X Y) → W ⟶ s.pt
fac_left : ∀ (s : BinaryCofan.{v, u} X Y), inl ≫ desc s = s.inl
fac_right : ∀ (s : BinaryCofan.{v, u} X Y), inr ≫ desc s = s.inr
uniq : ∀ (s : BinaryCofan.{v, u} X Y) (m : W ⟶ s.pt), inl ≫ m = s.inl → inr ≫ m = s.inr → m = desc s
s : Cocone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair } ⟶ s.pt)
    ((mk inl inr).ι.app { as := right } ≫ desc s) (s.ι.app { as := right })

Tactic:
fac_right s
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
inl : X ⟶ W
inr : Y ⟶ W
desc : (s : BinaryCofan.{v, u} X Y) → W ⟶ s.pt
fac_left : ∀ (s : BinaryCofan.{v, u} X Y), inl ≫ desc s = s.inl
fac_right : ∀ (s : BinaryCofan.{v, u} X Y), inr ≫ desc s = s.inr
uniq : ∀ (s : BinaryCofan.{v, u} X Y) (m : W ⟶ s.pt), inl ≫ m = s.inl → inr ≫ m = s.inr → m = desc s
s : Cocone.{0, v, 0, u} (pair X Y)
⊢ Eq (α := Functor.obj.{0, v, 0, u} (pair X Y) { as := left : Discrete WalkingPair } ⟶ s.pt)
    ((mk inl inr).ι.app { as := left } ≫ desc s) (s.ι.app { as := left })

Tactic:
exacts [fac_left s, fac_right s]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
s : BinaryFan.{v, u} X Y
h : IsLimit s
f : W ⟶ X
g : W ⟶ Y
⊢ lift h f g ≫ s.fst = f

Tactic:
h.fac (BinaryFan.mk f g) _

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift, CategoryTheory.Limits.BinaryFan.mk, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
s : BinaryFan.{v, u} X Y
h : IsLimit s
f : W ⟶ X
g : W ⟶ Y
⊢ lift h f g ≫ s.snd = g

Tactic:
h.fac (BinaryFan.mk f g) _

Premises used: CategoryTheory.Limits.BinaryFan.IsLimit.lift, CategoryTheory.Limits.BinaryFan.mk, CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
s : BinaryCofan.{v, u} X Y
h : IsColimit s
f : X ⟶ W
g : Y ⟶ W
⊢ s.inl ≫ desc h f g = f

Tactic:
h.fac (BinaryCofan.mk f g) _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.BinaryCofan.IsColimit.desc, CategoryTheory.Limits.BinaryCofan.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y W : C
s : BinaryCofan.{v, u} X Y
h : IsColimit s
f : X ⟶ W
g : Y ⟶ W
⊢ s.inr ≫ desc h f g = g

Tactic:
h.fac (BinaryCofan.mk f g) _

Premises used: CategoryTheory.Limits.IsColimit.fac, CategoryTheory.Limits.BinaryCofan.IsColimit.desc, CategoryTheory.Limits.BinaryCofan.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsTerminal.{v, u} Y
c : BinaryFan.{v, u} X Y
mp : Nonempty (IsLimit c) → IsIso c.fst
mpr : IsIso c.fst → Nonempty (IsLimit c)
⊢ Nonempty (IsLimit c) ↔ IsIso c.fst

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsTerminal.{v, u} Y
c : BinaryFan.{v, u} X Y
H : IsLimit c
mp : ∀ (l : X ⟶ c.pt) (hl : l ≫ c.fst = 𝟙 X), IsIso c.fst
⊢ IsIso c.fst

Tactic:
obtain ⟨l, hl, -⟩ := BinaryFan.IsLimit.lift' H (𝟙 X) (h.from X)

Premises used: CategoryTheory.Limits.IsTerminal.from, CategoryTheory.CategoryStruct.id, CategoryTheory.Limits.BinaryFan.IsLimit.lift'
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsTerminal.{v, u} Y
c : BinaryFan.{v, u} X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ c.fst = 𝟙 X
⊢ (c.fst ≫ l) ≫ c.fst =
    𝟙
        (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
          { as := left : Discrete WalkingPair }) ≫
      c.fst

Tactic:
simpa [hl, -Category.comp_id] using Category.comp_id _

Premises used: CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsTerminal.{v, u} Y
c : BinaryFan.{v, u} X Y
H : IsLimit c
l : X ⟶ c.pt
hl : l ≫ c.fst = 𝟙 X
⊢ IsIso c.fst

Tactic:
exact
      ⟨⟨l,
          BinaryFan.IsLimit.hom_ext H (by simpa [hl, -Category.comp_id] using Category.comp_id _)
            (h.hom_ext _ _),
          hl⟩⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsTerminal.{v, u} Y
c : BinaryFan.{v, u} X Y
h_1 : IsIso c.fst
T : C
x : T ⟶ X
x_1 : T ⟶ Y
⊢ (fun {T : C} (f : T ⟶ X) (x : T ⟶ Y) ↦ f ≫ inv c.fst) x x_1 ≫ c.fst = x

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsTerminal.{v, u} Y
c : BinaryFan.{v, u} X Y
h_1 : IsIso c.fst
T : C
x : T ⟶ X
x_1 : T ⟶ Y
x_2 : T ⟶ c.pt
e : x_2 ≫ c.fst = x
h_2 : x_2 ≫ c.snd = x_1
⊢ x_2 = (fun {T : C} (f : T ⟶ X) (x : T ⟶ Y) ↦ f ≫ inv c.fst) x x_1

Tactic:
simp [← e]
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsTerminal.{v, u} Y
c : BinaryFan.{v, u} X Y
h_1 : IsIso c.fst
⊢ Nonempty (IsLimit c)

Tactic:
exact
      ⟨BinaryFan.IsLimit.mk _ (fun f _ => f ≫ inv c.fst) (fun _ _ => by simp)
          (fun _ _ => h.hom_ext _ _) fun _ _ _ e _ => by simp [← e]⟩
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsTerminal.{v, u} X
c : BinaryFan.{v, u} X Y
⊢ Nonempty (IsLimit c) ↔ IsIso c.snd

Tactic:
Iff.trans ?_ (BinaryFan.isLimit_iff_isIso_fst h (BinaryFan.mk c.snd c.fst))

Premises used: CategoryTheory.Limits.BinaryFan.fst, CategoryTheory.Limits.BinaryFan.mk, CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst, Iff.trans, CategoryTheory.Limits.BinaryFan.snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsTerminal.{v, u} X
c : BinaryFan.{v, u} X Y
refine : Nonempty (IsLimit c) ↔ Nonempty (IsLimit (mk c.snd c.fst))
⊢ Nonempty (IsLimit c) ↔ IsIso c.snd

Tactic:
refine Iff.trans ?_ (BinaryFan.isLimit_iff_isIso_fst h (BinaryFan.mk c.snd c.fst))

Premises used: CategoryTheory.Limits.BinaryFan.fst, CategoryTheory.Limits.BinaryFan.mk, CategoryTheory.Limits.BinaryFan.isLimit_iff_isIso_fst, Iff.trans, CategoryTheory.Limits.BinaryFan.snd
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsTerminal.{v, u} X
c : BinaryFan.{v, u} X Y
⊢ Nonempty (IsLimit c) ↔ Nonempty (IsLimit (mk c.snd c.fst))

Tactic:
⟨fun h => ⟨BinaryFan.isLimitFlip h.some⟩, fun h =>
      ⟨(BinaryFan.isLimitFlip h.some).ofIsoLimit (isoBinaryFanMk c).symm⟩⟩

Premises used: Nonempty.some, Nonempty.intro, CategoryTheory.Limits.isoBinaryFanMk, Iff.intro, CategoryTheory.Iso.symm, CategoryTheory.Limits.BinaryFan.isLimitFlip, CategoryTheory.Limits.IsLimit.ofIsoLimit
-- Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsTerminal.{v, u} X
c : BinaryFan.{v, u} X Y
⊢ Nonempty (IsLimit c) ↔ Nonempty (IsLimit (mk c.snd c.fst))

Tactic:
exact
    ⟨fun h => ⟨BinaryFan.isLimitFlip h.some⟩, fun h =>
      ⟨(BinaryFan.isLimitFlip h.some).ofIsoLimit (isoBinaryFanMk c).symm⟩⟩