awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
X Y : C ⥤ Type u
inst_1 : IsSifted C
⊢ PUnit.{u + 1} ≅ obj (C := C ⥤ Type u) colim (⊤_ C ⥤ Type u)
have t : (k : C) →
  IsLimit (F := comp (D := C ⥤ Type u) (empty (C ⥤ Type u)) (obj (evaluation C (Type u)) k))
    (mapCone (obj (evaluation C (Type u)) k) (asEmptyCone (Types.constPUnitFunctor C)))
Tactic: apply_rules [(Types.colimitConstPUnitIsoPUnit C).symm.trans, HasColimit.isoOfNatIso,
      IsTerminal.uniqueUpToIso _ terminalIsTerminal, evaluationJointlyReflectsLimits]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete WalkingPair) colim
⊢ IsSiftedOrEmpty C
have I : (d : C × C) → colimit (Functor.diag C ⋙ obj coyoneda (op d)) ≅ PUnit.{u + 1}
Tactic: apply final_of_colimit_comp_coyoneda_iso_pUnit
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
⊢ Nonempty C
have suffices : IsConnected C
Tactic: suffices connected : IsConnected C by infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
⊢ IsConnected C
have rw : Nonempty.{u + 1} (colimit (Types.constPUnitFunctor C) ≅ PUnit.{u + 1})
Tactic: rw [Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
⊢ Nonempty.{u + 1} (colimit (Types.constPUnitFunctor C) ≅ PUnit.{u + 1})
have val : colimit (Types.constPUnitFunctor C) ≅ PUnit.{u + 1}
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (hypothesis)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
⊢ colimit (Types.constPUnitFunctor C) ≅ PUnit.{u + 1}
have this : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete PEmpty.{1}) colim
Tactic: haveI : PreservesLimitsOfShape (Discrete PEmpty) (colim : (C ⥤ _) ⥤ Type u) :=
    preservesLimitsOfShape_of_equiv (Discrete.equivalence finZeroEquiv') _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete PEmpty.{1}) colim
⊢ colimit (Types.constPUnitFunctor C) ≅ PUnit.{u + 1}
have val : colimit (J := C) (⊤_ C ⥤ Type u) ≅ PUnit.{u + 1}
Tactic: apply HasColimit.isoOfNatIso (_ : Types.constPUnitFunctor C ≅ (⊤_ (C ⥤ Type u))) |>.trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete PEmpty.{1}) colim
val : colimit (J := C) (⊤_ C ⥤ Type u) ≅ PUnit.{u + 1}
⊢ colimit (Types.constPUnitFunctor C) ≅ PUnit.{u + 1}
have apply : Iso (C := C ⥤ Type u) (Types.constPUnitFunctor C) (⊤_ C ⥤ Type u)
Tactic: apply HasColimit.isoOfNatIso (_ : Types.constPUnitFunctor C ≅ (⊤_ (C ⥤ Type u))) |>.trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete PEmpty.{1}) colim
⊢ colimit (J := C) (⊤_ C ⥤ Type u) ≅ PUnit.{u + 1}
have val : ⊤_ Type u ≅ PUnit.{u + 1}
Tactic: apply PreservesTerminal.iso colim |>.trans
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete (Fin 0)) colim
this : PreservesLimitsOfShape.{0, 0, u, u, u + 1, u + 1} (C := C ⥤ Type u) (Discrete PEmpty.{1}) colim
⊢ Iso (C := C ⥤ Type u) (Types.constPUnitFunctor C) (⊤_ C ⥤ Type u)
have t : (k : C) →
  IsLimit (F := comp (D := C ⥤ Type u) (empty (C ⥤ Type u)) (obj (evaluation C (Type u)) k))
    (mapCone (obj (evaluation C (Type u)) k) (asEmptyCone (Types.constPUnitFunctor C)))
Tactic: apply_rules [IsTerminal.uniqueUpToIso _ terminalIsTerminal, evaluationJointlyReflectsLimits]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (hypothesis)
Goal:
C : Type u
inst : SmallCategory C
h : PreservesFiniteProducts.{u, u, u + 1, u + 1} (C := C ⥤ Type u) colim
⊢ IsSifted C
have this : IsSiftedOrEmpty C
Tactic: have := isSiftedOrEmpty_of_colim_preservesFiniteProducts C
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (hypothesis)
Goal:
C : Type u
inst : SmallCategory C
h : PreservesFiniteProducts.{u, u, u + 1, u + 1} (C := C ⥤ Type u) colim
this : IsSiftedOrEmpty C
⊢ IsSifted C
have this₁ : Nonempty C
Tactic: have := nonempty_of_colim_preservesLimitsOfShapeFinZero C
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (hypothesis)
Goal:
C : Type u
inst : SmallCategory C
D : Type u
inst_1 : SmallCategory D
inst_2 : IsSifted C
F : C ⥤ D
inst_3 : F.Final
⊢ IsSifted D
have this : PreservesFiniteProducts.{u, u, u + 1, u + 1} (C := D ⥤ Type u) colim
Tactic: have : PreservesFiniteProducts (colim : (D ⥤ Type u) ⥤ _) :=
    ⟨fun n ↦ preservesLimitsOfShape_of_natIso (Final.colimIso F)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Sifted (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₁
inst_1 : Category.{v₁, u₁} D
h₁ : IsSifted.{v, u} C
F : Functor.{v, v₁, u, u₁} C D
inst_2 : F.Final
⊢ IsSifted.{v₁, u₁} D
have rw : ∀ (h₁ : IsSifted (AsSmall C)) (F : Functor.{v, v₁, u, u₁} C D) [F.Final], IsSifted (AsSmall D)
Tactic: rw [isSifted_iff_asSmallIsSifted] at h₁ ⊢
Cleared hypotheses: h₁, F, inst_2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
⊢ r = s
have by_contra : ∀ (r_ne_s : ¬r = s), False
Tactic: by_contra r_ne_s
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ 2 ≤ #(X ⟶ Y)
have rw : ∃ (x : X ⟶ Y) (y : X ⟶ Y), x ≠ y
Tactic: rw [Cardinal.two_le_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (hypothesis)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ False
have z : 2 ≤ #(X ⟶ Y)
Tactic: have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
        rw [Cardinal.two_le_iff]
        exact ⟨_, _, r_ne_s⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
⊢ False
have apply : HPow.hPow (α := Cardinal.{u}) 2 α ≤ α
Tactic: apply not_le_of_gt (Cardinal.cantor α)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
apply : Cardinal.{u}
⊢ HPow.hPow (α := Cardinal.{u}) 2 α ≤ α
have apply₁ : HPow.hPow (α := Cardinal.{u}) 2 α ≤ #(X ⟶ yp)
Tactic: apply _root_.trans _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
apply : Cardinal.{u}
apply₁ : HPow.hPow (α := Cardinal.{u}) 2 α ≤ #(X ⟶ yp)
⊢ HPow.hPow (α := Cardinal.{u}) 2 α ≤ α
have apply₂ : #(X ⟶ yp) ≤ α
Tactic: apply _root_.trans _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
⊢ HPow.hPow (α := Cardinal.{u}) 2 α ≤ #(X ⟶ yp)
have apply : #(X ⟶ Y) ^ α ≤ #(X ⟶ yp)
Tactic: apply le_trans (Cardinal.power_le_power_right z)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
⊢ #(X ⟶ Y) ^ α ≤ #(X ⟶ yp)
have rw : #(md → (X ⟶ Y)) ≤ #(X ⟶ yp)
Tactic: rw [Cardinal.power_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
⊢ #(md → (X ⟶ Y)) ≤ #(X ⟶ yp)
have hab : #(md → (X ⟶ Y)) = #(X ⟶ yp)
Tactic: apply le_of_eq
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
⊢ #(md → (X ⟶ Y)) = #(X ⟶ yp)
have hab : Nonempty.{u + 1} ((md → (X ⟶ Y)) ≃ (X ⟶ yp))
Tactic: rw [Cardinal.eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
⊢ Nonempty.{u + 1} ((md → (X ⟶ Y)) ≃ (X ⟶ yp))
have hab : Function.LeftInverse (fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) Pi.lift
Tactic: refine ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
hab : Function.LeftInverse (fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) Pi.lift
⊢ Nonempty.{u + 1} ((md → (X ⟶ Y)) ≃ (X ⟶ yp))
have hab₁ : Function.RightInverse (fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) Pi.lift
Tactic: refine ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, ?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
f : md → (X ⟶ Y)
⊢ (fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) (Pi.lift f) = f
have hab : ∀ (k : md), (fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) (Pi.lift f) k = f k
Tactic: ext k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
f : X ⟶ yp
⊢ Pi.lift ((fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) f) = f
have hab : ∀ (j : C) (snd : (W : C) × (j ⟶ W)),
  CategoryStruct.comp (Y := ∏ᶜ fun (a : md) ↦ Y)
      (Pi.lift ((fun (f : X ⟶ yp) (k : md) ↦ f ≫ Pi.π (fun (x : md) ↦ Y) k) f))
      (Pi.π (fun (a : md) ↦ Y) (Sigma.mk (β := fun (Z : C) ↦ (W : C) × (Z ⟶ W)) j snd)) =
    f ≫ Pi.π (fun (a : md) ↦ Y) (Sigma.mk (β := fun (Z : C) ↦ (W : C) × (Z ⟶ W)) j snd)
Tactic: ext ⟨j⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
⊢ #(X ⟶ yp) ≤ α
have apply : (X ⟶ yp) → md
Tactic: apply Cardinal.mk_le_of_injective _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
apply : (X ⟶ yp) → md
⊢ #(X ⟶ yp) ≤ α
have apply₁ : Function.Injective (β := md) fun (f : X ⟶ yp) ↦
  Sigma.mk (β := fun (Z : C) ↦ (W : C) × (Z ⟶ W)) X (Sigma.mk (β := fun (W : C) ↦ X ⟶ W) yp f)
Tactic: apply Cardinal.mk_le_of_injective _
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
md : Type u := (Z : C) × (W : C) × (Z ⟶ W)
α : Cardinal.{u} := #md
yp : C := ∏ᶜ fun (x : md) ↦ Y
f g : X ⟶ yp
k :
  Eq.{u + 1} (α := md)
    ((fun (f : X ⟶ yp) ↦
        (Sigma.mk (β := fun (Z : C) ↦ (W : C) × (Z ⟶ W)) X (Sigma.mk (β := fun (W : C) ↦ X ⟶ W) yp f) :
          (Z : C) × (W : C) × (Z ⟶ W)))
      f)
    ((fun (f : X ⟶ yp) ↦
        (Sigma.mk (β := fun (Z : C) ↦ (W : C) × (Z ⟶ W)) X (Sigma.mk (β := fun (W : C) ↦ X ⟶ W) yp f) :
          (Z : C) × (W : C) × (Z ⟶ W)))
      g)
⊢ f = g
have refl : f = f
Tactic: cases k
Cleared hypotheses: g, k
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
⊢ r = s
have by_contra : ¬r = s → False
Tactic: classical
      by_contra r_ne_s
      have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
        rw [Cardinal.two_le_iff]
        exact ⟨_, _, r_ne_s⟩
      let md := Σ Z W : C, Z ⟶ W
      let α := #md
      apply not_le_of_gt (Cardinal.cantor α)
      let yp : C := ∏ᶜ fun _ : md => Y
      apply _root_.trans _ _
      · exact #(X ⟶ yp)
      · apply le_trans (Cardinal.power_le_power_right z)
        rw [Cardinal.power_def]
        apply le_of_eq
        rw [Cardinal.eq]
        refine ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, ?_, ?_⟩⟩
        · intro f
          ext k
          simp [yp]
        · intro f
          ext ⟨j⟩
          simp [yp]
      · apply Cardinal.mk_le_of_injective _
        · intro f
          exact ⟨_, _, f⟩
        · rintro f g k
          cases k
          rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
by_contra by_contra₁ by_contra₂ : ∀ (r_ne_s : ¬r = s), False
⊢ r = s
have by_contra₃ : ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)), False
Tactic: classical
      by_contra r_ne_s
      have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
        rw [Cardinal.two_le_iff]
        exact ⟨_, _, r_ne_s⟩
      let md := Σ Z W : C, Z ⟶ W
      let α := #md
      apply not_le_of_gt (Cardinal.cantor α)
      let yp : C := ∏ᶜ fun _ : md => Y
      apply _root_.trans _ _
      · exact #(X ⟶ yp)
      · apply le_trans (Cardinal.power_le_power_right z)
        rw [Cardinal.power_def]
        apply le_of_eq
        rw [Cardinal.eq]
        refine ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, ?_, ?_⟩⟩
        · intro f
          ext k
          simp [yp]
        · intro f
          ext ⟨j⟩
          simp [yp]
      · apply Cardinal.mk_le_of_injective _
        · intro f
          exact ⟨_, _, f⟩
        · rintro f g k
          cases k
          rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
by_contra by_contra₁ by_contra₂ : ∀ (r_ne_s : ¬r = s), False
by_contra₃ by_contra₄ by_contra₅ : ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)), False
⊢ r = s
have by_contra₆ : ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
  let md := (Z : C) × (W : C) × (Z ⟶ W);
  let α := #md;
  HPow.hPow (α := Cardinal.{u}) 2 α ≤ α
Tactic: classical
      by_contra r_ne_s
      have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
        rw [Cardinal.two_le_iff]
        exact ⟨_, _, r_ne_s⟩
      let md := Σ Z W : C, Z ⟶ W
      let α := #md
      apply not_le_of_gt (Cardinal.cantor α)
      let yp : C := ∏ᶜ fun _ : md => Y
      apply _root_.trans _ _
      · exact #(X ⟶ yp)
      · apply le_trans (Cardinal.power_le_power_right z)
        rw [Cardinal.power_def]
        apply le_of_eq
        rw [Cardinal.eq]
        refine ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, ?_, ?_⟩⟩
        · intro f
          ext k
          simp [yp]
        · intro f
          ext ⟨j⟩
          simp [yp]
      · apply Cardinal.mk_le_of_injective _
        · intro f
          exact ⟨_, _, f⟩
        · rintro f g k
          cases k
          rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
by_contra by_contra₁ by_contra₂ : ∀ (r_ne_s : ¬r = s), False
by_contra₃ by_contra₄ by_contra₅ : ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)), False
by_contra₆ :
  ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
    let md := (Z : C) × (W : C) × (Z ⟶ W);
    let α := #md;
    HPow.hPow (α := Cardinal.{u}) 2 α ≤ α
by_contra₇ :
  ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
    let md := (Z : C) × (W : C) × (Z ⟶ W);
    let α := #md;
    HPow.hPow (α := Cardinal.{u}) 2 α ≤ α
⊢ r = s
have by_contra₈ : (r_ne_s : ¬r = s) → (z : 2 ≤ #(X ⟶ Y)) → Cardinal.{u}
Tactic: classical
      by_contra r_ne_s
      have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
        rw [Cardinal.two_le_iff]
        exact ⟨_, _, r_ne_s⟩
      let md := Σ Z W : C, Z ⟶ W
      let α := #md
      apply not_le_of_gt (Cardinal.cantor α)
      let yp : C := ∏ᶜ fun _ : md => Y
      apply _root_.trans _ _
      · exact #(X ⟶ yp)
      · apply le_trans (Cardinal.power_le_power_right z)
        rw [Cardinal.power_def]
        apply le_of_eq
        rw [Cardinal.eq]
        refine ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, ?_, ?_⟩⟩
        · intro f
          ext k
          simp [yp]
        · intro f
          ext ⟨j⟩
          simp [yp]
      · apply Cardinal.mk_le_of_injective _
        · intro f
          exact ⟨_, _, f⟩
        · rintro f g k
          cases k
          rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
by_contra by_contra₁ by_contra₂ : ∀ (r_ne_s : ¬r = s), False
by_contra₃ by_contra₄ by_contra₅ : ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)), False
by_contra₆ :
  ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
    let md := (Z : C) × (W : C) × (Z ⟶ W);
    let α := #md;
    HPow.hPow (α := Cardinal.{u}) 2 α ≤ α
by_contra₇ :
  ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
    let md := (Z : C) × (W : C) × (Z ⟶ W);
    let α := #md;
    HPow.hPow (α := Cardinal.{u}) 2 α ≤ α
by_contra₈ : (r_ne_s : ¬r = s) → (z : 2 ≤ #(X ⟶ Y)) → Cardinal.{u}
⊢ r = s
have by_contra₉ : ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
  let md := (Z : C) × (W : C) × (Z ⟶ W);
  let α := #md;
  let yp : C := ∏ᶜ fun (x : md) ↦ Y;
  HPow.hPow (α := Cardinal.{u}) 2 α ≤ #(X ⟶ yp)
Tactic: classical
      by_contra r_ne_s
      have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
        rw [Cardinal.two_le_iff]
        exact ⟨_, _, r_ne_s⟩
      let md := Σ Z W : C, Z ⟶ W
      let α := #md
      apply not_le_of_gt (Cardinal.cantor α)
      let yp : C := ∏ᶜ fun _ : md => Y
      apply _root_.trans _ _
      · exact #(X ⟶ yp)
      · apply le_trans (Cardinal.power_le_power_right z)
        rw [Cardinal.power_def]
        apply le_of_eq
        rw [Cardinal.eq]
        refine ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, ?_, ?_⟩⟩
        · intro f
          ext k
          simp [yp]
        · intro f
          ext ⟨j⟩
          simp [yp]
      · apply Cardinal.mk_le_of_injective _
        · intro f
          exact ⟨_, _, f⟩
        · rintro f g k
          cases k
          rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.SmallComplete (goal)
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasProducts C
X Y : C
r s : X ⟶ Y
by_contra by_contra₁ by_contra₂ : ∀ (r_ne_s : ¬r = s), False
by_contra₃ by_contra₄ by_contra₅ : ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)), False
by_contra₆ :
  ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
    let md := (Z : C) × (W : C) × (Z ⟶ W);
    let α := #md;
    HPow.hPow (α := Cardinal.{u}) 2 α ≤ α
by_contra₇ :
  ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
    let md := (Z : C) × (W : C) × (Z ⟶ W);
    let α := #md;
    HPow.hPow (α := Cardinal.{u}) 2 α ≤ α
by_contra₈ : (r_ne_s : ¬r = s) → (z : 2 ≤ #(X ⟶ Y)) → Cardinal.{u}
by_contra₉ :
  ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
    let md := (Z : C) × (W : C) × (Z ⟶ W);
    let α := #md;
    let yp : C := ∏ᶜ fun (x : md) ↦ Y;
    HPow.hPow (α := Cardinal.{u}) 2 α ≤ #(X ⟶ yp)
⊢ r = s
have by_contra₁₀ : ∀ (r_ne_s : ¬r = s) (z : 2 ≤ #(X ⟶ Y)),
  let md := (Z : C) × (W : C) × (Z ⟶ W);
  let α := #md;
  let yp : C := ∏ᶜ fun (x : md) ↦ Y;
  #(X ⟶ yp) ≤ α
Tactic: classical
      by_contra r_ne_s
      have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
        rw [Cardinal.two_le_iff]
        exact ⟨_, _, r_ne_s⟩
      let md := Σ Z W : C, Z ⟶ W
      let α := #md
      apply not_le_of_gt (Cardinal.cantor α)
      let yp : C := ∏ᶜ fun _ : md => Y
      apply _root_.trans _ _
      · exact #(X ⟶ yp)
      · apply le_trans (Cardinal.power_le_power_right z)
        rw [Cardinal.power_def]
        apply le_of_eq
        rw [Cardinal.eq]
        refine ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, ?_, ?_⟩⟩
        · intro f
          ext k
          simp [yp]
        · intro f
          ext ⟨j⟩
          simp [yp]
      · apply Cardinal.mk_le_of_injective _
        · intro f
          exact ⟨_, _, f⟩
        · rintro f g k
          cases k
          rfl
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Types.Coequalizers (goal)
Goal:
X Y Z : Type u
f g : X ⟶ Y
⊢ Eq (α :=
    X ⟶
      Function.Coequalizer (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
        (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
    (f ≫
      ↾Function.Coequalizer.mk
          (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
          (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
    (g ≫
      ↾Function.Coequalizer.mk
          (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
          (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
have h : ∀ (x : X),
  Eq (α :=
    Function.Coequalizer (α := (fun (X : Type u) ↦ X) X) (β := (fun (X : Type u) ↦ X) Y)
      (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
      (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y))
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (f ≫
          ↾Function.Coequalizer.mk
              (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
              (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)))
      x)
    (TypeCat.Fun.toFun
      (hom (FC := TypeCat.Fun)
        (g ≫
          ↾Function.Coequalizer.mk
              (⇑(hom (FC := TypeCat.Fun) f) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)
              (⇑(hom (FC := TypeCat.Fun) g) : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y)))
      x)
Tactic: ext x