Partial values of a type

This file defines Part α, the partial values of a type. o : Part α carries a proposition o.Dom, its domain, along with a function get : o.Dom → α, its value. The rule is then that every partial value has a value but, to access it, you need to provide a proof of the domain. Part α behaves the same as Option α except that o : Option α is decidably none or some a for some a : α, while the domain of o : Part α doesn't have to be decidable. That means you can translate back and forth between a partial value with a decidable domain and an option, and Option α and Part α are classically equivalent. In general, Part α is bigger than Option α. In current mathlib, Part ℕ, aka PartENat, is used to move decidability of the order to decidability of PartENat.find (which is the smallest natural satisfying a predicate, or ∞ if there's none).

Main declarations

Option-like declarations:

• Part.none: The partial value whose domain is False.
• Part.some a: The partial value whose domain is True and whose value is a.
• Part.ofOption: Converts an Option α to a Part α by sending none to none and some a to some a.
• Part.toOption: Converts a Part α with a decidable domain to an Option α.
• Part.equivOption: Classical equivalence between Part α and Option α. Monadic structure:
• Part.bind: o.bind f has value (f (o.get _)).get _ (f o morally) and is defined when o and f (o.get _) are defined.
• Part.map: Maps the value and keeps the same domain. Other:
• Part.restrict: Part.restrict p o replaces the domain of o : Part α by p : Prop so long as p → o.Dom.
• Part.assert: assert p f appends p to the domains of the values of a partial function.
• Part.unwrap: Gets the value of a partial value regardless of its domain. Unsound.

Notation

For a : α, o : Part α, a ∈ o means that o is defined and equal to a. Formally, it means o.Dom and o.get _ = a.

structure Part (α : Type u) : Type u

Part α is the type of "partial values" of type α. It is similar to Option α except the domain condition can be an arbitrary proposition, not necessarily decidable.

• Dom : Prop

  The domain of a partial value

• get : self.Dom → α

  Extract a value from a partial value given a proof of Dom

def Part.toOption {α : Type u_1} (o : Part α) [Decidable o.Dom] : Option α

Convert a Part α with a decidable domain to an option

Equations

• o.toOption = if h : o.Dom then some (o.get h) else none

@[simp]

theorem Part.toOption_isSome {α : Type u_1} (o : Part α) [Decidable o.Dom] : o.toOption.isSome = true ↔ o.Dom

@[simp]

theorem Part.toOption_eq_none {α : Type u_1} (o : Part α) [Decidable o.Dom] : o.toOption = none ↔ ¬o.Dom

@[deprecated Part.toOption_eq_none]

theorem Part.toOption_isNone {α : Type u_1} (o : Part α) [Decidable o.Dom] : o.toOption = none ↔ ¬o.Dom

Alias of Part.toOption_eq_none.

theorem Part.ext' {α : Type u_1} {o : Part α} {p : Part α} : (o.Dom ↔ p.Dom) → (∀ (h₁ : o.Dom) (h₂ : p.Dom), o.get h₁ = p.get h₂) → o = p

Part extensionality

@[simp]

theorem Part.eta {α : Type u_1} (o : Part α) : { Dom := o.Dom, get := fun (h : o.Dom) => o.get h } = o

Part eta expansion

def Part.Mem {α : Type u_1} (o : Part α) (a : α) : Prop

a ∈ o means that o is defined and equal to a

Equations

• o.Mem a = ∃ (h : o.Dom), o.get h = a

instance Part.instMembership {α : Type u_1} : Membership α (Part α)

Equations

• Part.instMembership = { mem := Part.Mem }

theorem Part.mem_eq {α : Type u_1} (a : α) (o : Part α) : (a ∈ o) = ∃ (h : o.Dom), o.get h = a

theorem Part.dom_iff_mem {α : Type u_1} {o : Part α} : o.Dom ↔ ∃ (y : α), y ∈ o

theorem Part.get_mem {α : Type u_1} {o : Part α} (h : o.Dom) : o.get h ∈ o

@[simp]

theorem Part.mem_mk_iff {α : Type u_1} {p : Prop} {o : p → α} {a : α} : a ∈ { Dom := p, get := o } ↔ ∃ (h : p), o h = a

theorem Part.ext_iff {α : Type u_1} {o : Part α} {p : Part α} : o = p ↔ ∀ (a : α), a ∈ o ↔ a ∈ p

theorem Part.ext {α : Type u_1} {o : Part α} {p : Part α} (H : ∀ (a : α), a ∈ o ↔ a ∈ p) : o = p

Part extensionality

def Part.none {α : Type u_1} : Part α

The none value in Part has a False domain and an empty function.

Equations

• Part.none = { Dom := False, get := fun (t : False) => False.rec (fun (x : False) => α) t }

instance Part.instInhabited {α : Type u_1} : Inhabited (Part α)

Equations

• Part.instInhabited = { default := Part.none }

@[simp]

theorem Part.not_mem_none {α : Type u_1} (a : α) : a ∉ Part.none

def Part.some {α : Type u_1} (a : α) : Part α

The some a value in Part has a True domain and the function returns a.

Equations

• Part.some a = { Dom := True, get := fun (x : True) => a }

@[simp]

theorem Part.some_dom {α : Type u_1} (a : α) : (Part.some a).Dom

theorem Part.mem_unique {α : Type u_1} {a : α} {b : α} {o : Part α} : a ∈ o → b ∈ o → a = b

theorem Part.Mem.left_unique {α : Type u_1} : Relator.LeftUnique fun (x1 : α) (x2 : Part α) => x1 ∈ x2

theorem Part.get_eq_of_mem {α : Type u_1} {o : Part α} {a : α} (h : a ∈ o) (h' : o.Dom) : o.get h' = a

theorem Part.subsingleton {α : Type u_1} (o : Part α) : {a : α | a ∈ o}.Subsingleton

@[simp]

theorem Part.get_some {α : Type u_1} {a : α} (ha : (Part.some a).Dom) : (Part.some a).get ha = a

theorem Part.mem_some {α : Type u_1} (a : α) : a ∈ Part.some a

@[simp]

theorem Part.mem_some_iff {α : Type u_1} {a : α} {b : α} : b ∈ Part.some a ↔ b = a

theorem Part.eq_some_iff {α : Type u_1} {a : α} {o : Part α} : o = Part.some a ↔ a ∈ o

theorem Part.eq_none_iff {α : Type u_1} {o : Part α} : o = Part.none ↔ ∀ (a : α), a ∉ o

theorem Part.eq_none_iff' {α : Type u_1} {o : Part α} : o = Part.none ↔ ¬o.Dom

@[simp]

theorem Part.not_none_dom {α : Type u_1} : ¬Part.none.Dom

@[simp]

theorem Part.some_ne_none {α : Type u_1} (x : α) : Part.some x ≠ Part.none

@[simp]

theorem Part.none_ne_some {α : Type u_1} (x : α) : Part.none ≠ Part.some x

theorem Part.ne_none_iff {α : Type u_1} {o : Part α} : o ≠ Part.none ↔ ∃ (x : α), o = Part.some x

theorem Part.eq_none_or_eq_some {α : Type u_1} (o : Part α) : o = Part.none ∨ ∃ (x : α), o = Part.some x

theorem Part.some_injective {α : Type u_1} : Function.Injective Part.some

@[simp]

theorem Part.some_inj {α : Type u_1} {a : α} {b : α} : Part.some a = Part.some b ↔ a = b

@[simp]

theorem Part.some_get {α : Type u_1} {a : Part α} (ha : a.Dom) : Part.some (a.get ha) = a

theorem Part.get_eq_iff_eq_some {α : Type u_1} {a : Part α} {ha : a.Dom} {b : α} : a.get ha = b ↔ a = Part.some b

theorem Part.get_eq_get_of_eq {α : Type u_1} (a : Part α) (ha : a.Dom) {b : Part α} (h : a = b) : a.get ha = b.get ⋯

theorem Part.get_eq_iff_mem {α : Type u_1} {o : Part α} {a : α} (h : o.Dom) : o.get h = a ↔ a ∈ o

theorem Part.eq_get_iff_mem {α : Type u_1} {o : Part α} {a : α} (h : o.Dom) : a = o.get h ↔ a ∈ o

@[simp]

theorem Part.none_toOption {α : Type u_1} [Decidable Part.none.Dom] : Part.none.toOption = none

@[simp]

theorem Part.some_toOption {α : Type u_1} (a : α) [Decidable (Part.some a).Dom] : (Part.some a).toOption = some a

instance Part.noneDecidable {α : Type u_1} : Decidable Part.none.Dom

Equations

• Part.noneDecidable = instDecidableFalse

instance Part.someDecidable {α : Type u_1} (a : α) : Decidable (Part.some a).Dom

Equations

• Part.someDecidable a = instDecidableTrue

def Part.getOrElse {α : Type u_1} (a : Part α) [Decidable a.Dom] (d : α) : α

Retrieves the value of a : Part α if it exists, and return the provided default value otherwise.

Equations

• a.getOrElse d = if ha : a.Dom then a.get ha else d

theorem Part.getOrElse_of_dom {α : Type u_1} (a : Part α) (h : a.Dom) [Decidable a.Dom] (d : α) : a.getOrElse d = a.get h

theorem Part.getOrElse_of_not_dom {α : Type u_1} (a : Part α) (h : ¬a.Dom) [Decidable a.Dom] (d : α) : a.getOrElse d = d

@[simp]

theorem Part.getOrElse_none {α : Type u_1} (d : α) [Decidable Part.none.Dom] : Part.none.getOrElse d = d

@[simp]

theorem Part.getOrElse_some {α : Type u_1} (a : α) (d : α) [Decidable (Part.some a).Dom] : (Part.some a).getOrElse d = a

theorem Part.mem_toOption {α : Type u_1} {o : Part α} [Decidable o.Dom] {a : α} : a ∈ o.toOption ↔ a ∈ o

@[simp]

theorem Part.toOption_eq_some_iff {α : Type u_1} {o : Part α} [Decidable o.Dom] {a : α} : o.toOption = some a ↔ a ∈ o

theorem Part.Dom.toOption {α : Type u_1} {o : Part α} [Decidable o.Dom] (h : o.Dom) : o.toOption = some (o.get h)

theorem Part.toOption_eq_none_iff {α : Type u_1} {a : Part α} [Decidable a.Dom] : a.toOption = none ↔ ¬a.Dom

theorem Part.elim_toOption {α : Type u_4} {β : Type u_5} (a : Part α) [Decidable a.Dom] (b : β) (f : α → β) : a.toOption.elim b f = if h : a.Dom then f (a.get h) else b

def Part.ofOption {α : Type u_1} : Option α → Part α

Converts an Option α into a Part α.

Equations

• ↑none = Part.none
• ↑(some a) = Part.some a

@[simp]

theorem Part.mem_ofOption {α : Type u_1} {a : α} {o : Option α} : a ∈ ↑o ↔ a ∈ o

@[simp]

theorem Part.ofOption_dom {α : Type u_4} (o : Option α) : (↑o).Dom ↔ o.isSome = true

theorem Part.ofOption_eq_get {α : Type u_4} (o : Option α) : ↑o = { Dom := o.isSome = true, get := o.get }

instance Part.instCoeOption {α : Type u_1} : Coe (Option α) (Part α)

Equations

• Part.instCoeOption = { coe := Part.ofOption }

theorem Part.mem_coe {α : Type u_1} {a : α} {o : Option α} : a ∈ ↑o ↔ a ∈ o

@[simp]

theorem Part.coe_none {α : Type u_1} : ↑none = Part.none

@[simp]

theorem Part.coe_some {α : Type u_1} (a : α) : ↑(some a) = Part.some a

theorem Part.induction_on {α : Type u_1} {P : Part α → Prop} (a : Part α) (hnone : P Part.none) (hsome : ∀ (a : α), P (Part.some a)) : P a

instance Part.ofOptionDecidable {α : Type u_1} (o : Option α) : Decidable (↑o).Dom

Equations

• Part.ofOptionDecidable none = Part.noneDecidable
• Part.ofOptionDecidable (some a) = Part.someDecidable a

@[simp]

theorem Part.to_ofOption {α : Type u_1} (o : Option α) : (↑o).toOption = o

@[simp]

theorem Part.of_toOption {α : Type u_1} (o : Part α) [Decidable o.Dom] : ↑o.toOption = o

noncomputable def Part.equivOption {α : Type u_1} : Part α ≃ Option α

Part α is (classically) equivalent to Option α.

Equations

• Part.equivOption = { toFun := fun (o : Part α) => o.toOption, invFun := Part.ofOption, left_inv := ⋯, right_inv := ⋯ }

instance Part.instPartialOrder {α : Type u_1} : PartialOrder (Part α)

We give Part α the order where everything is greater than none.

Equations

• Part.instPartialOrder = PartialOrder.mk ⋯

instance Part.instOrderBot {α : Type u_1} : OrderBot (Part α)

Equations

• Part.instOrderBot = OrderBot.mk ⋯

theorem Part.le_total_of_le_of_le {α : Type u_1} {x : Part α} {y : Part α} (z : Part α) (hx : x ≤ z) (hy : y ≤ z) : x ≤ y ∨ y ≤ x

def Part.assert {α : Type u_1} (p : Prop) (f : p → Part α) : Part α

assert p f is a bind-like operation which appends an additional condition p to the domain and uses f to produce the value.

Equations

• Part.assert p f = { Dom := ∃ (h : p), (f h).Dom, get := fun (ha : ∃ (h : p), (f h).Dom) => (f ⋯).get ⋯ }

def Part.bind {α : Type u_1} {β : Type u_2} (f : Part α) (g : α → Part β) : Part β

The bind operation has value g (f.get), and is defined when all the parts are defined.

Equations

• f.bind g = Part.assert f.Dom fun (b : f.Dom) => g (f.get b)

@[simp]

theorem Part.map_Dom {α : Type u_1} {β : Type u_2} (f : α → β) (o : Part α) : (Part.map f o).Dom = o.Dom

@[simp]

theorem Part.map_get {α : Type u_1} {β : Type u_2} (f : α → β) (o : Part α) : ∀ (a : o.Dom), (Part.map f o).get a = (f ∘ o.get) a

def Part.map {α : Type u_1} {β : Type u_2} (f : α → β) (o : Part α) : Part β

The map operation for Part just maps the value and maintains the same domain.

Equations

• Part.map f o = { Dom := o.Dom, get := f ∘ o.get }

theorem Part.mem_map {α : Type u_1} {β : Type u_2} (f : α → β) {o : Part α} {a : α} : a ∈ o → f a ∈ Part.map f o

@[simp]

theorem Part.mem_map_iff {α : Type u_1} {β : Type u_2} (f : α → β) {o : Part α} {b : β} : b ∈ Part.map f o ↔ ∃ a ∈ o, f a = b

@[simp]

theorem Part.map_none {α : Type u_1} {β : Type u_2} (f : α → β) : Part.map f Part.none = Part.none

@[simp]

theorem Part.map_some {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : Part.map f (Part.some a) = Part.some (f a)

theorem Part.mem_assert {α : Type u_1} {p : Prop} {f : p → Part α} {a : α} (h : p) : a ∈ f h → a ∈ Part.assert p f

@[simp]

theorem Part.mem_assert_iff {α : Type u_1} {p : Prop} {f : p → Part α} {a : α} : a ∈ Part.assert p f ↔ ∃ (h : p), a ∈ f h

theorem Part.assert_pos {α : Type u_1} {p : Prop} {f : p → Part α} (h : p) : Part.assert p f = f h

theorem Part.assert_neg {α : Type u_1} {p : Prop} {f : p → Part α} (h : ¬p) : Part.assert p f = Part.none

theorem Part.mem_bind {α : Type u_1} {β : Type u_2} {f : Part α} {g : α → Part β} {a : α} {b : β} : a ∈ f → b ∈ g a → b ∈ f.bind g

@[simp]

theorem Part.mem_bind_iff {α : Type u_1} {β : Type u_2} {f : Part α} {g : α → Part β} {b : β} : b ∈ f.bind g ↔ ∃ a ∈ f, b ∈ g a

theorem Part.Dom.bind {α : Type u_1} {β : Type u_2} {o : Part α} (h : o.Dom) (f : α → Part β) : o.bind f = f (o.get h)

theorem Part.Dom.of_bind {α : Type u_1} {β : Type u_2} {f : α → Part β} {a : Part α} (h : (a.bind f).Dom) : a.Dom

@[simp]

theorem Part.bind_none {α : Type u_1} {β : Type u_2} (f : α → Part β) : Part.none.bind f = Part.none

@[simp]

theorem Part.bind_some {α : Type u_1} {β : Type u_2} (a : α) (f : α → Part β) : (Part.some a).bind f = f a

theorem Part.bind_of_mem {α : Type u_1} {β : Type u_2} {o : Part α} {a : α} (h : a ∈ o) (f : α → Part β) : o.bind f = f a

theorem Part.bind_some_eq_map {α : Type u_1} {β : Type u_2} (f : α → β) (x : Part α) : x.bind (Part.some ∘ f) = Part.map f x

theorem Part.bind_toOption {α : Type u_1} {β : Type u_2} (f : α → Part β) (o : Part α) [Decidable o.Dom] [(a : α) → Decidable (f a).Dom] [Decidable (o.bind f).Dom] : (o.bind f).toOption = o.toOption.elim none fun (a : α) => (f a).toOption

theorem Part.bind_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_4} (f : Part α) (g : α → Part β) (k : β → Part γ) : (f.bind g).bind k = f.bind fun (x : α) => (g x).bind k

@[simp]

theorem Part.bind_map {α : Type u_1} {β : Type u_2} {γ : Type u_4} (f : α → β) (x : Part α) (g : β → Part γ) : (Part.map f x).bind g = x.bind fun (y : α) => g (f y)

@[simp]

theorem Part.map_bind {α : Type u_1} {β : Type u_2} {γ : Type u_4} (f : α → Part β) (x : Part α) (g : β → γ) : Part.map g (x.bind f) = x.bind fun (y : α) => Part.map g (f y)

theorem Part.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β → γ) (f : α → β) (o : Part α) : Part.map g (Part.map f o) = Part.map (g ∘ f) o

instance Part.instMonad : Monad Part

Equations

• Part.instMonad = Monad.mk

instance Part.instLawfulMonad : LawfulMonad Part

Equations

• Part.instLawfulMonad = ⋯

theorem Part.map_id' {α : Type u_1} {f : α → α} (H : ∀ (x : α), f x = x) (o : Part α) : Part.map f o = o

@[simp]

theorem Part.bind_some_right {α : Type u_1} (x : Part α) : x.bind Part.some = x

@[simp]

theorem Part.pure_eq_some {α : Type u_1} (a : α) : pure a = Part.some a

@[simp]

theorem Part.ret_eq_some {α : Type u_1} (a : α) : pure a = Part.some a

@[simp]

theorem Part.map_eq_map {α : Type u_4} {β : Type u_4} (f : α → β) (o : Part α) : f <$> o = Part.map f o

@[simp]

theorem Part.bind_eq_bind {α : Type u_4} {β : Type u_4} (f : Part α) (g : α → Part β) : f >>= g = f.bind g

theorem Part.bind_le {β : Type u_2} {α : Type u_2} (x : Part α) (f : α → Part β) (y : Part β) : x >>= f ≤ y ↔ ∀ a ∈ x, f a ≤ y

def Part.restrict {α : Type u_1} (p : Prop) (o : Part α) (H : p → o.Dom) : Part α

restrict p o h replaces the domain of o with p, and is well defined when p implies o is defined.

Equations

• Part.restrict p o H = { Dom := p, get := fun (h : p) => o.get ⋯ }

@[simp]

theorem Part.mem_restrict {α : Type u_1} (p : Prop) (o : Part α) (h : p → o.Dom) (a : α) : a ∈ Part.restrict p o h ↔ p ∧ a ∈ o

unsafe def Part.unwrap {α : Type u_1} (o : Part α) : α

unwrap o gets the value at o, ignoring the condition. This function is unsound.

theorem Part.assert_defined {α : Type u_1} {p : Prop} {f : p → Part α} (h : p) : (f h).Dom → (Part.assert p f).Dom

theorem Part.bind_defined {α : Type u_1} {β : Type u_2} {f : Part α} {g : α → Part β} (h : f.Dom) : (g (f.get h)).Dom → (f.bind g).Dom

@[simp]

theorem Part.bind_dom {α : Type u_1} {β : Type u_2} {f : Part α} {g : α → Part β} : (f.bind g).Dom ↔ ∃ (h : f.Dom), (g (f.get h)).Dom

We define several instances for constants and operations on Part α inherited from α.

This section could be moved to a separate file to avoid the import of Mathlib.Algebra.Group.Defs.

instance Part.instZero {α : Type u_1} [Zero α] : Zero (Part α)

Equations

• Part.instZero = { zero := pure 0 }

instance Part.instOne {α : Type u_1} [One α] : One (Part α)

Equations

• Part.instOne = { one := pure 1 }

instance Part.instAdd {α : Type u_1} [Add α] : Add (Part α)

Equations

• Part.instAdd = { add := fun (a b : Part α) => Seq.seq ((fun (x1 x2 : α) => x1 + x2) <$> a) fun (x : Unit) => b }

instance Part.instMul {α : Type u_1} [Mul α] : Mul (Part α)

Equations

• Part.instMul = { mul := fun (a b : Part α) => Seq.seq ((fun (x1 x2 : α) => x1 * x2) <$> a) fun (x : Unit) => b }

instance Part.instNeg {α : Type u_1} [Neg α] : Neg (Part α)

Equations

• Part.instNeg = { neg := Part.map Neg.neg }

instance Part.instInv {α : Type u_1} [Inv α] : Inv (Part α)

Equations

• Part.instInv = { inv := Part.map Inv.inv }

instance Part.instSub {α : Type u_1} [Sub α] : Sub (Part α)

Equations

• Part.instSub = { sub := fun (a b : Part α) => Seq.seq ((fun (x1 x2 : α) => x1 - x2) <$> a) fun (x : Unit) => b }

instance Part.instDiv {α : Type u_1} [Div α] : Div (Part α)

Equations

• Part.instDiv = { div := fun (a b : Part α) => Seq.seq ((fun (x1 x2 : α) => x1 / x2) <$> a) fun (x : Unit) => b }

instance Part.instMod {α : Type u_1} [Mod α] : Mod (Part α)

Equations

• Part.instMod = { mod := fun (a b : Part α) => Seq.seq ((fun (x1 x2 : α) => x1 % x2) <$> a) fun (x : Unit) => b }

instance Part.instAppend {α : Type u_1} [Append α] : Append (Part α)

Equations

• Part.instAppend = { append := fun (a b : Part α) => Seq.seq ((fun (x1 x2 : α) => x1 ++ x2) <$> a) fun (x : Unit) => b }

instance Part.instInter {α : Type u_1} [Inter α] : Inter (Part α)

Equations

• Part.instInter = { inter := fun (a b : Part α) => Seq.seq ((fun (x1 x2 : α) => x1 ∩ x2) <$> a) fun (x : Unit) => b }

instance Part.instUnion {α : Type u_1} [Union α] : Union (Part α)

Equations

• Part.instUnion = { union := fun (a b : Part α) => Seq.seq ((fun (x1 x2 : α) => x1 ∪ x2) <$> a) fun (x : Unit) => b }

instance Part.instSDiff {α : Type u_1} [SDiff α] : SDiff (Part α)

Equations

• Part.instSDiff = { sdiff := fun (a b : Part α) => Seq.seq ((fun (x1 x2 : α) => x1 \ x2) <$> a) fun (x : Unit) => b }

theorem Part.mul_def {α : Type u_1} [Mul α] (a : Part α) (b : Part α) : a * b = do let y ← a Part.map (fun (x : α) => y * x) b

theorem Part.one_def {α : Type u_1} [One α] : 1 = Part.some 1

theorem Part.inv_def {α : Type u_1} [Inv α] (a : Part α) : a⁻¹ = Part.map (fun (x : α) => x⁻¹) a

theorem Part.div_def {α : Type u_1} [Div α] (a : Part α) (b : Part α) : a / b = do let y ← a Part.map (fun (x : α) => y / x) b

theorem Part.mod_def {α : Type u_1} [Mod α] (a : Part α) (b : Part α) : a % b = do let y ← a Part.map (fun (x : α) => y % x) b

theorem Part.append_def {α : Type u_1} [Append α] (a : Part α) (b : Part α) : a ++ b = do let y ← a Part.map (fun (x : α) => y ++ x) b

theorem Part.inter_def {α : Type u_1} [Inter α] (a : Part α) (b : Part α) : a ∩ b = do let y ← a Part.map (fun (x : α) => y ∩ x) b

theorem Part.union_def {α : Type u_1} [Union α] (a : Part α) (b : Part α) : a ∪ b = do let y ← a Part.map (fun (x : α) => y ∪ x) b

theorem Part.sdiff_def {α : Type u_1} [SDiff α] (a : Part α) (b : Part α) : a \ b = do let y ← a Part.map (fun (x : α) => y \ x) b

theorem Part.zero_mem_zero {α : Type u_1} [Zero α] : 0 ∈ 0

theorem Part.one_mem_one {α : Type u_1} [One α] : 1 ∈ 1

theorem Part.add_mem_add {α : Type u_1} [Add α] (a : Part α) (b : Part α) (ma : α) (mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma + mb ∈ a + b

theorem Part.mul_mem_mul {α : Type u_1} [Mul α] (a : Part α) (b : Part α) (ma : α) (mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma * mb ∈ a * b

theorem Part.left_dom_of_add_dom {α : Type u_1} [Add α] {a : Part α} {b : Part α} (hab : (a + b).Dom) : a.Dom

theorem Part.left_dom_of_mul_dom {α : Type u_1} [Mul α] {a : Part α} {b : Part α} (hab : (a * b).Dom) : a.Dom

theorem Part.right_dom_of_add_dom {α : Type u_1} [Add α] {a : Part α} {b : Part α} (hab : (a + b).Dom) : b.Dom

theorem Part.right_dom_of_mul_dom {α : Type u_1} [Mul α] {a : Part α} {b : Part α} (hab : (a * b).Dom) : b.Dom

@[simp]

theorem Part.add_get_eq {α : Type u_1} [Add α] (a : Part α) (b : Part α) (hab : (a + b).Dom) : (a + b).get hab = a.get ⋯ + b.get ⋯

@[simp]

theorem Part.mul_get_eq {α : Type u_1} [Mul α] (a : Part α) (b : Part α) (hab : (a * b).Dom) : (a * b).get hab = a.get ⋯ * b.get ⋯

theorem Part.some_add_some {α : Type u_1} [Add α] (a : α) (b : α) : Part.some a + Part.some b = Part.some (a + b)

theorem Part.some_mul_some {α : Type u_1} [Mul α] (a : α) (b : α) : Part.some a * Part.some b = Part.some (a * b)

theorem Part.neg_mem_neg {α : Type u_1} [Neg α] (a : Part α) (ma : α) (ha : ma ∈ a) : -ma ∈ -a

theorem Part.inv_mem_inv {α : Type u_1} [Inv α] (a : Part α) (ma : α) (ha : ma ∈ a) : ma⁻¹ ∈ a⁻¹

theorem Part.neg_some {α : Type u_1} [Neg α] (a : α) : -Part.some a = Part.some (-a)

theorem Part.inv_some {α : Type u_1} [Inv α] (a : α) : (Part.some a)⁻¹ = Part.some a⁻¹

theorem Part.sub_mem_sub {α : Type u_1} [Sub α] (a : Part α) (b : Part α) (ma : α) (mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma - mb ∈ a - b

theorem Part.div_mem_div {α : Type u_1} [Div α] (a : Part α) (b : Part α) (ma : α) (mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma / mb ∈ a / b

theorem Part.left_dom_of_sub_dom {α : Type u_1} [Sub α] {a : Part α} {b : Part α} (hab : (a - b).Dom) : a.Dom

theorem Part.left_dom_of_div_dom {α : Type u_1} [Div α] {a : Part α} {b : Part α} (hab : (a / b).Dom) : a.Dom

theorem Part.right_dom_of_sub_dom {α : Type u_1} [Sub α] {a : Part α} {b : Part α} (hab : (a - b).Dom) : b.Dom

theorem Part.right_dom_of_div_dom {α : Type u_1} [Div α] {a : Part α} {b : Part α} (hab : (a / b).Dom) : b.Dom

@[simp]

theorem Part.sub_get_eq {α : Type u_1} [Sub α] (a : Part α) (b : Part α) (hab : (a - b).Dom) : (a - b).get hab = a.get ⋯ - b.get ⋯

@[simp]

theorem Part.div_get_eq {α : Type u_1} [Div α] (a : Part α) (b : Part α) (hab : (a / b).Dom) : (a / b).get hab = a.get ⋯ / b.get ⋯

theorem Part.some_sub_some {α : Type u_1} [Sub α] (a : α) (b : α) : Part.some a - Part.some b = Part.some (a - b)

theorem Part.some_div_some {α : Type u_1} [Div α] (a : α) (b : α) : Part.some a / Part.some b = Part.some (a / b)

theorem Part.mod_mem_mod {α : Type u_1} [Mod α] (a : Part α) (b : Part α) (ma : α) (mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma % mb ∈ a % b

theorem Part.left_dom_of_mod_dom {α : Type u_1} [Mod α] {a : Part α} {b : Part α} (hab : (a % b).Dom) : a.Dom

theorem Part.right_dom_of_mod_dom {α : Type u_1} [Mod α] {a : Part α} {b : Part α} (hab : (a % b).Dom) : b.Dom

@[simp]

theorem Part.mod_get_eq {α : Type u_1} [Mod α] (a : Part α) (b : Part α) (hab : (a % b).Dom) : (a % b).get hab = a.get ⋯ % b.get ⋯

theorem Part.some_mod_some {α : Type u_1} [Mod α] (a : α) (b : α) : Part.some a % Part.some b = Part.some (a % b)

theorem Part.append_mem_append {α : Type u_1} [Append α] (a : Part α) (b : Part α) (ma : α) (mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma ++ mb ∈ a ++ b

theorem Part.left_dom_of_append_dom {α : Type u_1} [Append α] {a : Part α} {b : Part α} (hab : (a ++ b).Dom) : a.Dom

theorem Part.right_dom_of_append_dom {α : Type u_1} [Append α] {a : Part α} {b : Part α} (hab : (a ++ b).Dom) : b.Dom

@[simp]

theorem Part.append_get_eq {α : Type u_1} [Append α] (a : Part α) (b : Part α) (hab : (a ++ b).Dom) : (a ++ b).get hab = a.get ⋯ ++ b.get ⋯

theorem Part.some_append_some {α : Type u_1} [Append α] (a : α) (b : α) : Part.some a ++ Part.some b = Part.some (a ++ b)

theorem Part.inter_mem_inter {α : Type u_1} [Inter α] (a : Part α) (b : Part α) (ma : α) (mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma ∩ mb ∈ a ∩ b

theorem Part.left_dom_of_inter_dom {α : Type u_1} [Inter α] {a : Part α} {b : Part α} (hab : (a ∩ b).Dom) : a.Dom

theorem Part.right_dom_of_inter_dom {α : Type u_1} [Inter α] {a : Part α} {b : Part α} (hab : (a ∩ b).Dom) : b.Dom

@[simp]

theorem Part.inter_get_eq {α : Type u_1} [Inter α] (a : Part α) (b : Part α) (hab : (a ∩ b).Dom) : (a ∩ b).get hab = a.get ⋯ ∩ b.get ⋯

theorem Part.some_inter_some {α : Type u_1} [Inter α] (a : α) (b : α) : Part.some a ∩ Part.some b = Part.some (a ∩ b)

theorem Part.union_mem_union {α : Type u_1} [Union α] (a : Part α) (b : Part α) (ma : α) (mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma ∪ mb ∈ a ∪ b

theorem Part.left_dom_of_union_dom {α : Type u_1} [Union α] {a : Part α} {b : Part α} (hab : (a ∪ b).Dom) : a.Dom

theorem Part.right_dom_of_union_dom {α : Type u_1} [Union α] {a : Part α} {b : Part α} (hab : (a ∪ b).Dom) : b.Dom

@[simp]

theorem Part.union_get_eq {α : Type u_1} [Union α] (a : Part α) (b : Part α) (hab : (a ∪ b).Dom) : (a ∪ b).get hab = a.get ⋯ ∪ b.get ⋯

theorem Part.some_union_some {α : Type u_1} [Union α] (a : α) (b : α) : Part.some a ∪ Part.some b = Part.some (a ∪ b)

theorem Part.sdiff_mem_sdiff {α : Type u_1} [SDiff α] (a : Part α) (b : Part α) (ma : α) (mb : α) (ha : ma ∈ a) (hb : mb ∈ b) : ma \ mb ∈ a \ b

theorem Part.left_dom_of_sdiff_dom {α : Type u_1} [SDiff α] {a : Part α} {b : Part α} (hab : (a \ b).Dom) : a.Dom

theorem Part.right_dom_of_sdiff_dom {α : Type u_1} [SDiff α] {a : Part α} {b : Part α} (hab : (a \ b).Dom) : b.Dom

@[simp]

theorem Part.sdiff_get_eq {α : Type u_1} [SDiff α] (a : Part α) (b : Part α) (hab : (a \ b).Dom) : (a \ b).get hab = a.get ⋯ \ b.get ⋯

theorem Part.some_sdiff_some {α : Type u_1} [SDiff α] (a : α) (b : α) : Part.some a \ Part.some b = Part.some (a \ b)