data.equiv.basic

# Equivalence between types

In this file we define two types:

• `equiv α β` a.k.a. `α ≃ β`: a bijective map `α → β` bundled with its inverse map; we use this (and not equality!) to express that various `Type`s or `Sort`s are equivalent.

• `equiv.perm α`: the group of permutations `α ≃ α`.

Then we define

• canonical isomorphisms between various types: e.g.,

• `equiv.refl α` is the identity map interpreted as `α ≃ α`;

• `equiv.sum_equiv_sigma_bool` is the canonical equivalence between the sum of two types `α ⊕ β` and the sigma-type `Σ b : bool, cond b α β`;

• `equiv.prod_sum_distrib : α × (β ⊕ γ) ≃ (α × β) ⊕ (α × γ)` shows that type product and type sum satisfy the distributive law up to a canonical equivalence;

• operations on equivalences: e.g.,

• `equiv.symm e : β ≃ α` is the inverse of `e : α ≃ β`;

• `equiv.trans e₁ e₂ : α ≃ γ` is the composition of `e₁ : α ≃ β` and `e₂ : β ≃ γ` (note the order of the arguments!);

• `equiv.prod_congr ea eb : α₁ × β₁ ≃ α₂ × β₂`: combine two equivalences `ea : α₁ ≃ α₂` and `eb : β₁ ≃ β₂` using `prod.map`.

• definitions that transfer some instances along an equivalence. By convention, we transfer instances from right to left.

• `equiv.inhabited` takes `e : α ≃ β` and `[inhabited β]` and returns `inhabited α`;
• `equiv.unique` takes `e : α ≃ β` and `[unique β]` and returns `unique α`;
• `equiv.decidable_eq` takes `e : α ≃ β` and `[decidable_eq β]` and returns `decidable_eq α`.

More definitions of this kind can be found in other files. E.g., `data/equiv/transfer_instance` does it for many algebraic type classes like `group`, `module`, etc.

• group structure on `equiv.perm α`. More lemmas about `equiv.perm` can be found in `data/equiv/perm`.

## Tags

equivalence, congruence, bijective map

@[nolint]
structure equiv  :
Sort u_1Sort u_2Sort (max 1 (imax u_1 u_2) (imax u_2 u_1))
• to_fun : α → β
• inv_fun : β → α
• left_inv :
• right_inv :

`α ≃ β` is the type of functions from `α → β` with a two-sided inverse.

def function.involutive.to_equiv {α : Sort u} (f : α → α) :
α α

Convert an involutive function `f` to an equivalence with `to_fun = inv_fun = f`.

Equations
def equiv.perm  :
Sort u_1Sort (max 1 u_1)

`perm α` is the type of bijections from `α` to itself.

Equations
@[instance]
def equiv.has_coe_to_fun {α : Sort u} {β : Sort v} :

Equations
@[simp]
theorem equiv.coe_fn_mk {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : f) (r : f) :
{to_fun := f, inv_fun := g, left_inv := l, right_inv := r} = f

theorem equiv.injective_coe_fn {α : Sort u} {β : Sort v} :
function.injective (λ (e : α β) (x : α), e x)

The map `coe_fn : (r ≃ s) → (r → s)` is injective.

@[simp]
theorem equiv.coe_inj {α : Sort u} {β : Sort v} {e₁ e₂ : α β} :
e₁ = e₂ e₁ = e₂

@[ext]
theorem equiv.ext {α : Sort u} {β : Sort v} {f g : α β} :
(∀ (x : α), f x = g x)f = g

@[ext]
theorem equiv.perm.ext {α : Sort u} {σ τ : equiv.perm α} :
(∀ (x : α), σ x = τ x)σ = τ

theorem equiv.ext_iff {α : Sort u} {β : Sort v} {f g : α β} :
f = g ∀ (x : α), f x = g x

theorem equiv.perm.ext_iff {α : Sort u} {σ τ : equiv.perm α} :
σ = τ ∀ (x : α), σ x = τ x

def equiv.refl (α : Sort u_1) :
α α

Any type is equivalent to itself.

Equations
@[instance]
def equiv.inhabited' {α : Sort u} :
inhabited α)

Equations
def equiv.symm {α : Sort u} {β : Sort v} :
α ββ α

Inverse of an equivalence `e : α ≃ β`.

Equations
def equiv.simps.inv_fun {α : Sort u} {β : Sort v} :
α ββ → α
Equations
def equiv.trans {α : Sort u} {β : Sort v} {γ : Sort w} :
α ββ γα γ

Composition of equivalences `e₁ : α ≃ β` and `e₂ : β ≃ γ`.

Equations
@[simp]
theorem equiv.to_fun_as_coe {α : Sort u} {β : Sort v} (e : α β) :

@[simp]
theorem equiv.inv_fun_as_coe {α : Sort u} {β : Sort v} (e : α β) :

theorem equiv.injective {α : Sort u} {β : Sort v} (e : α β) :

theorem equiv.surjective {α : Sort u} {β : Sort v} (e : α β) :

theorem equiv.bijective {α : Sort u} {β : Sort v} (f : α β) :

@[simp]
theorem equiv.range_eq_univ {α : Type u_1} {β : Type u_2} (e : α β) :

theorem equiv.subsingleton {α : Sort u} {β : Sort v} (e : α β) [subsingleton β] :

def equiv.decidable_eq {α : Sort u} {β : Sort v} (e : α β) [decidable_eq β] :

Transfer `decidable_eq` across an equivalence.

Equations
theorem equiv.nonempty_iff_nonempty {α : Sort u} {β : Sort v} :
α β(nonempty α nonempty β)

def equiv.inhabited {α : Sort u} {β : Sort v} [inhabited β] :
α β

If `α ≃ β` and `β` is inhabited, then so is `α`.

Equations
def equiv.unique {α : Sort u} {β : Sort v} [unique β] :
α β

If `α ≃ β` and `β` is a singleton type, then so is `α`.

Equations
def equiv.cast {α β : Sort u_1} :
α = βα β

Equivalence between equal types.

Equations
@[simp]
theorem equiv.coe_fn_symm_mk {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : f) (r : f) :
({to_fun := f, inv_fun := g, left_inv := l, right_inv := r}.symm) = g

@[simp]
theorem equiv.coe_refl {α : Sort u} :

theorem equiv.refl_apply {α : Sort u} (x : α) :
(equiv.refl α) x = x

@[simp]
theorem equiv.coe_trans {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) :
(f.trans g) = g f

theorem equiv.trans_apply {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) (a : α) :
(f.trans g) a = g (f a)

@[simp]
theorem equiv.apply_symm_apply {α : Sort u} {β : Sort v} (e : α β) (x : β) :
e ((e.symm) x) = x

@[simp]
theorem equiv.symm_apply_apply {α : Sort u} {β : Sort v} (e : α β) (x : α) :
(e.symm) (e x) = x

@[simp]
theorem equiv.symm_comp_self {α : Sort u} {β : Sort v} (e : α β) :

@[simp]
theorem equiv.self_comp_symm {α : Sort u} {β : Sort v} (e : α β) :

@[simp]
theorem equiv.symm_trans_apply {α : Sort u} {β : Sort v} {γ : Sort w} (f : α β) (g : β γ) (a : γ) :
((f.trans g).symm) a = (f.symm) ((g.symm) a)

@[simp]
theorem equiv.apply_eq_iff_eq {α : Sort u} {β : Sort v} (f : α β) {x y : α} :
f x = f y x = y

theorem equiv.apply_eq_iff_eq_symm_apply {α : Sort u_1} {β : Sort u_2} (f : α β) {x : α} {y : β} :
f x = y x = (f.symm) y

@[simp]
theorem equiv.cast_apply {α β : Sort u_1} (h : α = β) (x : α) :
(equiv.cast h) x = cast h x

theorem equiv.symm_apply_eq {α : Sort u_1} {β : Sort u_2} (e : α β) {x : β} {y : α} :
(e.symm) x = y x = e y

theorem equiv.eq_symm_apply {α : Sort u_1} {β : Sort u_2} (e : α β) {x : β} {y : α} :
y = (e.symm) x e y = x

@[simp]
theorem equiv.symm_symm {α : Sort u} {β : Sort v} (e : α β) :
e.symm.symm = e

@[simp]
theorem equiv.trans_refl {α : Sort u} {β : Sort v} (e : α β) :
e.trans (equiv.refl β) = e

@[simp]
theorem equiv.refl_symm {α : Sort u} :

@[simp]
theorem equiv.refl_trans {α : Sort u} {β : Sort v} (e : α β) :
(equiv.refl α).trans e = e

@[simp]
theorem equiv.symm_trans {α : Sort u} {β : Sort v} (e : α β) :
e.symm.trans e =

@[simp]
theorem equiv.trans_symm {α : Sort u} {β : Sort v} (e : α β) :
e.trans e.symm =

theorem equiv.trans_assoc {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α β) (bc : β γ) (cd : γ δ) :
(ab.trans bc).trans cd = ab.trans (bc.trans cd)

theorem equiv.left_inverse_symm {α : Sort u} {β : Sort v} (f : α β) :

theorem equiv.right_inverse_symm {α : Sort u} {β : Sort v} (f : α β) :

def equiv.equiv_congr {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} :
α βγ δα γ δ)

If `α` is equivalent to `β` and `γ` is equivalent to `δ`, then the type of equivalences `α ≃ γ` is equivalent to the type of equivalences `β ≃ δ`.

Equations
def equiv.perm_congr {α : Type u_1} {β : Type u_2} :
α β

If `α` is equivalent to `β`, then `perm α` is equivalent to `perm β`.

Equations
theorem equiv.image_eq_preimage {α : Type u_1} {β : Type u_2} (e : α β) (s : set α) :
e '' s = (e.symm) ⁻¹' s

theorem equiv.subset_image {α : Type u_1} {β : Type u_2} (e : α β) (s : set α) (t : set β) :
t e '' s (e.symm) '' t s

theorem equiv.symm_image_image {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) :
(f.symm) '' (f '' s) = s

theorem equiv.image_compl {α : Type u_1} {β : Type u_2} (f : α β) (s : set α) :
f '' s = (f '' s)

### The group of permutations (self-equivalences) of a type `α`

@[instance]
def equiv.perm.perm_group {α : Type u} :

Equations
theorem equiv.perm.mul_apply {α : Type u} (f g : equiv.perm α) (x : α) :
(f * g) x = f (g x)

@[simp]
theorem equiv.perm.one_apply {α : Type u} (x : α) :
1 x = x

@[simp]
theorem equiv.perm.inv_apply_self {α : Type u} (f : equiv.perm α) (x : α) :
f⁻¹ (f x) = x

@[simp]
theorem equiv.perm.apply_inv_self {α : Type u} (f : equiv.perm α) (x : α) :
f (f⁻¹ x) = x

theorem equiv.perm.one_def {α : Type u} :
1 =

theorem equiv.perm.mul_def {α : Type u} (f g : equiv.perm α) :
f * g = f

theorem equiv.perm.inv_def {α : Type u} (f : equiv.perm α) :

@[simp]
theorem equiv.perm.coe_mul {α : Type u} (f g : equiv.perm α) :
f * g = f g

def equiv.equiv_empty {α : Sort u} :
(α → false)

If `α` is an empty type, then it is equivalent to the `empty` type.

Equations

`false` is equivalent to `empty`.

Equations
def equiv.equiv_pempty {α : Sort v'} :
(α → false)

If `α` is an empty type, then it is equivalent to the `pempty` type in any universe.

Equations

`false` is equivalent to `pempty`.

Equations

`empty` is equivalent to `pempty`.

Equations

`pempty` types from any two universes are equivalent.

Equations
def equiv.empty_of_not_nonempty {α : Sort u_1} :

If `α` is not `nonempty`, then it is equivalent to `empty`.

Equations
def equiv.pempty_of_not_nonempty {α : Sort u_1} :

If `α` is not `nonempty`, then it is equivalent to `pempty`.

Equations
def equiv.prop_equiv_punit {p : Prop} :
p →

The `Sort` of proofs of a true proposition is equivalent to `punit`.

Equations

`true` is equivalent to `punit`.

Equations
@[simp]
theorem equiv.ulift_symm_apply {α : Type v} :
(equiv.ulift.symm) = ulift.up

def equiv.ulift {α : Type v} :
α

`ulift α` is equivalent to `α`.

Equations
@[simp]
theorem equiv.ulift_apply {α : Type v} :

@[simp]
theorem equiv.plift_apply {α : Sort u} :

def equiv.plift {α : Sort u} :
α

`plift α` is equivalent to `α`.

Equations
@[simp]
theorem equiv.plift_symm_apply {α : Sort u} :
(equiv.plift.symm) = plift.up

def equiv.of_iff {P Q : Prop} :
(P Q)P Q

equivalence of propositions is the same as iff

Equations
@[simp]
theorem equiv.arrow_congr_apply {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) (f : α₁ → β₁) (a : α₂) :
(e₁.arrow_congr e₂) f a = (e₂ f (e₁.symm)) a

def equiv.arrow_congr {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} :
α₁ α₂β₁ β₂(α₁ → β₁) (α₂ → β₂)

If `α₁` is equivalent to `α₂` and `β₁` is equivalent to `β₂`, then the type of maps `α₁ → β₁` is equivalent to the type of maps `α₂ → β₂`.

Equations
theorem equiv.arrow_congr_comp {α₁ : Sort u_1} {β₁ : Sort u_2} {γ₁ : Sort u_3} {α₂ : Sort u_4} {β₂ : Sort u_5} {γ₂ : Sort u_6} (ea : α₁ α₂) (eb : β₁ β₂) (ec : γ₁ γ₂) (f : α₁ → β₁) (g : β₁ → γ₁) :
(ea.arrow_congr ec) (g f) = (eb.arrow_congr ec) g (ea.arrow_congr eb) f

@[simp]
theorem equiv.arrow_congr_refl {α : Sort u_1} {β : Sort u_2} :
(equiv.refl β) = equiv.refl (α → β)

@[simp]
theorem equiv.arrow_congr_trans {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} {α₃ : Sort u_5} {β₃ : Sort u_6} (e₁ : α₁ α₂) (e₁' : β₁ β₂) (e₂ : α₂ α₃) (e₂' : β₂ β₃) :
(e₁.trans e₂).arrow_congr (e₁'.trans e₂') = (e₁.arrow_congr e₁').trans (e₂.arrow_congr e₂')

@[simp]
theorem equiv.arrow_congr_symm {α₁ : Sort u_1} {β₁ : Sort u_2} {α₂ : Sort u_3} {β₂ : Sort u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
(e₁.arrow_congr e₂).symm = e₁.symm.arrow_congr e₂.symm

def equiv.arrow_congr' {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} :
α₁ α₂β₁ β₂(α₁ → β₁) (α₂ → β₂)

A version of `equiv.arrow_congr` in `Type`, rather than `Sort`.

The `equiv_rw` tactic is not able to use the default `Sort` level `equiv.arrow_congr`, because Lean's universe rules will not unify `?l_1` with `imax (1 ?m_1)`.

Equations
@[simp]
theorem equiv.arrow_congr'_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (hα : α₁ α₂) (hβ : β₁ β₂) (f : α₁ → β₁) (a : α₂) :
(hα.arrow_congr' hβ) f a = (f ((hα.symm) a))

@[simp]
theorem equiv.arrow_congr'_refl {α : Type u_1} {β : Type u_2} :
(equiv.refl β) = equiv.refl (α → β)

@[simp]
theorem equiv.arrow_congr'_trans {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} {α₃ : Type u_5} {β₃ : Type u_6} (e₁ : α₁ α₂) (e₁' : β₁ β₂) (e₂ : α₂ α₃) (e₂' : β₂ β₃) :
(e₁.trans e₂).arrow_congr' (e₁'.trans e₂') = (e₁.arrow_congr' e₁').trans (e₂.arrow_congr' e₂')

@[simp]
theorem equiv.arrow_congr'_symm {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
(e₁.arrow_congr' e₂).symm = e₁.symm.arrow_congr' e₂.symm

def equiv.conj {α : Sort u} {β : Sort v} :
α β(α → α) (β → β)

Conjugate a map `f : α → α` by an equivalence `α ≃ β`.

Equations
@[simp]
theorem equiv.conj_apply {α : Sort u} {β : Sort v} (e : α β) (f : α → α) (a : β) :
(e.conj) f a = e (f ((e.symm) a))

@[simp]
theorem equiv.conj_refl {α : Sort u} :
(equiv.refl α).conj = equiv.refl (α → α)

@[simp]
theorem equiv.conj_symm {α : Sort u} {β : Sort v} (e : α β) :

@[simp]
theorem equiv.conj_trans {α : Sort u} {β : Sort v} {γ : Sort w} (e₁ : α β) (e₂ : β γ) :
(e₁.trans e₂).conj = e₁.conj.trans e₂.conj

theorem equiv.conj_comp {α : Sort u} {β : Sort v} (e : α β) (f₁ f₂ : α → α) :
(e.conj) (f₁ f₂) = (e.conj) f₁ (e.conj) f₂

theorem equiv.semiconj_conj {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁) :
((e.conj) f)

theorem equiv.semiconj₂_conj {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) :
((e.arrow_congr e.conj) f)

@[instance]
def equiv.is_associative {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) [ f] :

@[instance]
def equiv.is_idempotent {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) [ f] :

@[instance]
def equiv.is_left_cancel {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) [ f] :

@[instance]
def equiv.is_right_cancel {α₁ : Type u_1} {β₁ : Type u_2} (e : α₁ β₁) (f : α₁ → α₁ → α₁) [ f] :

`punit` sorts in any two universes are equivalent.

Equations
def equiv.arrow_punit_equiv_punit (α : Sort u_1) :
(α → punit) punit

The sort of maps to `punit.{v}` is equivalent to `punit.{w}`.

Equations
def equiv.punit_arrow_equiv (α : Sort u_1) :
(punit → α) α

The sort of maps from `punit` is equivalent to the codomain.

Equations
def equiv.empty_arrow_equiv_punit (α : Sort u_1) :
(empty → α) punit

The sort of maps from `empty` is equivalent to `punit`.

Equations
def equiv.pempty_arrow_equiv_punit (α : Sort u_1) :
(pempty → α) punit

The sort of maps from `pempty` is equivalent to `punit`.

Equations
def equiv.false_arrow_equiv_punit (α : Sort u_1) :
(false → α) punit

The sort of maps from `false` is equivalent to `punit`.

Equations
def equiv.prod_congr {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} :
α₁ α₂β₁ β₂α₁ × β₁ α₂ × β₂

Product of two equivalences. If `α₁ ≃ α₂` and `β₁ ≃ β₂`, then `α₁ × β₁ ≃ α₂ × β₂`.

Equations
@[simp]
theorem equiv.prod_congr_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) (x : α₁ × β₁) :
(e₁.prod_congr e₂) x = e₂ x

@[simp]
theorem equiv.prod_congr_symm {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (e₁ : α₁ α₂) (e₂ : β₁ β₂) :
(e₁.prod_congr e₂).symm = e₁.symm.prod_congr e₂.symm

def equiv.prod_comm (α : Type u_1) (β : Type u_2) :
α × β β × α

Type product is commutative up to an equivalence: `α × β ≃ β × α`.

Equations
@[simp]
theorem equiv.prod_comm_apply (α : Type u_1) (β : Type u_2) (a : α × β) :
β) a = a.swap

@[simp]
theorem equiv.prod_comm_symm (α : Type u_1) (β : Type u_2) :
β).symm =

@[simp]
theorem equiv.prod_assoc_symm_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : α × β × γ) :
β γ).symm) p = ((p.fst, p.snd.fst), p.snd.snd)

def equiv.prod_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
× β) × γ α × β × γ

Type product is associative up to an equivalence.

Equations
@[simp]
theorem equiv.prod_assoc_apply (α : Type u_1) (β : Type u_2) (γ : Type u_3) (p : × β) × γ) :
β γ) p = (p.fst.fst, p.fst.snd, p.snd)

theorem equiv.prod_assoc_preimage {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} {t : set β} {u : set γ} :
β γ) ⁻¹' s.prod (t.prod u) = (s.prod t).prod u

def equiv.prod_punit (α : Type u_1) :
α

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

Equations
@[simp]
theorem equiv.prod_punit_apply (α : Type u_1) (p : α × punit) :
p = p.fst

def equiv.punit_prod (α : Type u_1) :
α

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

Equations
@[simp]
theorem equiv.punit_prod_apply (α : Type u_1) (a : punit × α) :
a = a.snd

def equiv.prod_empty (α : Type u_1) :

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

Equations
def equiv.empty_prod (α : Type u_1) :

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

Equations
def equiv.prod_pempty (α : Type u_1) :

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

Equations
def equiv.pempty_prod (α : Type u_1) :

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

Equations
def equiv.psum_equiv_sum (α : Type u_1) (β : Type u_2) :
psum α β α β

`psum` is equivalent to `sum`.

Equations
@[simp]
theorem equiv.sum_congr_apply {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} (ea : α₁ α₂) (eb : β₁ β₂) (a : α₁ β₁) :
(ea.sum_congr eb) a = sum.map ea eb a

def equiv.sum_congr {α₁ : Type u_1} {β₁ : Type u_2} {α₂ : Type u_3} {β₂ : Type u_4} :
α₁ α₂β₁ β₂α₁ β₁ α₂ β₂

If `α ≃ α'` and `β ≃ β'`, then `α ⊕ β ≃ α' ⊕ β'`.

Equations
@[simp]
theorem equiv.sum_congr_symm {α β γ δ : Type u} (e : α β) (f : γ δ) :

`bool` is equivalent the sum of two `punit`s.

Equations

`Prop` is noncomputably equivalent to `bool`.

Equations
@[simp]
theorem equiv.sum_comm_apply (α : Type u_1) (β : Type u_2) (a : α β) :
β) a = a.swap

def equiv.sum_comm (α : Type u_1) (β : Type u_2) :
α β β α

Sum of types is commutative up to an equivalence.

Equations
@[simp]
theorem equiv.sum_comm_symm (α : Type u_1) (β : Type u_2) :
β).symm =

def equiv.sum_assoc (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
β) γ α β γ

Sum of types is associative up to an equivalence.

Equations
@[simp]
theorem equiv.sum_assoc_apply_in1 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) :
β γ) (sum.inl (sum.inl a)) =

@[simp]
theorem equiv.sum_assoc_apply_in2 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) :
β γ) (sum.inl (sum.inr b)) = sum.inr (sum.inl b)

@[simp]
theorem equiv.sum_assoc_apply_in3 {α : Type u_1} {β : Type u_2} {γ : Type u_3} (c : γ) :
β γ) (sum.inr c) = sum.inr (sum.inr c)

def equiv.sum_empty (α : Type u_1) :
α

Sum with `empty` is equivalent to the original type.

Equations
@[simp]
theorem equiv.sum_empty_apply_inl {α : Type u_1} (a : α) :
(sum.inl a) = a

def equiv.empty_sum (α : Type u_1) :
α

The sum of `empty` with any `Sort*` is equivalent to the right summand.

Equations
@[simp]
theorem equiv.empty_sum_apply_inr {α : Type u_1} (a : α) :
(sum.inr a) = a

def equiv.sum_pempty (α : Type u_1) :
α

Sum with `pempty` is equivalent to the original type.

Equations
@[simp]
theorem equiv.sum_pempty_apply_inl {α : Type u_1} (a : α) :
(sum.inl a) = a

def equiv.pempty_sum (α : Type u_1) :
α

The sum of `pempty` with any `Sort*` is equivalent to the right summand.

Equations
@[simp]
theorem equiv.pempty_sum_apply_inr {α : Type u_1} (a : α) :
(sum.inr a) = a

def equiv.option_equiv_sum_punit (α : Type u_1) :

`option α` is equivalent to `α ⊕ punit`

Equations
• = {to_fun := λ (o : option α), equiv.option_equiv_sum_punit._match_1 α o, inv_fun := λ (s : α punit), equiv.option_equiv_sum_punit._match_2 α s, left_inv := _, right_inv := _}
• equiv.option_equiv_sum_punit._match_1 α (some a) =
• equiv.option_equiv_sum_punit._match_1 α none =
• equiv.option_equiv_sum_punit._match_2 α (sum.inr _x) = none
• equiv.option_equiv_sum_punit._match_2 α (sum.inl a) = some a
@[simp]
theorem equiv.option_equiv_sum_punit_none {α : Type u_1} :

@[simp]
theorem equiv.option_equiv_sum_punit_some {α : Type u_1} (a : α) :
=

@[simp]
theorem equiv.option_equiv_sum_punit_coe {α : Type u_1} (a : α) :

@[simp]
theorem equiv.option_equiv_sum_punit_symm_inl {α : Type u_1} (a : α) :
(sum.inl a) = a

@[simp]
theorem equiv.option_equiv_sum_punit_symm_inr {α : Type u_1} (a : punit) :

def equiv.option_is_some_equiv (α : Type u_1) :
{x // (x.is_some)} α

The set of `x : option α` such that `is_some x` is equivalent to `α`.

Equations
def equiv.sum_equiv_sigma_bool (α β : Type u_1) :
α β Σ (b : bool), cond b α β

`α ⊕ β` is equivalent to a `sigma`-type over `bool`.

Equations
• = {to_fun := λ (s : α β), equiv.sum_equiv_sigma_bool._match_1 α β s, inv_fun := λ (s : Σ (b : bool), cond b α β), equiv.sum_equiv_sigma_bool._match_2 α β s, left_inv := _, right_inv := _}
• equiv.sum_equiv_sigma_bool._match_1 α β (sum.inr b) = ff, b⟩
• equiv.sum_equiv_sigma_bool._match_1 α β (sum.inl a) = tt, a⟩
• equiv.sum_equiv_sigma_bool._match_2 α β tt, a⟩ =
• equiv.sum_equiv_sigma_bool._match_2 α β ff, b⟩ =
@[simp]
theorem equiv.sigma_preimage_equiv_symm_apply_fst {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) :
( x).fst = f x

def equiv.sigma_preimage_equiv {α : Type u_1} {β : Type u_2} (f : α → β) :
(Σ (y : β), {x // f x = y}) α

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

Equations
@[simp]
theorem equiv.sigma_preimage_equiv_apply {α : Type u_1} {β : Type u_2} (f : α → β) (x : Σ (y : β), {x // f x = y}) :
= (x.snd)

@[simp]
theorem equiv.sigma_preimage_equiv_symm_apply_snd_coe {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) :
(( x).snd) = x

def equiv.set_prod_equiv_sigma {α : Type u_1} {β : Type u_2} (s : set × β)) :
s Σ (x : α), {y : β | (x, y) s}

A set `s` in `α × β` is equivalent to the sigma-type `Σ x, {y | (x, y) ∈ s}`.

Equations
def equiv.sum_compl {α : Type u_1} (p : α → Prop)  :
{a // p a} {a // ¬p a} α

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

Equations
@[simp]
theorem equiv.sum_compl_apply_inl {α : Type u_1} (p : α → Prop) (x : {a // p a}) :

@[simp]
theorem equiv.sum_compl_apply_inr {α : Type u_1} (p : α → Prop) (x : {a // ¬p a}) :

@[simp]
theorem equiv.sum_compl_apply_symm_of_pos {α : Type u_1} (p : α → Prop) (a : α) (h : p a) :

@[simp]
theorem equiv.sum_compl_apply_symm_of_neg {α : Type u_1} (p : α → Prop) (a : α) (h : ¬p a) :

@[simp]
theorem equiv.subtype_preimage_symm_apply_coe {α : Sort u} {β : Sort v} (p : α → Prop) (x₀ : {a // p a} → β) (x : {a // ¬p a} → β) (a : α) :
( x₀).symm) x) a = dite (p a) (λ (h : p a), x₀ a, h⟩) (λ (h : ¬p a), x a, h⟩)

@[simp]
theorem equiv.subtype_preimage_apply {α : Sort u} {β : Sort v} (p : α → Prop) (x₀ : {a // p a} → β) (x : {x // x coe = x₀}) (a : {a // ¬p a}) :
x₀) x a = x a

def equiv.subtype_preimage {α : Sort u} {β : Sort v} (p : α → Prop) (x₀ : {a // p a} → β) :
{x // x coe = x₀} ({a // ¬p a} → β)

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

Equations
theorem equiv.subtype_preimage_symm_apply_coe_pos {α : Sort u} {β : Sort v} (p : α → Prop) (x₀ : {a // p a} → β) (x : {a // ¬p a} → β) (a : α) (h : p a) :
( x₀).symm) x) a = x₀ a, h⟩

theorem equiv.subtype_preimage_symm_apply_coe_neg {α : Sort u} {β : Sort v} (p : α → Prop) (x₀ : {a // p a} → β) (x : {a // ¬p a} → β) (a : α) (h : ¬p a) :
( x₀).symm) x) a = x a, h⟩

def equiv.fun_unique (α : Sort u) (β : Sort v) [unique α] :
(α → β) β

If `α` has a unique term, then the type of function `α → β` is equivalent to `β`.

Equations
@[simp]
theorem equiv.fun_unique_symm_apply (α : Sort u) (β : Sort v) [unique α] (b : β) (a : α) :
β).symm) b a = b

@[simp]
theorem equiv.fun_unique_apply (α : Sort u) (β : Sort v) [unique α] (f : α → β) :
β) f = f (default α)

def equiv.Pi_congr_right {α : Sort u_1} {β₁ : α → Sort u_2} {β₂ : α → Sort u_3} :
(Π (a : α), β₁ a β₂ a)((Π (a : α), β₁ a) Π (a : α), β₂ a)

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

Equations
def equiv.Pi_curry {α : Type u_1} {β : α → Type u_2} (γ : Π (a : α), β aSort u_3) :
(Π (x : Σ (i : α), β i), γ x.fst x.snd) Π (a : α) (b : β a), γ a b

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

Equations
def equiv.psigma_equiv_sigma {α : Type u_1} (β : α → Type u_2) :
(Σ' (i : α), β i) Σ (i : α), β i

A `psigma`-type is equivalent to the corresponding `sigma`-type.

Equations
@[simp]
theorem equiv.psigma_equiv_sigma_symm_apply {α : Type u_1} (β : α → Type u_2) (a : Σ (i : α), β i) :
a = a.fst, a.snd

@[simp]
theorem equiv.psigma_equiv_sigma_apply {α : Type u_1} (β : α → Type u_2) (a : Σ' (i : α), β i) :
= a.fst, a.snd

@[simp]
theorem equiv.sigma_congr_right_apply {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} (F : Π (a : α), β₁ a β₂ a) (a : Σ (a : α), β₁ a) :
= a.fst, (F a.fst) a.snd

def equiv.sigma_congr_right {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} :
(Π (a : α), β₁ a β₂ a)((Σ (a : α), β₁ a) Σ (a : α), β₂ a)

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

Equations
@[simp]
theorem equiv.sigma_congr_right_symm_apply {α : Type u_1} {β₁ : α → Type u_2} {β₂ : α → Type u_3} (F : Π (a : α), β₁ a β₂ a) (a : Σ (a : α), β₂ a) :
.symm) a = a.fst, ((F a.fst).symm) a.snd

@[simp]
theorem equiv.sigma_congr_left_apply {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ α₂) (a : Σ (a : α₁), β (e a)) :

def equiv.sigma_congr_left {α₁ : Type u_1} {α₂ : Type u_2} {β : α₂ → Type u_3} (e : α₁ α₂) :
(Σ (a : α₁), β (e a)) Σ (a : α₂), β a

An equivalence `f : α₁ ≃ α₂` generates an equivalence between `Σ a, β (f a)` and `Σ a, β a`.

Equations
def equiv.sigma_congr_left' {α₁ : Type u_1} {α₂ : Type u_2} {β : α₁ → Type u_3} (f : α₁ α₂) :
(Σ (a : α₁), β a) Σ (a : α₂), β ((f.symm) a)

Transporting a sigma type through an equivalence of the base

Equations
def equiv.sigma_congr {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : α₁ → Type u_3} {β₂ : α₂ → Type u_4} (f : α₁ α₂) :
(Π (a : α₁), β₁ a β₂ (f a))sigma β₁ sigma β₂

Transporting a sigma type through an equivalence of the base and a family of equivalences of matching fibers

Equations
def equiv.sigma_equiv_prod (α : Type u_1) (β : Type u_2) :
(Σ (_x : α), β) α × β

`sigma` type with a constant fiber is equivalent to the product.

Equations
@[simp]
theorem equiv.sigma_equiv_prod_apply (α : Type u_1) (β : Type u_2) (a : Σ (_x : α), β) :
a = (a.fst, a.snd)

@[simp]
theorem equiv.sigma_equiv_prod_symm_apply (α : Type u_1) (β : Type u_2) (a : α × β) :
β).symm) a = a.fst, a.snd

def equiv.sigma_equiv_prod_of_equiv {α : Type u_1} {β : Type u_2} {β₁ : α → Type u_3} :
(Π (a : α), β₁ a β)sigma β₁ α × β

If each fiber of a `sigma` type is equivalent to a fixed type, then the sigma type is equivalent to the product.

Equations
def equiv.prod_congr_left {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} :
(α₁ → β₁ β₂)β₁ × α₁ β₂ × α₁

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

Equations
@[simp]
theorem equiv.prod_congr_left_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) (b : β₁) (a : α₁) :
(b, a) = ((e a) b, a)

theorem equiv.prod_congr_refl_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : β₁ β₂) :
e.prod_congr (equiv.refl α₁) = equiv.prod_congr_left (λ (_x : α₁), e)

def equiv.prod_congr_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} :
(α₁ → β₁ β₂)α₁ × β₁ α₁ × β₂

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

Equations
@[simp]
theorem equiv.prod_congr_right_apply {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) (a : α₁) (b : β₁) :
(a, b) = (a, (e a) b)

theorem equiv.prod_congr_refl_left {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : β₁ β₂) :
(equiv.refl α₁).prod_congr e = equiv.prod_congr_right (λ (_x : α₁), e)

@[simp]
theorem equiv.prod_congr_left_trans_prod_comm {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) :
α₁) = α₁).trans

@[simp]
theorem equiv.prod_congr_right_trans_prod_comm {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) :
β₂) = β₁).trans

theorem equiv.sigma_congr_right_sigma_equiv_prod {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) :
β₂) = β₁).trans

theorem equiv.sigma_equiv_prod_sigma_congr_right {α₁ : Type u_1} {β₁ : Type u_2} {β₂ : Type u_3} (e : α₁ → β₁ β₂) :
β₁).symm.trans = β₂).symm

def equiv.perm.prod_extend_right {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] :
α₁ → equiv.perm (α₁ × β₁)

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

Equations
@[simp]
theorem equiv.perm.prod_extend_right_apply_eq {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (a : α₁) (e : equiv.perm β₁) (b : β₁) :
(a, b) = (a, e b)

theorem equiv.perm.prod_extend_right_apply_ne {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (e : equiv.perm β₁) {a a' : α₁} (h : a' a) (b : β₁) :
(a', b) = (a', b)

theorem equiv.perm.eq_of_prod_extend_right_ne {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] {e : equiv.perm β₁} {a a' : α₁} {b : β₁} :
(a', b) (a', b)a' = a

@[simp]
theorem equiv.perm.fst_prod_extend_right {α₁ : Type u_1} {β₁ : Type u_2} [decidable_eq α₁] (a : α₁) (e : equiv.perm β₁) (ab : α₁ × β₁) :
ab).fst = ab.fst

def equiv.arrow_prod_equiv_prod_arrow (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
(γ → α × β) (γ → α) × (γ → β)

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

Equations
def equiv.arrow_arrow_equiv_prod_arrow (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
(α → β → γ) × β → γ)

Functions `α → β → γ` are equivalent to functions on `α × β`.

Equations
def equiv.sum_arrow_equiv_prod_arrow (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
β → γ) (α → γ) × (β → γ)

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

Equations
def equiv.sum_prod_distrib (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
β) × γ α × γ β × γ

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

Equations
@[simp]
theorem equiv.sum_prod_distrib_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) (c : γ) :
γ) (sum.inl a, c) = sum.inl (a, c)

@[simp]
theorem equiv.sum_prod_distrib_apply_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) (c : γ) :
γ) (sum.inr b, c) = sum.inr (b, c)

def equiv.prod_sum_distrib (α : Type u_1) (β : Type u_2) (γ : Type u_3) :
α × γ) α × β α × γ

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

Equations
@[simp]
theorem equiv.prod_sum_distrib_apply_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) (b : β) :
γ) (a, sum.inl b) = sum.inl (a, b)

@[simp]
theorem equiv.prod_sum_distrib_apply_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α) (c : γ) :
γ) (a, sum.inr c) = sum.inr (a, c)

def equiv.sigma_prod_distrib {ι : Type u_1} (α : ι → Type u_2) (β : Type u_3) :
(Σ (i : ι), α i) × β Σ (i : ι), α i × β

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

Equations
def equiv.bool_prod_equiv_sum (α : Type u) :
α α

The product `bool × α` is equivalent to `α ⊕ α`.

Equations
def equiv.bool_to_equiv_prod (α : Type u) :
(bool → α) α × α

The function type `bool → α` is equivalent to `α × α`.

Equations
@[simp]
theorem equiv.bool_to_equiv_prod_apply {α : Type u} (f : bool → α) :
= (f ff, f tt)

@[simp]
theorem equiv.bool_to_equiv_prod_symm_apply_ff {α : Type u} (p : α × α) :
p ff = p.fst

@[simp]
theorem equiv.bool_to_equiv_prod_symm_apply_tt {α : Type u} (p : α × α) :
p tt = p.snd

The set of natural numbers is equivalent to `ℕ ⊕ punit`.

Equations
• equiv.nat_equiv_nat_sum_punit = {to_fun := λ (n : ), equiv.nat_equiv_nat_sum_punit._match_1 n, inv_fun := λ (s : , equiv.nat_equiv_nat_sum_punit._match_2 s, left_inv := equiv.nat_equiv_nat_sum_punit._proof_1, right_inv := equiv.nat_equiv_nat_sum_punit._proof_2}
• equiv.nat_equiv_nat_sum_punit._match_1 a.succ =
• equiv.nat_equiv_nat_sum_punit._match_1 0 =
• equiv.nat_equiv_nat_sum_punit._match_2 = 0
• equiv.nat_equiv_nat_sum_punit._match_2 (sum.inl n) = n.succ

`ℕ ⊕ punit` is equivalent to `ℕ`.

Equations

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

Equations
def equiv.list_equiv_of_equiv {α : Type u_1} {β : Type u_2} :
α βlist α list β

An equivalence between `α` and `β` generates an equivalence between `list α` and `list β`.

Equations
def equiv.fin_equiv_subtype (n : ) :
fin n {m // m < n}

`fin n` is equivalent to `{m // m < n}`.

Equations
def equiv.unique_congr {α : Sort u} {β : Sort v} :
α β

If `α` is equivalent to `β`, then `unique α` is equivalent to `β`.

Equations
def equiv.subtype_congr {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α β) :
(∀ (a : α), p a q (e a)){a // p a} {b // q b}

If `α` is equivalent to `β` and the predicates `p : α → Prop` and `q : β → Prop` are equivalent at corresponding points, then `{a // p a}` is equivalent to `{b // q b}`.

Equations
@[simp]
theorem equiv.subtype_congr_apply {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α β) (h : ∀ (a : α), p a q (e a)) (x : {x // p x}) :
(e.subtype_congr h) x = e x, _⟩

@[simp]
theorem equiv.subtype_congr_symm_apply {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (e : α β) (h : ∀ (a : α), p a q (e a)) (y : {y // q y}) :
((e.subtype_congr h).symm) y = (e.symm) y, _⟩

@[simp]
theorem equiv.subtype_congr_right_symm_apply_coe {α : Sort u} {p q : α → Prop} (e : ∀ (x : α), p x q x) (y : {b // (λ (x : α), q x) b}) :
( y) = y

@[simp]
theorem equiv.subtype_congr_right_apply_coe {α : Sort u} {p q : α → Prop} (e : ∀ (x : α), p x q x) (x : {a // (λ (x : α), p x) a}) :
x) = x

def equiv.subtype_congr_right {α : Sort u} {p q : α → Prop} :
(∀ (x : α), p x q x){x // p x} {x // q x}

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

Equations
def equiv.subtype_equiv_of_subtype {α : Sort u} {β : Sort v} {p : β → Prop} (e : α β) :
{a // p (e a)} {b // p b}

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

Equations
def equiv.subtype_equiv_of_subtype' {α : Sort u} {β : Sort v} {p : α → Prop} (e : α β) :
{a // p a} {b // p ((e.symm) b)}

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

Equations
def equiv.subtype_congr_prop {α : Type u_1} {p q : α → Prop} :
p = q

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

Equations
def equiv.set_congr {α : Type u_1} {s t : set α} :
s = ts t

The subtypes corresponding to equal sets are equivalent.

Equations
@[simp]
theorem equiv.set_congr_apply {α : Type u_1} {s t : set α} (h : s = t) (x : {a // (λ (a : α), (λ (x : α), x s) a) a}) :
x = x, _⟩

def equiv.subtype_subtype_equiv_subtype_exists {α : Type u} (p : α → Prop) (q : → Prop) :
{a // ∃ (h : p a), q a, h⟩}

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

Equations
• = {to_fun := λ (_x : subtype q), equiv.subtype_subtype_equiv_subtype_exists._match_1 p q _x, inv_fun := λ (_x : {a // ∃ (h : p a), q a, h⟩}), equiv.subtype_subtype_equiv_subtype_exists._match_2 p q _x, left_inv := _, right_inv := _}
• equiv.subtype_subtype_equiv_subtype_exists._match_1 p q a, ha⟩, ha'⟩ = a, _⟩
• equiv.subtype_subtype_equiv_subtype_exists._match_2 p q a, ha⟩ = a, _⟩, _⟩
def equiv.subtype_subtype_equiv_subtype_inter {α : Type u} (p q : α → Prop) :
{x // q x.val} {x // p x q x}

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

Equations
def equiv.subtype_subtype_equiv_subtype {α : Type u} {p q : α → Prop} :
(∀ {x : α}, q xp x){x // q x.val}

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

Equations
def equiv.subtype_univ_equiv {α : Type u} {p : α → Prop} :
(∀ (x : α), p x) α

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

Equations
def equiv.subtype_sigma_equiv {α : Type u} (p : α → Type v) (q : α → Prop) :
{y // q y.fst} Σ (x : subtype q), p x.val

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

Equations
def equiv.sigma_subtype_equiv_of_subset {α : Type u} (p : α → Type v) (q : α → Prop) :
(∀ (x : α), p xq x)((Σ (x : subtype q), p x) Σ (x : α), p x)

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

Equations
def equiv.sigma_subtype_preimage_equiv {α : Type u} {β : Type v} (f : α → β) (p : β → Prop) :
(∀ (x : α), p (f x))(Σ (y : subtype p), {x // f x = y}) α

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

Equations
def equiv.sigma_subtype_preimage_equiv_subtype {α : Type u} {β : Type v} (f : α → β) {p : α → Prop} {q : β → Prop} :
(∀ (x : α), p x q (f x))(Σ (y : subtype q), {x // f x = y})

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

Equations
def equiv.pi_equiv_subtype_sigma (ι : Type u_1) (π : ι → Type u_2) :
(Π (i : ι), «π» i) {f : ι → (Σ (i : ι), «π» i) | ∀ (i : ι), (f i).fst = i}

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

Equations
def equiv.subtype_pi_equiv_pi {α : Sort u} {β : α → Sort v} {p : Π (a : α), β a → Prop} :
{f // ∀ (a : α), p a (f a)} Π (a : α), {b // p a b}

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

Equations
def equiv.subtype_prod_equiv_prod {α : Type u} {β : Type v} {p : α → Prop} {q : β → Prop} :
{c // p c.fst q c.snd} {a // p a} × {b // q b}

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

Equations
def equiv.subtype_equiv_codomain {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} → Y) :
{g // g coe = f} Y

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

Equations
@[simp]
theorem equiv.coe_subtype_equiv_codomain {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} → Y) :
= λ (g : {g // g coe = f}), g x

@[simp]
theorem equiv.subtype_equiv_codomain_apply {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} → Y) (g : {g // g coe = f}) :
= g x

theorem equiv.coe_subtype_equiv_codomain_symm {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} → Y) :
= λ (y : Y), λ (x' : X), dite (x' x) (λ (h : x' x), f x', h⟩) (λ (h : ¬x' x), y), _⟩

@[simp]
theorem equiv.subtype_equiv_codomain_symm_apply {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} → Y) (y : Y) (x' : X) :
y) x' = dite (x' x) (λ (h : x' x), f x', h⟩) (λ (h : ¬x' x), y)

@[simp]
theorem equiv.subtype_equiv_codomain_symm_apply_eq {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} → Y) (y : Y) :
y) x = y

theorem equiv.subtype_equiv_codomain_symm_apply_ne {X : Type u_1} {Y : Type u_2} [decidable_eq X] {x : X} (f : {x' // x' x} → Y) (y : Y) (x' : X) (h : x' x) :
y) x' = f x', h⟩

@[simp]
theorem equiv.set.univ_symm_apply (α : Type u_1) (a : α) :

def equiv.set.univ (α : Type u_1) :

`univ α` is equivalent to `α`.

Equations
@[simp]
theorem equiv.set.univ_apply (α : Type u_1) (a : set.univ) :
a = a

def equiv.set.empty (α : Type u_1) :

An empty set is equivalent to the `empty` type.

Equations
def equiv.set.pempty (α : Type u_1) :

An empty set is equivalent to a `pempty` type.

Equations
def equiv.set.union' {α : Type u_1} {s t : set α} (p : α → Prop)  :
(∀ (x : α), x sp x)(∀ (x : α), x t¬p x)(s t) s t

If sets `s` and `t` are separated by a decidable predicate, then `s ∪ t` is equivalent to `s ⊕ t`.

Equations
def equiv.set.union {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x s)] :
s t (s t) s t

If sets `s` and `t` are disjoint, then `s ∪ t` is equivalent to `s ⊕ t`.

Equations
theorem equiv.set.union_apply_left {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x s)] (H : s t ) {a : (s t)} (ha : a s) :
a = sum.inl a, ha⟩

theorem equiv.set.union_apply_right {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x s)] (H : s t ) {a : (s t)} (ha : a t) :
a = sum.inr a, ha⟩

@[simp]
theorem equiv.set.union_symm_apply_left {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x s)] (H : s t ) (a : s) :

@[simp]
theorem equiv.set.union_symm_apply_right {α : Type u_1} {s t : set α} [decidable_pred (λ (x : α), x s)] (H : s t ) (a : t) :

def equiv.set.singleton {α : Type u_1} (a : α) :

A singleton set is equivalent to a `punit` type.

Equations
@[simp]
theorem equiv.set.of_eq_apply {α : Type u} {s t : set α} (h : s = t) (x : s) :
x = x, _⟩

def equiv.set.of_eq {α : Type u} {s t : set α} :
s = ts t

Equal sets are equivalent.

Equations
@[simp]
theorem equiv.set.of_eq_symm_apply {α : Type u} {s t : set α} (h : s = t) (x : t) :

def equiv.set.insert {α : Type u} {s : set α} {a : α} :
a s(insert a s)

If `a ∉ s`, then `insert a s` is equivalent to `s ⊕ punit`.

Equations
@[simp]
theorem equiv.set.insert_symm_apply_inl {α : Type u} {s : set α} {a : α} (H : a s) (b : s) :

@[simp]
theorem equiv.set.insert_symm_apply_inr {α : Type u} {s : set α} {a : α} (H : a s) (b : punit) :

@[simp]
theorem equiv.set.insert_apply_left {α : Type u} {s : set α} {a : α} (H : a s) :
a, _⟩ =

@[simp]
theorem equiv.set.insert_apply_right {α : Type u} {s : set α} {a : α} (H : a s) (b : s) :
b, _⟩ =

def equiv.set.sum_compl {α : Type u_1} (s : set α)  :

If `s : set α` is a set with decidable membership, then `s ⊕ sᶜ` is equivalent to `α`.

Equations
@[simp]
theorem equiv.set.sum_compl_apply_inl {α : Type u} (s : set α) (x : s) :
(sum.inl x) = x

@[simp]
theorem equiv.set.sum_compl_apply_inr {α : Type u} (s : set α) (x : s) :
(sum.inr x) = x

theorem equiv.set.sum_compl_symm_apply_of_mem {α : Type u} {s : set α} {x : α} (hx : x s) :
.symm) x = sum.inl x, hx⟩

theorem equiv.set.sum_compl_symm_apply_of_not_mem {α : Type u} {s : set α} {x : α} (hx : x s) :
.symm) x = sum.inr x, hx⟩

@[simp]
theorem equiv.set.sum_compl_symm_apply {α : Type u_1} {s : set α} {x : s} :

@[simp]
theorem equiv.set.sum_compl_symm_apply_compl {α : Type u_1} {s : set α} {x : s} :

def equiv.set.sum_diff_subset {α : Type u_1} {s t : set α} (h : s t)  :
s (t \ s) t

`sum_diff_subset s t` is the natural equivalence between `s ⊕ (t \ s)` and `t`, where `s` and `t` are two sets.

Equations
@[simp]
theorem equiv.set.sum_diff_subset_apply_inl {α : Type u_1} {s t : set α} (h : s t) (x : s) :
=

@[simp]
theorem equiv.set.sum_diff_subset_apply_inr {α : Type u_1} {s t : set α} (h : s t) (x : (t \ s)) :
=

theorem equiv.set.sum_diff_subset_symm_apply_of_mem {α : Type u_1} {s t : set α} (h : s t) {x : t} (hx : x.val s) :
x = sum.inl x, hx⟩

theorem equiv.set.sum_diff_subset_symm_apply_of_not_mem {α : Type u_1} {s t : set α} (h : s t) {x : t} (hx : x.val s) :
x = sum.inr x, _⟩

def equiv.set.union_sum_inter {α : Type u} (s t : set α)  :
(s t) (s t) s t

If `s` is a set with decidable membership, then the sum of `s ∪ t` and `s ∩ t` is equivalent to `s ⊕ t`.

Equations
def equiv.set.compl {α : Type u} {β : Type v} {s : set α} {t : set β} (e₀ : s t) :
{e // ∀ (x : s), e x = (e₀ x)} (s t)

Given an equivalence `e₀` between sets `s : set α` and `t : set β`, the set of equivalences `e : α ≃ β` such that `e ↑x = ↑(e₀ x)` for each `x : s` is equivalent to the set of equivalences between `sᶜ` and `tᶜ`.

Equations
def equiv.set.prod {α : Type u_1} {β : Type u_2} (s : set α) (t : set β) :
(s.prod t) s × t

The set product of two sets is equivalent to the type product of their coercions to types.

Equations
def equiv.set.image_of_inj_on {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) :
ss (f '' s)

If a function `f` is injective on a set `s`, then `s` is equivalent to `f '' s`.

Equations
def equiv.set.image {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) :
s (f '' s)

If `f` is an injective function, then `s` is equivalent to `f '' s`.

Equations
• H =
@[simp]
theorem equiv.set.image_apply {α : Type u_1} {β : Type u_2} (f : α → β) (s : set α) (H : function.injective f) (p : s) :
s H) p = f p, _⟩

theorem equiv.set.image_symm_preimage {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f) (u s : set α) :
(λ (x : (f '' s)), ( s hf).symm) x)) ⁻¹' u = coe ⁻¹' (f '' u)

def equiv.set.range {α : Sort u_1} {β : Type u_2} (f : α → β) :
α (set.range f)

If `f : α → β` is an injective function, then `α` is equivalent to the range of `f`.

Equations
@[simp]
theorem equiv.set.range_apply {α : Sort u_1} {β : Type u_2} (f : α → β) (H : function.injective f) (x : α) :
H) x = f x, _⟩

theorem equiv.set.apply_range_symm {α : Sort u_1} {β : Type u_2} (f : α → β) (H : function.injective f) (b : (set.range f)) :
f ( H).symm) b) = b

def equiv.set.congr {α : Type u_1} {β : Type u_2} :
α βset α set β

If `α` is equivalent to `β`, then `set α` is equivalent to `set β`.

Equations
def equiv.set.sep {α : Type u} (s : set α) (t : α → Prop) :
{x ∈ s | t x} {x : s | t x}

The set `{x ∈ s | t x}` is equivalent to the set of `x : s` such that `t x`.

Equations
def equiv.set.powerset {α : Type u_1} (S : set α) :

The set `𝒫 S := {x | x ⊆ S}` is equivalent to the type `set S`.

Equations
def equiv.of_bijective {α : Sort u_1} {β : Type u_2} (f : α → β) :
α β

If `f` is a bijective function, then its domain is equivalent to its codomain.

Equations
@[simp]
theorem equiv.of_bijective_apply {α : Sort u_1} {β : Type u_2} (f : α → β) (hf : function.bijective f) (a : α) :
hf) a = f a

@[simp]
theorem equiv.of_injective_apply {α : Sort u_1} {β : Type u_2} (f : α → β) (hf : function.injective f) (a : α) :
hf) a = f a, _⟩

def equiv.of_injective {α : Sort u_1} {β : Type u_2} (f : α → β) :
α (set.range f)

If `f` is an injective function, then its domain is equivalent to its range.

Equations
def equiv.subtype_quotient_equiv_quotient_subtype {α : Sort u} (p₁ : α → Prop) [s₁ : setoid α] [s₂ : setoid (subtype p₁)] (p₂ : quotient s₁ → Prop) :
(∀ (a : α), p₁ a p₂ a)(∀ (x y : subtype p₁), y x y){x // p₂ x} quotient s₂

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

Equations
def equiv.swap_core {α : Sort u} [decidable_eq α] :
α → α → α → α

A helper function for `equiv.swap`.

Equations
theorem equiv.swap_core_self {α : Sort u} [decidable_eq α] (r a : α) :
r = r

theorem equiv.swap_core_swap_core {α : Sort u} [decidable_eq α] (r a b : α) :
b r) = r

theorem equiv.swap_core_comm {α : Sort u} [decidable_eq α] (r a b : α) :
r = r

def equiv.swap {α : Sort u} [decidable_eq α] :
α → α →

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

Equations
theorem equiv.swap_self {α : Sort u} [decidable_eq α] (a : α) :
a =

theorem equiv.swap_comm {α : Sort u} [decidable_eq α] (a b : α) :
b = a

theorem equiv.swap_apply_def {α : Sort u} [decidable_eq α] (a b x : α) :
b) x = ite (x = a) b (ite (x = b) a x)

@[simp]
theorem equiv.swap_apply_left {α : Sort u} [decidable_eq α] (a b : α) :
b) a = b

@[simp]
theorem equiv.swap_apply_right {α : Sort u} [decidable_eq α] (a b : α) :
b) b = a

theorem equiv.swap_apply_of_ne_of_ne {α : Sort u} [decidable_eq α] {a b x : α} :
x ax b b) x = x

@[simp]
theorem equiv.swap_swap {α : Sort u} [decidable_eq α] (a b : α) :
equiv.trans b) b) =

theorem equiv.swap_comp_apply {α : Sort u} [decidable_eq α] {a b x : α} (π : equiv.perm α) :
(equiv.trans «π» b)) x = ite («π» x = a) b (ite («π» x = b) a («π» x))

@[simp]
theorem equiv.swap_inv {α : Type u_1} [decidable_eq α] (x y : α) :
y)⁻¹ = y

@[simp]
theorem equiv.symm_trans_swap_trans {α : Sort u} {β : Sort v} [decidable_eq α] [decidable_eq β] (a b : α) (e : α β) :
(e.symm.trans b)).trans e = equiv.swap (e a) (e b)

@[simp]
theorem equiv.swap_mul_self {α : Type u_1} [decidable_eq α] (i j : α) :
j) * j = 1

@[simp]
theorem equiv.swap_apply_self {α : Type u_1} [decidable_eq α] (i j a : α) :
j) ( j) a) = a

def equiv.set_value {α : Sort u} {β : Sort v} [decidable_eq α] :
α βα → β → α β

Augment an equivalence with a prescribed mapping `f a = b`

Equations
@[simp]
theorem equiv.set_value_eq {α : Sort u} {β : Sort v} [decidable_eq α] (f : α β) (a : α) (b : β) :
(f.set_value a b) a = b

theorem equiv.forall_congr {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (f : α β) :
(∀ {x : α}, p x q (f x))((∀ (x : α), p x) ∀ (y : β), q y)

theorem equiv.forall_congr' {α : Sort u} {β : Sort v} {p : α → Prop} {q : β → Prop} (f : α β) :
(∀ {x : β}, p ((f.symm) x) q x)((∀ (x : α), p x) ∀ (y : β), q y)

theorem equiv.forall₂_congr {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {p : α₁ → β₁ → Prop} {q : α₂ → β₂ → Prop} (eα : α₁ α₂) (eβ : β₁ β₂) :
(∀ {x : α₁} {y : β₁}, p x y q (eα x) (eβ y))((∀ (x : α₁) (y : β₁), p x y) ∀ (x : α₂) (y : β₂), q x y)

theorem equiv.forall₂_congr' {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {p : α₁ → β₁ → Prop} {q : α₂ → β₂ → Prop} (eα : α₁ α₂) (eβ : β₁ β₂) :
(∀ {x : α₂} {y : β₂}, p ((eα.symm) x) ((eβ.symm) y) q x y)((∀ (x : α₁) (y : β₁), p x y) ∀ (x : α₂) (y : β₂), q x y)

theorem equiv.forall₃_congr {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {γ₁ : Sort ug1} {γ₂ : Sort ug2} {p : α₁ → β₁ → γ₁ → Prop} {q : α₂ → β₂ → γ₂ → Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (eγ : γ₁ γ₂) :
(∀ {x : α₁} {y : β₁} {z : γ₁}, p x y z q (eα x) (eβ y) (eγ z))((∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z)

theorem equiv.forall₃_congr' {α₁ : Sort ua1} {α₂ : Sort ua2} {β₁ : Sort ub1} {β₂ : Sort ub2} {γ₁ : Sort ug1} {γ₂ : Sort ug2} {p : α₁ → β₁ → γ₁ → Prop} {q : α₂ → β₂ → γ₂ → Prop} (eα : α₁ α₂) (eβ : β₁ β₂) (eγ : γ₁ γ₂) :
(∀ {x : α₂} {y : β₂} {z : γ₂}, p ((eα.symm) x) ((eβ.symm) y) ((eγ.symm) z) q x y z)((∀ (x : α₁) (y : β₁) (z : γ₁), p x y z) ∀ (x : α₂) (y : β₂) (z : γ₂), q x y z)

theorem equiv.forall_congr_left' {α : Sort u} {β : Sort v} {p : α → Prop} (f : α β) :
(∀ (x : α), p x) ∀ (y : β), p ((f.symm) y)

theorem equiv.forall_congr_left {α : Sort u} {β : Sort v} {p : β → Prop} (f : α β) :
(∀ (x : α), p (f x)) ∀ (y : β), p y

@[simp]
theorem equiv.Pi_congr_left'_apply {α : Sort u} {β : Sort v} (P : α → Sort w) (e : α β) (f : Π (a : α), P a) (x : β) :
e) f x = f ((e.symm) x)

def equiv.Pi_congr_left' {α : Sort u} {β : Sort v} (P : α → Sort w) (e : α β) :
(Π (a : α), P a) Π (b : β), P ((e.symm) b)

Transport dependent functions through an equivalence of the base space.

Equations
@[simp]
theorem equiv.Pi_congr_left'_symm_apply {α : Sort u} {β : Sort v} (P : α → Sort w) (e : α β) (f : Π (b : β), P ((e.symm) b)) (x : α) :
e).symm) f x = _.mpr (f (e x))

def equiv.Pi_congr_left {α : Sort u} {β : Sort v} (P : β → Sort w) (e : α β) :
(Π (a : α), P (e a)) Π (b : β), P b

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

Equations
def equiv.Pi_congr {α : Sort u} {β : Sort v} {W : α → Sort w} {Z : β → Sort z} (h₁ : α β) :
(Π (a : α), W a Z (h₁ a))((Π (a : α), W a) Π (b : β), Z b)

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

Equations
def equiv.Pi_congr' {α : Sort u} {β : Sort v} {W : α → Sort w} {Z : β → Sort z} (h₁ : α β) :
(Π (b : β), W ((h₁.symm) b) Z b)((Π (a : α), W a) Π (b : β), Z b)

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

Equations
@[instance]
def ulift.subsingleton {α : Type u_1} [subsingleton α] :

@[instance]
def plift.subsingleton {α : Sort u_1} [subsingleton α] :

@[instance]
def ulift.decidable_eq {α : Type u_1} [decidable_eq α] :

Equations
@[instance]
def plift.decidable_eq {α : Sort u_1} [decidable_eq α] :

Equations
def equiv_of_unique_of_unique {α : Sort u} {β : Sort v} [unique α] [unique β] :
α β

If both `α` and `β` are singletons, then `α ≃ β`.

Equations
def equiv_punit_of_unique {α : Sort u} [unique α] :

If `α` is a singleton, then it is equivalent to any `punit`.

Equations
def subsingleton_prod_self_equiv {α : Type u_1} [subsingleton α] :
α × α α

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

Equations
def equiv_of_subsingleton_of_subsingleton {α : Sort u} {β : Sort v} [subsingleton α] [subsingleton β] :
(α → β)(β → α)α β

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

Equations
def unique_unique_equiv {α : Sort u} :

`unique (unique α)` is equivalent to `unique α`.

Equations
def quot.congr {α : Sort u} {β : Sort v} {ra : α → α → Prop} {rb : β → β → Prop} (e : α β) :
(∀ (a₁ a₂ : α), ra a₁ a₂ rb (e a₁) (e a₂))quot ra quot rb

An equivalence `e : α ≃ β` generates an equivalence between quotient spaces, if `ra a₁ a₂ ↔ rb (e a₁) (e a₂).

Equations
def quot.congr_right {α : Sort u} {r r' : α → α → Prop} :
(∀ (a₁ a₂ : α), r a₁ a₂ r' a₁ a₂)quot r quot r'

Quotients are congruent on equivalences under equality of their relation. An alternative is just to use rewriting with `eq`, but then computational proofs get stuck.

Equations
• = eq
def quot.congr_left {α : Sort u} {β : Sort v} {r : α → α → Prop} (e : α β) :
quot r quot (λ (b b' : β), r ((e.symm) b) ((e.symm) b'))

An equivalence `e : α ≃ β` generates an equivalence between the quotient space of `α` by a relation `ra` and the quotient space of `β` by the image of this relation under `e`.

Equations
def quotient.congr {α : Sort u} {β : Sort v} {ra : setoid α} {rb : setoid β} (e : α β) :
(∀ (a₁ a₂ : α), setoid.r a₁ a₂ setoid.r (e a₁) (e a₂))quotient ra quotient rb

An equivalence `e : α ≃ β` generates an equivalence between quotient spaces, if `ra a₁ a₂ ↔ rb (e a₁) (e a₂).

Equations
• eq = eq
def quotient.congr_right {α : Sort u} {r r' : setoid α} :
(∀ (a₁ a₂ : α), setoid.r a₁ a₂ setoid.r a₁ a₂) quotient r'

Quotients are congruent on equivalences under equality of their relation. An alternative is just to use rewriting with `eq`, but then computational proofs get stuck.

Equations
def set.bij_on.equiv {α : Type u_1} {β : Type u_2} {s : set β} (f : α → β) :
α s

If a function is a bijection between `univ` and a set `s` in the target type, it induces an equivalence between the original type and the type `↑s`.

Equations
theorem dite_comp_equiv_update {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : set α} (e : β s) (v : β → γ) (w : α → γ) (j : β) (x : γ) [decidable_eq β] [decidable_eq α] [Π (j : α), decidable (j s)] :
(λ (i : α), dite (i s) (λ (h : i s), x ((e.symm) i, h⟩)) (λ (h : i s), w i)) = function.update (λ (i : α), dite (i s) (λ (h : i s), v ((e.symm) i, h⟩)) (λ (h : i s), w i)) (e j) x

The composition of an updated function with an equiv on a subset can be expressed as an updated function.