Documentation

Mathlib.Data.PFun

Partial functions #

This file defines partial functions. Partial functions are like functions, except they can also be "undefined" on some inputs. We define them as functions α → Part β.

Definitions #

Partial functions as relations #

Partial functions can be considered as relations, so we specialize some Rel definitions to PFun:

PFun α as a monad #

Monad operations:

def PFun (α : Type u_1) (β : Type u_2) :
Type (max u_1 u_2)

PFun α β, or α →. β, is the type of partial functions from α to β. It is defined as α → Part β.

Equations
Instances For

    α →. β is notation for the type PFun α β of partial functions from α to β.

    Equations
    Instances For
      instance PFun.inhabited {α : Type u_1} {β : Type u_2} :
      Inhabited (α →. β)
      Equations
      • PFun.inhabited = { default := fun (x : α) => Part.none }
      def PFun.Dom {α : Type u_1} {β : Type u_2} (f : α →. β) :
      Set α

      The domain of a partial function

      Equations
      • f.Dom = {a : α | (f a).Dom}
      Instances For
        @[simp]
        theorem PFun.mem_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) :
        x f.Dom ∃ (y : β), y f x
        @[simp]
        theorem PFun.dom_mk {α : Type u_1} {β : Type u_2} (p : αProp) (f : (a : α) → p aβ) :
        (PFun.Dom fun (x : α) => { Dom := p x, get := f x }) = {x : α | p x}
        theorem PFun.dom_eq {α : Type u_1} {β : Type u_2} (f : α →. β) :
        f.Dom = {x : α | ∃ (y : β), y f x}
        def PFun.fn {α : Type u_1} {β : Type u_2} (f : α →. β) (a : α) :
        f.Dom aβ

        Evaluate a partial function

        Equations
        • f.fn a = (f a).get
        Instances For
          @[simp]
          theorem PFun.fn_apply {α : Type u_1} {β : Type u_2} (f : α →. β) (a : α) :
          f.fn a = (f a).get
          def PFun.evalOpt {α : Type u_1} {β : Type u_2} (f : α →. β) [D : DecidablePred fun (x : α) => x f.Dom] (x : α) :

          Evaluate a partial function to return an Option

          Equations
          • f.evalOpt x = (f x).toOption
          Instances For
            theorem PFun.ext' {α : Type u_1} {β : Type u_2} {f : α →. β} {g : α →. β} (H1 : ∀ (a : α), a f.Dom a g.Dom) (H2 : ∀ (a : α) (p : f.Dom a) (q : g.Dom a), f.fn a p = g.fn a q) :
            f = g

            Partial function extensionality

            theorem PFun.ext {α : Type u_1} {β : Type u_2} {f : α →. β} {g : α →. β} (H : ∀ (a : α) (b : β), b f a b g a) :
            f = g
            def PFun.asSubtype {α : Type u_1} {β : Type u_2} (f : α →. β) (s : f.Dom) :
            β

            Turns a partial function into a function out of its domain.

            Equations
            • f.asSubtype s = f.fn s
            Instances For
              def PFun.equivSubtype {α : Type u_1} {β : Type u_2} :
              (α →. β) (p : αProp) × (Subtype pβ)

              The type of partial functions α →. β is equivalent to the type of pairs (p : α → Prop, f : Subtype p → β).

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem PFun.asSubtype_eq_of_mem {α : Type u_1} {β : Type u_2} {f : α →. β} {x : α} {y : β} (fxy : y f x) (domx : x f.Dom) :
                f.asSubtype x, domx = y
                def PFun.lift {α : Type u_1} {β : Type u_2} (f : αβ) :
                α →. β

                Turn a total function into a partial function.

                Equations
                Instances For
                  instance PFun.coe {α : Type u_1} {β : Type u_2} :
                  Coe (αβ) (α →. β)
                  Equations
                  • PFun.coe = { coe := PFun.lift }
                  @[simp]
                  theorem PFun.coe_val {α : Type u_1} {β : Type u_2} (f : αβ) (a : α) :
                  f a = Part.some (f a)
                  @[simp]
                  theorem PFun.dom_coe {α : Type u_1} {β : Type u_2} (f : αβ) :
                  (f).Dom = Set.univ
                  theorem PFun.lift_injective {α : Type u_1} {β : Type u_2} :
                  def PFun.graph {α : Type u_1} {β : Type u_2} (f : α →. β) :
                  Set (α × β)

                  Graph of a partial function f as the set of pairs (x, f x) where x is in the domain of f.

                  Equations
                  • f.graph = {p : α × β | p.2 f p.1}
                  Instances For
                    def PFun.graph' {α : Type u_1} {β : Type u_2} (f : α →. β) :
                    Rel α β

                    Graph of a partial function as a relation. x and y are related iff f x is defined and "equals" y.

                    Equations
                    • f.graph' x y = (y f x)
                    Instances For
                      def PFun.ran {α : Type u_1} {β : Type u_2} (f : α →. β) :
                      Set β

                      The range of a partial function is the set of values f x where x is in the domain of f.

                      Equations
                      • f.ran = {b : β | ∃ (a : α), b f a}
                      Instances For
                        def PFun.restrict {α : Type u_1} {β : Type u_2} (f : α →. β) {p : Set α} (H : p f.Dom) :
                        α →. β

                        Restrict a partial function to a smaller domain.

                        Equations
                        Instances For
                          @[simp]
                          theorem PFun.mem_restrict {α : Type u_1} {β : Type u_2} {f : α →. β} {s : Set α} (h : s f.Dom) (a : α) (b : β) :
                          b f.restrict h a a s b f a
                          def PFun.res {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) :
                          α →. β

                          Turns a function into a partial function with a prescribed domain.

                          Equations
                          Instances For
                            theorem PFun.mem_res {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (a : α) (b : β) :
                            b PFun.res f s a a s f a = b
                            theorem PFun.res_univ {α : Type u_1} {β : Type u_2} (f : αβ) :
                            PFun.res f Set.univ = f
                            theorem PFun.dom_iff_graph {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) :
                            x f.Dom ∃ (y : β), (x, y) f.graph
                            theorem PFun.lift_graph {α : Type u_1} {β : Type u_2} {f : αβ} {a : α} {b : β} :
                            (a, b) (f).graph f a = b
                            def PFun.pure {α : Type u_1} {β : Type u_2} (x : β) :
                            α →. β

                            The monad pure function, the total constant x function

                            Equations
                            Instances For
                              def PFun.bind {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : βα →. γ) :
                              α →. γ

                              The monad bind function, pointwise Part.bind

                              Equations
                              • f.bind g a = (f a).bind fun (b : β) => g b a
                              Instances For
                                @[simp]
                                theorem PFun.bind_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : βα →. γ) (a : α) :
                                f.bind g a = (f a).bind fun (b : β) => g b a
                                def PFun.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : βγ) (g : α →. β) :
                                α →. γ

                                The monad map function, pointwise Part.map

                                Equations
                                Instances For
                                  instance PFun.monad {α : Type u_1} :
                                  Monad (PFun α)
                                  Equations
                                  • PFun.monad = Monad.mk
                                  instance PFun.lawfulMonad {α : Type u_1} :
                                  Equations
                                  • =
                                  theorem PFun.pure_defined {α : Type u_1} {β : Type u_2} (p : Set α) (x : β) :
                                  p (PFun.pure x).Dom
                                  theorem PFun.bind_defined {α : Type u_7} {β : Type u_8} {γ : Type u_8} (p : Set α) {f : α →. β} {g : βα →. γ} (H1 : p f.Dom) (H2 : ∀ (x : β), p (g x).Dom) :
                                  p (f >>= g).Dom
                                  def PFun.fix {α : Type u_1} {β : Type u_2} (f : α →. β α) :
                                  α →. β

                                  First return map. Transforms a partial function f : α →. β ⊕ α into the partial function α →. β which sends a : α to the first value in β it hits by iterating f, if such a value exists. By abusing notation to illustrate, either f a is in the β part of β ⊕ α (in which case f.fix a returns f a), or it is undefined (in which case f.fix a is undefined as well), or it is in the α part of β ⊕ α (in which case we repeat the procedure, so f.fix a will return f.fix (f a)).

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    theorem PFun.dom_of_mem_fix {α : Type u_1} {β : Type u_2} {f : α →. β α} {a : α} {b : β} (h : b f.fix a) :
                                    (f a).Dom
                                    theorem PFun.mem_fix_iff {α : Type u_1} {β : Type u_2} {f : α →. β α} {a : α} {b : β} :
                                    b f.fix a Sum.inl b f a ∃ (a' : α), Sum.inr a' f a b f.fix a'
                                    theorem PFun.fix_stop {α : Type u_1} {β : Type u_2} {f : α →. β α} {b : β} {a : α} (hb : Sum.inl b f a) :
                                    b f.fix a

                                    If advancing one step from a leads to b : β, then f.fix a = b

                                    theorem PFun.fix_fwd_eq {α : Type u_1} {β : Type u_2} {f : α →. β α} {a : α} {a' : α} (ha' : Sum.inr a' f a) :
                                    f.fix a = f.fix a'

                                    If advancing one step from a on f leads to a' : α, then f.fix a = f.fix a'

                                    theorem PFun.fix_fwd {α : Type u_1} {β : Type u_2} {f : α →. β α} {b : β} {a : α} {a' : α} (hb : b f.fix a) (ha' : Sum.inr a' f a) :
                                    b f.fix a'
                                    def PFun.fixInduction {α : Type u_1} {β : Type u_2} {C : αSort u_7} {f : α →. β α} {b : β} {a : α} (h : b f.fix a) (H : (a' : α) → b f.fix a'((a'' : α) → Sum.inr a'' f a'C a'')C a') :
                                    C a

                                    A recursion principle for PFun.fix.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      theorem PFun.fixInduction_spec {α : Type u_1} {β : Type u_2} {C : αSort u_7} {f : α →. β α} {b : β} {a : α} (h : b f.fix a) (H : (a' : α) → b f.fix a'((a'' : α) → Sum.inr a'' f a'C a'')C a') :
                                      PFun.fixInduction h H = H a h fun (a' : α) (h' : Sum.inr a' f a) => PFun.fixInduction H
                                      def PFun.fixInduction' {α : Type u_1} {β : Type u_2} {C : αSort u_7} {f : α →. β α} {b : β} {a : α} (h : b f.fix a) (hbase : (a_final : α) → Sum.inl b f a_finalC a_final) (hind : (a₀ a₁ : α) → b f.fix a₁Sum.inr a₁ f a₀C a₁C a₀) :
                                      C a

                                      Another induction lemma for b ∈ f.fix a which allows one to prove a predicate P holds for a given that f a inherits P from a and P holds for preimages of b.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        theorem PFun.fixInduction'_stop {α : Type u_1} {β : Type u_2} {C : αSort u_7} {f : α →. β α} {b : β} {a : α} (h : b f.fix a) (fa : Sum.inl b f a) (hbase : (a_final : α) → Sum.inl b f a_finalC a_final) (hind : (a₀ a₁ : α) → b f.fix a₁Sum.inr a₁ f a₀C a₁C a₀) :
                                        PFun.fixInduction' h hbase hind = hbase a fa
                                        theorem PFun.fixInduction'_fwd {α : Type u_1} {β : Type u_2} {C : αSort u_7} {f : α →. β α} {b : β} {a : α} {a' : α} (h : b f.fix a) (h' : b f.fix a') (fa : Sum.inr a' f a) (hbase : (a_final : α) → Sum.inl b f a_finalC a_final) (hind : (a₀ a₁ : α) → b f.fix a₁Sum.inr a₁ f a₀C a₁C a₀) :
                                        PFun.fixInduction' h hbase hind = hind a a' h' fa (PFun.fixInduction' h' hbase hind)
                                        def PFun.image {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) :
                                        Set β

                                        Image of a set under a partial function.

                                        Equations
                                        • f.image s = f.graph'.image s
                                        Instances For
                                          theorem PFun.image_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) :
                                          f.image s = {y : β | xs, y f x}
                                          theorem PFun.mem_image {α : Type u_1} {β : Type u_2} (f : α →. β) (y : β) (s : Set α) :
                                          y f.image s xs, y f x
                                          theorem PFun.image_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s : Set α} {t : Set α} (h : s t) :
                                          f.image s f.image t
                                          theorem PFun.image_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) (t : Set α) :
                                          f.image (s t) f.image s f.image t
                                          theorem PFun.image_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set α) (t : Set α) :
                                          f.image (s t) = f.image s f.image t
                                          def PFun.preimage {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
                                          Set α

                                          Preimage of a set under a partial function.

                                          Equations
                                          Instances For
                                            theorem PFun.Preimage_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
                                            f.preimage s = {x : α | ys, y f x}
                                            @[simp]
                                            theorem PFun.mem_preimage {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (x : α) :
                                            x f.preimage s ys, y f x
                                            theorem PFun.preimage_subset_dom {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
                                            f.preimage s f.Dom
                                            theorem PFun.preimage_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s : Set β} {t : Set β} (h : s t) :
                                            f.preimage s f.preimage t
                                            theorem PFun.preimage_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (t : Set β) :
                                            f.preimage (s t) f.preimage s f.preimage t
                                            theorem PFun.preimage_union {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (t : Set β) :
                                            f.preimage (s t) = f.preimage s f.preimage t
                                            theorem PFun.preimage_univ {α : Type u_1} {β : Type u_2} (f : α →. β) :
                                            f.preimage Set.univ = f.Dom
                                            theorem PFun.coe_preimage {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set β) :
                                            (f).preimage s = f ⁻¹' s
                                            def PFun.core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
                                            Set α

                                            Core of a set s : Set β with respect to a partial function f : α →. β. Set of all a : α such that f a ∈ s, if f a is defined.

                                            Equations
                                            • f.core s = f.graph'.core s
                                            Instances For
                                              theorem PFun.core_def {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
                                              f.core s = {x : α | yf x, y s}
                                              @[simp]
                                              theorem PFun.mem_core {α : Type u_1} {β : Type u_2} (f : α →. β) (x : α) (s : Set β) :
                                              x f.core s yf x, y s
                                              theorem PFun.compl_dom_subset_core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
                                              f.Dom f.core s
                                              theorem PFun.core_mono {α : Type u_1} {β : Type u_2} (f : α →. β) {s : Set β} {t : Set β} (h : s t) :
                                              f.core s f.core t
                                              theorem PFun.core_inter {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (t : Set β) :
                                              f.core (s t) = f.core s f.core t
                                              theorem PFun.mem_core_res {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) (x : α) :
                                              x (PFun.res f s).core t x sf x t
                                              theorem PFun.core_res {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set α) (t : Set β) :
                                              (PFun.res f s).core t = s f ⁻¹' t
                                              theorem PFun.core_restrict {α : Type u_1} {β : Type u_2} (f : αβ) (s : Set β) :
                                              (f).core s = f ⁻¹' s
                                              theorem PFun.preimage_subset_core {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
                                              f.preimage s f.core s
                                              theorem PFun.preimage_eq {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
                                              f.preimage s = f.core s f.Dom
                                              theorem PFun.core_eq {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
                                              f.core s = f.preimage s f.Dom
                                              theorem PFun.preimage_asSubtype {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) :
                                              f.asSubtype ⁻¹' s = Subtype.val ⁻¹' f.preimage s
                                              def PFun.toSubtype {α : Type u_1} {β : Type u_2} (p : βProp) (f : αβ) :

                                              Turns a function into a partial function to a subtype.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem PFun.dom_toSubtype {α : Type u_1} {β : Type u_2} (p : βProp) (f : αβ) :
                                                (PFun.toSubtype p f).Dom = {a : α | p (f a)}
                                                @[simp]
                                                theorem PFun.toSubtype_apply {α : Type u_1} {β : Type u_2} (p : βProp) (f : αβ) (a : α) :
                                                PFun.toSubtype p f a = { Dom := p (f a), get := Subtype.mk (f a) }
                                                theorem PFun.dom_toSubtype_apply_iff {α : Type u_1} {β : Type u_2} {p : βProp} {f : αβ} {a : α} :
                                                (PFun.toSubtype p f a).Dom p (f a)
                                                theorem PFun.mem_toSubtype_iff {α : Type u_1} {β : Type u_2} {p : βProp} {f : αβ} {a : α} {b : Subtype p} :
                                                b PFun.toSubtype p f a b = f a
                                                def PFun.id (α : Type u_7) :
                                                α →. α

                                                The identity as a partial function

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem PFun.coe_id (α : Type u_7) :
                                                  id = PFun.id α
                                                  @[simp]
                                                  theorem PFun.id_apply {α : Type u_1} (a : α) :
                                                  def PFun.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) :
                                                  α →. γ

                                                  Composition of partial functions as a partial function.

                                                  Equations
                                                  • f.comp g a = (g a).bind f
                                                  Instances For
                                                    @[simp]
                                                    theorem PFun.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (a : α) :
                                                    f.comp g a = (g a).bind f
                                                    @[simp]
                                                    theorem PFun.id_comp {α : Type u_1} {β : Type u_2} (f : α →. β) :
                                                    (PFun.id β).comp f = f
                                                    @[simp]
                                                    theorem PFun.comp_id {α : Type u_1} {β : Type u_2} (f : α →. β) :
                                                    f.comp (PFun.id α) = f
                                                    @[simp]
                                                    theorem PFun.dom_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) :
                                                    (f.comp g).Dom = g.preimage f.Dom
                                                    @[simp]
                                                    theorem PFun.preimage_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (s : Set γ) :
                                                    (f.comp g).preimage s = g.preimage (f.preimage s)
                                                    @[simp]
                                                    theorem PFun.Part.bind_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : β →. γ) (g : α →. β) (a : Part α) :
                                                    a.bind (f.comp g) = (a.bind g).bind f
                                                    @[simp]
                                                    theorem PFun.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : γ →. δ) (g : β →. γ) (h : α →. β) :
                                                    (f.comp g).comp h = f.comp (g.comp h)
                                                    theorem PFun.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : βγ) (f : αβ) :
                                                    (g f) = (g).comp f
                                                    def PFun.prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) :
                                                    α →. β × γ

                                                    Product of partial functions.

                                                    Equations
                                                    • f.prodLift g x = { Dom := (f x).Dom (g x).Dom, get := fun (h : (f x).Dom (g x).Dom) => ((f x).get , (g x).get ) }
                                                    Instances For
                                                      @[simp]
                                                      theorem PFun.dom_prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) :
                                                      (f.prodLift g).Dom = {x : α | (f x).Dom (g x).Dom}
                                                      theorem PFun.get_prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) (x : α) (h : (f.prodLift g x).Dom) :
                                                      (f.prodLift g x).get h = ((f x).get , (g x).get )
                                                      @[simp]
                                                      theorem PFun.prodLift_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : α →. γ) (x : α) :
                                                      f.prodLift g x = { Dom := (f x).Dom (g x).Dom, get := fun (h : (f x).Dom (g x).Dom) => ((f x).get , (g x).get ) }
                                                      theorem PFun.mem_prodLift {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α →. β} {g : α →. γ} {x : α} {y : β × γ} :
                                                      y f.prodLift g x y.1 f x y.2 g x
                                                      def PFun.prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) :
                                                      α × β →. γ × δ

                                                      Product of partial functions.

                                                      Equations
                                                      • f.prodMap g x = { Dom := (f x.1).Dom (g x.2).Dom, get := fun (h : (f x.1).Dom (g x.2).Dom) => ((f x.1).get , (g x.2).get ) }
                                                      Instances For
                                                        @[simp]
                                                        theorem PFun.dom_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) :
                                                        (f.prodMap g).Dom = {x : α × β | (f x.1).Dom (g x.2).Dom}
                                                        theorem PFun.get_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) (x : α × β) (h : (f.prodMap g x).Dom) :
                                                        (f.prodMap g x).get h = ((f x.1).get , (g x.2).get )
                                                        @[simp]
                                                        theorem PFun.prodMap_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) (x : α × β) :
                                                        f.prodMap g x = { Dom := (f x.1).Dom (g x.2).Dom, get := fun (h : (f x.1).Dom (g x.2).Dom) => ((f x.1).get , (g x.2).get ) }
                                                        theorem PFun.mem_prodMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α →. γ} {g : β →. δ} {x : α × β} {y : γ × δ} :
                                                        y f.prodMap g x y.1 f x.1 y.2 g x.2
                                                        @[simp]
                                                        theorem PFun.prodLift_fst_comp_snd_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α →. γ) (g : β →. δ) :
                                                        (f.comp Prod.fst).prodLift (g.comp Prod.snd) = f.prodMap g
                                                        @[simp]
                                                        theorem PFun.prodMap_id_id {α : Type u_1} {β : Type u_2} :
                                                        (PFun.id α).prodMap (PFun.id β) = PFun.id (α × β)
                                                        @[simp]
                                                        theorem PFun.prodMap_comp_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ι : Type u_6} (f₁ : α →. β) (f₂ : β →. γ) (g₁ : δ →. ε) (g₂ : ε →. ι) :
                                                        (f₂.comp f₁).prodMap (g₂.comp g₁) = (f₂.prodMap g₂).comp (f₁.prodMap g₁)