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 means that o is defined and equal to a. Formally, it means o.Dom and o.get _ = a.

structure Part (α : 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

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

    Convert a Part α with a decidable domain to an option

    Equations
    • o.toOption = if h : o.Dom then some (o.get h) else none
    Instances For
      @[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 : α) :

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

      Equations
      • o.Mem a = ∃ (h : o.Dom), o.get h = a
      Instances For
        instance Part.instMembership {α : Type u_1} :
        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
        Instances For
          instance Part.instInhabited {α : Type u_1} :
          Equations
          • Part.instInhabited = { default := Part.none }
          @[simp]
          theorem Part.not_mem_none {α : Type u_1} (a : α) :
          aPart.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
          Instances For
            @[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 (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 : α) :
            @[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 : α), ao
            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} :
            @[simp]
            theorem Part.some_inj {α : Type u_1} {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
            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
            Instances For
              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
              Instances For
                @[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
                @[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 α is (classically) equivalent to Option α.

                Equations
                • Part.equivOption = { toFun := fun (o : Part α) => o.toOption, invFun := Part.ofOption, left_inv := , right_inv := }
                Instances For
                  instance Part.instPartialOrder {α : Type u_1} :

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

                  Equations
                  instance Part.instOrderBot {α : Type u_1} :
                  Equations
                  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
                  • Part.assert p f = { Dom := ∃ (h : p), (f h).Dom, get := fun (ha : ∃ (h : p), (f h).Dom) => (f ).get }
                  Instances For
                    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
                    Instances For
                      @[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
                      Instances For
                        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 ao, 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 : α) :
                        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 : p), 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 f.bind g
                        @[simp]
                        theorem Part.mem_bind_iff {α : Type u_1} {β : Type u_2} {f : Part α} {g : αPart β} {b : β} :
                        b f.bind g af, 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
                        Equations
                        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 : α) :
                        @[simp]
                        theorem Part.ret_eq_some {α : Type u_1} (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 ax, f 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
                        Instances For
                          @[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.

                          Instances For
                            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 (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
                            instance Part.instInv {α : Type u_1} [Inv α] :
                            Inv (Part α)
                            Equations
                            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 α] :
                            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 ya Part.map (fun (x : α) => y * x) b
                            theorem Part.one_def {α : Type u_1} [One α] :
                            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 ya Part.map (fun (x : α) => y / x) b
                            theorem Part.mod_def {α : Type u_1} [Mod α] (a : Part α) (b : Part α) :
                            a % b = do let ya Part.map (fun (x : α) => y % x) b
                            theorem Part.append_def {α : Type u_1} [Append α] (a : Part α) (b : Part α) :
                            a ++ b = do let ya Part.map (fun (x : α) => y ++ x) b
                            theorem Part.inter_def {α : Type u_1} [Inter α] (a : Part α) (b : Part α) :
                            a b = do let ya Part.map (fun (x : α) => y x) b
                            theorem Part.union_def {α : Type u_1} [Union α] (a : Part α) (b : Part α) :
                            a b = do let ya Part.map (fun (x : α) => y x) b
                            theorem Part.sdiff_def {α : Type u_1} [SDiff α] (a : Part α) (b : Part α) :
                            a \ b = do let ya 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 : α) :
                            theorem Part.some_mul_some {α : Type u_1} [Mul α] (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) :
                            theorem Part.neg_some {α : Type u_1} [Neg α] (a : α) :
                            theorem Part.inv_some {α : Type u_1} [Inv α] (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 : α) :
                            theorem Part.some_div_some {α : Type u_1} [Div α] (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 : α) :
                            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 : α) :
                            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 : α) :
                            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 : α) :
                            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 : α) :