[GOAL]
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ range (map f) = {l | ∀ (x : β), x ∈ l → x ∈ range f}
[PROOFSTEP]
refine' antisymm (range_subset_iff.2 fun l => forall_mem_map_iff.2 fun y _ => mem_range_self _) fun l hl => _
[GOAL]
α : Type u_1
β : Type u_2
l✝ : List α
f : α → β
l : List β
hl : l ∈ {l | ∀ (x : β), x ∈ l → x ∈ range f}
⊢ l ∈ range (map f)
[PROOFSTEP]
induction' l with a l ihl
[GOAL]
case nil
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
exact ⟨[], rfl⟩
[GOAL]
case cons
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
rcases ihl fun x hx => hl x <| subset_cons _ _ hx with ⟨l, rfl⟩
[GOAL]
case cons.intro
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
rcases hl a (mem_cons_self _ _) with ⟨a, rfl⟩
[GOAL]
case cons.intro.intro
α : Type u_1
β : Type u_2
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)
[PROOFSTEP]
exact ⟨a :: l, map_cons _ _ _⟩
[GOAL]
α : Type u_1
β : Type u_2
l : List α
s : Set α
⊢ range (map Subtype.val) = {l | ∀ (x : α), x ∈ l → x ∈ s}
[PROOFSTEP]
rw [range_list_map, Subtype.range_coe]
[GOAL]
α : Type u_1
β : Type u_2
l : List α
⊢ (range fun k => nthLe l ↑k (_ : ↑k < length l)) = {x | x ∈ l}
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
l : List α
x : α
⊢ (x ∈ range fun k => nthLe l ↑k (_ : ↑k < length l)) ↔ x ∈ {x | x ∈ l}
[PROOFSTEP]
rw [mem_setOf_eq, mem_iff_get]
[GOAL]
case h
α : Type u_1
β : Type u_2
l : List α
x : α
⊢ (x ∈ range fun k => nthLe l ↑k (_ : ↑k < length l)) ↔ ∃ n, List.get l n = x
[PROOFSTEP]
exact ⟨fun ⟨⟨n, h₁⟩, h₂⟩ => ⟨⟨n, h₁⟩, h₂⟩, fun ⟨⟨n, h₁⟩, h₂⟩ => ⟨⟨n, h₁⟩, h₂⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
l : List α
⊢ range (get? l) = insert none (some '' {x | x ∈ l})
[PROOFSTEP]
rw [← range_list_nthLe, ← range_comp]
[GOAL]
α : Type u_1
β : Type u_2
l : List α
⊢ range (get? l) = insert none (range (some ∘ fun k => nthLe l ↑k (_ : ↑k < length l)))
[PROOFSTEP]
refine' (range_subset_iff.2 fun n => _).antisymm (insert_subset_iff.2 ⟨_, _⟩)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
l : List α
n : ℕ
⊢ get? l n ∈ insert none (range (some ∘ fun k => nthLe l ↑k (_ : ↑k < length l)))
case refine'_2
α : Type u_1
β : Type u_2
l : List α
⊢ none ∈ range (get? l)
case refine'_3
α : Type u_1
β : Type u_2
l : List α
⊢ range (some ∘ fun k => nthLe l ↑k (_ : ↑k < length l)) ⊆ range (get? l)
[PROOFSTEP]
exacts [(le_or_lt l.length n).imp get?_eq_none.2 (fun hlt => ⟨⟨_, hlt⟩, (get?_eq_get hlt).symm⟩),
  ⟨_, get?_eq_none.2 le_rfl⟩, range_subset_iff.2 <| fun k => ⟨_, get?_eq_get _⟩]
[GOAL]
α : Type u_1
β : Type u_2
l : List α
d : α
⊢ (range fun n => getD l n d) = (fun o => Option.getD o d) '' range (get? l)
[PROOFSTEP]
simp only [← range_comp, (· ∘ ·), getD_eq_getD_get?]
[GOAL]
α : Type u_1
β : Type u_2
l : List α
d : α
⊢ (fun o => Option.getD o d) '' range (get? l) = insert d {x | x ∈ l}
[PROOFSTEP]
simp only [range_list_get?, image_insert_eq, Option.getD, image_image, image_id']
[GOAL]
α : Type u_1
β : Type u_2
l✝ : List α
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ ∃ y, map c y = l
[PROOFSTEP]
rw [← Set.mem_range, Set.range_list_map]
[GOAL]
α : Type u_1
β : Type u_2
l✝ : List α
c : β → α
p : α → Prop
inst✝ : CanLift α β c p
l : List α
H : ∀ (x : α), x ∈ l → p x
⊢ l ∈ {l | ∀ (x : α), x ∈ l → x ∈ Set.range c}
[PROOFSTEP]
exact fun a ha => CanLift.prf a (H a ha)
