α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ ∃ g, ∀ (x : ↑s), ↑g ↑x = ↑f x
apply extend_function.{v, u} f
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
g : α ≃ β
⊢ Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
cases' id h with g
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift (#α) = lift (#β)
g : α ≃ β
⊢ Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
g : α ≃ β
⊢ Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
rw [← lift_mk_eq.{u, v, max u v}] at h
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift (#α) = lift (#β)
g : α ≃ β
⊢ lift (#↑s) = lift (#↑(range ↑f))
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift (#α) = lift (#β)
g : α ≃ β
⊢ Nonempty (↑(sᶜ) ≃ ↑(range ↑fᶜ))
rw [← lift_mk_eq.{u, v, max u v}, mk_compl_eq_mk_compl_finite_lift.{u, v, max u v} h]
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift (#α) = lift (#β)
g : α ≃ β
⊢ Injective ↑f
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift (#α) = lift (#β)
g : α ≃ β
⊢ lift (#↑s) = lift (#↑(range ↑f))
rw [mk_range_eq_lift.{u, v, max u v}]
no goals
case intro
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift (#α) = lift (#β)
g : α ≃ β
⊢ Injective ↑f
exact f.2