awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
j : WalkingPair
left :
  (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → WalkingPair) x with
          | WalkingPair.left => right
          | right => WalkingPair.left :
          WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → WalkingPair) x with
            | WalkingPair.left => right
            | right => WalkingPair.left :
            WalkingPair))
        WalkingPair.left) =
    WalkingPair.left
⊢ (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → WalkingPair) x with
          | WalkingPair.left => right
          | right => WalkingPair.left :
          WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → WalkingPair) x with
            | WalkingPair.left => right
            | right => WalkingPair.left :
            WalkingPair))
        j) =
    j
have right : (fun (x : WalkingPair) ↦
      (match (motive := WalkingPair → WalkingPair) x with
        | WalkingPair.left => right
        | right => WalkingPair.left :
        WalkingPair))
    ((fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → WalkingPair) x with
          | WalkingPair.left => right
          | right => WalkingPair.left :
          WalkingPair))
      right) =
  right
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
j : WalkingPair
⊢ (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))
        j) =
    j
have left : (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: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
j : WalkingPair
left :
  (fun (b : Bool) ↦ (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b right WalkingPair.left : WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → Bool) x with
            | WalkingPair.left => true
            | right => false :
            Bool))
        WalkingPair.left) =
    WalkingPair.left
⊢ (fun (b : Bool) ↦ (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b right WalkingPair.left : WalkingPair))
      ((fun (x : WalkingPair) ↦
          (match (motive := WalkingPair → Bool) x with
            | WalkingPair.left => true
            | right => false :
            Bool))
        j) =
    j
have right : (fun (b : Bool) ↦ (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b right WalkingPair.left : WalkingPair))
    ((fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → Bool) x with
          | WalkingPair.left => true
          | right => false :
          Bool))
      right) =
  right
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
b : Bool
⊢ (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)) b) =
    b
have false : (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: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
b : Bool
false :
  (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → Bool) x with
          | left => true
          | right => Bool.false :
          Bool))
      ((fun (b : Bool) ↦ (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b right left : WalkingPair)) Bool.false) =
    Bool.false
⊢ (fun (x : WalkingPair) ↦
        (match (motive := WalkingPair → Bool) x with
          | left => true
          | right => Bool.false :
          Bool))
      ((fun (b : Bool) ↦ (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b right left : WalkingPair)) b) =
    b
have true : (fun (x : WalkingPair) ↦
      (match (motive := WalkingPair → Bool) x with
        | left => true
        | right => Bool.false :
        Bool))
    ((fun (b : Bool) ↦ (Bool.recOn (motive := fun (x : Bool) ↦ WalkingPair) b right left : WalkingPair)) true) =
  true
Tactic: cases b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ c.π.app j = e.hom ≫ c'.π.app j
have left : 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: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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 })
⊢ c.π.app j = e.hom ≫ c'.π.app j
have right : 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: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ c.ι.app j ≫ e.hom = c'.ι.app j
have left : 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: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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 })
⊢ c.ι.app j ≫ e.hom = c'.ι.app j
have right : 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: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ 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 })
have left : 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: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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 })
⊢ 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 })
have right : 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: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ 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 })
have left : 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: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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 })
⊢ 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 })
have right : 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: cases l
Cleared hypotheses: l
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ lift s ≫ (mk fst snd).π.app j = s.π.app j
have left : 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: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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 })
⊢ lift s ≫ (mk fst snd).π.app j = s.π.app j
have right : 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: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ (mk inl inr).ι.app j ≫ desc s = s.ι.app j
have left : 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: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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 })
⊢ (mk inl inr).ι.app j ≫ desc s = s.ι.app j
have right : 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: rcases j with ⟨⟨⟩⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsTerminal.{v, u} Y
c : BinaryFan.{v, u} X Y
⊢ Nonempty (IsLimit c) ↔ IsIso c.fst
have mp : Nonempty (IsLimit c) → IsIso c.fst
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ Nonempty (IsLimit c) ↔ IsIso c.fst
have mpr : IsIso c.fst → Nonempty (IsLimit c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
⊢ IsIso c.fst
have mp : ∀ (l : X ⟶ c.pt) (hl : l ≫ c.fst = 𝟙 X), IsIso c.fst
Tactic: obtain ⟨l, hl, -⟩ := BinaryFan.IsLimit.lift' H (𝟙 X) (h.from X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
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
have refine : Nonempty (IsLimit c) ↔ Nonempty (IsLimit (mk c.snd c.fst))
Tactic: refine Iff.trans ?_ (BinaryFan.isLimit_iff_isIso_fst h (BinaryFan.mk c.snd c.fst))
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryFan.{v, u} X Y
f : X ⟶ X'
inst_1 : IsIso f
h : IsLimit c
⊢ IsLimit (mk (c.fst ≫ f) c.snd)
have lift : (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })) →
  s.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair }
Tactic: fapply BinaryFan.isLimitMk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryFan.{v, u} X Y
f : X ⟶ X'
inst_1 : IsIso f
h : IsLimit c
lift :
  (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })) →
    s.pt ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair }
⊢ IsLimit (mk (c.fst ≫ f) c.snd)
have fac_left : ∀ (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
  IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst ≫ f = s.fst
Tactic: fapply BinaryFan.isLimitMk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryFan.{v, u} X Y
f : X ⟶ X'
inst_1 : IsIso f
h : IsLimit c
lift :
  (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })) →
    s.pt ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair }
fac_left :
  ∀ (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst ≫ f = s.fst
⊢ IsLimit (mk (c.fst ≫ f) c.snd)
have fac_right : ∀ (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
  IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd = s.snd
Tactic: fapply BinaryFan.isLimitMk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryFan.{v, u} X Y
f : X ⟶ X'
inst_1 : IsIso f
h : IsLimit c
lift :
  (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })) →
    s.pt ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair }
fac_left :
  ∀ (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst ≫ f = s.fst
fac_right :
  ∀ (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })),
    IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd = s.snd
⊢ IsLimit (mk (c.fst ≫ f) c.snd)
have uniq : ∀ (s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair }))
  (m :
    s.pt ⟶
      Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair }),
  m ≫ c.fst ≫ f = s.fst → m ≫ c.snd = s.snd → m = IsLimit.lift h (s.fst ≫ inv f) s.snd
Tactic: fapply BinaryFan.isLimitMk
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryFan.{v, u} X Y
f : X ⟶ X'
inst_1 : IsIso f
h : IsLimit c
s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
m :
  s.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
⊢ m = IsLimit.lift h (s.fst ≫ inv f) s.snd
have uniq : m ≫ c.fst = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst
Tactic: apply BinaryFan.IsLimit.hom_ext h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y_1 X Y X' : C
c : BinaryFan.{v, u} X Y
f : X ⟶ X'
inst_1 : IsIso f
h : IsLimit c
s : BinaryFan.{v, u} X' (Functor.obj.{0, v, 0, u} (pair X Y) { as := right : Discrete WalkingPair })
m :
  s.pt ⟶
    Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
      { as := left : Discrete WalkingPair }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
uniq : m ≫ c.fst = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst
⊢ m = IsLimit.lift h (s.fst ≫ inv f) s.snd
have uniq₁ : m ≫ c.snd = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd
Tactic: apply BinaryFan.IsLimit.hom_ext h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
⊢ Nonempty (IsColimit c) ↔ IsIso c.inl
have mp : Nonempty (IsColimit c) → IsIso c.inl
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
mp : Nonempty (IsColimit c) → IsIso c.inl
⊢ Nonempty (IsColimit c) ↔ IsIso c.inl
have mpr : IsIso c.inl → Nonempty (IsColimit c)
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
H : IsColimit c
⊢ IsIso c.inl
have mp : ∀ (l : c.pt ⟶ X) (hl : c.inl ≫ l = 𝟙 X), IsIso c.inl
Tactic: obtain ⟨l, hl, -⟩ := BinaryCofan.IsColimit.desc' H (𝟙 X) (h.to X)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
⊢ IsIso c.inl
have mp : c.inl ≫ l ≫ c.inl =
  c.inl ≫
    𝟙
      (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
        { as := left : Discrete WalkingPair })
Tactic: refine ⟨⟨l, hl, BinaryCofan.IsColimit.hom_ext H (?_) (h.hom_ext _ _)⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
⊢ c.inl ≫ l ≫ c.inl =
    c.inl ≫
      𝟙
        (Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const (Discrete WalkingPair)) c.pt)
          { as := left : Discrete WalkingPair })
have mp : c.inl ≫ l ≫ c.inl = c.inl
Tactic: rw [Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
⊢ c.inl ≫ l ≫ c.inl = c.inl
have e : (c.inl ≫ l) ≫ c.inl = 𝟙 X ≫ c.inl
Tactic: have e : (inl c ≫ l) ≫ inl c = 𝟙 X ≫ inl c := congrArg (· ≫ inl c) hl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
h : IsInitial.{v, u} Y
c : BinaryCofan.{v, u} X Y
H : IsColimit c
l : c.pt ⟶ X
hl : c.inl ≫ l = 𝟙 X
e : (c.inl ≫ l) ≫ c.inl = 𝟙 X ≫ c.inl
⊢ c.inl ≫ l ≫ c.inl = c.inl
have mp : ∀ (e : c.inl ≫ l ≫ c.inl = 𝟙 X ≫ c.inl), c.inl ≫ l ≫ c.inl = c.inl
Tactic: rwa [Category.assoc, Category.id_comp] at e
Cleared hypotheses: e