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 Cmdinstead of Ctrl.
```/-
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.fst, x.snd)apply symm_apply: ∀ {α : Type u_1} {β : Type u_2} (x : α × β), ↑pprodEquivProd.symm x = { fst := x.fst, snd := x.snd }symm_apply]
def pprodEquivProd: {α : Type u_1} → {β : Type u_2} → PProd α β ≃ α × βpprodEquivProd : PProd: Sort ?u.21 → Sort ?u.20 → Sort (max(max1?u.21)?u.20)PProd α: ?m.7α β: ?m.15β ≃ α: ?m.7α × β: ?m.15β where
toFun x: ?m.34x := (x: ?m.34x.1: {α : Sort ?u.43} → {β : Sort ?u.42} → PProd α β → α1, x: ?m.34x.2: {α : Sort ?u.49} → {β : Sort ?u.48} → PProd α β → β2)
invFun x: ?m.55x := ⟨x: ?m.55x.1: {α : Type ?u.66} → {β : Type ?u.65} → α × β → α1, x: ?m.55x.2: {α : Type ?u.70} → {β : Type ?u.69} → α × β → β2⟩
left_inv := fun _: ?m.76_ => rfl: ∀ {α : Sort ?u.78} {a : α}, a = arfl
right_inv := fun _: ?m.88_ => rfl: ∀ {α : Sort ?u.90} {a : α}, a = arfl
#align equiv.pprod_equiv_prod Equiv.pprodEquivProd: {α : Type u_1} → {β : Type u_2} → PProd α β ≃ α × βEquiv.pprodEquivProd
#align equiv.pprod_equiv_prod_apply Equiv.pprodEquivProd_apply: ∀ {α : Type u_1} {β : Type u_2} (x : PProd α β), ↑pprodEquivProd x = (x.fst, x.snd)Equiv.pprodEquivProd_apply
#align equiv.pprod_equiv_prod_symm_apply Equiv.pprodEquivProd_symm_apply: ∀ {α : Type u_1} {β : Type u_2} (x : α × β), ↑pprodEquivProd.symm x = { fst := x.fst, snd := x.snd }Equiv.pprodEquivProd_symm_apply

/-- 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 }apply]
def pprodCongr: {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → {δ : Sort u_4} → α ≃ β → γ ≃ δ → PProd α γ ≃ PProd β δpprodCongr (e₁: α ≃ βe₁ : α: ?m.370α ≃ β: ?m.376β) (e₂: γ ≃ δe₂ : γ: ?m.386γ ≃ δ: ?m.396δ) : PProd: Sort ?u.410 → Sort ?u.409 → Sort (max(max1?u.410)?u.409)PProd α: ?m.370α γ: ?m.386γ ≃ PProd: Sort ?u.412 → Sort ?u.411 → Sort (max(max1?u.412)?u.411)PProd β: ?m.376β δ: ?m.396δ where
toFun x: ?m.427x := ⟨e₁: α ≃ βe₁ x: ?m.427x.1: {α : Sort ?u.501} → {β : Sort ?u.500} → PProd α β → α1, e₂: γ ≃ δe₂ x: ?m.427x.2: {α : Sort ?u.568} → {β : Sort ?u.567} → PProd α β → β2⟩
invFun x: ?m.574x := ⟨e₁: α ≃ βe₁.symm: {α : Sort ?u.585} → {β : Sort ?u.584} → α ≃ β → β ≃ αsymm x: ?m.574x.1: {α : Sort ?u.662} → {β : Sort ?u.661} → PProd α β → α1, e₂: γ ≃ δe₂.symm: {α : Sort ?u.666} → {β : Sort ?u.665} → α ≃ β → β ≃ αsymm x: ?m.574x.2: {α : Sort ?u.743} → {β : Sort ?u.742} → PProd α β → β2⟩
left_inv := fun ⟨x: αx, y: γy⟩ => byGoals accomplished! 🐙 α: Sort ?u.400β: Sort ?u.399γ: Sort ?u.404δ: Sort ?u.403e₁: α ≃ βe₂: γ ≃ δx✝: PProd α γx: αy: γ(fun x => { fst := ↑e₁.symm x.fst, snd := ↑e₂.symm x.snd })
((fun x => { fst := ↑e₁ x.fst, snd := ↑e₂ x.snd }) { fst := x, snd := y }) =   { fst := x, snd := y }simpGoals accomplished! 🐙
right_inv := fun ⟨x: βx, y: δy⟩ => byGoals accomplished! 🐙 α: Sort ?u.400β: Sort ?u.399γ: Sort ?u.404δ: Sort ?u.403e₁: α ≃ βe₂: γ ≃ δx✝: PProd β δx: βy: δ(fun x => { fst := ↑e₁ x.fst, snd := ↑e₂ x.snd })
((fun x => { fst := ↑e₁.symm x.fst, snd := ↑e₂.symm x.snd }) { fst := x, snd := y }) =   { fst := x, snd := y }simpGoals accomplished! 🐙
#align equiv.pprod_congr Equiv.pprodCongr: {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → {δ : Sort u_4} → α ≃ β → γ ≃ δ → PProd α γ ≃ PProd β δ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 }Equiv.pprodCongr_apply

/-- 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)apply symm_apply: ∀ {α₁ : Sort u_1} {α₂ : Type u_2} {β₁ : Sort u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (a : α₂ × β₂),
↑(pprodProd ea eb).symm a = ↑(pprodCongr ea eb).symm { fst := a.fst, snd := a.snd }symm_apply]
def pprodProd: {α₁ : Sort u_1} → {α₂ : Type u_2} → {β₁ : Sort u_3} → {β₂ : Type u_4} → α₁ ≃ α₂ → β₁ ≃ β₂ → PProd α₁ β₁ ≃ α₂ × β₂pprodProd (ea: α₁ ≃ α₂ea : α₁: ?m.1894α₁ ≃ α₂: ?m.1900α₂) (eb: β₁ ≃ β₂eb : β₁: ?m.1910β₁ ≃ β₂: ?m.1920β₂) :
PProd: Sort ?u.1934 → Sort ?u.1933 → Sort (max(max1?u.1934)?u.1933)PProd α₁: ?m.1894α₁ β₁: ?m.1910β₁ ≃ α₂: ?m.1900α₂ × β₂: ?m.1920β₂ :=
(ea: α₁ ≃ α₂ea.pprodCongr: {α : Sort ?u.1947} →
{β : Sort ?u.1946} → {γ : Sort ?u.1945} → {δ : Sort ?u.1944} → α ≃ β → γ ≃ δ → PProd α γ ≃ PProd β δpprodCongr eb: β₁ ≃ β₂eb).trans: {α : Sort ?u.1966} → {β : Sort ?u.1965} → {γ : Sort ?u.1964} → α ≃ β → β ≃ γ → α ≃ γtrans pprodEquivProd: {α : Type ?u.1978} → {β : Type ?u.1977} → PProd α β ≃ α × βpprodEquivProd
#align equiv.pprod_prod Equiv.pprodProd: {α₁ : Sort u_1} → {α₂ : Type u_2} → {β₁ : Sort u_3} → {β₂ : Type u_4} → α₁ ≃ α₂ → β₁ ≃ β₂ → PProd α₁ β₁ ≃ α₂ × β₂Equiv.pprodProd
#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)Equiv.pprodProd_apply
#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).symm a = ↑(pprodCongr ea eb).symm { fst := a.fst, snd := a.snd }Equiv.pprodProd_symm_apply

/-- 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.symm eb.symm).symm { fst := a.fst, snd := a.snd }apply symm_apply: ∀ {α₁ : Type u_1} {α₂ : Sort u_2} {β₁ : Type u_3} {β₂ : Sort u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (a : PProd α₂ β₂),
↑(prodPProd ea eb).symm a = (↑ea.symm a.fst, ↑eb.symm a.snd)symm_apply]
def prodPProd: {α₁ : Type u_1} → {α₂ : Sort u_2} → {β₁ : Type u_3} → {β₂ : Sort u_4} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ × β₁ ≃ PProd α₂ β₂prodPProd (ea: α₁ ≃ α₂ea : α₁: ?m.2558α₁ ≃ α₂: ?m.2564α₂) (eb: β₁ ≃ β₂eb : β₁: ?m.2574β₁ ≃ β₂: ?m.2584β₂) :
α₁: ?m.2558α₁ × β₁: ?m.2574β₁ ≃ PProd: Sort ?u.2600 → Sort ?u.2599 → Sort (max(max1?u.2600)?u.2599)PProd α₂: ?m.2564α₂ β₂: ?m.2584β₂ :=
(ea: α₁ ≃ α₂ea.symm: {α : Sort ?u.2609} → {β : Sort ?u.2608} → α ≃ β → β ≃ αsymm.pprodProd: {α₁ : Sort ?u.2617} →
{α₂ : Type ?u.2616} → {β₁ : Sort ?u.2615} → {β₂ : Type ?u.2614} → α₁ ≃ α₂ → β₁ ≃ β₂ → PProd α₁ β₁ ≃ α₂ × β₂pprodProd eb: β₁ ≃ β₂eb.symm: {α : Sort ?u.2631} → {β : Sort ?u.2630} → α ≃ β → β ≃ αsymm).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 α₂ β₂Equiv.prodPProd
#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).symm a = (↑ea.symm a.fst, ↑eb.symm a.snd)Equiv.prodPProd_symm_apply
#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.symm eb.symm).symm { fst := a.fst, snd := a.snd }Equiv.prodPProd_apply

/-- `PProd α β` is equivalent to `PLift α × PLift β` -/
@[simps! apply: ∀ {α : Sort u_1} {β : Sort u_2} (a : PProd α β),
↑pprodEquivProdPLift a = (↑Equiv.plift.symm a.fst, ↑Equiv.plift.symm a.snd)apply symm_apply: ∀ {α : Sort u_1} {β : Sort u_2} (a : PLift α × PLift β),
↑pprodEquivProdPLift.symm a = ↑(pprodCongr Equiv.plift.symm Equiv.plift.symm).symm { fst := a.fst, snd := a.snd }symm_apply]
def pprodEquivProdPLift: {α : Sort u_1} → {β : Sort u_2} → PProd α β ≃ PLift α × PLift βpprodEquivProdPLift : PProd: Sort ?u.3242 → Sort ?u.3241 → Sort (max(max1?u.3242)?u.3241)PProd α: ?m.3228α β: ?m.3236β ≃ PLift: Sort ?u.3245 → Type ?u.3245PLift α: ?m.3228α × PLift: Sort ?u.3246 → Type ?u.3246PLift β: ?m.3236β :=
Equiv.plift: {α : Sort ?u.3250} → PLift α ≃ αEquiv.plift.symm: {α : Sort ?u.3253} → {β : Sort ?u.3252} → α ≃ β → β ≃ αsymm.pprodProd: {α₁ : Sort ?u.3261} →
{α₂ : Type ?u.3260} → {β₁ : Sort ?u.3259} → {β₂ : Type ?u.3258} → α₁ ≃ α₂ → β₁ ≃ β₂ → PProd α₁ β₁ ≃ α₂ × β₂pprodProd Equiv.plift: {α : Sort ?u.3280} → PLift α ≃ αEquiv.plift.symm: {α : Sort ?u.3283} → {β : Sort ?u.3282} → α ≃ β → β ≃ αsymm
#align equiv.pprod_equiv_prod_plift Equiv.pprodEquivProdPLift: {α : Sort u_1} → {β : Sort u_2} → PProd α β ≃ PLift α × 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.symm a = ↑(pprodCongr Equiv.plift.symm Equiv.plift.symm).symm { fst := a.fst, snd := a.snd }Equiv.pprodEquivProdPLift_symm_apply
#align equiv.pprod_equiv_prod_plift_apply Equiv.pprodEquivProdPLift_apply: ∀ {α : Sort u_1} {β : Sort u_2} (a : PProd α β),
↑pprodEquivProdPLift a = (↑Equiv.plift.symm a.fst, ↑Equiv.plift.symm a.snd)Equiv.pprodEquivProdPLift_apply

/-- 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: Simps.Config.asFn) apply: ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂),
↑(prodCongr e₁ e₂) = Prod.map ↑e₁ ↑e₂apply]
def prodCongr: {α₁ : Type ?u.3881} →
{α₂ : Type ?u.3883} → {β₁ : Type ?u.3880} → {β₂ : Type ?u.3882} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ × β₁ ≃ α₂ × β₂prodCongr (e₁: α₁ ≃ α₂e₁ : α₁: ?m.3841α₁ ≃ α₂: ?m.3847α₂) (e₂: β₁ ≃ β₂e₂ : β₁: ?m.3857β₁ ≃ β₂: ?m.3867β₂) : α₁: ?m.3841α₁ × β₁: ?m.3857β₁ ≃ α₂: ?m.3847α₂ × β₂: ?m.3867β₂ :=
⟨Prod.map: {α₁ : Type ?u.3906} →
{α₂ : Type ?u.3905} → {β₁ : Type ?u.3904} → {β₂ : Type ?u.3903} → (α₁ → α₂) → (β₁ → β₂) → α₁ × β₁ → α₂ × β₂Prod.map e₁: α₁ ≃ α₂e₁ e₂: β₁ ≃ β₂e₂, Prod.map: {α₁ : Type ?u.4059} →
{α₂ : Type ?u.4058} → {β₁ : Type ?u.4057} → {β₂ : Type ?u.4056} → (α₁ → α₂) → (β₁ → β₂) → α₁ × β₁ → α₂ × β₂Prod.map e₁: α₁ ≃ α₂e₁.symm: {α : Sort ?u.4067} → {β : Sort ?u.4066} → α ≃ β → β ≃ αsymm e₂: β₁ ≃ β₂e₂.symm: {α : Sort ?u.4141} → {β : Sort ?u.4140} → α ≃ β → β ≃ αsymm, fun ⟨a: α₁a, b: β₁b⟩ => byGoals accomplished! 🐙 α₁: Type ?u.3881α₂: Type ?u.3883β₁: Type ?u.3880β₂: Type ?u.3882e₁: α₁ ≃ α₂e₂: β₁ ≃ β₂x✝: α₁ × β₁a: α₁b: β₁Prod.map (↑e₁.symm) (↑e₂.symm) (Prod.map ↑e₁ ↑e₂ (a, b)) = (a, b)simpGoals accomplished! 🐙, fun ⟨a: α₂a, b: β₂b⟩ => byGoals accomplished! 🐙 α₁: Type ?u.3881α₂: Type ?u.3883β₁: Type ?u.3880β₂: Type ?u.3882e₁: α₁ ≃ α₂e₂: β₁ ≃ β₂x✝: α₂ × β₂a: α₂b: β₂Prod.map (↑e₁) (↑e₂) (Prod.map ↑e₁.symm ↑e₂.symm (a, b)) = (a, b)simpGoals accomplished! 🐙⟩
#align equiv.prod_congr Equiv.prodCongr: {α₁ : Type u_1} → {α₂ : Type u_2} → {β₁ : Type u_3} → {β₂ : Type u_4} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ × β₁ ≃ α₂ × β₂Equiv.prodCongr
#align equiv.prod_congr_apply Equiv.prodCongr_apply: ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂),
↑(prodCongr e₁ e₂) = Prod.map ↑e₁ ↑e₂Equiv.prodCongr_apply

@[simp]
theorem prodCongr_symm: ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂),
(prodCongr e₁ e₂).symm = prodCongr e₁.symm e₂.symmprodCongr_symm (e₁: α₁ ≃ α₂e₁ : α₁: ?m.5641α₁ ≃ α₂: ?m.5647α₂) (e₂: β₁ ≃ β₂e₂ : β₁: ?m.5657β₁ ≃ β₂: ?m.5667β₂) :
(prodCongr: {α₁ : Type ?u.5682} →
{α₂ : Type ?u.5681} → {β₁ : Type ?u.5680} → {β₂ : Type ?u.5679} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ × β₁ ≃ α₂ × β₂prodCongr e₁: α₁ ≃ α₂e₁ e₂: β₁ ≃ β₂e₂).symm: {α : Sort ?u.5692} → {β : Sort ?u.5691} → α ≃ β → β ≃ αsymm = prodCongr: {α₁ : Type ?u.5703} →
{α₂ : Type ?u.5702} → {β₁ : Type ?u.5701} → {β₂ : Type ?u.5700} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ × β₁ ≃ α₂ × β₂prodCongr e₁: α₁ ≃ α₂e₁.symm: {α : Sort ?u.5709} → {β : Sort ?u.5708} → α ≃ β → β ≃ αsymm e₂: β₁ ≃ β₂e₂.symm: {α : Sort ?u.5720} → {β : Sort ?u.5719} → α ≃ β → β ≃ αsymm :=
rfl: ∀ {α : Sort ?u.5740} {a : α}, a = arfl
#align equiv.prod_congr_symm Equiv.prodCongr_symm: ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ ≃ α₂) (e₂ : β₁ ≃ β₂),
(prodCongr e₁ e₂).symm = prodCongr e₁.symm e₂.symmEquiv.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 (α: Type ?u.5832α β: Type ?u.5831β) : α: ?m.5823α × β: ?m.5826β ≃ β: ?m.5826β × α: ?m.5823α :=
⟨Prod.swap: {α : Type ?u.5851} → {β : Type ?u.5850} → α × β → β × αProd.swap, Prod.swap: {α : Type ?u.5862} → {β : Type ?u.5861} → α × β → β × αProd.swap, Prod.swap_swap: ∀ {α : Type ?u.5868} {β : Type ?u.5869} (x : α × β), Prod.swap (Prod.swap x) = xProd.swap_swap, Prod.swap_swap: ∀ {α : Type ?u.5881} {β : Type ?u.5882} (x : α × β), Prod.swap (Prod.swap x) = xProd.swap_swap⟩
#align equiv.prod_comm Equiv.prodComm: (α : Type u_1) → (β : Type u_2) → α × β ≃ β × αEquiv.prodComm

@[simp]
theorem coe_prodComm: ∀ (α : Type u_1) (β : Type u_2), ↑(prodComm α β) = Prod.swapcoe_prodComm (α: Type u_1α β: ?m.5980β) : (⇑(prodComm: (α : Type ?u.5992) → (β : Type ?u.5991) → α × β ≃ β × αprodComm α: ?m.5977α β: ?m.5980β) : α: ?m.5977α × β: ?m.5980β → β: ?m.5980β × α: ?m.5977α) = Prod.swap: {α : Type ?u.6067} → {β : Type ?u.6066} → α × β → β × αProd.swap :=
rfl: ∀ {α : Sort ?u.6124} {a : α}, a = arfl
#align equiv.coe_prod_comm Equiv.coe_prodComm: ∀ (α : Type u_1) (β : Type u_2), ↑(prodComm α β) = Prod.swapEquiv.coe_prodComm

@[simp]
theorem prodComm_apply: ∀ {α : Type u_1} {β : Type u_2} (x : α × β), ↑(prodComm α β) x = Prod.swap xprodComm_apply (x: α × βx : α: ?m.6165α × β: ?m.6171β) : prodComm: (α : Type ?u.6180) → (β : Type ?u.6179) → α × β ≃ β × αprodComm α: ?m.6165α β: ?m.6171β x: α × βx = x: α × βx.swap: {α : Type ?u.6252} → {β : Type ?u.6251} → α × β → β × αswap :=
rfl: ∀ {α : Sort ?u.6268} {a : α}, a = arfl
#align equiv.prod_comm_apply Equiv.prodComm_apply: ∀ {α : Type u_1} {β : Type u_2} (x : α × β), ↑(prodComm α β) x = Prod.swap xEquiv.prodComm_apply

@[simp]
theorem prodComm_symm: ∀ (α : Type u_1) (β : Type u_2), (prodComm α β).symm = prodComm β αprodComm_symm (α: Type u_1α β: Type u_2β) : (prodComm: (α : Type ?u.6314) → (β : Type ?u.6313) → α × β ≃ β × αprodComm α: ?m.6306α β: ?m.6309β).symm: {α : Sort ?u.6316} → {β : Sort ?u.6315} → α ≃ β → β ≃ αsymm = prodComm: (α : Type ?u.6325) → (β : Type ?u.6324) → α × β ≃ β × αprodComm β: ?m.6309β α: ?m.6306α :=
rfl: ∀ {α : Sort ?u.6334} {a : α}, a = arfl
#align equiv.prod_comm_symm Equiv.prodComm_symm: ∀ (α : Type u_1) (β : Type u_2), (prodComm α β).symm = prodComm β αEquiv.prodComm_symm

/-- Type product is associative up to an equivalence. -/
@[simps: ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : α × β × γ),
↑(prodAssoc α β γ).symm p = ((p.fst, p.snd.fst), p.snd.snd)simps]
def prodAssoc: (α : Type ?u.6397) → (β : Type ?u.6396) → (γ : Type ?u.6394) → (α × β) × γ ≃ α × β × γprodAssoc (α: Type ?u.6397α β: Type ?u.6396β γ: ?m.6389γ) : (α: ?m.6383α × β: ?m.6386β) × γ: ?m.6389γ ≃ α: ?m.6383α × β: ?m.6386β × γ: ?m.6389γ :=
⟨fun p: ?m.6419p => (p: ?m.6419p.1: {α : Type ?u.6428} → {β : Type ?u.6427} → α × β → α1.1: {α : Type ?u.6434} → {β : Type ?u.6433} → α × β → α1, p: ?m.6419p.1: {α : Type ?u.6446} → {β : Type ?u.6445} → α × β → α1.2: {α : Type ?u.6450} → {β : Type ?u.6449} → α × β → β2, p: ?m.6419p.2: {α : Type ?u.6454} → {β : Type ?u.6453} → α × β → β2), fun p: ?m.6460p => ((p: ?m.6460p.1: {α : Type ?u.6471} → {β : Type ?u.6470} → α × β → α1, p: ?m.6460p.2: {α : Type ?u.6475} → {β : Type ?u.6474} → α × β → β2.1: {α : Type ?u.6479} → {β : Type ?u.6478} → α × β → α1), p: ?m.6460p.2: {α : Type ?u.6483} → {β : Type ?u.6482} → α × β → β2.2: {α : Type ?u.6487} → {β : Type ?u.6486} → α × β → β2), fun ⟨⟨_, _⟩, _⟩ => rfl: ∀ {α : Sort ?u.6541} {a : α}, a = arfl,
fun ⟨_, ⟨_, _⟩⟩ => rfl: ∀ {α : Sort ?u.6702} {a : α}, a = arfl⟩
#align equiv.prod_assoc Equiv.prodAssoc: (α : Type u_1) → (β : Type u_2) → (γ : Type u_3) → (α × β) × γ ≃ α × β × γEquiv.prodAssoc
#align equiv.prod_assoc_symm_apply Equiv.prodAssoc_symm_apply: ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : α × β × γ),
↑(prodAssoc α β γ).symm p = ((p.fst, p.snd.fst), p.snd.snd)Equiv.prodAssoc_symm_apply
#align equiv.prod_assoc_apply Equiv.prodAssoc_apply: ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : (α × β) × γ), ↑(prodAssoc α β γ) p = (p.fst.fst, p.fst.snd, p.snd)Equiv.prodAssoc_apply

/-- `γ`-valued functions on `α × β` are equivalent to functions `α → β → γ`. -/
@[simps: ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), ↑(curry α β γ) = Function.currysimps (config := { fullyApplied := false: Boolfalse })]
def curry: (α : Type u_1) → (β : Type u_2) → (γ : Type u_3) → (α × β → γ) ≃ (α → β → γ)curry (α: ?m.7175α β: Type ?u.7187β γ: ?m.7181γ) : (α: ?m.7175α × β: ?m.7178β → γ: ?m.7181γ) ≃ (α: ?m.7175α → β: ?m.7178β → γ: ?m.7181γ) where
toFun := Function.curry: {α : Type ?u.7212} → {β : Type ?u.7211} → {φ : Type ?u.7210} → (α × β → φ) → α → β → φFunction.curry
invFun := uncurry: {α : Type ?u.7231} → {β : Type ?u.7230} → {φ : Type ?u.7229} → (α → β → φ) → α × β → φuncurry
left_inv := uncurry_curry: ∀ {α : Type ?u.7247} {β : Type ?u.7246} {φ : Type ?u.7245} (f : α × β → φ), uncurry (Function.curry f) = funcurry_curry
right_inv := curry_uncurry: ∀ {α : Type ?u.7263} {β : Type ?u.7262} {φ : Type ?u.7261} (f : α → β → φ), Function.curry (uncurry f) = fcurry_uncurry
#align equiv.curry Equiv.curry: (α : Type u_1) → (β : Type u_2) → (γ : Type u_3) → (α × β → γ) ≃ (α → β → γ)Equiv.curry
#align equiv.curry_symm_apply Equiv.curry_symm_apply: ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), ↑(curry α β γ).symm = uncurryEquiv.curry_symm_apply
#align equiv.curry_apply Equiv.curry_apply: ∀ (α : Type u_1) (β : Type u_2) (γ : Type u_3), ↑(curry α β γ) = Function.curryEquiv.curry_apply

section

/-- `PUnit` is a right identity for type product up to an equivalence. -/
@[simps: ∀ (α : Type u_1) (p : α × PUnit), ↑(prodPUnit α) p = p.fstsimps]
def prodPUnit: (α : Type ?u.7558) → α × PUnit ≃ αprodPUnit (α: ?m.7552α) : α: ?m.7552α × PUnit: Sort ?u.7559PUnit ≃ α: ?m.7552α :=
⟨fun p: ?m.7575p => p: ?m.7575p.1: {α : Type ?u.7578} → {β : Type ?u.7577} → α × β → α1, fun a: ?m.7586a => (a: ?m.7586a, PUnit.unit: PUnitPUnit.unit), fun ⟨_, PUnit.unit: PUnitPUnit.unit⟩ => rfl: ∀ {α : Sort ?u.7625} {a : α}, a = arfl, fun _: ?m.7705_ => rfl: ∀ {α : Sort ?u.7707} {a : α}, a = arfl⟩
#align equiv.prod_punit Equiv.prodPUnit: (α : Type u_1) → α × PUnit ≃ αEquiv.prodPUnit
#align equiv.prod_punit_apply Equiv.prodPUnit_apply: ∀ (α : Type u_1) (p : α × PUnit), ↑(prodPUnit α) p = p.fstEquiv.prodPUnit_apply
#align equiv.prod_punit_symm_apply Equiv.prodPUnit_symm_apply: ∀ (α : Type u_1) (a : α), ↑(prodPUnit α).symm a = (a, PUnit.unit)Equiv.prodPUnit_symm_apply

/-- `PUnit` is a left identity for type product up to an equivalence. -/
@[simps!]
def punitProd: (α : Type u_1) → PUnit × α ≃ αpunitProd (α: ?m.7867α) : PUnit: Sort ?u.7874PUnit × α: ?m.7867α ≃ α: ?m.7867α :=
calc
PUnit: Sort ?u.7882PUnit × α: Type ?u.7872α ≃ α: Type ?u.7872α × PUnit: Sort ?u.7885PUnit := prodComm: (α : Type ?u.7887) → (β : Type ?u.7886) → α × β ≃ β × αprodComm _: Type ?u.7887_ _: Type ?u.7886_
_: ?m✝_ ≃ α: Type ?u.7872α := prodPUnit: (α : Type ?u.7905) → α × PUnit ≃ αprodPUnit _: Type ?u.7905_
#align equiv.punit_prod Equiv.punitProd: (α : Type u_1) → PUnit × α ≃ αEquiv.punitProd
#align equiv.punit_prod_symm_apply Equiv.punitProd_symm_apply: ∀ (α : Type u_1) (a : α), ↑(punitProd α).symm a = (PUnit.unit, a)Equiv.punitProd_symm_apply
#align equiv.punit_prod_apply Equiv.punitProd_apply: ∀ (α : Type u_1) (a : PUnit × α), ↑(punitProd α) a = a.sndEquiv.punitProd_apply

/-- Any `Unique` type is a right identity for type product up to equivalence. -/
def prodUnique: (α : Type u_1) → (β : Type u_2) → [inst : Unique β] → α × β ≃ αprodUnique (α: Type ?u.8324α β: Type ?u.8323β) [Unique: Sort ?u.8318 → Sort (max1?u.8318)Unique β: ?m.8315β] : α: ?m.8312α × β: ?m.8315β ≃ α: ?m.8312α :=
((Equiv.refl: (α : Sort ?u.8329) → α ≃ αEquiv.refl α: Type ?u.8324α).prodCongr: {α₁ : Type ?u.8333} →
{α₂ : Type ?u.8332} → {β₁ : Type ?u.8331} → {β₂ : Type ?u.8330} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ × β₁ ≃ α₂ × β₂prodCongr <| equivPUnit: (α : Sort ?u.8346) → [inst : Unique α] → α ≃ PUnitequivPUnit.{_,1} β: Type ?u.8323β).trans: {α : Sort ?u.8356} → {β : Sort ?u.8355} → {γ : Sort ?u.8354} → α ≃ β → β ≃ γ → α ≃ γtrans <| prodPUnit: (α : Type ?u.8368) → α × PUnit ≃ αprodPUnit α: Type ?u.8324α
#align equiv.prod_unique Equiv.prodUnique: (α : Type u_1) → (β : Type u_2) → [inst : Unique β] → α × β ≃ αEquiv.prodUnique

@[simp]
theorem coe_prodUnique: ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β], ↑(prodUnique α β) = Prod.fstcoe_prodUnique [Unique: Sort ?u.8407 → Sort (max1?u.8407)Unique β: ?m.8404β] : (⇑(prodUnique: (α : Type ?u.8429) → (β : Type ?u.8428) → [inst : Unique β] → α × β ≃ αprodUnique α: ?m.8416α β: ?m.8404β) : α: ?m.8416α × β: ?m.8404β → α: ?m.8416α) = Prod.fst: {α : Type ?u.8499} → {β : Type ?u.8498} → α × β → αProd.fst :=
rfl: ∀ {α : Sort ?u.8557} {a : α}, a = arfl
#align equiv.coe_prod_unique Equiv.coe_prodUnique: ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β], ↑(prodUnique α β) = Prod.fstEquiv.coe_prodUnique

theorem prodUnique_apply: ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β] (x : α × β), ↑(prodUnique α β) x = x.fstprodUnique_apply [Unique: Sort ?u.8616 → Sort (max1?u.8616)Unique β: ?m.8604β] (x: α × βx : α: ?m.8613α × β: ?m.8604β) : prodUnique: (α : Type ?u.8625) → (β : Type ?u.8624) → [inst : Unique β] → α × β ≃ αprodUnique α: ?m.8613α β: ?m.8604β x: α × βx = x: α × βx.1: {α : Type ?u.8694} → {β : Type ?u.8693} → α × β → α1 :=
rfl: ∀ {α : Sort ?u.8706} {a : α}, a = arfl
#align equiv.prod_unique_apply Equiv.prodUnique_apply: ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β] (x : α × β), ↑(prodUnique α β) x = x.fstEquiv.prodUnique_apply

@[simp]
theorem prodUnique_symm_apply: ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β] (x : α), ↑(prodUnique α β).symm x = (x, default)prodUnique_symm_apply [Unique: Sort ?u.8732 → Sort (max1?u.8732)Unique β: ?m.8729β] (x: αx : α: ?m.8736α) :
(prodUnique: (α : Type ?u.8746) → (β : Type ?u.8745) → [inst : Unique β] → α × β ≃ αprodUnique α: ?m.8736α β: ?m.8729β).symm: {α : Sort ?u.8752} → {β : Sort ?u.8751} → α ≃ β → β ≃ αsymm x: αx = (x: αx, default: {α : Sort ?u.8833} → [self : Inhabited α] → αdefault) :=
rfl: ∀ {α : Sort ?u.9208} {a : α}, a = arfl
#align equiv.prod_unique_symm_apply Equiv.prodUnique_symm_apply: ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β] (x : α), ↑(prodUnique α β).symm x = (x, default)Equiv.prodUnique_symm_apply

/-- Any `Unique` type is a left identity for type product up to equivalence. -/
def uniqueProd: (α : Type ?u.9271) → (β : Type ?u.9272) → [inst : Unique β] → β × α ≃ αuniqueProd (α: ?m.9260α β: Type ?u.9272β) [Unique: Sort ?u.9266 → Sort (max1?u.9266)Unique β: ?m.9263β] : β: ?m.9263β × α: ?m.9260α ≃ α: ?m.9260α :=
((equivPUnit: (α : Sort ?u.9277) → [inst : Unique α] → α ≃ PUnitequivPUnit.{_,1} β: Type ?u.9272β).prodCongr: {α₁ : Type ?u.9284} →
{α₂ : Type ?u.9283} → {β₁ : Type ?u.9282} → {β₂ : Type ?u.9281} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ × β₁ ≃ α₂ × β₂prodCongr <| Equiv.refl: (α : Sort ?u.9297) → α ≃ αEquiv.refl α: Type ?u.9271α).trans: {α : Sort ?u.9304} → {β : Sort ?u.9303} → {γ : Sort ?u.9302} → α ≃ β → β ≃ γ → α ≃ γtrans <| punitProd: (α : Type ?u.9316) → PUnit × α ≃ αpunitProd α: Type ?u.9271α
#align equiv.unique_prod Equiv.uniqueProd: (α : Type u_1) → (β : Type u_2) → [inst : Unique β] → β × α ≃ αEquiv.uniqueProd

@[simp]
theorem coe_uniqueProd: ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β], ↑(uniqueProd α β) = Prod.sndcoe_uniqueProd [Unique: Sort ?u.9355 → Sort (max1?u.9355)Unique β: ?m.9352β] : (⇑(uniqueProd: (α : Type ?u.9377) → (β : Type ?u.9376) → [inst : Unique β] → β × α ≃ αuniqueProd α: ?m.9364α β: ?m.9352β) : β: ?m.9352β × α: ?m.9364α → α: ?m.9364α) = Prod.snd: {α : Type ?u.9447} → {β : Type ?u.9446} → α × β → βProd.snd :=
rfl: ∀ {α : Sort ?u.9505} {a : α}, a = arfl
#align equiv.coe_unique_prod Equiv.coe_uniqueProd: ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β], ↑(uniqueProd α β) = Prod.sndEquiv.coe_uniqueProd

theorem uniqueProd_apply: ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β] (x : β × α), ↑(uniqueProd α β) x = x.snduniqueProd_apply [Unique: Sort ?u.9567 → Sort (max1?u.9567)Unique β: ?m.9555β] (x: β × αx : β: ?m.9555β × α: ?m.9564α) : uniqueProd: (α : Type ?u.9576) → (β : Type ?u.9575) → [inst : Unique β] → β × α ≃ αuniqueProd α: ?m.9564α β: ?m.9555β x: β × αx = x: β × αx.2: {α : Type ?u.9645} → {β : Type ?u.9644} → α × β → β2 :=
rfl: ∀ {α : Sort ?u.9657} {a : α}, a = arfl
#align equiv.unique_prod_apply Equiv.uniqueProd_apply: ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β] (x : β × α), ↑(uniqueProd α β) x = x.sndEquiv.uniqueProd_apply

@[simp]
theorem uniqueProd_symm_apply: ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β] (x : α), ↑(uniqueProd α β).symm x = (default, x)uniqueProd_symm_apply [Unique: Sort ?u.9690 → Sort (max1?u.9690)Unique β: ?m.9680β] (x: αx : α: ?m.9687α) :
(uniqueProd: (α : Type ?u.9697) → (β : Type ?u.9696) → [inst : Unique β] → β × α ≃ αuniqueProd α: ?m.9687α β: ?m.9680β).symm: {α : Sort ?u.9703} → {β : Sort ?u.9702} → α ≃ β → β ≃ αsymm x: αx = (default: {α : Sort ?u.9783} → [self : Inhabited α] → αdefault, x: αx) :=
rfl: ∀ {α : Sort ?u.10158} {a : α}, a = arfl
#align equiv.unique_prod_symm_apply Equiv.uniqueProd_symm_apply: ∀ {β : Type u_1} {α : Type u_2} [inst : Unique β] (x : α), ↑(uniqueProd α β).symm x = (default, x)Equiv.uniqueProd_symm_apply

/-- `Empty` type is a right absorbing element for type product up to an equivalence. -/
def prodEmpty: (α : Type ?u.10216) → α × Empty ≃ EmptyprodEmpty (α: Type ?u.10216α) : α: ?m.10210α × Empty: TypeEmpty ≃ Empty: TypeEmpty :=
equivEmpty: (α : Sort ?u.10219) → [inst : IsEmpty α] → α ≃ EmptyequivEmpty _: Sort ?u.10219_
#align equiv.prod_empty Equiv.prodEmpty: (α : Type u_1) → α × Empty ≃ EmptyEquiv.prodEmpty

/-- `Empty` type is a left absorbing element for type product up to an equivalence. -/
def emptyProd: (α : Type ?u.10318) → Empty × α ≃ EmptyemptyProd (α: ?m.10313α) : Empty: TypeEmpty × α: ?m.10313α ≃ Empty: TypeEmpty :=
equivEmpty: (α : Sort ?u.10322) → [inst : IsEmpty α] → α ≃ EmptyequivEmpty _: Sort ?u.10322_
#align equiv.empty_prod Equiv.emptyProd: (α : Type u_1) → Empty × α ≃ EmptyEquiv.emptyProd

/-- `PEmpty` type is a right absorbing element for type product up to an equivalence. -/
def prodPEmpty: (α : Type ?u.10413) → α × PEmpty ≃ PEmptyprodPEmpty (α: ?m.10407α) : α: ?m.10407α × PEmpty: Sort ?u.10414PEmpty ≃ PEmpty: Sort ?u.10415PEmpty :=
equivPEmpty: (α : Sort ?u.10418) → [inst : IsEmpty α] → α ≃ PEmptyequivPEmpty _: Sort ?u.10418_
#align equiv.prod_pempty Equiv.prodPEmpty: (α : Type u_1) → α × PEmpty ≃ PEmptyEquiv.prodPEmpty

/-- `PEmpty` type is a left absorbing element for type product up to an equivalence. -/
def pemptyProd: (α : Type ?u.10509) → PEmpty × α ≃ PEmptypemptyProd (α: ?m.10504α) : PEmpty: Sort ?u.10511PEmpty × α: ?m.10504α ≃ PEmpty: Sort ?u.10512PEmpty :=
equivPEmpty: (α : Sort ?u.10515) → [inst : IsEmpty α] → α ≃ PEmptyequivPEmpty _: Sort ?u.10515_
#align equiv.pempty_prod Equiv.pemptyProd: (α : Type u_1) → PEmpty × α ≃ PEmptyEquiv.pemptyProd

end

section

open Sum

/-- `PSum` is equivalent to `Sum`. -/
def psumEquivSum: (α : Type u_1) → (β : Type u_2) → α ⊕' β ≃ α ⊕ βpsumEquivSum (α: ?m.10604α β: ?m.10607β) : PSum: Sort ?u.10613 → Sort ?u.10612 → Sort (max(max1?u.10613)?u.10612)PSum α: ?m.10604α β: ?m.10607β ≃ Sum: Type ?u.10615 → Type ?u.10614 → Type (max?u.10615?u.10614)Sum α: ?m.10604α β: ?m.10607β where
toFun s: ?m.10626s := PSum.casesOn: {α : Sort ?u.10629} →
{β : Sort ?u.10628} →
{motive : α ⊕' β → Sort ?u.10630} →
(t : α ⊕' β) → ((val : α) → motive (PSum.inl val)) → ((val : β) → motive (PSum.inr val)) → motive tPSum.casesOn s: ?m.10626s inl: {α : Type ?u.10707} → {β : Type ?u.10706} → α → α ⊕ βinl inr: {α : Type ?u.10714} → {β : Type ?u.10713} → β → α ⊕ βinr
invFun := Sum.elim: {α : Type ?u.10669} → {β : Type ?u.10668} → {γ : Sort ?u.10667} → (α → γ) → (β → γ) → α ⊕ β → γSum.elim PSum.inl: {α : Sort ?u.10678} → {β : Sort ?u.10677} → α → α ⊕' βPSum.inl PSum.inr: {α : Sort ?u.10685} → {β : Sort ?u.10684} → β → α ⊕' βPSum.inr
left_inv s: ?m.10695s := byGoals accomplished! 🐙 α: Type ?u.10615β: Type ?u.10614s: α ⊕' βSum.elim PSum.inl PSum.inr ((fun s => PSum.casesOn s inl inr) s) = scases s: α ⊕' βsα: Type ?u.10615β: Type ?u.10614val✝: αinlSum.elim PSum.inl PSum.inr ((fun s => PSum.casesOn s inl inr) (PSum.inl val✝)) = PSum.inl val✝α: Type ?u.10615β: Type ?u.10614val✝: βinrSum.elim PSum.inl PSum.inr ((fun s => PSum.casesOn s inl inr) (PSum.inr val✝)) = PSum.inr val✝ α: Type ?u.10615β: Type ?u.10614s: α ⊕' βSum.elim PSum.inl PSum.inr ((fun s => PSum.casesOn s inl inr) s) = s<;>α: Type ?u.10615β: Type ?u.10614val✝: αinlSum.elim PSum.inl PSum.inr ((fun s => PSum.casesOn s inl inr) (PSum.inl val✝)) = PSum.inl val✝α: Type ?u.10615β: Type ?u.10614val✝: βinrSum.elim PSum.inl PSum.inr ((fun s => PSum.casesOn s inl inr) (PSum.inr val✝)) = PSum.inr val✝ α: Type ?u.10615β: Type ?u.10614s: α ⊕' βSum.elim PSum.inl PSum.inr ((fun s => PSum.casesOn s inl inr) s) = srflGoals accomplished! 🐙
right_inv s: ?m.10701s := byGoals accomplished! 🐙 α: Type ?u.10615β: Type ?u.10614s: α ⊕ β(fun s => PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr s) = scases s: α ⊕ βsα: Type ?u.10615β: Type ?u.10614val✝: αinl(fun s => PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr (inl val✝)) = inl val✝α: Type ?u.10615β: Type ?u.10614val✝: βinr(fun s => PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr (inr val✝)) = inr val✝ α: Type ?u.10615β: Type ?u.10614s: α ⊕ β(fun s => PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr s) = s<;>α: Type ?u.10615β: Type ?u.10614val✝: αinl(fun s => PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr (inl val✝)) = inl val✝α: Type ?u.10615β: Type ?u.10614val✝: βinr(fun s => PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr (inr val✝)) = inr val✝ α: Type ?u.10615β: Type ?u.10614s: α ⊕ β(fun s => PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr s) = srflGoals accomplished! 🐙
#align equiv.psum_equiv_sum Equiv.psumEquivSum: (α : Type u_1) → (β : Type u_2) → α ⊕' β ≃ α ⊕ βEquiv.psumEquivSum

/-- If `α ≃ α'` and `β ≃ β'`, then `α ⊕ β ≃ α' ⊕ β'`. This is `Sum.map` as an equivalence. -/
@[simps apply: ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) (a : α₁ ⊕ β₁),
↑(sumCongr ea eb) a = Sum.map (↑ea) (↑eb) aapply]
def sumCongr: {α₁ : Type u_1} → {α₂ : Type u_2} → {β₁ : Type u_3} → {β₂ : Type u_4} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕ β₂sumCongr (ea: α₁ ≃ α₂ea : α₁: ?m.11002α₁ ≃ α₂: ?m.11008α₂) (eb: β₁ ≃ β₂eb : β₁: ?m.11018β₁ ≃ β₂: ?m.11028β₂) : Sum: Type ?u.11042 → Type ?u.11041 → Type (max?u.11042?u.11041)Sum α₁: ?m.11002α₁ β₁: ?m.11018β₁ ≃ Sum: Type ?u.11044 → Type ?u.11043 → Type (max?u.11044?u.11043)Sum α₂: ?m.11008α₂ β₂: ?m.11028β₂ :=
⟨Sum.map: {α : Type ?u.11067} →
{α' : Type ?u.11065} → {β : Type ?u.11066} → {β' : Type ?u.11064} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'Sum.map ea: α₁ ≃ α₂ea eb: β₁ ≃ β₂eb, Sum.map: {α : Type ?u.11220} →
{α' : Type ?u.11218} → {β : Type ?u.11219} → {β' : Type ?u.11217} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'Sum.map ea: α₁ ≃ α₂ea.symm: {α : Sort ?u.11228} → {β : Sort ?u.11227} → α ≃ β → β ≃ αsymm eb: β₁ ≃ β₂eb.symm: {α : Sort ?u.11302} → {β : Sort ?u.11301} → α ≃ β → β ≃ αsymm, fun x: ?m.11379x => byGoals accomplished! 🐙 α₁: Type ?u.11042α₂: Type ?u.11044β₁: Type ?u.11041β₂: Type ?u.11043ea: α₁ ≃ α₂eb: β₁ ≃ β₂x: α₁ ⊕ β₁Sum.map (↑ea.symm) (↑eb.symm) (Sum.map (↑ea) (↑eb) x) = xsimpGoals accomplished! 🐙, fun x: ?m.11385x => byGoals accomplished! 🐙 α₁: Type ?u.11042α₂: Type ?u.11044β₁: Type ?u.11041β₂: Type ?u.11043ea: α₁ ≃ α₂eb: β₁ ≃ β₂x: α₂ ⊕ β₂Sum.map (↑ea) (↑eb) (Sum.map (↑ea.symm) (↑eb.symm) x) = xsimpGoals accomplished! 🐙⟩
#align equiv.sum_congr Equiv.sumCongr: {α₁ : Type u_1} → {α₂ : Type u_2} → {β₁ : Type u_3} → {β₂ : Type u_4} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕ β₂Equiv.sumCongr
#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) aEquiv.sumCongr_apply

/-- If `α ≃ α'` and `β ≃ β'`, then `PSum α β ≃ PSum α' β'`. -/
def psumCongr: {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → {δ : Sort u_4} → α ≃ β → γ ≃ δ → α ⊕' γ ≃ β ⊕' δpsumCongr (e₁: α ≃ βe₁ : α: ?m.12539α ≃ β: ?m.12545β) (e₂: γ ≃ δe₂ : γ: ?m.12555γ ≃ δ: ?m.12565δ) : PSum: Sort ?u.12579 → Sort ?u.12578 → Sort (max(max1?u.12579)?u.12578)PSum α: ?m.12539α γ: ?m.12555γ ≃ PSum: Sort ?u.12581 → Sort ?u.12580 → Sort (max(max1?u.12581)?u.12580)PSum β: ?m.12545β δ: ?m.12565δ where
toFun x: ?m.12596x := PSum.casesOn: {α : Sort ?u.12599} →
{β : Sort ?u.12598} →
{motive : α ⊕' β → Sort ?u.12600} →
(t : α ⊕' β) → ((val : α) → motive (PSum.inl val)) → ((val : β) → motive (PSum.inr val)) → motive tPSum.casesOn x: ?m.12596x (PSum.inl: {α : Sort ?u.12690} → {β : Sort ?u.12689} → α → α ⊕' βPSum.inl ∘ e₁: α ≃ βe₁) (PSum.inr: {α : Sort ?u.12771} → {β : Sort ?u.12770} → β → α ⊕' βPSum.inr ∘ e₂: γ ≃ δe₂)
invFun x: ?m.12638x := PSum.casesOn: {α : Sort ?u.12641} →
{β : Sort ?u.12640} →
{motive : α ⊕' β → Sort ?u.12642} →
(t : α ⊕' β) → ((val : α) → motive (PSum.inl val)) → ((val : β) → motive (PSum.inr val)) → motive tPSum.casesOn x: ?m.12638x (PSum.inl: {α : Sort ?u.12852} → {β : Sort ?u.12851} → α → α ⊕' βPSum.inl ∘ e₁: α ≃ βe₁.symm: {α : Sort ?u.12859} → {β : Sort ?u.12858} → α ≃ β → β ≃ αsymm) (PSum.inr: {α : Sort ?u.12949} → {β : Sort ?u.12948} → β → α ⊕' βPSum.inr ∘ e₂: γ ≃ δe₂.symm: {α : Sort ?u.12956} → {β : Sort ?u.12955} → α ≃ β → β ≃ αsymm)
left_inv := byGoals accomplished! 🐙 α: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δLeftInverse (fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) fun x =>
PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)rintro (x | x): α ⊕' γ(x: αxx | x: α ⊕' γ | x: γx(x | x): α ⊕' γ)α: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δx: αinl(fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm))
((fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)) (PSum.inl x)) =   PSum.inl xα: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δx: γinr(fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm))
((fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)) (PSum.inr x)) =   PSum.inr x α: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δLeftInverse (fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) fun x =>
PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)<;>α: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δx: αinl(fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm))
((fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)) (PSum.inl x)) =   PSum.inl xα: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δx: γinr(fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm))
((fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)) (PSum.inr x)) =   PSum.inr x α: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δLeftInverse (fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) fun x =>
PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)simpGoals accomplished! 🐙
right_inv := byGoals accomplished! 🐙 α: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δFunction.RightInverse (fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) fun x =>
PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)rintro (x | x): β ⊕' δ(x: βxx | x: β ⊕' δ | x: δx(x | x): β ⊕' δ)α: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δx: βinl(fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂))
((fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) (PSum.inl x)) =   PSum.inl xα: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δx: δinr(fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂))
((fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) (PSum.inr x)) =   PSum.inr x α: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δFunction.RightInverse (fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) fun x =>
PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)<;>α: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δx: βinl(fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂))
((fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) (PSum.inl x)) =   PSum.inl xα: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δx: δinr(fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂))
((fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) (PSum.inr x)) =   PSum.inr x α: Sort ?u.12569β: Sort ?u.12568γ: Sort ?u.12573δ: Sort ?u.12572e₁: α ≃ βe₂: γ ≃ δFunction.RightInverse (fun x => PSum.casesOn x (PSum.inl ∘ ↑e₁.symm) (PSum.inr ∘ ↑e₂.symm)) fun x =>
PSum.casesOn x (PSum.inl ∘ ↑e₁) (PSum.inr ∘ ↑e₂)simpGoals accomplished! 🐙
#align equiv.psum_congr Equiv.psumCongr: {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → {δ : Sort u_4} → α ≃ β → γ ≃ δ → α ⊕' γ ≃ β ⊕' δEquiv.psumCongr

/-- 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: α₁ ≃ α₂ea : α₁: ?m.16857α₁ ≃ α₂: ?m.16863α₂) (eb: β₁ ≃ β₂eb : β₁: ?m.16873β₁ ≃ β₂: ?m.16883β₂) :
PSum: Sort ?u.16897 → Sort ?u.16896 → Sort (max(max1?u.16897)?u.16896)PSum α₁: ?m.16857α₁ β₁: ?m.16873β₁ ≃ Sum: Type ?u.16899 → Type ?u.16898 → Type (max?u.16899?u.16898)Sum α₂: ?m.16863α₂ β₂: ?m.16883β₂ :=
(ea: α₁ ≃ α₂ea.psumCongr: {α : Sort ?u.16910} → {β : Sort ?u.16909} → {γ : Sort ?u.16908} → {δ : Sort ?u.16907} → α ≃ β → γ ≃ δ → α ⊕' γ ≃ β ⊕' δpsumCongr eb: β₁ ≃ β₂eb).trans: {α : Sort ?u.16929} → {β : Sort ?u.16928} → {γ : Sort ?u.16927} → α ≃ β → β ≃ γ → α ≃ γtrans (psumEquivSum: (α : Type ?u.16941) → (β : Type ?u.16940) → α ⊕' β ≃ α ⊕ β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} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕' β₁ ≃ α₂ ⊕ β₂Equiv.psumSum

/-- 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: α₁ ≃ α₂ea : α₁: ?m.17082α₁ ≃ α₂: ?m.17088α₂) (eb: β₁ ≃ β₂eb : β₁: ?m.17098β₁ ≃ β₂: ?m.17108β₂) :
Sum: Type ?u.17122 → Type ?u.17121 → Type (max?u.17122?u.17121)Sum α₁: ?m.17082α₁ β₁: ?m.17098β₁ ≃ PSum: Sort ?u.17124 → Sort ?u.17123 → Sort (max(max1?u.17124)?u.17123)PSum α₂: ?m.17088α₂ β₂: ?m.17108β₂ :=
(ea: α₁ ≃ α₂ea.symm: {α : Sort ?u.17133} → {β : Sort ?u.17132} → α ≃ β → β ≃ αsymm.psumSum: {α₁ : Sort ?u.17141} →
{α₂ : Type ?u.17140} → {β₁ : Sort ?u.17139} → {β₂ : Type ?u.17138} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕' β₁ ≃ α₂ ⊕ β₂psumSum eb: β₁ ≃ β₂eb.symm: {α : Sort ?u.17155} → {β : Sort ?u.17154} → α ≃ β → β ≃ αsymm).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} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕' β₂Equiv.sumPSum

@[simp]
theorem sumCongr_trans: ∀ {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6} (e : α₁ ≃ β₁)
(f : α₂ ≃ β₂) (g : β₁ ≃ γ₁) (h : β₂ ≃ γ₂), (sumCongr e f).trans (sumCongr g h) = sumCongr (e.trans g) (f.trans h)sumCongr_trans (e: α₁ ≃ β₁e : α₁: ?m.17320α₁ ≃ β₁: ?m.17326β₁) (f: α₂ ≃ β₂f : α₂: ?m.17336α₂ ≃ β₂: ?m.17346β₂) (g: β₁ ≃ γ₁g : β₁: ?m.17326β₁ ≃ γ₁: ?m.17360γ₁) (h: β₂ ≃ γ₂h : β₂: ?m.17346β₂ ≃ γ₂: ?m.17378γ₂) :
(Equiv.sumCongr: {α₁ : Type ?u.17401} →
{α₂ : Type ?u.17400} → {β₁ : Type ?u.17399} → {β₂ : Type ?u.17398} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕ β₂Equiv.sumCongr e: α₁ ≃ β₁e f: α₂ ≃ β₂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} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕ β₂Equiv.sumCongr g: β₁ ≃ γ₁g h: β₂ ≃ γ₂h) = Equiv.sumCongr: {α₁ : Type ?u.17444} →
{α₂ : Type ?u.17443} → {β₁ : Type ?u.17442} → {β₂ : Type ?u.17441} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕ β₂Equiv.sumCongr (e: α₁ ≃ β₁e.trans: {α : Sort ?u.17451} → {β : Sort ?u.17450} → {γ : Sort ?u.17449} → α ≃ β → β ≃ γ → α ≃ γtrans g: β₁ ≃ γ₁g) (f: α₂ ≃ β₂f.trans: {α : Sort ?u.17468} → {β : Sort ?u.17467} → {γ : Sort ?u.17466} → α ≃ β → β ≃ γ → α ≃ γtrans h: β₂ ≃ γ₂h) := byGoals accomplished! 🐙
α₁: Type u_1β₁: Type u_2α₂: Type u_3β₂: Type u_4γ₁: Type u_5γ₂: Type u_6e: α₁ ≃ β₁f: α₂ ≃ β₂g: β₁ ≃ γ₁h: β₂ ≃ γ₂(sumCongr e f).trans (sumCongr g h) = sumCongr (e.trans g) (f.trans h)ext i: ?αiα₁: Type u_1β₁: Type u_2α₂: Type u_3β₂: Type u_4γ₁: Type u_5γ₂: Type u_6e: α₁ ≃ β₁f: α₂ ≃ β₂g: β₁ ≃ γ₁h: β₂ ≃ γ₂i: α₁ ⊕ α₂H↑((sumCongr e f).trans (sumCongr g h)) i = ↑(sumCongr (e.trans g) (f.trans h)) i
α₁: Type u_1β₁: Type u_2α₂: Type u_3β₂: Type u_4γ₁: Type u_5γ₂: Type u_6e: α₁ ≃ β₁f: α₂ ≃ β₂g: β₁ ≃ γ₁h: β₂ ≃ γ₂(sumCongr e f).trans (sumCongr g h) = sumCongr (e.trans g) (f.trans h)cases i: ?αiα₁: Type u_1β₁: Type u_2α₂: Type u_3β₂: Type u_4γ₁: Type u_5γ₂: Type u_6e: α₁ ≃ β₁f: α₂ ≃ β₂g: β₁ ≃ γ₁h: β₂ ≃ γ₂val✝: α₁H.inl↑((sumCongr e f).trans (sumCongr g h)) (inl val✝) = ↑(sumCongr (e.trans g) (f.trans h)) (inl val✝)α₁: Type u_1β₁: Type u_2α₂: Type u_3β₂: Type u_4γ₁: Type u_5γ₂: Type u_6e: α₁ ≃ β₁f: α₂ ≃ β₂g: β₁ ≃ γ₁h: β₂ ≃ γ₂val✝: α₂H.inr↑((sumCongr e f).trans (sumCongr g h)) (inr val✝) = ↑(sumCongr (e.trans g) (f.trans h)) (inr val✝) α₁: Type u_1β₁: Type u_2α₂: Type u_3β₂: Type u_4γ₁: Type u_5γ₂: Type u_6e: α₁ ≃ β₁f: α₂ ≃ β₂g: β₁ ≃ γ₁h: β₂ ≃ γ₂i: α₁ ⊕ α₂H↑((sumCongr e f).trans (sumCongr g h)) i = ↑(sumCongr (e.trans g) (f.trans h)) i<;>α₁: Type u_1β₁: Type u_2α₂: Type u_3β₂: Type u_4γ₁: Type u_5γ₂: Type u_6e: α₁ ≃ β₁f: α₂ ≃ β₂g: β₁ ≃ γ₁h: β₂ ≃ γ₂val✝: α₁H.inl↑((sumCongr e f).trans (sumCongr g h)) (inl val✝) = ↑(sumCongr (e.trans g) (f.trans h)) (inl val✝)α₁: Type u_1β₁: Type u_2α₂: Type u_3β₂: Type u_4γ₁: Type u_5γ₂: Type u_6e: α₁ ≃ β₁f: α₂ ≃ β₂g: β₁ ≃ γ₁h: β₂ ≃ γ₂val✝: α₂H.inr↑((sumCongr e f).trans (sumCongr g h)) (inr val✝) = ↑(sumCongr (e.trans g) (f.trans h)) (inr val✝) α₁: Type u_1β₁: Type u_2α₂: Type u_3β₂: Type u_4γ₁: Type u_5γ₂: Type u_6e: α₁ ≃ β₁f: α₂ ≃ β₂g: β₁ ≃ γ₁h: β₂ ≃ γ₂i: α₁ ⊕ α₂H↑((sumCongr e f).trans (sumCongr g h)) i = ↑(sumCongr (e.trans g) (f.trans h)) irflGoals accomplished! 🐙
#align equiv.sum_congr_trans 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 : β₂ ≃ γ₂), (sumCongr e f).trans (sumCongr g h) = sumCongr (e.trans g) (f.trans h)Equiv.sumCongr_trans

@[simp]
theorem sumCongr_symm: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : α ≃ β) (f : γ ≃ δ),
(sumCongr e f).symm = sumCongr e.symm f.symmsumCongr_symm (e: α ≃ βe : α: ?m.17681α ≃ β: ?m.17687β) (f: γ ≃ δf : γ: ?m.17697γ ≃ δ: ?m.17707δ) :
(Equiv.sumCongr: {α₁ : Type ?u.17722} →
{α₂ : Type ?u.17721} → {β₁ : Type ?u.17720} → {β₂ : Type ?u.17719} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕ β₂Equiv.sumCongr e: α ≃ βe f: γ ≃ δf).symm: {α : Sort ?u.17732} → {β : Sort ?u.17731} → α ≃ β → β ≃ αsymm = Equiv.sumCongr: {α₁ : Type ?u.17743} →
{α₂ : Type ?u.17742} → {β₁ : Type ?u.17741} → {β₂ : Type ?u.17740} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕ β₂Equiv.sumCongr e: α ≃ βe.symm: {α : Sort ?u.17749} → {β : Sort ?u.17748} → α ≃ β → β ≃ αsymm f: γ ≃ δf.symm: {α : Sort ?u.17760} → {β : Sort ?u.17759} → α ≃ β → β ≃ αsymm :=
rfl: ∀ {α : Sort ?u.17780} {a : α}, a = arfl
#align equiv.sum_congr_symm Equiv.sumCongr_symm: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : α ≃ β) (f : γ ≃ δ),
(sumCongr e f).symm = sumCongr e.symm f.symmEquiv.sumCongr_symm

@[simp]
theorem sumCongr_refl: ∀ {α : Type u_1} {β : Type u_2}, sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)sumCongr_refl : Equiv.sumCongr: {α₁ : Type ?u.17932} →
{α₂ : Type ?u.17931} → {β₁ : Type ?u.17930} → {β₂ : Type ?u.17929} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕ β₂Equiv.sumCongr (Equiv.refl: (α : Sort ?u.17937) → α ≃ αEquiv.refl α: ?m.17906α) (Equiv.refl: (α : Sort ?u.17942) → α ≃ αEquiv.refl β: ?m.17925β) = Equiv.refl: (α : Sort ?u.17947) → α ≃ αEquiv.refl (Sum: Type ?u.17949 → Type ?u.17948 → Type (max?u.17949?u.17948)Sum α: ?m.17906α β: ?m.17925β) := byGoals accomplished! 🐙
α: Type u_1β: Type u_2sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)ext i: ?αiα: Type u_1β: Type u_2i: α ⊕ βH↑(sumCongr (Equiv.refl α) (Equiv.refl β)) i = ↑(Equiv.refl (α ⊕ β)) i
α: Type u_1β: Type u_2sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)cases i: ?αiα: Type u_1β: Type u_2val✝: αH.inl↑(sumCongr (Equiv.refl α) (Equiv.refl β)) (inl val✝) = ↑(Equiv.refl (α ⊕ β)) (inl val✝)α: Type u_1β: Type u_2val✝: βH.inr↑(sumCongr (Equiv.refl α) (Equiv.refl β)) (inr val✝) = ↑(Equiv.refl (α ⊕ β)) (inr val✝) α: Type u_1β: Type u_2i: α ⊕ βH↑(sumCongr (Equiv.refl α) (Equiv.refl β)) i = ↑(Equiv.refl (α ⊕ β)) i<;>α: Type u_1β: Type u_2val✝: αH.inl↑(sumCongr (Equiv.refl α) (Equiv.refl β)) (inl val✝) = ↑(Equiv.refl (α ⊕ β)) (inl val✝)α: Type u_1β: Type u_2val✝: βH.inr↑(sumCongr (Equiv.refl α) (Equiv.refl β)) (inr val✝) = ↑(Equiv.refl (α ⊕ β)) (inr val✝) α: Type u_1β: Type u_2i: α ⊕ βH↑(sumCongr (Equiv.refl α) (Equiv.refl β)) i = ↑(Equiv.refl (α ⊕ β)) irflGoals accomplished! 🐙
#align equiv.sum_congr_refl Equiv.sumCongr_refl: ∀ {α : Type u_1} {β : Type u_2}, sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)Equiv.sumCongr_refl

namespace Perm

/-- Combine a permutation of `α` and of `β` into a permutation of `α ⊕ β`. -/
@[reducible]
def sumCongr: {α : Type ?u.18119} → {β : Type ?u.18118} → Perm α → Perm β → Perm (α ⊕ β)sumCongr (ea: Perm αea : Equiv.Perm: Sort ?u.18111 → Sort (max1?u.18111)Equiv.Perm α: ?m.18100α) (eb: Perm βeb : Equiv.Perm: Sort ?u.18114 → Sort (max1?u.18114)Equiv.Perm β: ?m.18108β) : Equiv.Perm: Sort ?u.18117 → Sort (max1?u.18117)Equiv.Perm (Sum: Type ?u.18119 → Type ?u.18118 → Type (max?u.18119?u.18118)Sum α: ?m.18100α β: ?m.18108β) :=
Equiv.sumCongr: {α₁ : Type ?u.18132} →
{α₂ : Type ?u.18131} → {β₁ : Type ?u.18130} → {β₂ : Type ?u.18129} → α₁ ≃ α₂ → β₁ ≃ β₂ → α₁ ⊕ β₁ ≃ α₂ ⊕ β₂Equiv.sumCongr ea: Perm αea eb: Perm βeb
#align equiv.perm.sum_congr Equiv.Perm.sumCongr: {α : Type u_1} → {β : Type u_2} → Perm α → Perm β → Perm (α ⊕ β)Equiv.Perm.sumCongr

@[simp]
theorem sumCongr_apply: ∀ {α : Type u_1} {β : Type u_2} (ea : Perm α) (eb : Perm β) (x : α ⊕ β), ↑(sumCongr ea eb) x = Sum.map (↑ea) (↑eb) xsumCongr_apply (ea: Perm αea : Equiv.Perm: Sort ?u.18236 → Sort (max1?u.18236)Equiv.Perm α: ?m.18233α) (eb: Perm βeb : Equiv.Perm: Sort ?u.18247 → Sort (max1?u.18247)Equiv.Perm β: ?m.18241β) (x: α ⊕ βx : Sum: Type ?u.18251 → Type ?u.18250 → Type (max?u.18251?u.18250)Sum α: ?m.18233α β: ?m.18241β) :
sumCongr: {α : Type ?u.18256} → {β : Type ?u.18255} → Perm α → Perm β → Perm (α ⊕ β)sumCongr ea: Perm αea eb: Perm βeb x: α ⊕ βx = Sum.map: {α : Type ?u.18334} →
{α' : Type ?u.18332} → {β : Type ?u.18333} → {β' : Type ?u.18331} → (α → α') → (β → β') → α ⊕ β → α' ⊕ β'Sum.map (⇑ea: Perm αea) (⇑eb: Perm βeb) x: α ⊕ βx :=
Equiv.sumCongr_apply: ∀ {α₁ : Type ?u.18486} {α₂ : Type ?u.18485} {β₁ : Type ?u.18484} {β₂ : Type ?u.18483} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂)
(a : α₁ ⊕ β₁), ↑(Equiv.sumCongr ea eb) a = Sum.map (↑ea) (↑eb) aEquiv.sumCongr_apply ea: Perm αea eb: Perm βeb x: α ⊕ βx
#align equiv.perm.sum_congr_apply Equiv.Perm.sumCongr_apply: ∀ {α : Type u_1} {β : Type u_2} (ea : Perm α) (eb : Perm β) (x : α ⊕ β), ↑(sumCongr ea eb) x = Sum.map (↑ea) (↑eb) xEquiv.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: ∀ {α : Type u_1} {β : Type u_2} (e : Perm α) (f : Perm β) (g : Perm α) (h : Perm β),
(sumCongr e f).trans (sumCongr g h) = sumCongr (e.trans g) (f.trans h)sumCongr_trans (e: Perm αe : Equiv.Perm: Sort ?u.18551 → Sort (max1?u.18551)Equiv.Perm α: ?m.18548α) (f: Perm βf : Equiv.Perm: Sort ?u.18562 → Sort (max1?u.18562)Equiv.Perm β: ?m.18556β) (g: Perm αg : Equiv.Perm: Sort ?u.18565 → Sort (max1?u.18565)Equiv.Perm α: ?m.18548α)
(h: Perm βh : Equiv.Perm: Sort ?u.18568 → Sort (max1?u.18568)Equiv.Perm β: ?m.18556β) : (sumCongr: {α : Type ?u.18573} → {β : Type ?u.18572} → Perm α → Perm β → Perm (α ⊕ β)sumCongr e: Perm αe f: Perm βf).trans: {α : Sort ?u.18580} → {β : Sort ?u.18579} → {γ : Sort ?u.18578} → α ≃ β → β ≃ γ → α ≃ γtrans (sumCongr: {α : Type ?u.18592} → {β : Type ?u.18591} → Perm α → Perm β → Perm (α ⊕ β)sumCongr g: Perm αg h: Perm βh) = sumCongr: {α : Type ?u.18600} → {β : Type ?u.18599} → Perm α → Perm β → Perm (α ⊕ β)sumCongr (e: Perm αe.trans: {α : Sort ?u.18605} → {β : Sort ?u.18604} → {γ : Sort ?u.18603} → α ≃ β → β ≃ γ → α ≃ γtrans g: Perm αg) (f: Perm βf.trans: {α : Sort ?u.18620} → {β : Sort ?u.18619} → {γ : Sort ?u.18618} → α ≃ β → β ≃ γ → α ≃ γtrans h: Perm βh) :=
Equiv.sumCongr_trans: ∀ {α₁ : Type ?u.18641} {β₁ : Type ?u.18642} {α₂ : Type ?u.18643} {β₂ : Type ?u.18644} {γ₁ : Type ?u.18645}
{γ₂ : Type ?u.18646} (e : α₁ ≃ β₁) (f : α₂ ≃ β₂) (g : β₁ ≃ γ₁) (h : β₂ ≃ γ₂),
(Equiv.sumCongr e f).trans (Equiv.sumCongr g h) = Equiv.sumCongr (e.trans g) (f.trans h)Equiv.sumCongr_trans e: Perm αe f: Perm βf g: Perm αg h: Perm βh
#align equiv.perm.sum_congr_trans Equiv.Perm.sumCongr_trans: ∀ {α : Type u_1} {β : Type u_2} (e : Perm α) (f : Perm β) (g : Perm α) (h : Perm β),
(sumCongr e f).trans (sumCongr g h) = sumCongr (e.trans g) (f.trans h)Equiv.Perm.sumCongr_trans

theorem sumCongr_symm: ∀ {α : Type u_1} {β : Type u_2} (e : Perm α) (f : Perm β), (sumCongr e f).symm = sumCongr e.symm f.symmsumCongr_symm (e: Perm αe : Equiv.Perm: Sort ?u.18681 → Sort (max1?u.18681)Equiv.Perm α: ?m.18678α) (f: Perm βf : Equiv.Perm: Sort ?u.18692 → Sort (max1?u.18692)Equiv.Perm β: ?m.18686β) :
(sumCongr: {α : Type ?u.18697} → {β : Type ?u.18696} → Perm α → Perm β → Perm (α ⊕ β)sumCongr e: Perm αe f: Perm βf).symm: {α : Sort ?u.18703} → {β : Sort ?u.18702} → α ≃ β → β ≃ αsymm = sumCongr: {α : Type ?u.18712} → {β : Type ?u.18711} → Perm α → Perm β → Perm (α ⊕ β)sumCongr e: Perm αe.symm: {α : Sort ?u.18716} → {β : Sort ?u.18715} → α ≃ β → β ≃ αsymm f: Perm βf.symm: {α : Sort ?u.18727} → {β : Sort ?u.18726} → α ≃ β → β ≃ αsymm :=
Equiv.sumCongr_symm: ∀ {α : Type ?u.18743} {β : Type ?u.18744} {γ : Type ?u.18745} {δ : Type ?u.18746} (e : α ≃ β) (f : γ ≃ δ),
(Equiv.sumCongr e f).symm = Equiv.sumCongr e.symm f.symmEquiv.sumCongr_symm e: Perm αe f: Perm βf
#align equiv.perm.sum_congr_symm Equiv.Perm.sumCongr_symm: ∀ {α : Type u_1} {β : Type u_2} (e : Perm α) (f : Perm β), (sumCongr e f).symm = sumCongr e.symm f.symmEquiv.Perm.sumCongr_symm

theorem sumCongr_refl: ∀ {α : Type u_1} {β : Type u_2}, sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)sumCongr_refl : sumCongr: {α : Type ?u.18791} → {β : Type ?u.18790} → Perm α → Perm β → Perm (α ⊕ β)sumCongr (Equiv.refl: (α : Sort ?u.18794) → α ≃ αEquiv.refl α: ?m.18773α) (Equiv.refl: (α : Sort ?u.18797) → α ≃ αEquiv.refl β: ?m.18786β) = Equiv.refl: (α : Sort ?u.18800) → α ≃ αEquiv.refl (Sum: Type ?u.18802 → Type ?u.18801 → Type (max?u.18802?u.18801)Sum α: ?m.18773α β: ?m.18786β) :=
Equiv.sumCongr_refl: ∀ {α : Type ?u.18807} {β : Type ?u.18808}, Equiv.sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)Equiv.sumCongr_refl
#align equiv.perm.sum_congr_refl Equiv.Perm.sumCongr_refl: ∀ {α : Type u_1} {β : Type u_2}, sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)Equiv.Perm.sumCongr_refl

end Perm

/-- `Bool` is equivalent the sum of two `PUnit`s. -/
def boolEquivPUnitSumPUnit: Bool ≃ PUnit ⊕ PUnitboolEquivPUnitSumPUnit : Bool: TypeBool ≃ Sum: Type ?u.18829 → Type ?u.18828 → Type (max?u.18829?u.18828)Sum PUnit: Type uPUnit.{u + 1} PUnit: Type vPUnit.{v + 1} :=
⟨fun b: ?m.18844b => cond: {α : Type ?u.18846} → Bool → α → α → αcond b: ?m.18844b (inr: {α : Type ?u.18849} → {β : Type ?u.18848} → β → α ⊕ βinr PUnit.unit: PUnitPUnit.unit) (inl: {α : Type ?u.18856} → {β : Type ?u.18855} → α → α ⊕ βinl PUnit.unit: PUnitPUnit.unit), Sum.elim: {α : Type ?u.18864} → {β : Type ?u.18863} → {γ : Sort ?u.18862} → (α → γ) → (β → γ) → α ⊕ β → γSum.elim (fun _: ?m.18871_ => false: Boolfalse) fun _: ?m.18876_ => true: Booltrue,
fun b: ?m.18884b => byGoals accomplished! 🐙 b: BoolSum.elim (fun x => false) (fun x => true) ((fun b => bif b then inr PUnit.unit else inl PUnit.unit) b) = bcases b: BoolbfalseSum.elim (fun x => false) (fun x => true) ((fun b => bif b then inr PUnit.unit else inl PUnit.unit) false) = falsetrueSum.elim (fun x => false) (fun x => true) ((fun b => bif b then inr PUnit.unit else inl PUnit.unit) true) = true b: BoolSum.elim (fun x => false) (fun x => true) ((fun b => bif b then inr PUnit.unit else inl PUnit.unit) b) = b<;>falseSum.elim (fun x => false) (fun x => true) ((fun b => bif b then inr PUnit.unit else inl PUnit.unit) false) = falsetrueSum.elim (fun x => false) (fun x => true) ((fun b => bif b then inr PUnit.unit else inl PUnit.unit) true) = true b: BoolSum.elim (fun x => false) (fun x => true) ((fun b => bif b then inr PUnit.unit else inl PUnit.unit) b) = brflGoals accomplished! 🐙, fun s: ?m.18890s => byGoals accomplished! 🐙 s: PUnit ⊕ PUnit(fun b => bif b then inr PUnit.unit else inl PUnit.unit) (Sum.elim (fun x => false) (fun x => true) s) = srcases s: PUnit ⊕ PUnits with (⟨⟨⟩⟩ | ⟨⟨⟩⟩): PUnit ⊕ PUnit(⟨⟨⟩⟩ | ⟨⟨⟩⟩: PUnit ⊕ PUnit⟨⟨⟩: PUnit⟨⟩⟨⟨⟩⟩ | ⟨⟨⟩⟩: PUnit ⊕ PUnit⟩ | ⟨⟨⟩: PUnit⟨⟩⟨⟨⟩⟩ | ⟨⟨⟩⟩: PUnit ⊕ PUnit⟩(⟨⟨⟩⟩ | ⟨⟨⟩⟩): PUnit ⊕ PUnit)inl.unit(fun b => bif b then inr PUnit.unit else inl PUnit.unit) (Sum.elim (fun x => false) (fun x => true) (inl PUnit.unit)) =   inl PUnit.unitinr.unit(fun b => bif b then inr PUnit.unit else inl PUnit.unit) (Sum.elim (fun x => false) (fun x => true) (inr PUnit.unit)) =   inr PUnit.unit s: PUnit ⊕ PUnit(fun b => bif b then inr PUnit.unit else inl PUnit.unit) (Sum.elim (fun x => false) (fun x => true) s) = s<;>inl.unit(fun b => bif b then inr PUnit.unit else inl PUnit.unit) (Sum.elim (fun x => false) (fun x => true) (inl PUnit.unit)) =   inl PUnit.unitinr.unit(fun b => bif b then inr PUnit.unit else inl PUnit.unit) (Sum.elim (fun x => false) (fun x => true) (inr PUnit.unit)) =   inr PUnit.unit s: PUnit ⊕ PUnit(fun b => bif b then inr PUnit.unit else inl PUnit.unit) (Sum.elim (fun x => false) (fun x => true) s) = srflGoals accomplished! 🐙⟩
#align equiv.bool_equiv_punit_sum_punit Equiv.boolEquivPUnitSumPUnit: Bool ≃ PUnit ⊕ PUnitEquiv.boolEquivPUnitSumPUnit

/-- Sum of types is commutative up to an equivalence. This is `Sum.swap` as an equivalence. -/
@[simps (config := { fullyApplied := false: Boolfalse }) apply: ∀ (α : Type u_1) (β : Type u_2), ↑(sumComm α β) = Sum.swapapply]
def sumComm: (α : Type u_1) → (β : Type u_2) → α ⊕ β ≃ β ⊕ αsumComm (α: ?m.19124α β: Type ?u.19132β) : Sum: Type ?u.19133 → Type ?u.19132 → Type (max?u.19133?u.19132)Sum α: ?m.19124α β: ?m.19127β ≃ Sum: Type ?u.19135 → Type ?u.19134 → Type (max?u.19135?u.19134)Sum β: ?m.19127β α: ?m.19124α :=
⟨Sum.swap: {α : Type ?u.19152} → {β : Type ?u.19151} → α ⊕ β → β ⊕ αSum.swap, Sum.swap: {α : Type ?u.19163} → {β : Type ?u.19162} → α ⊕ β → β ⊕ αSum.swap, Sum.swap_swap: ∀ {α : Type ?u.19170} {β : Type ?u.19169} (x : α ⊕ β), Sum.swap (Sum.swap x) = xSum.swap_swap, Sum.swap_swap: ∀ {α : Type ?u.19183} {β : Type ?u.19182} (x : α ⊕ β), Sum.swap (Sum.swap x) = xSum.swap_swap⟩
#align equiv.sum_comm Equiv.sumComm: (α : Type u_1) → (β : Type u_2) → α ⊕ β ≃ β ⊕ αEquiv.sumComm
#align equiv.sum_comm_apply Equiv.sumComm_apply: ∀ (α : Type u_1) (β : Type u_2), ↑(sumComm α β) = Sum.swapEquiv.sumComm_apply

@[simp]
theorem sumComm_symm: ∀ (α : Type u_1) (β : Type u_2), (sumComm α β).symm = sumComm β αsumComm_symm (α: ?m.19328α β: Type u_2β) : (sumComm: (α : Type ?u.19336) → (β : Type ?u.19335) → α ⊕ β ≃ β ⊕ αsumComm α: ?m.19328α β: ?m.19331β).symm: {α : Sort ?u.19338} → {β : Sort ?u.19337} → α ≃ β → β ≃ αsymm = sumComm: (α : Type ?u.19347) → (β : Type ?u.19346) → α ⊕ β ≃ β ⊕ αsumComm β: ?m.19331β α: ?m.19328α :=
rfl: ∀ {α : Sort ?u.19356} {a : α}, a = arfl
#align equiv.sum_comm_symm Equiv.sumComm_symm: ∀ (α : Type u_1) (β : Type u_2), (sumComm α β).symm = sumComm β αEquiv.sumComm_symm

/-- Sum of types is associative up to an equivalence. -/
def sumAssoc: (α : Type u_1) → (β : Type u_2) → (γ : Type u_3) → (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γsumAssoc (α: Type ?u.19421α β: Type ?u.19420β γ: ?m.19413γ) : Sum: Type ?u.19419 → Type ?u.19418 → Type (max?u.19419?u.19418)Sum (Sum: Type ?u.19421 → Type ?u.19420 → Type (max?u.19421?u.19420)Sum α: ?m.19407α β: ?m.19410β) γ: ?m.19413γ ≃ Sum: Type ?u.19423 → Type ?u.19422 → Type (max?u.19423?u.19422)Sum α: ?m.19407α (Sum: Type ?u.19425 → Type ?u.19424 → Type (max?u.19425?u.19424)Sum β: ?m.19410β γ: ?m.19413γ) :=
⟨Sum.elim: {α : Type ?u.19444} → {β : Type ?u.19443} → {γ : Sort ?u.19442} → (α → γ) → (β → γ) → α ⊕ β → γSum.elim (Sum.elim: {α : Type ?u.19454} → {β : Type ?u.19453} → {γ : Sort ?u.19452} → (α → γ) → (β → γ) → α ⊕ β → γSum.elim Sum.inl: {α : Type ?u.19463} → {β : Type ?u.19462} → α → α ⊕ βSum.inl (Sum.inr: {α : Type ?u.19480} → {β : Type ?u.19479} → β → α ⊕ βSum.inr ∘ Sum.inl: {α : Type ?u.19487} → {β : Type ?u.19486} → α → α ⊕ βSum.inl)) (Sum.inr: {α : Type ?u.19510} → {β : Type ?u.19509} → β → α ⊕ βSum.inr ∘ Sum.inr: {α : Type ?u.19517} → {β : Type ?u.19516} → β → α ⊕ βSum.inr),
Sum.elim: {α : Type ?u.19531} → {β : Type ?u.19530} → {γ : Sort ?u.19529} → (α → γ) → (β → γ) → α ⊕ β → γSum.elim (Sum.inl: {α : Type ?u.19546} → {β : Type ?u.19545} → α → α ⊕ βSum.inl ∘ Sum.inl: {α : Type ?u.19553} → {β : Type ?u.19552} → α → α ⊕ βSum.inl) <| Sum.elim: {α : Type ?u.19564} → {β : Type ?u.19563} → {γ : Sort ?u.19562} → (α → γ) → (β → γ) → α ⊕ β → γSum.elim (Sum.inl: {α : Type ?u.19579} → {β : Type ?u.19578} → α → α ⊕ βSum.inl ∘ Sum.inr: {α : Type ?u.19586} → {β : Type ?u.19585} → β → α ⊕ βSum.inr) Sum.inr: {α : Type ?u.19596} → {β : Type ?u.19595} → β → α ⊕ βSum.inr,
byGoals accomplished! 🐙 α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418LeftInverse (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr)) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr))rintro (⟨_ | _⟩ | _): (α ⊕ β) ⊕ γ(⟨_ | _⟩ | _: (α ⊕ β) ⊕ γ⟨_: α__ | _: α ⊕ β | _: β_⟨_ | _⟩ | _: (α ⊕ β) ⊕ γ⟩ | _: γ_(⟨_ | _⟩ | _): (α ⊕ β) ⊕ γ)α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418val✝: αinl.inlSum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inl val✝))) =   inl (inl val✝)α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418val✝: βinl.inrSum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inr val✝))) =   inl (inr val✝)α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418val✝: γinrSum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inr val✝)) = inr val✝ α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418LeftInverse (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr)) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr))<;>α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418val✝: αinl.inlSum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inl val✝))) =   inl (inl val✝)α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418val✝: βinl.inrSum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inl (inr val✝))) =   inl (inr val✝)α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418val✝: γinrSum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (inr val✝)) = inr val✝ α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418LeftInverse (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr)) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr))rflGoals accomplished! 🐙, byGoals accomplished! 🐙
α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418Function.RightInverse (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr))
(Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr))rintro (_ | ⟨_ | _⟩): α ⊕ β ⊕ γ(_: α__ | ⟨_ | _⟩: α ⊕ β ⊕ γ | ⟨_: β__ | _: β ⊕ γ | _: γ__ | ⟨_ | _⟩: α ⊕ β ⊕ γ⟩(_ | ⟨_ | _⟩): α ⊕ β ⊕ γ)α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418val✝: αinlSum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inl val✝)) = inl val✝α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418val✝: βinr.inlSum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inr (inl val✝))) =   inr (inl val✝)α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418val✝: γinr.inrSum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inr (inr val✝))) =   inr (inr val✝) α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418Function.RightInverse (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr))
(Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr))<;>α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418val✝: αinlSum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inl val✝)) = inl val✝α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418val✝: βinr.inlSum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inr (inl val✝))) =   inr (inl val✝)α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418val✝: γinr.inrSum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr) (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr) (inr (inr val✝))) =   inr (inr val✝) α: Type ?u.19421β: Type ?u.19420γ: Type ?u.19418Function.RightInverse (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr))
(Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr))rflGoals accomplished! 🐙⟩
#align equiv.sum_assoc Equiv.sumAssoc: (α : Type u_1) → (β : Type u_2) → (γ : Type u_3) → (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γEquiv.sumAssoc

@[simp]
theorem sumAssoc_apply_inl_inl: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α), ↑(sumAssoc α β γ) (inl (inl a)) = inl asumAssoc_apply_inl_inl (a: unknown metavariable '?_uniq.19929'a) : sumAssoc: (α : Type ?u.19946) → (β : Type ?u.19945) → (γ : Type ?u.19944) → (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γsumAssoc α: ?m.19915α β: ?m.19926β γ: ?m.19937γ (inl: {α : Type ?u.20019} → {β : Type ?u.20018} → α → α ⊕ βinl (inl: {α : Type ?u.20025} → {β : Type ?u.20024} → α → α ⊕ βinl a: ?m.19940a)) = inl: {α : Type ?u.20031} → {β : Type ?u.20030} → α → α ⊕ βinl a: ?m.19940a :=
rfl: ∀ {α : Sort ?u.20076} {a : α}, a = arfl
#align equiv.sum_assoc_apply_inl_inl Equiv.sumAssoc_apply_inl_inl: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α), ↑(sumAssoc α β γ) (inl (inl a)) = inl aEquiv.sumAssoc_apply_inl_inl

@[simp]
theorem sumAssoc_apply_inl_inr: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β), ↑(sumAssoc α β γ) (inl (inr b)) = inr (inl b)sumAssoc_apply_inl_inr (b: unknown metavariable '?_uniq.20150'b) : sumAssoc: (α : Type ?u.20167) → (β : Type ?u.20166) → (γ : Type ?u.20165) → (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γsumAssoc α: ?m.20136α β: ?m.20147β γ: ?m.20158γ (inl: {α : Type ?u.20240} → {β : Type ?u.20239} → α → α ⊕ βinl (inr: {α : Type ?u.20246} → {β : Type ?u.20245} → β → α ⊕ βinr b: ?m.20161b)) = inr: {α : Type ?u.20252} → {β : Type ?u.20251} → β → α ⊕ βinr (inl: {α : Type ?u.20256} → {β : Type ?u.20255} → α → α ⊕ βinl b: ?m.20161b) :=
rfl: ∀ {α : Sort ?u.20303} {a : α}, a = arfl
#align equiv.sum_assoc_apply_inl_inr Equiv.sumAssoc_apply_inl_inr: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β), ↑(sumAssoc α β γ) (inl (inr b)) = inr (inl b)Equiv.sumAssoc_apply_inl_inr

@[simp]
theorem sumAssoc_apply_inr: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ), ↑(sumAssoc α β γ) (inr c) = inr (inr c)sumAssoc_apply_inr (c: unknown metavariable '?_uniq.20366'c) : sumAssoc: (α : Type ?u.20394) → (β : Type ?u.20393) → (γ : Type ?u.20392) → (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γsumAssoc α: ?m.20363α β: ?m.20374β γ: ?m.20385γ (inr: {α : Type ?u.20467} → {β : Type ?u.20466} → β → α ⊕ βinr c: ?m.20388c) = inr: {α : Type ?u.20473} → {β : Type ?u.20472} → β → α ⊕ βinr (inr: {α : Type ?u.20477} → {β : Type ?u.20476} → β → α ⊕ βinr c: ?m.20388c) :=
rfl: ∀ {α : Sort ?u.20524} {a : α}, a = arfl
#align equiv.sum_assoc_apply_inr Equiv.sumAssoc_apply_inr: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ), ↑(sumAssoc α β γ) (inr c) = inr (inr c)Equiv.sumAssoc_apply_inr

@[simp]
theorem sumAssoc_symm_apply_inl: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α), ↑(sumAssoc α β γ).symm (inl a) = inl (inl a)sumAssoc_symm_apply_inl {α: Type u_1α β: ?m.20576β γ: ?m.20579γ} (a: ?m.20582a) : (sumAssoc: (α : Type ?u.20588) → (β : Type ?u.20587) → (γ : Type ?u.20586) → (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γsumAssoc α: ?m.20573α β: ?m.20576β γ: ?m.20579γ).symm: {α : Sort ?u.20590} → {β : Sort ?u.20589} → α ≃ β → β ≃ αsymm (inl: {α : Type ?u.20668} → {β : Type ?u.20667} → α → α ⊕ βinl a: ?m.20582a) = inl: {α : Type ?u.20674} → {β : Type ?u.20673} → α → α ⊕ βinl (inl: {α : Type ?u.20678} → {β : Type ?u.20677} → α → α ⊕ βinl a: ?m.20582a) :=
rfl: ∀ {α : Sort ?u.20731} {a : α}, a = arfl
#align equiv.sum_assoc_symm_apply_inl Equiv.sumAssoc_symm_apply_inl: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α), ↑(sumAssoc α β γ).symm (inl a) = inl (inl a)Equiv.sumAssoc_symm_apply_inl

@[simp]
theorem sumAssoc_symm_apply_inr_inl: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β), ↑(sumAssoc α β γ).symm (inr (inl b)) = inl (inr b)sumAssoc_symm_apply_inr_inl {α: ?m.20783α β: ?m.20786β γ: Type u_3γ} (b: ?m.20792b) :
(sumAssoc: (α : Type ?u.20798) → (β : Type ?u.20797) → (γ : Type ?u.20796) → (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γsumAssoc α: ?m.20783α β: ?m.20786β γ: ?m.20789γ).symm: {α : Sort ?u.20800} → {β : Sort ?u.20799} → α ≃ β → β ≃ αsymm (inr: {α : Type ?u.20878} → {β : Type ?u.20877} → β → α ⊕ βinr (inl: {α : Type ?u.20884} → {β : Type ?u.20883} → α → α ⊕ βinl b: ?m.20792b)) = inl: {α : Type ?u.20890} → {β : Type ?u.20889} → α → α ⊕ βinl (inr: {α : Type ?u.20894} → {β : Type ?u.20893} → β → α ⊕ βinr b: ?m.20792b) :=
rfl: ∀ {α : Sort ?u.20947} {a : α}, a = arfl
#align equiv.sum_assoc_symm_apply_inr_inl Equiv.sumAssoc_symm_apply_inr_inl: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β), ↑(sumAssoc α β γ).symm (inr (inl b)) = inl (inr b)Equiv.sumAssoc_symm_apply_inr_inl

@[simp]
theorem sumAssoc_symm_apply_inr_inr: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ), ↑(sumAssoc α β γ).symm (inr (inr c)) = inr csumAssoc_symm_apply_inr_inr {α: Type u_1α β: ?m.21005β γ: Type u_3γ} (c: ?m.21011c) : (sumAssoc: (α : Type ?u.21017) → (β : Type ?u.21016) → (γ : Type ?u.21015) → (α ⊕ β) ⊕ γ ≃ α ⊕ β ⊕ γsumAssoc α: ?m.21002α β: ?m.21005β γ: ?m.21008γ).symm: {α : Sort ?u.21019} → {β : Sort ?u.21018} → α ≃ β → β ≃ αsymm (inr: {α : Type ?u.21097} → {β : Type ?u.21096} → β → α ⊕ βinr (inr: {α : Type ?u.21103} → {β : Type ?u.21102} → β → α ⊕ βinr c: ?m.21011c)) = inr: {α : Type ?u.21109} → {β : Type ?u.21108} → β → α ⊕ βinr c: ?m.21011c :=
rfl: ∀ {α : Sort ?u.21154} {a : α}, a = arfl
#align equiv.sum_assoc_symm_apply_inr_inr Equiv.sumAssoc_symm_apply_inr_inr: ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ), ↑(sumAssoc α β γ).symm (inr (inr c)) = inr cEquiv.sumAssoc_symm_apply_inr_inr

/-- Sum with `IsEmpty` is equivalent to the original type. -/
@[simps symm_apply: ∀ (α : Type u_1) (β : Type u_2) [inst : IsEmpty β] (val : α), ↑(sumEmpty α β).symm val = inl valsymm_apply]
def sumEmpty: (α : Type u_1) → (β : Type u_2) → [inst : IsEmpty β] → α ⊕ β ≃ αsumEmpty (α: Type ?u.21221α β: ?m.21212β) [IsEmpty: Sort ?u.21215 → PropIsEmpty β: ?m.21212β] : Sum: Type ?u.21221 → Type ?u.21220 → Type (max?u.21221?u.21220)Sum α: ?m.21209α β: ?m.21212β ≃ α: ?m.21209α where
toFun := Sum.elim: {α : Type ?u.21234} → {β : Type ?u.21233} → {γ : Sort ?u.21232} → (α → γ) → (β → γ) → α ⊕ β → γSum.elim id: {α : Sort ?u.21242} → α → αid isEmptyElim: {α : Sort ?u.21248} → [inst : IsEmpty α] → {p : α → Sort ?u.21247} → (a : α) → p aisEmptyElim
invFun := inl: {α : Type ?u.21295} → {β : Type ?u.21294} → α → α ⊕ βinl
left_inv s: ?m.21302s := byGoals accomplished! 🐙
α: Type ?u.21221β: Type ?u.21220inst✝: IsEmpty βs: α ⊕ βinl (Sum.elim id (fun a => isEmptyElim a) s) = srcases s: α ⊕ βs with (_ | x): α ⊕ β(_: α__ | x: α ⊕ β | x: βx(_ | x): α ⊕ β)α: Type ?u.21221β: Type ?u.21220inst✝: IsEmpty βval✝: αinlinl (Sum.elim id (fun a => isEmptyElim a) (inl val✝)) = inl val✝α: Type ?u.21221β: Type ?u.21220inst✝: IsEmpty βx: βinrinl (Sum.elim id (fun a => isEmptyElim a) (inr x)) = inr x
α: Type ?u.21221β: Type ?u.21220inst✝: IsEmpty βs: α ⊕ βinl (Sum.elim id (fun a => isEmptyElim a) s) = s·α: Type ?u.21221β: Type ?u.21220inst✝: IsEmpty βval✝: αinlinl (Sum.elim id (fun a => isEmptyElim a) (inl val✝)) = inl val✝ α: Type ?u.21221β: Type ?u.21220inst✝: IsEmpty βval✝: αinlinl (Sum.elim id (fun a => isEmptyElim a) (inl val✝)) = inl val✝α: Type ?u.21221β: Type ?u.21220inst✝: IsEmpty βx: βinrinl (Sum.elim id (fun a => isEmptyElim a) (inr x)) = inr xrflGoals accomplished! 🐙
α: Type ?u.21221β: Type ?u.21220inst✝: IsEmpty βs: α ⊕ βinl (Sum.elim id (fun a => isEmptyElim a) s) = s·α: Type ?u.21221β: Type ?u.21220inst✝: IsEmpty βx: βinrinl (Sum.elim id (fun a => isEmptyElim a) (inr x)) = inr x α: Type ?u.21221β: Type ?u.21220inst✝: IsEmpty βx: βinrinl (Sum.elim id (fun a => isEmptyElim a) (inr x)) = inr xexact isEmptyElim: ∀ {α : Sort ?u.21363} [inst : IsEmpty α] {p : α → Sort ?u.21362} (a : α), p aisEmptyElim x: βxGoals accomplished! 🐙
right_inv _: ?m.21308_ := rfl: ∀ {α : Sort ?u.21310} {a : α}, a = arfl
#align equiv.sum_empty Equiv.sumEmpty: (α : Type u_1) → (β : Type u_2) → [inst : IsEmpty β] → α ⊕ β ≃ αEquiv.sumEmpty
#align equiv.sum_empty_symm_apply Equiv.sumEmpty_symm_apply: ∀ (α : Type u_1) (β : Type u_2) [inst : IsEmpty β] (val : α), ↑(sumEmpty α β).symm val = inl valEquiv.sumEmpty_symm_apply

@[simp]
theorem sumEmpty_apply_inl: ∀ {β : Type u_1} {α : Type u_2} [inst : IsEmpty β] (a : α), ↑(sumEmpty α β) (inl a) = asumEmpty_apply_inl [IsEmpty: Sort ?u.21482 → PropIsEmpty β: ?m.21479β] (a: αa : α: ?m.21486α) : sumEmpty: (α : Type ?u.21496) → (β : Type ?u.21495) → [inst : IsEmpty β] → α ⊕ β ≃ αsumEmpty α: ?m.21486α β: ?m.21479β (Sum.inl: {α : Type ?u.21563} → {β : Type ?u.21562} → α → α ⊕ βSum.inl a: αa) = a: αa :=
rfl: ∀ {α : Sort ?u.21575} {a : α}, a = arfl
#align equiv.sum_empty_apply_inl Equiv.sumEmpty_apply_inl: ∀ {β : Type u_1} {α : Type u_2} [inst : IsEmpty β] (a : α), ↑(sumEmpty α β) (inl a) = aEquiv.sumEmpty_apply_inl

/-- The sum of `IsEmpty` with any type is equivalent to that type. -/
@[simps! symm_apply: ∀ (α : Type u_1) (β : Type u_2) [inst : IsEmpty α] (a : β), ↑(emptySum α β).symm a = inr asymm_apply]
def emptySum: (α : Type ?u.21627) → (β : Type ?u.21626) → [inst : IsEmpty α] → α ⊕ β ≃ βemptySum (α: ?m.21615α β: Type ?u.21626β) [IsEmpty: Sort ?u.21621 → PropIsEmpty α: ?m.21615α] : Sum: Type ?u.21627 → Type ?u.21626 → Type (max?u.21627?u.21626)Sum α: ?m.21615α β: ?m.21618β ≃ β: ?m.21618β :=
(sumComm: (α : Type ?u.21633) → (β : Type ?u.21632) → α ⊕ β ≃ β ⊕ αsumComm _: Type ?u.21633_ _: Type ?u.21632_).trans: {α : Sort ?u.21638} → {β : Sort ?u.21637} → {γ : Sort ?u.21636} → α ≃ β → β ≃ γ → α ≃ γtrans <| sumEmpty: (α : Type ?u.21654) → (β : Type ?u.21653) → [inst : IsEmpty β] → α ⊕ β ≃ αsumEmpty _: Type ?u.21654_ _: Type ?u.21653_
#align equiv.empty_sum Equiv.emptySum: (α : Type u_1) → (β : Type u_2) → [inst : IsEmpty α] → α ⊕ β ≃ βEquiv.emptySum
#align equiv.empty_sum_symm_apply Equiv.emptySum_symm_apply: ∀ (α : Type u_1) (β : Type u_2) [inst : IsEmpty α] (a : β), ↑(emptySum α β).symm a = inr aEquiv.emptySum_symm_apply

@[simp]
theorem emptySum_apply_inr: ∀ {α : Type u_1} {β : Type u_2} [inst : IsEmpty α] (b : β), ↑(emptySum α β) (inr b) = bemptySum_apply_inr [IsEmpty: Sort ?u.21855 → PropIsEmpty α: ?m.21852α] (b: βb : β: ?m.21859β) : emptySum: (α : Type ?u.21869) → (β : Type ?u.21868) → [inst : IsEmpty α] → α ⊕ β ≃ βemptySum α: ?m.21852α β: ?m.21859β (Sum.inr: {α : Type ?u.21936} → {β : Type ?u.21935} → β → α ⊕ βSum.inr b: βb) = b: βb :=
rfl: ∀ {α : Sort ?u.21948} {a : α}, a = arfl
#align equiv.empty_sum_apply_inr Equiv.emptySum_apply_inr: ∀ {α : Type u_1} {β : Type u_2} [inst : IsEmpty α] (b : β), ↑(emptySum α β) (inr b) = bEquiv.emptySum_apply_inr

/-- `Option α` is equivalent to `α ⊕ PUnit` -/
def optionEquivSumPUnit: (α : Type ?u.21993) → Option α ≃ α ⊕ PUnitoptionEquivSumPUnit (α: ?m.21988α) : Option: Type ?u.21993 → Type ?u.21993Option α: ?m.21988α ≃ Sum: Type ?u.21995 → Type ?u.21994 → Type (max?u.21995?u.21994)Sum α: ?m.21988α PUnit: Sort ?u.21996PUnit :=
⟨fun o: ?m.22012o => o: ?m.22012o.elim: {α : Type ?u.22015} → {β : Sort ?u.22014} → Option α → β → (α → β) → βelim (inr: {α : Type ?u.22025} → {β : Type ?u.22024} → β → α ⊕ βinr PUnit.unit: PUnitPUnit.unit) inl: {α : Type ?u.22032} → {β : Type ?u.22031} → α → α ⊕ βinl, fun s: ?m.22041s => s: ?m.22041s.elim: {α : Type ?u.22045} → {β : Type ?u.22044} → {γ : Sort ?u.22043} → (α → γ) → (β → γ) → α ⊕ β → γelim some: {α : Type ?u.22055} → α → Option αsome fun _: ?m.22061_ => none: {α : Type ?u.22063} → Option αnone,
fun o: ?m.22070o => byGoals accomplished! 🐙 α: Type ?u.21993o: Option α(fun s => Sum.elim some (fun x => none) s) ((fun o => Option.elim o (inr PUnit.unit) inl) o) = ocases o: Option αoα: Type ?u.21993none(fun s => Sum.elim some (fun x => none) s) ((fun o => Option.elim o (inr PUnit.unit) inl) none) = noneα: Type ?u.21993val✝: αsome(fun s => Sum.elim some (fun x => none) s) ((fun o => Option.elim o (inr PUnit.unit) inl) (some val✝)) = some val✝ α: Type ?u.21993o: Option α(fun s => Sum.elim some (fun x => none) s) ((fun o => Option.elim o (inr PUnit.unit) inl) o) = o<;>α: Type ?u.21993none(fun s => Sum.elim some (fun x => none) s) ((fun o => Option.elim o (inr PUnit.unit) inl) none) = noneα: Type ?u.21993val✝: αsome(fun s => Sum.elim some (fun x => none) s) ((fun o => Option.elim o (inr PUnit.unit) inl) (some val✝)) = some val✝ α: Type ?u.21993o: Option α(fun s => Sum.elim some (fun x => none) s) ((fun o => Option.elim o (inr PUnit.unit) inl) o) = orflGoals accomplished! 🐙,
fun s: ?m.22076s => byGoals accomplished! 🐙 α: Type ?u.21993s: α ⊕ PUnit(fun o => Option.elim o (inr PUnit.unit) inl) ((fun s => Sum.elim some (fun x => none) s) s) = srcases s: α ⊕ PUnits with (_ | ⟨⟨⟩⟩): α ⊕ PUnit(_: α__ | ⟨⟨⟩⟩: α ⊕ PUnit | ⟨⟨⟩: PUnit⟨⟩_ | ⟨⟨⟩⟩: α ⊕ PUnit⟩(_ | ⟨⟨⟩⟩): α ⊕ PUnit)α: Type ?u.21993val✝: αinl(fun o => Option.elim o (inr PUnit.unit) inl) ((fun s => Sum.elim some (fun x => none) s) (inl val✝)) = inl val✝α: Type ?u.21993inr.unit(fun o => Option.elim o (inr PUnit.unit) inl) ((fun s => Sum.elim some (fun x => none) s) (inr PUnit.unit)) =   inr PUnit.unit α: Type ?u.21993s: α ⊕ PUnit(fun o => Option.elim o (inr PUnit.unit) inl) ((fun s => Sum.elim some (fun x => none) s) s) = s<;>α: Type ?u.21993val✝: αinl(fun o => Option.elim o (inr PUnit.unit) inl) ((fun s => Sum.elim some (fun x => none) s) (inl val✝)) = inl val✝α: Type ?u.21993inr.unit(fun o => Option.elim o (inr PUnit.unit) inl) ((fun s => Sum.elim some (fun x => none) s) (inr PUnit.unit)) =   inr PUnit.unit α: Type ?u.21993s: α ⊕ PUnit(fun o => Option.elim o (inr PUnit.unit) inl) ((fun s => Sum.elim some (fun x => none) s) s) = srflGoals accomplished! 🐙⟩
#align equiv.option_equiv_sum_punit Equiv.optionEquivSumPUnit: (α : Type u_1) → Option α ≃ α ⊕ PUnitEquiv.optionEquivSumPUnit

@[simp]
theorem optionEquivSumPUnit_none: ∀ {α : Type u_1}, ↑(optionEquivSumPUnit α) none = inr PUnit.unitoptionEquivSumPUnit_none : optionEquivSumPUnit: (α : Type ?u.22367) → Option α ≃ α ⊕ PUnitoptionEquivSumPUnit α: ?m.22362α none: {α : Type ?u.22435} → Option αnone = Sum.inr: {α : Type ?u.22439} → {β : Type ?u.22438} → β → α ⊕ βSum.inr PUnit.unit: PUnitPUnit.unit :=
rfl: ∀ {α : Sort ?u.22482} {a : α}, a = arfl
#align equiv.option_equiv_sum_punit_none Equiv.optionEquivSumPUnit_none: ∀ {α : Type u_1}, ↑(optionEquivSumPUnit α) none = inr PUnit.unitEquiv.optionEquivSumPUnit_none

@[simp]
theorem optionEquivSumPUnit_some: ∀ {α : Type u_1} (a : α), ↑(optionEquivSumPUnit α) (some a) = inl aoptionEquivSumPUnit_some (a: αa) : optionEquivSumPUnit: (α : Type ?u.22540) → Option α ≃ α ⊕ PUnitoptionEquivSumPUnit α: ?m.22532α (some: {α : Type ?u.22608} → α → Option αsome a: ?m.22535a) = Sum.inl: {α : Type ?u.22612} → {β : Type ?u.22611} → α → α ⊕ βSum.inl a: ?m.22535a :=
rfl: ∀ {α : Sort ?u.22655} {a : α}, a = arfl
#align equiv.option_equiv_sum_punit_some Equiv.optionEquivSumPUnit_some: ∀ {α : Type u_1} (a : α), ↑(optionEquivSumPUnit α) (some a) = inl aEquiv.optionEquivSumPUnit_some

@[simp]
theorem optionEquivSumPUnit_coe: ∀ {α : Type u_1} (a : α), ↑(optionEquivSumPUnit α) (some a) = inl aoptionEquivSumPUnit_coe (a: αa : α: ?m.22703α) : optionEquivSumPUnit: (α : Type ?u.22710) → Option α ≃ α ⊕ PUnitoptionEquivSumPUnit α: ?m.22703α a: αa = Sum.inl: {α : Type ?u.22861} → {β : Type ?u.22860} → α → α ⊕ βSum.inl a: αa :=
rfl: ∀ {α : Sort ?u.22904} {a : α}, a = arfl
#align equiv.option_equiv_sum_punit_coe Equiv.optionEquivSumPUnit_coe: ∀ {α : Type u_1} (a : α), ↑(optionEquivSumPUnit α) (some a) = inl aEquiv.optionEquivSumPUnit_coe

@[simp]
theorem optionEquivSumPUnit_symm_inl: ∀ {α : Type u_1} (a : α), ↑(optionEquivSumPUnit α).symm (inl a) = some aoptionEquivSumPUnit_symm_inl (a: αa) : (optionEquivSumPUnit: (α : Type ?u.22966) → Option α ≃ α ⊕ PUnitoptionEquivSumPUnit α: ?m.22958α).symm: {α : Sort ?u.22968} → {β : Sort ?u.22967} → α ≃ β → β ≃ αsymm (Sum.inl: {α : Type ?u.23040} → {β : Type ?u.23039} → α → α ⊕ βSum.inl a: ?m.22961a) = a: ?m.22961a :=
rfl: ∀ {α : Sort ?u.23221} {a : α}, a = arfl
#align equiv.option_equiv_sum_punit_symm_inl Equiv.optionEquivSumPUnit_symm_inl: ∀ {α : Type u_1} (a : α), ↑(optionEquivSumPUnit α).symm (inl a) = some aEquiv.optionEquivSumPUnit_symm_inl

@[simp]
theorem optionEquivSumPUnit_symm_inr: ∀ {α : Type u_1} (a : PUnit), ↑(optionEquivSumPUnit α).symm (inr a) = noneoptionEquivSumPUnit_symm_inr (a: PUnita) : (optionEquivSumPUnit: (α : Type ?u.23272) → Option α ≃ α ⊕ PUnitoptionEquivSumPUnit α: ?m.23264α).symm: {α : Sort ?u.23274} → {β : Sort ?u.23273} → α ≃ β → β ≃ αsymm (Sum.inr: {α : Type ?u.23346} → {β : Type ?u.23345} → β → α ⊕ βSum.inr a: ?m.23267a) = none: {α : Type ?u.23351} → Option αnone :=
rfl: ∀ {α : Sort ?u.23389} {a : α}, a = arfl
#align equiv.option_equiv_sum_punit_symm_inr Equiv.optionEquivSumPUnit_symm_inr: ∀ {α : Type u_1} (a : PUnit), ↑(optionEquivSumPUnit α).symm (inr a) = noneEquiv.optionEquivSumPUnit_symm_inr

/-- The set of `x : Option α` such that `isSome x` is equivalent to `α`. -/
@[simps: ∀ (α : Type u_1) (x : α), ↑(↑(optionIsSomeEquiv α).symm x) = some xsimps]
def optionIsSomeEquiv: (α : Type u_1) → { x // Option.isSome x = true } ≃ αoptionIsSomeEquiv (α: Type ?u.23433α) : { x: Option αx : Option: Type ?u.23433 → Type ?u.23433Option α: ?m.23425α // x: Option αx.isSome: {α : Type ?u.23435} → Option α → BoolisSome } ≃ α: ?m.23425α where
toFun o: ?m.23530o := Option.get: {α : Type ?u.23532} → (o : Option α) → Option.isSome o = true → αOption.get _: Option ?m.23533_ o: ?m.23530o.2: ∀ {α : Sort ?u.23535} {p : α → Prop} (self : Subtype p), p ↑self2
invFun x: ?m.23551x := ⟨some: {α : Type ?u.23562} → α → Option αsome x: ?m.23551x, rfl: ∀ {α : Sort ?u.23564} {a : α}, a = arfl⟩
left_inv _: ?m.23584_ := Subtype.eq: ∀ {α : Type ?u.23586} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2Subtype.eq <| ```