awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ Eq (α := (cospan f_1 g ⋙ F).obj (some WalkingPair.left) ⟶ (cospan (F.map f_1) (F.map g)).obj none)
    ((cospan f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.left)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map f)
have some : Eq (α := (cospan f_1 g ⋙ F).obj (some WalkingPair.left) ⟶ (cospan (F.map f_1) (F.map g)).obj none)
  ((cospan f_1 g ⋙ F).map (term WalkingPair.left) ≫
    Iso.hom
      (Option.casesOn (motive := fun (x : WalkingCospan) ↦
        (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
        fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
  (Iso.hom
      (Option.casesOn (motive := fun (x : WalkingCospan) ↦
        (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.left)
        (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
    (cospan (F.map f_1) (F.map g)).map (term WalkingPair.left))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ Eq (α := (cospan f_1 g ⋙ F).obj (some WalkingPair.left) ⟶ (cospan (F.map f_1) (F.map g)).obj (some WalkingPair.left))
    ((cospan f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.left)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.left)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map f)
have some : Eq (α := (cospan f_1 g ⋙ F).obj (some WalkingPair.left) ⟶ (cospan (F.map f_1) (F.map g)).obj (some WalkingPair.left))
  ((cospan f_1 g ⋙ F).map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
    Iso.hom
      (Option.casesOn (motive := fun (x : WalkingCospan) ↦
        (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.left)
        (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
  (Iso.hom
      (Option.casesOn (motive := fun (x : WalkingCospan) ↦
        (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.left)
        (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
    (cospan (F.map f_1) (F.map g)).map (WidePullbackShape.Hom.id (some WalkingPair.left)))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ Eq (α := (cospan f_1 g ⋙ F).obj (some WalkingPair.right) ⟶ (cospan (F.map f_1) (F.map g)).obj none)
    ((cospan f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
          fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.right)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map f)
have some : Eq (α := (cospan f_1 g ⋙ F).obj (some WalkingPair.right) ⟶ (cospan (F.map f_1) (F.map g)).obj none)
  ((cospan f_1 g ⋙ F).map (term WalkingPair.right) ≫
    Iso.hom
      (Option.casesOn (motive := fun (x : WalkingCospan) ↦
        (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) none (Iso.refl ((cospan f_1 g ⋙ F).obj none))
        fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
  (Iso.hom
      (Option.casesOn (motive := fun (x : WalkingCospan) ↦
        (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.right)
        (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
    (cospan (F.map f_1) (F.map g)).map (term WalkingPair.right))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ Eq (α :=
    (cospan f_1 g ⋙ F).obj (some WalkingPair.right) ⟶ (cospan (F.map f_1) (F.map g)).obj (some WalkingPair.right))
    ((cospan f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.right)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.right)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map f)
have some : Eq (α := (cospan f_1 g ⋙ F).obj (some WalkingPair.right) ⟶ (cospan (F.map f_1) (F.map g)).obj (some WalkingPair.right))
  ((cospan f_1 g ⋙ F).map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
    Iso.hom
      (Option.casesOn (motive := fun (x : WalkingCospan) ↦
        (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.right)
        (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))))
  (Iso.hom
      (Option.casesOn (motive := fun (x : WalkingCospan) ↦
        (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (some WalkingPair.right)
        (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (cospan f_1 g ⋙ F).obj (some x) ≅ (cospan (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((cospan f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
    (cospan (F.map f_1) (F.map g)).map (WidePullbackShape.Hom.id (some WalkingPair.right)))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
f : Quiver.Hom (V := WalkingSpan) none none
⊢ Eq (α := (span f_1 g ⋙ F).obj none ⟶ (span (F.map f_1) (F.map g)).obj none)
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          none (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          none (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (F.map f_1) (F.map g)).map f)
have none : Eq (α := (span f_1 g ⋙ F).obj none ⟶ (span (F.map f_1) (F.map g)).obj none)
  ((span f_1 g ⋙ F).map (WidePushoutShape.Hom.id none) ≫
    Iso.hom
      (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
        none (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
  (Iso.hom
      (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
        none (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
    (span (F.map f_1) (F.map g)).map (WidePushoutShape.Hom.id none))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ Eq (α := (span f_1 g ⋙ F).obj none ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.left))
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          none (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (F.map f_1) (F.map g)).map f)
have none : Eq (α := (span f_1 g ⋙ F).obj none ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.left))
  ((span f_1 g ⋙ F).map (init WalkingPair.left) ≫
    Iso.hom
      (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
        (some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
  (Iso.hom
      (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
        none (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
    (span (F.map f_1) (F.map g)).map (init WalkingPair.left))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ Eq (α := (span f_1 g ⋙ F).obj none ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.right))
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          none (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (F.map f_1) (F.map g)).map f)
have none : Eq (α := (span f_1 g ⋙ F).obj none ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.right))
  ((span f_1 g ⋙ F).map (init WalkingPair.right) ≫
    Iso.hom
      (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
        (some WalkingPair.right) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
  (Iso.hom
      (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
        none (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
    (span (F.map f_1) (F.map g)).map (init WalkingPair.right))
Tactic: cases f
Cleared hypotheses: f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ Eq (α := (span f_1 g ⋙ F).obj (some WalkingPair.left) ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.left))
    ((span f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
          (some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
      (span (F.map f_1) (F.map g)).map f)
have some : Eq (α := (span f_1 g ⋙ F).obj (some WalkingPair.left) ⟶ (span (F.map f_1) (F.map g)).obj (some WalkingPair.left))
  ((span f_1 g ⋙ F).map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
    Iso.hom
      (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
        (some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))))
  (Iso.hom
      (Option.casesOn (motive := fun (x : WalkingSpan) ↦ (span f_1 g ⋙ F).obj x ≅ (span (F.map f_1) (F.map g)).obj x)
        (some WalkingPair.left) (Iso.refl ((span f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
        WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
          (span f_1 g ⋙ F).obj (some x) ≅ (span (F.map f_1) (F.map g)).obj (some x)) val
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.left)))
          (Iso.refl ((span f_1 g ⋙ F).obj (some WalkingPair.right)))) ≫
    (span (F.map f_1) (F.map g)).map (WidePushoutShape.Hom.id (some WalkingPair.left)))
Tactic: cases f
Cleared hypotheses: f