Documentation

Mathlib.Logic.Equiv.Basic

Equivalence between types #

In this file we continue the work on equivalences begun in Logic/Equiv/Defs.lean, defining

Tags #

equivalence, congruence, bijective map

@[simp]
theorem Equiv.pprodEquivProd_apply {α : Type u_1} {β : Type u_2} (x : PProd α β) :
Equiv.pprodEquivProd x = (x.fst, x.snd)
@[simp]
theorem Equiv.pprodEquivProd_symm_apply {α : Type u_1} {β : Type u_2} (x : α × β) :
Equiv.pprodEquivProd.symm x = { fst := x.1, snd := x.2 }
def Equiv.pprodEquivProd {α : Type u_1} {β : Type u_2} :
PProd α β α × β

PProd α β is equivalent to α × β

Equations
  • Equiv.pprodEquivProd = { toFun := fun (x : PProd α β) => (x.fst, x.snd), invFun := fun (x : α × β) => { fst := x.1, snd := x.2 }, left_inv := , right_inv := }
Instances For
    @[simp]
    theorem Equiv.pprodCongr_apply {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (e₁ : α β) (e₂ : γ δ) (x : PProd α γ) :
    (Equiv.pprodCongr e₁ e₂) x = { fst := e₁ x.fst, snd := e₂ x.snd }
    def Equiv.pprodCongr {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (e₁ : α β) (e₂ : γ δ) :
    PProd α γ PProd β δ

    Product of two equivalences, in terms of PProd. If α ≃ β and γ ≃ δ, then PProd α γ ≃ PProd β δ.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem Equiv.pprodProd_apply {α₁ : Sort u_1} {α₂ : Type u_2} {β₁ : Sort u_3} {β₂ : Type u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
      ∀ (a : PProd α₁ β₁), (Equiv.pprodProd ea eb) a = (ea a.fst, eb a.snd)
      @[simp]
      theorem Equiv.pprodProd_symm_apply {α₁ : Sort u_1} {α₂ : Type u_2} {β₁ : Sort u_3} {β₂ : Type u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
      ∀ (a : α₂ × β₂), (Equiv.pprodProd ea eb).symm a = (Equiv.pprodCongr ea eb).symm { fst := a.1, snd := a.2 }
      def Equiv.pprodProd {α₁ : Sort u_1} {α₂ : Type u_2} {β₁ : Sort u_3} {β₂ : Type u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
      PProd α₁ β₁ α₂ × β₂

      Combine two equivalences using PProd in the domain and Prod in the codomain.

      Equations
      Instances For
        @[simp]
        theorem Equiv.prodPProd_apply {α₁ : Type u_1} {α₂ : Sort u_2} {β₁ : Type u_3} {β₂ : Sort u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
        ∀ (a : α₁ × β₁), (Equiv.prodPProd ea eb) a = (Equiv.pprodCongr ea.symm eb.symm).symm { fst := a.1, snd := a.2 }
        @[simp]
        theorem Equiv.prodPProd_symm_apply {α₁ : Type u_1} {α₂ : Sort u_2} {β₁ : Type u_3} {β₂ : Sort u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
        ∀ (a : PProd α₂ β₂), (Equiv.prodPProd ea eb).symm a = (ea.symm a.fst, eb.symm a.snd)
        def Equiv.prodPProd {α₁ : Type u_1} {α₂ : Sort u_2} {β₁ : Type u_3} {β₂ : Sort u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
        α₁ × β₁ PProd α₂ β₂

        Combine two equivalences using PProd in the codomain and Prod in the domain.

        Equations
        Instances For
          @[simp]
          theorem Equiv.pprodEquivProdPLift_symm_apply {α : Sort u_1} {β : Sort u_2} :
          ∀ (a : PLift α × PLift β), Equiv.pprodEquivProdPLift.symm a = (Equiv.pprodCongr Equiv.plift.symm Equiv.plift.symm).symm { fst := a.1, snd := a.2 }
          @[simp]
          theorem Equiv.pprodEquivProdPLift_apply {α : Sort u_1} {β : Sort u_2} :
          ∀ (a : PProd α β), Equiv.pprodEquivProdPLift a = (Equiv.plift.symm a.fst, Equiv.plift.symm a.snd)
          def Equiv.pprodEquivProdPLift {α : Sort u_1} {β : Sort u_2} :
          PProd α β PLift α × PLift β

          PProd α β is equivalent to PLift α × PLift β

          Equations
          Instances For
            @[simp]
            theorem Equiv.prodCongr_apply {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
            (Equiv.prodCongr e₁ e₂) = Prod.map e₁ e₂
            def Equiv.prodCongr {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
            α₁ × β₁ α₂ × β₂

            Product of two equivalences. If α₁ ≃ α₂ and β₁ ≃ β₂, then α₁ × β₁ ≃ α₂ × β₂. This is Prod.map as an equivalence.

            Equations
            Instances For
              @[simp]
              theorem Equiv.prodCongr_symm {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
              (Equiv.prodCongr e₁ e₂).symm = Equiv.prodCongr e₁.symm e₂.symm
              def Equiv.prodComm (α : Type u_1) (β : Type u_2) :
              α × β β × α

              Type product is commutative up to an equivalence: α × β ≃ β × α. This is Prod.swap as an equivalence.

              Equations
              • Equiv.prodComm α β = { toFun := Prod.swap, invFun := Prod.swap, left_inv := , right_inv := }
              Instances For
                @[simp]
                theorem Equiv.coe_prodComm (α : Type u_1) (β : Type u_2) :
                (Equiv.prodComm α β) = Prod.swap
                @[simp]
                theorem Equiv.prodComm_apply {α : Type u_1} {β : Type u_2} (x : α × β) :
                @[simp]
                theorem Equiv.prodComm_symm (α : Type u_1) (β : Type u_2) :
                (Equiv.prodComm α β).symm = Equiv.prodComm β α
                @[simp]
                theorem Equiv.prodAssoc_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : (α × β) × γ) :
                (Equiv.prodAssoc α β γ) p = (p.1.1, p.1.2, p.2)
                @[simp]
                theorem Equiv.prodAssoc_symm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : α × β × γ) :
                (Equiv.prodAssoc α β γ).symm p = ((p.1, p.2.1), p.2.2)
                def Equiv.prodAssoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
                (α × β) × γ α × β × γ

                Type product is associative up to an equivalence.

                Equations
                • Equiv.prodAssoc α β γ = { toFun := fun (p : (α × β) × γ) => (p.1.1, p.1.2, p.2), invFun := fun (p : α × β × γ) => ((p.1, p.2.1), p.2.2), left_inv := , right_inv := }
                Instances For
                  @[simp]
                  theorem Equiv.prodProdProdComm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (δ : Type u_4) (abcd : (α × β) × γ × δ) :
                  (Equiv.prodProdProdComm α β γ δ) abcd = ((abcd.1.1, abcd.2.1), abcd.1.2, abcd.2.2)
                  def Equiv.prodProdProdComm (α : Type u_1) (β : Type u_2) (γ : Type u_3) (δ : Type u_4) :
                  (α × β) × γ × δ (α × γ) × β × δ

                  Four-way commutativity of prod. The name matches mul_mul_mul_comm.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem Equiv.prodProdProdComm_symm (α : Type u_1) (β : Type u_2) (γ : Type u_3) (δ : Type u_4) :
                    (Equiv.prodProdProdComm α β γ δ).symm = Equiv.prodProdProdComm α γ β δ
                    @[simp]
                    theorem Equiv.curry_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
                    (Equiv.curry α β γ) = Function.curry
                    @[simp]
                    theorem Equiv.curry_symm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
                    (Equiv.curry α β γ).symm = Function.uncurry
                    def Equiv.curry (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
                    (α × βγ) (αβγ)

                    γ-valued functions on α × β are equivalent to functions α → β → γ.

                    Equations
                    • Equiv.curry α β γ = { toFun := Function.curry, invFun := Function.uncurry, left_inv := , right_inv := }
                    Instances For
                      @[simp]
                      theorem Equiv.prodPUnit_symm_apply (α : Type u_1) (a : α) :
                      (Equiv.prodPUnit α).symm a = (a, PUnit.unit)
                      @[simp]
                      theorem Equiv.prodPUnit_apply (α : Type u_1) (p : α × PUnit.{u_2 + 1} ) :
                      (Equiv.prodPUnit α) p = p.1
                      def Equiv.prodPUnit (α : Type u_1) :

                      PUnit is a right identity for type product up to an equivalence.

                      Equations
                      Instances For
                        @[simp]
                        theorem Equiv.punitProd_apply (α : Type u_1) :
                        ∀ (a : PUnit.{u_2 + 1} × α), (Equiv.punitProd α) a = a.2
                        @[simp]
                        theorem Equiv.punitProd_symm_apply (α : Type u_1) :
                        ∀ (a : α), (Equiv.punitProd α).symm a = (PUnit.unit, a)
                        def Equiv.punitProd (α : Type u_1) :

                        PUnit is a left identity for type product up to an equivalence.

                        Equations
                        Instances For
                          @[simp]
                          theorem Equiv.sigmaPUnit_apply (α : Type u_1) (p : (_ : α) × PUnit.{u_2 + 1} ) :
                          (Equiv.sigmaPUnit α) p = p.fst
                          @[simp]
                          theorem Equiv.sigmaPUnit_symm_apply_snd (α : Type u_1) (a : α) :
                          ((Equiv.sigmaPUnit α).symm a).snd = PUnit.unit
                          @[simp]
                          theorem Equiv.sigmaPUnit_symm_apply_fst (α : Type u_1) (a : α) :
                          ((Equiv.sigmaPUnit α).symm a).fst = a
                          def Equiv.sigmaPUnit (α : Type u_1) :
                          (_ : α) × PUnit.{u_2 + 1} α

                          PUnit is a right identity for dependent type product up to an equivalence.

                          Equations
                          Instances For
                            def Equiv.prodUnique (α : Type u_1) (β : Type u_2) [Unique β] :
                            α × β α

                            Any Unique type is a right identity for type product up to equivalence.

                            Equations
                            Instances For
                              @[simp]
                              theorem Equiv.coe_prodUnique {β : Type u_1} {α : Type u_2} [Unique β] :
                              (Equiv.prodUnique α β) = Prod.fst
                              theorem Equiv.prodUnique_apply {β : Type u_1} {α : Type u_2} [Unique β] (x : α × β) :
                              (Equiv.prodUnique α β) x = x.1
                              @[simp]
                              theorem Equiv.prodUnique_symm_apply {β : Type u_1} {α : Type u_2} [Unique β] (x : α) :
                              (Equiv.prodUnique α β).symm x = (x, default)
                              def Equiv.uniqueProd (α : Type u_1) (β : Type u_2) [Unique β] :
                              β × α α

                              Any Unique type is a left identity for type product up to equivalence.

                              Equations
                              Instances For
                                @[simp]
                                theorem Equiv.coe_uniqueProd {β : Type u_1} {α : Type u_2} [Unique β] :
                                (Equiv.uniqueProd α β) = Prod.snd
                                theorem Equiv.uniqueProd_apply {β : Type u_1} {α : Type u_2} [Unique β] (x : β × α) :
                                (Equiv.uniqueProd α β) x = x.2
                                @[simp]
                                theorem Equiv.uniqueProd_symm_apply {β : Type u_1} {α : Type u_2} [Unique β] (x : α) :
                                (Equiv.uniqueProd α β).symm x = (default, x)
                                def Equiv.sigmaUnique (α : Type u_2) (β : αType u_1) [(a : α) → Unique (β a)] :
                                (a : α) × β a α

                                Any family of Unique types is a right identity for dependent type product up to equivalence.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem Equiv.coe_sigmaUnique {α : Type u_2} {β : αType u_1} [(a : α) → Unique (β a)] :
                                  (Equiv.sigmaUnique α β) = Sigma.fst
                                  theorem Equiv.sigmaUnique_apply {α : Type u_2} {β : αType u_1} [(a : α) → Unique (β a)] (x : (a : α) × β a) :
                                  (Equiv.sigmaUnique α β) x = x.fst
                                  @[simp]
                                  theorem Equiv.sigmaUnique_symm_apply {α : Type u_2} {β : αType u_1} [(a : α) → Unique (β a)] (x : α) :
                                  (Equiv.sigmaUnique α β).symm x = { fst := x, snd := default }
                                  def Equiv.prodEmpty (α : Type u_1) :

                                  Empty type is a right absorbing element for type product up to an equivalence.

                                  Equations
                                  Instances For
                                    def Equiv.emptyProd (α : Type u_1) :

                                    Empty type is a left absorbing element for type product up to an equivalence.

                                    Equations
                                    Instances For

                                      PEmpty type is a right absorbing element for type product up to an equivalence.

                                      Equations
                                      Instances For

                                        PEmpty type is a left absorbing element for type product up to an equivalence.

                                        Equations
                                        Instances For
                                          def Equiv.psumEquivSum (α : Type u_1) (β : Type u_2) :
                                          α ⊕' β α β

                                          PSum is equivalent to Sum.

                                          Equations
                                          Instances For
                                            @[simp]
                                            theorem Equiv.sumCongr_apply {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
                                            ∀ (a : α₁ β₁), (Equiv.sumCongr ea eb) a = Sum.map (ea) (eb) a
                                            def Equiv.sumCongr {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
                                            α₁ β₁ α₂ β₂

                                            If α ≃ α' and β ≃ β', then α ⊕ β ≃ α' ⊕ β'. This is Sum.map as an equivalence.

                                            Equations
                                            Instances For
                                              def Equiv.psumCongr {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (e₁ : α β) (e₂ : γ δ) :
                                              α ⊕' γ β ⊕' δ

                                              If α ≃ α' and β ≃ β', then PSum α β ≃ PSum α' β'.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                def Equiv.psumSum {α₁ : Sort u_1} {α₂ : Type u_2} {β₁ : Sort u_3} {β₂ : Type u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
                                                α₁ ⊕' β₁ α₂ β₂

                                                Combine two Equivs using PSum in the domain and Sum in the codomain.

                                                Equations
                                                Instances For
                                                  def Equiv.sumPSum {α₁ : Type u_1} {α₂ : Sort u_2} {β₁ : Type u_3} {β₂ : Sort u_4} (ea : α₁ α₂) (eb : β₁ β₂) :
                                                  α₁ β₁ α₂ ⊕' β₂

                                                  Combine two Equivs using Sum in the domain and PSum in the codomain.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem Equiv.sumCongr_trans {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} (e : α₁ β₁) (f : α₂ β₂) (g : β₁ γ₁) (h : β₂ γ₂) :
                                                    (Equiv.sumCongr e f).trans (Equiv.sumCongr g h) = Equiv.sumCongr (e.trans g) (f.trans h)
                                                    @[simp]
                                                    theorem Equiv.sumCongr_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : α β) (f : γ δ) :
                                                    (Equiv.sumCongr e f).symm = Equiv.sumCongr e.symm f.symm
                                                    @[simp]
                                                    theorem Equiv.sumCongr_refl {α : Type u_1} {β : Type u_2} :
                                                    def Equiv.subtypeSum {α : Type u_1} {β : Type u_2} {p : α βProp} :
                                                    { c : α β // p c } { a : α // p (Sum.inl a) } { b : β // p (Sum.inr b) }

                                                    A subtype of a sum is equivalent to a sum of subtypes.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[reducible]
                                                      def Equiv.Perm.sumCongr {α : Type u_1} {β : Type u_2} (ea : Equiv.Perm α) (eb : Equiv.Perm β) :
                                                      Equiv.Perm (α β)

                                                      Combine a permutation of α and of β into a permutation of α ⊕ β.

                                                      Equations
                                                      Instances For
                                                        @[simp]
                                                        theorem Equiv.Perm.sumCongr_apply {α : Type u_1} {β : Type u_2} (ea : Equiv.Perm α) (eb : Equiv.Perm β) (x : α β) :
                                                        (Equiv.Perm.sumCongr ea eb) x = Sum.map (ea) (eb) x
                                                        theorem Equiv.Perm.sumCongr_trans {α : Type u_1} {β : Type u_2} (e : Equiv.Perm α) (f : Equiv.Perm β) (g : Equiv.Perm α) (h : Equiv.Perm β) :
                                                        (Equiv.Perm.sumCongr e f).trans (Equiv.Perm.sumCongr g h) = Equiv.Perm.sumCongr (e.trans g) (f.trans h)
                                                        theorem Equiv.Perm.sumCongr_symm {α : Type u_1} {β : Type u_2} (e : Equiv.Perm α) (f : Equiv.Perm β) :
                                                        (Equiv.Perm.sumCongr e f).symm = Equiv.Perm.sumCongr e.symm f.symm

                                                        Bool is equivalent the sum of two PUnits.

                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          @[simp]
                                                          theorem Equiv.sumComm_apply (α : Type u_1) (β : Type u_2) :
                                                          (Equiv.sumComm α β) = Sum.swap
                                                          def Equiv.sumComm (α : Type u_1) (β : Type u_2) :
                                                          α β β α

                                                          Sum of types is commutative up to an equivalence. This is Sum.swap as an equivalence.

                                                          Equations
                                                          • Equiv.sumComm α β = { toFun := Sum.swap, invFun := Sum.swap, left_inv := , right_inv := }
                                                          Instances For
                                                            @[simp]
                                                            theorem Equiv.sumComm_symm (α : Type u_1) (β : Type u_2) :
                                                            (Equiv.sumComm α β).symm = Equiv.sumComm β α
                                                            def Equiv.sumAssoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
                                                            (α β) γ α β γ

                                                            Sum of types is associative up to an equivalence.

                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              @[simp]
                                                              theorem Equiv.sumAssoc_apply_inl_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) :
                                                              @[simp]
                                                              theorem Equiv.sumAssoc_apply_inl_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) :
                                                              @[simp]
                                                              theorem Equiv.sumAssoc_apply_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) :
                                                              @[simp]
                                                              theorem Equiv.sumAssoc_symm_apply_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) :
                                                              (Equiv.sumAssoc α β γ).symm (Sum.inl a) = Sum.inl (Sum.inl a)
                                                              @[simp]
                                                              theorem Equiv.sumAssoc_symm_apply_inr_inl {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) :
                                                              (Equiv.sumAssoc α β γ).symm (Sum.inr (Sum.inl b)) = Sum.inl (Sum.inr b)
                                                              @[simp]
                                                              theorem Equiv.sumAssoc_symm_apply_inr_inr {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) :
                                                              (Equiv.sumAssoc α β γ).symm (Sum.inr (Sum.inr c)) = Sum.inr c
                                                              @[simp]
                                                              theorem Equiv.sumEmpty_symm_apply (α : Type u_1) (β : Type u_2) [IsEmpty β] (val : α) :
                                                              (Equiv.sumEmpty α β).symm val = Sum.inl val
                                                              def Equiv.sumEmpty (α : Type u_1) (β : Type u_2) [IsEmpty β] :
                                                              α β α

                                                              Sum with IsEmpty is equivalent to the original type.

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem Equiv.sumEmpty_apply_inl {β : Type u_1} {α : Type u_2} [IsEmpty β] (a : α) :
                                                                (Equiv.sumEmpty α β) (Sum.inl a) = a
                                                                @[simp]
                                                                theorem Equiv.emptySum_symm_apply (α : Type u_1) (β : Type u_2) [IsEmpty α] :
                                                                ∀ (a : β), (Equiv.emptySum α β).symm a = Sum.inr a
                                                                def Equiv.emptySum (α : Type u_1) (β : Type u_2) [IsEmpty α] :
                                                                α β β

                                                                The sum of IsEmpty with any type is equivalent to that type.

                                                                Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem Equiv.emptySum_apply_inr {α : Type u_1} {β : Type u_2} [IsEmpty α] (b : β) :
                                                                  (Equiv.emptySum α β) (Sum.inr b) = b

                                                                  Option α is equivalent to α ⊕ PUnit

                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    @[simp]
                                                                    @[simp]
                                                                    @[simp]
                                                                    theorem Equiv.optionEquivSumPUnit_symm_inl {α : Type u_1} (a : α) :
                                                                    @[simp]
                                                                    theorem Equiv.optionIsSomeEquiv_apply (α : Type u_1) (o : { x : Option α // Option.isSome x = true }) :
                                                                    @[simp]
                                                                    theorem Equiv.optionIsSomeEquiv_symm_apply_coe (α : Type u_1) (x : α) :
                                                                    ((Equiv.optionIsSomeEquiv α).symm x) = some x
                                                                    def Equiv.optionIsSomeEquiv (α : Type u_1) :
                                                                    { x : Option α // Option.isSome x = true } α

                                                                    The set of x : Option α such that isSome x is equivalent to α.

                                                                    Equations
                                                                    • One or more equations did not get rendered due to their size.
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem Equiv.piOptionEquivProd_symm_apply {α : Type u_2} {β : Option αType u_1} (x : β none × ((a : α) → β (some a))) (a : Option α) :
                                                                      Equiv.piOptionEquivProd.symm x a = Option.casesOn a x.1 x.2
                                                                      @[simp]
                                                                      theorem Equiv.piOptionEquivProd_apply {α : Type u_2} {β : Option αType u_1} (f : (a : Option α) → β a) :
                                                                      Equiv.piOptionEquivProd f = (f none, fun (a : α) => f (some a))
                                                                      def Equiv.piOptionEquivProd {α : Type u_2} {β : Option αType u_1} :
                                                                      ((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
                                                                        def Equiv.sumEquivSigmaBool (α : Type u) (β : Type u) :
                                                                        α β (b : Bool) × Bool.casesOn b α β

                                                                        α ⊕ β is equivalent to a Sigma-type over Bool. Note that this definition assumes α and β to be types from the same universe, so it cannot be used directly to transfer theorems about sigma types to theorems about sum types. In many cases one can use ULift to work around this difficulty.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[simp]
                                                                          theorem Equiv.sigmaFiberEquiv_symm_apply_fst {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
                                                                          ((Equiv.sigmaFiberEquiv f).symm x).fst = f x
                                                                          @[simp]
                                                                          theorem Equiv.sigmaFiberEquiv_apply {α : Type u_1} {β : Type u_2} (f : αβ) (x : (y : β) × { x : α // f x = y }) :
                                                                          (Equiv.sigmaFiberEquiv f) x = x.snd
                                                                          @[simp]
                                                                          theorem Equiv.sigmaFiberEquiv_symm_apply_snd_coe {α : Type u_1} {β : Type u_2} (f : αβ) (x : α) :
                                                                          ((Equiv.sigmaFiberEquiv f).symm x).snd = x
                                                                          def Equiv.sigmaFiberEquiv {α : Type u_1} {β : Type u_2} (f : αβ) :
                                                                          (y : β) × { x : α // f x = y } α

                                                                          sigmaFiberEquiv f for f : α → β is the natural equivalence between the type of all fibres of f and the total space α.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            def Equiv.sigmaEquivOptionOfInhabited (α : Type u) [Inhabited α] [DecidableEq α] :
                                                                            (β : Type u) × (α Option β)

                                                                            Inhabited types are equivalent to Option β for some β by identifying default with none.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              def Equiv.sumCompl {α : Type u_1} (p : αProp) [DecidablePred p] :
                                                                              { a : α // p a } { a : α // ¬p a } α

                                                                              For any predicate p on α, the sum of the two subtypes {a // p a} and its complement {a // ¬ p a} is naturally equivalent to α.

                                                                              See subtypeOrEquiv for sum types over subtypes {x // p x} and {x // q x} that are not necessarily IsCompl p q.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                @[simp]
                                                                                theorem Equiv.sumCompl_apply_inl {α : Type u_1} (p : αProp) [DecidablePred p] (x : { a : α // p a }) :
                                                                                (Equiv.sumCompl p) (Sum.inl x) = x
                                                                                @[simp]
                                                                                theorem Equiv.sumCompl_apply_inr {α : Type u_1} (p : αProp) [DecidablePred p] (x : { a : α // ¬p a }) :
                                                                                (Equiv.sumCompl p) (Sum.inr x) = x
                                                                                @[simp]
                                                                                theorem Equiv.sumCompl_apply_symm_of_pos {α : Type u_1} (p : αProp) [DecidablePred p] (a : α) (h : p a) :
                                                                                (Equiv.sumCompl p).symm a = Sum.inl { val := a, property := h }
                                                                                @[simp]
                                                                                theorem Equiv.sumCompl_apply_symm_of_neg {α : Type u_1} (p : αProp) [DecidablePred p] (a : α) (h : ¬p a) :
                                                                                (Equiv.sumCompl p).symm a = Sum.inr { val := a, property := h }
                                                                                def Equiv.subtypeCongr {α : Type u_1} {p : αProp} {q : αProp} [DecidablePred p] [DecidablePred q] (e : { x : α // p x } { x : α // q x }) (f : { x : α // ¬p x } { x : α // ¬q x }) :

                                                                                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_1} {p : εProp} [DecidablePred p] (ep : Equiv.Perm { a : ε // p a }) (en : Equiv.Perm { a : ε // ¬p a }) :

                                                                                  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_1} {p : εProp} [DecidablePred p] (ep : Equiv.Perm { a : ε // p a }) (en : Equiv.Perm { a : ε // ¬p a }) (a : ε) :
                                                                                    (Equiv.Perm.subtypeCongr ep en) a = if h : p a then (ep { val := a, property := h }) else (en { val := a, property := h })
                                                                                    @[simp]
                                                                                    theorem Equiv.Perm.subtypeCongr.left_apply {ε : Type u_1} {p : εProp} [DecidablePred p] (ep : Equiv.Perm { a : ε // p a }) (en : Equiv.Perm { a : ε // ¬p a }) {a : ε} (h : p a) :
                                                                                    (Equiv.Perm.subtypeCongr ep en) a = (ep { val := a, property := h })
                                                                                    @[simp]
                                                                                    theorem Equiv.Perm.subtypeCongr.left_apply_subtype {ε : Type u_1} {p : εProp} [DecidablePred p] (ep : Equiv.Perm { a : ε // p a }) (en : Equiv.Perm { a : ε // ¬p a }) (a : { a : ε // p a }) :
                                                                                    (Equiv.Perm.subtypeCongr ep en) a = (ep a)
                                                                                    @[simp]
                                                                                    theorem Equiv.Perm.subtypeCongr.right_apply {ε : Type u_1} {p : εProp} [DecidablePred p] (ep : Equiv.Perm { a : ε // p a }) (en : Equiv.Perm { a : ε // ¬p a }) {a : ε} (h : ¬p a) :
                                                                                    (Equiv.Perm.subtypeCongr ep en) a = (en { val := a, property := h })
                                                                                    @[simp]
                                                                                    theorem Equiv.Perm.subtypeCongr.right_apply_subtype {ε : Type u_1} {p : εProp} [DecidablePred p] (ep : Equiv.Perm { a : ε // p a }) (en : Equiv.Perm { a : ε // ¬p a }) (a : { a : ε // ¬p a }) :
                                                                                    (Equiv.Perm.subtypeCongr ep en) a = (en a)
                                                                                    @[simp]
                                                                                    theorem Equiv.Perm.subtypeCongr.refl {ε : Type u_1} {p : εProp} [DecidablePred p] :
                                                                                    Equiv.Perm.subtypeCongr (Equiv.refl { a : ε // p a }) (Equiv.refl { a : ε // ¬p a }) = Equiv.refl ε
                                                                                    @[simp]
                                                                                    theorem Equiv.Perm.subtypeCongr.symm {ε : Type u_1} {p : εProp} [DecidablePred p] (ep : Equiv.Perm { a : ε // p a }) (en : Equiv.Perm { a : ε // ¬p a }) :
                                                                                    @[simp]
                                                                                    theorem Equiv.Perm.subtypeCongr.trans {ε : Type u_1} {p : εProp} [DecidablePred p] (ep : Equiv.Perm { a : ε // p a }) (ep' : Equiv.Perm { a : ε // p a }) (en : Equiv.Perm { a : ε // ¬p a }) (en' : Equiv.Perm { a : ε // ¬p a }) :
                                                                                    (Equiv.Perm.subtypeCongr ep en).trans (Equiv.Perm.subtypeCongr ep' en') = Equiv.Perm.subtypeCongr (ep.trans ep') (en.trans en')
                                                                                    @[simp]
                                                                                    theorem Equiv.subtypePreimage_apply {α : Sort u_1} {β : Sort u_2} (p : αProp) [DecidablePred p] (x₀ : { a : α // p a }β) (x : { x : αβ // x Subtype.val = x₀ }) (a : { a : α // ¬p a }) :
                                                                                    (Equiv.subtypePreimage p x₀) x a = x a
                                                                                    @[simp]
                                                                                    theorem Equiv.subtypePreimage_symm_apply_coe {α : Sort u_1} {β : Sort u_2} (p : αProp) [DecidablePred p] (x₀ : { a : α // p a }β) (x : { a : α // ¬p a }β) (a : α) :
                                                                                    ((Equiv.subtypePreimage p x₀).symm x) a = if h : p a then x₀ { val := a, property := h } else x { val := a, property := h }
                                                                                    def Equiv.subtypePreimage {α : Sort u_1} {β : Sort u_2} (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
                                                                                      theorem Equiv.subtypePreimage_symm_apply_coe_pos {α : Sort u_1} {β : Sort u_2} (p : αProp) [DecidablePred p] (x₀ : { a : α // p a }β) (x : { a : α // ¬p a }β) (a : α) (h : p a) :
                                                                                      ((Equiv.subtypePreimage p x₀).symm x) a = x₀ { val := a, property := h }
                                                                                      theorem Equiv.subtypePreimage_symm_apply_coe_neg {α : Sort u_1} {β : Sort u_2} (p : αProp) [DecidablePred p] (x₀ : { a : α // p a }β) (x : { a : α // ¬p a }β) (a : α) (h : ¬p a) :
                                                                                      ((Equiv.subtypePreimage p x₀).symm x) a = x { val := a, property := h }
                                                                                      def Equiv.piCongrRight {α : Sort u_3} {β₁ : αSort u_1} {β₂ : αSort u_2} (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
                                                                                      • Equiv.piCongrRight F = { toFun := fun (H : (a : α) → β₁ a) (a : α) => (F a) (H a), invFun := fun (H : (a : α) → β₂ a) (a : α) => (F a).symm (H a), left_inv := , right_inv := }
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem Equiv.piComm_apply {α : Sort u_2} {β : Sort u_3} (φ : αβSort u_1) (f : (x : α) → (y : β) → φ x y) (y : β) (x : α) :
                                                                                        (Equiv.piComm φ) f y x = Function.swap f y x
                                                                                        def Equiv.piComm {α : Sort u_2} {β : Sort u_3} (φ : αβSort u_1) :
                                                                                        ((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
                                                                                        • Equiv.piComm φ = { toFun := Function.swap, invFun := Function.swap, left_inv := , right_inv := }
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          theorem Equiv.piComm_symm {α : Sort u_2} {β : Sort u_3} {φ : αβSort u_1} :
                                                                                          def Equiv.piCurry {α : Type u_1} {β : αType u_2} (γ : (a : α) → β aType u_3) :
                                                                                          ((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
                                                                                          • Equiv.piCurry γ = { toFun := Sigma.curry, invFun := Sigma.uncurry, left_inv := , right_inv := }
                                                                                          Instances For
                                                                                            def Equiv.prodCongrLeft {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁β₁ β₂) :
                                                                                            β₁ × α₁ β₂ × α₁

                                                                                            A family of equivalences ∀ (a : α₁), β₁ ≃ β₂ generates an equivalence between β₁ × α₁ and β₂ × α₁.

                                                                                            Equations
                                                                                            • Equiv.prodCongrLeft e = { toFun := fun (ab : β₁ × α₁) => ((e ab.2) ab.1, ab.2), invFun := fun (ab : β₂ × α₁) => ((e ab.2).symm ab.1, ab.2), left_inv := , right_inv := }
                                                                                            Instances For
                                                                                              @[simp]
                                                                                              theorem Equiv.prodCongrLeft_apply {α₁ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_1} (e : α₁β₁ β₂) (b : β₁) (a : α₁) :
                                                                                              (Equiv.prodCongrLeft e) (b, a) = ((e a) b, a)
                                                                                              theorem Equiv.prodCongr_refl_right {α₁ : Type u_3} {β₁ : Type u_1} {β₂ : Type u_2} (e : β₁ β₂) :
                                                                                              Equiv.prodCongr e (Equiv.refl α₁) = Equiv.prodCongrLeft fun (x : α₁) => e
                                                                                              def Equiv.prodCongrRight {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁β₁ β₂) :
                                                                                              α₁ × β₁ α₁ × β₂

                                                                                              A family of equivalences ∀ (a : α₁), β₁ ≃ β₂ generates an equivalence between α₁ × β₁ and α₁ × β₂.

                                                                                              Equations
                                                                                              • Equiv.prodCongrRight e = { toFun := fun (ab : α₁ × β₁) => (ab.1, (e ab.1) ab.2), invFun := fun (ab : α₁ × β₂) => (ab.1, (e ab.1).symm ab.2), left_inv := , right_inv := }
                                                                                              Instances For
                                                                                                @[simp]
                                                                                                theorem Equiv.prodCongrRight_apply {α₁ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_1} (e : α₁β₁ β₂) (a : α₁) (b : β₁) :
                                                                                                (Equiv.prodCongrRight e) (a, b) = (a, (e a) b)
                                                                                                theorem Equiv.prodCongr_refl_left {α₁ : Type u_3} {β₁ : Type u_1} {β₂ : Type u_2} (e : β₁ β₂) :
                                                                                                Equiv.prodCongr (Equiv.refl α₁) e = Equiv.prodCongrRight fun (x : α₁) => e
                                                                                                @[simp]
                                                                                                theorem Equiv.prodCongrLeft_trans_prodComm {α₁ : Type u_3} {β₁ : Type u_2} {β₂ : Type u_1} (e : α₁β₁ β₂) :
                                                                                                (Equiv.prodCongrLeft e).trans (Equiv.prodComm β₂ α₁) = (Equiv.prodComm β₁ α₁).trans (Equiv.prodCongrRight e)
                                                                                                @[simp]
                                                                                                theorem Equiv.prodCongrRight_trans_prodComm {α₁ : Type u_3} {β₁ : Type u_2} {β₂ : Type u_1} (e : α₁β₁ β₂) :
                                                                                                (Equiv.prodCongrRight e).trans (Equiv.prodComm α₁ β₂) = (Equiv.prodComm α₁ β₁).trans (Equiv.prodCongrLeft e)
                                                                                                theorem Equiv.sigmaCongrRight_sigmaEquivProd {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁β₁ β₂) :
                                                                                                theorem Equiv.sigmaEquivProd_sigmaCongrRight {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁β₁ β₂) :
                                                                                                (Equiv.sigmaEquivProd α₁ β₁).symm.trans (Equiv.sigmaCongrRight e) = (Equiv.prodCongrRight e).trans (Equiv.sigmaEquivProd α₁ β₂).symm
                                                                                                @[simp]
                                                                                                theorem Equiv.ofFiberEquiv_apply {α : Type u_1} {γ : Type u_2} {β : Type u_3} {f : αγ} {g : βγ} (e : (c : γ) → { a : α // f a = c } { b : β // g b = c }) :
                                                                                                ∀ (a : α), (Equiv.ofFiberEquiv e) a = ((e (f a)) ((Equiv.sigmaFiberEquiv f).symm a).snd)
                                                                                                @[simp]
                                                                                                theorem Equiv.ofFiberEquiv_symm_apply {α : Type u_1} {γ : Type u_2} {β : Type u_3} {f : αγ} {g : βγ} (e : (c : γ) → { a : α // f a = c } { b : β // g b = c }) :
                                                                                                ∀ (a : β), (Equiv.ofFiberEquiv e).symm a = ((Equiv.sigmaCongrRight e).symm ((Equiv.sigmaFiberEquiv g).symm a)).snd
                                                                                                def Equiv.ofFiberEquiv {α : Type u_1} {γ : Type u_2} {β : Type u_3} {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
                                                                                                  theorem Equiv.ofFiberEquiv_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αγ} {g : βγ} (e : (c : γ) → { a : α // f a = c } { b : β // g b = c }) (a : α) :
                                                                                                  g ((Equiv.ofFiberEquiv e) a) = f a
                                                                                                  @[simp]
                                                                                                  theorem Equiv.prodShear_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} {α₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : α₁β₁ β₂) :
                                                                                                  (Equiv.prodShear e₁ e₂) = fun (x : α₁ × β₁) => (e₁ x.1, (e₂ x.1) x.2)
                                                                                                  @[simp]
                                                                                                  theorem Equiv.prodShear_symm_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} {α₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : α₁β₁ β₂) :
                                                                                                  (Equiv.prodShear e₁ e₂).symm = fun (y : α₂ × β₂) => (e₁.symm y.1, (e₂ (e₁.symm y.1)).symm y.2)
                                                                                                  def Equiv.prodShear {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} {α₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : α₁β₁ β₂) :
                                                                                                  α₁ × β₁ α₂ × β₂

                                                                                                  A variation on Equiv.prodCongr where the equivalence in the second component can depend on the first component. A typical example is a shear mapping, explaining the name of this declaration.

                                                                                                  Equations
                                                                                                  • Equiv.prodShear e₁ e₂ = { toFun := fun (x : α₁ × β₁) => (e₁ x.1, (e₂ x.1) x.2), invFun := fun (y : α₂ × β₂) => (e₁.symm y.1, (e₂ (e₁.symm y.1)).symm y.2), left_inv := , right_inv := }
                                                                                                  Instances For
                                                                                                    def Equiv.Perm.prodExtendRight {α₁ : Type u_1} {β₁ : Type u_2} [DecidableEq α₁] (a : α₁) (e : Equiv.Perm β₁) :
                                                                                                    Equiv.Perm (α₁ × β₁)

                                                                                                    prodExtendRight a e extends e : Perm β to Perm (α × β) by sending (a, b) to (a, e b) and keeping the other (a', b) fixed.

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem Equiv.Perm.prodExtendRight_apply_eq {α₁ : Type u_2} {β₁ : Type u_1} [DecidableEq α₁] (a : α₁) (e : Equiv.Perm β₁) (b : β₁) :
                                                                                                      (Equiv.Perm.prodExtendRight a e) (a, b) = (a, e b)
                                                                                                      theorem Equiv.Perm.prodExtendRight_apply_ne {α₁ : Type u_1} {β₁ : Type u_2} [DecidableEq α₁] (e : Equiv.Perm β₁) {a : α₁} {a' : α₁} (h : a' a) (b : β₁) :
                                                                                                      (Equiv.Perm.prodExtendRight a e) (a', b) = (a', b)
                                                                                                      theorem Equiv.Perm.eq_of_prodExtendRight_ne {α₁ : Type u_2} {β₁ : Type u_1} [DecidableEq α₁] {e : Equiv.Perm β₁} {a : α₁} {a' : α₁} {b : β₁} (h : (Equiv.Perm.prodExtendRight a e) (a', b) (a', b)) :
                                                                                                      a' = a
                                                                                                      @[simp]
                                                                                                      theorem Equiv.Perm.fst_prodExtendRight {α₁ : Type u_1} {β₁ : Type u_2} [DecidableEq α₁] (a : α₁) (e : Equiv.Perm β₁) (ab : α₁ × β₁) :
                                                                                                      ((Equiv.Perm.prodExtendRight a e) ab).1 = ab.1
                                                                                                      def Equiv.arrowProdEquivProdArrow (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
                                                                                                      (γα × β) (γα) × (γβ)

                                                                                                      The type of functions to a product α × β is equivalent to the type of pairs of functions γ → α and γ → β.

                                                                                                      Equations
                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                      Instances For
                                                                                                        @[simp]
                                                                                                        theorem Equiv.sumPiEquivProdPi_symm_apply {ι : Type u_2} {ι' : Type u_3} (π : ι ι'Type u_1) (g : ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))) (t : ι ι') :
                                                                                                        (Equiv.sumPiEquivProdPi π).symm g t = Sum.rec g.1 g.2 t
                                                                                                        @[simp]
                                                                                                        theorem Equiv.sumPiEquivProdPi_apply {ι : Type u_2} {ι' : Type u_3} (π : ι ι'Type u_1) (f : (i : ι ι') → π i) :
                                                                                                        (Equiv.sumPiEquivProdPi π) f = (fun (i : ι) => f (Sum.inl i), fun (i' : ι') => f (Sum.inr i'))
                                                                                                        def Equiv.sumPiEquivProdPi {ι : Type u_2} {ι' : Type u_3} (π : ι ι'Type u_1) :
                                                                                                        ((i : ι ι') → π i) ((i : ι) → π (Sum.inl i)) × ((i' : ι') → π (Sum.inr i'))

                                                                                                        The type of dependent functions on a sum type ι ⊕ ι' is equivalent to the type of pairs of functions on ι and on ι'. This is a dependent version of Equiv.sumArrowEquivProdArrow.

                                                                                                        Equations
                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                        Instances For
                                                                                                          @[simp]
                                                                                                          theorem Equiv.prodPiEquivSumPi_symm_apply {ι : Type u_1} {ι' : Type u_2} (π : ιType u) (π' : ι'Type u) :
                                                                                                          ∀ (a : (i : ι ι') → Sum.elim π π' i), (Equiv.prodPiEquivSumPi π π').symm a = (Equiv.sumPiEquivProdPi (Sum.elim π π')) a
                                                                                                          @[simp]
                                                                                                          theorem Equiv.prodPiEquivSumPi_apply {ι : Type u_1} {ι' : Type u_2} (π : ιType u) (π' : ι'Type u) :
                                                                                                          ∀ (a : ((i : ι) → Sum.elim π π' (Sum.inl i)) × ((i' : ι') → Sum.elim π π' (Sum.inr i'))) (i : ι ι'), (Equiv.prodPiEquivSumPi π π') a i = (Equiv.sumPiEquivProdPi (Sum.elim π π')).symm a i
                                                                                                          def Equiv.prodPiEquivSumPi {ι : Type u_1} {ι' : Type u_2} (π : ιType u) (π' : ι'Type u) :
                                                                                                          ((i : ι) → π i) × ((i' : ι') → π' i') ((i : ι ι') → Sum.elim π π' i)

                                                                                                          The equivalence between a product of two dependent functions types and a single dependent function type. Basically a symmetric version of Equiv.sumPiEquivProdPi.

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            def Equiv.sumArrowEquivProdArrow (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
                                                                                                            (α βγ) (αγ) × (βγ)

                                                                                                            The type of functions on a sum type α ⊕ β is equivalent to the type of pairs of functions on α and on β.

                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For
                                                                                                              @[simp]
                                                                                                              theorem Equiv.sumArrowEquivProdArrow_apply_fst {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α βγ) (a : α) :
                                                                                                              ((Equiv.sumArrowEquivProdArrow α β γ) f).1 a = f (Sum.inl a)
                                                                                                              @[simp]
                                                                                                              theorem Equiv.sumArrowEquivProdArrow_apply_snd {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α βγ) (b : β) :
                                                                                                              ((Equiv.sumArrowEquivProdArrow α β γ) f).2 b = f (Sum.inr b)
                                                                                                              @[simp]
                                                                                                              theorem Equiv.sumArrowEquivProdArrow_symm_apply_inl {α : Type u_1} {γ : Type u_2} {β : Type u_3} (f : αγ) (g : βγ) (a : α) :
                                                                                                              (Equiv.sumArrowEquivProdArrow α β γ).symm (f, g) (Sum.inl a) = f a
                                                                                                              @[simp]
                                                                                                              theorem Equiv.sumArrowEquivProdArrow_symm_apply_inr {α : Type u_1} {γ : Type u_2} {β : Type u_3} (f : αγ) (g : βγ) (b : β) :
                                                                                                              (Equiv.sumArrowEquivProdArrow α β γ).symm (f, g) (Sum.inr b) = g b
                                                                                                              def Equiv.sumProdDistrib (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
                                                                                                              (α β) × γ α × γ β × γ

                                                                                                              Type product is right distributive with respect to type sum up to an equivalence.

                                                                                                              Equations
                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                              Instances For
                                                                                                                @[simp]
                                                                                                                theorem Equiv.sumProdDistrib_apply_left {α : Type u_1} {γ : Type u_2} {β : Type u_3} (a : α) (c : γ) :
                                                                                                                (Equiv.sumProdDistrib α β γ) (Sum.inl a, c) = Sum.inl (a, c)
                                                                                                                @[simp]
                                                                                                                theorem Equiv.sumProdDistrib_apply_right {β : Type u_1} {γ : Type u_2} {α : Type u_3} (b : β) (c : γ) :
                                                                                                                (Equiv.sumProdDistrib α β γ) (Sum.inr b, c) = Sum.inr (b, c)
                                                                                                                @[simp]
                                                                                                                theorem Equiv.sumProdDistrib_symm_apply_left {α : Type u_1} {γ : Type u_2} {β : Type u_3} (a : α × γ) :
                                                                                                                (Equiv.sumProdDistrib α β γ).symm (Sum.inl a) = (Sum.inl a.1, a.2)
                                                                                                                @[simp]
                                                                                                                theorem Equiv.sumProdDistrib_symm_apply_right {β : Type u_1} {γ : Type u_2} {α : Type u_3} (b : β × γ) :
                                                                                                                (Equiv.sumProdDistrib α β γ).symm (Sum.inr b) = (Sum.inr b.1, b.2)
                                                                                                                def Equiv.prodSumDistrib (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
                                                                                                                α × (β γ) α × β α × γ

                                                                                                                Type product is left distributive with respect to type sum up to an equivalence.

                                                                                                                Equations
                                                                                                                Instances For
                                                                                                                  @[simp]
                                                                                                                  theorem Equiv.prodSumDistrib_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) (b : β) :
                                                                                                                  (Equiv.prodSumDistrib α β γ) (a, Sum.inl b) = Sum.inl (a, b)
                                                                                                                  @[simp]
                                                                                                                  theorem Equiv.prodSumDistrib_apply_right {α : Type u_1} {γ : Type u_2} {β : Type u_3} (a : α) (c : γ) :
                                                                                                                  (Equiv.prodSumDistrib α β γ) (a, Sum.inr c) = Sum.inr (a, c)
                                                                                                                  @[simp]
                                                                                                                  theorem Equiv.prodSumDistrib_symm_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α × β) :
                                                                                                                  (Equiv.prodSumDistrib α β γ).symm (Sum.inl a) = (a.1, Sum.inl a.2)
                                                                                                                  @[simp]
                                                                                                                  theorem Equiv.prodSumDistrib_symm_apply_right {α : Type u_1} {γ : Type u_2} {β : Type u_3} (a : α × γ) :
                                                                                                                  (Equiv.prodSumDistrib α β γ).symm (Sum.inr a) = (a.1, Sum.inr a.2)
                                                                                                                  @[simp]
                                                                                                                  theorem Equiv.sigmaSumDistrib_apply {ι : Type u_3} (α : ιType u_1) (β : ιType u_2) (p : (i : ι) × (α i β i)) :
                                                                                                                  (Equiv.sigmaSumDistrib α β) p = Sum.map (Sigma.mk p.fst) (Sigma.mk p.fst) p.snd
                                                                                                                  @[simp]
                                                                                                                  theorem Equiv.sigmaSumDistrib_symm_apply {ι : Type u_3} (α : ιType u_1) (β : ιType u_2) :
                                                                                                                  ∀ (a : (i : ι) × α i (i : ι) × β i), (Equiv.sigmaSumDistrib α β).symm a = Sum.elim (Sigma.map id fun (x : ι) => Sum.inl) (Sigma.map id fun (x : ι) => Sum.inr) a
                                                                                                                  def Equiv.sigmaSumDistrib {ι : Type u_3} (α : ιType u_1) (β : ιType u_2) :
                                                                                                                  (i : ι) × (α i β i) (i : ι) × α i (i : ι) × β i

                                                                                                                  An indexed sum of disjoint sums of types is equivalent to the sum of the indexed sums.

                                                                                                                  Equations
                                                                                                                  • One or more equations did not get rendered due to their size.
                                                                                                                  Instances For
                                                                                                                    def Equiv.sigmaProdDistrib {ι : Type u_3} (α : ιType u_1) (β : Type u_2) :
                                                                                                                    ((i : ι) × α i) × β (i : ι) × α i × β

                                                                                                                    The product of an indexed sum of types (formally, a Sigma-type Σ i, α i) by a type β is equivalent to the sum of products Σ i, (α i × β).

                                                                                                                    Equations
                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                    Instances For
                                                                                                                      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
                                                                                                                        @[simp]
                                                                                                                        theorem Equiv.boolProdEquivSum_apply (α : Type u_1) (p : Bool × α) :
                                                                                                                        @[simp]
                                                                                                                        theorem Equiv.boolProdEquivSum_symm_apply (α : Type u_1) :
                                                                                                                        ∀ (a : α α), (Equiv.boolProdEquivSum α).symm a = Sum.elim (Prod.mk false) (Prod.mk true) a
                                                                                                                        def Equiv.boolProdEquivSum (α : Type u_1) :
                                                                                                                        Bool × α α α

                                                                                                                        The product Bool × α is equivalent to α ⊕ α.

                                                                                                                        Equations
                                                                                                                        Instances For
                                                                                                                          @[simp]
                                                                                                                          theorem Equiv.boolArrowEquivProd_apply (α : Type u_1) (f : Boolα) :
                                                                                                                          @[simp]
                                                                                                                          theorem Equiv.boolArrowEquivProd_symm_apply (α : Type u_1) (p : α × α) (b : Bool) :
                                                                                                                          (Equiv.boolArrowEquivProd α).symm p b = Bool.casesOn b p.1 p.2
                                                                                                                          def Equiv.boolArrowEquivProd (α : Type u_1) :
                                                                                                                          (Boolα) α × α

                                                                                                                          The function type Bool → α is equivalent to α × α.

                                                                                                                          Equations
                                                                                                                          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.listEquivOfEquiv {α : Type u_1} {β : Type u_2} (e : α β) :
                                                                                                                                List α List β

                                                                                                                                An equivalence between α and β generates an equivalence between List α and List β.

                                                                                                                                Equations
                                                                                                                                Instances For
                                                                                                                                  def Equiv.uniqueCongr {α : Sort u_1} {β : Sort u_2} (e : α β) :

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

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

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

                                                                                                                                    theorem Equiv.isEmpty {α : Sort u_1} {β : Sort u_2} (e : α β) [IsEmpty β] :
                                                                                                                                    def Equiv.subtypeEquiv {α : Sort u_1} {β : Sort u_2} {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
                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                    Instances For
                                                                                                                                      theorem Equiv.coe_subtypeEquiv_eq_map {X : Type u_1} {Y : Type u_2} {p : XProp} {q : YProp} (e : X Y) (h : ∀ (x : X), p x q (e x)) :
                                                                                                                                      (Equiv.subtypeEquiv e h) = Subtype.map e
                                                                                                                                      @[simp]
                                                                                                                                      theorem Equiv.subtypeEquiv_refl {α : Sort u_1} {p : αProp} (h : optParam (∀ (a : α), p a p ((Equiv.refl α) a)) ) :
                                                                                                                                      Equiv.subtypeEquiv (Equiv.refl α) h = Equiv.refl { a : α // p a }
                                                                                                                                      @[simp]
                                                                                                                                      theorem Equiv.subtypeEquiv_symm {α : Sort u_1} {β : Sort u_2} {p : αProp} {q : βProp} (e : α β) (h : ∀ (a : α), p a q (e a)) :
                                                                                                                                      @[simp]
                                                                                                                                      theorem Equiv.subtypeEquiv_trans {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {p : αProp} {q : βProp} {r : γProp} (e : α β) (f : β γ) (h : ∀ (a : α), p a q (e a)) (h' : ∀ (b : β), q b r (f b)) :
                                                                                                                                      (Equiv.subtypeEquiv e h).trans (Equiv.subtypeEquiv f h') = Equiv.subtypeEquiv (e.trans f)
                                                                                                                                      @[simp]
                                                                                                                                      theorem Equiv.subtypeEquiv_apply {α : Sort u_1} {β : Sort u_2} {p : αProp} {q : βProp} (e : α β) (h : ∀ (a : α), p a q (e a)) (x : { x : α // p x }) :
                                                                                                                                      (Equiv.subtypeEquiv e h) x = { val := e x, property := }
                                                                                                                                      @[simp]
                                                                                                                                      theorem Equiv.subtypeEquivRight_symm_apply_coe {α : Sort u_1} {p : αProp} {q : αProp} (e : ∀ (x : α), p x q x) (b : { b : α // (fun (x : α) => q x) b }) :
                                                                                                                                      ((Equiv.subtypeEquivRight e).symm b) = b
                                                                                                                                      @[simp]
                                                                                                                                      theorem Equiv.subtypeEquivRight_apply_coe {α : Sort u_1} {p : αProp} {q : αProp} (e : ∀ (x : α), p x q x) (a : { a : α // (fun (x : α) => p x) a }) :
                                                                                                                                      ((Equiv.subtypeEquivRight e) a) = a
                                                                                                                                      def Equiv.subtypeEquivRight {α : Sort u_1} {p : αProp} {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
                                                                                                                                        theorem Equiv.subtypeEquivRight_apply {α : Sort u_1} {p : αProp} {q : αProp} (e : ∀ (x : α), p x q x) (z : { x : α // p x }) :
                                                                                                                                        (Equiv.subtypeEquivRight e) z = { val := z, property := }
                                                                                                                                        theorem Equiv.subtypeEquivRight_symm_apply {α : Sort u_1} {p : αProp} {q : αProp} (e : ∀ (x : α), p x q x) (z : { x : α // q x }) :
                                                                                                                                        (Equiv.subtypeEquivRight e).symm z = { val := z, property := }
                                                                                                                                        def Equiv.subtypeEquivOfSubtype {β : Sort u_1} {α : Sort u_2} {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_2} {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 : αProp} {q : αProp} (h : p = q) :

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

                                                                                                                                            Equations
                                                                                                                                            Instances For
                                                                                                                                              @[simp]
                                                                                                                                              theorem Equiv.subtypeSubtypeEquivSubtypeExists_apply_coe {α : Sort u_1} (p : αProp) (q : Subtype pProp) (a : Subtype q) :
                                                                                                                                              @[simp]
                                                                                                                                              theorem Equiv.subtypeSubtypeEquivSubtypeExists_symm_apply_coe_coe {α : Sort u_1} (p : αProp) (q : Subtype pProp) (a : { a : α // ∃ (h : p a), q { val := a, property := h } }) :
                                                                                                                                              ((Equiv.subtypeSubtypeEquivSubtypeExists p q).symm a) = a
                                                                                                                                              def Equiv.subtypeSubtypeEquivSubtypeExists {α : Sort u_1} (p : αProp) (q : Subtype pProp) :
                                                                                                                                              Subtype q { a : α // ∃ (h : p a), q { val := a, property := 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
                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                              Instances For
                                                                                                                                                @[simp]
                                                                                                                                                theorem Equiv.subtypeSubtypeEquivSubtypeInter_symm_apply_coe_coe {α : Type u} (p : αProp) (q : αProp) :
                                                                                                                                                ∀ (a : { x : α // p x q x }), ((Equiv.subtypeSubtypeEquivSubtypeInter p q).symm a) = a
                                                                                                                                                @[simp]
                                                                                                                                                theorem Equiv.subtypeSubtypeEquivSubtypeInter_apply_coe {α : Type u} (p : αProp) (q : αProp) :
                                                                                                                                                ∀ (a : { x : Subtype p // q x }), ((Equiv.subtypeSubtypeEquivSubtypeInter p q) a) = a
                                                                                                                                                def Equiv.subtypeSubtypeEquivSubtypeInter {α : Type u} (p : αProp) (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.subtypeSubtypeEquivSubtype_apply_coe {α : Type u_1} {p : αProp} {q : αProp} (h : ∀ {x : α}, q xp x) :
                                                                                                                                                  ∀ (a : { x : Subtype p // q x }), ((Equiv.subtypeSubtypeEquivSubtype h) a) = a
                                                                                                                                                  @[simp]
                                                                                                                                                  theorem Equiv.subtypeSubtypeEquivSubtype_symm_apply_coe_coe {α : Type u_1} {p : αProp} {q : αProp} (h : ∀ {x : α}, q xp x) :
                                                                                                                                                  ∀ (a : Subtype q), ((Equiv.subtypeSubtypeEquivSubtype h).symm a) = a
                                                                                                                                                  def Equiv.subtypeSubtypeEquivSubtype {α : Type u_1} {p : αProp} {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.subtypeUnivEquiv_symm_apply {α : Type u_1} {p : αProp} (h : ∀ (x : α), p x) (x : α) :
                                                                                                                                                    (Equiv.subtypeUnivEquiv h).symm x = { val := x, property := }
                                                                                                                                                    @[simp]
                                                                                                                                                    theorem Equiv.subtypeUnivEquiv_apply {α : Type u_1} {p : αProp} (h : ∀ (x : α), p x) (x : Subtype p) :
                                                                                                                                                    def Equiv.subtypeUnivEquiv {α : Type u_1} {p : αProp} (h : ∀ (x : α), p x) :

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

                                                                                                                                                    Equations
                                                                                                                                                    • Equiv.subtypeUnivEquiv h = { toFun := fun (x : Subtype p) => x, invFun := fun (x : α) => { val := x, property := }, left_inv := , right_inv := }
                                                                                                                                                    Instances For
                                                                                                                                                      def Equiv.subtypeSigmaEquiv {α : Type u_1} (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_1} (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_1} {β : Type u_2} (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_1} {β : Type u_2} (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_1} (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
                                                                                                                                                              • One or more equations did not get rendered due to their size.
                                                                                                                                                              Instances For
                                                                                                                                                                def Equiv.piEquivSubtypeSigma (ι : Type u_2) (π : ιType u_1) :
                                                                                                                                                                ((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.subtypeProdEquivProd {α : Type u_1} {β : Type u_2} {p : αProp} {q : βProp} :
                                                                                                                                                                    { c : α × β // p c.1 q c.2 } { a : α // p a } × { b : β // q b }

                                                                                                                                                                    A subtype of a product defined by componentwise conditions is equivalent to a product of subtypes.

                                                                                                                                                                    Equations
                                                                                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                                                                                    Instances For
                                                                                                                                                                      def Equiv.subtypeProdEquivSigmaSubtype {α : Type u_1} {β : Type u_2} (p : αβProp) :
                                                                                                                                                                      { x : α × β // p x.1 x.2 } (a : α) × { b : β // p a b }

                                                                                                                                                                      A subtype of a Prod is equivalent to a sigma type whose fibers are subtypes.

                                                                                                                                                                      Equations
                                                                                                                                                                      • One or more equations did not get rendered due to their size.
                                                                                                                                                                      Instances For
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem Equiv.piEquivPiSubtypeProd_symm_apply {α : Type u_1} (p : αProp) (β : αType u_2) [DecidablePred p] (f : ((i : { x : α // p x }) → β i) × ((i : { x : α // ¬p x }) → β i)) (x : α) :
                                                                                                                                                                        (Equiv.piEquivPiSubtypeProd p β).symm f x = if h : p x then f.1 { val := x, property := h } else f.2 { val := x, property := h }
                                                                                                                                                                        @[simp]
                                                                                                                                                                        theorem Equiv.piEquivPiSubtypeProd_apply {α : Type u_1} (p : αProp) (β : αType u_2) [DecidablePred p] (f : (i : α) → β i) :
                                                                                                                                                                        (Equiv.piEquivPiSubtypeProd p β) f = (fun (x : { x : α // p x }) => f x, fun (x : { x : α // ¬p x }) => f x)
                                                                                                                                                                        def Equiv.piEquivPiSubtypeProd {α : Type u_1} (p : αProp) (β : αType u_2) [DecidablePred p] :
                                                                                                                                                                        ((i : α) → β i) ((i : { x : α // p x }) → β i) × ((i : { x : α // ¬p x }) → β i)

                                                                                                                                                                        The type ∀ (i : α), β i can be split as a product by separating the indices in α depending on whether they satisfy a predicate p or not.

                                                                                                                                                                        Equations
                                                                                                                                                                        • One or more equations did not get rendered due to their size.
                                                                                                                                                                        Instances For
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem Equiv.piSplitAt_apply {α : Type u_1} [DecidableEq α] (i : α) (β : αType u_2) (f : (j : α) → β j) :
                                                                                                                                                                          (Equiv.piSplitAt i β) f = (f i, fun (j : { j : α // j i }) => f j)
                                                                                                                                                                          @[simp]
                                                                                                                                                                          theorem Equiv.piSplitAt_symm_apply {α : Type u_1} [DecidableEq α] (i : α) (β : αType u_2) (f : β i × ((j : { j : α // j i }) → β j)) (j : α) :
                                                                                                                                                                          (Equiv.piSplitAt i β).symm f j = if h : j = i then f.1 else f.2 { val := j, property := h }
                                                                                                                                                                          def Equiv.piSplitAt {α : Type u_1} [DecidableEq α] (i : α) (β : αType u_2) :
                                                                                                                                                                          ((j : α) → β j) β i × ((j : { j : α // j i }) → β j)

                                                                                                                                                                          A product of types can be split as the binary product of one of the types and the product of all the remaining types.

                                                                                                                                                                          Equations
                                                                                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                                                                                          Instances For
                                                                                                                                                                            @[simp]
                                                                                                                                                                            theorem Equiv.funSplitAt_apply {α : Type u_1} [DecidableEq α] (i : α) (β : Type u_2) (f : (j : α) → (fun (a : α) => β) j) :
                                                                                                                                                                            (Equiv.funSplitAt i β) f = (f i, fun (j : { j : α // ¬j = i }) => f j)
                                                                                                                                                                            @[simp]
                                                                                                                                                                            theorem Equiv.funSplitAt_symm_apply {α : Type u_1} [DecidableEq α] (i : α) (β : Type u_2) (f : (fun (a : α) => β) i × ((j : { j : α // j i }) → (fun (a : α) => β) j)) (j : α) :
                                                                                                                                                                            (Equiv.funSplitAt i β).symm f j = if h : j = i then f.1 else f.2 { val := j, property := }
                                                                                                                                                                            def Equiv.funSplitAt {α : Type u_1} [DecidableEq α] (i : α) (β : Type u_2) :
                                                                                                                                                                            (αβ) β × ({ j : α // j i }β)

                                                                                                                                                                            A product of copies of a type can be split as the binary product of one copy and the product of all the remaining copies.

                                                                                                                                                                            Equations
                                                                                                                                                                            Instances For
                                                                                                                                                                              def Equiv.subtypeEquivCodomain {X : Sort u_1} [DecidableEq X] {x : X} {Y : Sort u_2} (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_2} [DecidableEq X] {x : X} {Y : Sort u_1} (f : { x' : X // x' x }Y) :
                                                                                                                                                                                (Equiv.subtypeEquivCodomain f) = fun (g : { g : XY // g Subtype.val = f }) => g x
                                                                                                                                                                                @[simp]
                                                                                                                                                                                theorem Equiv.subtypeEquivCodomain_apply {X : Sort u_2} [DecidableEq X] {x : X} {Y : Sort u_1} (f : { x' : X // x' x }Y) (g : { g : XY // g Subtype.val = f }) :
                                                                                                                                                                                theorem Equiv.coe_subtypeEquivCodomain_symm {X : Sort u_2} [DecidableEq X] {x : X} {Y : Sort u_1} (f : { x' : X // x' x }Y) :
                                                                                                                                                                                (Equiv.subtypeEquivCodomain f).symm = fun (y : Y) => { val := fun (x' : X) => if h : x' x then f { val := x', property := h } else y, property := }
                                                                                                                                                                                @[simp]
                                                                                                                                                                                theorem Equiv.subtypeEquivCodomain_symm_apply {X : Sort u_2} [DecidableEq X] {x : X} {Y : Sort u_1} (f : { x' : X // x' x }Y) (y : Y) (x' : X) :
                                                                                                                                                                                ((Equiv.subtypeEquivCodomain f).symm y) x' = if h : x' x then f { val := x', property := h } else y
                                                                                                                                                                                theorem Equiv.subtypeEquivCodomain_symm_apply_eq {X : Sort u_2} [DecidableEq X] {x : X} {Y : Sort u_1} (f : { x' : X // x' x }Y) (y : Y) :
                                                                                                                                                                                ((Equiv.subtypeEquivCodomain f).symm y) x = y
                                                                                                                                                                                theorem Equiv.subtypeEquivCodomain_symm_apply_ne {X : Sort u_2} [DecidableEq X] {x : X} {Y : Sort u_1} (f : { x' : X // x' x }Y) (y : Y) (x' : X) (h : x' x) :
                                                                                                                                                                                ((Equiv.subtypeEquivCodomain f).symm y) x' = f { val := x', property := h }
                                                                                                                                                                                instance Equiv.instCanLiftForAllEquivCoeInstFunLikeEquivBijective {α : Sort u_1} {β : Sort u_2} :
                                                                                                                                                                                CanLift (αβ) (α β) DFunLike.coe Function.Bijective
                                                                                                                                                                                Equations
                                                                                                                                                                                • =
                                                                                                                                                                                def Equiv.Perm.extendDomain {α' : Type u_1} {β' : Type u_2} (e : Equiv.Perm α') {p : β'Prop} [DecidablePred p] (f : α' Subtype p) :

                                                                                                                                                                                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_1} {β' : Type u_2} (e : Equiv.Perm α') {p : β'Prop} [DecidablePred p] (f : α' Subtype p) (a : α') :
                                                                                                                                                                                  (Equiv.Perm.extendDomain e f) (f a) = (f (e a))
                                                                                                                                                                                  theorem Equiv.Perm.extendDomain_apply_subtype {α' : Type u_1} {β' : Type u_2} (e : Equiv.Perm α') {p : β'Prop} [DecidablePred p] (f : α' Subtype p) {b : β'} (h : p b) :
                                                                                                                                                                                  (Equiv.Perm.extendDomain e f) b = (f (e (f.symm { val := b, property := h })))
                                                                                                                                                                                  theorem Equiv.Perm.extendDomain_apply_not_subtype {α' : Type u_1} {β' : Type u_2} (e : Equiv.Perm α') {p : β'Prop} [DecidablePred p] (f : α' Subtype p) {b : β'} (h : ¬p b) :
                                                                                                                                                                                  @[simp]
                                                                                                                                                                                  theorem Equiv.Perm.extendDomain_refl {α' : Type u_1} {β' : Type u_2} {p : β'Prop} [DecidablePred p] (f : α' Subtype p) :
                                                                                                                                                                                  @[simp]
                                                                                                                                                                                  theorem Equiv.Perm.extendDomain_symm {α' : Type u_1} {β' : Type u_2} (e : Equiv.Perm α') {p : β'Prop} [DecidablePred p] (f : α' Subtype p) :
                                                                                                                                                                                  theorem Equiv.Perm.extendDomain_trans {α' : Type u_1} {β' : Type u_2} {p : β'Prop} [DecidablePred p] (f : α' Subtype p) (e : Equiv.Perm α') (e' : Equiv.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₁), Setoid.r x y 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₁), Setoid.r x y x y) (x : α) (hx : p₂ x) :
                                                                                                                                                                                    (Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h) { val := x, property := hx } = { val := x, property := }
                                                                                                                                                                                    @[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₁), Setoid.r x y x y) (x : Subtype p₁) :
                                                                                                                                                                                    (Equiv.subtypeQuotientEquivQuotientSubtype p₁ p₂ hp₂ h).symm x = { val := x, property := }
                                                                                                                                                                                    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 : α) :
                                                                                                                                                                                      theorem Equiv.swapCore_swapCore {α : Sort u_1} [DecidableEq α] (r : α) (a : α) (b : α) :
                                                                                                                                                                                      theorem Equiv.swapCore_comm {α : Sort u_1} [DecidableEq α] (r : α) (a : α) (b : α) :
                                                                                                                                                                                      def Equiv.swap {α : Sort u_1} [DecidableEq α] (a : α) (b : α) :

                                                                                                                                                                                      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 : α) :
                                                                                                                                                                                        theorem Equiv.swap_apply_def {α : Sort u_1} [DecidableEq α] (a : α) (b : α) (x : α) :
                                                                                                                                                                                        (Equiv.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 : α) :
                                                                                                                                                                                        (Equiv.swap a b) a = b
                                                                                                                                                                                        @[simp]
                                                                                                                                                                                        theorem Equiv.swap_apply_right {α : Sort u_1} [DecidableEq α] (a : α) (b : α) :
                                                                                                                                                                                        (Equiv.swap a b) b = a
                                                                                                                                                                                        theorem Equiv.swap_apply_of_ne_of_ne {α : Sort u_1} [DecidableEq α] {a : α} {b : α} {x : α} :
                                                                                                                                                                                        x ax b(Equiv.swap a b) x = x
                                                                                                                                                                                        @[simp]
                                                                                                                                                                                        theorem Equiv.swap_swap {α : Sort u_1} [DecidableEq α] (a : α) (b : α) :
                                                                                                                                                                                        (Equiv.swap a b).trans (Equiv.swap a b) = Equiv.refl α
                                                                                                                                                                                        @[simp]
                                                                                                                                                                                        theorem Equiv.symm_swap {α : Sort u_1} [DecidableEq α] (a : α) (b : α) :
                                                                                                                                                                                        (Equiv.swap a b).symm = Equiv.swap a b
                                                                                                                                                                                        @[simp]
                                                                                                                                                                                        theorem Equiv.swap_eq_refl_iff {α : Sort u_1} [DecidableEq α] {x : α} {y : α} :
                                                                                                                                                                                        theorem Equiv.swap_comp_apply {α : Sort u_1} [DecidableEq α] {a : α} {b : α} {x : α} (π : Equiv.Perm α) :
                                                                                                                                                                                        (π.trans (Equiv.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_2} [DecidableEq α] {β : Sort u_1} (i : α) (j : α) (f : αβ) :
                                                                                                                                                                                        f (Equiv.swap i j) = Function.update (Function.update f j (f i)) i (f j)
                                                                                                                                                                                        @[simp]
                                                                                                                                                                                        theorem Equiv.symm_trans_swap_trans {α : Sort u_2} [DecidableEq α] {β : Sort u_1} [DecidableEq β] (a : α) (b : α) (e : α β) :
                                                                                                                                                                                        (e.symm.trans (Equiv.swap a b)).trans e = Equiv.swap (e a) (e b)
                                                                                                                                                                                        @[simp]
                                                                                                                                                                                        theorem Equiv.trans_swap_trans_symm {α : Sort u_2} [DecidableEq α] {β : Sort u_1} [DecidableEq β] (a : β) (b : β) (e : α β) :
                                                                                                                                                                                        (e.trans (Equiv.swap a b)).trans e.symm = Equiv.swap (e.symm a) (e.symm b)
                                                                                                                                                                                        @[simp]
                                                                                                                                                                                        theorem Equiv.swap_apply_self {α : Sort u_1} [DecidableEq α] (i : α) (j : α) (a : α) :
                                                                                                                                                                                        (Equiv.swap i j) ((Equiv.swap i j) a) = a
                                                                                                                                                                                        theorem Equiv.apply_swap_eq_self {α : Sort u_2} [DecidableEq α] {β : Sort u_1} {v : αβ} {i : α} {j : α} (hv : v i = v j) (k : α) :
                                                                                                                                                                                        v ((Equiv.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 : α} :
                                                                                                                                                                                        (Equiv.swap x y) z = w z = (Equiv.swap x y) w
                                                                                                                                                                                        theorem Equiv.swap_apply_ne_self_iff {α : Sort u_1} [DecidableEq α] {a : α} {b : α} {x : α} :
                                                                                                                                                                                        (Equiv.swap a b) x x a b (x = a x = b)
                                                                                                                                                                                        @[simp]
                                                                                                                                                                                        theorem Equiv.Perm.sumCongr_swap_refl {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (i : α) (j : α) :
                                                                                                                                                                                        @[simp]
                                                                                                                                                                                        theorem Equiv.Perm.sumCongr_refl_swap {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (i : β) (j : β) :
                                                                                                                                                                                        def Equiv.setValue {α : Sort u_1} [DecidableEq α] {β : Sort u_2} (f : α β) (a : α) (b : β) :
                                                                                                                                                                                        α β

                                                                                                                                                                                        Augment an equivalence with a prescribed mapping f a = b

                                                                                                                                                                                        Equations
                                                                                                                                                                                        Instances For
                                                                                                                                                                                          @[simp]
                                                                                                                                                                                          theorem Equiv.setValue_eq {α : Sort u_2} [DecidableEq α] {β : Sort u_1} (f : α β) (a : α) (b : β) :
                                                                                                                                                                                          (Equiv.setValue f a b) a = b
                                                                                                                                                                                          def Function.Involutive.toPerm {α : Sort u_1} (f : αα) (h : Function.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 : Function.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_2} [DecidableEq α] [DecidableEq β] {f : αβ} (hf : Function.Injective f) (x : α) (y : α) (z : α) :
                                                                                                                                                                                            f ((Equiv.swap x y) z) = (Equiv.swap (f x) (f y)) (f z)
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem Equiv.piCongrLeft'_apply {α : Sort u_2} {β : Sort u_3} (P : αSort u_1) (e : α β) (f : (a : α) → P a) (x : β) :
                                                                                                                                                                                            (Equiv.piCongrLeft' P e) f x = f (e.symm x)
                                                                                                                                                                                            @[simp]
                                                                                                                                                                                            theorem Equiv.piCongrLeft'_symm_apply {α : Sort u_2} {β : Sort u_3} (P : αSort u_1) (e : α β) (f : (b : β) → P (e.symm b)) (x : α) :
                                                                                                                                                                                            (Equiv.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.

                                                                                                                                                                                            def Equiv.piCongrLeft' {α : Sort u_2} {β : Sort u_3} (P : αSort u_1) (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'_symm {α : Sort u_2} {β : Sort u_3} (P : Sort u_1) (e : α β) :
                                                                                                                                                                                              (Equiv.piCongrLeft' (fun (x : α) => P) e).symm = Equiv.piCongrLeft' (fun (a : β) => P) e.symm

                                                                                                                                                                                              This lemma is impractical to state in the dependent case.

                                                                                                                                                                                              theorem Equiv.piCongrLeft'_symm_apply_apply {α : Sort u_2} {β : Sort u_3} (P : αSort u_1) (e : α β) (g : (b : β) → P (e.symm b)) (b : β) :
                                                                                                                                                                                              (Equiv.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_2} (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_2} (P : βSort w) (e : α β) (f : (a : α) → P (e a)) (b : β) :
                                                                                                                                                                                                (Equiv.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_2} (P : βSort w) (e : α β) (g : (b : β) → P b) (a : α) :
                                                                                                                                                                                                (Equiv.piCongrLeft P e).symm g a = g (e a)
                                                                                                                                                                                                theorem Equiv.piCongrLeft_apply_apply {β : Sort u_1} {α : Sort u_2} (P : βSort w) (e : α β) (f : (a : α) → P (e a)) (a : α) :
                                                                                                                                                                                                (Equiv.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_2} {α : Sort u_1} {P : βSort v} {e : α β} (f : (a : α) → P (e a)) (b : β) :
                                                                                                                                                                                                (Equiv.piCongrLeft P e) f b = cast (f (e.symm b))
                                                                                                                                                                                                theorem Equiv.piCongrLeft_sum_inl {ι'' : Sort u_2} {ι : Type u_3} {ι' : Type u_4} (π : ι''Type u_1) (e : ι ι' ι'') (f : (i : ι) → π (e (Sum.inl i))) (g : (i : ι') → π (e (Sum.inr i))) (i : ι) :
                                                                                                                                                                                                (Equiv.piCongrLeft π e) ((Equiv.sumPiEquivProdPi fun (x : ι ι') => π (e x)).symm (f, g)) (e (Sum.inl i)) = f i
                                                                                                                                                                                                theorem Equiv.piCongrLeft_sum_inr {ι'' : Sort u_2} {ι : Type u_3} {ι' : Type u_4} (π : ι''Type u_1) (e : ι ι' ι'') (f : (i : ι) → π (e (Sum.inl i))) (g : (i : ι') → π (e (Sum.inr i))) (j : ι') :
                                                                                                                                                                                                (Equiv.piCongrLeft π e) ((Equiv.sumPiEquivProdPi fun (x : ι ι') => π (e x)).symm (f, g)) (e (Sum.inr j)) = g j
                                                                                                                                                                                                def Equiv.piCongr {α : Sort u_1} {β : Sort u_2} {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_2} {β : Sort u_1} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (a : α) → W a Z (h₁ a)) :
                                                                                                                                                                                                  (Equiv.piCongr h₁ h₂).symm = fun (f : (b : β) → Z b) (a : α) => (h₂ a).symm (f (h₁ a))
                                                                                                                                                                                                  theorem Equiv.piCongr_symm_apply {α : Sort u_1} {β : Sort u_2} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (a : α) → W a Z (h₁ a)) (f : (b : β) → Z b) :
                                                                                                                                                                                                  (Equiv.piCongr h₁ h₂).symm f = fun (a : α) => (h₂ a).symm (f (h₁ a))
                                                                                                                                                                                                  @[simp]
                                                                                                                                                                                                  theorem Equiv.piCongr_apply_apply {α : Sort u_2} {β : Sort u_1} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (a : α) → W a Z (h₁ a)) (f : (a : α) → W a) (a : α) :
                                                                                                                                                                                                  (Equiv.piCongr h₁ h₂) f (h₁ a) = (h₂ a) (f a)
                                                                                                                                                                                                  def Equiv.piCongr' {α : Sort u_1} {β : Sort u_2} {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_2} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (b : β) → W (h₁.symm b) Z b) :
                                                                                                                                                                                                    (Equiv.piCongr' h₁ h₂) = fun (f : (a : α) → W a) (b : β) => (h₂ b) (f (h₁.symm b))
                                                                                                                                                                                                    theorem Equiv.piCongr'_apply {α : Sort u_2} {β : Sort u_1} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (b : β) → W (h₁.symm b) Z b) (f : (a : α) → W a) :
                                                                                                                                                                                                    (Equiv.piCongr' h₁ h₂) f = fun (b : β) => (h₂ b) (f (h₁.symm b))
                                                                                                                                                                                                    @[simp]
                                                                                                                                                                                                    theorem Equiv.piCongr'_symm_apply_symm_apply {α : Sort u_1} {β : Sort u_2} {W : αSort w} {Z : βSort z} (h₁ : α β) (h₂ : (b : β) → W (h₁.symm b) Z b) (f : (b : β) → Z b) (b : β) :
                                                                                                                                                                                                    (Equiv.piCongr' h₁ h₂).symm f (h₁.symm b) = (h₂ b).symm (f b)
                                                                                                                                                                                                    theorem Equiv.semiconj_conj {α₁ : Type u_2} {β₁ : Type u_1} (e : α₁ β₁) (f : α₁α₁) :
                                                                                                                                                                                                    Function.Semiconj (e) f ((Equiv.conj e) f)
                                                                                                                                                                                                    theorem Equiv.semiconj₂_conj {α₁ : Type u_2} {β₁ : Type u_1} (e : α₁ β₁) (f : α₁α₁α₁) :
                                                                                                                                                                                                    instance Equiv.instAssociativeCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁α₁α₁) [Std.Associative f] :
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    • =
                                                                                                                                                                                                    instance Equiv.instIdempotentOpCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁α₁α₁) [Std.IdempotentOp f] :
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    • =
                                                                                                                                                                                                    instance Equiv.instIsLeftCancelCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll {α₁ : Sort u_1} {β₁ : Sort u_2} (e : α₁ β₁) (f : α₁α₁α₁) [IsLeftCancel α₁ f] :
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    • =
                                                                                                                                                                                                    instance Equiv.instIsRightCancelCoeEquivForAllForAllInstFunLikeEquivArrowCongrForAllForAll {α₁ : Sort u_1} {β₁ : Sort u_2} (e : α₁ β₁) (f : α₁α₁α₁) [IsRightCancel α₁ f] :
                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    • =
                                                                                                                                                                                                    theorem Function.Injective.swap_apply {α : Sort u_1} {β : Sort u_2} [DecidableEq α] [DecidableEq β] {f : αβ} (hf : Function.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_2} [DecidableEq α] [DecidableEq β] {f : αβ} (hf : Function.Injective f) (x : α) (y : α) :
                                                                                                                                                                                                    (Equiv.swap (f x) (f y)) f = f (Equiv.swap x y)
                                                                                                                                                                                                    def subsingletonProdSelfEquiv {α : Type u_1} [Subsingleton α] :
                                                                                                                                                                                                    α × α α

                                                                                                                                                                                                    If α is a subsingleton, then it is equivalent to α × α.

                                                                                                                                                                                                    Equations
                                                                                                                                                                                                    • subsingletonProdSelfEquiv = { toFun := fun (p : α × α) => p.1, invFun := fun (a : α) => (a, a), left_inv := , right_inv := }
                                                                                                                                                                                                    Instances For
                                                                                                                                                                                                      def equivOfSubsingletonOfSubsingleton {α : Sort u_1} {β : Sort u_2} [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_2} {β : Sort u_3} [DecidableEq α'] [DecidableEq α] (f : αβ) (g : α' α) (a : α) (v : β) :
                                                                                                                                                                                                              Function.update f a v g = Function.update (f g) (g.symm a) v
                                                                                                                                                                                                              theorem Function.update_apply_equiv_apply {α' : Sort u_1} {α : Sort u_2} {β : Sort u_3} [DecidableEq α'] [DecidableEq α] (f : αβ) (g : α' α) (a : α) (v : β) (a' : α') :
                                                                                                                                                                                                              Function.update f a v (g a') = Function.update (f g) (g.symm a) v a'
                                                                                                                                                                                                              theorem Function.piCongrLeft'_update {α : Sort u_2} {β : Sort u_3} [DecidableEq α] [DecidableEq β] (P : αSort u_1) (e : α β) (f : (a : α) → P a) (b : β) (x : P (e.symm b)) :
                                                                                                                                                                                                              theorem Function.piCongrLeft'_symm_update {α : Sort u_2} {β : Sort u_3} [DecidableEq α] [DecidableEq β] (P : αSort u_1) (e : α β) (f : (b : β) → P (e.symm b)) (b : β) (x : P (e.symm b)) :
                                                                                                                                                                                                              (Equiv.piCongrLeft' P e).symm (Function.update f b x) = Function.update ((Equiv.piCongrLeft' P e).symm f) (e.symm b) x