α : Type u_2
β : Type u_1
l✝ : List α
f : α → β
l : List β
hl : l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ l ∈ range (map f)
α : Type u_2
β : Type u_1
l : List α
f : α → β
⊢ range (map f) = {l | ∀ (x : β), x ∈ l → x ∈ range f}
refine'
  antisymm (range_subset_iff.2 fun l => forall_mem_map_iff.2 fun y _ => mem_range_self _)
    fun l hl => _
case nil
α : Type u_2
β : Type u_1
l✝ : List α
f : α → β
l : List β
hl✝ : l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
hl : [] ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ [] ∈ range (map f)

case cons
α : Type u_2
β : Type u_1
l✝¹ : List α
f : α → β
l✝ : List β
hl✝ : l✝ ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
a : β
l : List β
ihl : l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → l ∈ range (map f)
hl : a :: l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ a :: l ∈ range (map f)
α : Type u_2
β : Type u_1
l✝ : List α
f : α → β
l : List β
hl : l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ l ∈ range (map f)
induction' l with a l ihl
case cons.intro
α : Type u_2
β : Type u_1
l✝¹ : List α
f : α → β
l✝ : List β
hl✝ : l✝ ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
a : β
l : List α
ihl : map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → map f l ∈ range (map f)
hl : a :: map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ a :: map f l ∈ range (map f)
case cons
α : Type u_2
β : Type u_1
l✝¹ : List α
f : α → β
l✝ : List β
hl✝ : l✝ ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
a : β
l : List β
ihl : l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → l ∈ range (map f)
hl : a :: l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ a :: l ∈ range (map f)
rcases ihl fun x hx => hl x <| subset_cons _ _ hx with ⟨l, rfl⟩
case cons.intro.intro
α : Type u_2
β : Type u_1
l✝¹ : List α
f : α → β
l✝ : List β
hl✝ : l✝ ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
l : List α
ihl : map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → map f l ∈ range (map f)
a : α
hl : f a :: map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ f a :: map f l ∈ range (map f)
case cons.intro
α : Type u_2
β : Type u_1
l✝¹ : List α
f : α → β
l✝ : List β
hl✝ : l✝ ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
a : β
l : List α
ihl : map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → map f l ∈ range (map f)
hl : a :: map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ a :: map f l ∈ range (map f)
rcases hl a (mem_cons_self _ _) with ⟨a, rfl⟩
no goals
case cons.intro.intro
α : Type u_2
β : Type u_1
l✝¹ : List α
f : α → β
l✝ : List β
hl✝ : l✝ ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
l : List α
ihl : map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f} → map f l ∈ range (map f)
a : α
hl : f a :: map f l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ f a :: map f l ∈ range (map f)
exact ⟨a :: l, map_cons _ _ _⟩
no goals
case nil
α : Type u_2
β : Type u_1
l✝ : List α
f : α → β
l : List β
hl✝ : l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
hl : [] ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ [] ∈ range (map f)
exact ⟨[], rfl⟩