Theorem: Equiv.ofInjective_image (Matroid/ForMathlib/Logic_Embedding_Set.lean)

State before:
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
f : α → β
hf : Injective f
s : Set α
⊢ ↑(⇑(ofInjective f hf) '' s) = f '' s
Tactic:
ext
State after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
f : α → β
hf : Injective f
s : Set α
x✝ : β
⊢ x✝ ∈ ↑(⇑(ofInjective f hf) '' s) ↔ x✝ ∈ f '' s

State before:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
a : α
b : β
s✝ : Set α
f✝ : ↑s✝ ↪ β
f : α → β
hf : Injective f
s : Set α
x✝ : β
⊢ x✝ ∈ ↑(⇑(ofInjective f hf) '' s) ↔ x✝ ∈ f '' s
Tactic:
simp
State after:
no goals