-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pushouts (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
j : WalkingSpan
x : (span t l).obj j
none :
  ∀ (x : (span t l).obj Option.none),
    (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
        Eq (α := (fun (X : Type u) ↦ X) X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄)
              x₂ :
            (fun (X : Type u) ↦ X) X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app Option.none) :
                (a : (fun (X : Type u) ↦ X) ((span t l).obj Option.none)) →
                  (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj Option.none))
              x :
            (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) Option.none))) ∨
      ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
        Eq (α := (fun (X : Type u) ↦ X) X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄)
              x₃ :
            (fun (X : Type u) ↦ X) X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app Option.none) :
                (a : (fun (X : Type u) ↦ X) ((span t l).obj Option.none)) →
                  (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj Option.none))
              x :
            (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) Option.none))
some :
  ∀ (x : (span t l).obj (Option.some WalkingPair.left)),
    (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
        Eq (α := (fun (X : Type u) ↦ X) X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄)
              x₂ :
            (fun (X : Type u) ↦ X) X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app (Option.some WalkingPair.left)) :
                (a : (fun (X : Type u) ↦ X) ((span t l).obj (Option.some WalkingPair.left))) →
                  (fun (X : Type u) ↦ X)
                    (((Functor.const WalkingSpan).obj h.cocone.pt).obj (Option.some WalkingPair.left)))
              x :
            (fun (X : Type u) ↦ X)
              (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) (Option.some WalkingPair.left)))) ∨
      ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
        Eq (α := (fun (X : Type u) ↦ X) X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄)
              x₃ :
            (fun (X : Type u) ↦ X) X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app (Option.some WalkingPair.left)) :
                (a : (fun (X : Type u) ↦ X) ((span t l).obj (Option.some WalkingPair.left))) →
                  (fun (X : Type u) ↦ X)
                    (((Functor.const WalkingSpan).obj h.cocone.pt).obj (Option.some WalkingPair.left)))
              x :
            (fun (X : Type u) ↦ X)
              (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) (Option.some WalkingPair.left)))
⊢ (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ :
          (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app j) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj j)) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj j))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) j))) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ :
          (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app j) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj j)) →
                (fun (X : Type u) ↦ X) (((Functor.const WalkingSpan).obj h.cocone.pt).obj j))
            x :
          (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) j))
have some₁ : ∀ (x : (span t l).obj (Option.some WalkingPair.right)),
  (∃ (x₂ : (fun (X : Type u) ↦ X) X₂),
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₄) x₂ :
          (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app (Option.some WalkingPair.right)) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj (Option.some WalkingPair.right))) →
                (fun (X : Type u) ↦ X)
                  (((Functor.const WalkingSpan).obj h.cocone.pt).obj (Option.some WalkingPair.right)))
            x :
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) (Option.some WalkingPair.right)))) ∨
    ∃ (x₃ : (fun (X : Type u) ↦ X) X₃),
      Eq (α := (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) x₃ :
          (fun (X : Type u) ↦ X) X₄)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (h.cocone.ι.app (Option.some WalkingPair.right)) :
              (a : (fun (X : Type u) ↦ X) ((span t l).obj (Option.some WalkingPair.right))) →
                (fun (X : Type u) ↦ X)
                  (((Functor.const WalkingSpan).obj h.cocone.pt).obj (Option.some WalkingPair.right)))
            x :
          (fun (X : Type u) ↦ X)
            (Functor.obj (Functor.obj (Functor.const WalkingSpan) h.cocone.pt) (Option.some WalkingPair.right)))
Tactic: obtain (_ | _ | _) := j
Cleared hypotheses: j, x