α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ (#↑t) ≤ (#↑{x | x ∈ s ∧ f x ∈ t})
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ (#↑t) ≤ (#↑{x | x ∈ s ∧ f x ∈ t})
rw [image_eq_range] at h
case h.e'_4
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ (#↑{x | x ∈ s ∧ f x ∈ t}) = (#↑((fun x => f ↑x) ⁻¹' t))
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ (#↑t) ≤ (#↑{x | x ∈ s ∧ f x ∈ t})
convert mk_preimage_of_subset_range _ _ h using 1
case h.e'_4
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ (#↑{x | f ↑x ∈ t}) = (#↑((fun x => f ↑x) ⁻¹' t))
case h.e'_4
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ (#↑{x | x ∈ s ∧ f x ∈ t}) = (#↑((fun x => f ↑x) ⁻¹' t))
rw [mk_sep]
no goals
case h.e'_4
α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ range fun x => f ↑x
⊢ (#↑{x | f ↑x ∈ t}) = (#↑((fun x => f ↑x) ⁻¹' t))
rfl