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

! This file was ported from Lean 3 source module logic.equiv.defs
! leanprover-community/mathlib commit c4658a649d216f57e99621708b09dcb3dcccbd23
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.FunLike.Equiv
import Mathlib.Data.Quot
import Mathlib.Init.Data.Bool.Lemmas
import Mathlib.Logic.Unique

/-!
# 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 `α ≃ α`. More lemmas about `Equiv.Perm` can be found in
`GroupTheory.Perm`.

Then we define

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

- `Equiv.refl α` is the identity map interpreted as `α ≃ α`;

* 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!);

* 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.decidableEq` takes `e : α ≃ β` and `[DecidableEq β]` and returns `DecidableEq α`.

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

Many more such isomorphisms and operations are defined in `Logic.Equiv.Basic`.

## Tags

equivalence, congruence, bijective map
-/

open Function

universe u v w z

variable {α: Sort uα : Sort u: Type uSortSort u: Type u u} {β: Sort vβ : Sort v: Type vSortSort v: Type v v} {γ: Sort wγ : Sort w: Type wSortSort w: Type w w}

/-- `α ≃ β` is the type of functions from `α → β` with a two-sided inverse. -/
structure Equiv: {α : Sort u_1} →
{β : Sort u_2} →
(toFun : α → β) → (invFun : β → α) → LeftInverse invFun toFun → Function.RightInverse invFun toFun → Equiv α βEquiv (α: Sort ?u.14α : Sort _: Type ?u.14SortSort _: Type ?u.14 _) (β: Sort ?u.17β : Sort _: Type ?u.17SortSort _: Type ?u.17 _) where
toFun: {α : Sort u_1} → {β : Sort u_2} → Equiv α β → α → βtoFun : α: Sort ?u.14α → β: Sort ?u.17β
invFun: {α : Sort u_1} → {β : Sort u_2} → Equiv α β → β → αinvFun : β: Sort ?u.17β → α: Sort ?u.14α
left_inv: ∀ {α : Sort u_1} {β : Sort u_2} (self : Equiv α β), LeftInverse self.invFun self.toFunleft_inv : LeftInverse: {α : Sort ?u.31} → {β : Sort ?u.30} → (β → α) → (α → β) → PropLeftInverse invFun: β → αinvFun toFun: α → βtoFun
right_inv: ∀ {α : Sort u_1} {β : Sort u_2} (self : Equiv α β), Function.RightInverse self.invFun self.toFunright_inv : RightInverse: {α : Sort ?u.43} → {β : Sort ?u.42} → (β → α) → (α → β) → PropRightInverse invFun: β → αinvFun toFun: α → βtoFun
#align equiv Equiv: Sort u_1 → Sort u_2 → Sort (max(max1u_1)u_2)Equiv

infixl:25 " ≃ " => Equiv: Sort u_1 → Sort u_2 → Sort (max(max1u_1)u_2)Equiv

/-- Turn an element of a type `F` satisfying `EquivLike F α β` into an actual
`Equiv`. This is declared as the default coercion from `F` to `α ≃ β`. -/
@[coe]
def EquivLike.toEquiv: {α : Sort u} → {β : Sort v} → {F : Sort u_1} → [inst : EquivLike F α β] → F → α ≃ βEquivLike.toEquiv {F: ?m.8760F} [EquivLike: Sort ?u.8765 → outParam (Sort ?u.8764) → outParam (Sort ?u.8763) → Sort (max(max(max1?u.8765)?u.8764)?u.8763)EquivLike F: ?m.8760F α: Sort uα β: Sort vβ] (f: Ff :F: ?m.8760F) : α: Sort uα ≃ β: Sort vβ where
toFun := f: Ff
invFun := EquivLike.inv: {E : Sort ?u.8869} →
{α : outParam (Sort ?u.8868)} → {β : outParam (Sort ?u.8867)} → [self : EquivLike E α β] → E → β → αEquivLike.inv f: Ff
left_inv := EquivLike.left_inv: ∀ {E : Sort ?u.8888} {α : outParam (Sort ?u.8887)} {β : outParam (Sort ?u.8886)} [self : EquivLike E α β] (e : E),
LeftInverse (inv e) (coe e)EquivLike.left_inv f: Ff
right_inv := EquivLike.right_inv: ∀ {E : Sort ?u.8911} {α : outParam (Sort ?u.8910)} {β : outParam (Sort ?u.8909)} [self : EquivLike E α β] (e : E),
Function.RightInverse (inv e) (coe e)EquivLike.right_inv f: Ff

/-- Any type satisfying `EquivLike` can be cast into `Equiv` via `EquivLike.toEquiv`. -/
instance: {α : Sort u} → {β : Sort v} → {F : Sort u_1} → [inst : EquivLike F α β] → CoeTC F (α ≃ β)instance {F: Sort ?u.9203F} [EquivLike: Sort ?u.9203 → outParam (Sort ?u.9202) → outParam (Sort ?u.9201) → Sort (max(max(max1?u.9203)?u.9202)?u.9201)EquivLike F: ?m.9198F α: Sort uα β: Sort vβ] : CoeTC: Sort ?u.9207 → Sort ?u.9206 → Sort (max(max1?u.9207)?u.9206)CoeTC F: ?m.9198F (α: Sort uα ≃ β: Sort vβ) :=
⟨EquivLike.toEquiv: {α : Sort ?u.9224} → {β : Sort ?u.9223} → {F : Sort ?u.9222} → [inst : EquivLike F α β] → F → α ≃ βEquivLike.toEquiv⟩

/-- `Perm α` is the type of bijections from `α` to itself. -/
@[reducible]
def Equiv.Perm: Sort u_1 → Sort (max1u_1)Equiv.Perm (α: Sort ?u.9318α : Sort _: Type ?u.9318SortSort _: Type ?u.9318 _) :=
Equiv: Sort ?u.9326 → Sort ?u.9325 → Sort (max(max1?u.9326)?u.9325)Equiv α: Sort ?u.9318α α: Sort ?u.9318α
#align equiv.perm Equiv.Perm: Sort u_1 → Sort (max1u_1)Equiv.Perm

namespace Equiv

instance: {α : Sort u} → {β : Sort v} → EquivLike (α ≃ β) α βinstance : EquivLike: Sort ?u.9340 → outParam (Sort ?u.9339) → outParam (Sort ?u.9338) → Sort (max(max(max1?u.9340)?u.9339)?u.9338)EquivLike (α: Sort uα ≃ β: Sort vβ) α: Sort uα β: Sort vβ where
coe := toFun: {α : Sort ?u.9354} → {β : Sort ?u.9353} → α ≃ β → α → βtoFun
inv := invFun: {α : Sort ?u.9366} → {β : Sort ?u.9365} → α ≃ β → β → αinvFun
left_inv := left_inv: ∀ {α : Sort ?u.9376} {β : Sort ?u.9375} (self : α ≃ β), LeftInverse self.invFun self.toFunleft_inv
right_inv := right_inv: ∀ {α : Sort ?u.9390} {β : Sort ?u.9389} (self : α ≃ β), Function.RightInverse self.invFun self.toFunright_inv
coe_injective' e₁: ?m.9404e₁ e₂: ?m.9407e₂ h₁: ?m.9410h₁ h₂: ?m.9413h₂ := byGoals accomplished! 🐙 α: Sort uβ: Sort vγ: Sort we₁, e₂: α ≃ βh₁: e₁.toFun = e₂.toFunh₂: e₁.invFun = e₂.invFune₁ = e₂cases e₁: α ≃ βe₁α: Sort uβ: Sort vγ: Sort we₂: α ≃ βtoFun✝: α → βinvFun✝: β → αleft_inv✝: LeftInverse invFun✝ toFun✝right_inv✝: Function.RightInverse invFun✝ toFun✝h₁: { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun = e₂.toFunh₂: { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun = e₂.invFunmk{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = e₂;α: Sort uβ: Sort vγ: Sort we₂: α ≃ βtoFun✝: α → βinvFun✝: β → αleft_inv✝: LeftInverse invFun✝ toFun✝right_inv✝: Function.RightInverse invFun✝ toFun✝h₁: { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFun = e₂.toFunh₂: { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun = e₂.invFunmk{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = e₂ α: Sort uβ: Sort vγ: Sort we₁, e₂: α ≃ βh₁: e₁.toFun = e₂.toFunh₂: e₁.invFun = e₂.invFune₁ = e₂cases e₂: α ≃ βe₂α: Sort uβ: Sort vγ: Sort wtoFun✝¹: α → βinvFun✝¹: β → αleft_inv✝¹: LeftInverse invFun✝¹ toFun✝¹right_inv✝¹: Function.RightInverse invFun✝¹ toFun✝¹toFun✝: α → βinvFun✝: β → αleft_inv✝: LeftInverse invFun✝ toFun✝right_inv✝: Function.RightInverse invFun✝ toFun✝h₁: { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun =   { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFunh₂: { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =   { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFunmk.mk{ toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =   { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ };α: Sort uβ: Sort vγ: Sort wtoFun✝¹: α → βinvFun✝¹: β → αleft_inv✝¹: LeftInverse invFun✝¹ toFun✝¹right_inv✝¹: Function.RightInverse invFun✝¹ toFun✝¹toFun✝: α → βinvFun✝: β → αleft_inv✝: LeftInverse invFun✝ toFun✝right_inv✝: Function.RightInverse invFun✝ toFun✝h₁: { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.toFun =   { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.toFunh₂: { toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ }.invFun =   { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFunmk.mk{ toFun := toFun✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =   { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } α: Sort uβ: Sort vγ: Sort we₁, e₂: α ≃ βh₁: e₁.toFun = e₂.toFunh₂: e₁.invFun = e₂.invFune₁ = e₂congrGoals accomplished! 🐙

/-- Helper instance when inference gets stuck on following the normal chain
`EquivLike → EmbeddingLike → FunLike → CoeFun`. -/
instance: {α : Sort u} → {β : Sort v} → FunLike (α ≃ β) α fun x => βinstance : FunLike: Sort ?u.10011 →
(α : outParam (Sort ?u.10010)) → outParam (α → Sort ?u.10009) → Sort (max(max(max1?u.10011)?u.10010)?u.10009)FunLike (α: Sort uα ≃ β: Sort vβ) α: Sort uα (fun _: ?m.10015_ => β: Sort vβ) :=
EmbeddingLike.toFunLike: {F : Sort ?u.10023} →
{α : outParam (Sort ?u.10022)} →
{β : outParam (Sort ?u.10021)} → [self : EmbeddingLike F α β] → FunLike F α fun x => βEmbeddingLike.toFunLike

@[simp] theorem coe_fn_mk: ∀ {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : LeftInverse g f) (r : Function.RightInverse g f),
↑{ toFun := f, invFun := g, left_inv := l, right_inv := r } = fcoe_fn_mk (f: α → βf : α: Sort uα → β: Sort vβ) (g: β → αg l: LeftInverse g fl r: ?m.10284r) : (Equiv.mk: {α : Sort ?u.10292} →
{β : Sort ?u.10291} →
(toFun : α → β) → (invFun : β → α) → LeftInverse invFun toFun → Function.RightInverse invFun toFun → α ≃ βEquiv.mk f: α → βf g: ?m.10278g l: ?m.10281l r: ?m.10284r : α: Sort uα → β: Sort vβ) = f: α → βf :=
rfl: ∀ {α : Sort ?u.10391} {a : α}, a = arfl
#align equiv.coe_fn_mk Equiv.coe_fn_mk: ∀ {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : LeftInverse g f) (r : Function.RightInverse g f),
↑{ toFun := f, invFun := g, left_inv := l, right_inv := r } = fEquiv.coe_fn_mk

/-- The map `(r ≃ s) → (r → s)` is injective. -/
theorem coe_fn_injective: ∀ {α : Sort u} {β : Sort v}, Injective fun e => ↑ecoe_fn_injective : @Function.Injective: {α : Sort ?u.10447} → {β : Sort ?u.10446} → (α → β) → PropFunction.Injective (α: Sort uα ≃ β: Sort vβ) (α: Sort uα → β: Sort vβ) (fun e: ?m.10454e => e: ?m.10454e) :=
FunLike.coe_injective': ∀ {F : Sort ?u.10529} {α : outParam (Sort ?u.10528)} {β : outParam (α → Sort ?u.10527)} [self : FunLike F α β],
Injective FunLike.coeFunLike.coe_injective'
#align equiv.coe_fn_injective Equiv.coe_fn_injective: ∀ {α : Sort u} {β : Sort v}, Injective fun e => ↑eEquiv.coe_fn_injective

protected theorem coe_inj: ∀ {α : Sort u} {β : Sort v} {e₁ e₂ : α ≃ β}, ↑e₁ = ↑e₂ ↔ e₁ = e₂coe_inj {e₁: α ≃ βe₁ e₂: α ≃ βe₂ : α: Sort uα ≃ β: Sort vβ} : (e₁: α ≃ βe₁ : α: Sort uα → β: Sort vβ) = e₂: α ≃ βe₂ ↔ e₁: α ≃ βe₁ = e₂: α ≃ βe₂ :=
@FunLike.coe_fn_eq: ∀ {F : Sort ?u.10906} {α : Sort ?u.10904} {β : α → Sort ?u.10905} [i : FunLike F α β] {f g : F}, ↑f = ↑g ↔ f = gFunLike.coe_fn_eq _: Sort ?u.10906_ _: Sort ?u.10904_ _: ?m.10908 → Sort ?u.10905_ _ e₁: α ≃ βe₁ e₂: α ≃ βe₂
#align equiv.coe_inj Equiv.coe_inj: ∀ {α : Sort u} {β : Sort v} {e₁ e₂ : α ≃ β}, ↑e₁ = ↑e₂ ↔ e₁ = e₂Equiv.coe_inj

@[ext] theorem ext: ∀ {α : Sort u} {β : Sort v} {f g : α ≃ β}, (∀ (x : α), ↑f x = ↑g x) → f = gext {f: α ≃ βf g: α ≃ βg : Equiv: Sort ?u.10957 → Sort ?u.10956 → Sort (max(max1?u.10957)?u.10956)Equiv α: Sort uα β: Sort vβ} (H: ∀ (x : α), ↑f x = ↑g xH : ∀ x: ?m.10961x, f: α ≃ βf x: ?m.10961x = g: α ≃ βg x: ?m.10961x) : f: α ≃ βf = g: α ≃ βg := FunLike.ext: ∀ {F : Sort ?u.11090} {α : Sort ?u.11091} {β : α → Sort ?u.11089} [i : FunLike F α β] (f g : F),
(∀ (x : α), ↑f x = ↑g x) → f = gFunLike.ext f: α ≃ βf g: α ≃ βg H: ∀ (x : α), ↑f x = ↑g xH
#align equiv.ext Equiv.ext: ∀ {α : Sort u} {β : Sort v} {f g : α ≃ β}, (∀ (x : α), ↑f x = ↑g x) → f = gEquiv.ext

protected theorem congr_arg: ∀ {f : α ≃ β} {x x' : α}, x = x' → ↑f x = ↑f x'congr_arg {f: α ≃ βf : Equiv: Sort ?u.11150 → Sort ?u.11149 → Sort (max(max1?u.11150)?u.11149)Equiv α: Sort uα β: Sort vβ} {x: αx x': αx' : α: Sort uα} : x: αx = x': αx' → f: α ≃ βf x: αx = f: α ≃ βf x': αx' :=
FunLike.congr_arg: ∀ {F : Sort ?u.11284} {α : Sort ?u.11282} {β : Sort ?u.11283} [i : FunLike F α fun x => β] (f : F) {x y : α},
x = y → ↑f x = ↑f yFunLike.congr_arg f: α ≃ βf
#align equiv.congr_arg Equiv.congr_arg: ∀ {α : Sort u} {β : Sort v} {f : α ≃ β} {x x' : α}, x = x' → ↑f x = ↑f x'Equiv.congr_arg

protected theorem congr_fun: ∀ {α : Sort u} {β : Sort v} {f g : α ≃ β}, f = g → ∀ (x : α), ↑f x = ↑g xcongr_fun {f: α ≃ βf g: α ≃ βg : Equiv: Sort ?u.11339 → Sort ?u.11338 → Sort (max(max1?u.11339)?u.11338)Equiv α: Sort uα β: Sort vβ} (h: f = gh : f: α ≃ βf = g: α ≃ βg) (x: αx : α: Sort uα) : f: α ≃ βf x: αx = g: α ≃ βg x: αx :=
FunLike.congr_fun: ∀ {F : Sort ?u.11470} {α : Sort ?u.11472} {β : α → Sort ?u.11471} [i : FunLike F α β] {f g : F},
f = g → ∀ (x : α), ↑f x = ↑g xFunLike.congr_fun h: f = gh x: αx
#align equiv.congr_fun Equiv.congr_fun: ∀ {α : Sort u} {β : Sort v} {f g : α ≃ β}, f = g → ∀ (x : α), ↑f x = ↑g xEquiv.congr_fun

theorem ext_iff: ∀ {f g : α ≃ β}, f = g ↔ ∀ (x : α), ↑f x = ↑g xext_iff {f: α ≃ βf g: α ≃ βg : Equiv: Sort ?u.11529 → Sort ?u.11528 → Sort (max(max1?u.11529)?u.11528)Equiv α: Sort uα β: Sort vβ} : f: α ≃ βf = g: α ≃ βg ↔ ∀ x: ?m.11537x, f: α ≃ βf x: ?m.11537x = g: α ≃ βg x: ?m.11537x := FunLike.ext_iff: ∀ {F : Sort ?u.11659} {α : Sort ?u.11661} {β : α → Sort ?u.11660} [i : FunLike F α β] {f g : F},
f = g ↔ ∀ (x : α), ↑f x = ↑g xFunLike.ext_iff
#align equiv.ext_iff Equiv.ext_iff: ∀ {α : Sort u} {β : Sort v} {f g : α ≃ β}, f = g ↔ ∀ (x : α), ↑f x = ↑g xEquiv.ext_iff

@[ext] theorem Perm.ext: ∀ {σ τ : Perm α}, (∀ (x : α), ↑σ x = ↑τ x) → σ = τPerm.ext {σ: Perm ασ τ: Perm ατ : Equiv.Perm: Sort ?u.11738 → Sort (max1?u.11738)Equiv.Perm α: Sort uα} (H: ∀ (x : α), ↑σ x = ↑τ xH : ∀ x: ?m.11742x, σ: Perm ασ x: ?m.11742x = τ: Perm ατ x: ?m.11742x) : σ: Perm ασ = τ: Perm ατ := Equiv.ext: ∀ {α : Sort ?u.11870} {β : Sort ?u.11869} {f g : α ≃ β}, (∀ (x : α), ↑f x = ↑g x) → f = gEquiv.ext H: ∀ (x : α), ↑σ x = ↑τ xH
#align equiv.perm.ext Equiv.Perm.ext: ∀ {α : Sort u} {σ τ : Perm α}, (∀ (x : α), ↑σ x = ↑τ x) → σ = τEquiv.Perm.ext

protected theorem Perm.congr_arg: ∀ {f : Perm α} {x x' : α}, x = x' → ↑f x = ↑f x'Perm.congr_arg {f: Perm αf : Equiv.Perm: Sort ?u.11906 → Sort (max1?u.11906)Equiv.Perm α: Sort uα} {x: αx x': αx' : α: Sort uα} : x: αx = x': αx' → f: Perm αf x: αx = f: Perm αf x': αx' :=
Equiv.congr_arg: ∀ {α : Sort ?u.12038} {β : Sort ?u.12037} {f : α ≃ β} {x x' : α}, x = x' → ↑f x = ↑f x'Equiv.congr_arg
#align equiv.perm.congr_arg Equiv.Perm.congr_arg: ∀ {α : Sort u} {f : Perm α} {x x' : α}, x = x' → ↑f x = ↑f x'Equiv.Perm.congr_arg

protected theorem Perm.congr_fun: ∀ {α : Sort u} {f g : Perm α}, f = g → ∀ (x : α), ↑f x = ↑g xPerm.congr_fun {f: Perm αf g: Perm αg : Equiv.Perm: Sort ?u.12077 → Sort (max1?u.12077)Equiv.Perm α: Sort uα} (h: f = gh : f: Perm αf = g: Perm αg) (x: αx : α: Sort uα) : f: Perm αf x: αx = g: Perm αg x: αx :=
Equiv.congr_fun: ∀ {α : Sort ?u.12208} {β : Sort ?u.12207} {f g : α ≃ β}, f = g → ∀ (x : α), ↑f x = ↑g xEquiv.congr_fun h: f = gh x: αx
#align equiv.perm.congr_fun Equiv.Perm.congr_fun: ∀ {α : Sort u} {f g : Perm α}, f = g → ∀ (x : α), ↑f x = ↑g xEquiv.Perm.congr_fun

theorem Perm.ext_iff: ∀ {α : Sort u} {σ τ : Perm α}, σ = τ ↔ ∀ (x : α), ↑σ x = ↑τ xPerm.ext_iff {σ: Perm ασ τ: Perm ατ : Equiv.Perm: Sort ?u.12236 → Sort (max1?u.12236)Equiv.Perm α: Sort uα} : σ: Perm ασ = τ: Perm ατ ↔ ∀ x: ?m.12246x, σ: Perm ασ x: ?m.12246x = τ: Perm ατ x: ?m.12246x := Equiv.ext_iff: ∀ {α : Sort ?u.12369} {β : Sort ?u.12368} {f g : α ≃ β}, f = g ↔ ∀ (x : α), ↑f x = ↑g xEquiv.ext_iff
#align equiv.perm.ext_iff Equiv.Perm.ext_iff: ∀ {α : Sort u} {σ τ : Perm α}, σ = τ ↔ ∀ (x : α), ↑σ x = ↑τ xEquiv.Perm.ext_iff

/-- Any type is equivalent to itself. -/
@[refl] protected def refl: (α : Sort ?u.12396) → α ≃ αrefl (α: Sort ?u.12396α : Sort _: Type ?u.12396SortSort _: Type ?u.12396 _) : α: Sort ?u.12396α ≃ α: Sort ?u.12396α := ⟨id: {α : Sort ?u.12415} → α → αid, id: {α : Sort ?u.12420} → α → αid, fun _: ?m.12426_ => rfl: ∀ {α : Sort ?u.12428} {a : α}, a = arfl, fun _: ?m.12437_ => rfl: ∀ {α : Sort ?u.12439} {a : α}, a = arfl⟩
#align equiv.refl Equiv.refl: (α : Sort u_1) → α ≃ αEquiv.refl

instance inhabited': {α : Sort u} → Inhabited (α ≃ α)inhabited' : Inhabited: Sort ?u.12507 → Sort (max1?u.12507)Inhabited (α: Sort uα ≃ α: Sort uα) := ⟨Equiv.refl: (α : Sort ?u.12516) → α ≃ αEquiv.refl α: Sort uα⟩

/-- Inverse of an equivalence `e : α ≃ β`. -/
@[symm]
protected def symm: α ≃ β → β ≃ αsymm (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : β: Sort vβ ≃ α: Sort uα := ⟨e: α ≃ βe.invFun: {α : Sort ?u.12601} → {β : Sort ?u.12600} → α ≃ β → β → αinvFun, e: α ≃ βe.toFun: {α : Sort ?u.12610} → {β : Sort ?u.12609} → α ≃ β → α → βtoFun, e: α ≃ βe.right_inv: ∀ {α : Sort ?u.12617} {β : Sort ?u.12616} (self : α ≃ β), Function.RightInverse self.invFun self.toFunright_inv, e: α ≃ βe.left_inv: ∀ {α : Sort ?u.12622} {β : Sort ?u.12621} (self : α ≃ β), LeftInverse self.invFun self.toFunleft_inv⟩
#align equiv.symm Equiv.symm: {α : Sort u} → {β : Sort v} → α ≃ β → β ≃ αEquiv.symm

pp_extended_field_notation Equiv.symm: {α : Sort u} → {β : Sort v} → α ≃ β → β ≃ αEquiv.symm

/-- See Note [custom simps projection] -/
def Simps.symm_apply: {α : Sort u} → {β : Sort v} → α ≃ β → β → αSimps.symm_apply (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : β: Sort vβ → α: Sort uα := e: α ≃ βe.symm: {α : Sort ?u.19960} → {β : Sort ?u.19959} → α ≃ β → β ≃ αsymm
#align equiv.simps.symm_apply Equiv.Simps.symm_apply: {α : Sort u} → {β : Sort v} → α ≃ β → β → αEquiv.Simps.symm_apply

initialize_simps_projections Equiv: Sort u_1 → Sort u_2 → Sort (max(max1u_1)u_2)Equiv (toFun: (α : Sort u_1) → (β : Sort u_2) → α ≃ β → α → βtoFun → apply: (α : Sort u_1) → (β : Sort u_2) → α ≃ β → α → βapply, invFun: (α : Sort u_1) → (β : Sort u_2) → α ≃ β → β → αinvFun → symm_apply: {α : Sort u} → {β : Sort v} → α ≃ β → β → αsymm_apply)

-- Porting note:
-- Added these lemmas as restatements of `left_inv` and `right_inv`,
-- which use the coercions.
-- We might even consider switching the names, and having these as a public API.
theorem left_inv': ∀ (e : α ≃ β), LeftInverse ↑e.symm ↑eleft_inv' (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : Function.LeftInverse: {α : Sort ?u.20251} → {β : Sort ?u.20250} → (β → α) → (α → β) → PropFunction.LeftInverse e: α ≃ βe.symm: {α : Sort ?u.20255} → {β : Sort ?u.20254} → α ≃ β → β ≃ αsymm e: α ≃ βe := e: α ≃ βe.left_inv: ∀ {α : Sort ?u.20396} {β : Sort ?u.20395} (self : α ≃ β), LeftInverse self.invFun self.toFunleft_inv
theorem right_inv': ∀ (e : α ≃ β), Function.RightInverse ↑e.symm ↑eright_inv' (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : Function.RightInverse: {α : Sort ?u.20421} → {β : Sort ?u.20420} → (β → α) → (α → β) → PropFunction.RightInverse e: α ≃ βe.symm: {α : Sort ?u.20425} → {β : Sort ?u.20424} → α ≃ β → β ≃ αsymm e: α ≃ βe := e: α ≃ βe.right_inv: ∀ {α : Sort ?u.20566} {β : Sort ?u.20565} (self : α ≃ β), Function.RightInverse self.invFun self.toFunright_inv

/-- Composition of equivalences `e₁ : α ≃ β` and `e₂ : β ≃ γ`. -/
@[trans]
protected def trans: {α : Sort u} → {β : Sort v} → {γ : Sort w} → α ≃ β → β ≃ γ → α ≃ γtrans (e₁: α ≃ βe₁ : α: Sort uα ≃ β: Sort vβ) (e₂: β ≃ γe₂ : β: Sort vβ ≃ γ: Sort wγ) : α: Sort uα ≃ γ: Sort wγ :=
⟨e₂: β ≃ γe₂ ∘ e₁: α ≃ βe₁, e₁: α ≃ βe₁.symm: {α : Sort ?u.20763} → {β : Sort ?u.20762} → α ≃ β → β ≃ αsymm ∘ e₂: β ≃ γe₂.symm: {α : Sort ?u.20835} → {β : Sort ?u.20834} → α ≃ β → β ≃ αsymm, e₂: β ≃ γe₂.left_inv: ∀ {α : Sort ?u.20910} {β : Sort ?u.20909} (self : α ≃ β), LeftInverse self.invFun self.toFunleft_inv.comp: ∀ {α : Sort ?u.20915} {β : Sort ?u.20914} {γ : Sort ?u.20916} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β},
LeftInverse f g → LeftInverse h i → LeftInverse (h ∘ f) (g ∘ i)comp e₁: α ≃ βe₁.left_inv: ∀ {α : Sort ?u.20966} {β : Sort ?u.20965} (self : α ≃ β), LeftInverse self.invFun self.toFunleft_inv, e₂: β ≃ γe₂.right_inv: ∀ {α : Sort ?u.20978} {β : Sort ?u.20977} (self : α ≃ β), Function.RightInverse self.invFun self.toFunright_inv.comp: ∀ {α : Sort ?u.20983} {β : Sort ?u.20982} {γ : Sort ?u.20984} {f : α → β} {g : β → α} {h : β → γ} {i : γ → β},
Function.RightInverse f g → Function.RightInverse h i → Function.RightInverse (h ∘ f) (g ∘ i)comp e₁: α ≃ βe₁.right_inv: ∀ {α : Sort ?u.21020} {β : Sort ?u.21019} (self : α ≃ β), Function.RightInverse self.invFun self.toFunright_inv⟩
#align equiv.trans Equiv.trans: {α : Sort u} → {β : Sort v} → {γ : Sort w} → α ≃ β → β ≃ γ → α ≃ γEquiv.trans

pp_extended_field_notation Equiv.trans: {α : Sort u} → {β : Sort v} → {γ : Sort w} → α ≃ β → β ≃ γ → α ≃ γEquiv.trans

@[simps: ∀ {a : Sort u_2} {b : Sort u_1} {c : Sort u_3} (e₁ : a ≃ b) (e₂ : b ≃ c), Trans.trans e₁ e₂ = e₁.trans e₂simps]
instance: Trans Equiv Equiv Equivinstance : Trans: {α : Sort ?u.28602} →
{β : Sort ?u.28601} →
{γ : Sort ?u.28600} →
(α → β → Sort ?u.28605) →
(β → γ → Sort ?u.28604) →
outParam (α → γ → Sort ?u.28603) →
Sort (max(max(max(max(max(max1?u.28605)?u.28602)?u.28601)?u.28600)?u.28604)?u.28603)Trans Equiv: Sort ?u.28610 → Sort ?u.28609 → Sort (max(max1?u.28610)?u.28609)Equiv Equiv: Sort ?u.28618 → Sort ?u.28617 → Sort (max(max1?u.28618)?u.28617)Equiv Equiv: Sort ?u.28626 → Sort ?u.28625 → Sort (max(max1?u.28626)?u.28625)Equiv where
trans := Equiv.trans: {α : Sort ?u.28671} → {β : Sort ?u.28670} → {γ : Sort ?u.28669} → α ≃ β → β ≃ γ → α ≃ γEquiv.trans

-- porting note: this is not a syntactic tautology any more because
-- the coercion from `e` to a function is now `FunLike.coe` not `e.toFun`
@[simp] theorem toFun_as_coe: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.toFun = ↑etoFun_as_coe (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : e: α ≃ βe.toFun: {α : Sort ?u.29014} → {β : Sort ?u.29013} → α ≃ β → α → βtoFun = e: α ≃ βe := rfl: ∀ {α : Sort ?u.29254} {a : α}, a = arfl
#align equiv.to_fun_as_coe Equiv.toFun_as_coe: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.toFun = ↑eEquiv.toFun_as_coe

-- porting note: `simp` should prove this using `toFun_as_coe`, but it doesn't.
-- This might be a bug in `simp` -- see https://github.com/leanprover/lean4/issues/1937
-- If this issue is fixed then the simp linter probably will start complaining, and
-- this theorem can be deleted hopefully without breaking any `simp` proofs.
@[simp] theorem toFun_as_coe_apply: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (x : α), toFun e x = ↑e xtoFun_as_coe_apply (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) (x: αx : α: Sort uα) : e: α ≃ βe.toFun: {α : Sort ?u.29285} → {β : Sort ?u.29284} → α ≃ β → α → βtoFun x: αx = e: α ≃ βe x: αx := rfl: ∀ {α : Sort ?u.29358} {a : α}, a = arfl

@[simp] theorem invFun_as_coe: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.invFun = ↑e.symminvFun_as_coe (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : e: α ≃ βe.invFun: {α : Sort ?u.29390} → {β : Sort ?u.29389} → α ≃ β → β → αinvFun = e: α ≃ βe.symm: {α : Sort ?u.29397} → {β : Sort ?u.29396} → α ≃ β → β ≃ αsymm := rfl: ∀ {α : Sort ?u.29637} {a : α}, a = arfl
#align equiv.inv_fun_as_coe Equiv.invFun_as_coe: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.invFun = ↑e.symmEquiv.invFun_as_coe

protected theorem injective: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Injective ↑einjective (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : Injective: {α : Sort ?u.29665} → {β : Sort ?u.29664} → (α → β) → PropInjective e: α ≃ βe := EquivLike.injective: ∀ {E : Sort ?u.29741} {α : Sort ?u.29739} {β : Sort ?u.29740} [iE : EquivLike E α β] (e : E), Injective ↑eEquivLike.injective e: α ≃ βe
#align equiv.injective Equiv.injective: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Injective ↑eEquiv.injective

protected theorem surjective: ∀ (e : α ≃ β), Surjective ↑esurjective (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : Surjective: {α : Sort ?u.29781} → {β : Sort ?u.29780} → (α → β) → PropSurjective e: α ≃ βe := EquivLike.surjective: ∀ {E : Sort ?u.29858} {α : Sort ?u.29856} {β : Sort ?u.29857} [iE : EquivLike E α β] (e : E), Surjective ↑eEquivLike.surjective e: α ≃ βe
#align equiv.surjective Equiv.surjective: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Surjective ↑eEquiv.surjective

protected theorem bijective: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Bijective ↑ebijective (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : Bijective: {α : Sort ?u.29899} → {β : Sort ?u.29898} → (α → β) → PropBijective e: α ≃ βe := EquivLike.bijective: ∀ {E : Sort ?u.29975} {α : Sort ?u.29973} {β : Sort ?u.29974} [iE : EquivLike E α β] (e : E), Bijective ↑eEquivLike.bijective e: α ≃ βe
#align equiv.bijective Equiv.bijective: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Bijective ↑eEquiv.bijective

protected theorem subsingleton: α ≃ β → ∀ [inst : Subsingleton β], Subsingleton αsubsingleton (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) [Subsingleton: Sort ?u.30014 → PropSubsingleton β: Sort vβ] : Subsingleton: Sort ?u.30017 → PropSubsingleton α: Sort uα :=
e: α ≃ βe.injective: ∀ {α : Sort ?u.30022} {β : Sort ?u.30021} (e : α ≃ β), Injective ↑einjective.subsingleton: ∀ {α : Sort ?u.30027} {β : Sort ?u.30028} {f : α → β}, Injective f → ∀ [inst : Subsingleton β], Subsingleton αsubsingleton
#align equiv.subsingleton Equiv.subsingleton: ∀ {α : Sort u} {β : Sort v}, α ≃ β → ∀ [inst : Subsingleton β], Subsingleton αEquiv.subsingleton

protected theorem subsingleton.symm: α ≃ β → ∀ [inst : Subsingleton α], Subsingleton βsubsingleton.symm (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) [Subsingleton: Sort ?u.30065 → PropSubsingleton α: Sort uα] : Subsingleton: Sort ?u.30068 → PropSubsingleton β: Sort vβ :=
e: α ≃ βe.symm: {α : Sort ?u.30073} → {β : Sort ?u.30072} → α ≃ β → β ≃ αsymm.injective: ∀ {α : Sort ?u.30079} {β : Sort ?u.30078} (e : α ≃ β), Injective ↑einjective.subsingleton: ∀ {α : Sort ?u.30084} {β : Sort ?u.30085} {f : α → β}, Injective f → ∀ [inst : Subsingleton β], Subsingleton αsubsingleton
#align equiv.subsingleton.symm Equiv.subsingleton.symm: ∀ {α : Sort u} {β : Sort v}, α ≃ β → ∀ [inst : Subsingleton α], Subsingleton βEquiv.subsingleton.symm

theorem subsingleton_congr: α ≃ β → (Subsingleton α ↔ Subsingleton β)subsingleton_congr (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : Subsingleton: Sort ?u.30122 → PropSubsingleton α: Sort uα ↔ Subsingleton: Sort ?u.30123 → PropSubsingleton β: Sort vβ :=
⟨fun _: ?m.30135_ => e: α ≃ βe.symm: {α : Sort ?u.30138} → {β : Sort ?u.30137} → α ≃ β → β ≃ αsymm.subsingleton: ∀ {α : Sort ?u.30144} {β : Sort ?u.30143}, α ≃ β → ∀ [inst : Subsingleton β], Subsingleton αsubsingleton, fun _: ?m.30162_ => e: α ≃ βe.subsingleton: ∀ {α : Sort ?u.30165} {β : Sort ?u.30164}, α ≃ β → ∀ [inst : Subsingleton β], Subsingleton αsubsingleton⟩
#align equiv.subsingleton_congr Equiv.subsingleton_congr: ∀ {α : Sort u} {β : Sort v}, α ≃ β → (Subsingleton α ↔ Subsingleton β)Equiv.subsingleton_congr

instance equiv_subsingleton_cod: ∀ {α : Sort u} {β : Sort v} [inst : Subsingleton β], Subsingleton (α ≃ β)equiv_subsingleton_cod [Subsingleton: Sort ?u.30190 → PropSubsingleton β: Sort vβ] : Subsingleton: Sort ?u.30193 → PropSubsingleton (α: Sort uα ≃ β: Sort vβ) :=
⟨fun _: ?m.30204_ _: ?m.30207_ => Equiv.ext: ∀ {α : Sort ?u.30210} {β : Sort ?u.30209} {f g : α ≃ β}, (∀ (x : α), ↑f x = ↑g x) → f = gEquiv.ext fun _: ?m.30221_ => Subsingleton.elim: ∀ {α : Sort ?u.30223} [h : Subsingleton α] (a b : α), a = bSubsingleton.elim _: ?m.30224_ _: ?m.30224_⟩

instance equiv_subsingleton_dom: ∀ [inst : Subsingleton α], Subsingleton (α ≃ β)equiv_subsingleton_dom [Subsingleton: Sort ?u.30293 → PropSubsingleton α: Sort uα] : Subsingleton: Sort ?u.30296 → PropSubsingleton (α: Sort uα ≃ β: Sort vβ) :=
⟨fun f: ?m.30307f _: ?m.30310_ => Equiv.ext: ∀ {α : Sort ?u.30313} {β : Sort ?u.30312} {f g : α ≃ β}, (∀ (x : α), ↑f x = ↑g x) → f = gEquiv.ext fun _: ?m.30324_ => @Subsingleton.elim: ∀ {α : Sort ?u.30326} [h : Subsingleton α] (a b : α), a = bSubsingleton.elim _: Sort ?u.30326_ (Equiv.subsingleton.symm: ∀ {α : Sort ?u.30329} {β : Sort ?u.30328}, α ≃ β → ∀ [inst : Subsingleton α], Subsingleton βEquiv.subsingleton.symm f: ?m.30307f) _: ?m.30327_ _: ?m.30327_⟩

instance permUnique: [inst : Subsingleton α] → Unique (Perm α)permUnique [Subsingleton: Sort ?u.30387 → PropSubsingleton α: Sort uα] : Unique: Sort ?u.30390 → Sort (max1?u.30390)Unique (Perm: Sort ?u.30391 → Sort (max1?u.30391)Perm α: Sort uα) :=
uniqueOfSubsingleton: {α : Sort ?u.30394} → [inst : Subsingleton α] → α → Unique αuniqueOfSubsingleton (Equiv.refl: (α : Sort ?u.30419) → α ≃ αEquiv.refl α: Sort uα)

theorem Perm.subsingleton_eq_refl: ∀ {α : Sort u} [inst : Subsingleton α] (e : Perm α), e = Equiv.refl αPerm.subsingleton_eq_refl [Subsingleton: Sort ?u.30475 → PropSubsingleton α: Sort uα] (e: Perm αe : Perm: Sort ?u.30478 → Sort (max1?u.30478)Perm α: Sort uα) : e: Perm αe = Equiv.refl: (α : Sort ?u.30482) → α ≃ αEquiv.refl α: Sort uα :=
Subsingleton.elim: ∀ {α : Sort ?u.30487} [h : Subsingleton α] (a b : α), a = bSubsingleton.elim _: ?m.30488_ _: ?m.30488_
#align equiv.perm.subsingleton_eq_refl Equiv.Perm.subsingleton_eq_refl: ∀ {α : Sort u} [inst : Subsingleton α] (e : Perm α), e = Equiv.refl αEquiv.Perm.subsingleton_eq_refl

/-- Transfer `DecidableEq` across an equivalence. -/
protected def decidableEq: α ≃ β → [inst : DecidableEq β] → DecidableEq αdecidableEq (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) [DecidableEq: Sort ?u.30548 → Sort (max1?u.30548)DecidableEq β: Sort vβ] : DecidableEq: Sort ?u.30557 → Sort (max1?u.30557)DecidableEq α: Sort uα :=
e: α ≃ βe.injective: ∀ {α : Sort ?u.30570} {β : Sort ?u.30569} (e : α ≃ β), Injective ↑einjective.decidableEq: {α : Sort ?u.30576} → {β : Sort ?u.30575} → {f : α → β} → [inst : DecidableEq β] → Injective f → DecidableEq αdecidableEq
#align equiv.decidable_eq Equiv.decidableEq: {α : Sort u} → {β : Sort v} → α ≃ β → [inst : DecidableEq β] → DecidableEq αEquiv.decidableEq

theorem nonempty_congr: ∀ {α : Sort u} {β : Sort v}, α ≃ β → (Nonempty α ↔ Nonempty β)nonempty_congr (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : Nonempty: Sort ?u.30746 → PropNonempty α: Sort uα ↔ Nonempty: Sort ?u.30747 → PropNonempty β: Sort vβ := Nonempty.congr: ∀ {α : Sort ?u.30750} {β : Sort ?u.30751}, (α → β) → (β → α) → (Nonempty α ↔ Nonempty β)Nonempty.congr e: α ≃ βe e: α ≃ βe.symm: {α : Sort ?u.30825} → {β : Sort ?u.30824} → α ≃ β → β ≃ αsymm
#align equiv.nonempty_congr Equiv.nonempty_congr: ∀ {α : Sort u} {β : Sort v}, α ≃ β → (Nonempty α ↔ Nonempty β)Equiv.nonempty_congr

protected theorem nonempty: ∀ {α : Sort u} {β : Sort v}, α ≃ β → ∀ [inst : Nonempty β], Nonempty αnonempty (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) [Nonempty: Sort ?u.30914 → PropNonempty β: Sort vβ] : Nonempty: Sort ?u.30917 → PropNonempty α: Sort uα := e: α ≃ βe.nonempty_congr: ∀ {α : Sort ?u.30922} {β : Sort ?u.30921}, α ≃ β → (Nonempty α ↔ Nonempty β)nonempty_congr.mpr: ∀ {a b : Prop}, (a ↔ b) → b → ampr ‹_›
#align equiv.nonempty Equiv.nonempty: ∀ {α : Sort u} {β : Sort v}, α ≃ β → ∀ [inst : Nonempty β], Nonempty αEquiv.nonempty

/-- If `α ≃ β` and `β` is inhabited, then so is `α`. -/
protected def inhabited: {α : Sort u} → {β : Sort v} → [inst : Inhabited β] → α ≃ β → Inhabited αinhabited [Inhabited: Sort ?u.30946 → Sort (max1?u.30946)Inhabited β: Sort vβ] (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : Inhabited: Sort ?u.30953 → Sort (max1?u.30953)Inhabited α: Sort uα := ⟨e: α ≃ βe.symm: {α : Sort ?u.30963} → {β : Sort ?u.30962} → α ≃ β → β ≃ αsymm default: {α : Sort ?u.31032} → [self : Inhabited α] → αdefault⟩
#align equiv.inhabited Equiv.inhabited: {α : Sort u} → {β : Sort v} → [inst : Inhabited β] → α ≃ β → Inhabited αEquiv.inhabited

/-- If `α ≃ β` and `β` is a singleton type, then so is `α`. -/
protected def unique: {α : Sort u} → {β : Sort v} → [inst : Unique β] → α ≃ β → Unique αunique [Unique: Sort ?u.31213 → Sort (max1?u.31213)Unique β: Sort vβ] (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : Unique: Sort ?u.31220 → Sort (max1?u.31220)Unique α: Sort uα := e: α ≃ βe.symm: {α : Sort ?u.31225} → {β : Sort ?u.31224} → α ≃ β → β ≃ αsymm.surjective: ∀ {α : Sort ?u.31231} {β : Sort ?u.31230} (e : α ≃ β), Surjective ↑esurjective.unique: {α : Sort ?u.31238} → {β : Sort ?u.31237} → (f : α → β) → Surjective f → [inst : Unique α] → Unique βunique
#align equiv.unique Equiv.unique: {α : Sort u} → {β : Sort v} → [inst : Unique β] → α ≃ β → Unique αEquiv.unique

/-- Equivalence between equal types. -/
protected def cast: {α β : Sort u_1} → α = β → α ≃ βcast {α: Sort ?u.31342α β: Sort ?u.31342β : Sort _: Type ?u.31339SortSort _: Type ?u.31339 _} (h: α = βh : α: Sort ?u.31339α = β: Sort ?u.31342β) : α: Sort ?u.31339α ≃ β: Sort ?u.31342β :=
⟨cast: {α β : Sort ?u.31385} → α = β → α → βcast h: α = βh, cast: {α β : Sort ?u.31396} → α = β → α → βcast h: α = βh.symm: ∀ {α : Sort ?u.31401} {a b : α}, a = b → b = asymm, fun _: ?m.31413_ => byGoals accomplished! 🐙 α✝: Sort uβ✝: Sort vγ: Sort wα, β: Sort ?u.31342h: α = βx✝: αcast (_ : β = α) (cast h x✝) = x✝cases h: α = βhα✝: Sort uβ: Sort vγ: Sort wα: Sort ?u.31342x✝: αreflcast (_ : α = α) (cast (_ : α = α) x✝) = x✝;α✝: Sort uβ: Sort vγ: Sort wα: Sort ?u.31342x✝: αreflcast (_ : α = α) (cast (_ : α = α) x✝) = x✝ α✝: Sort uβ✝: Sort vγ: Sort wα, β: Sort ?u.31342h: α = βx✝: αcast (_ : β = α) (cast h x✝) = x✝rflGoals accomplished! 🐙, fun _: ?m.31419_ => byGoals accomplished! 🐙 α✝: Sort uβ✝: Sort vγ: Sort wα, β: Sort ?u.31342h: α = βx✝: βcast h (cast (_ : β = α) x✝) = x✝cases h: α = βhα✝: Sort uβ: Sort vγ: Sort wα: Sort ?u.31342x✝: αreflcast (_ : α = α) (cast (_ : α = α) x✝) = x✝;α✝: Sort uβ: Sort vγ: Sort wα: Sort ?u.31342x✝: αreflcast (_ : α = α) (cast (_ : α = α) x✝) = x✝ α✝: Sort uβ✝: Sort vγ: Sort wα, β: Sort ?u.31342h: α = βx✝: βcast h (cast (_ : β = α) x✝) = x✝rflGoals accomplished! 🐙⟩
#align equiv.cast Equiv.cast: {α β : Sort u_1} → α = β → α ≃ βEquiv.cast

@[simp] theorem coe_fn_symm_mk: ∀ {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : LeftInverse g f) (r : Function.RightInverse g f),
↑{ toFun := f, invFun := g, left_inv := l, right_inv := r }.symm = gcoe_fn_symm_mk (f: α → βf : α: Sort uα → β: Sort vβ) (g: ?m.31697g l: ?m.31700l r: ?m.31703r) : ((Equiv.mk: {α : Sort ?u.31711} →
{β : Sort ?u.31710} →
(toFun : α → β) → (invFun : β → α) → LeftInverse invFun toFun → Function.RightInverse invFun toFun → α ≃ βEquiv.mk f: α → βf g: ?m.31697g l: ?m.31700l r: ?m.31703r).symm: {α : Sort ?u.31732} → {β : Sort ?u.31731} → α ≃ β → β ≃ αsymm : β: Sort vβ → α: Sort uα) = g: ?m.31697g := rfl: ∀ {α : Sort ?u.31814} {a : α}, a = arfl
#align equiv.coe_fn_symm_mk Equiv.coe_fn_symm_mk: ∀ {α : Sort u} {β : Sort v} (f : α → β) (g : β → α) (l : LeftInverse g f) (r : Function.RightInverse g f),
↑{ toFun := f, invFun := g, left_inv := l, right_inv := r }.symm = gEquiv.coe_fn_symm_mk

@[simp] theorem coe_refl: ∀ {α : Sort u}, ↑(Equiv.refl α) = idcoe_refl : (Equiv.refl: (α : Sort ?u.31876) → α ≃ αEquiv.refl α: Sort uα : α: Sort uα → α: Sort uα) = id: {α : Sort ?u.31940} → α → αid := rfl: ∀ {α : Sort ?u.31979} {a : α}, a = arfl
#align equiv.coe_refl Equiv.coe_refl: ∀ {α : Sort u}, ↑(Equiv.refl α) = idEquiv.coe_refl

/-- This cannot be a `simp` lemmas as it incorrectly matches against `e : α ≃ synonym α`, when
`synonym α` is semireducible. This makes a mess of `Multiplicative.ofAdd` etc. -/
theorem Perm.coe_subsingleton: ∀ {α : Type u_1} [inst : Subsingleton α] (e : Perm α), ↑e = idPerm.coe_subsingleton {α: Type ?u.32011α : Type _: Type (?u.32011+1)Type _} [Subsingleton: Sort ?u.32014 → PropSubsingleton α: Type ?u.32011α] (e: Perm αe : Perm: Sort ?u.32017 → Sort (max1?u.32017)Perm α: Type ?u.32011α) : (e: Perm αe : α: Type ?u.32011α → α: Type ?u.32011α) = id: {α : Sort ?u.32093} → α → αid := byGoals accomplished! 🐙
α✝: Sort uβ: Sort vγ: Sort wα: Type u_1inst✝: Subsingleton αe: Perm α↑e = idrw [α✝: Sort uβ: Sort vγ: Sort wα: Type u_1inst✝: Subsingleton αe: Perm α↑e = idPerm.subsingleton_eq_refl: ∀ {α : Sort ?u.32144} [inst : Subsingleton α] (e : Perm α), e = Equiv.refl αPerm.subsingleton_eq_refl e: Perm αe,α✝: Sort uβ: Sort vγ: Sort wα: Type u_1inst✝: Subsingleton αe: Perm α↑(Equiv.refl α) = id α✝: Sort uβ: Sort vγ: Sort wα: Type u_1inst✝: Subsingleton αe: Perm α↑e = idcoe_refl: ∀ {α : Sort ?u.32170}, ↑(Equiv.refl α) = idcoe_reflα✝: Sort uβ: Sort vγ: Sort wα: Type u_1inst✝: Subsingleton αe: Perm αid = id]Goals accomplished! 🐙
#align equiv.perm.coe_subsingleton Equiv.Perm.coe_subsingleton: ∀ {α : Type u_1} [inst : Subsingleton α] (e : Perm α), ↑e = idEquiv.Perm.coe_subsingleton

-- porting note: marking this as `@[simp]` because `simp` doesn't fire on `coe_refl`
-- in an expression such as `Equiv.refl a x`
@[simp] theorem refl_apply: ∀ {α : Sort u} (x : α), ↑(Equiv.refl α) x = xrefl_apply (x: αx : α: Sort uα) : Equiv.refl: (α : Sort ?u.32226) → α ≃ αEquiv.refl α: Sort uα x: αx = x: αx := rfl: ∀ {α : Sort ?u.32291} {a : α}, a = arfl
#align equiv.refl_apply Equiv.refl_apply: ∀ {α : Sort u} (x : α), ↑(Equiv.refl α) x = xEquiv.refl_apply

@[simp] theorem coe_trans: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ), ↑(f.trans g) = ↑g ∘ ↑fcoe_trans (f: α ≃ βf : α: Sort uα ≃ β: Sort vβ) (g: β ≃ γg : β: Sort vβ ≃ γ: Sort wγ) : (f: α ≃ βf.trans: {α : Sort ?u.32337} → {β : Sort ?u.32336} → {γ : Sort ?u.32335} → α ≃ β → β ≃ γ → α ≃ γtrans g: β ≃ γg : α: Sort uα → γ: Sort wγ) = g: β ≃ γg ∘ f: α ≃ βf := rfl: ∀ {α : Sort ?u.32567} {a : α}, a = arfl
#align equiv.coe_trans Equiv.coe_trans: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ), ↑(f.trans g) = ↑g ∘ ↑fEquiv.coe_trans

-- porting note: marking this as `@[simp]` because `simp` doesn't fire on `coe_trans`
-- in an expression such as `Equiv.trans f g x`
@[simp] theorem trans_apply: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ) (a : α), ↑(f.trans g) a = ↑g (↑f a)trans_apply (f: α ≃ βf : α: Sort uα ≃ β: Sort vβ) (g: β ≃ γg : β: Sort vβ ≃ γ: Sort wγ) (a: αa : α: Sort uα) : (f: α ≃ βf.trans: {α : Sort ?u.32628} → {β : Sort ?u.32627} → {γ : Sort ?u.32626} → α ≃ β → β ≃ γ → α ≃ γtrans g: β ≃ γg) a: αa = g: β ≃ γg (f: α ≃ βf a: αa) := rfl: ∀ {α : Sort ?u.32842} {a : α}, a = arfl
#align equiv.trans_apply Equiv.trans_apply: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ) (a : α), ↑(f.trans g) a = ↑g (↑f a)Equiv.trans_apply

@[simp] theorem apply_symm_apply: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (x : β), ↑e (↑e.symm x) = xapply_symm_apply (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) (x: βx : β: Sort vβ) : e: α ≃ βe (e: α ≃ βe.symm: {α : Sort ?u.32964} → {β : Sort ?u.32963} → α ≃ β → β ≃ αsymm x: βx) = x: βx := e: α ≃ βe.right_inv: ∀ {α : Sort ?u.33036} {β : Sort ?u.33035} (self : α ≃ β), Function.RightInverse self.invFun self.toFunright_inv x: βx
#align equiv.apply_symm_apply Equiv.apply_symm_apply: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (x : β), ↑e (↑e.symm x) = xEquiv.apply_symm_apply

@[simp] theorem symm_apply_apply: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (x : α), ↑e.symm (↑e x) = xsymm_apply_apply (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) (x: αx : α: Sort uα) : e: α ≃ βe.symm: {α : Sort ?u.33093} → {β : Sort ?u.33092} → α ≃ β → β ≃ αsymm (e: α ≃ βe x: αx) = x: αx := e: α ≃ βe.left_inv: ∀ {α : Sort ?u.33231} {β : Sort ?u.33230} (self : α ≃ β), LeftInverse self.invFun self.toFunleft_inv x: αx
#align equiv.symm_apply_apply Equiv.symm_apply_apply: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (x : α), ↑e.symm (↑e x) = xEquiv.symm_apply_apply

@[simp] theorem symm_comp_self: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), ↑e.symm ∘ ↑e = idsymm_comp_self (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : e: α ≃ βe.symm: {α : Sort ?u.33292} → {β : Sort ?u.33291} → α ≃ β → β ≃ αsymm ∘ e: α ≃ βe = id: {α : Sort ?u.33430} → α → αid := funext: ∀ {α : Sort ?u.33470} {β : α → Sort ?u.33469} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = gfunext e: α ≃ βe.symm_apply_apply: ∀ {α : Sort ?u.33484} {β : Sort ?u.33483} (e : α ≃ β) (x : α), ↑e.symm (↑e x) = xsymm_apply_apply
#align equiv.symm_comp_self Equiv.symm_comp_self: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), ↑e.symm ∘ ↑e = idEquiv.symm_comp_self

@[simp] theorem self_comp_symm: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), ↑e ∘ ↑e.symm = idself_comp_symm (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : e: α ≃ βe ∘ e: α ≃ βe.symm: {α : Sort ?u.33623} → {β : Sort ?u.33622} → α ≃ β → β ≃ αsymm = id: {α : Sort ?u.33693} → α → αid := funext: ∀ {α : Sort ?u.33733} {β : α → Sort ?u.33732} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = gfunext e: α ≃ βe.apply_symm_apply: ∀ {α : Sort ?u.33747} {β : Sort ?u.33746} (e : α ≃ β) (x : β), ↑e (↑e.symm x) = xapply_symm_apply
#align equiv.self_comp_symm Equiv.self_comp_symm: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), ↑e ∘ ↑e.symm = idEquiv.self_comp_symm

@[simp] theorem symm_trans_apply: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ) (a : γ), ↑(f.trans g).symm a = ↑f.symm (↑g.symm a)symm_trans_apply (f: α ≃ βf : α: Sort uα ≃ β: Sort vβ) (g: β ≃ γg : β: Sort vβ ≃ γ: Sort wγ) (a: γa : γ: Sort wγ) :
(f: α ≃ βf.trans: {α : Sort ?u.33819} → {β : Sort ?u.33818} → {γ : Sort ?u.33817} → α ≃ β → β ≃ γ → α ≃ γtrans g: β ≃ γg).symm: {α : Sort ?u.33835} → {β : Sort ?u.33834} → α ≃ β → β ≃ αsymm a: γa = f: α ≃ βf.symm: {α : Sort ?u.33905} → {β : Sort ?u.33904} → α ≃ β → β ≃ αsymm (g: β ≃ γg.symm: {α : Sort ?u.33973} → {β : Sort ?u.33972} → α ≃ β → β ≃ αsymm a: γa) := rfl: ∀ {α : Sort ?u.34045} {a : α}, a = arfl
#align equiv.symm_trans_apply Equiv.symm_trans_apply: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ) (a : γ), ↑(f.trans g).symm a = ↑f.symm (↑g.symm a)Equiv.symm_trans_apply

-- The `simp` attribute is needed to make this a `dsimp` lemma.
-- `simp` will always rewrite with `Equiv.symm_symm` before this has a chance to fire.
@[simp, nolint simpNF: Std.Tactic.Lint.LintersimpNF] theorem symm_symm_apply: ∀ {α : Sort u} {β : Sort v} (f : α ≃ β) (b : α), ↑f.symm.symm b = ↑f bsymm_symm_apply (f: α ≃ βf : α: Sort uα ≃ β: Sort vβ) (b: αb : α: Sort uα) : f: α ≃ βf.symm: {α : Sort ?u.34104} → {β : Sort ?u.34103} → α ≃ β → β ≃ αsymm.symm: {α : Sort ?u.34110} → {β : Sort ?u.34109} → α ≃ β → β ≃ αsymm b: αb = f: α ≃ βf b: αb := rfl: ∀ {α : Sort ?u.34235} {a : α}, a = arfl
#align equiv.symm_symm_apply Equiv.symm_symm_apply: ∀ {α : Sort u} {β : Sort v} (f : α ≃ β) (b : α), ↑f.symm.symm b = ↑f bEquiv.symm_symm_apply

theorem apply_eq_iff_eq: ∀ {α : Sort u} {β : Sort v} (f : α ≃ β) {x y : α}, ↑f x = ↑f y ↔ x = yapply_eq_iff_eq (f: α ≃ βf : α: Sort uα ≃ β: Sort vβ) {x: αx y: αy : α: Sort uα} : f: α ≃ βf x: αx = f: α ≃ βf y: αy ↔ x: αx = y: αy := EquivLike.apply_eq_iff_eq: ∀ {E : Sort ?u.34412} {α : Sort ?u.34413} {β : Sort ?u.34411} [iE : EquivLike E α β] (f : E) {x y : α},
↑f x = ↑f y ↔ x = yEquivLike.apply_eq_iff_eq f: α ≃ βf
#align equiv.apply_eq_iff_eq Equiv.apply_eq_iff_eq: ∀ {α : Sort u} {β : Sort v} (f : α ≃ β) {x y : α}, ↑f x = ↑f y ↔ x = yEquiv.apply_eq_iff_eq

theorem apply_eq_iff_eq_symm_apply: ∀ {α : Sort u} {β : Sort v} {x : α} {y : (fun x => β) x} (f : α ≃ β), ↑f x = y ↔ x = ↑f.symm yapply_eq_iff_eq_symm_apply (f: α ≃ βf : α: Sort uα ≃ β: Sort vβ) : f: α ≃ βf x: ?m.34536x = y: ?m.34594y ↔ x: ?m.34536x = f: α ≃ βf.symm: {α : Sort ?u.34654} → {β : Sort ?u.34653} → α ≃ β → β ≃ αsymm y: ?m.34594y := byGoals accomplished! 🐙
α: Sort uβ: Sort vγ: Sort wx: αy: (fun x => β) xf: α ≃ β↑f x = y ↔ x = ↑f.symm yconv_lhs => α: Sort uβ: Sort vγ: Sort wx: αy: (fun x => β) xf: α ≃ β↑f x = y ↔ x = ↑f.symm yrw [α: Sort uβ: Sort vγ: Sort wx: αy: (fun x => β) xf: α ≃ β↑f x = y← apply_symm_apply: ∀ {α : Sort ?u.34759} {β : Sort ?u.34758} (e : α ≃ β) (x : β), ↑e (↑e.symm x) = xapply_symm_apply f: α ≃ βf y: (fun x => β) xyα: Sort uβ: Sort vγ: Sort wx: αy: (fun x => β) xf: α ≃ β↑f x = ↑f (↑f.symm y)]α: Sort uβ: Sort vγ: Sort wx: αy: (fun x => β) xf: α ≃ β↑f x = ↑f (↑f.symm y)
α: Sort uβ: Sort vγ: Sort wx: αy: (fun x => β) xf: α ≃ β↑f x = y ↔ x = ↑f.symm yrw [α: Sort uβ: Sort vγ: Sort wx: αy: (fun x => β) xf: α ≃ β↑f x = ↑f (↑f.symm y) ↔ x = ↑f.symm yapply_eq_iff_eq: ∀ {α : Sort ?u.34799} {β : Sort ?u.34798} (f : α ≃ β) {x y : α}, ↑f x = ↑f y ↔ x = yapply_eq_iff_eqα: Sort uβ: Sort vγ: Sort wx: αy: (fun x => β) xf: α ≃ βx = ↑f.symm y ↔ x = ↑f.symm y]Goals accomplished! 🐙
#align equiv.apply_eq_iff_eq_symm_apply Equiv.apply_eq_iff_eq_symm_apply: ∀ {α : Sort u} {β : Sort v} {x : α} {y : (fun x => β) x} (f : α ≃ β), ↑f x = y ↔ x = ↑f.symm yEquiv.apply_eq_iff_eq_symm_apply

@[simp] theorem cast_apply: ∀ {α β : Sort u_1} (h : α = β) (x : α), ↑(Equiv.cast h) x = cast h xcast_apply {α: ?m.34873α β: ?m.34876β} (h: α = βh : α: ?m.34873α = β: ?m.34876β) (x: αx : α: ?m.34873α) : Equiv.cast: {α β : Sort ?u.34887} → α = β → α ≃ βEquiv.cast h: α = βh x: αx = cast: {α β : Sort ?u.34959} → α = β → α → βcast h: α = βh x: αx := rfl: ∀ {α : Sort ?u.34972} {a : α}, a = arfl
#align equiv.cast_apply Equiv.cast_apply: ∀ {α β : Sort u_1} (h : α = β) (x : α), ↑(Equiv.cast h) x = cast h xEquiv.cast_apply

@[simp] theorem cast_symm: ∀ {α β : Sort u_1} (h : α = β), (Equiv.cast h).symm = Equiv.cast (_ : β = α)cast_symm {α: Sort u_1α β: ?m.35019β} (h: α = βh : α: ?m.35016α = β: ?m.35019β) : (Equiv.cast: {α β : Sort ?u.35028} → α = β → α ≃ βEquiv.cast h: α = βh).symm: {α : Sort ?u.35035} → {β : Sort ?u.35034} → α ≃ β → β ≃ αsymm = Equiv.cast: {α β : Sort ?u.35043} → α = β → α ≃ βEquiv.cast h: α = βh.symm: ∀ {α : Sort ?u.35046} {a b : α}, a = b → b = asymm := rfl: ∀ {α : Sort ?u.35062} {a : α}, a = arfl
#align equiv.cast_symm Equiv.cast_symm: ∀ {α β : Sort u_1} (h : α = β), (Equiv.cast h).symm = Equiv.cast (_ : β = α)Equiv.cast_symm

@[simp] theorem cast_refl: ∀ {α : Sort u_1} (h : optParam (α = α) (_ : α = α)), Equiv.cast h = Equiv.refl αcast_refl {α: ?m.35117α} (h: optParam (α = α) (_ : ?m.35126 = ?m.35126)h : α: ?m.35117α = α: ?m.35117α := rfl: ∀ {α : Sort ?u.35124} {a : α}, a = arfl) : Equiv.cast: {α β : Sort ?u.35137} → α = β → α ≃ βEquiv.cast h: optParam (α = α) (_ : ?m.35126 = ?m.35126)h = Equiv.refl: (α : Sort ?u.35143) → α ≃ αEquiv.refl α: ?m.35117α := rfl: ∀ {α : Sort ?u.35150} {a : α}, a = arfl
#align equiv.cast_refl Equiv.cast_refl: ∀ {α : Sort u_1} (h : optParam (α = α) (_ : α = α)), Equiv.cast h = Equiv.refl αEquiv.cast_refl

@[simp] theorem cast_trans: ∀ {α β γ : Sort u_1} (h : α = β) (h2 : β = γ), (Equiv.cast h).trans (Equiv.cast h2) = Equiv.cast (_ : α = γ)cast_trans {α: Sort u_1α β: ?m.35189β γ: ?m.35192γ} (h: α = βh : α: ?m.35186α = β: ?m.35189β) (h2: β = γh2 : β: ?m.35189β = γ: ?m.35192γ) :
(Equiv.cast: {α β : Sort ?u.35206} → α = β → α ≃ βEquiv.cast h: α = βh).trans: {α : Sort ?u.35214} → {β : Sort ?u.35213} → {γ : Sort ?u.35212} → α ≃ β → β ≃ γ → α ≃ γtrans (Equiv.cast: {α β : Sort ?u.35225} → α = β → α ≃ βEquiv.cast h2: β = γh2) = Equiv.cast: {α β : Sort ?u.35230} → α = β → α ≃ βEquiv.cast (h: α = βh.trans: ∀ {α : Sort ?u.35233} {a b c : α}, a = b → b = c → a = ctrans h2: β = γh2) :=
ext: ∀ {α : Sort ?u.35255} {β : Sort ?u.35254} {f g : α ≃ β}, (∀ (x : α), ↑f x = ↑g x) → f = gext fun x: ?m.35266x => byGoals accomplished! 🐙 α✝: Sort uβ✝: Sort vγ✝: Sort wα, β, γ: Sort u_1h: α = βh2: β = γx: α↑((Equiv.cast h).trans (Equiv.cast h2)) x = ↑(Equiv.cast (_ : α = γ)) xsubsts h: α = βh h2: α = γh2α✝: Sort uβ: Sort vγ: Sort wα: Sort u_1x: α↑((Equiv.cast (_ : α = α)).trans (Equiv.cast (_ : α = α))) x = ↑(Equiv.cast (_ : α = α)) x;α✝: Sort uβ: Sort vγ: Sort wα: Sort u_1x: α↑((Equiv.cast (_ : α = α)).trans (Equiv.cast (_ : α = α))) x = ↑(Equiv.cast (_ : α = α)) x α✝: Sort uβ✝: Sort vγ✝: Sort wα, β, γ: Sort u_1h: α = βh2: β = γx: α↑((Equiv.cast h).trans (Equiv.cast h2)) x = ↑(Equiv.cast (_ : α = γ)) xrflGoals accomplished! 🐙
#align equiv.cast_trans Equiv.cast_trans: ∀ {α β γ : Sort u_1} (h : α = β) (h2 : β = γ), (Equiv.cast h).trans (Equiv.cast h2) = Equiv.cast (_ : α = γ)Equiv.cast_trans

theorem cast_eq_iff_heq: ∀ {α β : Sort u_1} (h : α = β) {a : α} {b : β}, ↑(Equiv.cast h) a = b ↔ HEq a bcast_eq_iff_heq {α: ?m.35347α β: Sort u_1β} (h: α = βh : α: ?m.35347α = β: ?m.35350β) {a: αa : α: ?m.35347α} {b: βb : β: ?m.35350β} : Equiv.cast: {α β : Sort ?u.35363} → α = β → α ≃ βEquiv.cast h: α = βh a: αa = b: βb ↔ HEq: {α : Sort ?u.35437} → α → {β : Sort ?u.35437} → β → PropHEq a: αa b: βb := byGoals accomplished! 🐙
α✝: Sort uβ✝: Sort vγ: Sort wα, β: Sort u_1h: α = βa: αb: β↑(Equiv.cast h) a = b ↔ HEq a bsubst h: α = βhα✝: Sort uβ: Sort vγ: Sort wα: Sort u_1a, b: α↑(Equiv.cast (_ : α = α)) a = b ↔ HEq a b;α✝: Sort uβ: Sort vγ: Sort wα: Sort u_1a, b: α↑(Equiv.cast (_ : α = α)) a = b ↔ HEq a b α✝: Sort uβ✝: Sort vγ: Sort wα, β: Sort u_1h: α = βa: αb: β↑(Equiv.cast h) a = b ↔ HEq a bsimp [coe_refl: ∀ {α : Sort ?u.35462}, ↑(Equiv.refl α) = idcoe_refl]Goals accomplished! 🐙
#align equiv.cast_eq_iff_heq Equiv.cast_eq_iff_heq: ∀ {α β : Sort u_1} (h : α = β) {a : α} {b : β}, ↑(Equiv.cast h) a = b ↔ HEq a bEquiv.cast_eq_iff_heq

theorem symm_apply_eq: ∀ {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : (fun x => α) x}, ↑e.symm x = y ↔ x = ↑e ysymm_apply_eq {α: ?m.35654α β: ?m.35657β} (e: α ≃ βe : α: ?m.35654α ≃ β: ?m.35657β) {x: βx y: (fun x => α) xy} : e: α ≃ βe.symm: {α : Sort ?u.35672} → {β : Sort ?u.35671} → α ≃ β → β ≃ αsymm x: ?m.35664x = y: ?m.35667y ↔ x: ?m.35664x = e: α ≃ βe y: ?m.35667y :=
⟨fun H: ?m.35829H => byGoals accomplished! 🐙 α✝: Sort uβ✝: Sort vγ: Sort wα: Sort u_1β: Sort u_2e: α ≃ βx: βy: (fun x => α) xH: ↑e.symm x = yx = ↑e ysimp [H: ↑e.symm x = yH.symm: ∀ {α : Sort ?u.35845} {a b : α}, a = b → b = asymm]Goals accomplished! 🐙, fun H: ?m.35836H => byGoals accomplished! 🐙 α✝: Sort uβ✝: Sort vγ: Sort wα: Sort u_1β: Sort u_2e: α ≃ βx: βy: (fun x => α) xH: x = ↑e y↑e.symm x = ysimp [H: x = ↑e yH]Goals accomplished! 🐙⟩
#align equiv.symm_apply_eq Equiv.symm_apply_eq: ∀ {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : (fun x => α) x}, ↑e.symm x = y ↔ x = ↑e yEquiv.symm_apply_eq

theorem eq_symm_apply: ∀ {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : (fun x => α) x}, y = ↑e.symm x ↔ ↑e y = xeq_symm_apply {α: ?m.36056α β: ?m.36059β} (e: α ≃ βe : α: ?m.36056α ≃ β: ?m.36059β) {x: βx y: (fun x => α) xy} : y: ?m.36069y = e: α ≃ βe.symm: {α : Sort ?u.36074} → {β : Sort ?u.36073} → α ≃ β → β ≃ αsymm x: ?m.36066x ↔ e: α ≃ βe y: ?m.36069y = x: ?m.36066x :=
(eq_comm: ∀ {α : Sort ?u.36223} {a b : α}, a = b ↔ b = aeq_comm.trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)trans e: α ≃ βe.symm_apply_eq: ∀ {α : Sort ?u.36237} {β : Sort ?u.36238} (e : α ≃ β) {x : β} {y : (fun x => α) x}, ↑e.symm x = y ↔ x = ↑e ysymm_apply_eq).trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)trans eq_comm: ∀ {α : Sort ?u.36273} {a b : α}, a = b ↔ b = aeq_comm
#align equiv.eq_symm_apply Equiv.eq_symm_apply: ∀ {α : Sort u_1} {β : Sort u_2} (e : α ≃ β) {x : β} {y : (fun x => α) x}, y = ↑e.symm x ↔ ↑e y = xEquiv.eq_symm_apply

@[simp] theorem symm_symm: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.symm.symm = esymm_symm (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : e: α ≃ βe.symm: {α : Sort ?u.36302} → {β : Sort ?u.36301} → α ≃ β → β ≃ αsymm.symm: {α : Sort ?u.36308} → {β : Sort ?u.36307} → α ≃ β → β ≃ αsymm = e: α ≃ βe := byGoals accomplished! 🐙 α: Sort uβ: Sort vγ: Sort we: α ≃ βe.symm.symm = ecases e: α ≃ βeα: Sort uβ: Sort vγ: Sort wtoFun✝: α → βinvFun✝: β → αleft_inv✝: LeftInverse invFun✝ toFun✝right_inv✝: Function.RightInverse invFun✝ toFun✝mk{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.symm.symm =   { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ };α: Sort uβ: Sort vγ: Sort wtoFun✝: α → βinvFun✝: β → αleft_inv✝: LeftInverse invFun✝ toFun✝right_inv✝: Function.RightInverse invFun✝ toFun✝mk{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.symm.symm =   { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } α: Sort uβ: Sort vγ: Sort we: α ≃ βe.symm.symm = erflGoals accomplished! 🐙
#align equiv.symm_symm Equiv.symm_symm: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.symm.symm = eEquiv.symm_symm

@[simp] theorem trans_refl: ∀ (e : α ≃ β), e.trans (Equiv.refl β) = etrans_refl (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : e: α ≃ βe.trans: {α : Sort ?u.36427} → {β : Sort ?u.36426} → {γ : Sort ?u.36425} → α ≃ β → β ≃ γ → α ≃ γtrans (Equiv.refl: (α : Sort ?u.36438) → α ≃ αEquiv.refl β: Sort vβ) = e: α ≃ βe := byGoals accomplished! 🐙 α: Sort uβ: Sort vγ: Sort we: α ≃ βe.trans (Equiv.refl β) = ecases e: α ≃ βeα: Sort uβ: Sort vγ: Sort wtoFun✝: α → βinvFun✝: β → αleft_inv✝: LeftInverse invFun✝ toFun✝right_inv✝: Function.RightInverse invFun✝ toFun✝mk{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (Equiv.refl β) =   { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ };α: Sort uβ: Sort vγ: Sort wtoFun✝: α → βinvFun✝: β → αleft_inv✝: LeftInverse invFun✝ toFun✝right_inv✝: Function.RightInverse invFun✝ toFun✝mk{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.trans (Equiv.refl β) =   { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } α: Sort uβ: Sort vγ: Sort we: α ≃ βe.trans (Equiv.refl β) = erflGoals accomplished! 🐙
#align equiv.trans_refl Equiv.trans_refl: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.trans (Equiv.refl β) = eEquiv.trans_refl

@[simp] theorem refl_symm: ∀ {α : Sort u}, (Equiv.refl α).symm = Equiv.refl αrefl_symm : (Equiv.refl: (α : Sort ?u.36553) → α ≃ αEquiv.refl α: Sort uα).symm: {α : Sort ?u.36555} → {β : Sort ?u.36554} → α ≃ β → β ≃ αsymm = Equiv.refl: (α : Sort ?u.36563) → α ≃ αEquiv.refl α: Sort uα := rfl: ∀ {α : Sort ?u.36566} {a : α}, a = arfl
#align equiv.refl_symm Equiv.refl_symm: ∀ {α : Sort u}, (Equiv.refl α).symm = Equiv.refl αEquiv.refl_symm

@[simp] theorem refl_trans: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), (Equiv.refl α).trans e = erefl_trans (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : (Equiv.refl: (α : Sort ?u.36606) → α ≃ αEquiv.refl α: Sort uα).trans: {α : Sort ?u.36609} → {β : Sort ?u.36608} → {γ : Sort ?u.36607} → α ≃ β → β ≃ γ → α ≃ γtrans e: α ≃ βe = e: α ≃ βe := byGoals accomplished! 🐙 α: Sort uβ: Sort vγ: Sort we: α ≃ β(Equiv.refl α).trans e = ecases e: α ≃ βeα: Sort uβ: Sort vγ: Sort wtoFun✝: α → βinvFun✝: β → αleft_inv✝: LeftInverse invFun✝ toFun✝right_inv✝: Function.RightInverse invFun✝ toFun✝mk(Equiv.refl α).trans { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } =   { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ };α: Sort uβ: Sort vγ: Sort wtoFun✝: α → βinvFun✝: β → αleft_inv✝: LeftInverse invFun✝ toFun✝right_inv✝: Function.RightInverse invFun✝ toFun✝mk(Equiv.refl α).trans { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } =   { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } α: Sort uβ: Sort vγ: Sort we: α ≃ β(Equiv.refl α).trans e = erflGoals accomplished! 🐙
#align equiv.refl_trans Equiv.refl_trans: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), (Equiv.refl α).trans e = eEquiv.refl_trans

@[simp] theorem symm_trans_self: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.symm.trans e = Equiv.refl βsymm_trans_self (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : e: α ≃ βe.symm: {α : Sort ?u.36739} → {β : Sort ?u.36738} → α ≃ β → β ≃ αsymm.trans: {α : Sort ?u.36746} → {β : Sort ?u.36745} → {γ : Sort ?u.36744} → α ≃ β → β ≃ γ → α ≃ γtrans e: α ≃ βe = Equiv.refl: (α : Sort ?u.36759) → α ≃ αEquiv.refl β: Sort vβ := ext: ∀ {α : Sort ?u.36766} {β : Sort ?u.36765} {f g : α ≃ β}, (∀ (x : α), ↑f x = ↑g x) → f = gext <| byGoals accomplished! 🐙 α: Sort uβ: Sort vγ: Sort we: α ≃ β∀ (x : β), ↑(e.symm.trans e) x = ↑(Equiv.refl β) xsimpGoals accomplished! 🐙
#align equiv.symm_trans_self Equiv.symm_trans_self: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.symm.trans e = Equiv.refl βEquiv.symm_trans_self

@[simp] theorem self_trans_symm: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.trans e.symm = Equiv.refl αself_trans_symm (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) : e: α ≃ βe.trans: {α : Sort ?u.37170} → {β : Sort ?u.37169} → {γ : Sort ?u.37168} → α ≃ β → β ≃ γ → α ≃ γtrans e: α ≃ βe.symm: {α : Sort ?u.37182} → {β : Sort ?u.37181} → α ≃ β → β ≃ αsymm = Equiv.refl: (α : Sort ?u.37192) → α ≃ αEquiv.refl α: Sort uα := ext: ∀ {α : Sort ?u.37199} {β : Sort ?u.37198} {f g : α ≃ β}, (∀ (x : α), ↑f x = ↑g x) → f = gext <| byGoals accomplished! 🐙 α: Sort uβ: Sort vγ: Sort we: α ≃ β∀ (x : α), ↑(e.trans e.symm) x = ↑(Equiv.refl α) xsimpGoals accomplished! 🐙
#align equiv.self_trans_symm Equiv.self_trans_symm: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.trans e.symm = Equiv.refl αEquiv.self_trans_symm

theorem trans_assoc: ∀ {δ : Sort u_1} (ab : α ≃ β) (bc : β ≃ γ) (cd : γ ≃ δ), (ab.trans bc).trans cd = ab.trans (bc.trans cd)trans_assoc {δ: ?m.37589δ} (ab: α ≃ βab : α: Sort uα ≃ β: Sort vβ) (bc: β ≃ γbc : β: Sort vβ ≃ γ: Sort wγ) (cd: γ ≃ δcd : γ: Sort wγ ≃ δ: ?m.37589δ) :
(ab: α ≃ βab.trans: {α : Sort ?u.37607} → {β : Sort ?u.37606} → {γ : Sort ?u.37605} → α ≃ β → β ≃ γ → α ≃ γtrans bc: β ≃ γbc).trans: {α : Sort ?u.37624} → {β : Sort ?u.37623} → {γ : Sort ?u.37622} → α ≃ β → β ≃ γ → α ≃ γtrans cd: γ ≃ δcd = ab: α ≃ βab.trans: {α : Sort ?u.37641} → {β : Sort ?u.37640} → {γ : Sort ?u.37639} → α ≃ β → β ≃ γ → α ≃ γtrans (bc: β ≃ γbc.trans: {α : Sort ?u.37652} → {β : Sort ?u.37651} → {γ : Sort ?u.37650} → α ≃ β → β ≃ γ → α ≃ γtrans cd: γ ≃ δcd) := Equiv.ext: ∀ {α : Sort ?u.37676} {β : Sort ?u.37675} {f g : α ≃ β}, (∀ (x : α), ↑f x = ↑g x) → f = gEquiv.ext fun _: ?m.37687_ => rfl: ∀ {α : Sort ?u.37689} {a : α}, a = arfl
#align equiv.trans_assoc 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)Equiv.trans_assoc

theorem leftInverse_symm: ∀ (f : α ≃ β), LeftInverse ↑f.symm ↑fleftInverse_symm (f: α ≃ βf : Equiv: Sort ?u.37737 → Sort ?u.37736 → Sort (max(max1?u.37737)?u.37736)Equiv α: Sort uα β: Sort vβ) : LeftInverse: {α : Sort ?u.37741} → {β : Sort ?u.37740} → (β → α) → (α → β) → PropLeftInverse f: α ≃ βf.symm: {α : Sort ?u.37745} → {β : Sort ?u.37744} → α ≃ β → β ≃ αsymm f: α ≃ βf := f: α ≃ βf.left_inv: ∀ {α : Sort ?u.37886} {β : Sort ?u.37885} (self : α ≃ β), LeftInverse self.invFun self.toFunleft_inv
#align equiv.left_inverse_symm Equiv.leftInverse_symm: ∀ {α : Sort u} {β : Sort v} (f : α ≃ β), LeftInverse ↑f.symm ↑fEquiv.leftInverse_symm

theorem rightInverse_symm: ∀ {α : Sort u} {β : Sort v} (f : α ≃ β), Function.RightInverse ↑f.symm ↑frightInverse_symm (f: α ≃ βf : Equiv: Sort ?u.37907 → Sort ?u.37906 → Sort (max(max1?u.37907)?u.37906)Equiv α: Sort uα β: Sort vβ) : Function.RightInverse: {α : Sort ?u.37911} → {β : Sort ?u.37910} → (β → α) → (α → β) → PropFunction.RightInverse f: α ≃ βf.symm: {α : Sort ?u.37915} → {β : Sort ?u.37914} → α ≃ β → β ≃ αsymm f: α ≃ βf := f: α ≃ βf.right_inv: ∀ {α : Sort ?u.38056} {β : Sort ?u.38055} (self : α ≃ β), Function.RightInverse self.invFun self.toFunright_inv
#align equiv.right_inverse_symm Equiv.rightInverse_symm: ∀ {α : Sort u} {β : Sort v} (f : α ≃ β), Function.RightInverse ↑f.symm ↑fEquiv.rightInverse_symm

theorem injective_comp: ∀ (e : α ≃ β) (f : β → γ), Injective (f ∘ ↑e) ↔ Injective finjective_comp (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) (f: β → γf : β: Sort vβ → γ: Sort wγ) : Injective: {α : Sort ?u.38085} → {β : Sort ?u.38084} → (α → β) → PropInjective (f: β → γf ∘ e: α ≃ βe) ↔ Injective: {α : Sort ?u.38171} → {β : Sort ?u.38170} → (α → β) → PropInjective f: β → γf :=
EquivLike.injective_comp: ∀ {E : Sort ?u.38183} {α : Sort ?u.38180} {β : Sort ?u.38182} {γ : Sort ?u.38181} [iE : EquivLike E α β] (e : E)
(f : β → γ), Injective (f ∘ ↑e) ↔ Injective fEquivLike.injective_comp e: α ≃ βe f: β → γf
#align equiv.injective_comp Equiv.injective_comp: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ), Injective (f ∘ ↑e) ↔ Injective fEquiv.injective_comp

theorem comp_injective: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ), Injective (↑e ∘ f) ↔ Injective fcomp_injective (f: α → βf : α: Sort uα → β: Sort vβ) (e: β ≃ γe : β: Sort vβ ≃ γ: Sort wγ) : Injective: {α : Sort ?u.38243} → {β : Sort ?u.38242} → (α → β) → PropInjective (e: β ≃ γe ∘ f: α → βf) ↔ Injective: {α : Sort ?u.38329} → {β : Sort ?u.38328} → (α → β) → PropInjective f: α → βf :=
EquivLike.comp_injective: ∀ {F : Sort ?u.38341} {α : Sort ?u.38338} {β : Sort ?u.38340} {γ : Sort ?u.38339} [iF : EquivLike F β γ] (f : α → β)
(e : F), Injective (↑e ∘ f) ↔ Injective fEquivLike.comp_injective f: α → βf e: β ≃ γe
#align equiv.comp_injective Equiv.comp_injective: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ), Injective (↑e ∘ f) ↔ Injective fEquiv.comp_injective

theorem surjective_comp: ∀ (e : α ≃ β) (f : β → γ), Surjective (f ∘ ↑e) ↔ Surjective fsurjective_comp (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) (f: β → γf : β: Sort vβ → γ: Sort wγ) : Surjective: {α : Sort ?u.38401} → {β : Sort ?u.38400} → (α → β) → PropSurjective (f: β → γf ∘ e: α ≃ βe) ↔ Surjective: {α : Sort ?u.38487} → {β : Sort ?u.38486} → (α → β) → PropSurjective f: β → γf :=
EquivLike.surjective_comp: ∀ {E : Sort ?u.38499} {α : Sort ?u.38496} {β : Sort ?u.38498} {γ : Sort ?u.38497} [iE : EquivLike E α β] (e : E)
(f : β → γ), Surjective (f ∘ ↑e) ↔ Surjective fEquivLike.surjective_comp e: α ≃ βe f: β → γf
#align equiv.surjective_comp Equiv.surjective_comp: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ), Surjective (f ∘ ↑e) ↔ Surjective fEquiv.surjective_comp

theorem comp_surjective: ∀ (f : α → β) (e : β ≃ γ), Surjective (↑e ∘ f) ↔ Surjective fcomp_surjective (f: α → βf : α: Sort uα → β: Sort vβ) (e: β ≃ γe : β: Sort vβ ≃ γ: Sort wγ) : Surjective: {α : Sort ?u.38559} → {β : Sort ?u.38558} → (α → β) → PropSurjective (e: β ≃ γe ∘ f: α → βf) ↔ Surjective: {α : Sort ?u.38645} → {β : Sort ?u.38644} → (α → β) → PropSurjective f: α → βf :=
EquivLike.comp_surjective: ∀ {F : Sort ?u.38657} {α : Sort ?u.38654} {β : Sort ?u.38656} {γ : Sort ?u.38655} [iF : EquivLike F β γ] (f : α → β)
(e : F), Surjective (↑e ∘ f) ↔ Surjective fEquivLike.comp_surjective f: α → βf e: β ≃ γe
#align equiv.comp_surjective Equiv.comp_surjective: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ), Surjective (↑e ∘ f) ↔ Surjective fEquiv.comp_surjective

theorem bijective_comp: ∀ (e : α ≃ β) (f : β → γ), Bijective (f ∘ ↑e) ↔ Bijective fbijective_comp (e: α ≃ βe : α: Sort uα ≃ β: Sort vβ) (f: β → γf : β: Sort vβ → γ: Sort wγ) : Bijective: {α : Sort ?u.38717} → {β : Sort ?u.38716} → (α → β) → PropBijective (f: β → γf ∘ e: α ≃ βe) ↔ Bijective: {α : Sort ?u.38803} → {β : Sort ?u.38802} → (α → β) → PropBijective f: β → γf :=
EquivLike.bijective_comp: ∀ {E : Sort ?u.38815} {α : Sort ?u.38812} {β : Sort ?u.38814} {γ : Sort ?u.38813} [iE : EquivLike E α β] (e : E)
(f : β → γ), Bijective (f ∘ ↑e) ↔ Bijective fEquivLike.bijective_comp e: α ≃ βe f: β → γf
#align equiv.bijective_comp Equiv.bijective_comp: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ), Bijective (f ∘ ↑e) ↔ Bijective fEquiv.bijective_comp

theorem comp_bijective: ∀ (f : α → β) (e : β ≃ γ), Bijective (↑e ∘ f) ↔ Bijective fcomp_bijective (f: α → βf : α: Sort uα → β: Sort vβ) (e: β ≃ γe : β: Sort vβ ≃ γ: Sort wγ) : Bijective: {α : Sort ?u.38875} → {β : Sort ?u.38874} → (α → β) → PropBijective (e: β ≃ γe ∘ f: α → βf) ↔ Bijective: {α : Sort ?u.38961} → {β : Sort ?u.38960} → (α → β) → PropBijective f: α → βf :=
EquivLike.comp_bijective: ∀ {F : Sort ?u.38973} {α : Sort ?u.38970} {β : Sort ?u.38972} {γ : Sort ?u.38971} [iF : EquivLike F β γ] (f : α → β)
(e : F), Bijective (↑e ∘ f) ↔ Bijective fEquivLike.comp_bijective f: α → βf e: β ≃ γe
#align equiv.comp_bijective Equiv.comp_bijective: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ), Bijective (↑e ∘ f) ↔ Bijective fEquiv.comp_bijective

/-- If `α` is equivalent to `β` and `γ` is equivalent to `δ`, then the type of equivalences `α ≃ γ`
is equivalent to the type of equivalences `β ≃ δ`. -/
def equivCongr: {δ : Sort ?u.39038} → α ≃ β → γ ≃ δ → α ≃ γ ≃ (β ≃ δ)equivCongr (ab: α ≃ βab : α: Sort uα ≃ β: Sort vβ) (cd: γ ≃ δcd : γ: Sort wγ ≃ δ: ?m.39031δ) : (α: Sort uα ≃ γ: Sort wγ) ≃ (β: Sort vβ ≃ δ: ?m.39031δ) where
toFun ac: ?m.39059ac := (ab: α ≃ βab.symm: {α : Sort ?u.39062} → {β : Sort ?u.39061} → α ≃ β → β ≃ αsymm.trans: {α : Sort ?u.39069} → {β : Sort ?u.39068} → {γ : Sort ?u.39067} → α ≃ β → β ≃ γ → α ≃ γtrans ac: ?m.39059ac).trans: {α : Sort ?u.39086} → {β : Sort ?u.39085} → {γ : Sort ?u.39084} → α ≃ β → β ≃ γ → α ≃ γtrans cd: γ ≃ δcd
invFun bd: ?m.39104bd := ab: α ≃ βab.trans: {α : Sort ?u.39108} → {β : Sort ?u.39107} → {γ : Sort ?u.39106} → α ≃ β → β ≃ γ → α ≃ γtrans <| bd: ?m.39104bd.trans: {α : Sort ?u.39119} → {β : Sort ?u.39118} → {γ : Sort ?u.39117} → α ≃ β → β ≃ γ → α ≃ γtrans <| cd: γ ≃ δcd.symm: {α : Sort ?u.39129} → {β : Sort ?u.39128} → α ≃ β → β ≃ αsymm
left_inv ac: ?m.39140ac := byGoals accomplished! 🐙 α: Sort uβ: Sort vγ: Sort wδ: Sort ?u.39038ab: α ≃ βcd: γ ≃ δac: α ≃ γ(fun bd => ab.trans (bd.trans cd.symm)) ((fun ac => (ab.symm.trans ac).trans cd) ac) = acext x: ?αxα: Sort uβ: Sort vγ: Sort wδ: Sort ?u.39038ab: α ≃ βcd: γ ≃ δac: α ≃ γx: αH↑((fun bd => ab.trans (bd.trans cd.symm)) ((fun ac => (ab.symm.trans ac).trans cd) ac)) x = ↑ac x;α: Sort uβ: Sort vγ: Sort wδ: Sort ?u.39038ab: α ≃ βcd: γ ≃ δac: α ≃ γx: αH↑((fun bd => ab.trans (bd.trans cd.symm)) ((fun ac => (ab.symm.trans ac).trans cd) ac)) x = ↑ac x α: Sort uβ: Sort vγ: Sort wδ: Sort ?u.39038ab: α ≃ βcd: γ ≃ δac: α ≃ γ(fun bd => ab.trans (bd.trans cd.symm)) ((fun ac => (ab.symm.trans ac).trans cd) ac) = acsimp only [trans_apply: ∀ {α : Sort ?u.39202} {β : Sort ?u.39201} {γ : Sort ?u.39200} (f : α ≃ β) (g : β ≃ γ) (a : α),
↑(f.trans g) a = ↑g (↑f a)trans_apply, comp_apply: ∀ {β : Sort ?u.39231} {δ : Sort ?u.39232} {α : Sort ?u.39233} {f : β → δ} {g : α → β} {x : α}, (f ∘ g) x = f (g x)comp_apply, symm_apply_apply: ∀ {α : Sort ?u.39256} {β : Sort ?u.39255} (e : α ≃ β) (x : α), ↑e.symm (↑e x) = xsymm_apply_apply]Goals accomplished! 🐙
right_inv ac: ?m.39146ac := byGoals accomplished! 🐙 α: Sort uβ: Sort vγ: Sort wδ: Sort ?u.39038ab: α ≃ βcd: γ ≃ δac: β ≃ δ(fun ac => (ab.symm.trans ac).trans cd) ((fun bd => ab.trans (bd.trans cd.symm)) ac) = acext x: ?αxα: Sort uβ: Sort vγ: Sort wδ: Sort ?u.39038ab: α ≃ βcd: γ ≃ δac: β ≃ δx: βH↑((fun ac => (ab.symm.trans ac).trans cd) ((fun bd => ab.trans (bd.trans cd.symm)) ac)) x = ↑ac x;α: Sort uβ: Sort vγ: Sort wδ: Sort ?u.39038ab: α ≃ βcd: γ ≃ δac: β ≃ δx: βH↑((fun ac => (ab.symm.trans ac).trans cd) ((fun bd => ab.trans (bd.trans cd.symm)) ac)) x = ↑ac x α: Sort uβ: Sort vγ: Sort wδ: Sort ?u.39038ab: α ≃ βcd: γ ≃ δac: β ≃ δ(fun ac => (ab.symm.trans ac).trans cd) ((fun bd => ab.trans (bd.trans cd.symm)) ac) = acsimp only [trans_apply: ∀ {α : Sort ?u.39765} {β : Sort ?u.39764} {γ : Sort ?u.39763} (f : α ≃ β) (g : β ≃ γ) (a : α),
↑(f.trans g) a = ↑g (↑f a)trans_apply, comp_apply: ∀ {β : Sort ?u.39779} {δ : Sort ?u.39780} {α : Sort ?u.39781} {f : β → δ} {g : α → β} {x : α}, (f ∘ g) x = f (g x)comp_apply, apply_symm_apply: ∀ {α : Sort ?u.39796} {β : Sort ?u.39795} (e : α ≃ β) (x : β), ↑e (↑e.symm x) = xapply_symm_apply]Goals accomplished! 🐙
#align equiv.equiv_congr Equiv.equivCongr: {α : Sort u} → {β : Sort v} → {γ : Sort w} → {δ : Sort u_1} → α ≃ β → γ ≃ δ → α ≃ γ ≃ (β ≃ δ)Equiv.equivCongr

@[simp] theorem equivCongr_refl: ∀ {α : Sort u_1} {β : Sort u_2}, equivCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ≃ β)equivCongr_refl {α: Sort u_1α β: ?m.40419β} :
(Equiv.refl: (α : Sort ?u.40423) → α ≃ αEquiv.refl α: ?m.40416α).equivCongr: {α : Sort ?u.40427} → {β : Sort ?u.40426} → {γ : Sort ?u.40425} → {δ : Sort ?u.40424} → α ≃ β → γ ≃ δ → α ≃ γ ≃ (β ≃ δ)equivCongr (Equiv.refl: (α : Sort ?u.40440) → α ≃ αEquiv.refl β: ?m.40419β) = Equiv.refl: (α : Sort ?u.40445) → α ≃ αEquiv.refl (α: ?m.40416α ≃ β: ?m.40419β) := byGoals accomplished! 🐙 α✝: Sort uβ✝: Sort vγ: Sort wα: Sort u_1β: Sort u_2equivCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ≃ β)extα✝: Sort uβ✝: Sort vγ: Sort wα: Sort u_1β: Sort u_2x✝¹: α ≃ βx✝: αH.H↑(↑(equivCongr (Equiv.refl α) (Equiv.refl β)) x✝¹) x✝ = ↑(↑(Equiv.refl (α ≃ β)) x✝¹) x✝;α✝: Sort uβ✝: Sort vγ: Sort wα: Sort u_1β: Sort u_2x✝¹: α ≃ βx✝: αH.H↑(↑(equivCongr (Equiv.refl α) (Equiv.refl β)) x✝¹) x✝ = ↑(↑(Equiv.refl (α ≃ β)) x✝¹) x✝ α✝: Sort uβ✝: Sort vγ: Sort wα: Sort u_1β: Sort u_2equivCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ≃ β)rflGoals accomplished! 🐙
#align equiv.equiv_congr_refl Equiv.equivCongr_refl: ∀ {α : Sort u_1} {β : Sort u_2}, equivCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ≃ β)Equiv.equivCongr_refl

@[simp] theorem equivCongr_symm: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (cd : γ ≃ δ),
(equivCongr ab cd).symm = equivCongr ab.symm cd.symmequivCongr_symm {δ: Sort u_1δ} (ab: α ≃ βab : α: Sort uα ≃ β: Sort vβ) (cd: γ ≃ δcd : γ: Sort wγ ≃ δ: ?m.40551δ) :
(ab: α ≃ βab.equivCongr: {α : Sort ?u.40566} → {β : Sort ?u.40565} → {γ : Sort ?u.40564} → {δ : Sort ?u.40563} → α ≃ β → γ ≃ δ → α ≃ γ ≃ (β ≃ δ)equivCongr cd: γ ≃ δcd).symm: {α : Sort ?u.40584} → {β : Sort ?u.40583} → α ≃ β → β ≃ αsymm = ab: α ≃ βab.symm: {α : Sort ?u.40593} → {β : Sort ?u.40592} → α ≃ β → β ≃ αsymm.equivCongr: {α : Sort ?u.40599} → {β : Sort ?u.40598} → {γ : Sort ?u.40597} → {δ : Sort ?u.40596} → α ≃ β → γ ≃ δ → α ≃ γ ≃ (β ≃ δ)equivCongr cd: γ ≃ δcd.symm: {α : Sort ?u.40613} → {β : Sort ?u.40612} → α ≃ β → β ≃ αsymm := byGoals accomplished! 🐙 α: Sort uβ: Sort vγ: Sort wδ: Sort u_1ab: α ≃ βcd: γ ≃ δ(equivCongr ab cd).symm = equivCongr ab.symm cd.symmextα: Sort uβ: Sort vγ: Sort wδ: Sort u_1ab: α ≃ βcd: γ ≃ δx✝¹: β ≃ δx✝: αH.H↑(↑(equivCongr ab cd).symm x✝¹) x✝ = ↑(↑(equivCongr ab.symm cd.symm) x✝¹) x✝;α: Sort uβ: Sort vγ: Sort wδ: Sort u_1ab: α ≃ βcd: γ ≃ δx✝¹: β ≃ δx✝: αH.H↑(↑(equivCongr ab cd).symm x✝¹) x✝ = ↑(↑(equivCongr ab.symm cd.symm) x✝¹) x✝ α: Sort uβ: Sort vγ: Sort wδ: Sort u_1ab: α ≃ βcd: γ ≃ δ(equivCongr ab cd).symm = equivCongr ab.symm cd.symmrflGoals accomplished! 🐙
#align equiv.equiv_congr_symm Equiv.equivCongr_symm: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} (ab : α ≃ β) (cd : γ ≃ δ),
(equivCongr ab cd).symm = equivCongr ab.symm cd.symmEquiv.equivCongr_symm

@[simp] theorem equivCongr_trans: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} {ε : Sort u_2} {ζ : Sort u_3} (ab : α ≃ β) (de : δ ≃ ε)
(bc : β ≃ γ) (ef : ε ≃ ζ), (equivCongr ab de).trans (equivCongr bc ef) = equivCongr (ab.trans bc) (de.trans ef)equivCongr_trans {δ: Sort u_1δ ε: ?m.40765ε ζ: ?m.40768ζ} (ab: α ≃ βab : α: Sort uα ≃ β: Sort vβ) (de: δ ≃ εde : δ: ?m.40762δ ≃ ε: ?m.40765ε) (bc: β ≃ γbc : β: Sort vβ ≃ γ: Sort wγ) (ef: ε ≃ ζef : ε: ?m.40765ε ≃ ζ: ?m.40768ζ) :
(ab: α ≃ βab.equivCongr: {α : Sort ?u.40791} → {β : Sort ?u.40790} → {γ : Sort ?u.40789} → {δ : Sort ?u.40788} → α ≃ β → γ ≃ δ → α ≃ γ ≃ (β ≃ δ)equivCongr de: δ ≃ εde).trans: {α : Sort ?u.40810} → {β : Sort ?u.40809} → {γ : Sort ?u.40808} → α ≃ β → β ≃ γ → α ≃ γtrans (bc: β ≃ γbc.equivCongr: {α : Sort ?u.40824} → {β : Sort ?u.40823} → {γ : Sort ?u.40822} → {δ : Sort ?u.40821} → α ≃ β → γ ≃ δ → α ≃ γ ≃ (β ≃ δ)equivCongr ef: ε ≃ ζef) = (ab: α ≃ βab.trans: {α : Sort ?u.40851} → {β : Sort ?u.40850} → {γ : Sort ?u.40849} → α ≃ β → β ≃ γ → α ≃ γtrans bc: β ≃ γbc).equivCongr: {α : Sort ?u.40865} → {β : Sort ?u.40864} → {γ : Sort ?u.40863} → {δ : Sort ?u.40862} → α ≃ β → γ ≃ δ → α ≃ γ ≃ (β ≃ δ)equivCongr (de: δ ≃ εde.trans: {α : Sort ?u.40880} → {β : Sort ?u.40879} → {γ : Sort ?u.40878} → α ≃ β → β ≃ γ → α ≃ γtrans ef: ε ≃ ζef) := byGoals accomplished! 🐙
α: Sort uβ: Sort vγ: Sort wδ: Sort u_1ε: Sort u_2ζ: Sort u_3ab: α ≃ βde: δ ≃ εbc: β ≃ γef: ε ≃ ζ(equivCongr ab de).trans (equivCongr bc ef) = equivCongr (ab.trans bc) (de.trans ef)extα: Sort uβ: Sort vγ: Sort wδ: Sort u_1ε: Sort u_2ζ: Sort u_3ab: α ≃ βde: δ ≃ εbc: β ≃ γef: ε ≃ ζx✝¹: α ≃ δx✝: γH.H↑(↑((equivCongr ab de).trans (equivCongr bc ef)) x✝¹) x✝ = ↑(↑(equivCongr (ab.trans bc) (de.trans ef)) x✝¹) x✝;α: Sort uβ: Sort vγ: Sort wδ: Sort u_1ε: Sort u_2ζ: Sort u_3ab: α ≃ βde: δ ≃ εbc: β ≃ γef: ε ≃ ζx✝¹: α ≃ δx✝: γH.H↑(↑((equivCongr ab de).trans (equivCongr bc ef)) x✝¹) x✝ = ↑(↑(equivCongr (ab.trans bc) (de.trans ef)) x✝¹) x✝ α: Sort uβ: Sort vγ: Sort wδ: Sort u_1ε: Sort u_2ζ: Sort u_3ab: α ≃ βde: δ ≃ εbc: β ≃ γef: ε ≃ ζ(equivCongr ab de).trans (equivCongr bc ef) = equivCongr (ab.trans bc) (de.trans ef)rflGoals accomplished! 🐙
#align equiv.equiv_congr_trans Equiv.equivCongr_trans: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort u_1} {ε : Sort u_2} {ζ : Sort u_3} (ab : α ≃ β) (de : δ ≃ ε)
(bc : β ≃ γ) (ef : ε ≃ ζ), (equivCongr ab de).trans (equivCongr bc ef) = equivCongr (ab.trans bc) (de.trans ef)Equiv.equivCongr_trans

@[simp] theorem equivCongr_refl_left: ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (bg : β ≃ γ) (e : α ≃ β), ↑(equivCongr (Equiv.refl α) bg) e = e.trans bgequivCongr_refl_left {α: Sort u_1α β: ?m.41073β γ: ?m.41076γ} (bg: β ≃ γbg : β: ?m.41073β ≃ γ: ?m.41076γ) (e: α ≃ βe : α: ?m.41070α ≃ β: ?m.41073β) :
(Equiv.refl: (α : Sort ?u.41088) → α ≃ αEquiv.refl α: ?m.41070α).equivCongr: {α : Sort ?u.41092} → {β : Sort ?u.41091} → {γ : Sort ?u.41090} → {δ : Sort ?u.41089} → α ≃ β → γ ≃ δ → α ≃ γ ≃ (β ≃ δ)equivCongr bg: β ≃ γbg e: α ≃ βe = e: α ≃ βe.trans: {α : Sort ?u.41182} → {β : Sort ?u.41181} → {γ : Sort ?u.41180} → α ≃ β → β ≃ γ → α ≃ γtrans bg: β ≃ γbg := rfl: ∀ {α : Sort ?u.41203} {a : α}, a = arfl
#align equiv.equiv_congr_refl_left Equiv.equivCongr_refl_left: ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (bg : β ≃ γ) (e : α ≃ β), ↑(equivCongr (Equiv.refl α) bg) e = e.trans bg```