Documentation

Mathlib.Data.Part

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:

Notation #

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

structure Part (α : Type u) :
  • The domain of a partial value

    Dom : Prop
  • Extract a value from a partial value given a proof of Dom

    get : Domα

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.

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

    Convert a Part α with a decidable domain to an option

    Equations
    @[simp]
    theorem Part.toOption_isSome {α : Type u_1} (o : Part α) [inst : Decidable o.Dom] :
    @[simp]
    theorem Part.toOption_isNone {α : Type u_1} (o : Part α) [inst : Decidable o.Dom] :
    theorem Part.ext' {α : Type u_1} {o : Part α} {p : Part α} :
    (o.Dom p.Dom) → (∀ (h₁ : o.Dom) (h₂ : p.Dom), Part.get o h₁ = Part.get p h₂) → o = p

    Part extensionality

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

    Part eta expansion

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

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

    Equations
    instance Part.instMembershipPart {α : Type u_1} :
    Equations
    • Part.instMembershipPart = { mem := Part.Mem }
    theorem Part.mem_eq {α : Type u_1} (a : α) (o : Part α) :
    (a o) = h, Part.get o 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) :
    @[simp]
    theorem Part.mem_mk_iff {α : Type u_1} {p : Prop} {o : pα} {a : α} :
    a { Dom := p, get := o } h, o h = a
    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
    instance Part.instInhabitedPart {α : Type u_1} :
    Equations
    • Part.instInhabitedPart = { 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
    @[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 ob oa = b
    theorem Part.Mem.left_unique {α : Type u_1} :
    Relator.LeftUnique fun x x_1 => x x_1
    theorem Part.get_eq_of_mem {α : Type u_1} {o : Part α} {a : α} (h : a o) (h' : o.Dom) :
    Part.get o h' = a
    theorem Part.subsingleton {α : Type u_1} (o : Part α) :
    Set.Subsingleton { a | a o }
    @[simp]
    theorem Part.get_some {α : Type u_1} {a : α} (ha : (Part.some a).Dom) :
    theorem Part.mem_some {α : Type u_1} (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
    @[simp]
    theorem Part.some_inj {α : Type u_1} {a : α} {b : α} :
    @[simp]
    theorem Part.some_get {α : Type u_1} {a : Part α} (ha : a.Dom) :
    theorem Part.get_eq_iff_eq_some {α : Type u_1} {a : Part α} {ha : a.Dom} {b : α} :
    Part.get a 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) :
    Part.get a ha = Part.get b (_ : b.Dom)
    theorem Part.get_eq_iff_mem {α : Type u_1} {o : Part α} {a : α} (h : o.Dom) :
    Part.get o h = a a o
    theorem Part.eq_get_iff_mem {α : Type u_1} {o : Part α} {a : α} (h : o.Dom) :
    a = Part.get o h a o
    @[simp]
    theorem Part.none_toOption {α : Type u_1} [inst : Decidable Part.none.Dom] :
    Part.toOption Part.none = none
    @[simp]
    theorem Part.some_toOption {α : Type u_1} (a : α) [inst : Decidable (Part.some a).Dom] :
    instance Part.noneDecidable {α : Type u_1} :
    Decidable Part.none.Dom
    Equations
    def Part.getOrElse {α : Type u_1} (a : Part α) [inst : Decidable a.Dom] (d : α) :
    α

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

    Equations
    theorem Part.getOrElse_of_dom {α : Type u_1} (a : Part α) (h : a.Dom) [inst : Decidable a.Dom] (d : α) :
    theorem Part.getOrElse_of_not_dom {α : Type u_1} (a : Part α) (h : ¬a.Dom) [inst : Decidable a.Dom] (d : α) :
    @[simp]
    theorem Part.getOrElse_none {α : Type u_1} (d : α) [inst : Decidable Part.none.Dom] :
    Part.getOrElse Part.none d = d
    @[simp]
    theorem Part.getOrElse_some {α : Type u_1} (a : α) (d : α) [inst : Decidable (Part.some a).Dom] :
    theorem Part.mem_toOption {α : Type u_1} {o : Part α} [inst : Decidable o.Dom] {a : α} :
    @[simp]
    theorem Part.toOption_eq_some_iff {α : Type u_1} {o : Part α} [inst : Decidable o.Dom] {a : α} :
    theorem Part.Dom.toOption {α : Type u_1} {o : Part α} [inst : Decidable o.Dom] (h : o.Dom) :
    theorem Part.toOption_eq_none_iff {α : Type u_1} {a : Part α} [inst : Decidable a.Dom] :
    Part.toOption a = none ¬a.Dom
    theorem Part.elim_toOption {α : Type u_1} {β : Type u_2} (a : Part α) [inst : Decidable a.Dom] (b : β) (f : αβ) :
    Option.elim (Part.toOption a) b f = if h : a.Dom then f (Part.get a h) else b
    def Part.ofOption {α : Type u_1} :
    Option αPart α

    Converts an Option α into a Part α.

    Equations
    @[simp]
    theorem Part.mem_ofOption {α : Type u_1} {a : α} {o : Option α} :
    @[simp]
    theorem Part.ofOption_dom {α : Type u_1} (o : Option α) :
    theorem Part.ofOption_eq_get {α : Type u_1} (o : Option α) :
    Part.ofOption o = { Dom := Option.isSome o = true, get := Option.get o }
    instance Part.instCoeOptionPart {α : Type u_1} :
    Coe (Option α) (Part α)
    Equations
    • Part.instCoeOptionPart = { coe := Part.ofOption }
    theorem Part.mem_coe {α : Type u_1} {a : α} {o : Option α} :
    @[simp]
    theorem Part.coe_none {α : Type u_1} :
    Part.ofOption none = Part.none
    @[simp]
    theorem Part.coe_some {α : Type u_1} (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 α) :
    Equations
    @[simp]
    theorem Part.to_ofOption {α : Type u_1} (o : Option α) :
    @[simp]
    theorem Part.of_toOption {α : Type u_1} (o : Part α) [inst : Decidable o.Dom] :
    noncomputable def Part.equivOption {α : Type u_1} :

    Part α is (classically) equivalent to Option α.

    Equations
    • One or more equations did not get rendered due to their size.

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

    Equations
    Equations
    • Part.instOrderBotPartToLEToPreorderInstPartialOrderPart = OrderBot.mk (_ : ∀ (a : Part α) (x : α), x x a)
    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 : pPart α) :
    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
    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
    @[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.get (Part.map f o) 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
    theorem Part.mem_map {α : Type u_1} {β : Type u_2} (f : αβ) {o : Part α} {a : α} :
    a of 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, a o f a = b
    @[simp]
    theorem Part.map_none {α : Type u_2} {β : Type u_1} (f : αβ) :
    Part.map f Part.none = Part.none
    @[simp]
    theorem Part.map_some {α : Type u_2} {β : Type u_1} (f : αβ) (a : α) :
    theorem Part.mem_assert {α : Type u_1} {p : Prop} {f : pPart α} {a : α} (h : p) :
    a f ha Part.assert p f
    @[simp]
    theorem Part.mem_assert_iff {α : Type u_1} {p : Prop} {f : pPart α} {a : α} :
    a Part.assert p f h, a f h
    theorem Part.assert_pos {α : Type u_1} {p : Prop} {f : pPart α} (h : p) :
    Part.assert p f = f h
    theorem Part.assert_neg {α : Type u_1} {p : Prop} {f : pPart α} (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 fb g ab Part.bind f g
    @[simp]
    theorem Part.mem_bind_iff {α : Type u_1} {β : Type u_2} {f : Part α} {g : αPart β} {b : β} :
    b Part.bind f g a, a f b g a
    theorem Part.Dom.bind {α : Type u_1} {β : Type u_2} {o : Part α} (h : o.Dom) (f : αPart β) :
    Part.bind o f = f (Part.get o h)
    theorem Part.Dom.of_bind {α : Type u_2} {β : Type u_1} {f : αPart β} {a : Part α} (h : (Part.bind a f).Dom) :
    a.Dom
    @[simp]
    theorem Part.bind_none {α : Type u_2} {β : Type u_1} (f : αPart β) :
    Part.bind Part.none f = Part.none
    @[simp]
    theorem Part.bind_some {α : Type u_2} {β : Type u_1} (a : α) (f : αPart β) :
    theorem Part.bind_of_mem {α : Type u_1} {β : Type u_2} {o : Part α} {a : α} (h : a o) (f : αPart β) :
    Part.bind o f = f a
    theorem Part.bind_some_eq_map {α : Type u_1} {β : Type u_2} (f : αβ) (x : Part α) :
    Part.bind x (Part.some f) = Part.map f x
    theorem Part.bind_toOption {α : Type u_2} {β : Type u_1} (f : αPart β) (o : Part α) [inst : Decidable o.Dom] [inst : (a : α) → Decidable (f a).Dom] [inst : Decidable (Part.bind o f).Dom] :
    theorem Part.bind_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_1} (f : Part α) (g : αPart β) (k : βPart γ) :
    Part.bind (Part.bind f g) k = Part.bind f fun x => Part.bind (g x) k
    @[simp]
    theorem Part.bind_map {α : Type u_2} {β : Type u_3} {γ : Type u_1} (f : αβ) (x : Part α) (g : βPart γ) :
    Part.bind (Part.map f x) g = Part.bind x fun y => g (f y)
    @[simp]
    theorem Part.map_bind {α : Type u_3} {β : Type u_2} {γ : Type u_1} (f : αPart β) (x : Part α) (g : βγ) :
    Part.map g (Part.bind x f) = Part.bind x fun y => Part.map g (f y)
    theorem Part.map_map {α : Type u_1} {β : Type u_3} {γ : Type u_2} (g : βγ) (f : αβ) (o : Part α) :
    Part.map g (Part.map f o) = Part.map (g f) o
    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 α) :
    Part.bind x Part.some = x
    @[simp]
    theorem Part.pure_eq_some {α : Type u_1} (a : α) :
    @[simp]
    theorem Part.ret_eq_some {α : Type u_1} (a : α) :
    @[simp]
    theorem Part.map_eq_map {α : Type u_1} {β : Type u_1} (f : αβ) (o : Part α) :
    f <$> o = Part.map f o
    @[simp]
    theorem Part.bind_eq_bind {α : Type u_1} {β : Type u_1} (f : Part α) (g : αPart β) :
    f >>= g = Part.bind f g
    theorem Part.bind_le {β : Type u_1} {α : Type u_1} (x : Part α) (f : αPart β) (y : Part β) :
    x >>= f y ∀ (a : α), a xf a y
    def Part.restrict {α : Type u_1} (p : Prop) (o : Part α) (H : po.Dom) :
    Part α

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

    Equations
    @[simp]
    theorem Part.mem_restrict {α : Type u_1} (p : Prop) (o : Part α) (h : po.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.

    Equations
    theorem Part.assert_defined {α : Type u_1} {p : Prop} {f : pPart α} (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 (Part.get f h)).Dom(Part.bind f g).Dom
    @[simp]
    theorem Part.bind_dom {α : Type u_1} {β : Type u_2} {f : Part α} {g : αPart β} :
    (Part.bind f g).Dom h, (g (Part.get f h)).Dom
    instance Part.instZeroPart {α : Type u_1} [inst : Zero α] :
    Zero (Part α)
    Equations
    • Part.instZeroPart = { zero := pure 0 }
    instance Part.instOnePart {α : Type u_1} [inst : One α] :
    One (Part α)
    Equations
    • Part.instOnePart = { one := pure 1 }
    instance Part.instAddPart {α : Type u_1} [inst : Add α] :
    Add (Part α)
    Equations
    • Part.instAddPart = { add := fun a b => Seq.seq ((fun x x_1 => x + x_1) <$> a) fun x => b }
    instance Part.instMulPart {α : Type u_1} [inst : Mul α] :
    Mul (Part α)
    Equations
    • Part.instMulPart = { mul := fun a b => Seq.seq ((fun x x_1 => x * x_1) <$> a) fun x => b }
    instance Part.instNegPart {α : Type u_1} [inst : Neg α] :
    Neg (Part α)
    Equations
    • Part.instNegPart = { neg := Part.map Neg.neg }
    instance Part.instInvPart {α : Type u_1} [inst : Inv α] :
    Inv (Part α)
    Equations
    • Part.instInvPart = { inv := Part.map Inv.inv }
    instance Part.instSubPart {α : Type u_1} [inst : Sub α] :
    Sub (Part α)
    Equations
    • Part.instSubPart = { sub := fun a b => Seq.seq ((fun x x_1 => x - x_1) <$> a) fun x => b }
    instance Part.instDivPart {α : Type u_1} [inst : Div α] :
    Div (Part α)
    Equations
    • Part.instDivPart = { div := fun a b => Seq.seq ((fun x x_1 => x / x_1) <$> a) fun x => b }
    instance Part.instModPart {α : Type u_1} [inst : Mod α] :
    Mod (Part α)
    Equations
    • Part.instModPart = { mod := fun a b => Seq.seq ((fun x x_1 => x % x_1) <$> a) fun x => b }
    instance Part.instAppendPart {α : Type u_1} [inst : Append α] :
    Equations
    • Part.instAppendPart = { append := fun a b => Seq.seq ((fun x x_1 => x ++ x_1) <$> a) fun x => b }
    instance Part.instInterPart {α : Type u_1} [inst : Inter α] :
    Inter (Part α)
    Equations
    • Part.instInterPart = { inter := fun a b => Seq.seq ((fun x x_1 => x x_1) <$> a) fun x => b }
    instance Part.instUnionPart {α : Type u_1} [inst : Union α] :
    Union (Part α)
    Equations
    • Part.instUnionPart = { union := fun a b => Seq.seq ((fun x x_1 => x x_1) <$> a) fun x => b }
    instance Part.instSDiffPart {α : Type u_1} [inst : SDiff α] :
    SDiff (Part α)
    Equations
    • Part.instSDiffPart = { sdiff := fun a b => Seq.seq ((fun x x_1 => x \ x_1) <$> a) fun x => b }
    theorem Part.mul_def {α : Type u_1} [inst : 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} [inst : One α] :
    theorem Part.inv_def {α : Type u_1} [inst : Inv α] (a : Part α) :
    a⁻¹ = Part.map (fun x => x⁻¹) a
    theorem Part.div_def {α : Type u_1} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Zero α] :
    0 0
    theorem Part.one_mem_one {α : Type u_1} [inst : One α] :
    1 1
    theorem Part.add_mem_add {α : Type u_1} [inst : 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} [inst : 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} [inst : Add α] {a : Part α} {b : Part α} (hab : (a + b).Dom) :
    a.Dom
    theorem Part.left_dom_of_mul_dom {α : Type u_1} [inst : Mul α] {a : Part α} {b : Part α} (hab : (a * b).Dom) :
    a.Dom
    theorem Part.right_dom_of_add_dom {α : Type u_1} [inst : Add α] {a : Part α} {b : Part α} (hab : (a + b).Dom) :
    b.Dom
    theorem Part.right_dom_of_mul_dom {α : Type u_1} [inst : Mul α] {a : Part α} {b : Part α} (hab : (a * b).Dom) :
    b.Dom
    @[simp]
    theorem Part.add_get_eq {α : Type u_1} [inst : Add α] (a : Part α) (b : Part α) (hab : (a + b).Dom) :
    Part.get (a + b) hab = Part.get a (_ : a.Dom) + Part.get b (_ : b.Dom)
    @[simp]
    theorem Part.mul_get_eq {α : Type u_1} [inst : Mul α] (a : Part α) (b : Part α) (hab : (a * b).Dom) :
    Part.get (a * b) hab = Part.get a (_ : a.Dom) * Part.get b (_ : b.Dom)
    theorem Part.some_add_some {α : Type u_1} [inst : Add α] (a : α) (b : α) :
    theorem Part.some_mul_some {α : Type u_1} [inst : Mul α] (a : α) (b : α) :
    theorem Part.neg_mem_neg {α : Type u_1} [inst : Neg α] (a : Part α) (ma : α) (ha : ma a) :
    -ma -a
    theorem Part.inv_mem_inv {α : Type u_1} [inst : Inv α] (a : Part α) (ma : α) (ha : ma a) :
    theorem Part.neg_some {α : Type u_1} [inst : Neg α] (a : α) :
    theorem Part.inv_some {α : Type u_1} [inst : Inv α] (a : α) :
    theorem Part.sub_mem_sub {α : Type u_1} [inst : 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} [inst : 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} [inst : Sub α] {a : Part α} {b : Part α} (hab : (a - b).Dom) :
    a.Dom
    theorem Part.left_dom_of_div_dom {α : Type u_1} [inst : Div α] {a : Part α} {b : Part α} (hab : (a / b).Dom) :
    a.Dom
    theorem Part.right_dom_of_sub_dom {α : Type u_1} [inst : Sub α] {a : Part α} {b : Part α} (hab : (a - b).Dom) :
    b.Dom
    theorem Part.right_dom_of_div_dom {α : Type u_1} [inst : Div α] {a : Part α} {b : Part α} (hab : (a / b).Dom) :
    b.Dom
    @[simp]
    theorem Part.sub_get_eq {α : Type u_1} [inst : Sub α] (a : Part α) (b : Part α) (hab : (a - b).Dom) :
    Part.get (a - b) hab = Part.get a (_ : a.Dom) - Part.get b (_ : b.Dom)
    @[simp]
    theorem Part.div_get_eq {α : Type u_1} [inst : Div α] (a : Part α) (b : Part α) (hab : (a / b).Dom) :
    Part.get (a / b) hab = Part.get a (_ : a.Dom) / Part.get b (_ : b.Dom)
    theorem Part.some_sub_some {α : Type u_1} [inst : Sub α] (a : α) (b : α) :
    theorem Part.some_div_some {α : Type u_1} [inst : Div α] (a : α) (b : α) :
    theorem Part.mod_mem_mod {α : Type u_1} [inst : 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} [inst : Mod α] {a : Part α} {b : Part α} (hab : (a % b).Dom) :
    a.Dom
    theorem Part.right_dom_of_mod_dom {α : Type u_1} [inst : Mod α] {a : Part α} {b : Part α} (hab : (a % b).Dom) :
    b.Dom
    @[simp]
    theorem Part.mod_get_eq {α : Type u_1} [inst : Mod α] (a : Part α) (b : Part α) (hab : (a % b).Dom) :
    Part.get (a % b) hab = Part.get a (_ : a.Dom) % Part.get b (_ : b.Dom)
    theorem Part.some_mod_some {α : Type u_1} [inst : Mod α] (a : α) (b : α) :
    theorem Part.append_mem_append {α : Type u_1} [inst : 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} [inst : Append α] {a : Part α} {b : Part α} (hab : (a ++ b).Dom) :
    a.Dom
    theorem Part.right_dom_of_append_dom {α : Type u_1} [inst : Append α] {a : Part α} {b : Part α} (hab : (a ++ b).Dom) :
    b.Dom
    @[simp]
    theorem Part.append_get_eq {α : Type u_1} [inst : Append α] (a : Part α) (b : Part α) (hab : (a ++ b).Dom) :
    Part.get (a ++ b) hab = Part.get a (_ : a.Dom) ++ Part.get b (_ : b.Dom)
    theorem Part.some_append_some {α : Type u_1} [inst : Append α] (a : α) (b : α) :
    theorem Part.inter_mem_inter {α : Type u_1} [inst : 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} [inst : Inter α] {a : Part α} {b : Part α} (hab : (a b).Dom) :
    a.Dom
    theorem Part.right_dom_of_inter_dom {α : Type u_1} [inst : Inter α] {a : Part α} {b : Part α} (hab : (a b).Dom) :
    b.Dom
    @[simp]
    theorem Part.inter_get_eq {α : Type u_1} [inst : Inter α] (a : Part α) (b : Part α) (hab : (a b).Dom) :
    Part.get (a b) hab = Part.get a (_ : a.Dom) Part.get b (_ : b.Dom)
    theorem Part.some_inter_some {α : Type u_1} [inst : Inter α] (a : α) (b : α) :
    theorem Part.union_mem_union {α : Type u_1} [inst : 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} [inst : Union α] {a : Part α} {b : Part α} (hab : (a b).Dom) :
    a.Dom
    theorem Part.right_dom_of_union_dom {α : Type u_1} [inst : Union α] {a : Part α} {b : Part α} (hab : (a b).Dom) :
    b.Dom
    @[simp]
    theorem Part.union_get_eq {α : Type u_1} [inst : Union α] (a : Part α) (b : Part α) (hab : (a b).Dom) :
    Part.get (a b) hab = Part.get a (_ : a.Dom) Part.get b (_ : b.Dom)
    theorem Part.some_union_some {α : Type u_1} [inst : Union α] (a : α) (b : α) :
    theorem Part.sdiff_mem_sdiff {α : Type u_1} [inst : 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} [inst : SDiff α] {a : Part α} {b : Part α} (hab : (a \ b).Dom) :
    a.Dom
    theorem Part.right_dom_of_sdiff_dom {α : Type u_1} [inst : SDiff α] {a : Part α} {b : Part α} (hab : (a \ b).Dom) :
    b.Dom
    @[simp]
    theorem Part.sdiff_get_eq {α : Type u_1} [inst : SDiff α] (a : Part α) (b : Part α) (hab : (a \ b).Dom) :
    Part.get (a \ b) hab = Part.get a (_ : a.Dom) \ Part.get b (_ : b.Dom)
    theorem Part.some_sdiff_some {α : Type u_1} [inst : SDiff α] (a : α) (b : α) :