Theorem: image_val_range_comp_inclusion (Matroid/ForMathlib/Logic_Embedding_Set.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
s : Set α
t t' : Set β
ht : t ⊆ t'
f : ↑s → ↑t
⊢ ↑(range fun x => inclusion ht (f x)) = ↑(range f)
Tactic:
rw [← image_univ, image_val_image_comp_inclusion]
State after:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
s : Set α
t t' : Set β
ht : t ⊆ t'
f : ↑s → ↑t
⊢ ↑((fun x => f x) '' univ) = ↑(range f)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
s : Set α
t t' : Set β
ht : t ⊆ t'
f : ↑s → ↑t
⊢ ↑((fun x => f x) '' univ) = ↑(range f)
Tactic:
simp
State after:
no goals