α : Sort u_1
β : Sort u_2
γ : Sort ?u.7146
f : α → β
h : (fun y => ∃ x, f x = y) = fun x => True
⊢ Surjective f
α : Sort u_1
β : Sort u_2
γ : Sort ?u.7146
f : α → β
h : ∀ (g₁ g₂ : β → Prop), g₁ ∘ f = g₂ ∘ f → g₁ = g₂
⊢ Surjective f
specialize h (fun y ↦ ∃ x, f x = y) (fun _ ↦ True) (funext fun x ↦ eq_true ⟨_, rfl⟩)
α : Sort u_1
β : Sort u_2
γ : Sort ?u.7146
f : α → β
h : (fun y => ∃ x, f x = y) = fun x => True
y : β
⊢ ∃ a, f a = y
α : Sort u_1
β : Sort u_2
γ : Sort ?u.7146
f : α → β
h : (fun y => ∃ x, f x = y) = fun x => True
⊢ Surjective f
intro y
α : Sort u_1
β : Sort u_2
γ : Sort ?u.7146
f : α → β
h : (fun y => ∃ x, f x = y) = fun x => True
y : β
⊢ True
α : Sort u_1
β : Sort u_2
γ : Sort ?u.7146
f : α → β
h : (fun y => ∃ x, f x = y) = fun x => True
y : β
⊢ ∃ a, f a = y
rw [congr_fun h y]
no goals
α : Sort u_1
β : Sort u_2
γ : Sort ?u.7146
f : α → β
h : (fun y => ∃ x, f x = y) = fun x => True
y : β
⊢ True
trivial