α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
⊢ False
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
⊢ ¬Surjective f
intro hf
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
⊢ False
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
⊢ False
let T : Type max u v := Sigma f
case intro
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
⊢ False
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
⊢ False
cases' hf (Set T) with U hU
case intro
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
⊢ False
case intro
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
⊢ False
let g : Set T → T := fun s ↦ ⟨U, cast hU.symm s⟩
no goals
case intro
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
hg : Injective g
⊢ False
exact cantor_injective g hg
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
⊢ s = t
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
⊢ Injective g
intro s t h
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
⊢ cast hU (g s).snd = cast hU (g t).snd
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
⊢ s = t
suffices cast hU (g s).2 = cast hU (g t).2 by
  simp only [cast_cast, cast_eq] at this
  assumption
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
this : s = t
⊢ s = t
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
this : cast hU (g s).snd = cast hU (g t).snd
⊢ s = t
simp only [cast_cast, cast_eq] at this
no goals
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
this : s = t
⊢ s = t
assumption
no goals
α✝ : Sort ?u.9302
β : Sort ?u.9305
γ : Sort ?u.9308
f✝ : α✝ → β
α : Type u
f : α → Type (max u v)
hf : Surjective f
T : Type (max u v) := Sigma f
U : α
hU : f U = Set T
g : Set T → T := fun s => { fst := U, snd := cast (_ : Set T = f U) s }
s t : Set T
h : g s = g t
⊢ cast hU (g s).snd = cast hU (g t).snd
congr