awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_3 :
  ((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_4 :
  ∀ (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_4 :
  ((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₃))
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).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

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

Premises used: CategoryTheory.types_comp, congrFun, CategoryTheory.uliftFunctor_map
-- 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₁
⊢ ((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

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

Premises used: CategoryTheory.types_comp, congrFun, CategoryTheory.uliftFunctor_map
-- 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₂
⊢ ((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

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

Premises used: CategoryTheory.types_comp, congrFun, CategoryTheory.uliftFunctor_map
-- 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₃
⊢ ((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

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

Premises used: CategoryTheory.types_comp, congrFun, CategoryTheory.uliftFunctor_map
-- 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₃))
h₁ : sq₁.IsPullback
⊢ sq₂.IsPullback

Tactic:
(iff_of_equiv sq₁ sq₂ e₁ e₂ e₃ e₄ comm₁₂ comm₁₃ comm₂₄ comm₃₄).1 h₁

Premises used: CategoryTheory.Square.IsPullback.iff_of_equiv, Iff.mp
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasTerminal.{v₁, u₁} C
inst_3 : PreservesLimit (Functor.empty C) G
F : Functor.{0, v₂, 0, u₂} (Discrete PEmpty.{1}) D
⊢ HasLimit.{0, 0, v₂, u₂} (Functor.empty D)

Tactic:
haveI := HasLimit.mk ⟨_, isLimitOfHasTerminalOfPreservesLimit G⟩
-- Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : Functor.{v₁, v₂, u₁, u₂} C D
inst_2 : HasTerminal.{v₁, u₁} C
inst_3 : PreservesLimit (Functor.empty C) G
F : Functor.{0, v₂, 0, u₂} (Discrete PEmpty.{1}) D
this : HasLimit.{0, 0, v₂, u₂} (Functor.empty D)
⊢ HasLimit F

Tactic:
apply hasLimit_of_iso F.uniqueFromEmpty.symm

Premises used: CategoryTheory.Limits.hasLimit_of_iso, CategoryTheory.Functor.uniqueFromEmpty, CategoryTheory.Iso.symm