-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Square.lean
lemma IsPullback.iff_of_equiv : sq₁.IsPullback ↔ sq₂.IsPullback

Proof state:
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ sq₁.f₁₂ = sq₂.f₁₂ ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ sq₁.f₁₃ = sq₂.f₁₃ ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ sq₁.f₂₄ = sq₂.f₂₄ ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ sq₁.f₃₄ = sq₂.f₃₄ ∘ ⇑e₃
⊢ sq₁.IsPullback ↔ sq₂.IsPullback

Tactic:
rw [← IsPullback.map_iff sq₁ uliftFunctor.{max u v},
    ← IsPullback.map_iff sq₂ uliftFunctor.{max u v}]

Result:
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ sq₁.f₁₂ = sq₂.f₁₂ ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ sq₁.f₁₃ = sq₂.f₁₃ ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ sq₁.f₂₄ = sq₂.f₂₄ ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ sq₁.f₃₄ = sq₂.f₃₄ ∘ ⇑e₃
⊢ (sq₁.map uliftFunctor.{max u v, v}).IsPullback ↔ (sq₂.map uliftFunctor.{max u v, u}).IsPullback

Proof state:
case refine_1.h.a
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ sq₁.f₁₂ = sq₂.f₁₂ ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ sq₁.f₁₃ = sq₂.f₁₃ ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ sq₁.f₂₄ = sq₂.f₂₄ ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ sq₁.f₃₄ = sq₂.f₃₄ ∘ ⇑e₃
a✝ : (sq₁.map uliftFunctor.{max u v, v}).X₁
⊢ (((sq₁.map uliftFunctor.{max u v, v}).f₁₂ ≫ ((Equiv.ulift.trans e₂).trans Equiv.ulift.symm).toIso.hom) a✝).down =
    ((((Equiv.ulift.trans e₁).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₁₂) a✝).down

Tactic:
simpa [types_comp, uliftFunctor_map] using congrFun comm₁₂ _

Result:
no goals

Proof state:
case refine_1
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ sq₁.f₁₂ = sq₂.f₁₂ ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ sq₁.f₁₃ = sq₂.f₁₃ ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ sq₁.f₂₄ = sq₂.f₂₄ ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ sq₁.f₃₄ = sq₂.f₃₄ ∘ ⇑e₃
⊢ (sq₁.map uliftFunctor.{max u v, v}).f₁₂ ≫ ((Equiv.ulift.trans e₂).trans Equiv.ulift.symm).toIso.hom =
    ((Equiv.ulift.trans e₁).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₁₂

case refine_2
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ sq₁.f₁₂ = sq₂.f₁₂ ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ sq₁.f₁₃ = sq₂.f₁₃ ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ sq₁.f₂₄ = sq₂.f₂₄ ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ sq₁.f₃₄ = sq₂.f₃₄ ∘ ⇑e₃
⊢ (sq₁.map uliftFunctor.{max u v, v}).f₁₃ ≫ ((Equiv.ulift.trans e₃).trans Equiv.ulift.symm).toIso.hom =
    ((Equiv.ulift.trans e₁).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₁₃

case refine_3
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ sq₁.f₁₂ = sq₂.f₁₂ ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ sq₁.f₁₃ = sq₂.f₁₃ ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ sq₁.f₂₄ = sq₂.f₂₄ ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ sq₁.f₃₄ = sq₂.f₃₄ ∘ ⇑e₃
⊢ (sq₁.map uliftFunctor.{max u v, v}).f₂₄ ≫ ((Equiv.ulift.trans e₄).trans Equiv.ulift.symm).toIso.hom =
    ((Equiv.ulift.trans e₂).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₂₄

case refine_4
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ sq₁.f₁₂ = sq₂.f₁₂ ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ sq₁.f₁₃ = sq₂.f₁₃ ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ sq₁.f₂₄ = sq₂.f₂₄ ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ sq₁.f₃₄ = sq₂.f₃₄ ∘ ⇑e₃
⊢ (sq₁.map uliftFunctor.{max u v, v}).f₃₄ ≫ ((Equiv.ulift.trans e₄).trans Equiv.ulift.symm).toIso.hom =
    ((Equiv.ulift.trans e₃).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₃₄

Tactic:
all_goals ext; apply ULift.down_injective

Result:
case refine_1.h.a
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ sq₁.f₁₂ = sq₂.f₁₂ ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ sq₁.f₁₃ = sq₂.f₁₃ ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ sq₁.f₂₄ = sq₂.f₂₄ ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ sq₁.f₃₄ = sq₂.f₃₄ ∘ ⇑e₃
a✝ : (sq₁.map uliftFunctor.{max u v, v}).X₁
⊢ (((sq₁.map uliftFunctor.{max u v, v}).f₁₂ ≫ ((Equiv.ulift.trans e₂).trans Equiv.ulift.symm).toIso.hom) a✝).down =
    ((((Equiv.ulift.trans e₁).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₁₂) a✝).down

case refine_2.h.a
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ sq₁.f₁₂ = sq₂.f₁₂ ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ sq₁.f₁₃ = sq₂.f₁₃ ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ sq₁.f₂₄ = sq₂.f₂₄ ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ sq₁.f₃₄ = sq₂.f₃₄ ∘ ⇑e₃
a✝ : (sq₁.map uliftFunctor.{max u v, v}).X₁
⊢ (((sq₁.map uliftFunctor.{max u v, v}).f₁₃ ≫ ((Equiv.ulift.trans e₃).trans Equiv.ulift.symm).toIso.hom) a✝).down =
    ((((Equiv.ulift.trans e₁).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₁₃) a✝).down

case refine_3.h.a
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ sq₁.f₁₂ = sq₂.f₁₂ ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ sq₁.f₁₃ = sq₂.f₁₃ ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ sq₁.f₂₄ = sq₂.f₂₄ ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ sq₁.f₃₄ = sq₂.f₃₄ ∘ ⇑e₃
a✝ : (sq₁.map uliftFunctor.{max u v, v}).X₂
⊢ (((sq₁.map uliftFunctor.{max u v, v}).f₂₄ ≫ ((Equiv.ulift.trans e₄).trans Equiv.ulift.symm).toIso.hom) a✝).down =
    ((((Equiv.ulift.trans e₂).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₂₄) a✝).down

case refine_4.h.a
sq₁ : Square (Type v)
sq₂ : Square (Type u)
e₁ : sq₁.X₁ ≃ sq₂.X₁
e₂ : sq₁.X₂ ≃ sq₂.X₂
e₃ : sq₁.X₃ ≃ sq₂.X₃
e₄ : sq₁.X₄ ≃ sq₂.X₄
comm₁₂ : ⇑e₂ ∘ sq₁.f₁₂ = sq₂.f₁₂ ∘ ⇑e₁
comm₁₃ : ⇑e₃ ∘ sq₁.f₁₃ = sq₂.f₁₃ ∘ ⇑e₁
comm₂₄ : ⇑e₄ ∘ sq₁.f₂₄ = sq₂.f₂₄ ∘ ⇑e₂
comm₃₄ : ⇑e₄ ∘ sq₁.f₃₄ = sq₂.f₃₄ ∘ ⇑e₃
a✝ : (sq₁.map uliftFunctor.{max u v, v}).X₃
⊢ (((sq₁.map uliftFunctor.{max u v, v}).f₃₄ ≫ ((Equiv.ulift.trans e₄).trans Equiv.ulift.symm).toIso.hom) a✝).down =
    ((((Equiv.ulift.trans e₃).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₃₄) a✝).down