Theorem: image_val_image_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 α
r : Set ↑s
t t' : Set β
ht : t ⊆ t'
f : ↑s → ↑t
⊢ ↑((fun x => inclusion ht (f x)) '' r) = ↑(f '' r)
Tactic:
simp_rw [image_image, coe_inclusion]
State after:
no goals