awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square (goal)
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}).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₁₃
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square (goal)
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 =
    (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
have 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
Tactic: apply ULift.down_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square (goal)
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}).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₂₄
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square (goal)
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 =
    (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
have 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
Tactic: apply ULift.down_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square (goal)
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}).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₃₄
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square (goal)
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 =
    (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
have 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
Tactic: apply ULift.down_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal (hypothesis)
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 F
have this : HasLimit.{0, 0, v₂, u₂} (Functor.empty D)
Tactic: haveI := HasLimit.mk ⟨_, isLimitOfHasTerminalOfPreservesLimit G⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal (goal)
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 : HasTerminal.{v₂, u₂} D
i : IsIso (X := G.obj (terminal.{v₁, u₁} C)) (Y := terminal.{v₂, u₂} D) (terminalComparison G)
⊢ PreservesLimit (Functor.empty C) G
have apply : IsLimit (G.mapCone (asEmptyCone (terminal.{v₁, u₁} C)))
Tactic: apply preservesLimit_of_preserves_limit_cone terminalIsTerminal
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal (goal)
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 : HasTerminal.{v₂, u₂} D
i : IsIso (X := G.obj (terminal.{v₁, u₁} C)) (Y := terminal.{v₂, u₂} D) (terminalComparison G)
⊢ IsLimit (G.mapCone (asEmptyCone (terminal.{v₁, u₁} C)))
have apply : IsTerminal.{v₂, u₂} (G.obj (terminal.{v₁, u₁} C))
Tactic: apply (isLimitMapConeEmptyConeEquiv _ _).symm _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal (hypothesis)
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 : HasTerminal.{v₂, u₂} D
f : G.obj (terminal.{v₁, u₁} C) ⟶ terminal.{v₂, u₂} D
i : IsIso f
⊢ PreservesLimit (Functor.empty C) G
have i₁ : IsIso (X := G.obj (terminal.{v₁, u₁} C)) (Y := terminal.{v₂, u₂} D) (terminalComparison G)
Tactic: rw [Subsingleton.elim f (terminalComparison G)] at i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal (hypothesis)
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 : HasInitial.{v₁, u₁} C
inst_3 : PreservesColimit (Functor.empty C) G
F : Functor.{0, v₂, 0, u₂} (Discrete PEmpty.{1}) D
⊢ HasColimit F
have this : HasColimit.{0, 0, v₂, u₂} (Functor.empty D)
Tactic: haveI := HasColimit.mk ⟨_, isColimitOfHasInitialOfPreservesColimit G⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal (goal)
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 : HasInitial.{v₁, u₁} C
inst_3 : HasInitial.{v₂, u₂} D
i : IsIso (X := initial.{v₂, u₂} D) (Y := G.obj (initial.{v₁, u₁} C)) (initialComparison G)
⊢ PreservesColimit (Functor.empty C) G
have apply : IsColimit (G.mapCocone (asEmptyCocone (initial.{v₁, u₁} C)))
Tactic: apply preservesColimit_of_preserves_colimit_cocone initialIsInitial
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal (goal)
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 : HasInitial.{v₁, u₁} C
inst_3 : HasInitial.{v₂, u₂} D
i : IsIso (X := initial.{v₂, u₂} D) (Y := G.obj (initial.{v₁, u₁} C)) (initialComparison G)
⊢ IsColimit (G.mapCocone (asEmptyCocone (initial.{v₁, u₁} C)))
have apply : IsInitial.{v₂, u₂} (G.obj (initial.{v₁, u₁} C))
Tactic: apply (isColimitMapCoconeEmptyCoconeEquiv _ _).symm _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal (hypothesis)
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 : HasInitial.{v₁, u₁} C
inst_3 : HasInitial.{v₂, u₂} D
f : initial.{v₂, u₂} D ⟶ G.obj (initial.{v₁, u₁} C)
i : IsIso f
⊢ PreservesColimit (Functor.empty C) G
have i₁ : IsIso (X := initial.{v₂, u₂} D) (Y := G.obj (initial.{v₁, u₁} C)) (initialComparison G)
Tactic: rw [Subsingleton.elim f (initialComparison G)] at i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X : C
hX : IsZero.{v₁, u₁} X
⊢ IsZero.{v₂, u₂} (F.obj X)
have simp : ∀ (hX : Eq.{v₁ + 1} (α := X ⟶ X) (𝟙 X) 0), Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) 0
Tactic: simp only [IsZero.iff_id_eq_zero] at hX ⊢
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X : C
hX : Eq.{v₁ + 1} (α := X ⟶ X) (𝟙 X) 0
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) 0
have rw : F.map (𝟙 X) = 0
Tactic: rw [← F.map_id, hX, F.map_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
inst_2 : HasZeroMorphisms.{v₁, u₁} C
inst_3 : HasZeroMorphisms.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_4 : F.PreservesZeroMorphisms
X : C
hX : Eq.{v₁ + 1} (α := X ⟶ X) (𝟙 X) 0
rw : F.map (𝟙 X) = 0
⊢ Eq.{v₂ + 1} (α := F.obj X ⟶ F.obj X) (𝟙 (F.obj X)) 0
have rw₁ : Eq (α := F.obj X ⟶ F.obj X) (F.map 0) 0
Tactic: rw [← F.map_id, hX, F.map_zero]