/- To compile:
     alectryon lists.lean3 -o lists.lean3.html
       # Lean → HTML; produces ‘lists.lean3.html’ -/

variables {α β : Type*}

open list

theorem mem_map_of_mem (f : α → β)
  {a : α} {l : list α} (h : a ∈ l) : f a ∈ map f l :=
begin
α: Type u_1
β: Type u_2
f: α → β
a: α
l: list α
h: a ∈ l
f a ∈ map f l
  induction l with b l' ih,
α: Type u_1
β: Type u_2
f: α → β
a: α
h: a ∈ nil
list.nil
f a ∈ map f nil
α: Type u_1
β: Type u_2
f: α → β
a, b: α
l': list α
ih: a ∈ l' → f a ∈ map f l'
h: a ∈ b :: l'
list.cons
f a ∈ map f (b :: l')
  {
α: Type u_1
β: Type u_2
f: α → β
a: α
h: a ∈ nil
list.nil
f a ∈ map f nil
α: Type u_1
β: Type u_2
f: α → β
a, b: α
l': list α
ih: a ∈ l' → f a ∈ map f l'
h: a ∈ b :: l'
list.cons
f a ∈ map f (b :: l')cases h},
  {
α: Type u_1
β: Type u_2
f: α → β
a, b: α
l': list α
ih: a ∈ l' → f a ∈ map f l'
h: a ∈ b :: l'
list.cons
f a ∈ map f (b :: l')cases h with h,
α: Type u_1
β: Type u_2
f: α → β
a, b: α
l': list α
ih: a ∈ l' → f a ∈ map f l'
h: a = b
list.cons, or.inl
f a ∈ map f (b :: l')
α: Type u_1
β: Type u_2
f: α → β
a, b: α
l': list α
ih: a ∈ l' → f a ∈ map f l'
h: list.mem a l'
list.cons, or.inr
f a ∈ map f (b :: l')
    {
α: Type u_1
β: Type u_2
f: α → β
a, b: α
l': list α
ih: a ∈ l' → f a ∈ map f l'
h: a = b
list.cons, or.inl
f a ∈ map f (b :: l')
α: Type u_1
β: Type u_2
f: α → β
a, b: α
l': list α
ih: a ∈ l' → f a ∈ map f l'
h: list.mem a l'
list.cons, or.inr
f a ∈ map f (b :: l')apply or.inl,
α: Type u_1
β: Type u_2
f: α → β
a, b: α
l': list α
ih: a ∈ l' → f a ∈ map f l'
h: a = b
f a = f b rw h},
    {
α: Type u_1
β: Type u_2
f: α → β
a, b: α
l': list α
ih: a ∈ l' → f a ∈ map f l'
h: list.mem a l'
list.cons, or.inr
f a ∈ map f (b :: l')exact or.inr (ih h)}}
end

theorem exists_of_mem_map {f : α → β}
  {b : β} {l : list α} (h : b ∈ map f l) :
    ∃ a, a ∈ l ∧ f a = b :=
begin
α: Type u_1
β: Type u_2
f: α → β
b: β
l: list α
h: b ∈ map f l
∃ (a : α), a ∈ l ∧ f a = b
  induction l with c l' ih,
α: Type u_1
β: Type u_2
f: α → β
b: β
h: b ∈ map f nil
list.nil
∃ (a : α), a ∈ nil ∧ f a = b
α: Type u_1
β: Type u_2
f: α → β
b: β
c: α
l': list α
ih: b ∈ map f l' → (∃ (a : α), a ∈ l' ∧ f a = b)
h: b ∈ map f (c :: l')
list.cons
∃ (a : α), a ∈ c :: l' ∧ f a = b
  {
α: Type u_1
β: Type u_2
f: α → β
b: β
h: b ∈ map f nil
list.nil
∃ (a : α), a ∈ nil ∧ f a = b cases h },
  {
α: Type u_1
β: Type u_2
f: α → β
b: β
c: α
l': list α
ih: b ∈ map f l' → (∃ (a : α), a ∈ l' ∧ f a = b)
h: b ∈ map f (c :: l')
list.cons
∃ (a : α), a ∈ c :: l' ∧ f a = b cases (eq_or_mem_of_mem_cons h) with h h,
α: Type u_1
β: Type u_2
f: α → β
b: β
c: α
l': list α
ih: b ∈ map f l' → (∃ (a : α), a ∈ l' ∧ f a = b)
h: b ∈ map f (c :: l')
h: b = f c
list.cons, or.inl
∃ (a : α), a ∈ c :: l' ∧ f a = b
α: Type u_1
β: Type u_2
f: α → β
b: β
c: α
l': list α
ih: b ∈ map f l' → (∃ (a : α), a ∈ l' ∧ f a = b)
h: b ∈ map f (c :: l')
h: b ∈ map f l'
list.cons, or.inr
∃ (a : α), a ∈ c :: l' ∧ f a = b
    {
α: Type u_1
β: Type u_2
f: α → β
b: β
c: α
l': list α
ih: b ∈ map f l' → (∃ (a : α), a ∈ l' ∧ f a = b)
h: b ∈ map f (c :: l')
h: b = f c
list.cons, or.inl
∃ (a : α), a ∈ c :: l' ∧ f a = b exact ⟨c, mem_cons_self _ _, h.symm⟩ },
    {
α: Type u_1
β: Type u_2
f: α → β
b: β
c: α
l': list α
ih: b ∈ map f l' → (∃ (a : α), a ∈ l' ∧ f a = b)
h: b ∈ map f (c :: l')
h: b ∈ map f l'
list.cons, or.inr
∃ (a : α), a ∈ c :: l' ∧ f a = b cases ih h with a ha₁,
α: Type u_1
β: Type u_2
f: α → β
b: β
c: α
l': list α
ih: b ∈ map f l' → (∃ (a : α), a ∈ l' ∧ f a = b)
h: b ∈ map f (c :: l')
h: b ∈ map f l'
a: α
ha₁: a ∈ l' ∧ f a = b
∃ (a : α), a ∈ c :: l' ∧ f a = b
      exact ⟨a, mem_cons_of_mem _ ha₁.1, ha₁.2⟩ }}
end

@[simp] theorem mem_map {f : α → β} {b : β} {l : list α}
  : b ∈ map f l ↔ ∃ a, a ∈ l ∧ f a = b :=
⟨exists_of_mem_map,
 λ ⟨a, la, h⟩, by
α: Type u_1
β: Type u_2
f: α → β
b: β
l: list α
_x: ∃ (a : α), a ∈ l ∧ f a = b
_fun_match: (∃ (a : α), a ∈ l ∧ f a = b) → b ∈ map f l
a: α
la: a ∈ l
h: f a = b
b ∈ map f l rw [← h]; exact mem_map_of_mem f la⟩

lemma forall_mem_map_iff {f : α → β} {l : list α} {P : β → Prop} :
  (∀ i ∈ l.map f, P i) ↔ ∀ j ∈ l, P (f j) :=
begin
α: Type u_1
β: Type u_2
f: α → β
l: list α
P: β → Prop
(∀ (i : β), i ∈ map f l → P i) ↔ ∀ (j : α), j ∈ l → P (f j)
  split,
α: Type u_1
β: Type u_2
f: α → β
l: list α
P: β → Prop
(∀ (i : β), i ∈ map f l → P i) → ∀ (j : α), j ∈ l → P (f j)
α: Type u_1
β: Type u_2
f: α → β
l: list α
P: β → Prop
(∀ (j : α), j ∈ l → P (f j)) → ∀ (i : β), i ∈ map f l → P i
  {
α: Type u_1
β: Type u_2
f: α → β
l: list α
P: β → Prop
(∀ (i : β), i ∈ map f l → P i) → ∀ (j : α), j ∈ l → P (f j) assume H j hj,
α: Type u_1
β: Type u_2
f: α → β
l: list α
P: β → Prop
H: ∀ (i : β), i ∈ map f l → P i
j: α
hj: j ∈ l
P (f j)
    exact H (f j) (mem_map_of_mem f hj) },
  {
α: Type u_1
β: Type u_2
f: α → β
l: list α
P: β → Prop
(∀ (j : α), j ∈ l → P (f j)) → ∀ (i : β), i ∈ map f l → P i assume H i hi,
α: Type u_1
β: Type u_2
f: α → β
l: list α
P: β → Prop
H: ∀ (j : α), j ∈ l → P (f j)
i: β
hi: i ∈ map f l
P i
    cases mem_map.1 hi with j hj,
α: Type u_1
β: Type u_2
f: α → β
l: list α
P: β → Prop
H: ∀ (j : α), j ∈ l → P (f j)
i: β
hi: i ∈ map f l
j: α
hj: j ∈ l ∧ f j = i
P i
    rw ← hj.2,
α: Type u_1
β: Type u_2
f: α → β
l: list α
P: β → Prop
H: ∀ (j : α), j ∈ l → P (f j)
i: β
hi: i ∈ map f l
j: α
hj: j ∈ l ∧ f j = i
P (f j)
    exact H j hj.1 }
end