ι : Type ?u.9936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ → l₁ ⊆ l₂
ι : Type ?u.9936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ ↔ l₁ ⊆ l₂
refine' ⟨_, map_subset f⟩
ι : Type ?u.9936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
⊢ x ∈ l₂
ι : Type ?u.9936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
f : α → β
h : Injective f
⊢ map f l₁ ⊆ map f l₂ → l₁ ⊆ l₂
intro h2 x hx
case intro.intro
ι : Type ?u.9936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
x' : α
hx' : x' ∈ l₂
hxx' : f x' = f x
⊢ x ∈ l₂
ι : Type ?u.9936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
⊢ x ∈ l₂
rcases mem_map.1 (h2 (mem_map_of_mem f hx)) with ⟨x', hx', hxx'⟩
case intro.intro.refl
ι : Type ?u.9936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
hx' : x ∈ l₂
hxx' : f x = f x
⊢ x ∈ l₂
case intro.intro
ι : Type ?u.9936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
x' : α
hx' : x' ∈ l₂
hxx' : f x' = f x
⊢ x ∈ l₂
cases h hxx'
no goals
case intro.intro.refl
ι : Type ?u.9936
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁✝ l₂✝ l₁ l₂ : List α
f : α → β
h : Injective f
h2 : map f l₁ ⊆ map f l₂
x : α
hx : x ∈ l₁
hx' : x ∈ l₂
hxx' : f x = f x
⊢ x ∈ l₂
exact hx'