awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : Quiver.Hom (V := WalkingCospan) Option.none Option.none
none :
  Eq (α := F.obj Option.none ⟶ (cospan (F.map inl) (F.map inr)).obj Option.none)
    (F.map (WidePullbackShape.Hom.id Option.none) ≫
      Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) Option.none))
    (Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) Option.none) ≫
      (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id Option.none))
⊢ F.map f ≫
      Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) Option.none) =
    Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) Option.none) ≫
      (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : none ⟶ some WalkingPair.left
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.left)) =
    Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) ≫
      (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : none ⟶ some WalkingPair.right
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.right)) =
    Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) ≫
      (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : Option.some WalkingPair.left ⟶ none
some :
  F.map (term WalkingPair.left) ≫
      Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (Option.some WalkingPair.left)) ≫
      (cospan (F.map inl) (F.map inr)).map (term WalkingPair.left)
⊢ F.map f ≫ Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (Option.some WalkingPair.left)) ≫
      (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : Option.some WalkingPair.left ⟶ Option.some WalkingPair.left
some :
  F.map (WidePullbackShape.Hom.id (Option.some WalkingPair.left)) ≫
      Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (Option.some WalkingPair.left)) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (Option.some WalkingPair.left)) ≫
      (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (Option.some WalkingPair.left))
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (Option.some WalkingPair.left)) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (Option.some WalkingPair.left)) ≫
      (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.right)) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.left)) ≫
      (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : Option.some WalkingPair.right ⟶ none
some :
  F.map (term WalkingPair.right) ≫
      Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (Option.some WalkingPair.right)) ≫
      (cospan (F.map inl) (F.map inr)).map (term WalkingPair.right)
⊢ F.map f ≫ Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (Option.some WalkingPair.right)) ≫
      (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.left)) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.right)) ≫
      (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
f : Option.some WalkingPair.right ⟶ Option.some WalkingPair.right
some :
  F.map (WidePullbackShape.Hom.id (Option.some WalkingPair.right)) ≫
      Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (Option.some WalkingPair.right)) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (Option.some WalkingPair.right)) ≫
      (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (Option.some WalkingPair.right))
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (Option.some WalkingPair.right)) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (Option.some WalkingPair.right)) ≫
      (cospan (F.map inl) (F.map inr)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
⊢ Eq (α := F.obj none ⟶ (cospan (F.map inl) (F.map inr)).obj none)
    (F.map (WidePullbackShape.Hom.id none) ≫
      Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none))
    (Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) ≫
      (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id none))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
⊢ F.map (term WalkingPair.left) ≫
      Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.left)) ≫
      (cospan (F.map inl) (F.map inr)).map (term WalkingPair.left)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.left)) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.left)) ≫
      (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (some WalkingPair.left))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
⊢ F.map (term WalkingPair.right) ≫
      Iso.hom ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j)) none) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.right)) ≫
      (cospan (F.map inl) (F.map inr)).map (term WalkingPair.right)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingCospan C
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.right)) =
    Iso.hom
        ((fun (j : WalkingCospan) ↦ (eqToIso ⋯ : F.obj j ≅ (cospan (F.map inl) (F.map inr)).obj j))
          (some WalkingPair.right)) ≫
      (cospan (F.map inl) (F.map inr)).map (WidePullbackShape.Hom.id (some WalkingPair.right))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
j : WalkingSpan
none : F.obj Option.none = (span (F.map fst) (F.map snd)).obj Option.none
some : F.obj (Option.some WalkingPair.left) = (span (F.map fst) (F.map snd)).obj (Option.some WalkingPair.left)
some₁ : F.obj (Option.some WalkingPair.right) = (span (F.map fst) (F.map snd)).obj (Option.some WalkingPair.right)
⊢ F.obj j = (span (F.map fst) (F.map snd)).obj j

Tactic:
rcases j with (⟨⟩ | ⟨⟨⟩⟩)
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
⊢ F.obj none = (span (F.map fst) (F.map snd)).obj none

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
⊢ F.obj (some WalkingPair.left) = (span (F.map fst) (F.map snd)).obj (some WalkingPair.left)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
⊢ F.obj (some WalkingPair.right) = (span (F.map fst) (F.map snd)).obj (some WalkingPair.right)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : Quiver.Hom (V := WalkingSpan) Option.none Option.none
none :
  Eq (α := F.obj Option.none ⟶ (span (F.map fst) (F.map snd)).obj Option.none)
    (F.map (WidePushoutShape.Hom.id Option.none) ≫
      Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) Option.none))
    (Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) Option.none) ≫
      (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id Option.none))
⊢ F.map f ≫
      Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) Option.none) =
    Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) Option.none) ≫
      (span (F.map fst) (F.map snd)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : Option.none ⟶ some WalkingPair.left
none :
  F.map (init WalkingPair.left) ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.left)) =
    Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) Option.none) ≫
      (span (F.map fst) (F.map snd)).map (init WalkingPair.left)
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.left)) =
    Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) Option.none) ≫
      (span (F.map fst) (F.map snd)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : Option.none ⟶ some WalkingPair.right
none :
  F.map (init WalkingPair.right) ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.right)) =
    Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) Option.none) ≫
      (span (F.map fst) (F.map snd)).map (init WalkingPair.right)
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.right)) =
    Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) Option.none) ≫
      (span (F.map fst) (F.map snd)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : some WalkingPair.left ⟶ none
⊢ F.map f ≫ Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none) =
    Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.left)) ≫
      (span (F.map fst) (F.map snd)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : Option.some WalkingPair.left ⟶ Option.some WalkingPair.left
some :
  F.map (WidePushoutShape.Hom.id (Option.some WalkingPair.left)) ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (Option.some WalkingPair.left)) =
    Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (Option.some WalkingPair.left)) ≫
      (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (Option.some WalkingPair.left))
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (Option.some WalkingPair.left)) =
    Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (Option.some WalkingPair.left)) ≫
      (span (F.map fst) (F.map snd)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.right)) =
    Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.left)) ≫
      (span (F.map fst) (F.map snd)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : some WalkingPair.right ⟶ none
⊢ F.map f ≫ Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none) =
    Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.right)) ≫
      (span (F.map fst) (F.map snd)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.left)) =
    Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.right)) ≫
      (span (F.map fst) (F.map snd)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
f : Option.some WalkingPair.right ⟶ Option.some WalkingPair.right
some :
  F.map (WidePushoutShape.Hom.id (Option.some WalkingPair.right)) ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (Option.some WalkingPair.right)) =
    Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (Option.some WalkingPair.right)) ≫
      (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (Option.some WalkingPair.right))
⊢ F.map f ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (Option.some WalkingPair.right)) =
    Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (Option.some WalkingPair.right)) ≫
      (span (F.map fst) (F.map snd)).map f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
⊢ Eq (α := F.obj none ⟶ (span (F.map fst) (F.map snd)).obj none)
    (F.map (WidePushoutShape.Hom.id none) ≫
      Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none))
    (Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none) ≫
      (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id none))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
⊢ F.map (init WalkingPair.left) ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.left)) =
    Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none) ≫
      (span (F.map fst) (F.map snd)).map (init WalkingPair.left)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
⊢ F.map (init WalkingPair.right) ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.right)) =
    Iso.hom ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j)) none) ≫
      (span (F.map fst) (F.map snd)).map (init WalkingPair.right)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
⊢ F.map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.left)) =
    Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.left)) ≫
      (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (some WalkingPair.left))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{0, v, 0, u} WalkingSpan C
⊢ F.map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
      Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.right)) =
    Iso.hom
        ((fun (j : WalkingSpan) ↦ (eqToIso ⋯ : F.obj j ≅ (span (F.map fst) (F.map snd)).obj j))
          (some WalkingPair.right)) ≫
      (span (F.map fst) (F.map snd)).map (WidePushoutShape.Hom.id (some WalkingPair.right))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
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 : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).obj none ≅ (cospan (F.map f) (F.map g)).obj none

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
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 : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).obj (some WalkingPair.left) ≅ (cospan (F.map f) (F.map g)).obj (some WalkingPair.left)

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
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 : X ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).obj (some WalkingPair.right) ≅ (cospan (F.map f) (F.map g)).obj (some WalkingPair.right)

Tactic:
exact Iso.refl _

Premises used: CategoryTheory.Iso.refl