awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
f : op one ⟶ op zero
g : unop (op zero) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op zero))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op zero)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op one)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
have op : Eq (α :=
  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one) ⟶ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op zero))
  (CategoryStruct.comp (Y := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op left))
    (Iso.hom
      ((fun (j : WalkingParallelPairᵒᵖ) ↦
          (eqToIso sorry :
            (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
        (op zero))))
  (CategoryStruct.comp (Y := Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op one))
    (Iso.hom
      ((fun (j : WalkingParallelPairᵒᵖ) ↦
          (eqToIso sorry :
            (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
        (op one)))
    (Functor.map (𝟭 WalkingParallelPairᵒᵖ) (Quiver.Hom.op left)))
Tactic: cases g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
f : Opposite.op one ⟶ Opposite.op zero
g : unop (Opposite.op zero) ⟶ unop (Opposite.op one) := f.unop
this : f = g.op
op :
  Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op zero))
    (CategoryStruct.comp (Y := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op left))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op zero))))
    (CategoryStruct.comp (Y := Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op one))
      (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op one)))
      (Functor.map (𝟭 WalkingParallelPairᵒᵖ) (Quiver.Hom.op left)))
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op zero))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op zero)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op one)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
have op₁ : Eq (α :=
  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) ⟶
    Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op zero))
  (CategoryStruct.comp (Y := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map (Quiver.Hom.op right))
    (Iso.hom
      ((fun (j : WalkingParallelPairᵒᵖ) ↦
          (eqToIso sorry :
            (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
        (Opposite.op zero))))
  (CategoryStruct.comp (Y := Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op one))
    (Iso.hom
      ((fun (j : WalkingParallelPairᵒᵖ) ↦
          (eqToIso sorry :
            (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
        (Opposite.op one)))
    (Functor.map (𝟭 WalkingParallelPairᵒᵖ) (Quiver.Hom.op right)))
Tactic: cases g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
f : op one ⟶ op one
g : unop (op one) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op one))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op one)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op one)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
have op : Eq (α :=
  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one) ⟶ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op one))
  (CategoryStruct.comp (Y := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map
      (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op one)))))
    (Iso.hom
      ((fun (j : WalkingParallelPairᵒᵖ) ↦
          (eqToIso sorry :
            (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
        (op one))))
  (CategoryStruct.comp (Y := Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op one))
    (Iso.hom
      ((fun (j : WalkingParallelPairᵒᵖ) ↦
          (eqToIso sorry :
            (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
        (op one)))
    (Functor.map (𝟭 WalkingParallelPairᵒᵖ) (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op one))))))
Tactic: cases g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
j : WalkingParallelPair
⊢ walkingParallelPairOp.map
        ((NatIso.ofComponents (fun (j : WalkingParallelPair) ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app
          j) ≫
      NatTrans.app (Iso.hom (NatIso.ofComponents (fun (j : WalkingParallelPairᵒᵖ) ↦ eqToIso ⋯) ⋯))
        (walkingParallelPairOp.obj j) =
    𝟙 (walkingParallelPairOp.obj j)
have zero : walkingParallelPairOp.map
      ((NatIso.ofComponents (fun (j : WalkingParallelPair) ↦ eqToIso sorry) @walkingParallelPairOpEquiv._proof_2).hom.app
        zero) ≫
    NatTrans.app (Iso.hom (NatIso.ofComponents (fun (j : WalkingParallelPairᵒᵖ) ↦ eqToIso sorry) sorry))
      (walkingParallelPairOp.obj zero) =
  𝟙 (walkingParallelPairOp.obj zero)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
j : WalkingParallelPair
zero :
  walkingParallelPairOp.map
        ((NatIso.ofComponents (fun (j : WalkingParallelPair) ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app
          WalkingParallelPair.zero) ≫
      NatTrans.app (Iso.hom (NatIso.ofComponents (fun (j : WalkingParallelPairᵒᵖ) ↦ eqToIso ⋯) ⋯))
        (walkingParallelPairOp.obj WalkingParallelPair.zero) =
    𝟙 (walkingParallelPairOp.obj WalkingParallelPair.zero)
⊢ walkingParallelPairOp.map
        ((NatIso.ofComponents (fun (j : WalkingParallelPair) ↦ eqToIso ⋯) @walkingParallelPairOpEquiv._proof_2).hom.app
          j) ≫
      NatTrans.app (Iso.hom (NatIso.ofComponents (fun (j : WalkingParallelPairᵒᵖ) ↦ eqToIso ⋯) ⋯))
        (walkingParallelPairOp.obj j) =
    𝟙 (walkingParallelPairOp.obj j)
have one : walkingParallelPairOp.map
      ((NatIso.ofComponents (fun (j : WalkingParallelPair) ↦ eqToIso sorry) @walkingParallelPairOpEquiv._proof_2).hom.app
        one) ≫
    NatTrans.app (Iso.hom (NatIso.ofComponents (fun (j : WalkingParallelPairᵒᵖ) ↦ eqToIso sorry) sorry))
      (walkingParallelPairOp.obj one) =
  𝟙 (walkingParallelPairOp.obj one)
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
j : WalkingParallelPair
⊢ (parallelPair (F.map left) (F.map right)).obj j = F.obj j
have zero : (parallelPair (F.map left) (F.map right)).obj zero = F.obj zero
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingParallelPair C
j : WalkingParallelPair
zero : (parallelPair (F.map left) (F.map right)).obj WalkingParallelPair.zero = F.obj WalkingParallelPair.zero
⊢ (parallelPair (F.map left) (F.map right)).obj j = F.obj j
have one : (parallelPair (F.map left) (F.map right)).obj one = F.obj one
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F : Functor.{0, v, 0, u} WalkingParallelPair C
j : WalkingParallelPair
⊢ F.obj j = (parallelPair (F.map left) (F.map right)).obj j
have zero : F.obj zero = (parallelPair (F.map left) (F.map right)).obj zero
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
F : Functor.{0, v, 0, u} WalkingParallelPair C
j : WalkingParallelPair
zero : F.obj WalkingParallelPair.zero = (parallelPair (F.map left) (F.map right)).obj WalkingParallelPair.zero
⊢ F.obj j = (parallelPair (F.map left) (F.map right)).obj j
have one : F.obj one = (parallelPair (F.map left) (F.map right)).obj one
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
⊢ s.π.app one = s.ι ≫ f
have rw : s.π.app one = s.π.app zero ≫ f
Tactic: rw [← s.app_zero_eq_ι, ← s.w left, parallelPair_map_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
rw : s.π.app one = s.π.app zero ≫ f
⊢ s.π.app one = s.ι ≫ f
have rw₁ : s.π.app zero ≫ (parallelPair f g).map left = s.π.app zero ≫ f
Tactic: rw [← s.app_zero_eq_ι, ← s.w left, parallelPair_map_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
rw : s.π.app one = s.π.app zero ≫ f
rw₁ : s.π.app zero ≫ (parallelPair f g).map left = s.π.app zero ≫ f
⊢ s.π.app one = s.ι ≫ f
have rw₂ : s.π.app zero ≫ f = s.π.app zero ≫ f
Tactic: rw [← s.app_zero_eq_ι, ← s.w left, parallelPair_map_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
⊢ s.π.app one = s.ι ≫ g
have rw : s.π.app one = s.π.app zero ≫ g
Tactic: rw [← s.app_zero_eq_ι, ← s.w right, parallelPair_map_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
rw : s.π.app one = s.π.app zero ≫ g
⊢ s.π.app one = s.ι ≫ g
have rw₁ : s.π.app zero ≫ (parallelPair f g).map right = s.π.app zero ≫ g
Tactic: rw [← s.app_zero_eq_ι, ← s.w right, parallelPair_map_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
rw : s.π.app one = s.π.app zero ≫ g
rw₁ : s.π.app zero ≫ (parallelPair f g).map right = s.π.app zero ≫ g
⊢ s.π.app one = s.ι ≫ g
have rw₂ : s.π.app zero ≫ g = s.π.app zero ≫ g
Tactic: rw [← s.app_zero_eq_ι, ← s.w right, parallelPair_map_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Cofork f g
⊢ s.ι.app zero = f ≫ s.π
have rw : s.ι.app zero = f ≫ s.ι.app one
Tactic: rw [← s.app_one_eq_π, ← s.w left, parallelPair_map_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Cofork f g
rw : s.ι.app zero = f ≫ s.ι.app one
⊢ s.ι.app zero = f ≫ s.π
have rw₁ : (parallelPair f g).map left ≫ s.ι.app one = f ≫ s.ι.app one
Tactic: rw [← s.app_one_eq_π, ← s.w left, parallelPair_map_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Cofork f g
rw : s.ι.app zero = f ≫ s.ι.app one
rw₁ : (parallelPair f g).map left ≫ s.ι.app one = f ≫ s.ι.app one
⊢ s.ι.app zero = f ≫ s.π
have rw₂ : f ≫ s.ι.app one = f ≫ s.ι.app one
Tactic: rw [← s.app_one_eq_π, ← s.w left, parallelPair_map_left]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Cofork f g
⊢ s.ι.app zero = g ≫ s.π
have rw : s.ι.app zero = g ≫ s.ι.app one
Tactic: rw [← s.app_one_eq_π, ← s.w right, parallelPair_map_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Cofork f g
rw : s.ι.app zero = g ≫ s.ι.app one
⊢ s.ι.app zero = g ≫ s.π
have rw₁ : (parallelPair f g).map right ≫ s.ι.app one = g ≫ s.ι.app one
Tactic: rw [← s.app_one_eq_π, ← s.w right, parallelPair_map_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Cofork f g
rw : s.ι.app zero = g ≫ s.ι.app one
rw₁ : (parallelPair f g).map right ≫ s.ι.app one = g ≫ s.ι.app one
⊢ s.ι.app zero = g ≫ s.π
have rw₂ : g ≫ s.ι.app one = g ≫ s.ι.app one
Tactic: rw [← s.app_one_eq_π, ← s.w right, parallelPair_map_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f g : X_1 ⟶ Y
P : C
ι : P ⟶ X_1
w : ι ≫ f = ι ≫ g
X : WalkingParallelPair
⊢ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶ (parallelPair f g).obj X
have zero : Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) zero ⟶ (parallelPair f g).obj zero
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X_1 Y : C
f g : X_1 ⟶ Y
P : C
ι : P ⟶ X_1
w : ι ≫ f = ι ≫ g
X : WalkingParallelPair
zero :
  Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) WalkingParallelPair.zero ⟶
    (parallelPair f g).obj WalkingParallelPair.zero
⊢ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) X ⟶ (parallelPair f g).obj X
have one : Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one ⟶ (parallelPair f g).obj one
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
P : C
π : Y ⟶ P
w : f_1 ≫ π = g ≫ π
i j : WalkingParallelPair
f : i ⟶ j
⊢ Eq (α := (parallelPair f_1 g).obj i ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) j)
    ((parallelPair f_1 g).map f ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) j
        (f_1 ≫ π) π)
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) i
        (f_1 ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) f)
have left : Eq (α :=
  (parallelPair f_1 g).obj zero ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one)
  ((parallelPair f_1 g).map left ≫
    WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
      (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) one
      (f_1 ≫ π) π)
  (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
      (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) zero
      (f_1 ≫ π) π ≫
    Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) left)
Tactic: cases f
Cleared hypotheses: i, j, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
P : C
π : Y ⟶ P
w : f_1 ≫ π = g ≫ π
i j : WalkingParallelPair
f : i ⟶ j
left :
  Eq (α :=
    (parallelPair f_1 g).obj zero ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one)
    ((parallelPair f_1 g).map WalkingParallelPairHom.left ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) one
        (f_1 ≫ π) π)
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x)
        zero (f_1 ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) WalkingParallelPairHom.left)
⊢ Eq (α := (parallelPair f_1 g).obj i ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) j)
    ((parallelPair f_1 g).map f ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) j
        (f_1 ≫ π) π)
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) i
        (f_1 ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) f)
have right : Eq (α :=
  (parallelPair f_1 g).obj zero ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one)
  ((parallelPair f_1 g).map right ≫
    WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
      (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) one
      (f_1 ≫ π) π)
  (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
      (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) zero
      (f_1 ≫ π) π ≫
    Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) right)
Tactic: cases f
Cleared hypotheses: i, j, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f_1 g : X ⟶ Y
P : C
π : Y ⟶ P
w : f_1 ≫ π = g ≫ π
i j : WalkingParallelPair
f : i ⟶ j
left :
  Eq (α :=
    (parallelPair f_1 g).obj zero ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one)
    ((parallelPair f_1 g).map WalkingParallelPairHom.left ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) one
        (f_1 ≫ π) π)
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x)
        zero (f_1 ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) WalkingParallelPairHom.left)
right :
  Eq (α :=
    (parallelPair f_1 g).obj zero ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) one)
    ((parallelPair f_1 g).map WalkingParallelPairHom.right ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) one
        (f_1 ≫ π) π)
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x)
        zero (f_1 ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) WalkingParallelPairHom.right)
⊢ Eq (α := (parallelPair f_1 g).obj i ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) j)
    ((parallelPair f_1 g).map f ≫
      WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) j
        (f_1 ≫ π) π)
    (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
        (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) i
        (f_1 ≫ π) π ≫
      Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) f)
have id : Eq (α := (parallelPair f_1 g).obj i ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) i)
  ((parallelPair f_1 g).map (WalkingParallelPairHom.id i) ≫
    WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
      (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) i
      (f_1 ≫ π) π)
  (WalkingParallelPair.casesOn (motive := fun (x : WalkingParallelPair) ↦
      (parallelPair f_1 g).obj x ⟶ Functor.obj.{0, v, 0, u} (Functor.obj (Functor.const WalkingParallelPair) P) x) i
      (f_1 ≫ π) π ≫
    Functor.map (Functor.obj (Functor.const WalkingParallelPair) P) (WalkingParallelPairHom.id i))
Tactic: cases f
Cleared hypotheses: j, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
t : Fork f g
⊢ t.ι ≫ f = t.ι ≫ g
have rw : t.π.app one = t.ι ≫ g
Tactic: rw [← t.app_one_eq_ι_comp_left, ← t.app_one_eq_ι_comp_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
t : Fork f g
rw : t.π.app one = t.ι ≫ g
⊢ t.ι ≫ f = t.ι ≫ g
have rw₁ : t.π.app one = t.π.app one
Tactic: rw [← t.app_one_eq_ι_comp_left, ← t.app_one_eq_ι_comp_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
t : Cofork f g
⊢ f ≫ t.π = g ≫ t.π
have rw : t.ι.app zero = g ≫ t.π
Tactic: rw [← t.app_zero_eq_comp_π_left, ← t.app_zero_eq_comp_π_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
t : Cofork f g
rw : t.ι.app zero = g ≫ t.π
⊢ f ≫ t.π = g ≫ t.π
have rw₁ : t.ι.app zero = t.ι.app zero
Tactic: rw [← t.app_zero_eq_comp_π_left, ← t.app_zero_eq_comp_π_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
f g : X ⟶ Y
s : Fork f g
W : C
k l : W ⟶ s.pt
h : k ≫ s.ι = l ≫ s.ι
⊢ k ≫ s.ι ≫ f = l ≫ s.ι ≫ f
have simp : (k ≫ s.ι) ≫ f = (l ≫ s.ι) ≫ f
Tactic: simp only [← Category.assoc]