case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.102072
ι : Sort ?u.102075
ι' : Sort ?u.102078
s✝ : Set α
s : Set β
f : α → β
hf : Surjective f
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
hxy : fx ≠ fy
⊢ Set.Nontrivial (f ⁻¹' s)
α : Type u_2
β : Type u_1
γ : Type ?u.102072
ι : Sort ?u.102075
ι' : Sort ?u.102078
s✝ : Set α
s : Set β
hs : Set.Nontrivial s
f : α → β
hf : Surjective f
⊢ Set.Nontrivial (f ⁻¹' s)
rcases hs with ⟨fx, hx, fy, hy, hxy⟩
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.102072
ι : Sort ?u.102075
ι' : Sort ?u.102078
s✝ : Set α
s : Set β
f : α → β
hf : Surjective f
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
hxy : f x ≠ f y
⊢ Set.Nontrivial (f ⁻¹' s)
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.102072
ι : Sort ?u.102075
ι' : Sort ?u.102078
s✝ : Set α
s : Set β
f : α → β
hf : Surjective f
fx : β
hx : fx ∈ s
fy : β
hy : fy ∈ s
hxy : fx ≠ fy
⊢ Set.Nontrivial (f ⁻¹' s)
rcases hf fx, hf fy with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
no goals
case intro.intro.intro.intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.102072
ι : Sort ?u.102075
ι' : Sort ?u.102078
s✝ : Set α
s : Set β
f : α → β
hf : Surjective f
x : α
hx : f x ∈ s
y : α
hy : f y ∈ s
hxy : f x ≠ f y
⊢ Set.Nontrivial (f ⁻¹' s)
exact ⟨x, hx, y, hy, mt (congr_arg f) hxy⟩