α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Nonempty (↑(f ⁻¹' s) ↪ ↑s)
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ lift (#↑(f ⁻¹' s)) ≤ lift (#↑s)
rw [lift_mk_le.{u, v, 0}]
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective (Subtype.coind (fun x => f ↑x) (_ : ∀ (x : ↑(f ⁻¹' s)), f ↑x ∈ s))
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Nonempty (↑(f ⁻¹' s) ↪ ↑s)
use Subtype.coind (fun x => f x.1) fun x => mem_preimage.mp x.2
case hf
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective fun x => f ↑x
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective (Subtype.coind (fun x => f ↑x) (_ : ∀ (x : ↑(f ⁻¹' s)), f ↑x ∈ s))
apply Subtype.coind_injective
no goals
case hf
α✝ β✝ α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective fun x => f ↑x
exact h.comp Subtype.val_injective