case inl
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : Nonempty (α ≃ β)
val✝ : Fintype α
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x

case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : Nonempty (α ≃ β)
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
cases fintypeOrInfinite α
no goals
case inl
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : Nonempty (α ≃ β)
val✝ : Fintype α
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
exact extend_function_finite f h
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
apply extend_function f
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
⊢ Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
cases' id h with g
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
⊢ Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
haveI := Infinite.of_injective _ g.injective
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : lift (#α) = lift (#β)
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift (#↑(sᶜ)) = lift (#↑(range ↑fᶜ))
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : Nonempty (α ≃ β)
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
rw [← lift_mk_eq'] at h⊢
case inr.intro.h2
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : lift (#α) = lift (#β)
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ (#↑(range ↑f)) < (#β)
case inr.intro
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : lift (#α) = lift (#β)
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift (#↑(sᶜ)) = lift (#↑(range ↑fᶜ))
rwa [mk_compl_of_infinite s hs, mk_compl_of_infinite]
no goals
case inr.intro.h2
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : (#↑s) < (#α)
h : lift (#α) = lift (#β)
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ (#↑(range ↑f)) < (#β)
rwa [← lift_lt, mk_range_eq_of_injective f.injective, ← h, lift_lt]