case intro.intro
α✝ : Type ?u.101676
β✝ : Type ?u.101679
γ : Type ?u.101682
ι : Sort ?u.101685
ι' : Sort ?u.101688
s✝ : Set α✝
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
hs : Set.Subsingleton (f ⁻¹' s)
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
⊢ f x = f y
α✝ : Type ?u.101676
β✝ : Type ?u.101679
γ : Type ?u.101682
ι : Sort ?u.101685
ι' : Sort ?u.101688
s✝ : Set α✝
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
hs : Set.Subsingleton (f ⁻¹' s)
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
⊢ fx = fy
rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
no goals
case intro.intro
α✝ : Type ?u.101676
β✝ : Type ?u.101679
γ : Type ?u.101682
ι : Sort ?u.101685
ι' : Sort ?u.101688
s✝ : Set α✝
α : Type u_1
β : Type u_2
f : α → β
hf : Surjective f
s : Set β
hs : Set.Subsingleton (f ⁻¹' s)
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
⊢ f x = f y
exact congr_arg f (hs hx hy)