-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
Goal:
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : Equiv.{v + 1, u + 1} sq₁.X₁ sq₂.X₁
e₂ : Equiv.{v + 1, u + 1} sq₁.X₂ sq₂.X₂
e₃ : Equiv.{v + 1, u + 1} sq₁.X₃ sq₂.X₃
e₄ : Equiv.{v + 1, u + 1} sq₁.X₄ sq₂.X₄
comm₁₂ :
  Eq (α := (fun (X : Type v) ↦ X) sq₁.X₁ → sq₂.X₂)
    (Function.comp (β := sq₁.X₂) (⇑e₂ : (a : sq₁.X₂) → sq₂.X₂)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) sq₁.f₁₂) :
        (a : (fun (X : Type v) ↦ X) sq₁.X₁) → (fun (X : Type v) ↦ X) sq₁.X₂))
    (Function.comp (β := (fun (X : Type u) ↦ X) sq₂.X₁)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) sq₂.f₁₂) :
        (a : (fun (X : Type u) ↦ X) sq₂.X₁) → (fun (X : Type u) ↦ X) sq₂.X₂)
      (⇑e₁ : (a : sq₁.X₁) → sq₂.X₁))
comm₁₃ :
  Eq (α := (fun (X : Type v) ↦ X) sq₁.X₁ → sq₂.X₃)
    (Function.comp (β := sq₁.X₃) (⇑e₃ : (a : sq₁.X₃) → sq₂.X₃)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) sq₁.f₁₃) :
        (a : (fun (X : Type v) ↦ X) sq₁.X₁) → (fun (X : Type v) ↦ X) sq₁.X₃))
    (Function.comp (β := (fun (X : Type u) ↦ X) sq₂.X₁)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) sq₂.f₁₃) :
        (a : (fun (X : Type u) ↦ X) sq₂.X₁) → (fun (X : Type u) ↦ X) sq₂.X₃)
      (⇑e₁ : (a : sq₁.X₁) → sq₂.X₁))
comm₂₄ :
  Eq (α := (fun (X : Type v) ↦ X) sq₁.X₂ → sq₂.X₄)
    (Function.comp (β := sq₁.X₄) (⇑e₄ : (a : sq₁.X₄) → sq₂.X₄)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) sq₁.f₂₄) :
        (a : (fun (X : Type v) ↦ X) sq₁.X₂) → (fun (X : Type v) ↦ X) sq₁.X₄))
    (Function.comp (β := (fun (X : Type u) ↦ X) sq₂.X₂)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) sq₂.f₂₄) :
        (a : (fun (X : Type u) ↦ X) sq₂.X₂) → (fun (X : Type u) ↦ X) sq₂.X₄)
      (⇑e₂ : (a : sq₁.X₂) → sq₂.X₂))
comm₃₄ :
  Eq (α := (fun (X : Type v) ↦ X) sq₁.X₃ → sq₂.X₄)
    (Function.comp (β := sq₁.X₄) (⇑e₄ : (a : sq₁.X₄) → sq₂.X₄)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) sq₁.f₃₄) :
        (a : (fun (X : Type v) ↦ X) sq₁.X₃) → (fun (X : Type v) ↦ X) sq₁.X₄))
    (Function.comp (β := (fun (X : Type u) ↦ X) sq₂.X₃)
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) sq₂.f₃₄) :
        (a : (fun (X : Type u) ↦ X) sq₂.X₃) → (fun (X : Type u) ↦ X) sq₂.X₄)
      (⇑e₃ : (a : sq₁.X₃) → sq₂.X₃))
refine_1 :
  (sq₁.map uliftFunctor.{max u v, v}).f₁₂ ≫ ((Equiv.trans Equiv.ulift e₂).trans (Equiv.symm Equiv.ulift)).toIso.hom =
    ((Equiv.trans Equiv.ulift e₁).trans (Equiv.symm Equiv.ulift)).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₁₂
refine_2 :
  (sq₁.map uliftFunctor.{max u v, v}).f₁₃ ≫ ((Equiv.trans Equiv.ulift e₃).trans (Equiv.symm Equiv.ulift)).toIso.hom =
    ((Equiv.trans Equiv.ulift e₁).trans (Equiv.symm Equiv.ulift)).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₁₃
refine_3 :
  (sq₁.map uliftFunctor.{max u v, v}).f₂₄ ≫ ((Equiv.trans Equiv.ulift e₄).trans (Equiv.symm Equiv.ulift)).toIso.hom =
    ((Equiv.trans Equiv.ulift e₂).trans (Equiv.symm Equiv.ulift)).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₂₄
refine_4 :
  (sq₁.map uliftFunctor.{max u v, v}).f₃₄ ≫ ((Equiv.trans Equiv.ulift e₄).trans (Equiv.symm Equiv.ulift)).toIso.hom =
    ((Equiv.trans Equiv.ulift e₃).trans (Equiv.symm Equiv.ulift)).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₃₄
⊢ (sq₁.map uliftFunctor.{max u v, v}).IsPullback ↔ (sq₂.map uliftFunctor.{max u v, u}).IsPullback

Tactic:
refine iff_of_iso (Square.isoMk
    (((Equiv.trans Equiv.ulift e₁).trans Equiv.ulift.symm).toIso)
    (((Equiv.trans Equiv.ulift e₂).trans Equiv.ulift.symm).toIso)
    (((Equiv.trans Equiv.ulift e₃).trans Equiv.ulift.symm).toIso)
    (((Equiv.trans Equiv.ulift e₄).trans Equiv.ulift.symm).toIso)
    ?_ ?_ ?_ ?_)

Premises used: CategoryTheory.Square.IsPullback.iff_of_iso, CategoryTheory.Square.isoMk