α : Type u
β : Type v
f : α → β
h : Injective (preimage f)
y : β
⊢ ∃ a, f a = y
α : Type u
β : Type v
f : α → β
⊢ Injective (preimage f) ↔ Surjective f
refine' ⟨fun h y => _, Surjective.preimage_injective⟩
case intro
α : Type u
β : Type v
f : α → β
h : Injective (preimage f)
y : β
x : α
hx : x ∈ f ⁻¹' {y}
⊢ ∃ a, f a = y
α : Type u
β : Type v
f : α → β
h : Injective (preimage f)
y : β
⊢ ∃ a, f a = y
obtain ⟨x, hx⟩ : (f ⁻¹' {y}).Nonempty := by
  rw [h.nonempty_apply_iff preimage_empty]
  apply singleton_nonempty
no goals
case intro
α : Type u
β : Type v
f : α → β
h : Injective (preimage f)
y : β
x : α
hx : x ∈ f ⁻¹' {y}
⊢ ∃ a, f a = y
exact ⟨x, hx⟩
α : Type u
β : Type v
f : α → β
h : Injective (preimage f)
y : β
⊢ Set.Nonempty {y}
α : Type u
β : Type v
f : α → β
h : Injective (preimage f)
y : β
⊢ Set.Nonempty (f ⁻¹' {y})
rw [h.nonempty_apply_iff preimage_empty]
no goals
α : Type u
β : Type v
f : α → β
h : Injective (preimage f)
y : β
⊢ Set.Nonempty {y}
apply singleton_nonempty