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