Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mario Carneiro
Ported by: Kevin Buzzard, Ruben Vorster, Scott Morrison, Eric Rodriguez
! This file was ported from Lean 3 source module logic.equiv.basic
! leanprover-community/mathlib commit d2d8742b0c21426362a9dacebc6005db895ca963
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Bool.Basic
import Mathlib.Data.Prod.Basic
import Mathlib.Data.Sigma.Basic
import Mathlib.Data.Subtype
import Mathlib.Data.Sum.Basic
import Mathlib.Init.Data.Sigma.Basic
import Mathlib.Logic.Equiv.Defs
import Mathlib.Logic.Function.Conjugate
/-!
# Equivalence between types
In this file we continue the work on equivalences begun in `Logic/Equiv/Defs.lean`, defining
* canonical isomorphisms between various types: e.g.,
- `Equiv.sumEquivSigmaBool` is the canonical equivalence between the sum of two types `α ⊕ β`
and the sigma-type `Σ b : Bool, cond b α β`;
- `Equiv.prodSumDistrib : α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ)` shows that type product and type sum
satisfy the distributive law up to a canonical equivalence;
* operations on equivalences: e.g.,
- `Equiv.prodCongr ea eb : α₁ × β₁ ≃ α₂ × β₂`: combine two equivalences `ea : α₁ ≃ α₂` and
`eb : β₁ ≃ β₂` using `Prod.map`.
More definitions of this kind can be found in other files.
E.g., `Data/Equiv/TransferInstance.lean` does it for many algebraic type classes like
`Group`, `Module`, etc.
## Tags
equivalence, congruence, bijective map
-/
open Function
namespace Equiv
/-- `PProd α β` is equivalent to `α × β` -/
@[ simps apply : ∀ {α : Type u_1} {β : Type u_2} (x : PProd α β ↑pprodEquivProd x = (x .fstx .snd symm_apply : ∀ {α : Type u_1} {β : Type u_2} (x : α × β ↑pprodEquivProd .symmx = { fst := x .fstsnd := x .snd ]
def pprodEquivProd : PProd α β ≃ α × β where
toFun x := ( x . 1 , x . 2 )
invFun x := ⟨ x . 1 : {α : Type ?u.66} → {β : Type ?u.65} → α × β α , x . 2 : {α : Type ?u.70} → {β : Type ?u.69} → α × β β ⟩
left_inv := fun _ => rfl : ∀ {α : Sort ?u.78} {a : α }, a = a
right_inv := fun _ => rfl : ∀ {α : Sort ?u.90} {a : α }, a = a
#align equiv.pprod_equiv_prod Equiv.pprodEquivProd
#align equiv.pprod_equiv_prod_apply Equiv.pprodEquivProd_apply : ∀ {α : Type u_1} {β : Type u_2} (x : PProd α β ↑pprodEquivProd x = (x .fstx .snd
#align equiv.pprod_equiv_prod_symm_apply Equiv.pprodEquivProd_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (x : α × β ↑pprodEquivProd .symmx = { fst := x .fstsnd := x .snd
/-- Product of two equivalences, in terms of `PProd`. If `α ≃ β` and `γ ≃ δ`, then
`PProd α γ ≃ PProd β δ`. -/
-- porting note: in Lean 3 this had @[congr]`
@[ simps apply : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (e₁ : α ≃ β e₂ : γ ≃ δ x : PProd α γ ↑(pprodCongr e₁ e₂ x = { fst := ↑e₁ x .fst , snd := ↑e₂ x .snd } ]
def pprodCongr ( e₁ : α ≃ β ) ( e₂ : γ ≃ δ ) : PProd : Sort ?u.410 → Sort ?u.409 → Sort (max(max1?u.410)?u.409) α γ ≃ PProd : Sort ?u.412 → Sort ?u.411 → Sort (max(max1?u.412)?u.411) β δ where
toFun x := ⟨ e₁ x . 1 , e₂ x . 2 ⟩
invFun x := ⟨ e₁ . symm : {α : Sort ?u.585} → {β : Sort ?u.584} → α ≃ β β ≃ α x . 1 , e₂ . symm : {α : Sort ?u.666} → {β : Sort ?u.665} → α ≃ β β ≃ α x . 2 ⟩
left_inv := fun ⟨ x , y ⟩ => by (fun x => { fst := ↑e₁ .symmx .fst , snd := ↑e₂ .symmx .snd } )
((fun x => { fst := ↑e₁ x .fst , snd := ↑e₂ x .snd } ) { fst := x , snd := y } ) = { fst := x , snd := y } simp
right_inv := fun ⟨ x , y ⟩ => by (fun x => { fst := ↑e₁ x .fst , snd := ↑e₂ x .snd } )
((fun x => { fst := ↑e₁ .symmx .fst , snd := ↑e₂ .symmx .snd } ) { fst := x , snd := y } ) = { fst := x , snd := y } simp
#align equiv.pprod_congr Equiv.pprodCongr
#align equiv.pprod_congr_apply Equiv.pprodCongr_apply : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} (e₁ : α ≃ β e₂ : γ ≃ δ x : PProd α γ ↑(pprodCongr e₁ e₂ x = { fst := ↑e₁ x .fst , snd := ↑e₂ x .snd }
/-- Combine two equivalences using `PProd` in the domain and `Prod` in the codomain. -/
@[ simps! apply : ∀ {α₁ : Sort u_1} {α₂ : Type u_2} {β₁ : Sort u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂ eb : β₁ ≃ β₂ a : PProd α₁ β₁ ↑(pprodProd ea eb a = (↑ea a .fst , ↑eb a .snd ) symm_apply : ∀ {α₁ : Sort u_1} {α₂ : Type u_2} {β₁ : Sort u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂ eb : β₁ ≃ β₂ a : α₂ × β₂ ↑(pprodProd ea eb a = ↑(pprodCongr ea eb { fst := a .fstsnd := a .snd ]
def pprodProd ( ea : α₁ ≃ α₂ ) ( eb : β₁ ≃ β₂ ) :
PProd : Sort ?u.1934 → Sort ?u.1933 → Sort (max(max1?u.1934)?u.1933) α₁ β₁ ≃ α₂ × β₂ :=
( ea . pprodCongr eb ). trans : {α : Sort ?u.1966} → {β : Sort ?u.1965} → {γ : Sort ?u.1964} → α ≃ β β ≃ γ α ≃ γ trans pprodEquivProd : {α : Type ?u.1978} → {β : Type ?u.1977} → PProd α β ≃ α × β
#align equiv.pprod_prod Equiv.pprodProd : {α₁ : Sort u_1} → {α₂ : Type u_2} → {β₁ : Sort u_3} → {β₂ : Type u_4} → α₁ ≃ α₂ β₁ ≃ β₂ PProd α₁ β₁ ≃ α₂ × β₂
#align equiv.pprod_prod_apply Equiv.pprodProd_apply : ∀ {α₁ : Sort u_1} {α₂ : Type u_2} {β₁ : Sort u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂ eb : β₁ ≃ β₂ a : PProd α₁ β₁ ↑(pprodProd ea eb a = (↑ea a .fst , ↑eb a .snd )
#align equiv.pprod_prod_symm_apply Equiv.pprodProd_symm_apply : ∀ {α₁ : Sort u_1} {α₂ : Type u_2} {β₁ : Sort u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂ eb : β₁ ≃ β₂ a : α₂ × β₂ ↑(pprodProd ea eb a = ↑(pprodCongr ea eb { fst := a .fstsnd := a .snd
/-- Combine two equivalences using `PProd` in the codomain and `Prod` in the domain. -/
@[ simps! apply : ∀ {α₁ : Type u_1} {α₂ : Sort u_2} {β₁ : Type u_3} {β₂ : Sort u_4} (ea : α₁ ≃ α₂ eb : β₁ ≃ β₂ a : α₁ × β₁ ↑(prodPProd ea eb a = ↑(pprodCongr ea .symmeb .symm { fst := a .fstsnd := a .snd symm_apply : ∀ {α₁ : Type u_1} {α₂ : Sort u_2} {β₁ : Type u_3} {β₂ : Sort u_4} (ea : α₁ ≃ α₂ eb : β₁ ≃ β₂ a : PProd α₂ β₂ ↑(prodPProd ea eb a = (↑ea .symma .fst , ↑eb .symma .snd ) ]
def prodPProd ( ea : α₁ ≃ α₂ ) ( eb : β₁ ≃ β₂ ) :
α₁ × β₁ ≃ PProd : Sort ?u.2600 → Sort ?u.2599 → Sort (max(max1?u.2600)?u.2599) α₂ β₂ :=
( ea . symm : {α : Sort ?u.2609} → {β : Sort ?u.2608} → α ≃ β β ≃ α . pprodProd : {α₁ : Sort ?u.2617} →
{α₂ : Type ?u.2616} → {β₁ : Sort ?u.2615} → {β₂ : Type ?u.2614} → α₁ ≃ α₂ β₁ ≃ β₂ PProd α₁ β₁ ≃ α₂ × β₂ eb . symm : {α : Sort ?u.2631} → {β : Sort ?u.2630} → α ≃ β β ≃ α ). symm : {α : Sort ?u.2644} → {β : Sort ?u.2643} → α ≃ β β ≃ α symm
#align equiv.prod_pprod Equiv.prodPProd : {α₁ : Type u_1} → {α₂ : Sort u_2} → {β₁ : Type u_3} → {β₂ : Sort u_4} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ × β₁ ≃ PProd α₂ β₂
#align equiv.prod_pprod_symm_apply Equiv.prodPProd_symm_apply : ∀ {α₁ : Type u_1} {α₂ : Sort u_2} {β₁ : Type u_3} {β₂ : Sort u_4} (ea : α₁ ≃ α₂ eb : β₁ ≃ β₂ a : PProd α₂ β₂ ↑(prodPProd ea eb a = (↑ea .symma .fst , ↑eb .symma .snd )
#align equiv.prod_pprod_apply Equiv.prodPProd_apply : ∀ {α₁ : Type u_1} {α₂ : Sort u_2} {β₁ : Type u_3} {β₂ : Sort u_4} (ea : α₁ ≃ α₂ eb : β₁ ≃ β₂ a : α₁ × β₁ ↑(prodPProd ea eb a = ↑(pprodCongr ea .symmeb .symm { fst := a .fstsnd := a .snd
/-- `PProd α β` is equivalent to `PLift α × PLift β` -/
@[ simps! apply : ∀ {α : Sort u_1} {β : Sort u_2} (a : PProd α β ↑pprodEquivProdPLift a = (↑Equiv.plift .symma .fst , ↑Equiv.plift .symma .snd ) symm_apply : ∀ {α : Sort u_1} {β : Sort u_2} (a : PLift α × PLift β ↑pprodEquivProdPLift .symma = ↑(pprodCongr Equiv.plift .symmEquiv.plift .symm { fst := a .fstsnd := a .snd ]
def pprodEquivProdPLift : PProd : Sort ?u.3242 → Sort ?u.3241 → Sort (max(max1?u.3242)?u.3241) α β ≃ PLift α × PLift β :=
Equiv.plift . symm : {α : Sort ?u.3253} → {β : Sort ?u.3252} → α ≃ β β ≃ α . pprodProd : {α₁ : Sort ?u.3261} →
{α₂ : Type ?u.3260} → {β₁ : Sort ?u.3259} → {β₂ : Type ?u.3258} → α₁ ≃ α₂ β₁ ≃ β₂ PProd α₁ β₁ ≃ α₂ × β₂ Equiv.plift . symm : {α : Sort ?u.3283} → {β : Sort ?u.3282} → α ≃ β β ≃ α
#align equiv.pprod_equiv_prod_plift Equiv.pprodEquivProdPLift
#align equiv.pprod_equiv_prod_plift_symm_apply Equiv.pprodEquivProdPLift_symm_apply : ∀ {α : Sort u_1} {β : Sort u_2} (a : PLift α × PLift β ↑pprodEquivProdPLift .symma = ↑(pprodCongr Equiv.plift .symmEquiv.plift .symm { fst := a .fstsnd := a .snd
#align equiv.pprod_equiv_prod_plift_apply Equiv.pprodEquivProdPLift_apply : ∀ {α : Sort u_1} {β : Sort u_2} (a : PProd α β ↑pprodEquivProdPLift a = (↑Equiv.plift .symma .fst , ↑Equiv.plift .symma .snd )
/-- Product of two equivalences. If `α₁ ≃ α₂` and `β₁ ≃ β₂`, then `α₁ × β₁ ≃ α₂ × β₂`. This is
`Prod.map` as an equivalence. -/
-- porting note: in Lean 3 there was also a @[congr] tag
@[ simps ( config := .asFn ) apply ]
def prodCongr : {α₁ : Type ?u.3881} →
{α₂ : Type ?u.3883} → {β₁ : Type ?u.3880} → {β₂ : Type ?u.3882} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ × β₁ ≃ α₂ × β₂ prodCongr ( e₁ : α₁ ≃ α₂ ) ( e₂ : β₁ ≃ β₂ ) : α₁ × β₁ ≃ α₂ × β₂ :=
⟨ Prod.map : {α₁ : Type ?u.3906} →
{α₂ : Type ?u.3905} → {β₁ : Type ?u.3904} → {β₂ : Type ?u.3903} → (α₁ → α₂ (β₁ → β₂ α₁ × β₁ α₂ × β₂ e₁ e₂ , Prod.map : {α₁ : Type ?u.4059} →
{α₂ : Type ?u.4058} → {β₁ : Type ?u.4057} → {β₂ : Type ?u.4056} → (α₁ → α₂ (β₁ → β₂ α₁ × β₁ α₂ × β₂ e₁ . symm : {α : Sort ?u.4067} → {β : Sort ?u.4066} → α ≃ β β ≃ α e₂ . symm : {α : Sort ?u.4141} → {β : Sort ?u.4140} → α ≃ β β ≃ α , fun ⟨ a , b ⟩ => by α₁ : Type ?u.3881α₂ : Type ?u.3883β₁ : Type ?u.3880β₂ : Type ?u.3882e₁ : α₁ ≃ α₂ e₂ : β₁ ≃ β₂ x✝ : α₁ × β₁ a : α₁ b : β₁ simp , fun ⟨ a , b ⟩ => by α₁ : Type ?u.3881α₂ : Type ?u.3883β₁ : Type ?u.3880β₂ : Type ?u.3882e₁ : α₁ ≃ α₂ e₂ : β₁ ≃ β₂ x✝ : α₂ × β₂ a : α₂ b : β₂ simp ⟩
#align equiv.prod_congr Equiv.prodCongr : {α₁ : Type u_1} → {α₂ : Type u_2} → {β₁ : Type u_3} → {β₂ : Type u_4} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ × β₁ ≃ α₂ × β₂
#align equiv.prod_congr_apply Equiv.prodCongr_apply
@[ simp ]
theorem prodCongr_symm ( e₁ : α₁ ≃ α₂ ) ( e₂ : β₁ ≃ β₂ ) :
( prodCongr : {α₁ : Type ?u.5682} →
{α₂ : Type ?u.5681} → {β₁ : Type ?u.5680} → {β₂ : Type ?u.5679} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ × β₁ ≃ α₂ × β₂ e₁ e₂ ). symm : {α : Sort ?u.5692} → {β : Sort ?u.5691} → α ≃ β β ≃ α symm = prodCongr : {α₁ : Type ?u.5703} →
{α₂ : Type ?u.5702} → {β₁ : Type ?u.5701} → {β₂ : Type ?u.5700} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ × β₁ ≃ α₂ × β₂ e₁ . symm : {α : Sort ?u.5709} → {β : Sort ?u.5708} → α ≃ β β ≃ α e₂ . symm : {α : Sort ?u.5720} → {β : Sort ?u.5719} → α ≃ β β ≃ α :=
rfl : ∀ {α : Sort ?u.5740} {a : α }, a = a
#align equiv.prod_congr_symm Equiv.prodCongr_symm
/-- Type product is commutative up to an equivalence: `α × β ≃ β × α`. This is `Prod.swap` as an
equivalence.-/
def prodComm : (α : Type u_1) → (β : Type u_2) → α × β ≃ β × α prodComm ( α β ) : α × β ≃ β × α :=
⟨ Prod.swap : {α : Type ?u.5851} → {β : Type ?u.5850} → α × β β × α , Prod.swap : {α : Type ?u.5862} → {β : Type ?u.5861} → α × β β × α , Prod.swap_swap , Prod.swap_swap ⟩
#align equiv.prod_comm Equiv.prodComm : (α : Type u_1) → (β : Type u_2) → α × β ≃ β × α
@[ simp ]
theorem coe_prodComm ( α β ) : (⇑( prodComm : (α : Type ?u.5992) → (β : Type ?u.5991) → α × β ≃ β × α α β ) : α × β → β × α ) = Prod.swap : {α : Type ?u.6067} → {β : Type ?u.6066} → α × β β × α :=
rfl : ∀ {α : Sort ?u.6124} {a : α }, a = a
#align equiv.coe_prod_comm Equiv.coe_prodComm
@[ simp ]
theorem prodComm_apply ( x : α × β ) : prodComm : (α : Type ?u.6180) → (β : Type ?u.6179) → α × β ≃ β × α α β x = x . swap : {α : Type ?u.6252} → {β : Type ?u.6251} → α × β β × α :=
rfl : ∀ {α : Sort ?u.6268} {a : α }, a = a
#align equiv.prod_comm_apply Equiv.prodComm_apply
@[ simp ]
theorem prodComm_symm ( α β ) : ( prodComm : (α : Type ?u.6314) → (β : Type ?u.6313) → α × β ≃ β × α α β ). symm : {α : Sort ?u.6316} → {β : Sort ?u.6315} → α ≃ β β ≃ α symm = prodComm : (α : Type ?u.6325) → (β : Type ?u.6324) → α × β ≃ β × α β α :=
rfl : ∀ {α : Sort ?u.6334} {a : α }, a = a
#align equiv.prod_comm_symm Equiv.prodComm_symm
/-- Type product is associative up to an equivalence. -/
@[ simps : ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : α × β × γ ↑(prodAssoc α β γ p = ((p .fstp .snd , p .snd simps ]
def prodAssoc : (α : Type ?u.6397) → (β : Type ?u.6396) → (γ : Type ?u.6394) → (α × β × γ ≃ α × β × γ prodAssoc ( α β γ ) : ( α × β ) × γ ≃ α × β × γ :=
⟨ fun p => ( p . 1 : {α : Type ?u.6428} → {β : Type ?u.6427} → α × β α . 1 : {α : Type ?u.6434} → {β : Type ?u.6433} → α × β α , p . 1 : {α : Type ?u.6446} → {β : Type ?u.6445} → α × β α . 2 : {α : Type ?u.6450} → {β : Type ?u.6449} → α × β β , p . 2 : {α : Type ?u.6454} → {β : Type ?u.6453} → α × β β ), fun p => (( p . 1 : {α : Type ?u.6471} → {β : Type ?u.6470} → α × β α , p . 2 : {α : Type ?u.6475} → {β : Type ?u.6474} → α × β β . 1 : {α : Type ?u.6479} → {β : Type ?u.6478} → α × β α ), p . 2 : {α : Type ?u.6483} → {β : Type ?u.6482} → α × β β . 2 : {α : Type ?u.6487} → {β : Type ?u.6486} → α × β β ), fun ⟨⟨_, _⟩, _⟩ => rfl : ∀ {α : Sort ?u.6541} {a : α }, a = a ,
fun ⟨_, ⟨_, _⟩⟩ => rfl : ∀ {α : Sort ?u.6702} {a : α }, a = a ⟩
#align equiv.prod_assoc Equiv.prodAssoc : (α : Type u_1) → (β : Type u_2) → (γ : Type u_3) → (α × β × γ ≃ α × β × γ
#align equiv.prod_assoc_symm_apply Equiv.prodAssoc_symm_apply : ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : α × β × γ ↑(prodAssoc α β γ p = ((p .fstp .snd , p .snd
#align equiv.prod_assoc_apply Equiv.prodAssoc_apply : ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : (α × β × γ ), ↑(prodAssoc α β γ p = (p .fstp .fstp .snd
/-- `γ`-valued functions on `α × β` are equivalent to functions `α → β → γ`. -/
@[ simps ( config := { fullyApplied := false })]
def curry : (α : Type u_1) → (β : Type u_2) → (γ : Type u_3) → (α × β γ ≃ (α → β → γ curry ( α β γ ) : ( α × β → γ ) ≃ ( α → β → γ ) where
toFun := Function.curry : {α : Type ?u.7212} → {β : Type ?u.7211} → {φ : Type ?u.7210} → (α × β φ α → β → φ
invFun := uncurry : {α : Type ?u.7231} → {β : Type ?u.7230} → {φ : Type ?u.7229} → (α → β → φ α × β φ
left_inv := uncurry_curry
right_inv := curry_uncurry
#align equiv.curry Equiv.curry : (α : Type u_1) → (β : Type u_2) → (γ : Type u_3) → (α × β γ ≃ (α → β → γ
#align equiv.curry_symm_apply Equiv.curry_symm_apply : ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), ↑(curry α β γ = uncurry
#align equiv.curry_apply Equiv.curry_apply : ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), ↑(curry α β γ = Function.curry
section
/-- `PUnit` is a right identity for type product up to an equivalence. -/
@[ simps ]
def prodPUnit ( α ) : α × PUnit ≃ α :=
⟨ fun p => p . 1 : {α : Type ?u.7578} → {β : Type ?u.7577} → α × β α , fun a => ( a , PUnit.unit ), fun ⟨_, PUnit.unit ⟩ => rfl : ∀ {α : Sort ?u.7625} {a : α }, a = a , fun _ => rfl : ∀ {α : Sort ?u.7707} {a : α }, a = a ⟩
#align equiv.prod_punit Equiv.prodPUnit
#align equiv.prod_punit_apply Equiv.prodPUnit_apply
#align equiv.prod_punit_symm_apply Equiv.prodPUnit_symm_apply
/-- `PUnit` is a left identity for type product up to an equivalence. -/
@[ simps! ]
def punitProd ( α ) : PUnit × α ≃ α :=
calc
PUnit × α ≃ α × PUnit := prodComm : (α : Type ?u.7887) → (β : Type ?u.7886) → α × β ≃ β × α _ _
_ ≃ α := prodPUnit _
#align equiv.punit_prod Equiv.punitProd
#align equiv.punit_prod_symm_apply Equiv.punitProd_symm_apply
#align equiv.punit_prod_apply Equiv.punitProd_apply
/-- Any `Unique` type is a right identity for type product up to equivalence. -/
def prodUnique ( α β ) [ Unique : Sort ?u.8318 → Sort (max1?u.8318) β ] : α × β ≃ α :=
(( Equiv.refl : (α : Sort ?u.8329) → α ≃ α α ). prodCongr : {α₁ : Type ?u.8333} →
{α₂ : Type ?u.8332} → {β₁ : Type ?u.8331} → {β₂ : Type ?u.8330} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ × β₁ ≃ α₂ × β₂ prodCongr <| equivPUnit .{_,1} β ). trans : {α : Sort ?u.8356} → {β : Sort ?u.8355} → {γ : Sort ?u.8354} → α ≃ β β ≃ γ α ≃ γ trans <| prodPUnit α
#align equiv.prod_unique Equiv.prodUnique : (α : Type u_1) → (β : Type u_2) → [inst : Unique β α × β ≃ α
@[ simp ]
theorem coe_prodUnique [ Unique : Sort ?u.8407 → Sort (max1?u.8407) β ] : (⇑( prodUnique : (α : Type ?u.8429) → (β : Type ?u.8428) → [inst : Unique β α × β ≃ α α β ) : α × β → α ) = Prod.fst : {α : Type ?u.8499} → {β : Type ?u.8498} → α × β α :=
rfl : ∀ {α : Sort ?u.8557} {a : α }, a = a
#align equiv.coe_prod_unique Equiv.coe_prodUnique
theorem prodUnique_apply [ Unique : Sort ?u.8616 → Sort (max1?u.8616) β ] ( x : α × β ) : prodUnique : (α : Type ?u.8625) → (β : Type ?u.8624) → [inst : Unique β α × β ≃ α α β x = x . 1 : {α : Type ?u.8694} → {β : Type ?u.8693} → α × β α :=
rfl : ∀ {α : Sort ?u.8706} {a : α }, a = a
#align equiv.prod_unique_apply Equiv.prodUnique_apply
@[ simp ]
theorem prodUnique_symm_apply [ Unique : Sort ?u.8732 → Sort (max1?u.8732) β ] ( x : α ) :
( prodUnique : (α : Type ?u.8746) → (β : Type ?u.8745) → [inst : Unique β α × β ≃ α α β ). symm : {α : Sort ?u.8752} → {β : Sort ?u.8751} → α ≃ β β ≃ α symm x = ( x , default ) :=
rfl : ∀ {α : Sort ?u.9208} {a : α }, a = a
#align equiv.prod_unique_symm_apply Equiv.prodUnique_symm_apply : ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β x : α ), ↑(prodUnique α β x = (x , default )
/-- Any `Unique` type is a left identity for type product up to equivalence. -/
def uniqueProd : (α : Type ?u.9271) → (β : Type ?u.9272) → [inst : Unique β β × α ≃ α uniqueProd ( α β ) [ Unique : Sort ?u.9266 → Sort (max1?u.9266) β ] : β × α ≃ α :=
(( equivPUnit .{_,1} β ). prodCongr : {α₁ : Type ?u.9284} →
{α₂ : Type ?u.9283} → {β₁ : Type ?u.9282} → {β₂ : Type ?u.9281} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ × β₁ ≃ α₂ × β₂ prodCongr <| Equiv.refl : (α : Sort ?u.9297) → α ≃ α α ). trans : {α : Sort ?u.9304} → {β : Sort ?u.9303} → {γ : Sort ?u.9302} → α ≃ β β ≃ γ α ≃ γ trans <| punitProd α
#align equiv.unique_prod Equiv.uniqueProd : (α : Type u_1) → (β : Type u_2) → [inst : Unique β β × α ≃ α
@[ simp ]
theorem coe_uniqueProd [ Unique : Sort ?u.9355 → Sort (max1?u.9355) β ] : (⇑( uniqueProd : (α : Type ?u.9377) → (β : Type ?u.9376) → [inst : Unique β β × α ≃ α α β ) : β × α → α ) = Prod.snd : {α : Type ?u.9447} → {β : Type ?u.9446} → α × β β :=
rfl : ∀ {α : Sort ?u.9505} {a : α }, a = a
#align equiv.coe_unique_prod Equiv.coe_uniqueProd
theorem uniqueProd_apply [ Unique : Sort ?u.9567 → Sort (max1?u.9567) β ] ( x : β × α ) : uniqueProd : (α : Type ?u.9576) → (β : Type ?u.9575) → [inst : Unique β β × α ≃ α α β x = x . 2 : {α : Type ?u.9645} → {β : Type ?u.9644} → α × β β :=
rfl : ∀ {α : Sort ?u.9657} {a : α }, a = a
#align equiv.unique_prod_apply Equiv.uniqueProd_apply
@[ simp ]
theorem uniqueProd_symm_apply [ Unique : Sort ?u.9690 → Sort (max1?u.9690) β ] ( x : α ) :
( uniqueProd : (α : Type ?u.9697) → (β : Type ?u.9696) → [inst : Unique β β × α ≃ α α β ). symm : {α : Sort ?u.9703} → {β : Sort ?u.9702} → α ≃ β β ≃ α symm x = ( default , x ) :=
rfl : ∀ {α : Sort ?u.10158} {a : α }, a = a
#align equiv.unique_prod_symm_apply Equiv.uniqueProd_symm_apply : ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β x : α ), ↑(uniqueProd α β x = (default , x )
/-- `Empty` type is a right absorbing element for type product up to an equivalence. -/
def prodEmpty ( α ) : α × Empty ≃ Empty :=
equivEmpty _
#align equiv.prod_empty Equiv.prodEmpty
/-- `Empty` type is a left absorbing element for type product up to an equivalence. -/
def emptyProd ( α ) : Empty × α ≃ Empty :=
equivEmpty _
#align equiv.empty_prod Equiv.emptyProd
/-- `PEmpty` type is a right absorbing element for type product up to an equivalence. -/
def prodPEmpty ( α ) : α × PEmpty ≃ PEmpty :=
equivPEmpty _
#align equiv.prod_pempty Equiv.prodPEmpty
/-- `PEmpty` type is a left absorbing element for type product up to an equivalence. -/
def pemptyProd ( α ) : PEmpty × α ≃ PEmpty :=
equivPEmpty _
#align equiv.pempty_prod Equiv.pemptyProd
end
section
open Sum
/-- `PSum` is equivalent to `Sum`. -/
def psumEquivSum : (α : Type u_1) → (β : Type u_2) → α ⊕' β ≃ α ⊕ β psumEquivSum ( α β ) : PSum : Sort ?u.10613 → Sort ?u.10612 → Sort (max(max1?u.10613)?u.10612) α β ≃ Sum : Type ?u.10615 → Type ?u.10614 → Type (max?u.10615?u.10614) α β where
toFun s := PSum.casesOn : {α : Sort ?u.10629} →
{β : Sort ?u.10628} →
{motive : α ⊕' β Sort ?u.10630(t : α ⊕' β ((val : α ) → motive (PSum.inl val ) → ((val : β ) → motive (PSum.inr val ) → motive t s inl : {α : Type ?u.10707} → {β : Type ?u.10706} → α → α ⊕ β inr : {α : Type ?u.10714} → {β : Type ?u.10713} → β → α ⊕ β
invFun := Sum.elim : {α : Type ?u.10669} → {β : Type ?u.10668} → {γ : Sort ?u.10667} → (α → γ (β → γ α ⊕ β γ PSum.inl : {α : Sort ?u.10678} → {β : Sort ?u.10677} → α → α ⊕' β PSum.inr : {α : Sort ?u.10685} → {β : Sort ?u.10684} → β → α ⊕' β
left_inv s := by cases s <;> rfl
right_inv s := by cases s <;> rfl
#align equiv.psum_equiv_sum Equiv.psumEquivSum : (α : Type u_1) → (β : Type u_2) → α ⊕' β ≃ α ⊕ β
/-- If `α ≃ α'` and `β ≃ β'`, then `α ⊕ β ≃ α' ⊕ β'`. This is `Sum.map` as an equivalence. -/
@[ simps apply ]
def sumCongr : {α₁ : Type u_1} → {α₂ : Type u_2} → {β₁ : Type u_3} → {β₂ : Type u_4} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕ β₁ ≃ α₂ ⊕ β₂ sumCongr ( ea : α₁ ≃ α₂ ) ( eb : β₁ ≃ β₂ ) : Sum : Type ?u.11042 → Type ?u.11041 → Type (max?u.11042?u.11041) α₁ β₁ ≃ Sum : Type ?u.11044 → Type ?u.11043 → Type (max?u.11044?u.11043) α₂ β₂ :=
⟨ Sum.map : {α : Type ?u.11067} →
{α' : Type ?u.11065} → {β : Type ?u.11066} → {β' : Type ?u.11064} → (α → α' (β → β' α ⊕ β α' ⊕ β' ea eb , Sum.map : {α : Type ?u.11220} →
{α' : Type ?u.11218} → {β : Type ?u.11219} → {β' : Type ?u.11217} → (α → α' (β → β' α ⊕ β α' ⊕ β' ea . symm : {α : Sort ?u.11228} → {β : Sort ?u.11227} → α ≃ β β ≃ α eb . symm : {α : Sort ?u.11302} → {β : Sort ?u.11301} → α ≃ β β ≃ α , fun x => by α₁ : Type ?u.11042α₂ : Type ?u.11044β₁ : Type ?u.11041β₂ : Type ?u.11043ea : α₁ ≃ α₂ eb : β₁ ≃ β₂ x : α₁ ⊕ β₁ simp , fun x => by α₁ : Type ?u.11042α₂ : Type ?u.11044β₁ : Type ?u.11041β₂ : Type ?u.11043ea : α₁ ≃ α₂ eb : β₁ ≃ β₂ x : α₂ ⊕ β₂ simp ⟩
#align equiv.sum_congr Equiv.sumCongr : {α₁ : Type u_1} → {α₂ : Type u_2} → {β₁ : Type u_3} → {β₂ : Type u_4} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕ β₁ ≃ α₂ ⊕ β₂
#align equiv.sum_congr_apply Equiv.sumCongr_apply : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂ eb : β₁ ≃ β₂ a : α₁ ⊕ β₁ ↑(sumCongr ea eb a = Sum.map (↑ea ) (↑eb ) a
/-- If `α ≃ α'` and `β ≃ β'`, then `PSum α β ≃ PSum α' β'`. -/
def psumCongr ( e₁ : α ≃ β ) ( e₂ : γ ≃ δ ) : PSum : Sort ?u.12579 → Sort ?u.12578 → Sort (max(max1?u.12579)?u.12578) α γ ≃ PSum : Sort ?u.12581 → Sort ?u.12580 → Sort (max(max1?u.12581)?u.12580) β δ where
toFun x := PSum.casesOn : {α : Sort ?u.12599} →
{β : Sort ?u.12598} →
{motive : α ⊕' β Sort ?u.12600(t : α ⊕' β ((val : α ) → motive (PSum.inl val ) → ((val : β ) → motive (PSum.inr val ) → motive t x ( PSum.inl : {α : Sort ?u.12690} → {β : Sort ?u.12689} → α → α ⊕' β ∘ e₁ ) ( PSum.inr : {α : Sort ?u.12771} → {β : Sort ?u.12770} → β → α ⊕' β ∘ e₂ )
invFun x := PSum.casesOn : {α : Sort ?u.12641} →
{β : Sort ?u.12640} →
{motive : α ⊕' β Sort ?u.12642(t : α ⊕' β ((val : α ) → motive (PSum.inl val ) → ((val : β ) → motive (PSum.inr val ) → motive t x ( PSum.inl : {α : Sort ?u.12852} → {β : Sort ?u.12851} → α → α ⊕' β ∘ e₁ . symm : {α : Sort ?u.12859} → {β : Sort ?u.12858} → α ≃ β β ≃ α ) ( PSum.inr : {α : Sort ?u.12949} → {β : Sort ?u.12948} → β → α ⊕' β ∘ e₂ . symm : {α : Sort ?u.12956} → {β : Sort ?u.12955} → α ≃ β β ≃ α )
left_inv := by rintro ( x | x ) <;> simp
right_inv := by rintro ( x | x ) <;> simp
#align equiv.psum_congr Equiv.psumCongr : {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → {δ : Sort u_4} → α ≃ β γ ≃ δ α ⊕' γ ≃ β ⊕' δ
/-- Combine two `Equiv`s using `PSum` in the domain and `Sum` in the codomain. -/
def psumSum : {α₁ : Sort u_1} → {α₂ : Type u_2} → {β₁ : Sort u_3} → {β₂ : Type u_4} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕' β₁ ≃ α₂ ⊕ β₂ psumSum ( ea : α₁ ≃ α₂ ) ( eb : β₁ ≃ β₂ ) :
PSum : Sort ?u.16897 → Sort ?u.16896 → Sort (max(max1?u.16897)?u.16896) α₁ β₁ ≃ Sum : Type ?u.16899 → Type ?u.16898 → Type (max?u.16899?u.16898) α₂ β₂ :=
( ea . psumCongr : {α : Sort ?u.16910} → {β : Sort ?u.16909} → {γ : Sort ?u.16908} → {δ : Sort ?u.16907} → α ≃ β γ ≃ δ α ⊕' γ ≃ β ⊕' δ eb ). trans : {α : Sort ?u.16929} → {β : Sort ?u.16928} → {γ : Sort ?u.16927} → α ≃ β β ≃ γ α ≃ γ trans ( psumEquivSum : (α : Type ?u.16941) → (β : Type ?u.16940) → α ⊕' β ≃ α ⊕ β _ _ )
#align equiv.psum_sum Equiv.psumSum : {α₁ : Sort u_1} → {α₂ : Type u_2} → {β₁ : Sort u_3} → {β₂ : Type u_4} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕' β₁ ≃ α₂ ⊕ β₂
/-- Combine two `Equiv`s using `Sum` in the domain and `PSum` in the codomain. -/
def sumPSum : {α₁ : Type u_1} → {α₂ : Sort u_2} → {β₁ : Type u_3} → {β₂ : Sort u_4} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕ β₁ ≃ α₂ ⊕' β₂ sumPSum ( ea : α₁ ≃ α₂ ) ( eb : β₁ ≃ β₂ ) :
Sum : Type ?u.17122 → Type ?u.17121 → Type (max?u.17122?u.17121) α₁ β₁ ≃ PSum : Sort ?u.17124 → Sort ?u.17123 → Sort (max(max1?u.17124)?u.17123) α₂ β₂ :=
( ea . symm : {α : Sort ?u.17133} → {β : Sort ?u.17132} → α ≃ β β ≃ α . psumSum : {α₁ : Sort ?u.17141} →
{α₂ : Type ?u.17140} → {β₁ : Sort ?u.17139} → {β₂ : Type ?u.17138} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕' β₁ ≃ α₂ ⊕ β₂ eb . symm : {α : Sort ?u.17155} → {β : Sort ?u.17154} → α ≃ β β ≃ α ). symm : {α : Sort ?u.17168} → {β : Sort ?u.17167} → α ≃ β β ≃ α symm
#align equiv.sum_psum Equiv.sumPSum : {α₁ : Type u_1} → {α₂ : Sort u_2} → {β₁ : Type u_3} → {β₂ : Sort u_4} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕ β₁ ≃ α₂ ⊕' β₂
@[ simp ]
theorem sumCongr_trans ( e : α₁ ≃ β₁ ) ( f : α₂ ≃ β₂ ) ( g : β₁ ≃ γ₁ ) ( h : β₂ ≃ γ₂ ) :
( Equiv.sumCongr : {α₁ : Type ?u.17401} →
{α₂ : Type ?u.17400} → {β₁ : Type ?u.17399} → {β₂ : Type ?u.17398} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕ β₁ ≃ α₂ ⊕ β₂ e f ). trans : {α : Sort ?u.17412} → {β : Sort ?u.17411} → {γ : Sort ?u.17410} → α ≃ β β ≃ γ α ≃ γ trans ( Equiv.sumCongr : {α₁ : Type ?u.17426} →
{α₂ : Type ?u.17425} → {β₁ : Type ?u.17424} → {β₂ : Type ?u.17423} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕ β₁ ≃ α₂ ⊕ β₂ g h ) = Equiv.sumCongr : {α₁ : Type ?u.17444} →
{α₂ : Type ?u.17443} → {β₁ : Type ?u.17442} → {β₂ : Type ?u.17441} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕ β₁ ≃ α₂ ⊕ β₂ ( e . trans : {α : Sort ?u.17451} → {β : Sort ?u.17450} → {γ : Sort ?u.17449} → α ≃ β β ≃ γ α ≃ γ g ) ( f . trans : {α : Sort ?u.17468} → {β : Sort ?u.17467} → {γ : Sort ?u.17466} → α ≃ β β ≃ γ α ≃ γ h ) := by
ext i
cases i <;> rfl
#align equiv.sum_congr_trans Equiv.sumCongr_trans
@[ simp ]
theorem sumCongr_symm ( e : α ≃ β ) ( f : γ ≃ δ ) :
( Equiv.sumCongr : {α₁ : Type ?u.17722} →
{α₂ : Type ?u.17721} → {β₁ : Type ?u.17720} → {β₂ : Type ?u.17719} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕ β₁ ≃ α₂ ⊕ β₂ e f ). symm : {α : Sort ?u.17732} → {β : Sort ?u.17731} → α ≃ β β ≃ α symm = Equiv.sumCongr : {α₁ : Type ?u.17743} →
{α₂ : Type ?u.17742} → {β₁ : Type ?u.17741} → {β₂ : Type ?u.17740} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕ β₁ ≃ α₂ ⊕ β₂ e . symm : {α : Sort ?u.17749} → {β : Sort ?u.17748} → α ≃ β β ≃ α f . symm : {α : Sort ?u.17760} → {β : Sort ?u.17759} → α ≃ β β ≃ α :=
rfl : ∀ {α : Sort ?u.17780} {a : α }, a = a
#align equiv.sum_congr_symm Equiv.sumCongr_symm
@[ simp ]
theorem sumCongr_refl : Equiv.sumCongr : {α₁ : Type ?u.17932} →
{α₂ : Type ?u.17931} → {β₁ : Type ?u.17930} → {β₂ : Type ?u.17929} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕ β₁ ≃ α₂ ⊕ β₂ ( Equiv.refl : (α : Sort ?u.17937) → α ≃ α α ) ( Equiv.refl : (α : Sort ?u.17942) → α ≃ α β ) = Equiv.refl : (α : Sort ?u.17947) → α ≃ α ( Sum : Type ?u.17949 → Type ?u.17948 → Type (max?u.17949?u.17948) α β ) := by
ext i
cases i <;> rfl
#align equiv.sum_congr_refl Equiv.sumCongr_refl
namespace Perm
/-- Combine a permutation of `α` and of `β` into a permutation of `α ⊕ β`. -/
@[reducible]
def sumCongr ( ea : Equiv.Perm : Sort ?u.18111 → Sort (max1?u.18111) α ) ( eb : Equiv.Perm : Sort ?u.18114 → Sort (max1?u.18114) β ) : Equiv.Perm : Sort ?u.18117 → Sort (max1?u.18117) ( Sum : Type ?u.18119 → Type ?u.18118 → Type (max?u.18119?u.18118) α β ) :=
Equiv.sumCongr : {α₁ : Type ?u.18132} →
{α₂ : Type ?u.18131} → {β₁ : Type ?u.18130} → {β₂ : Type ?u.18129} → α₁ ≃ α₂ β₁ ≃ β₂ α₁ ⊕ β₁ ≃ α₂ ⊕ β₂ ea eb
#align equiv.perm.sum_congr Equiv.Perm.sumCongr
@[ simp ]
theorem sumCongr_apply ( ea : Equiv.Perm : Sort ?u.18236 → Sort (max1?u.18236) α ) ( eb : Equiv.Perm : Sort ?u.18247 → Sort (max1?u.18247) β ) ( x : Sum : Type ?u.18251 → Type ?u.18250 → Type (max?u.18251?u.18250) α β ) :
sumCongr ea eb x = Sum.map : {α : Type ?u.18334} →
{α' : Type ?u.18332} → {β : Type ?u.18333} → {β' : Type ?u.18331} → (α → α' (β → β' α ⊕ β α' ⊕ β' (⇑ ea ) (⇑ eb ) x :=
Equiv.sumCongr_apply ea eb x
#align equiv.perm.sum_congr_apply Equiv.Perm.sumCongr_apply
-- porting note: it seems the general theorem about `Equiv` is now applied, so there's no need
-- to have this version also have `@[simp]`. Similarly for below.
theorem sumCongr_trans ( e : Equiv.Perm : Sort ?u.18551 → Sort (max1?u.18551) α ) ( f : Equiv.Perm : Sort ?u.18562 → Sort (max1?u.18562) β ) ( g : Equiv.Perm : Sort ?u.18565 → Sort (max1?u.18565) α )
( h : Equiv.Perm : Sort ?u.18568 → Sort (max1?u.18568) β ) : ( sumCongr e f ). trans : {α : Sort ?u.18580} → {β : Sort ?u.18579} → {γ : Sort ?u.18578} → α ≃ β β ≃ γ α ≃ γ trans ( sumCongr g h ) = sumCongr ( e . trans : {α : Sort ?u.18605} → {β : Sort ?u.18604} → {γ : Sort ?u.18603} → α ≃ β β ≃ γ α ≃ γ g ) ( f . trans : {α : Sort ?u.18620} → {β : Sort ?u.18619} → {γ : Sort ?u.18618} → α ≃ β β ≃ γ α ≃ γ h ) :=
Equiv.sumCongr_trans e f g h
#align equiv.perm.sum_congr_trans Equiv.Perm.sumCongr_trans
theorem sumCongr_symm ( e : Equiv.Perm : Sort ?u.18681 → Sort (max1?u.18681) α ) ( f : Equiv.Perm : Sort ?u.18692 → Sort (max1?u.18692) β ) :
( sumCongr e f ). symm : {α : Sort ?u.18703} → {β : Sort ?u.18702} → α ≃ β β ≃ α symm = sumCongr e . symm : {α : Sort ?u.18716} → {β : Sort ?u.18715} → α ≃ β β ≃ α f . symm : {α : Sort ?u.18727} → {β : Sort ?u.18726} → α ≃ β β ≃ α :=
Equiv.sumCongr_symm e f
#align equiv.perm.sum_congr_symm Equiv.Perm.sumCongr_symm
theorem sumCongr_refl : sumCongr ( Equiv.refl : (α : Sort ?u.18794) → α ≃ α α ) ( Equiv.refl : (α : Sort ?u.18797) → α ≃ α β ) = Equiv.refl : (α : Sort ?u.18800) → α ≃ α ( Sum : Type ?u.18802 → Type ?u.18801 → Type (max?u.18802?u.18801) α β ) :=
Equiv.sumCongr_refl
#align equiv.perm.sum_congr_refl Equiv.Perm.sumCongr_refl
end Perm
/-- `Bool` is equivalent the sum of two `PUnit`s. -/
def boolEquivPUnitSumPUnit : Bool ≃ Sum : Type ?u.18829 → Type ?u.18828 → Type (max?u.18829?u.18828) PUnit .{u + 1} PUnit .{v + 1} :=
⟨ fun b => cond : {α : Type ?u.18846} → Bool → α → α → α b ( inr : {α : Type ?u.18849} → {β : Type ?u.18848} → β → α ⊕ β PUnit.unit ) ( inl : {α : Type ?u.18856} → {β : Type ?u.18855} → α → α ⊕ β PUnit.unit ), Sum.elim : {α : Type ?u.18864} → {β : Type ?u.18863} → {γ : Sort ?u.18862} → (α → γ (β → γ α ⊕ β γ ( fun _ => false ) fun _ => true ,
fun b => by cases b <;> rfl , fun s => by rcases s with ( ⟨ ⟨⟩ ⟩ | ⟨ ⟨⟩ ⟩ ) <;> rfl ⟩
#align equiv.bool_equiv_punit_sum_punit Equiv.boolEquivPUnitSumPUnit
/-- Sum of types is commutative up to an equivalence. This is `Sum.swap` as an equivalence. -/
@[ simps ( config := { fullyApplied := false }) apply ]
def sumComm : (α : Type u_1) → (β : Type u_2) → α ⊕ β ≃ β ⊕ α sumComm ( α β ) : Sum : Type ?u.19133 → Type ?u.19132 → Type (max?u.19133?u.19132) α β ≃ Sum : Type ?u.19135 → Type ?u.19134 → Type (max?u.19135?u.19134) β α :=
⟨ Sum.swap : {α : Type ?u.19152} → {β : Type ?u.19151} → α ⊕ β β ⊕ α , Sum.swap : {α : Type ?u.19163} → {β : Type ?u.19162} → α ⊕ β β ⊕ α , Sum.swap_swap , Sum.swap_swap ⟩
#align equiv.sum_comm Equiv.sumComm : (α : Type u_1) → (β : Type u_2) → α ⊕ β ≃ β ⊕ α
#align equiv.sum_comm_apply Equiv.sumComm_apply
@[ simp ]
theorem sumComm_symm ( α β ) : ( sumComm : (α : Type ?u.19336) → (β : Type ?u.19335) → α ⊕ β ≃ β ⊕ α α β ). symm : {α : Sort ?u.19338} → {β : Sort ?u.19337} → α ≃ β β ≃ α symm = sumComm : (α : Type ?u.19347) → (β : Type ?u.19346) → α ⊕ β ≃ β ⊕ α β α :=
rfl : ∀ {α : Sort ?u.19356} {a : α }, a = a
#align equiv.sum_comm_symm Equiv.sumComm_symm
/-- Sum of types is associative up to an equivalence. -/
def sumAssoc ( α β γ ) : Sum : Type ?u.19419 → Type ?u.19418 → Type (max?u.19419?u.19418) ( Sum : Type ?u.19421 → Type ?u.19420 → Type (max?u.19421?u.19420) α β ) γ ≃ Sum : Type ?u.19423 → Type ?u.19422 → Type (max?u.19423?u.19422) α ( Sum : Type ?u.19425 → Type ?u.19424 → Type (max?u.19425?u.19424) β γ ) :=
⟨ Sum.elim : {α : Type ?u.19444} → {β : Type ?u.19443} → {γ : Sort ?u.19442} → (α → γ (β → γ α ⊕ β γ ( Sum.elim : {α : Type ?u.19454} → {β : Type ?u.19453} → {γ : Sort ?u.19452} → (α → γ (β → γ α ⊕ β γ Sum.inl : {α : Type ?u.19463} → {β : Type ?u.19462} → α → α ⊕ β ( Sum.inr : {α : Type ?u.19480} → {β : Type ?u.19479} → β → α ⊕ β ∘ Sum.inl : {α : Type ?u.19487} → {β : Type ?u.19486} → α → α ⊕ β )) ( Sum.inr : {α : Type ?u.19510} → {β : Type ?u.19509} → β → α ⊕ β ∘ Sum.inr : {α : Type ?u.19517} → {β : Type ?u.19516} → β → α ⊕ β ),
Sum.elim : {α : Type ?u.19531} → {β : Type ?u.19530} → {γ : Sort ?u.19529} → (α → γ (β → γ α ⊕ β γ ( Sum.inl : {α : Type ?u.19546} → {β : Type ?u.19545} → α → α ⊕ β ∘ Sum.inl : {α : Type ?u.19553} → {β : Type ?u.19552} → α → α ⊕ β ) <| Sum.elim : {α : Type ?u.19564} → {β : Type ?u.19563} → {γ : Sort ?u.19562} → (α → γ (β → γ α ⊕ β γ ( Sum.inl : {α : Type ?u.19579} → {β : Type ?u.19578} → α → α ⊕ β ∘ Sum.inr : {α : Type ?u.19586} → {β : Type ?u.19585} → β → α ⊕ β ) Sum.inr : {α : Type ?u.19596} → {β : Type ?u.19595} → β → α ⊕ β ,
by rintro (⟨_ | _⟩ | _) : (α ⊕ β ⊕ γ ⟨ _ | _ ⟩ | _ (⟨_ | _⟩ | _) : (α ⊕ β ⊕ γ <;> rfl , by
rintro ( _ | ⟨ _ | _ ⟩ ) <;> rfl ⟩
#align equiv.sum_assoc Equiv.sumAssoc : (α : Type u_1) → (β : Type u_2) → (γ : Type u_3) → (α ⊕ β ⊕ γ ≃ α ⊕ β ⊕ γ
@[ simp ]
theorem sumAssoc_apply_inl_inl ( a : unknown metavariable '?_uniq.19929'
a ) : sumAssoc : (α : Type ?u.19946) → (β : Type ?u.19945) → (γ : Type ?u.19944) → (α ⊕ β ⊕ γ ≃ α ⊕ β ⊕ γ α β γ ( inl : {α : Type ?u.20019} → {β : Type ?u.20018} → α → α ⊕ β ( inl : {α : Type ?u.20025} → {β : Type ?u.20024} → α → α ⊕ β a )) = inl : {α : Type ?u.20031} → {β : Type ?u.20030} → α → α ⊕ β a :=
rfl : ∀ {α : Sort ?u.20076} {a : α }, a = a
#align equiv.sum_assoc_apply_inl_inl Equiv.sumAssoc_apply_inl_inl
@[ simp ]
theorem sumAssoc_apply_inl_inr ( b : unknown metavariable '?_uniq.20150'
b ) : sumAssoc : (α : Type ?u.20167) → (β : Type ?u.20166) → (γ : Type ?u.20165) → (α ⊕ β ⊕ γ ≃ α ⊕ β ⊕ γ α β γ ( inl : {α : Type ?u.20240} → {β : Type ?u.20239} → α → α ⊕ β ( inr : {α : Type ?u.20246} → {β : Type ?u.20245} → β → α ⊕ β b )) = inr : {α : Type ?u.20252} → {β : Type ?u.20251} → β → α ⊕ β ( inl : {α : Type ?u.20256} → {β : Type ?u.20255} → α → α ⊕ β b ) :=
rfl : ∀ {α : Sort ?u.20303} {a : α }, a = a
#align equiv.sum_assoc_apply_inl_inr Equiv.sumAssoc_apply_inl_inr
@[ simp ]
theorem sumAssoc_apply_inr ( c : unknown metavariable '?_uniq.20366'
c ) : sumAssoc : (α : Type ?u.20394) → (β : Type ?u.20393) → (γ : Type ?u.20392) → (α ⊕ β ⊕ γ ≃ α ⊕ β ⊕ γ α β γ ( inr : {α : Type ?u.20467} → {β : Type ?u.20466} → β → α ⊕ β c ) = inr : {α : Type ?u.20473} → {β : Type ?u.20472} → β → α ⊕ β ( inr : {α : Type ?u.20477} → {β : Type ?u.20476} → β → α ⊕ β c ) :=
rfl : ∀ {α : Sort ?u.20524} {a : α }, a = a
#align equiv.sum_assoc_apply_inr Equiv.sumAssoc_apply_inr
@[ simp ]
theorem sumAssoc_symm_apply_inl { α β γ } ( a ) : ( sumAssoc : (α : Type ?u.20588) → (β : Type ?u.20587) → (γ : Type ?u.20586) → (α ⊕ β ⊕ γ ≃ α ⊕ β ⊕ γ α β γ ). symm : {α : Sort ?u.20590} → {β : Sort ?u.20589} → α ≃ β β ≃ α symm ( inl : {α : Type ?u.20668} → {β : Type ?u.20667} → α → α ⊕ β a ) = inl : {α : Type ?u.20674} → {β : Type ?u.20673} → α → α ⊕ β ( inl : {α : Type ?u.20678} → {β : Type ?u.20677} → α → α ⊕ β a ) :=
rfl : ∀ {α : Sort ?u.20731} {a : α }, a = a
#align equiv.sum_assoc_symm_apply_inl Equiv.sumAssoc_symm_apply_inl
@[ simp ]
theorem sumAssoc_symm_apply_inr_inl { α β γ } ( b ) :
( sumAssoc : (α : Type ?u.20798) → (β : Type ?u.20797) → (γ : Type ?u.20796) → (α ⊕ β ⊕ γ ≃ α ⊕ β ⊕ γ α β γ ). symm : {α : Sort ?u.20800} → {β : Sort ?u.20799} → α ≃ β β ≃ α symm ( inr : {α : Type ?u.20878} → {β : Type ?u.20877} → β → α ⊕ β ( inl : {α : Type ?u.20884} → {β : Type ?u.20883} → α → α ⊕ β b )) = inl : {α : Type ?u.20890} → {β : Type ?u.20889} → α → α ⊕ β ( inr : {α : Type ?u.20894} → {β : Type ?u.20893} → β → α ⊕ β b ) :=
rfl : ∀ {α : Sort ?u.20947} {a : α }, a = a
#align equiv.sum_assoc_symm_apply_inr_inl Equiv.sumAssoc_symm_apply_inr_inl
@[ simp ]
theorem sumAssoc_symm_apply_inr_inr { α β γ } ( c ) : ( sumAssoc : (α : Type ?u.21017) → (β : Type ?u.21016) → (γ : Type ?u.21015) → (α ⊕ β ⊕ γ ≃ α ⊕ β ⊕ γ α β γ ). symm : {α : Sort ?u.21019} → {β : Sort ?u.21018} → α ≃ β β ≃ α symm ( inr : {α : Type ?u.21097} → {β : Type ?u.21096} → β → α ⊕ β ( inr : {α : Type ?u.21103} → {β : Type ?u.21102} → β → α ⊕ β c )) = inr : {α : Type ?u.21109} → {β : Type ?u.21108} → β → α ⊕ β c :=
rfl : ∀ {α : Sort ?u.21154} {a : α }, a = a
#align equiv.sum_assoc_symm_apply_inr_inr Equiv.sumAssoc_symm_apply_inr_inr
/-- Sum with `IsEmpty` is equivalent to the original type. -/
@[ simps symm_apply ]
def sumEmpty ( α β ) [ IsEmpty β ] : Sum : Type ?u.21221 → Type ?u.21220 → Type (max?u.21221?u.21220) α β ≃ α where
toFun := Sum.elim : {α : Type ?u.21234} → {β : Type ?u.21233} → {γ : Sort ?u.21232} → (α → γ (β → γ α ⊕ β γ id : {α : Sort ?u.21242} → α → α isEmptyElim : {α : Sort ?u.21248} → [inst : IsEmpty α {p : α → Sort ?u.21247(a : α ) → p a
invFun := inl : {α : Type ?u.21295} → {β : Type ?u.21294} → α → α ⊕ β
left_inv s := by
rcases s with ( _ | x )
· rfl
· exact isEmptyElim : ∀ {α : Sort ?u.21363} [inst : IsEmpty α p : α → Sort ?u.21362a : α ), p a x
right_inv _ := rfl : ∀ {α : Sort ?u.21310} {a : α }, a = a
#align equiv.sum_empty Equiv.sumEmpty
#align equiv.sum_empty_symm_apply Equiv.sumEmpty_symm_apply
@[ simp ]
theorem sumEmpty_apply_inl [ IsEmpty β ] ( a : α ) : sumEmpty α β ( Sum.inl : {α : Type ?u.21563} → {β : Type ?u.21562} → α → α ⊕ β a ) = a :=
rfl : ∀ {α : Sort ?u.21575} {a : α }, a = a
#align equiv.sum_empty_apply_inl Equiv.sumEmpty_apply_inl
/-- The sum of `IsEmpty` with any type is equivalent to that type. -/
@[ simps! symm_apply ]
def emptySum ( α β ) [ IsEmpty α ] : Sum : Type ?u.21627 → Type ?u.21626 → Type (max?u.21627?u.21626) α β ≃ β :=
( sumComm : (α : Type ?u.21633) → (β : Type ?u.21632) → α ⊕ β ≃ β ⊕ α _ _ ). trans : {α : Sort ?u.21638} → {β : Sort ?u.21637} → {γ : Sort ?u.21636} → α ≃ β β ≃ γ α ≃ γ trans <| sumEmpty _ _
#align equiv.empty_sum Equiv.emptySum
#align equiv.empty_sum_symm_apply Equiv.emptySum_symm_apply
@[ simp ]
theorem emptySum_apply_inr [ IsEmpty α ] ( b : β ) : emptySum α β ( Sum.inr : {α : Type ?u.21936} → {β : Type ?u.21935} → β → α ⊕ β b ) = b :=
rfl : ∀ {α : Sort ?u.21948} {a : α }, a = a
#align equiv.empty_sum_apply_inr Equiv.emptySum_apply_inr
/-- `Option α` is equivalent to `α ⊕ PUnit` -/
def optionEquivSumPUnit ( α ) : Option α ≃ Sum : Type ?u.21995 → Type ?u.21994 → Type (max?u.21995?u.21994) α PUnit :=
⟨ fun o => o . elim : {α : Type ?u.22015} → {β : Sort ?u.22014} → Option α β → (α → β β ( inr : {α : Type ?u.22025} → {β : Type ?u.22024} → β → α ⊕ β PUnit.unit ) inl : {α : Type ?u.22032} → {β : Type ?u.22031} → α → α ⊕ β , fun s => s . elim : {α : Type ?u.22045} → {β : Type ?u.22044} → {γ : Sort ?u.22043} → (α → γ (β → γ α ⊕ β γ some fun _ => none ,
fun o => by cases o <;> rfl ,
fun s => by rcases s with ( _ | ⟨ ⟨⟩ ⟩ ) <;> rfl ⟩
#align equiv.option_equiv_sum_punit Equiv.optionEquivSumPUnit
@[ simp ]
theorem optionEquivSumPUnit_none : optionEquivSumPUnit α none = Sum.inr : {α : Type ?u.22439} → {β : Type ?u.22438} → β → α ⊕ β PUnit.unit :=
rfl : ∀ {α : Sort ?u.22482} {a : α }, a = a
#align equiv.option_equiv_sum_punit_none Equiv.optionEquivSumPUnit_none
@[ simp ]
theorem optionEquivSumPUnit_some ( a ) : optionEquivSumPUnit α ( some a ) = Sum.inl : {α : Type ?u.22612} → {β : Type ?u.22611} → α → α ⊕ β a :=
rfl : ∀ {α : Sort ?u.22655} {a : α }, a = a
#align equiv.option_equiv_sum_punit_some Equiv.optionEquivSumPUnit_some
@[ simp ]
theorem optionEquivSumPUnit_coe ( a : α ) : optionEquivSumPUnit α a = Sum.inl : {α : Type ?u.22861} → {β : Type ?u.22860} → α → α ⊕ β a :=
rfl : ∀ {α : Sort ?u.22904} {a : α }, a = a
#align equiv.option_equiv_sum_punit_coe Equiv.optionEquivSumPUnit_coe
@[ simp ]
theorem optionEquivSumPUnit_symm_inl ( a ) : ( optionEquivSumPUnit α ). symm : {α : Sort ?u.22968} → {β : Sort ?u.22967} → α ≃ β β ≃ α symm ( Sum.inl : {α : Type ?u.23040} → {β : Type ?u.23039} → α → α ⊕ β a ) = a :=
rfl : ∀ {α : Sort ?u.23221} {a : α }, a = a
#align equiv.option_equiv_sum_punit_symm_inl Equiv.optionEquivSumPUnit_symm_inl
@[ simp ]
theorem optionEquivSumPUnit_symm_inr ( a ) : ( optionEquivSumPUnit α ). symm : {α : Sort ?u.23274} → {β : Sort ?u.23273} → α ≃ β β ≃ α symm ( Sum.inr : {α : Type ?u.23346} → {β : Type ?u.23345} → β → α ⊕ β a ) = none :=
rfl : ∀ {α : Sort ?u.23389} {a : α }, a = a
#align equiv.option_equiv_sum_punit_symm_inr Equiv.optionEquivSumPUnit_symm_inr
/-- The set of `x : Option α` such that `isSome x` is equivalent to `α`. -/
@[ simps ]
def optionIsSomeEquiv ( α ) : { x : Option α // x . isSome } ≃ α where
toFun o := Option.get _ o . 2
invFun x := ⟨ some x , rfl : ∀ {α : Sort ?u.23564} {a : α }, a = a ⟩
left_inv _ := Subtype.eq : ∀ {α : Type ?u.23586} {p : α → Prop a1 a2 : { x // p x }, ↑a1 = ↑a2 a1 = a2 <|