-- Module: Mathlib.CategoryTheory.Limits.Types.Pushouts
Goal:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' :
  Function.Injective (α := (fun (X : Type u) ↦ X) X₂) (β := (fun (X : Type u) ↦ X) X₅)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (r ≫ k)) : (a : (fun (X : Type u) ↦ X) X₂) → (fun (X : Type u) ↦ X) X₅)
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
            (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
      y₃ ∉
          Set.range (ι := (fun (X : Type u) ↦ X) X₁)
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) :
              (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃) →
        Eq (α := (fun (X : Type u) ↦ X) X₅)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (b ≫ k) :
                  (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) (b ≫ k) :
                  (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₅)
                y₃ :
              (fun (X : Type u) ↦ X) X₅) →
          x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this :
  Function.Injective (α := (fun (X : Type u) ↦ X) X₁) (β := (fun (X : Type u) ↦ X) X₃)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
w :
  ∀ (x : ToType (FC := TypeCat.Fun) X₁),
    Eq (α := X₄)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) r : (a : X₂) → X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) t : (a : X₁) → X₂) x : X₂) :
        X₄)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) b : (a : X₃) → X₄)
          ((ConcreteCategory.hom (FC := TypeCat.Fun) l : (a : X₁) → X₃) x : X₃) :
        X₄)
x₂ : X₂
y₃ : X₃
hy₃ :
  y₃ ∉
    Set.range (ι := (fun (X : Type u) ↦ X) X₁)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃)
eq :
  Eq (α := (fun (X : Type u) ↦ X) X₅)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) k : (a : (fun (X : Type u) ↦ X) X₄) → (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₄) :
      (fun (X : Type u) ↦ X) X₅)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) k : (a : (fun (X : Type u) ↦ X) X₄) → (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₄) y₃ :
          (fun (X : Type u) ↦ X) X₄) :
      (fun (X : Type u) ↦ X) X₅)
inl :
  ∀ (x₁ : X₁)
    (hy₃ :
      ((ConcreteCategory.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₃) ∉
        Set.range (ι := (fun (X : Type u) ↦ X) X₁)
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) l) : (a : (fun (X : Type u) ↦ X) X₁) → (fun (X : Type u) ↦ X) X₃))
    (eq :
      Eq (α := (fun (X : Type u) ↦ X) X₅)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) k : (a : (fun (X : Type u) ↦ X) X₄) → (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₄)
                ((ConcreteCategory.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₂) :
              (fun (X : Type u) ↦ X) X₄) :
          (fun (X : Type u) ↦ X) X₅)
        ((ConcreteCategory.hom (FC := TypeCat.Fun) k : (a : (fun (X : Type u) ↦ X) X₄) → (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₄)
                ((ConcreteCategory.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₃) :
              (fun (X : Type u) ↦ X) 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₄)
          ((ConcreteCategory.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₂) :
        (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₄)
          ((ConcreteCategory.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₃) :
        (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) b : (a : (fun (X : Type u) ↦ X) X₃) → (fun (X : Type u) ↦ X) X₄) y₃ :
      (fun (X : Type u) ↦ X) X₄)

Tactic:
obtain ⟨x₁, rfl, rfl⟩ := exists_of_isPullback h₂ x₂ y₃ eq

Premises used: rfl, CategoryTheory.Limits.Types.exists_of_isPullback