Theorem: Set.embeddingOfSubset_image (Matroid/ForMathlib/Logic_Embedding_Set.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f : ↑s✝ ↪ β
s t : Set α
hst : s ⊆ t
r : Set ↑s
⊢ ⇑(s.embeddingOfSubset t hst) '' r = {x | ↑x ∈ ↑r}
Tactic:
ext ⟨x,h⟩
State after:
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f : ↑s✝ ↪ β
s t : Set α
hst : s ⊆ t
r : Set ↑s
x : α
h : x ∈ t
⊢ ⟨x, h⟩ ∈ ⇑(s.embeddingOfSubset t hst) '' r ↔ ⟨x, h⟩ ∈ {x | ↑x ∈ ↑r}

State before:
case h.mk
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f : ↑s✝ ↪ β
s t : Set α
hst : s ⊆ t
r : Set ↑s
x : α
h : x ∈ t
⊢ ⟨x, h⟩ ∈ ⇑(s.embeddingOfSubset t hst) '' r ↔ ⟨x, h⟩ ∈ {x | ↑x ∈ ↑r}
Tactic:
simp [embeddingOfSubset_apply]
State after:
no goals