awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
j : WalkingParallelPairᵒᵖ
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j = Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j
have op : ∀ (X : WalkingParallelPair),
  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op X) = Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op X)
Tactic: induction j with | _ X
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X : WalkingParallelPair
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op X) = Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op X)
have op : (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero) = Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op zero)
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X : WalkingParallelPair
op :
  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero) =
    Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op zero)
⊢ (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op X) =
    Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op X)
have op₁ : (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) =
  Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op one)
Tactic: cases X
Cleared hypotheses: X
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
i j : WalkingParallelPairᵒᵖ
f : i ⟶ j
⊢ Eq (α := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj i ⟶ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j)
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          j))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          i) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) f)
have op : ∀ (i : WalkingParallelPair) (f : op i ⟶ j),
  Eq (α := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op i) ⟶ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j)
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso sorry :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          j))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso sorry :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op i)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) f)
Tactic: induction i with | _ i
Cleared hypotheses: i, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
j : WalkingParallelPairᵒᵖ
i : WalkingParallelPair
f : op i ⟶ j
⊢ Eq (α := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op i) ⟶ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j)
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          j))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op i)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) f)
have op : ∀ (j : WalkingParallelPair) (f : op i ⟶ op j),
  Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op i) ⟶ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op j))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso sorry :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op j)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso sorry :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op i)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) f)
Tactic: induction j with | _ j
Cleared hypotheses: j, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (hypothesis)
Goal:
i j : WalkingParallelPair
f : op i ⟶ op j
g : unop (op j) ⟶ unop (op i) := f.unop
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op i) ⟶ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op j))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op j)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op i)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) f)
have this : f = g.op
Tactic: have : f = g.op := rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
i j : WalkingParallelPair
f : op i ⟶ op j
g : unop (op j) ⟶ unop (op i) := f.unop
this : f = g.op
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op i) ⟶ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op j))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map f ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op j)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op i)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) f)
have op : Eq (α :=
  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op i) ⟶ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op j))
  ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
    Iso.hom
      ((fun (j : WalkingParallelPairᵒᵖ) ↦
          (eqToIso sorry :
            (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
        (op j)))
  (Iso.hom
      ((fun (j : WalkingParallelPairᵒᵖ) ↦
          (eqToIso sorry :
            (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
        (op i)) ≫
    Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
i j : WalkingParallelPair
f : op i ⟶ op j
g : unop (op j) ⟶ unop (op i) := f.unop
this : f = g.op
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op i) ⟶ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op j))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op j)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op i)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
have op : ∀ (f : op zero ⟶ op j),
  let g := f.unop;
  ∀ (this : f = g.op),
    Eq (α :=
      (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero) ⟶
        Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op j))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
        Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso sorry :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (op j)))
      (Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso sorry :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (op zero)) ≫
        Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
Tactic: cases i
Cleared hypotheses: i, f, g, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
i j : WalkingParallelPair
f : Opposite.op i ⟶ Opposite.op j
g : unop (Opposite.op j) ⟶ unop (Opposite.op i) := f.unop
this : f = g.op
op :
  ∀ (f : Opposite.op zero ⟶ Opposite.op j),
    let g := f.unop;
    ∀ (this : f = g.op),
      Eq (α :=
        (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero) ⟶
          Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op j))
        ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
          Iso.hom
            ((fun (j : WalkingParallelPairᵒᵖ) ↦
                (eqToIso ⋯ :
                  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅
                    Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
              (Opposite.op j)))
        (Iso.hom
            ((fun (j : WalkingParallelPairᵒᵖ) ↦
                (eqToIso ⋯ :
                  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅
                    Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
              (Opposite.op zero)) ≫
          Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op i) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op j))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op j)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op i)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
have op₁ : ∀ (f : Opposite.op one ⟶ Opposite.op j),
  let g := f.unop;
  ∀ (this : f = g.op),
    Eq (α :=
      (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) ⟶
        Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op j))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
        Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso sorry :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (Opposite.op j)))
      (Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso sorry :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (Opposite.op one)) ≫
        Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
Tactic: cases i
Cleared hypotheses: i, f, g, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
j : WalkingParallelPair
f : op zero ⟶ op j
g : unop (op j) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero) ⟶ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op j))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op j)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op zero)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
have op : ∀ (f : op zero ⟶ op zero),
  let g := f.unop;
  ∀ (this : f = g.op),
    Eq (α :=
      (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero) ⟶
        Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op zero))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
        Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso sorry :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (op zero)))
      (Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso sorry :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (op zero)) ≫
        Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
Tactic: cases j
Cleared hypotheses: j, f, g, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
j : WalkingParallelPair
f : Opposite.op zero ⟶ Opposite.op j
g : unop (Opposite.op j) ⟶ unop (Opposite.op zero) := f.unop
this : f = g.op
op :
  ∀ (f : Opposite.op zero ⟶ Opposite.op zero),
    let g := f.unop;
    ∀ (this : f = g.op),
      Eq (α :=
        (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero) ⟶
          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 zero)) ≫
          Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op j))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op j)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op zero)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
have op₁ : ∀ (f : Opposite.op zero ⟶ Opposite.op one),
  let g := f.unop;
  ∀ (this : f = g.op),
    Eq (α :=
      (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op zero) ⟶
        Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op one))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
        Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso sorry :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (Opposite.op one)))
      (Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso sorry :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (Opposite.op zero)) ≫
        Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
Tactic: cases j
Cleared hypotheses: j, f, g, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
j : WalkingParallelPair
f : op one ⟶ op j
g : unop (op j) ⟶ unop (op one) := f.unop
this : f = g.op
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op one) ⟶ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op j))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op j)))
    (Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (op one)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
have op : ∀ (f : op one ⟶ op zero),
  let g := 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 sorry :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (op zero)))
      (Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso sorry :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (op one)) ≫
        Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
Tactic: cases j
Cleared hypotheses: j, f, g, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
j : WalkingParallelPair
f : Opposite.op one ⟶ Opposite.op j
g : unop (Opposite.op j) ⟶ unop (Opposite.op one) := f.unop
this : f = g.op
op :
  ∀ (f : Opposite.op one ⟶ Opposite.op zero),
    let g := f.unop;
    ∀ (this : f = g.op),
      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)
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) ⟶
      Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op j))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
      Iso.hom
        ((fun (j : WalkingParallelPairᵒᵖ) ↦
            (eqToIso ⋯ :
              (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
          (Opposite.op j)))
    (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₁ : ∀ (f : Opposite.op one ⟶ Opposite.op one),
  let g := f.unop;
  ∀ (this : f = g.op),
    Eq (α :=
      (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (Opposite.op one) ⟶
        Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (Opposite.op one))
      ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map g.op ≫
        Iso.hom
          ((fun (j : WalkingParallelPairᵒᵖ) ↦
              (eqToIso sorry :
                (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
            (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ᵒᵖ) g.op)
Tactic: cases j
Cleared hypotheses: j, f, g, this
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
f : op zero ⟶ op zero
g : unop (op zero) ⟶ unop (op zero) := f.unop
this : f = g.op
⊢ Eq (α :=
    (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero) ⟶
      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 zero)) ≫
      Functor.map (𝟭 WalkingParallelPairᵒᵖ) g.op)
have op : Eq (α :=
  (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero) ⟶
    Functor.obj (𝟭 WalkingParallelPairᵒᵖ) (op zero))
  (CategoryStruct.comp (Y := (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj (op zero))
    ((walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).map
      (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op zero)))))
    (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 zero))
    (Iso.hom
      ((fun (j : WalkingParallelPairᵒᵖ) ↦
          (eqToIso sorry :
            (walkingParallelPairOp.leftOp ⋙ walkingParallelPairOp).obj j ≅ Functor.obj (𝟭 WalkingParallelPairᵒᵖ) j))
        (op zero)))
    (Functor.map (𝟭 WalkingParallelPairᵒᵖ) (Quiver.Hom.op (WalkingParallelPairHom.id (unop (op zero))))))
Tactic: cases g