Documentation

Mathlib.Logic.Equiv.Basic

Equivalence between types #

In this file we continue the work on equivalences begun in Mathlib/Logic/Equiv/Defs.lean, defining a lot of equivalences between various types and operations on these equivalences.

More definitions of this kind can be found in other files. E.g., Mathlib/Algebra/Equiv/TransferInstance.lean does it for many algebraic type classes like Group, Module, etc.

Tags #

equivalence, congruence, bijective map

def Equiv.piOptionEquivProd {α : Type u_10} {β : Option αType u_9} :
((a : Option α) → β a) β none × ((a : α) → β (some a))

The product over Option α of β a is the binary product of the product over α of β (some α) and β none

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Equiv.piOptionEquivProd_symm_apply {α : Type u_10} {β : Option αType u_9} (x : β none × ((a : α) → β (some a))) (a : Option α) :
    @[simp]
    theorem Equiv.piOptionEquivProd_apply {α : Type u_10} {β : Option αType u_9} (f : (a : Option α) → β a) :
    piOptionEquivProd f = (f none, fun (a : α) => f (some a))
    def Equiv.subtypeCongr {α : Type u_9} {p q : αProp} [DecidablePred p] [DecidablePred q] (e : { x : α // p x } { x : α // q x }) (f : { x : α // ¬p x } { x : α // ¬q x }) :
    Perm α

    Combines an Equiv between two subtypes with an Equiv between their complements to form a permutation.

    Equations
    Instances For
      def Equiv.Perm.subtypeCongr {ε : Type u_9} {p : εProp} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) :
      Perm ε

      Combining permutations on ε that permute only inside or outside the subtype split induced by p : ε → Prop constructs a permutation on ε.

      Equations
      Instances For
        theorem Equiv.Perm.subtypeCongr.apply {ε : Type u_9} {p : εProp} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) (a : ε) :
        (ep.subtypeCongr en) a = if h : p a then (ep a, h) else (en a, h)
        @[simp]
        theorem Equiv.Perm.subtypeCongr.left_apply {ε : Type u_9} {p : εProp} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) {a : ε} (h : p a) :
        (ep.subtypeCongr en) a = (ep a, h)
        @[simp]
        theorem Equiv.Perm.subtypeCongr.left_apply_subtype {ε : Type u_9} {p : εProp} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) (a : { a : ε // p a }) :
        (ep.subtypeCongr en) a = (ep a)
        @[simp]
        theorem Equiv.Perm.subtypeCongr.right_apply {ε : Type u_9} {p : εProp} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) {a : ε} (h : ¬p a) :
        (ep.subtypeCongr en) a = (en a, h)
        @[simp]
        theorem Equiv.Perm.subtypeCongr.right_apply_subtype {ε : Type u_9} {p : εProp} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) (a : { a : ε // ¬p a }) :
        (ep.subtypeCongr en) a = (en a)
        @[simp]
        theorem Equiv.Perm.subtypeCongr.refl {ε : Type u_9} {p : εProp} [DecidablePred p] :
        subtypeCongr (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) = Equiv.refl ε
        @[simp]
        theorem Equiv.Perm.subtypeCongr.symm {ε : Type u_9} {p : εProp} [DecidablePred p] (ep : Perm { a : ε // p a }) (en : Perm { a : ε // ¬p a }) :
        @[simp]
        theorem Equiv.Perm.subtypeCongr.trans {ε : Type u_9} {p : εProp} [DecidablePred p] (ep ep' : Perm { a : ε // p a }) (en en' : Perm { a : ε // ¬p a }) :
        def Equiv.subtypePreimage {α : Sort u_1} {β : Sort u_4} (p : αProp) [DecidablePred p] (x₀ : { a : α // p a }β) :
        { x : αβ // x Subtype.val = x₀ } ({ a : α // ¬p a }β)

        For a fixed function x₀ : {a // p a} → β defined on a subtype of α, the subtype of functions x : α → β that agree with x₀ on the subtype {a // p a} is naturally equivalent to the type of functions {a // ¬ p a} → β.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem Equiv.subtypePreimage_symm_apply_coe {α : Sort u_1} {β : Sort u_4} (p : αProp) [DecidablePred p] (x₀ : { a : α // p a }β) (x : { a : α // ¬p a }β) (a : α) :
          ((subtypePreimage p x₀).symm x) a = if h : p a then x₀ a, h else x a, h
          @[simp]
          theorem Equiv.subtypePreimage_apply {α : Sort u_1} {β : Sort u_4} (p : αProp) [DecidablePred p] (x₀ : { a : α // p a }β) (x : { x : αβ // x Subtype.val = x₀ }) (a : { a : α // ¬p a }) :
          (subtypePreimage p x₀) x a = x a
          theorem Equiv.subtypePreimage_symm_apply_coe_pos {α : Sort u_1} {β : Sort u_4} (p : αProp) [DecidablePred p] (x₀ : { a : α // p a }β) (x : { a : α // ¬p a }β) (a : α) (h : p a) :
          ((subtypePreimage p x₀).symm x) a = x₀ a, h
          theorem Equiv.subtypePreimage_symm_apply_coe_neg {α : Sort u_1} {β : Sort u_4} (p : αProp) [DecidablePred p] (x₀ : { a : α // p a }β) (x : { a : α // ¬p a }β) (a : α) (h : ¬p a) :
          ((subtypePreimage p x₀).symm x) a = x a, h
          def Equiv.piCongrRight {α : Sort u_1} {β₁ : αSort u_9} {β₂ : αSort u_10} (F : (a : α) → β₁ a β₂ a) :
          ((a : α) → β₁ a) ((a : α) → β₂ a)

          A family of equivalences ∀ a, β₁ a ≃ β₂ a generates an equivalence between ∀ a, β₁ a and ∀ a, β₂ a.

          Equations
          Instances For
            @[simp]
            theorem Equiv.piCongrRight_apply {α : Sort u_1} {β₁ : αSort u_9} {β₂ : αSort u_10} (F : (a : α) → β₁ a β₂ a) (a✝ : (i : α) → β₁ i) (i : α) :
            (piCongrRight F) a✝ i = Pi.map (fun (a : α) => (F a)) a✝ i
            @[simp]
            theorem Equiv.piCongrRight_symm_apply {α : Sort u_1} {β₁ : αSort u_9} {β₂ : αSort u_10} (F : (a : α) → β₁ a β₂ a) (a✝ : (i : α) → β₂ i) (i : α) :
            (piCongrRight F).symm a✝ i = Pi.map (fun (a : α) => (F a).symm) a✝ i
            def Equiv.piComm {α : Sort u_1} {β : Sort u_4} (φ : αβSort u_9) :
            ((a : α) → (b : β) → φ a b) ((b : β) → (a : α) → φ a b)

            Given φ : α → β → Sort*, we have an equivalence between ∀ a b, φ a b and ∀ b a, φ a b. This is Function.swap as an Equiv.

            Equations
            Instances For
              @[simp]
              theorem Equiv.piComm_apply {α : Sort u_1} {β : Sort u_4} (φ : αβSort u_9) (f : (x : α) → (y : β) → φ x y) (y : β) (x : α) :
              (piComm φ) f y x = Function.swap f y x
              @[simp]
              theorem Equiv.piComm_symm {α : Sort u_1} {β : Sort u_4} {φ : αβSort u_9} :
              def Equiv.piCurry {α : Type u_11} {β : αType u_9} (γ : (a : α) → β aType u_10) :
              ((x : (i : α) × β i) → γ x.fst x.snd) ((a : α) → (b : β a) → γ a b)

              Dependent curry equivalence: the type of dependent functions on Σ i, β i is equivalent to the type of dependent functions of two arguments (i.e., functions to the space of functions).

              This is Sigma.curry and Sigma.uncurry together as an equiv.

              Equations
              Instances For
                @[simp]
                theorem Equiv.piCurry_apply {α : Type u_11} {β : αType u_9} (γ : (a : α) → β aType u_10) (f : (x : (i : α) × β i) → γ x.fst x.snd) :
                @[simp]
                theorem Equiv.piCurry_symm_apply {α : Type u_11} {β : αType u_9} (γ : (a : α) → β aType u_10) (f : (a : α) → (b : β a) → γ a b) :
                def Equiv.ofFiberEquiv {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : αγ} {g : βγ} (e : (c : γ) → { a : α // f a = c } { b : β // g b = c }) :
                α β

                A family of equivalences between fibers gives an equivalence between domains.

                Equations
                Instances For
                  @[simp]
                  theorem Equiv.ofFiberEquiv_apply {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : αγ} {g : βγ} (e : (c : γ) → { a : α // f a = c } { b : β // g b = c }) (a✝ : α) :
                  (ofFiberEquiv e) a✝ = ((e (f a✝)) ((sigmaFiberEquiv f).symm a✝).snd)
                  @[simp]
                  theorem Equiv.ofFiberEquiv_symm_apply {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : αγ} {g : βγ} (e : (c : γ) → { a : α // f a = c } { b : β // g b = c }) (a✝ : β) :
                  theorem Equiv.ofFiberEquiv_map {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : αγ} {g : βγ} (e : (c : γ) → { a : α // f a = c } { b : β // g b = c }) (a : α) :
                  g ((ofFiberEquiv e) a) = f a
                  def Equiv.sigmaNatSucc (f : Type u) :
                  (n : ) × f n f 0 (n : ) × f (n + 1)

                  An equivalence that separates out the 0th fiber of (Σ (n : ℕ), f n).

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

                    The set of natural numbers is equivalent to ℕ ⊕ PUnit.

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

                      The type of integer numbers is equivalent to ℕ ⊕ ℕ.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        def Equiv.uniqueCongr {α : Sort u_1} {β : Sort u_4} (e : α β) :

                        If α is equivalent to β, then Unique α is equivalent to Unique β.

                        Equations
                        Instances For
                          theorem Equiv.isEmpty_congr {α : Sort u_1} {β : Sort u_4} (e : α β) :

                          If α is equivalent to β, then IsEmpty α is equivalent to IsEmpty β.

                          theorem Equiv.isEmpty {α : Sort u_1} {β : Sort u_4} (e : α β) [IsEmpty β] :
                          def Equiv.subtypeEquiv {α : Sort u_1} {β : Sort u_4} {p : αProp} {q : βProp} (e : α β) (h : ∀ (a : α), p a q (e a)) :
                          { a : α // p a } { b : β // q b }

                          If α is equivalent to β and the predicates p : α → Prop and q : β → Prop are equivalent at corresponding points, then {a // p a} is equivalent to {b // q b}. For the statement where α = β, that is, e : perm α, see Perm.subtypePerm.

                          Equations
                          • e.subtypeEquiv h = { toFun := fun (a : { a : α // p a }) => e a, , invFun := fun (b : { b : β // q b }) => e.symm b, , left_inv := , right_inv := }
                          Instances For
                            @[simp]
                            theorem Equiv.subtypeEquiv_apply {α : Sort u_1} {β : Sort u_4} {p : αProp} {q : βProp} (e : α β) (h : ∀ (a : α), p a q (e a)) (a : { a : α // p a }) :
                            (e.subtypeEquiv h) a = e a,
                            theorem Equiv.coe_subtypeEquiv_eq_map {X : Sort u_9} {Y : Sort u_10} {p : XProp} {q : YProp} (e : X Y) (h : ∀ (x : X), p x q (e x)) :
                            (e.subtypeEquiv h) = Subtype.map e
                            @[simp]
                            theorem Equiv.subtypeEquiv_refl {α : Sort u_1} {p : αProp} (h : ∀ (a : α), p a p ((Equiv.refl α) a) := ) :
                            @[simp]
                            theorem Equiv.subtypeEquiv_symm {α : Sort u_1} {β : Sort u_4} {p : αProp} {q : βProp} (e : α β) (h : ∀ (a : α), p a q (e a)) :
                            @[simp]
                            theorem Equiv.subtypeEquiv_trans {α : Sort u_1} {β : Sort u_4} {γ : Sort u_7} {p : αProp} {q : βProp} {r : γProp} (e : α β) (f : β γ) (h : ∀ (a : α), p a q (e a)) (h' : ∀ (b : β), q b r (f b)) :
                            def Equiv.subtypeEquivRight {α : Sort u_1} {p q : αProp} (e : ∀ (x : α), p x q x) :
                            { x : α // p x } { x : α // q x }

                            If two predicates p and q are pointwise equivalent, then {x // p x} is equivalent to {x // q x}.

                            Equations
                            Instances For
                              @[simp]
                              theorem Equiv.subtypeEquivRight_symm_apply_coe {α : Sort u_1} {p q : αProp} (e : ∀ (x : α), p x q x) (b : { b : α // q b }) :
                              ((subtypeEquivRight e).symm b) = b
                              @[simp]
                              theorem Equiv.subtypeEquivRight_apply_coe {α : Sort u_1} {p q : αProp} (e : ∀ (x : α), p x q x) (a : { a : α // p a }) :
                              ((subtypeEquivRight e) a) = a
                              theorem Equiv.subtypeEquivRight_apply {α : Sort u_1} {p q : αProp} (e : ∀ (x : α), p x q x) (z : { x : α // p x }) :
                              (subtypeEquivRight e) z = z,
                              theorem Equiv.subtypeEquivRight_symm_apply {α : Sort u_1} {p q : αProp} (e : ∀ (x : α), p x q x) (z : { x : α // q x }) :
                              (subtypeEquivRight e).symm z = z,
                              def Equiv.subtypeEquivOfSubtype {α : Sort u_1} {β : Sort u_4} {p : βProp} (e : α β) :
                              { a : α // p (e a) } { b : β // p b }

                              If α ≃ β, then for any predicate p : β → Prop the subtype {a // p (e a)} is equivalent to the subtype {b // p b}.

                              Equations
                              Instances For
                                def Equiv.subtypeEquivOfSubtype' {α : Sort u_1} {β : Sort u_4} {p : αProp} (e : α β) :
                                { a : α // p a } { b : β // p (e.symm b) }

                                If α ≃ β, then for any predicate p : α → Prop the subtype {a // p a} is equivalent to the subtype {b // p (e.symm b)}. This version is used by equiv_rw.

                                Equations
                                Instances For
                                  def Equiv.subtypeEquivProp {α : Sort u_1} {p q : αProp} (h : p = q) :

                                  If two predicates are equal, then the corresponding subtypes are equivalent.

                                  Equations
                                  Instances For
                                    def Equiv.subtypeSubtypeEquivSubtypeExists {α : Sort u_1} (p : αProp) (q : Subtype pProp) :
                                    Subtype q { a : α // (h : p a), q a, h }

                                    A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates. This version allows the “inner” predicate to depend on h : p a.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem Equiv.subtypeSubtypeEquivSubtypeExists_symm_apply_coe_coe {α : Sort u_1} (p : αProp) (q : Subtype pProp) (a : { a : α // (h : p a), q a, h }) :
                                      @[simp]
                                      theorem Equiv.subtypeSubtypeEquivSubtypeExists_apply_coe {α : Sort u_1} (p : αProp) (q : Subtype pProp) (a : Subtype q) :
                                      ((subtypeSubtypeEquivSubtypeExists p q) a) = a
                                      def Equiv.subtypeSubtypeEquivSubtypeInter {α : Type u} (p q : αProp) :
                                      { x : Subtype p // q x } { x : α // p x q x }

                                      A subtype of a subtype is equivalent to the subtype of elements satisfying both predicates.

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem Equiv.subtypeSubtypeEquivSubtypeInter_symm_apply_coe_coe {α : Type u} (p q : αProp) (a✝ : { x : α // p x q x }) :
                                        ((subtypeSubtypeEquivSubtypeInter p q).symm a✝) = a✝
                                        @[simp]
                                        theorem Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe {α : Type u} (p q : αProp) (a✝ : { x : Subtype p // q x }) :
                                        ((subtypeSubtypeEquivSubtypeInter p q) a✝) = a✝
                                        def Equiv.subtypeSubtypeEquivSubtype {α : Type u_9} {p q : αProp} (h : ∀ {x : α}, q xp x) :
                                        { x : Subtype p // q x } Subtype q

                                        If the outer subtype has more restrictive predicate than the inner one, then we can drop the latter.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem Equiv.subtypeSubtypeEquivSubtype_apply_coe {α : Type u_9} {p q : αProp} (h : ∀ {x : α}, q xp x) (a✝ : { x : Subtype p // q x }) :
                                          ((subtypeSubtypeEquivSubtype h) a✝) = a✝
                                          @[simp]
                                          theorem Equiv.subtypeSubtypeEquivSubtype_symm_apply_coe_coe {α : Type u_9} {p q : αProp} (h : ∀ {x : α}, q xp x) (a✝ : Subtype q) :
                                          ((subtypeSubtypeEquivSubtype h).symm a✝) = a✝
                                          def Equiv.subtypeUnivEquiv {α : Type u_9} {p : αProp} (h : ∀ (x : α), p x) :

                                          If a proposition holds for all elements, then the subtype is equivalent to the original type.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem Equiv.subtypeUnivEquiv_apply {α : Type u_9} {p : αProp} (h : ∀ (x : α), p x) (x : Subtype p) :
                                            (subtypeUnivEquiv h) x = x
                                            @[simp]
                                            theorem Equiv.subtypeUnivEquiv_symm_apply {α : Type u_9} {p : αProp} (h : ∀ (x : α), p x) (x : α) :
                                            (subtypeUnivEquiv h).symm x = x,
                                            def Equiv.subtypeSigmaEquiv {α : Type u_9} (p : αType v) (q : αProp) :
                                            { y : Sigma p // q y.fst } (x : Subtype q) × p x

                                            A subtype of a sigma-type is a sigma-type over a subtype.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              def Equiv.sigmaSubtypeEquivOfSubset {α : Type u_9} (p : αType v) (q : αProp) (h : ∀ (x : α), p xq x) :
                                              (x : Subtype q) × p x (x : α) × p x

                                              A sigma type over a subtype is equivalent to the sigma set over the original type, if the fiber is empty outside of the subset

                                              Equations
                                              Instances For
                                                def Equiv.sigmaSubtypeFiberEquiv {α : Type u_9} {β : Type u_10} (f : αβ) (p : βProp) (h : ∀ (x : α), p (f x)) :
                                                (y : Subtype p) × { x : α // f x = y } α

                                                If a predicate p : β → Prop is true on the range of a map f : α → β, then Σ y : {y // p y}, {x // f x = y} is equivalent to α.

                                                Equations
                                                Instances For
                                                  def Equiv.sigmaSubtypeFiberEquivSubtype {α : Type u_9} {β : Type u_10} (f : αβ) {p : αProp} {q : βProp} (h : ∀ (x : α), p x q (f x)) :
                                                  (y : Subtype q) × { x : α // f x = y } Subtype p

                                                  If for each x we have p x ↔ q (f x), then Σ y : {y // q y}, f ⁻¹' {y} is equivalent to {x // p x}.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    def Equiv.sigmaOptionEquivOfSome {α : Type u_9} (p : Option αType v) (h : p noneFalse) :
                                                    (x : Option α) × p x (x : α) × p (some x)

                                                    A sigma type over an Option is equivalent to the sigma set over the original type, if the fiber is empty at none.

                                                    Equations
                                                    Instances For
                                                      def Equiv.piEquivSubtypeSigma (ι : Type u_10) (π : ιType u_9) :
                                                      ((i : ι) → π i) { f : ι(i : ι) × π i // ∀ (i : ι), (f i).fst = i }

                                                      The Pi-type ∀ i, π i is equivalent to the type of sections f : ι → Σ i, π i of the Sigma type such that for all i we have (f i).fst = i.

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        def Equiv.subtypePiEquivPi {α : Sort u_1} {β : αSort v} {p : (a : α) → β aProp} :
                                                        { f : (a : α) → β a // ∀ (a : α), p a (f a) } ((a : α) → { b : β a // p a b })

                                                        The type of functions f : ∀ a, β a such that for all a we have p a (f a) is equivalent to the type of functions ∀ a, {b : β a // p a b}.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          def Equiv.subtypeEquivCodomain {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' x }Y) :
                                                          { g : XY // g Subtype.val = f } Y

                                                          The type of all functions X → Y with prescribed values for all x' ≠ x is equivalent to the codomain Y.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem Equiv.coe_subtypeEquivCodomain {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' x }Y) :
                                                            (subtypeEquivCodomain f) = fun (g : { g : XY // g Subtype.val = f }) => g x
                                                            @[simp]
                                                            theorem Equiv.subtypeEquivCodomain_apply {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' x }Y) (g : { g : XY // g Subtype.val = f }) :
                                                            (subtypeEquivCodomain f) g = g x
                                                            theorem Equiv.coe_subtypeEquivCodomain_symm {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' x }Y) :
                                                            (subtypeEquivCodomain f).symm = fun (y : Y) => fun (x' : X) => if h : x' x then f x', h else y,
                                                            @[simp]
                                                            theorem Equiv.subtypeEquivCodomain_symm_apply {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' x }Y) (y : Y) (x' : X) :
                                                            ((subtypeEquivCodomain f).symm y) x' = if h : x' x then f x', h else y
                                                            theorem Equiv.subtypeEquivCodomain_symm_apply_eq {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' x }Y) (y : Y) :
                                                            ((subtypeEquivCodomain f).symm y) x = y
                                                            theorem Equiv.subtypeEquivCodomain_symm_apply_ne {X : Sort u_9} {Y : Sort u_10} [DecidableEq X] {x : X} (f : { x' : X // x' x }Y) (y : Y) (x' : X) (h : x' x) :
                                                            ((subtypeEquivCodomain f).symm y) x' = f x', h
                                                            def Equiv.Perm.extendDomain {α' : Type u_9} {β' : Type u_10} (e : Perm α') {p : β'Prop} [DecidablePred p] (f : α' Subtype p) :
                                                            Perm β'

                                                            Extend the domain of e : Equiv.Perm α to one that is over β via f : α → Subtype p, where p : β → Prop, permuting only the b : β that satisfy p b. This can be used to extend the domain across a function f : α → β, keeping everything outside of Set.range f fixed. For this use-case Equiv given by f can be constructed by Equiv.of_leftInverse' or Equiv.of_leftInverse when there is a known inverse, or Equiv.ofInjective in the general case.

                                                            Equations
                                                            Instances For
                                                              @[simp]
                                                              theorem Equiv.Perm.extendDomain_apply_image {α' : Type u_9} {β' : Type u_10} (e : Perm α') {p : β'Prop} [DecidablePred p] (f : α' Subtype p) (a : α') :
                                                              (e.extendDomain f) (f a) = (f (e a))
                                                              theorem Equiv.Perm.extendDomain_apply_subtype {α' : Type u_9} {β' : Type u_10} (e : Perm α') {p : β'Prop} [DecidablePred p] (f : α' Subtype p) {b : β'} (h : p b) :
                                                              (e.extendDomain f) b = (f (e (f.symm b, h)))
                                                              theorem Equiv.Perm.extendDomain_apply_not_subtype {α' : Type u_9} {β' : Type u_10} (e : Perm α') {p : β'Prop} [DecidablePred p] (f : α' Subtype p) {b : β'} (h : ¬p b) :
                                                              (e.extendDomain f) b = b
                                                              @[simp]
                                                              theorem Equiv.Perm.extendDomain_refl {α' : Type u_9} {β' : Type u_10} {p : β'Prop} [DecidablePred p] (f : α' Subtype p) :
                                                              @[simp]
                                                              theorem Equiv.Perm.extendDomain_symm {α' : Type u_9} {β' : Type u_10} (e : Perm α') {p : β'Prop} [DecidablePred p] (f : α' Subtype p) :
                                                              theorem Equiv.Perm.extendDomain_trans {α' : Type u_9} {β' : Type u_10} {p : β'Prop} [DecidablePred p] (f : α' Subtype p) (e e' : Perm α') :
                                                              def Equiv.subtypeQuotientEquivQuotientSubtype {α : Sort u_1} (p₁ : αProp) {s₁ : Setoid α} {s₂ : Setoid (Subtype p₁)} (p₂ : Quotient s₁Prop) (hp₂ : ∀ (a : α), p₁ a p₂ a) (h : ∀ (x y : Subtype p₁), s₂ x y s₁ x y) :
                                                              { x : Quotient s₁ // p₂ x } Quotient s₂

                                                              Subtype of the quotient is equivalent to the quotient of the subtype. Let α be a setoid with equivalence relation ~. Let p₂ be a predicate on the quotient type α/~, and p₁ be the lift of this predicate to α: p₁ a ↔ p₂ ⟦a⟧. Let ~₂ be the restriction of ~ to {x // p₁ x}. Then {x // p₂ x} is equivalent to the quotient of {x // p₁ x} by ~₂.

                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                @[simp]
                                                                theorem Equiv.subtypeQuotientEquivQuotientSubtype_mk {α : Sort u_1} (p₁ : αProp) [s₁ : Setoid α] [s₂ : Setoid (Subtype p₁)] (p₂ : Quotient s₁Prop) (hp₂ : ∀ (a : α), p₁ a p₂ a) (h : ∀ (x y : Subtype p₁), s₂ x y x y) (x : α) (hx : p₂ x) :
                                                                (subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h) x, hx = x,
                                                                @[simp]
                                                                theorem Equiv.subtypeQuotientEquivQuotientSubtype_symm_mk {α : Sort u_1} (p₁ : αProp) [s₁ : Setoid α] [s₂ : Setoid (Subtype p₁)] (p₂ : Quotient s₁Prop) (hp₂ : ∀ (a : α), p₁ a p₂ a) (h : ∀ (x y : Subtype p₁), s₂ x y x y) (x : Subtype p₁) :
                                                                (subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h).symm x = x,
                                                                def Equiv.swapCore {α : Sort u_1} [DecidableEq α] (a b r : α) :
                                                                α

                                                                A helper function for Equiv.swap.

                                                                Equations
                                                                Instances For
                                                                  theorem Equiv.swapCore_self {α : Sort u_1} [DecidableEq α] (r a : α) :
                                                                  swapCore a a r = r
                                                                  theorem Equiv.swapCore_swapCore {α : Sort u_1} [DecidableEq α] (r a b : α) :
                                                                  swapCore a b (swapCore a b r) = r
                                                                  theorem Equiv.swapCore_comm {α : Sort u_1} [DecidableEq α] (r a b : α) :
                                                                  swapCore a b r = swapCore b a r
                                                                  def Equiv.swap {α : Sort u_1} [DecidableEq α] (a b : α) :
                                                                  Perm α

                                                                  swap a b is the permutation that swaps a and b and leaves other values as is.

                                                                  Equations
                                                                  Instances For
                                                                    @[simp]
                                                                    theorem Equiv.swap_self {α : Sort u_1} [DecidableEq α] (a : α) :
                                                                    theorem Equiv.swap_comm {α : Sort u_1} [DecidableEq α] (a b : α) :
                                                                    swap a b = swap b a
                                                                    theorem Equiv.swap_apply_def {α : Sort u_1} [DecidableEq α] (a b x : α) :
                                                                    (swap a b) x = if x = a then b else if x = b then a else x
                                                                    @[simp]
                                                                    theorem Equiv.swap_apply_left {α : Sort u_1} [DecidableEq α] (a b : α) :
                                                                    (swap a b) a = b
                                                                    @[simp]
                                                                    theorem Equiv.swap_apply_right {α : Sort u_1} [DecidableEq α] (a b : α) :
                                                                    (swap a b) b = a
                                                                    theorem Equiv.swap_apply_of_ne_of_ne {α : Sort u_1} [DecidableEq α] {a b x : α} :
                                                                    x ax b(swap a b) x = x
                                                                    theorem Equiv.eq_or_eq_of_swap_apply_ne_self {α : Sort u_1} [DecidableEq α] {a b x : α} (h : (swap a b) x x) :
                                                                    x = a x = b
                                                                    @[simp]
                                                                    theorem Equiv.swap_swap {α : Sort u_1} [DecidableEq α] (a b : α) :
                                                                    @[simp]
                                                                    theorem Equiv.symm_swap {α : Sort u_1} [DecidableEq α] (a b : α) :
                                                                    Equiv.symm (swap a b) = swap a b
                                                                    @[simp]
                                                                    theorem Equiv.swap_eq_refl_iff {α : Sort u_1} [DecidableEq α] {x y : α} :
                                                                    swap x y = Equiv.refl α x = y
                                                                    theorem Equiv.swap_comp_apply {α : Sort u_1} [DecidableEq α] {a b x : α} (π : Perm α) :
                                                                    (Equiv.trans π (swap a b)) x = if π x = a then b else if π x = b then a else π x
                                                                    theorem Equiv.swap_eq_update {α : Sort u_1} [DecidableEq α] (i j : α) :
                                                                    theorem Equiv.comp_swap_eq_update {α : Sort u_1} {β : Sort u_4} [DecidableEq α] (i j : α) (f : αβ) :
                                                                    f (swap i j) = Function.update (Function.update f j (f i)) i (f j)
                                                                    @[simp]
                                                                    theorem Equiv.symm_trans_swap_trans {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] (a b : α) (e : α β) :
                                                                    (e.symm.trans (swap a b)).trans e = swap (e a) (e b)
                                                                    @[simp]
                                                                    theorem Equiv.trans_swap_trans_symm {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] (a b : β) (e : α β) :
                                                                    (e.trans (swap a b)).trans e.symm = swap (e.symm a) (e.symm b)
                                                                    @[simp]
                                                                    theorem Equiv.swap_apply_self {α : Sort u_1} [DecidableEq α] (i j a : α) :
                                                                    (swap i j) ((swap i j) a) = a
                                                                    theorem Equiv.apply_swap_eq_self {α : Sort u_1} {β : Sort u_4} [DecidableEq α] {v : αβ} {i j : α} (hv : v i = v j) (k : α) :
                                                                    v ((swap i j) k) = v k

                                                                    A function is invariant to a swap if it is equal at both elements

                                                                    theorem Equiv.swap_apply_eq_iff {α : Sort u_1} [DecidableEq α] {x y z w : α} :
                                                                    (swap x y) z = w z = (swap x y) w
                                                                    theorem Equiv.swap_apply_ne_self_iff {α : Sort u_1} [DecidableEq α] {a b x : α} :
                                                                    (swap a b) x x a b (x = a x = b)
                                                                    @[simp]
                                                                    theorem Equiv.Perm.sumCongr_swap_refl {α : Type u_9} {β : Type u_10} [DecidableEq α] [DecidableEq β] (i j : α) :
                                                                    @[simp]
                                                                    theorem Equiv.Perm.sumCongr_refl_swap {α : Type u_9} {β : Type u_10} [DecidableEq α] [DecidableEq β] (i j : β) :
                                                                    def Equiv.setValue {α : Sort u_1} {β : Sort u_4} [DecidableEq α] (f : α β) (a : α) (b : β) :
                                                                    α β

                                                                    Augment an equivalence with a prescribed mapping f a = b

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem Equiv.setValue_eq {α : Sort u_1} {β : Sort u_4} [DecidableEq α] (f : α β) (a : α) (b : β) :
                                                                      (f.setValue a b) a = b
                                                                      def Function.Involutive.toPerm {α : Sort u_1} (f : αα) (h : Involutive f) :

                                                                      Convert an involutive function f to a permutation with toFun = invFun = f.

                                                                      Equations
                                                                      Instances For
                                                                        @[simp]
                                                                        theorem Function.Involutive.coe_toPerm {α : Sort u_1} {f : αα} (h : Involutive f) :
                                                                        (toPerm f h) = f
                                                                        @[simp]
                                                                        theorem Function.Involutive.toPerm_symm {α : Sort u_1} {f : αα} (h : Involutive f) :
                                                                        theorem Function.Involutive.toPerm_involutive {α : Sort u_1} {f : αα} (h : Involutive f) :
                                                                        theorem PLift.eq_up_iff_down_eq {α : Sort u_1} {x : PLift α} {y : α} :
                                                                        x = { down := y } x.down = y
                                                                        theorem Function.Injective.map_swap {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] {f : αβ} (hf : Injective f) (x y z : α) :
                                                                        f ((Equiv.swap x y) z) = (Equiv.swap (f x) (f y)) (f z)
                                                                        def Equiv.piCongrLeft' {α : Sort u_1} {β : Sort u_4} (P : αSort u_9) (e : α β) :
                                                                        ((a : α) → P a) ((b : β) → P (e.symm b))

                                                                        Transport dependent functions through an equivalence of the base space.

                                                                        Equations
                                                                        • Equiv.piCongrLeft' P e = { toFun := fun (f : (a : α) → P a) (x : β) => f (e.symm x), invFun := fun (f : (b : β) → P (e.symm b)) (x : α) => f (e x), left_inv := , right_inv := }
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem Equiv.piCongrLeft'_apply {α : Sort u_1} {β : Sort u_4} (P : αSort u_9) (e : α β) (f : (a : α) → P a) (x : β) :
                                                                          (piCongrLeft' P e) f x = f (e.symm x)
                                                                          theorem Equiv.piCongrLeft'_symm_apply {α : Sort u_1} {β : Sort u_4} (P : αSort u_9) (e : α β) (f : (b : β) → P (e.symm b)) (x : α) :
                                                                          (piCongrLeft' P e).symm f x = f (e x)

                                                                          Note: the "obvious" statement (piCongrLeft' P e).symm g a = g (e a) doesn't typecheck: the LHS would have type P a while the RHS would have type P (e.symm (e a)). For that reason, we have to explicitly substitute along e.symm (e a) = a in the statement of this lemma.

                                                                          @[simp]
                                                                          theorem Equiv.piCongrLeft'_symm {α : Sort u_1} {β : Sort u_4} (P : Sort u_9) (e : α β) :
                                                                          (piCongrLeft' (fun (x : α) => P) e).symm = piCongrLeft' (fun (a : β) => P) e.symm

                                                                          This lemma is impractical to state in the dependent case.

                                                                          @[simp]
                                                                          theorem Equiv.piCongrLeft'_symm_apply_apply {α : Sort u_1} {β : Sort u_4} (P : αSort u_9) (e : α β) (g : (b : β) → P (e.symm b)) (b : β) :
                                                                          (piCongrLeft' P e).symm g (e.symm b) = g b

                                                                          Note: the "obvious" statement (piCongrLeft' P e).symm g a = g (e a) doesn't typecheck: the LHS would have type P a while the RHS would have type P (e.symm (e a)). This lemma is a way around it in the case where a is of the form e.symm b, so we can use g b instead of g (e (e.symm b)).

                                                                          def Equiv.piCongrLeft {α : Sort u_1} {β : Sort u_4} (P : βSort w) (e : α β) :
                                                                          ((a : α) → P (e a)) ((b : β) → P b)

                                                                          Transporting dependent functions through an equivalence of the base, expressed as a "simplification".

                                                                          Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem Equiv.piCongrLeft_apply {α : Sort u_1} {β : Sort u_4} (P : βSort w) (e : α β) (f : (a : α) → P (e a)) (b : β) :
                                                                            (piCongrLeft P e) f b = f (e.symm b)

                                                                            Note: the "obvious" statement (piCongrLeft P e) f b = f (e.symm b) doesn't typecheck: the LHS would have type P b while the RHS would have type P (e (e.symm b)). For that reason, we have to explicitly substitute along e (e.symm b) = b in the statement of this lemma.

                                                                            @[simp]
                                                                            theorem Equiv.piCongrLeft_symm_apply {α : Sort u_1} {β : Sort u_4} (P : βSort w) (e : α β) (g : (b : β) → P b) (a : α) :
                                                                            (piCongrLeft P e).symm g a = g (e a)
                                                                            theorem Equiv.piCongrLeft_apply_apply {α : Sort u_1} {β : Sort u_4} (P : βSort w) (e : α β) (f : (a : α) → P (e a)) (a : α) :
                                                                            (piCongrLeft P e) f (e a) = f a

                                                                            Note: the "obvious" statement (piCongrLeft P e) f b = f (e.symm b) doesn't typecheck: the LHS would have type P b while the RHS would have type P (e (e.symm b)). This lemma is a way around it in the case where b is of the form e a, so we can use f a instead of f (e.symm (e a)).

                                                                            theorem Equiv.piCongrLeft_apply_eq_cast {α : Sort u_1} {β : Sort u_4} {P : βSort v} {e : α β} (f : (a : α) → P (e a)) (b : β) :
                                                                            (piCongrLeft P e) f b = cast (f (e.symm b))
                                                                            theorem Equiv.piCongrLeft_sumInl {ι : Type u_10} {ι' : Type u_11} {ι'' : Sort u_12} (π : ι''Type u_9) (e : ι ι' ι'') (f : (i : ι) → π (e (Sum.inl i))) (g : (i : ι') → π (e (Sum.inr i))) (i : ι) :
                                                                            (piCongrLeft π e) ((sumPiEquivProdPi fun (x : ι ι') => π (e x)).symm (f, g)) (e (Sum.inl i)) = f i
                                                                            theorem Equiv.piCongrLeft_sumInr {ι : Type u_10} {ι' : Type u_11} {ι'' : Sort u_12} (π : ι''Type u_9) (e : ι ι' ι'') (f : (i : ι) → π (e (Sum.inl i))) (g : (i : ι') → π (e (Sum.inr i))) (j : ι') :
                                                                            (piCongrLeft π e) ((sumPiEquivProdPi fun (x : ι ι') => π (e x)).symm (f, g)) (e (Sum.inr j)) = g j
                                                                            @[deprecated Equiv.piCongrLeft_sumInl (since := "2025-02-21")]
                                                                            theorem Equiv.piCongrLeft_sum_inl {ι : Type u_10} {ι' : Type u_11} {ι'' : Sort u_12} (π : ι''Type u_9) (e : ι ι' ι'') (f : (i : ι) → π (e (Sum.inl i))) (g : (i : ι') → π (e (Sum.inr i))) (i : ι) :
                                                                            (piCongrLeft π e) ((sumPiEquivProdPi fun (x : ι ι') => π (e x)).symm (f, g)) (e (Sum.inl i)) = f i

                                                                            Alias of Equiv.piCongrLeft_sumInl.

                                                                            @[deprecated Equiv.piCongrLeft_sumInr (since := "2025-02-21")]
                                                                            theorem Equiv.piCongrLeft_sum_inr {ι : Type u_10} {ι' : Type u_11} {ι'' : Sort u_12} (π : ι''Type u_9) (e : ι ι' ι'') (f : (i : ι) → π (e (Sum.inl i))) (g : (i : ι') → π (e (Sum.inr i))) (j : ι') :
                                                                            (piCongrLeft π e) ((sumPiEquivProdPi fun (x : ι ι') => π (e x)).symm (f, g)) (e (Sum.inr j)) = g j

                                                                            Alias of Equiv.piCongrLeft_sumInr.

                                                                            def Equiv.piCongr {α : Sort u_1} {β : Sort u_4} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (a : α) → W a Z (h₁ a)) :
                                                                            ((a : α) → W a) ((b : β) → Z b)

                                                                            Transport dependent functions through an equivalence of the base spaces and a family of equivalences of the matching fibers.

                                                                            Equations
                                                                            Instances For
                                                                              @[simp]
                                                                              theorem Equiv.coe_piCongr_symm {α : Sort u_1} {β : Sort u_4} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (a : α) → W a Z (h₁ a)) :
                                                                              (h₁.piCongr h₂).symm = fun (f : (b : β) → Z b) (a : α) => (h₂ a).symm (f (h₁ a))
                                                                              theorem Equiv.piCongr_symm_apply {α : Sort u_1} {β : Sort u_4} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (a : α) → W a Z (h₁ a)) (f : (b : β) → Z b) :
                                                                              (h₁.piCongr h₂).symm f = fun (a : α) => (h₂ a).symm (f (h₁ a))
                                                                              @[simp]
                                                                              theorem Equiv.piCongr_apply_apply {α : Sort u_1} {β : Sort u_4} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (a : α) → W a Z (h₁ a)) (f : (a : α) → W a) (a : α) :
                                                                              (h₁.piCongr h₂) f (h₁ a) = (h₂ a) (f a)
                                                                              def Equiv.piCongr' {α : Sort u_1} {β : Sort u_4} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (b : β) → W (h₁.symm b) Z b) :
                                                                              ((a : α) → W a) ((b : β) → Z b)

                                                                              Transport dependent functions through an equivalence of the base spaces and a family of equivalences of the matching fibres.

                                                                              Equations
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem Equiv.coe_piCongr' {α : Sort u_1} {β : Sort u_4} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (b : β) → W (h₁.symm b) Z b) :
                                                                                (h₁.piCongr' h₂) = fun (f : (a : α) → W a) (b : β) => (h₂ b) (f (h₁.symm b))
                                                                                theorem Equiv.piCongr'_apply {α : Sort u_1} {β : Sort u_4} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (b : β) → W (h₁.symm b) Z b) (f : (a : α) → W a) :
                                                                                (h₁.piCongr' h₂) f = fun (b : β) => (h₂ b) (f (h₁.symm b))
                                                                                @[simp]
                                                                                theorem Equiv.piCongr'_symm_apply_symm_apply {α : Sort u_1} {β : Sort u_4} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (b : β) → W (h₁.symm b) Z b) (f : (b : β) → Z b) (b : β) :
                                                                                (h₁.piCongr' h₂).symm f (h₁.symm b) = (h₂ b).symm (f b)
                                                                                def Equiv.piCongrSet {α : Type u_9} {W : αSort w} {s t : Set α} (h : s = t) :
                                                                                ((i : { i : α // i s }) → W i) ((i : { i : α // i t }) → W i)

                                                                                Transport dependent functions through an equality of sets.

                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For
                                                                                  @[simp]
                                                                                  theorem Equiv.piCongrSet_apply {α : Type u_9} {W : αSort w} {s t : Set α} (h : s = t) (f : (i : { i : α // i s }) → W i) (i : { i : α // i t }) :
                                                                                  (piCongrSet h) f i = f i,
                                                                                  @[simp]
                                                                                  theorem Equiv.piCongrSet_symm_apply {α : Type u_9} {W : αSort w} {s t : Set α} (h : s = t) (f : (i : { i : α // i t }) → W i) (i : { i : α // i s }) :
                                                                                  (piCongrSet h).symm f i = f i,
                                                                                  theorem Equiv.semiconj_conj {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ β₁) (f : α₁α₁) :
                                                                                  Function.Semiconj (⇑e) f (e.conj f)
                                                                                  theorem Equiv.semiconj₂_conj {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ β₁) (f : α₁α₁α₁) :
                                                                                  instance Equiv.instAssociativeCoeForallForallArrowCongr {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ β₁) (f : α₁α₁α₁) [Std.Associative f] :
                                                                                  instance Equiv.instIdempotentOpCoeForallForallArrowCongr {α₁ : Type u_9} {β₁ : Type u_10} (e : α₁ β₁) (f : α₁α₁α₁) [Std.IdempotentOp f] :
                                                                                  @[simp]
                                                                                  theorem Equiv.ulift_symm_down {α : Type v} (x : α) :
                                                                                  theorem Function.Injective.swap_apply {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] {f : αβ} (hf : Injective f) (x y z : α) :
                                                                                  (Equiv.swap (f x) (f y)) (f z) = f ((Equiv.swap x y) z)
                                                                                  theorem Function.Injective.swap_comp {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] {f : αβ} (hf : Injective f) (x y : α) :
                                                                                  (Equiv.swap (f x) (f y)) f = f (Equiv.swap x y)
                                                                                  def equivOfSubsingletonOfSubsingleton {α : Sort u_1} {β : Sort u_4} [Subsingleton α] [Subsingleton β] (f : αβ) (g : βα) :
                                                                                  α β

                                                                                  To give an equivalence between two subsingleton types, it is sufficient to give any two functions between them.

                                                                                  Equations
                                                                                  Instances For
                                                                                    noncomputable def Equiv.punitOfNonemptyOfSubsingleton {α : Sort u_1} [h : Nonempty α] [Subsingleton α] :

                                                                                    A nonempty subsingleton type is (noncomputably) equivalent to PUnit.

                                                                                    Equations
                                                                                    Instances For
                                                                                      def uniqueUniqueEquiv {α : Sort u_1} :

                                                                                      Unique (Unique α) is equivalent to Unique α.

                                                                                      Equations
                                                                                      Instances For
                                                                                        def uniqueEquivEquivUnique (α : Sort u) (β : Sort v) [Unique β] :
                                                                                        Unique α (α β)

                                                                                        If Unique β, then Unique α is equivalent to α ≃ β.

                                                                                        Equations
                                                                                        Instances For
                                                                                          theorem Function.update_comp_equiv {α : Sort u_1} {β : Sort u_4} {α' : Sort u_9} [DecidableEq α'] [DecidableEq α] (f : αβ) (g : α' α) (a : α) (v : β) :
                                                                                          update f a v g = update (f g) (g.symm a) v
                                                                                          theorem Function.update_apply_equiv_apply {α : Sort u_1} {β : Sort u_4} {α' : Sort u_9} [DecidableEq α'] [DecidableEq α] (f : αβ) (g : α' α) (a : α) (v : β) (a' : α') :
                                                                                          update f a v (g a') = update (f g) (g.symm a) v a'
                                                                                          theorem Function.piCongrLeft'_update {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] (P : αSort u_10) (e : α β) (f : (a : α) → P a) (b : β) (x : P (e.symm b)) :
                                                                                          (Equiv.piCongrLeft' P e) (update f (e.symm b) x) = update ((Equiv.piCongrLeft' P e) f) b x
                                                                                          theorem Function.piCongrLeft'_symm_update {α : Sort u_1} {β : Sort u_4} [DecidableEq α] [DecidableEq β] (P : αSort u_10) (e : α β) (f : (b : β) → P (e.symm b)) (b : β) (x : P (e.symm b)) :