Theorem: Set.embeddingOfSubset_preimage (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 ↑t
⊢ ⇑(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 ↑t
x : α
h : x ∈ s
⊢ ⟨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 ↑t
x : α
h : x ∈ s
⊢ ⟨x, h⟩ ∈ ⇑(s.embeddingOfSubset t hst) ⁻¹' r ↔ ⟨x, h⟩ ∈ {x | ↑x ∈ ↑r}
Tactic:
simp [hst h, embeddingOfSubset_apply]
State after:
no goals