awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (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
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ Eq (α :=
    (span ((span f g ⋙ G).map WalkingSpan.Hom.fst) ((span f g ⋙ G).map WalkingSpan.Hom.snd)).obj none ⟶
      (PushoutCocone.mk (G.map h) (G.map k) ⋯).pt)
    (((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
        none ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt))
    ((PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app none)
have none : (𝟙 (G.obj W) ≫ G.map (f ≫ h)) ≫ 𝟙 (G.obj Z) = G.map f ≫ G.map h
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (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
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ Eq (α :=
    (span ((span f g ⋙ G).map WalkingSpan.Hom.fst) ((span f g ⋙ G).map WalkingSpan.Hom.snd)).obj
        (some WalkingPair.left) ⟶
      (PushoutCocone.mk (G.map h) (G.map k) ⋯).pt)
    (((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
        (some WalkingPair.left) ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt))
    ((PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app (some WalkingPair.left))
have some : (𝟙 (G.obj X) ≫ G.map h) ≫ 𝟙 (G.obj Z) = G.map h
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (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
W X Y Z : C
h : X ⟶ Z
k : Y ⟶ Z
f : W ⟶ X
g : W ⟶ Y
comm : f ≫ h = g ≫ k
⊢ Eq (α :=
    (span ((span f g ⋙ G).map WalkingSpan.Hom.fst) ((span f g ⋙ G).map WalkingSpan.Hom.snd)).obj
        (some WalkingPair.right) ⟶
      (PushoutCocone.mk (G.map h) (G.map k) ⋯).pt)
    (((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj (G.mapCocone (PushoutCocone.mk h k comm))).ι.app
        (some WalkingPair.right) ≫
      Iso.hom
        (Iso.refl
          ((Cocone.precompose (diagramIsoSpan (span f g ⋙ G)).symm.hom).obj
              (G.mapCocone (PushoutCocone.mk h k comm))).pt))
    ((PushoutCocone.mk (G.map h) (G.map k) ⋯).ι.app (some WalkingPair.right))
have some : (𝟙 (G.obj Y) ≫ G.map k) ≫ 𝟙 (G.obj Z) = G.map k
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (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
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (G.mapCocone c)
have apply : IsColimit ((Cocone.precompose (diagramIsoSpan (span g f ⋙ G)).symm.hom).obj (G.mapCocone c))
Tactic: apply (IsColimit.precomposeHomEquiv (diagramIsoSpan.{v₂} _).symm _).toFun
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (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
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit ((Cocone.precompose (diagramIsoSpan (span g f ⋙ G)).symm.hom).obj (G.mapCocone c))
have apply : IsColimit (PushoutCocone.mk ((G.mapCocone c).ι.app WalkingSpan.left) ((G.mapCocone c).ι.app WalkingSpan.right) sorry)
Tactic: apply IsColimit.ofIsoColimit _ (PushoutCocone.isoMk _).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (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
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (PushoutCocone.mk ((G.mapCocone c).ι.app WalkingSpan.left) ((G.mapCocone c).ι.app WalkingSpan.right) ⋯)
have ht : IsColimit (PushoutCocone.mk ((G.mapCocone c).ι.app WalkingSpan.left) ((G.mapCocone c).ι.app WalkingSpan.right) sorry).flip
Tactic: apply PushoutCocone.isColimitOfFlip
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (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
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
⊢ IsColimit (PushoutCocone.mk ((G.mapCocone c).ι.app WalkingSpan.left) ((G.mapCocone c).ι.app WalkingSpan.right) ⋯).flip
have ht : IsColimit (G.mapCocone (PushoutCocone.mk (c.ι.app WalkingSpan.right) (c.ι.app WalkingSpan.left) sorry))
Tactic: apply (isColimitMapCoconePushoutCoconeEquiv _ _).toFun
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (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
W X Y : C
f : W ⟶ X
g : W ⟶ Y
inst_2 : PreservesColimit (span f g) G
c : Cocone (span g f)
hc : IsColimit c
ht : IsColimit (G.mapCocone (PushoutCocone.mk (c.ι.app WalkingSpan.right) (c.ι.app WalkingSpan.left) ⋯))
⊢ IsColimit (PushoutCocone.mk ((G.mapCocone c).ι.app WalkingSpan.left) ((G.mapCocone c).ι.app WalkingSpan.right) ⋯).flip
have apply : (span g f).map WalkingSpan.Hom.snd ≫ c.ι.app WalkingSpan.right =
  (span g f).map WalkingSpan.Hom.fst ≫ c.ι.app WalkingSpan.left
Tactic: apply (isColimitMapCoconePushoutCoconeEquiv _ _).toFun
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
i : IsIso (X := G.obj (pullback f g)) (Y := pullback (G.map f) (G.map g)) (pullbackComparison G f g)
⊢ PreservesLimit (cospan f g) G
have apply : IsLimit (G.mapCone (PullbackCone.mk (W := pullback f g) (pullback.fst f g) (pullback.snd f g) sorry))
Tactic: apply preservesLimit_of_preserves_limit_cone (pullbackIsPullback f g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (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
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst_2 : HasPullback f g
inst_3 : HasPullback (G.map f) (G.map g)
i : IsIso (X := G.obj (pullback f g)) (Y := pullback (G.map f) (G.map g)) (pullbackComparison G f g)
⊢ IsLimit (G.mapCone (PullbackCone.mk (W := pullback f g) (pullback.fst f g) (pullback.snd f g) ⋯))
have apply : IsLimit (PullbackCone.mk (W := G.obj (pullback f g)) (G.map (pullback.fst f g)) (G.map (pullback.snd f g)) sorry)
Tactic: apply (isLimitMapConePullbackConeEquiv _ _).symm _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (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
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
i : IsIso (X := pushout (G.map f) (G.map g)) (Y := G.obj (pushout f g)) (pushoutComparison G f g)
⊢ PreservesColimit (span f g) G
have apply : IsColimit (G.mapCocone (PushoutCocone.mk (W := pushout f g) (pushout.inl f g) (pushout.inr f g) sorry))
Tactic: apply preservesColimit_of_preserves_colimit_cocone (pushoutIsPushout f g)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks (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
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
inst_2 : HasPushout f g
inst_3 : HasPushout (G.map f) (G.map g)
i : IsIso (X := pushout (G.map f) (G.map g)) (Y := G.obj (pushout f g)) (pushoutComparison G f g)
⊢ IsColimit (G.mapCocone (PushoutCocone.mk (W := pushout f g) (pushout.inl f g) (pushout.inr f g) ⋯))
have apply : IsColimit (PushoutCocone.mk (W := G.obj (pushout f g)) (G.map (pushout.inl f g)) (G.map (pushout.inr f g)) sorry)
Tactic: apply (isColimitMapCoconePushoutCoconeEquiv _ _).symm _
-- 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₁.IsPullback ↔ sq₂.IsPullback
have rw : (sq₁.map uliftFunctor.{max u v, v}).IsPullback ↔ (sq₂.map uliftFunctor.{max u v, u}).IsPullback
Tactic: rw [← IsPullback.map_iff sq₁ uliftFunctor.{max u v},
      ← IsPullback.map_iff sq₂ uliftFunctor.{max u v}]
-- 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}).IsPullback ↔ (sq₂.map uliftFunctor.{max u v, u}).IsPullback
have refine_1 : (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: 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)
    ?_ ?_ ?_ ?_)
-- 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₃))
refine_1 :
  (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₁₂
⊢ (sq₁.map uliftFunctor.{max u v, v}).IsPullback ↔ (sq₂.map uliftFunctor.{max u v, u}).IsPullback
have refine_2 : (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: 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)
    ?_ ?_ ?_ ?_)
-- 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_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
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_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
Tactic: apply ULift.down_injective