-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Pullbacks (goal)
Goal:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
mp :
  IsPullback t l r b →
    t ≫ r = l ≫ b ∧
      (∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
          Eq (α := (fun (X : Type u) ↦ X) X₂)
                ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ :
                  (fun (X : Type u) ↦ X) X₂)
                ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) y₁ :
                  (fun (X : Type u) ↦ X) X₂) ∧
              Eq (α := (fun (X : Type u) ↦ X) X₃)
                ((hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ :
                  (fun (X : Type u) ↦ X) X₃)
                ((hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) y₁ :
                  (fun (X : Type u) ↦ X) X₃) →
            x₁ = y₁) ∧
        ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
          Eq (α := (fun (X : Type u) ↦ X) X₄)
              ((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₄)
              ((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₄) →
            ∃ (x₁ : (fun (X : Type u) ↦ X) X₁),
              (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
                (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃
⊢ IsPullback t l r b ↔
    t ≫ r = l ≫ b ∧
      (∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
          Eq (α := (fun (X : Type u) ↦ X) X₂)
                ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ :
                  (fun (X : Type u) ↦ X) X₂)
                ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) y₁ :
                  (fun (X : Type u) ↦ X) X₂) ∧
              Eq (α := (fun (X : Type u) ↦ X) X₃)
                ((hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ :
                  (fun (X : Type u) ↦ X) X₃)
                ((hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) y₁ :
                  (fun (X : Type u) ↦ X) X₃) →
            x₁ = y₁) ∧
        ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
          Eq (α := (fun (X : Type u) ↦ X) X₄)
              ((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₄)
              ((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₄) →
            ∃ (x₁ : (fun (X : Type u) ↦ X) X₁),
              (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
                (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃
have mpr : (t ≫ r = l ≫ b ∧
    (∀ (x₁ y₁ : (fun (X : Type u) ↦ X) X₁),
        Eq (α := (fun (X : Type u) ↦ X) X₂)
              ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ :
                (fun (X : Type u) ↦ X) X₂)
              ((hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) y₁ :
                (fun (X : Type u) ↦ X) X₂) ∧
            Eq (α := (fun (X : Type u) ↦ X) X₃)
              ((hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ :
                (fun (X : Type u) ↦ X) X₃)
              ((hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) y₁ :
                (fun (X : Type u) ↦ X) X₃) →
          x₁ = y₁) ∧
      ∀ (x₂ : (fun (X : Type u) ↦ X) X₂) (x₃ : (fun (X : Type u) ↦ X) X₃),
        Eq (α := (fun (X : Type u) ↦ X) X₄)
            ((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₄)
            ((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₄) →
          ∃ (x₁ : (fun (X : Type u) ↦ X) X₁),
            (hom (FC := TypeCat.Fun) t : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₂) x₁ = x₂ ∧
              (hom (FC := TypeCat.Fun) l : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) x₁ = x₃) →
  IsPullback t l r b
Tactic: constructor