awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
⊢ sq.IsPullback ↔ ∀ (X : Cᵒᵖ), (sq.map (Functor.obj coyoneda X)).IsPullback

Tactic:
⟨fun h _ ↦ h.map _, fun h ↦ IsPullback.mk _
    ((sq.pullbackCone.isLimitCoyonedaEquiv).symm (fun X ↦ (h X).isLimit))⟩

Premises used: CategoryTheory.Square.IsPullback.mk, CategoryTheory.Square.f₂₄, CategoryTheory.coyoneda, CategoryTheory.Limits.PullbackCone.isLimitCoyonedaEquiv, CategoryTheory.Square.IsPullback.isLimit, CategoryTheory.Square.pullbackCone, CategoryTheory.Square.f₃₄, CategoryTheory.Square.IsPullback.map, Iff.intro, Equiv.symm, DFunLike.coe, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square
Goal:
C : Type u
inst : Category.{v, u} C
sq : Square.{v, u} C
⊢ sq.IsPushout ↔ ∀ (X : C), (sq.op.map (Functor.obj yoneda X)).IsPullback

Tactic:
⟨fun h _ ↦ h.op.map _, fun h ↦ IsPushout.mk _
    ((sq.pushoutCocone.isColimitYonedaEquiv).symm
      (fun X ↦ IsLimit.ofIsoLimit (h X).isLimit (PullbackCone.ext (Iso.refl _))))⟩

Premises used: CategoryTheory.Square.IsPullback.isLimit, CategoryTheory.Square.IsPushout.mk, CategoryTheory.Square.pushoutCocone, CategoryTheory.Square.op, CategoryTheory.yoneda, CategoryTheory.Iso.refl, CategoryTheory.Limits.Cone.pt, CategoryTheory.Square.pullbackCone, CategoryTheory.Square.map, CategoryTheory.Limits.PullbackCone.ext, CategoryTheory.Square.IsPullback.map, Iff.intro, Equiv.symm, CategoryTheory.Square.IsPushout.op, CategoryTheory.Limits.IsLimit.ofIsoLimit, DFunLike.coe, CategoryTheory.Functor.obj, CategoryTheory.Limits.PushoutCocone.isColimitYonedaEquiv
-- 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₃))
rw : (sq₁.map uliftFunctor.{max u v, v}).IsPullback ↔ (sq₂.map uliftFunctor.{max u v, u}).IsPullback
⊢ sq₁.IsPullback ↔ sq₂.IsPullback

Tactic:
rw [← IsPullback.map_iff sq₁ uliftFunctor.{max u v},
      ← IsPullback.map_iff sq₂ uliftFunctor.{max u v}]
-- 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₃))
⊢ (sq₁.map uliftFunctor.{max u v, v}).IsPullback ↔ (sq₂.map uliftFunctor.{max u v, u}).IsPullback

Tactic:
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: Equiv.trans, CategoryTheory.Square.IsPullback.iff_of_iso, Equiv.ulift, Equiv.toIso, CategoryTheory.Square.isoMk, Equiv.symm
-- 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 :
  ∀ (x : (sq₁.map uliftFunctor.{max u v, v}).X₁),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((sq₁.map uliftFunctor.{max u v, v}).f₁₂ ≫
              ((Equiv.trans Equiv.ulift e₂).trans (Equiv.symm Equiv.ulift)).toIso.hom)).toFun
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (((Equiv.trans Equiv.ulift e₁).trans (Equiv.symm Equiv.ulift)).toIso.hom ≫
              (sq₂.map uliftFunctor.{max u v, u}).f₁₂)).toFun
        x
⊢ (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₁₂

Tactic:
ext
-- 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₃))
x : (sq₁.map uliftFunctor.{max u v, v}).X₁
refine_1 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((sq₁.map uliftFunctor.{max u v, v}).f₁₂ ≫
              ((Equiv.trans Equiv.ulift e₂).trans (Equiv.symm Equiv.ulift)).toIso.hom)).toFun
        x).down =
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((Equiv.trans Equiv.ulift e₁).trans (Equiv.symm Equiv.ulift)).toIso.hom ≫
              (sq₂.map uliftFunctor.{max u v, u}).f₁₂)).toFun
        x).down
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((sq₁.map uliftFunctor.{max u v, v}).f₁₂ ≫
            ((Equiv.trans Equiv.ulift e₂).trans (Equiv.symm Equiv.ulift)).toIso.hom)).toFun
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (((Equiv.trans Equiv.ulift e₁).trans (Equiv.symm Equiv.ulift)).toIso.hom ≫
            (sq₂.map uliftFunctor.{max u v, u}).f₁₂)).toFun
      x

Tactic:
apply ULift.down_injective

Premises used: ULift.down_injective
-- 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_2 :
  ∀ (x : (sq₁.map uliftFunctor.{max u v, v}).X₁),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((sq₁.map uliftFunctor.{max u v, v}).f₁₃ ≫
              ((Equiv.trans Equiv.ulift e₃).trans (Equiv.symm Equiv.ulift)).toIso.hom)).toFun
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (((Equiv.trans Equiv.ulift e₁).trans (Equiv.symm Equiv.ulift)).toIso.hom ≫
              (sq₂.map uliftFunctor.{max u v, u}).f₁₃)).toFun
        x
⊢ (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₁₃

Tactic:
ext
-- 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₃))
x : (sq₁.map uliftFunctor.{max u v, v}).X₁
refine_2 :
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
            ((sq₁.map uliftFunctor.{max u v, v}).f₁₃ ≫
              ((Equiv.trans Equiv.ulift e₃).trans (Equiv.symm Equiv.ulift)).toIso.hom)).toFun
        x).down =
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (((Equiv.trans Equiv.ulift e₁).trans (Equiv.symm Equiv.ulift)).toIso.hom ≫
              (sq₂.map uliftFunctor.{max u v, u}).f₁₃)).toFun
        x).down
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun)
          ((sq₁.map uliftFunctor.{max u v, v}).f₁₃ ≫
            ((Equiv.trans Equiv.ulift e₃).trans (Equiv.symm Equiv.ulift)).toIso.hom)).toFun
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun)
          (((Equiv.trans Equiv.ulift e₁).trans (Equiv.symm Equiv.ulift)).toIso.hom ≫
            (sq₂.map uliftFunctor.{max u v, u}).f₁₃)).toFun
      x

Tactic:
apply ULift.down_injective

Premises used: ULift.down_injective
-- 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_3 :
  ∀ (x : (sq₁.map uliftFunctor.{max u v, v}).X₂),
    (ConcreteCategory.hom (FC := TypeCat.Fun)
            ((sq₁.map uliftFunctor.{max u v, v}).f₂₄ ≫
              ((Equiv.trans Equiv.ulift e₄).trans (Equiv.symm Equiv.ulift)).toIso.hom)).toFun
        x =
      (ConcreteCategory.hom (FC := TypeCat.Fun)
            (((Equiv.trans Equiv.ulift e₂).trans (Equiv.symm Equiv.ulift)).toIso.hom ≫
              (sq₂.map uliftFunctor.{max u v, u}).f₂₄)).toFun
        x
⊢ (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₂₄

Tactic:
ext