[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
⊢ r = s
[PROOFSTEP]
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_lt (Cardinal.cantor α)
let yp : C := ∏ fun _ : md => Y
refine' _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
  · intro f
    ext ⟨j⟩
    simp
· apply Cardinal.mk_le_of_injective _
  · intro f
    exact ⟨_, _, f⟩
  · rintro f g k
    cases k
    rfl
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
⊢ r = s
[PROOFSTEP]
by_contra r_ne_s
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ False
[PROOFSTEP]
have z : (2 : Cardinal) ≤ #(X ⟶ Y) := by
  rw [Cardinal.two_le_iff]
  exact ⟨_, _, r_ne_s⟩
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ 2 ≤ #(X ⟶ Y)
[PROOFSTEP]
rw [Cardinal.two_le_iff]
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
⊢ ∃ x y, x ≠ y
[PROOFSTEP]
exact ⟨_, _, r_ne_s⟩
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : HasProducts C
X Y : C
r s : X ⟶ Y
r_ne_s : ¬r = s
z : 2 ≤ #(X ⟶ Y)
⊢ False
[PROOFSTEP]
let md := Σ Z W : C, Z ⟶ W
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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)
⊢ False
[PROOFSTEP]
let α := #md
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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
[PROOFSTEP]
apply not_le_of_lt (Cardinal.cantor α)
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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
⊢ 2 ^ α ≤ α
[PROOFSTEP]
let yp : C := ∏ fun _ : md => Y
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
⊢ 2 ^ α ≤ α
[PROOFSTEP]
refine' _root_.trans _ _
[GOAL]
case refine'_1
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
⊢ Cardinal.{u}
[PROOFSTEP]
exact #(X ⟶ yp)
[GOAL]
case refine'_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
⊢ 2 ^ α ≤ #(X ⟶ yp)
[PROOFSTEP]
apply le_trans (Cardinal.power_le_power_right z)
[GOAL]
case refine'_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
⊢ #(X ⟶ Y) ^ α ≤ #(X ⟶ yp)
[PROOFSTEP]
rw [Cardinal.power_def]
[GOAL]
case refine'_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
⊢ #(md → (X ⟶ Y)) ≤ #(X ⟶ yp)
[PROOFSTEP]
apply le_of_eq
[GOAL]
case refine'_2.a
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
⊢ #(md → (X ⟶ Y)) = #(X ⟶ yp)
[PROOFSTEP]
rw [Cardinal.eq]
[GOAL]
case refine'_2.a
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
⊢ Nonempty ((md → (X ⟶ Y)) ≃ (X ⟶ yp))
[PROOFSTEP]
refine' ⟨⟨Pi.lift, fun f k => f ≫ Pi.π _ k, _, _⟩⟩
[GOAL]
case refine'_2.a.refine'_1
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
⊢ Function.LeftInverse (fun f k => f ≫ Pi.π (fun x => Y) k) Pi.lift
[PROOFSTEP]
intro f
[GOAL]
case refine'_2.a.refine'_1
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
f : md → (X ⟶ Y)
⊢ (fun f k => f ≫ Pi.π (fun x => Y) k) (Pi.lift f) = f
[PROOFSTEP]
ext k
[GOAL]
case refine'_2.a.refine'_1.h
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
f : md → (X ⟶ Y)
k : md
⊢ (fun f k => f ≫ Pi.π (fun x => Y) k) (Pi.lift f) k = f k
[PROOFSTEP]
simp
[GOAL]
case refine'_2.a.refine'_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
⊢ Function.RightInverse (fun f k => f ≫ Pi.π (fun x => Y) k) Pi.lift
[PROOFSTEP]
intro f
[GOAL]
case refine'_2.a.refine'_2
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
f : X ⟶ yp
⊢ Pi.lift ((fun f k => f ≫ Pi.π (fun x => Y) k) f) = f
[PROOFSTEP]
ext ⟨j⟩
[GOAL]
case refine'_2.a.refine'_2.h.mk
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
f : X ⟶ yp
j : C
snd✝ : (W : C) × (j ⟶ W)
⊢ Pi.lift ((fun f k => f ≫ Pi.π (fun x => Y) k) f) ≫ Pi.π (fun a => Y) { fst := j, snd := snd✝ } =
    f ≫ Pi.π (fun a => Y) { fst := j, snd := snd✝ }
[PROOFSTEP]
simp
[GOAL]
case refine'_3
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
⊢ #(X ⟶ yp) ≤ α
[PROOFSTEP]
apply Cardinal.mk_le_of_injective _
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
⊢ (X ⟶ yp) → md
[PROOFSTEP]
intro f
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
f : X ⟶ yp
⊢ md
[PROOFSTEP]
exact ⟨_, _, f⟩
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
⊢ Function.Injective fun f => { fst := X, snd := { fst := yp, snd := f } }
[PROOFSTEP]
rintro f g k
[GOAL]
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
f g : X ⟶ yp
k :
  (fun f => { fst := X, snd := { fst := yp, snd := f } }) f = (fun f => { fst := X, snd := { fst := yp, snd := f } }) g
⊢ f = g
[PROOFSTEP]
cases k
[GOAL]
case refl
C : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 => Y
f : X ⟶ yp
⊢ f = f
[PROOFSTEP]
rfl
