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

Proof state:
case refine_4.h
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✝ =
    (((Equiv.ulift.trans e₃).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₃₄) a✝

Tactic:
apply ULift.down_injective

Result:
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

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₁.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)
  ?_ ?_ ?_ ?_)

Result:
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₃₄

Proof state:
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

Tactic:
simpa [types_comp, uliftFunctor_map] using congrFun comm₃₄ _

Result:
no goals

Proof state:
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:
ext

Result:
case refine_4.h
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✝ =
    (((Equiv.ulift.trans e₃).trans Equiv.ulift.symm).toIso.hom ≫ (sq₂.map uliftFunctor.{max u v, u}).f₃₄) a✝

Proof state:
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

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

Result:
no goals

Proof state:
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

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

Result:
no goals