/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Mario Carneiro

! 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 u
Sort
Sort u: Type u
 u} {
β: Sort v
β : 
Sort v: Type v
Sort
Sort v: Type v
 v} {
γ: Sort w
γ : 
Sort w: Type w
Sort
Sort 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.14
Sort
Sort _: Type ?u.14
 _) (
β: Sort ?u.17
β : 
Sort _: Type ?u.17
Sort
Sort _: 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.toFun
left_inv : 
LeftInverse: {α : Sort ?u.31} → {β : Sort ?u.30} → (β → α) → (α → β) → Prop
LeftInverse 
invFun: β → α
invFun 
toFun: α → β
toFun
  
right_inv: ∀ {α : Sort u_1} {β : Sort u_2} (self : Equiv α β), Function.RightInverse self.invFun self.toFun
right_inv : 
RightInverse: {α : Sort ?u.43} → {β : Sort ?u.42} → (β → α) → (α → β) → Prop
RightInverse 
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.8760
F} [
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.8760
F 
α: Sort u
α 
β: Sort v
β] (
f: F
f :
F: ?m.8760
F) : 
α: Sort u
α ≃ 
β: Sort v
β where
  toFun := 
f: F
f
  invFun := 
EquivLike.inv: {E : Sort ?u.8869} →
  {α : outParam (Sort ?u.8868)} → {β : outParam (Sort ?u.8867)} → [self : EquivLike E α β] → E → β → α
EquivLike.inv 
f: F
f
  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: F
f
  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: F
f

/-- 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.9203
F} [
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.9198
F 
α: Sort u
α 
β: Sort v
β] : 
CoeTC: Sort ?u.9207 → Sort ?u.9206 → Sort (max(max1?u.9207)?u.9206)
CoeTC 
F: ?m.9198
F (
α: 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.9318
Sort
Sort _: 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.toFun
left_inv
  right_inv := 
right_inv: ∀ {α : Sort ?u.9390} {β : Sort ?u.9389} (self : α ≃ β), Function.RightInverse self.invFun self.toFun
right_inv
  coe_injective' 
e₁: ?m.9404
e₁ 
e₂: ?m.9407
e₂ 
h₁: ?m.9410
h₁ 
h₂: ?m.9413
h₂ := by
Goals accomplished! 🐙 
α: Sort u

β: Sort v

γ: Sort w

e₁, e₂: α ≃ β

h₁: e₁.toFun = e₂.toFun

h₂: e₁.invFun = e₂.invFun

e₁ = e₂cases 
e₁: α ≃ β
e₁
α: Sort u

β: Sort v

γ: Sort w

e₂: α ≃ β

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₂.toFun

h₂: { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun = e₂.invFun

mk
{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = e₂;
α: Sort u

β: Sort v

γ: Sort w

e₂: α ≃ β

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₂.toFun

h₂: { toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }.invFun = e₂.invFun

mk
{ toFun := toFun✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ } = e₂ 
α: Sort u

β: Sort v

γ: Sort w

e₁, e₂: α ≃ β

h₁: e₁.toFun = e₂.toFun

h₂: e₁.invFun = e₂.invFun

e₁ = e₂cases 
e₂: α ≃ β
e₂
α: Sort u

β: Sort v

γ: Sort w

toFun✝¹: α → β

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✝ }.toFun

h₂: { 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✝ }.invFun

mk.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 w

toFun✝¹: α → β

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✝ }.toFun

h₂: { 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✝ }.invFun

mk.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 w

e₁, e₂: α ≃ β

h₁: e₁.toFun = e₂.toFun

h₂: e₁.invFun = e₂.invFun

e₁ = e₂congr
Goals 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 } = f
coe_fn_mk (
f: α → β
f : 
α: Sort u
α → 
β: Sort v
β) (
g: β → α
g 
l: LeftInverse g f
l 
r: ?m.10284
r) : (
Equiv.mk: {α : Sort ?u.10292} →
  {β : Sort ?u.10291} →
    (toFun : α → β) → (invFun : β → α) → LeftInverse invFun toFun → Function.RightInverse invFun toFun → α ≃ β
Equiv.mk 
f: α → β
f 
g: ?m.10278
g 
l: ?m.10281
l 
r: ?m.10284
r : 
α: Sort u
α → 
β: Sort v
β) = 
f: α → β
f :=
rfl: ∀ {α : Sort ?u.10391} {a : α}, a = a
rfl
#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 } = f
Equiv.coe_fn_mk

/-- The map `(r ≃ s) → (r → s)` is injective. -/
theorem 
coe_fn_injective: ∀ {α : Sort u} {β : Sort v}, Injective fun e => ↑e
coe_fn_injective : @
Function.Injective: {α : Sort ?u.10447} → {β : Sort ?u.10446} → (α → β) → Prop
Function.Injective (
α: Sort u
α ≃ 
β: Sort v
β) (
α: Sort u
α → 
β: Sort v
β) (fun 
e: ?m.10454
e => 
e: ?m.10454
e) :=
  
FunLike.coe_injective': ∀ {F : Sort ?u.10529} {α : outParam (Sort ?u.10528)} {β : outParam (α → Sort ?u.10527)} [self : FunLike F α β],
  Injective FunLike.coe
FunLike.coe_injective'
#align equiv.coe_fn_injective 
Equiv.coe_fn_injective: ∀ {α : Sort u} {β : Sort v}, Injective fun e => ↑e
Equiv.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 = g
FunLike.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 = g
ext {
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 x
H : ∀ 
x: ?m.10961
x, 
f: α ≃ β
f 
x: ?m.10961
x = 
g: α ≃ β
g 
x: ?m.10961
x) : 
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 = g
FunLike.ext 
f: α ≃ β
f 
g: α ≃ β
g 
H: ∀ (x : α), ↑f x = ↑g x
H
#align equiv.ext 
Equiv.ext: ∀ {α : Sort u} {β : Sort v} {f g : α ≃ β}, (∀ (x : α), ↑f x = ↑g x) → f = g
Equiv.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 y
FunLike.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 x
congr_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 = g
h : 
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 x
FunLike.congr_fun 
h: f = g
h 
x: α
x
#align equiv.congr_fun 
Equiv.congr_fun: ∀ {α : Sort u} {β : Sort v} {f g : α ≃ β}, f = g → ∀ (x : α), ↑f x = ↑g x
Equiv.congr_fun

theorem 
ext_iff: ∀ {f g : α ≃ β}, f = g ↔ ∀ (x : α), ↑f x = ↑g x
ext_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.11537
x, 
f: α ≃ β
f 
x: ?m.11537
x = 
g: α ≃ β
g 
x: ?m.11537
x := 
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 x
FunLike.ext_iff
#align equiv.ext_iff 
Equiv.ext_iff: ∀ {α : Sort u} {β : Sort v} {f g : α ≃ β}, f = g ↔ ∀ (x : α), ↑f x = ↑g x
Equiv.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 = ↑τ x
H : ∀ 
x: ?m.11742
x, 
σ: Perm α
σ 
x: ?m.11742
x = 
τ: Perm α
τ 
x: ?m.11742
x) : 
σ: Perm α
σ = 
τ: Perm α
τ := 
Equiv.ext: ∀ {α : Sort ?u.11870} {β : Sort ?u.11869} {f g : α ≃ β}, (∀ (x : α), ↑f x = ↑g x) → f = g
Equiv.ext 
H: ∀ (x : α), ↑σ x = ↑τ x
H
#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 x
Perm.congr_fun {
f: Perm α
f 
g: Perm α
g : 
Equiv.Perm: Sort ?u.12077 → Sort (max1?u.12077)
Equiv.Perm 
α: Sort u
α} (
h: f = g
h : 
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 x
Equiv.congr_fun 
h: f = g
h 
x: α
x
#align equiv.perm.congr_fun 
Equiv.Perm.congr_fun: ∀ {α : Sort u} {f g : Perm α}, f = g → ∀ (x : α), ↑f x = ↑g x
Equiv.Perm.congr_fun

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

/-- Any type is equivalent to itself. -/
@[refl] protected def 
refl: (α : Sort ?u.12396) → α ≃ α
refl (
α: Sort ?u.12396
α : 
Sort _: Type ?u.12396
Sort
Sort _: 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 = a
rfl, fun 
_: ?m.12437
_ => 
rfl: ∀ {α : Sort ?u.12439} {a : α}, a = a
rfl⟩
#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.toFun
right_inv, 
e: α ≃ β
e.
left_inv: ∀ {α : Sort ?u.12622} {β : Sort ?u.12621} (self : α ≃ β), LeftInverse self.invFun self.toFun
left_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 ↑e
left_inv' (
e: α ≃ β
e : 
α: Sort u
α ≃ 
β: Sort v
β) : 
Function.LeftInverse: {α : Sort ?u.20251} → {β : Sort ?u.20250} → (β → α) → (α → β) → Prop
Function.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.toFun
left_inv
theorem 
right_inv': ∀ (e : α ≃ β), Function.RightInverse ↑e.symm ↑e
right_inv' (
e: α ≃ β
e : 
α: Sort u
α ≃ 
β: Sort v
β) : 
Function.RightInverse: {α : Sort ?u.20421} → {β : Sort ?u.20420} → (β → α) → (α → β) → Prop
Function.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.toFun
right_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.toFun
left_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.toFun
left_inv, 
e₂: β ≃ γ
e₂.
right_inv: ∀ {α : Sort ?u.20978} {β : Sort ?u.20977} (self : α ≃ β), Function.RightInverse self.invFun self.toFun
right_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.toFun
right_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 Equiv
instance : 
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 = ↑e
toFun_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 = a
rfl
#align equiv.to_fun_as_coe 
Equiv.toFun_as_coe: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.toFun = ↑e
Equiv.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 x
toFun_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 = a
rfl

@[simp] theorem 
invFun_as_coe: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.invFun = ↑e.symm
invFun_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 = a
rfl
#align equiv.inv_fun_as_coe 
Equiv.invFun_as_coe: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.invFun = ↑e.symm
Equiv.invFun_as_coe

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

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

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

protected theorem 
subsingleton: α ≃ β → ∀ [inst : Subsingleton β], Subsingleton α
subsingleton (
e: α ≃ β
e : 
α: Sort u
α ≃ 
β: Sort v
β) [
Subsingleton: Sort ?u.30014 → Prop
Subsingleton 
β: Sort v
β] : 
Subsingleton: Sort ?u.30017 → Prop
Subsingleton 
α: Sort u
α :=
  
e: α ≃ β
e.
injective: ∀ {α : Sort ?u.30022} {β : Sort ?u.30021} (e : α ≃ β), Injective ↑e
injective.
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 → Prop
Subsingleton 
α: Sort u
α] : 
Subsingleton: Sort ?u.30068 → Prop
Subsingleton 
β: Sort v
β :=
  
e: α ≃ β
e.
symm: {α : Sort ?u.30073} → {β : Sort ?u.30072} → α ≃ β → β ≃ α
symm.
injective: ∀ {α : Sort ?u.30079} {β : Sort ?u.30078} (e : α ≃ β), Injective ↑e
injective.
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 → Prop
Subsingleton 
α: Sort u
α ↔ 
Subsingleton: Sort ?u.30123 → Prop
Subsingleton 
β: 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 → Prop
Subsingleton 
β: Sort v
β] : 
Subsingleton: Sort ?u.30193 → Prop
Subsingleton (
α: 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 = g
Equiv.ext fun 
_: ?m.30221
_ => 
Subsingleton.elim: ∀ {α : Sort ?u.30223} [h : Subsingleton α] (a b : α), a = b
Subsingleton.elim 
_: ?m.30224
_ 
_: ?m.30224
_⟩

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

instance 
permUnique: [inst : Subsingleton α] → Unique (Perm α)
permUnique [
Subsingleton: Sort ?u.30387 → Prop
Subsingleton 
α: 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 → Prop
Subsingleton 
α: 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 = b
Subsingleton.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 ↑e
injective.
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 → Prop
Nonempty 
α: Sort u
α ↔ 
Nonempty: Sort ?u.30747 → Prop
Nonempty 
β: 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 → Prop
Nonempty 
β: Sort v
β] : 
Nonempty: Sort ?u.30917 → Prop
Nonempty 
α: Sort u
α := 
e: α ≃ β
e.
nonempty_congr: ∀ {α : Sort ?u.30922} {β : Sort ?u.30921}, α ≃ β → (Nonempty α ↔ Nonempty β)
nonempty_congr.
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr ‹_›
#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 ↑e
surjective.
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.31339
Sort
Sort _: 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 = a
symm, fun 
_: ?m.31413
_ => by
Goals accomplished! 🐙 
α✝: Sort u

β✝: Sort v

γ: Sort w

α, β: Sort ?u.31342

h: α = β

x✝: α

cast (_ : β = α) (cast h x✝) = x✝cases 
h: α = β
h
α✝: Sort u

β: Sort v

γ: Sort w

α: Sort ?u.31342

x✝: α

refl
cast (_ : α = α) (cast (_ : α = α) x✝) = x✝;
α✝: Sort u

β: Sort v

γ: Sort w

α: Sort ?u.31342

x✝: α

refl
cast (_ : α = α) (cast (_ : α = α) x✝) = x✝ 
α✝: Sort u

β✝: Sort v

γ: Sort w

α, β: Sort ?u.31342

h: α = β

x✝: α

cast (_ : β = α) (cast h x✝) = x✝rfl
Goals accomplished! 🐙, fun 
_: ?m.31419
_ => by
Goals accomplished! 🐙 
α✝: Sort u

β✝: Sort v

γ: Sort w

α, β: Sort ?u.31342

h: α = β

x✝: β

cast h (cast (_ : β = α) x✝) = x✝cases 
h: α = β
h
α✝: Sort u

β: Sort v

γ: Sort w

α: Sort ?u.31342

x✝: α

refl
cast (_ : α = α) (cast (_ : α = α) x✝) = x✝;
α✝: Sort u

β: Sort v

γ: Sort w

α: Sort ?u.31342

x✝: α

refl
cast (_ : α = α) (cast (_ : α = α) x✝) = x✝ 
α✝: Sort u

β✝: Sort v

γ: Sort w

α, β: Sort ?u.31342

h: α = β

x✝: β

cast h (cast (_ : β = α) x✝) = x✝rfl
Goals 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 = g
coe_fn_symm_mk (
f: α → β
f : 
α: Sort u
α → 
β: Sort v
β) (
g: ?m.31697
g 
l: ?m.31700
l 
r: ?m.31703
r) : ((
Equiv.mk: {α : Sort ?u.31711} →
  {β : Sort ?u.31710} →
    (toFun : α → β) → (invFun : β → α) → LeftInverse invFun toFun → Function.RightInverse invFun toFun → α ≃ β
Equiv.mk 
f: α → β
f 
g: ?m.31697
g 
l: ?m.31700
l 
r: ?m.31703
r).
symm: {α : Sort ?u.31732} → {β : Sort ?u.31731} → α ≃ β → β ≃ α
symm : 
β: Sort v
β → 
α: Sort u
α) = 
g: ?m.31697
g := 
rfl: ∀ {α : Sort ?u.31814} {a : α}, a = a
rfl
#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 = g
Equiv.coe_fn_symm_mk

@[simp] theorem 
coe_refl: ∀ {α : Sort u}, ↑(Equiv.refl α) = id
coe_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 = a
rfl
#align equiv.coe_refl 
Equiv.coe_refl: ∀ {α : Sort u}, ↑(Equiv.refl α) = id
Equiv.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 = id
Perm.coe_subsingleton {
α: Type ?u.32011
α : 
Type _: Type (?u.32011+1)
Type _} [
Subsingleton: Sort ?u.32014 → Prop
Subsingleton 
α: 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 := by
Goals accomplished! 🐙
  
α✝: Sort u

β: Sort v

γ: Sort w

α: Type u_1

inst✝: Subsingleton α

e: Perm α

↑e = idrw [
α✝: Sort u

β: Sort v

γ: Sort w

α: Type u_1

inst✝: Subsingleton α

e: Perm α

↑e = id
Perm.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_1

inst✝: Subsingleton α

e: Perm α

↑(Equiv.refl α) = id 
α✝: Sort u

β: Sort v

γ: Sort w

α: Type u_1

inst✝: Subsingleton α

e: Perm α

↑e = id
coe_refl: ∀ {α : Sort ?u.32170}, ↑(Equiv.refl α) = id
coe_refl
α✝: Sort u

β: Sort v

γ: Sort w

α: Type u_1

inst✝: Subsingleton α

e: Perm α

id = id]
Goals accomplished! 🐙
#align equiv.perm.coe_subsingleton 
Equiv.Perm.coe_subsingleton: ∀ {α : Type u_1} [inst : Subsingleton α] (e : Perm α), ↑e = id
Equiv.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 = x
refl_apply (
x: α
x : 
α: Sort u
α) : 
Equiv.refl: (α : Sort ?u.32226) → α ≃ α
Equiv.refl 
α: Sort u
α 
x: α
x = 
x: α
x := 
rfl: ∀ {α : Sort ?u.32291} {a : α}, a = a
rfl
#align equiv.refl_apply 
Equiv.refl_apply: ∀ {α : Sort u} (x : α), ↑(Equiv.refl α) x = x
Equiv.refl_apply

@[simp] theorem 
coe_trans: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ), ↑(f.trans g) = ↑g ∘ ↑f
coe_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 = a
rfl
#align equiv.coe_trans 
Equiv.coe_trans: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α ≃ β) (g : β ≃ γ), ↑(f.trans g) = ↑g ∘ ↑f
Equiv.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 = a
rfl
#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) = x
apply_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.toFun
right_inv 
x: β
x
#align equiv.apply_symm_apply 
Equiv.apply_symm_apply: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (x : β), ↑e (↑e.symm x) = x
Equiv.apply_symm_apply

@[simp] theorem 
symm_apply_apply: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (x : α), ↑e.symm (↑e x) = x
symm_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.toFun
left_inv 
x: α
x
#align equiv.symm_apply_apply 
Equiv.symm_apply_apply: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β) (x : α), ↑e.symm (↑e x) = x
Equiv.symm_apply_apply

@[simp] theorem 
symm_comp_self: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), ↑e.symm ∘ ↑e = id
symm_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 = g
funext 
e: α ≃ β
e.
symm_apply_apply: ∀ {α : Sort ?u.33484} {β : Sort ?u.33483} (e : α ≃ β) (x : α), ↑e.symm (↑e x) = x
symm_apply_apply
#align equiv.symm_comp_self 
Equiv.symm_comp_self: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), ↑e.symm ∘ ↑e = id
Equiv.symm_comp_self

@[simp] theorem 
self_comp_symm: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), ↑e ∘ ↑e.symm = id
self_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 = g
funext 
e: α ≃ β
e.
apply_symm_apply: ∀ {α : Sort ?u.33747} {β : Sort ?u.33746} (e : α ≃ β) (x : β), ↑e (↑e.symm x) = x
apply_symm_apply
#align equiv.self_comp_symm 
Equiv.self_comp_symm: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), ↑e ∘ ↑e.symm = id
Equiv.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 = a
rfl
#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.Linter
simpNF] theorem 
symm_symm_apply: ∀ {α : Sort u} {β : Sort v} (f : α ≃ β) (b : α), ↑f.symm.symm b = ↑f b
symm_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 = a
rfl
#align equiv.symm_symm_apply 
Equiv.symm_symm_apply: ∀ {α : Sort u} {β : Sort v} (f : α ≃ β) (b : α), ↑f.symm.symm b = ↑f b
Equiv.symm_symm_apply

theorem 
apply_eq_iff_eq: ∀ {α : Sort u} {β : Sort v} (f : α ≃ β) {x y : α}, ↑f x = ↑f y ↔ x = y
apply_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 = y
EquivLike.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 = y
Equiv.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 y
apply_eq_iff_eq_symm_apply (
f: α ≃ β
f : 
α: Sort u
α ≃ 
β: Sort v
β) : 
f: α ≃ β
f 
x: ?m.34536
x = 
y: ?m.34594
y ↔ 
x: ?m.34536
x = 
f: α ≃ β
f.
symm: {α : Sort ?u.34654} → {β : Sort ?u.34653} → α ≃ β → β ≃ α
symm 
y: ?m.34594
y := by
Goals accomplished! 🐙
  
α: Sort u

β: Sort v

γ: Sort w

x: α

y: (fun x => β) x

f: α ≃ β

↑f x = y ↔ x = ↑f.symm yconv_lhs => 
α: Sort u

β: Sort v

γ: Sort w

x: α

y: (fun x => β) x

f: α ≃ β

↑f x = y ↔ x = ↑f.symm yrw [
α: Sort u

β: Sort v

γ: Sort w

x: α

y: (fun x => β) x

f: α ≃ β

↑f x = y← 
apply_symm_apply: ∀ {α : Sort ?u.34759} {β : Sort ?u.34758} (e : α ≃ β) (x : β), ↑e (↑e.symm x) = x
apply_symm_apply 
f: α ≃ β
f 
y: (fun x => β) x
y
α: Sort u

β: Sort v

γ: Sort w

x: α

y: (fun x => β) x

f: α ≃ β

↑f x = ↑f (↑f.symm y)]
α: Sort u

β: Sort v

γ: Sort w

x: α

y: (fun x => β) x

f: α ≃ β

↑f x = ↑f (↑f.symm y)
  
α: Sort u

β: Sort v

γ: Sort w

x: α

y: (fun x => β) x

f: α ≃ β

↑f x = y ↔ x = ↑f.symm yrw [
α: Sort u

β: Sort v

γ: Sort w

x: α

y: (fun x => β) x

f: α ≃ β

↑f x = ↑f (↑f.symm y) ↔ x = ↑f.symm y
apply_eq_iff_eq: ∀ {α : Sort ?u.34799} {β : Sort ?u.34798} (f : α ≃ β) {x y : α}, ↑f x = ↑f y ↔ x = y
apply_eq_iff_eq
α: Sort u

β: Sort v

γ: Sort w

x: α

y: (fun x => β) x

f: α ≃ β

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 y
Equiv.apply_eq_iff_eq_symm_apply

@[simp] theorem 
cast_apply: ∀ {α β : Sort u_1} (h : α = β) (x : α), ↑(Equiv.cast h) x = cast h x
cast_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 = a
rfl
#align equiv.cast_apply 
Equiv.cast_apply: ∀ {α β : Sort u_1} (h : α = β) (x : α), ↑(Equiv.cast h) x = cast h x
Equiv.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 = a
symm := 
rfl: ∀ {α : Sort ?u.35062} {a : α}, a = a
rfl
#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 = a
rfl) : 
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 = a
rfl
#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 = c
trans 
h2: β = γ
h2) :=
  
ext: ∀ {α : Sort ?u.35255} {β : Sort ?u.35254} {f g : α ≃ β}, (∀ (x : α), ↑f x = ↑g x) → f = g
ext fun 
x: ?m.35266
x => by
Goals accomplished! 🐙 
α✝: Sort u

β✝: Sort v

γ✝: Sort w

α, β, γ: Sort u_1

h: α = β

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_1

x: α

↑((Equiv.cast (_ : α = α)).trans (Equiv.cast (_ : α = α))) x = ↑(Equiv.cast (_ : α = α)) x;
α✝: Sort u

β: Sort v

γ: Sort w

α: Sort u_1

x: α

↑((Equiv.cast (_ : α = α)).trans (Equiv.cast (_ : α = α))) x = ↑(Equiv.cast (_ : α = α)) x 
α✝: Sort u

β✝: Sort v

γ✝: Sort w

α, β, γ: Sort u_1

h: α = β

h2: β = γ

x: α

↑((Equiv.cast h).trans (Equiv.cast h2)) x = ↑(Equiv.cast (_ : α = γ)) xrfl
Goals 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 b
cast_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} → β → Prop
HEq 
a: α
a 
b: β
b := by
Goals accomplished! 🐙
  
α✝: Sort u

β✝: Sort v

γ: Sort w

α, β: Sort u_1

h: α = β

a: α

b: β

↑(Equiv.cast h) a = b ↔ HEq a bsubst 
h: α = β
h
α✝: Sort u

β: Sort v

γ: Sort w

α: Sort u_1

a, b: α

↑(Equiv.cast (_ : α = α)) a = b ↔ HEq a b;
α✝: Sort u

β: Sort v

γ: Sort w

α: Sort u_1

a, b: α

↑(Equiv.cast (_ : α = α)) a = b ↔ HEq a b 
α✝: Sort u

β✝: Sort v

γ: Sort w

α, β: Sort u_1

h: α = β

a: α

b: β

↑(Equiv.cast h) a = b ↔ HEq a bsimp [
coe_refl: ∀ {α : Sort ?u.35462}, ↑(Equiv.refl α) = id
coe_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 b
Equiv.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 y
symm_apply_eq {
α: ?m.35654
α 
β: ?m.35657
β} (
e: α ≃ β
e : 
α: ?m.35654
α ≃ 
β: ?m.35657
β) {
x: β
x 
y: (fun x => α) x
y} : 
e: α ≃ β
e.
symm: {α : Sort ?u.35672} → {β : Sort ?u.35671} → α ≃ β → β ≃ α
symm 
x: ?m.35664
x = 
y: ?m.35667
y ↔ 
x: ?m.35664
x = 
e: α ≃ β
e 
y: ?m.35667
y :=
  ⟨fun 
H: ?m.35829
H => by
Goals accomplished! 🐙 
α✝: Sort u

β✝: Sort v

γ: Sort w

α: Sort u_1

β: Sort u_2

e: α ≃ β

x: β

y: (fun x => α) x

H: ↑e.symm x = y

x = ↑e ysimp [
H: ↑e.symm x = y
H.
symm: ∀ {α : Sort ?u.35845} {a b : α}, a = b → b = a
symm]
Goals accomplished! 🐙, fun 
H: ?m.35836
H => by
Goals accomplished! 🐙 
α✝: Sort u

β✝: Sort v

γ: Sort w

α: Sort u_1

β: Sort u_2

e: α ≃ β

x: β

y: (fun x => α) x

H: x = ↑e y

↑e.symm x = ysimp [
H: x = ↑e y
H]
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 y
Equiv.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 = x
eq_symm_apply {
α: ?m.36056
α 
β: ?m.36059
β} (
e: α ≃ β
e : 
α: ?m.36056
α ≃ 
β: ?m.36059
β) {
x: β
x 
y: (fun x => α) x
y} : 
y: ?m.36069
y = 
e: α ≃ β
e.
symm: {α : Sort ?u.36074} → {β : Sort ?u.36073} → α ≃ β → β ≃ α
symm 
x: ?m.36066
x ↔ 
e: α ≃ β
e 
y: ?m.36069
y = 
x: ?m.36066
x :=
  (
eq_comm: ∀ {α : Sort ?u.36223} {a b : α}, a = b ↔ b = a
eq_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 y
symm_apply_eq).
trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans 
eq_comm: ∀ {α : Sort ?u.36273} {a b : α}, a = b ↔ b = a
eq_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 = x
Equiv.eq_symm_apply

@[simp] theorem 
symm_symm: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.symm.symm = e
symm_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 := by
Goals accomplished! 🐙 
α: Sort u

β: Sort v

γ: Sort w

e: α ≃ β

e.symm.symm = ecases 
e: α ≃ β
e
α: Sort u

β: Sort v

γ: Sort w

toFun✝: α → β

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 w

toFun✝: α → β

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 w

e: α ≃ β

e.symm.symm = erfl
Goals accomplished! 🐙
#align equiv.symm_symm 
Equiv.symm_symm: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.symm.symm = e
Equiv.symm_symm

@[simp] theorem 
trans_refl: ∀ (e : α ≃ β), e.trans (Equiv.refl β) = e
trans_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 := by
Goals accomplished! 🐙 
α: Sort u

β: Sort v

γ: Sort w

e: α ≃ β

e.trans (Equiv.refl β) = ecases 
e: α ≃ β
e
α: Sort u

β: Sort v

γ: Sort w

toFun✝: α → β

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 w

toFun✝: α → β

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 w

e: α ≃ β

e.trans (Equiv.refl β) = erfl
Goals accomplished! 🐙
#align equiv.trans_refl 
Equiv.trans_refl: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.trans (Equiv.refl β) = e
Equiv.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 = a
rfl
#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 = e
refl_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 := by
Goals accomplished! 🐙 
α: Sort u

β: Sort v

γ: Sort w

e: α ≃ β

(Equiv.refl α).trans e = ecases 
e: α ≃ β
e
α: Sort u

β: Sort v

γ: Sort w

toFun✝: α → β

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 w

toFun✝: α → β

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 w

e: α ≃ β

(Equiv.refl α).trans e = erfl
Goals accomplished! 🐙
#align equiv.refl_trans 
Equiv.refl_trans: ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), (Equiv.refl α).trans e = e
Equiv.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 = g
ext <| by
Goals accomplished! 🐙 
α: Sort u

β: Sort v

γ: Sort w

e: α ≃ β

∀ (x : β), ↑(e.symm.trans e) x = ↑(Equiv.refl β) xsimp
Goals 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 = g
ext <| by
Goals accomplished! 🐙 
α: Sort u

β: Sort v

γ: Sort w

e: α ≃ β

∀ (x : α), ↑(e.trans e.symm) x = ↑(Equiv.refl α) xsimp
Goals 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 = g
Equiv.ext fun 
_: ?m.37687
_ => 
rfl: ∀ {α : Sort ?u.37689} {a : α}, a = a
rfl
#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 ↑f
leftInverse_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} → (β → α) → (α → β) → Prop
LeftInverse 
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.toFun
left_inv
#align equiv.left_inverse_symm 
Equiv.leftInverse_symm: ∀ {α : Sort u} {β : Sort v} (f : α ≃ β), LeftInverse ↑f.symm ↑f
Equiv.leftInverse_symm

theorem 
rightInverse_symm: ∀ {α : Sort u} {β : Sort v} (f : α ≃ β), Function.RightInverse ↑f.symm ↑f
rightInverse_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} → (β → α) → (α → β) → Prop
Function.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.toFun
right_inv
#align equiv.right_inverse_symm 
Equiv.rightInverse_symm: ∀ {α : Sort u} {β : Sort v} (f : α ≃ β), Function.RightInverse ↑f.symm ↑f
Equiv.rightInverse_symm

theorem 
injective_comp: ∀ (e : α ≃ β) (f : β → γ), Injective (f ∘ ↑e) ↔ Injective f
injective_comp (
e: α ≃ β
e : 
α: Sort u
α ≃ 
β: Sort v
β) (
f: β → γ
f : 
β: Sort v
β → 
γ: Sort w
γ) : 
Injective: {α : Sort ?u.38085} → {β : Sort ?u.38084} → (α → β) → Prop
Injective (
f: β → γ
f ∘ 
e: α ≃ β
e) ↔ 
Injective: {α : Sort ?u.38171} → {β : Sort ?u.38170} → (α → β) → Prop
Injective 
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 f
EquivLike.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 f
Equiv.injective_comp

theorem 
comp_injective: ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (f : α → β) (e : β ≃ γ), Injective (↑e ∘ f) ↔ Injective f
comp_injective (
f: α → β
f : 
α: Sort u
α → 
β: Sort v
β) (
e: β ≃ γ
e : 
β: Sort v
β ≃ 
γ: Sort w
γ) : 
Injective: {α : Sort ?u.38243} → {β : Sort ?u.38242} → (α → β) → Prop
Injective (
e: β ≃ γ
e ∘ 
f: α → β
f) ↔ 
Injective: {α : Sort ?u.38329} → {β : Sort ?u.38328} → (α → β) → Prop
Injective 
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 f
EquivLike.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 f
Equiv.comp_injective

theorem 
surjective_comp: ∀ (e : α ≃ β) (f : β → γ), Surjective (f ∘ ↑e) ↔ Surjective f
surjective_comp (
e: α ≃ β
e : 
α: Sort u
α ≃ 
β: Sort v
β) (
f: β → γ
f : 
β: Sort v
β → 
γ: Sort w
γ) : 
Surjective: {α : Sort ?u.38401} → {β : Sort ?u.38400} → (α → β) → Prop
Surjective (
f: β → γ
f ∘ 
e: α ≃ β
e) ↔ 
Surjective: {α : Sort ?u.38487} → {β : Sort ?u.38486} → (α → β) → Prop
Surjective 
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 f
EquivLike.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 f
Equiv.surjective_comp

theorem 
comp_surjective: ∀ (f : α → β) (e : β ≃ γ), Surjective (↑e ∘ f) ↔ Surjective f
comp_surjective (
f: α → β
f : 
α: Sort u
α → 
β: Sort v
β) (
e: β ≃ γ
e : 
β: Sort v
β ≃ 
γ: Sort w
γ) : 
Surjective: {α : Sort ?u.38559} → {β : Sort ?u.38558} → (α → β) → Prop
Surjective (
e: β ≃ γ
e ∘ 
f: α → β
f) ↔ 
Surjective: {α : Sort ?u.38645} → {β : Sort ?u.38644} → (α → β) → Prop
Surjective 
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 f
EquivLike.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 f
Equiv.comp_surjective

theorem 
bijective_comp: ∀ (e : α ≃ β) (f : β → γ), Bijective (f ∘ ↑e) ↔ Bijective f
bijective_comp (
e: α ≃ β
e : 
α: Sort u
α ≃ 
β: Sort v
β) (
f: β → γ
f : 
β: Sort v
β → 
γ: Sort w
γ) : 
Bijective: {α : Sort ?u.38717} → {β : Sort ?u.38716} → (α → β) → Prop
Bijective (
f: β → γ
f ∘ 
e: α ≃ β
e) ↔ 
Bijective: {α : Sort ?u.38803} → {β : Sort ?u.38802} → (α → β) → Prop
Bijective 
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 f
EquivLike.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 f
Equiv.bijective_comp

theorem 
comp_bijective: ∀ (f : α → β) (e : β ≃ γ), Bijective (↑e ∘ f) ↔ Bijective f
comp_bijective (
f: α → β
f : 
α: Sort u
α → 
β: Sort v
β) (
e: β ≃ γ
e : 
β: Sort v
β ≃ 
γ: Sort w
γ) : 
Bijective: {α : Sort ?u.38875} → {β : Sort ?u.38874} → (α → β) → Prop
Bijective (
e: β ≃ γ
e ∘ 
f: α → β
f) ↔ 
Bijective: {α : Sort ?u.38961} → {β : Sort ?u.38960} → (α → β) → Prop
Bijective 
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 f
EquivLike.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 f
Equiv.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.39059
ac := (
ab: α ≃ β
ab.
symm: {α : Sort ?u.39062} → {β : Sort ?u.39061} → α ≃ β → β ≃ α
symm.
trans: {α : Sort ?u.39069} → {β : Sort ?u.39068} → {γ : Sort ?u.39067} → α ≃ β → β ≃ γ → α ≃ γ
trans 
ac: ?m.39059
ac).
trans: {α : Sort ?u.39086} → {β : Sort ?u.39085} → {γ : Sort ?u.39084} → α ≃ β → β ≃ γ → α ≃ γ
trans 
cd: γ ≃ δ
cd
  invFun 
bd: ?m.39104
bd := 
ab: α ≃ β
ab.
trans: {α : Sort ?u.39108} → {β : Sort ?u.39107} → {γ : Sort ?u.39106} → α ≃ β → β ≃ γ → α ≃ γ
trans <| 
bd: ?m.39104
bd.
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.39140
ac := by
Goals accomplished! 🐙 
α: Sort u

β: Sort v

γ: Sort w

δ: Sort ?u.39038

ab: α ≃ β

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.39038

ab: α ≃ β

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.39038

ab: α ≃ β

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.39038

ab: α ≃ β

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) = x
symm_apply_apply]
Goals accomplished! 🐙
  right_inv 
ac: ?m.39146
ac := by
Goals accomplished! 🐙 
α: Sort u

β: Sort v

γ: Sort w

δ: Sort ?u.39038

ab: α ≃ β

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.39038

ab: α ≃ β

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.39038

ab: α ≃ β

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.39038

ab: α ≃ β

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) = x
apply_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
β) := by
Goals accomplished! 🐙 
α✝: Sort u

β✝: Sort v

γ: Sort w

α: Sort u_1

β: Sort u_2

equivCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ≃ β)ext
α✝: Sort u

β✝: Sort v

γ: Sort w

α: Sort u_1

β: Sort u_2

x✝¹: α ≃ β

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_2

x✝¹: α ≃ β

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_2

equivCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ≃ β)rfl
Goals 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.symm
equivCongr_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 := by
Goals accomplished! 🐙 
α: Sort u

β: Sort v

γ: Sort w

δ: Sort u_1

ab: α ≃ β

cd: γ ≃ δ

(equivCongr ab cd).symm = equivCongr ab.symm cd.symmext
α: Sort u

β: Sort v

γ: Sort w

δ: Sort u_1

ab: α ≃ β

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_1

ab: α ≃ β

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_1

ab: α ≃ β

cd: γ ≃ δ

(equivCongr ab cd).symm = equivCongr ab.symm cd.symmrfl
Goals 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.symm
Equiv.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) := by
Goals accomplished! 🐙
  
α: 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)ext
α: Sort u

β: Sort v

γ: Sort w

δ: Sort u_1

ε: Sort u_2

ζ: Sort u_3

ab: α ≃ β

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_3

ab: α ≃ β

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_3

ab: α ≃ β

de: δ ≃ ε

bc: β ≃ γ

ef: ε ≃ ζ

(equivCongr ab de).trans (equivCongr bc ef) = equivCongr (ab.trans bc) (de.trans ef)rfl
Goals 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 bg
equivCongr_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 = a
rfl
#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