@[implemented_by _private.Init.Data.Option.Attach.0.Option.attachWithImpl]

def Option.attachWith {α : Type u_1} (xs : Option α) (P : α → Prop) (H : ∀ (x : α), x ∈ xs → P x) : Option { x : α // P x }

"Attach" a proof P x that holds for the element of o, if present, to produce a new option with the same element but in the type {x // P x}.

Equations

• none.attachWith P H_2 = none
• (some x).attachWith P H_2 = some ⟨x, ⋯⟩

@[inline]

def Option.attach {α : Type u_1} (xs : Option α) : Option { x : α // x ∈ xs }

"Attach" the proof that the element of xs, if present, is in xs to produce a new option with the same elements but in the type {x // x ∈ xs}.

Equations

• xs.attach = xs.attachWith (Membership.mem xs) ⋯

@[simp]

theorem Option.attach_none {α : Type u_1} : none.attach = none

@[simp]

theorem Option.attachWith_none {α : Type u_1} {P : α → Prop} {H : ∀ (x : α), x ∈ none → P x} : none.attachWith P H = none

@[simp]

theorem Option.attach_some {α : Type u_1} {x : α} : (some x).attach = some ⟨x, ⋯⟩

@[simp]

theorem Option.attachWith_some {α : Type u_1} {x : α} {P : α → Prop} (h : ∀ (b : α), b ∈ some x → P b) : (some x).attachWith P h = some ⟨x, ⋯⟩

theorem Option.attach_congr {α : Type u_1} {o₁ : Option α} {o₂ : Option α} (h : o₁ = o₂) : o₁.attach = Option.map (fun (x : { x : α // x ∈ o₂ }) => ⟨x.val, ⋯⟩) o₂.attach

theorem Option.attachWith_congr {α : Type u_1} {o₁ : Option α} {o₂ : Option α} (w : o₁ = o₂) {P : α → Prop} {H : ∀ (x : α), x ∈ o₁ → P x} : o₁.attachWith P H = o₂.attachWith P ⋯

theorem Option.attach_map_coe {α : Type u_1} {β : Type u_2} (o : Option α) (f : α → β) : Option.map (fun (i : { i : α // i ∈ o }) => f i.val) o.attach = Option.map f o

theorem Option.attach_map_val {α : Type u_1} {β : Type u_2} (o : Option α) (f : α → β) : Option.map (fun (i : { x : α // x ∈ o }) => f i.val) o.attach = Option.map f o

@[simp]

theorem Option.attach_map_subtype_val {α : Type u_1} (o : Option α) : Option.map Subtype.val o.attach = o

theorem Option.attachWith_map_coe {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ (a : α), a ∈ o → p a) : Option.map (fun (i : { i : α // p i }) => f i.val) (o.attachWith p H) = Option.map f o

theorem Option.attachWith_map_val {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : α → β) (o : Option α) (H : ∀ (a : α), a ∈ o → p a) : Option.map (fun (i : { x : α // p x }) => f i.val) (o.attachWith p H) = Option.map f o

@[simp]

theorem Option.attachWith_map_subtype_val {α : Type u_1} {p : α → Prop} (o : Option α) (H : ∀ (a : α), a ∈ o → p a) : Option.map Subtype.val (o.attachWith p H) = o

@[simp]

theorem Option.mem_attach {α : Type u_1} (o : Option α) (x : { x : α // x ∈ o }) : x ∈ o.attach

@[simp]

theorem Option.isNone_attach {α : Type u_1} (o : Option α) : o.attach.isNone = o.isNone

@[simp]

theorem Option.isNone_attachWith {α : Type u_1} {p : α → Prop} (o : Option α) (H : ∀ (a : α), a ∈ o → p a) : (o.attachWith p H).isNone = o.isNone

@[simp]

theorem Option.isSome_attach {α : Type u_1} (o : Option α) : o.attach.isSome = o.isSome

@[simp]

theorem Option.isSome_attachWith {α : Type u_1} {p : α → Prop} (o : Option α) (H : ∀ (a : α), a ∈ o → p a) : (o.attachWith p H).isSome = o.isSome

@[simp]

theorem Option.attach_eq_none_iff {α : Type u_1} (o : Option α) : o.attach = none ↔ o = none

@[simp]

theorem Option.attach_eq_some_iff {α : Type u_1} {o : Option α} {x : { x : α // x ∈ o }} : o.attach = some x ↔ o = some x.val

@[simp]

theorem Option.attachWith_eq_none_iff {α : Type u_1} {p : α → Prop} (o : Option α) (H : ∀ (a : α), a ∈ o → p a) : o.attachWith p H = none ↔ o = none

@[simp]

theorem Option.attachWith_eq_some_iff {α : Type u_1} {p : α → Prop} {o : Option α} (H : ∀ (a : α), a ∈ o → p a) {x : { x : α // p x }} : o.attachWith p H = some x ↔ o = some x.val

@[simp]

theorem Option.get_attach {α : Type u_1} {o : Option α} (h : o.attach.isSome = true) : o.attach.get h = ⟨o.get ⋯, ⋯⟩

@[simp]

theorem Option.get_attachWith {α : Type u_1} {p : α → Prop} {o : Option α} (H : ∀ (a : α), a ∈ o → p a) (h : (o.attachWith p H).isSome = true) : (o.attachWith p H).get h = ⟨o.get ⋯, ⋯⟩

@[simp]

theorem Option.toList_attach {α : Type u_1} (o : Option α) : o.attach.toList = List.map (fun (x : { x : α // x ∈ o.toList }) => match x with | ⟨x, h⟩ => ⟨x, ⋯⟩) o.toList.attach

theorem Option.attach_map {α : Type u_1} {β : Type u_2} {o : Option α} (f : α → β) : (Option.map f o).attach = Option.map (fun (x : { x : α // x ∈ o }) => match x with | ⟨x, h⟩ => ⟨f x, ⋯⟩) o.attach

theorem Option.attachWith_map {α : Type u_1} {β : Type u_2} {o : Option α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ Option.map f o → P b} : (Option.map f o).attachWith P H = Option.map (fun (x : { x : α // (P ∘ f) x }) => match x with | ⟨x, h⟩ => ⟨f x, h⟩) (o.attachWith (P ∘ f) ⋯)

theorem Option.map_attach {α : Type u_1} {β : Type u_2} {o : Option α} (f : { x : α // x ∈ o } → β) : Option.map f o.attach = Option.pmap (fun (a : α) (h : a ∈ o) => f ⟨a, h⟩) o ⋯

theorem Option.map_attachWith {α : Type u_1} {β : Type u_2} {o : Option α} {P : α → Prop} {H : ∀ (a : α), a ∈ o → P a} (f : { x : α // P x } → β) : Option.map f (o.attachWith P H) = Option.pmap (fun (a : α) (h : a ∈ o ∧ P a) => f ⟨a, ⋯⟩) o ⋯

theorem Option.attach_bind {α : Type u_1} {β : Type u_2} {o : Option α} {f : α → Option β} : (o.bind f).attach = o.attach.bind fun (x : { x : α // x ∈ o }) => match x with | ⟨x, h⟩ => Option.map (fun (x_1 : { x_1 : β // x_1 ∈ f x }) => match x_1 with | ⟨y, h'⟩ => ⟨y, ⋯⟩) (f x).attach

theorem Option.bind_attach {α : Type u_1} {β : Type u_2} {o : Option α} {f : { x : α // x ∈ o } → Option β} : o.attach.bind f = o.pbind fun (a : α) (h : a ∈ o) => f ⟨a, h⟩

theorem Option.pbind_eq_bind_attach {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → a ∈ o → Option β} : o.pbind f = o.attach.bind fun (x : { x : α // x ∈ o }) => match x with | ⟨x, h⟩ => f x h

theorem Option.attach_filter {α : Type u_1} {o : Option α} {p : α → Bool} : (Option.filter p o).attach = o.attach.bind fun (x : { x : α // x ∈ o }) => match x with | ⟨x, h⟩ => if h' : p x = true then some ⟨x, ⋯⟩ else none

theorem Option.filter_attach {α : Type u_1} {o : Option α} {p : { x : α // x ∈ o } → Bool} : Option.filter p o.attach = o.pbind fun (a : α) (h : a ∈ o) => if p ⟨a, h⟩ = true then some ⟨a, h⟩ else none

unattach

Option.unattach is the (one-sided) inverse of Option.attach. It is a synonym for Option.map Subtype.val.

We use it by providing a simp lemma l.attach.unattach = l, and simp lemmas which recognize higher order functions applied to l : Option { x // p x } which only depend on the value, not the predicate, and rewrite these in terms of a simpler function applied to l.unattach.

Further, we provide simp lemmas that push unattach inwards.

def Option.unattach {α : Type u_1} {p : α → Prop} (o : Option { x : α // p x }) : Option α

A synonym for l.map (·.val). Mostly this should not be needed by users. It is introduced as an intermediate step by lemmas such as map_subtype, and is ideally subsequently simplified away by unattach_attach.

If not, usually the right approach is simp [Option.unattach, -Option.map_subtype] to unfold.

Equations

• o.unattach = Option.map (fun (x : { x : α // p x }) => x.val) o

@[simp]

theorem Option.unattach_none {α : Type u_1} {p : α → Prop} : none.unattach = none

@[simp]

theorem Option.unattach_some {α : Type u_1} {p : α → Prop} {a : { x : α // p x }} : (some a).unattach = some a.val

@[simp]

theorem Option.isSome_unattach {α : Type u_1} {p : α → Prop} {o : Option { x : α // p x }} : o.unattach.isSome = o.isSome

@[simp]

theorem Option.isNone_unattach {α : Type u_1} {p : α → Prop} {o : Option { x : α // p x }} : o.unattach.isNone = o.isNone

@[simp]

theorem Option.unattach_attach {α : Type u_1} (o : Option α) : o.attach.unattach = o

@[simp]

theorem Option.unattach_attachWith {α : Type u_1} {p : α → Prop} {o : Option α} {H : ∀ (a : α), a ∈ o → p a} : (o.attachWith p H).unattach = o

Recognizing higher order functions on subtypes using a function that only depends on the value.

@[simp]

theorem Option.map_subtype {α : Type u_1} {β : Type u_2} {p : α → Prop} {o : Option { x : α // p x }} {f : { x : α // p x } → β} {g : α → β} {hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x} : Option.map f o = Option.map g o.unattach

This lemma identifies maps over lists of subtypes, where the function only depends on the value, not the proposition, and simplifies these to the function directly taking the value.

@[simp]

theorem Option.bind_subtype {α : Type u_1} {β : Type u_2} {p : α → Prop} {o : Option { x : α // p x }} {f : { x : α // p x } → Option β} {g : α → Option β} {hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x} : o.bind f = o.unattach.bind g

@[simp]

theorem Option.unattach_filter {α : Type u_1} {p : α → Prop} {o : Option { x : α // p x }} {f : { x : α // p x } → Bool} {g : α → Bool} {hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x} : (Option.filter f o).unattach = Option.filter g o.unattach