/-
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 group_theory.perm.basic
! leanprover-community/mathlib commit b86832321b586c6ac23ef8cdef6a7a27e42b13bd
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Pi
import Mathlib.Algebra.Group.Prod
import Mathlib.Algebra.Hom.Iterate
import Mathlib.Logic.Equiv.Set

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

This file defines the `Group` structure on `Equiv.Perm α`.
-/


universe u v

namespace Equiv

variable {
α: Type u
α : 
Type u: Type (u+1)
Type u} {
β: Type v
β : 
Type v: Type (v+1)
Type v}

namespace Perm

instance 
permGroup: Group (Perm α)
permGroup : 
Group: Type ?u.10 → Type ?u.10
Group (
Perm: Sort ?u.11 → Sort (max1?u.11)
Perm 
α: Type u
α) where
  mul 
f: ?m.29
f 
g: ?m.32
g := 
Equiv.trans: {α : Sort ?u.36} → {β : Sort ?u.35} → {γ : Sort ?u.34} → α ≃ β → β ≃ γ → α ≃ γ
Equiv.trans 
g: ?m.32
g 
f: ?m.29
f
  one := 
Equiv.refl: (α : Sort ?u.96) → α ≃ α
Equiv.refl 
α: Type u
α
  inv := 
Equiv.symm: {α : Sort ?u.118} → {β : Sort ?u.117} → α ≃ β → β ≃ α
Equiv.symm
  mul_assoc 
f: ?m.49
f 
g: ?m.52
g 
h: ?m.55
h := (
trans_assoc: ∀ {α : Sort ?u.59} {β : Sort ?u.58} {γ : Sort ?u.57} {δ : Sort ?u.60} (ab : α ≃ β) (bc : β ≃ γ) (cd : γ ≃ δ),
  (ab.trans bc).trans cd = ab.trans (bc.trans cd)
trans_assoc 
_: ?m.61 ≃ ?m.62
_ 
_: ?m.62 ≃ ?m.63
_ 
_: ?m.63 ≃ ?m.64
_).
symm: ∀ {α : Sort ?u.68} {a b : α}, a = b → b = a
symm
  one_mul := 
trans_refl: ∀ {α : Sort ?u.98} {β : Sort ?u.97} (e : α ≃ β), e.trans (Equiv.refl β) = e
trans_refl
  mul_one := 
refl_trans: ∀ {α : Sort ?u.105} {β : Sort ?u.104} (e : α ≃ β), (Equiv.refl α).trans e = e
refl_trans
  mul_left_inv := 
self_trans_symm: ∀ {α : Sort ?u.209} {β : Sort ?u.208} (e : α ≃ β), e.trans e.symm = Equiv.refl α
self_trans_symm
#align equiv.perm.perm_group 
Equiv.Perm.permGroup: {α : Type u} → Group (Perm α)
Equiv.Perm.permGroup

@[simp]
theorem 
default_eq: default = 1
default_eq : (
default: {α : Sort ?u.1070} → [self : Inhabited α] → α
default : 
Perm: Sort ?u.1069 → Sort (max1?u.1069)
Perm 
α: Type u
α) = 
1: ?m.1228
1 :=
  
rfl: ∀ {α : Sort ?u.1517} {a : α}, a = a
rfl
#align equiv.perm.default_eq 
Equiv.Perm.default_eq: ∀ {α : Type u}, default = 1
Equiv.Perm.default_eq

/-- The permutation of a type is equivalent to the units group of the endomorphisms monoid of this
type. -/
@[
simps: ∀ {α : Type u} (e : Perm α) (a : α), Units.inv (↑equivUnitsEnd e) a = toFun e.symm a
simps]
def 
equivUnitsEnd: {α : Type u} → Perm α ≃* (Function.End α)ˣ
equivUnitsEnd : 
Perm: Sort ?u.1537 → Sort (max1?u.1537)
Perm 
α: Type u
α ≃* 
Units: (α : Type ?u.1538) → [inst : Monoid α] → Type ?u.1538
Units (
Function.End: Type ?u.1539 → Type ?u.1539
Function.End 
α: Type u
α) where
  -- Porting note: needed to add `.toFun`.
  toFun 
e: ?m.2160
e := ⟨
e: ?m.2160
e.
toFun: {α : Sort ?u.2197} → {β : Sort ?u.2196} → α ≃ β → α → β
toFun, 
e: ?m.2160
e.
symm: {α : Sort ?u.2202} → {β : Sort ?u.2201} → α ≃ β → β ≃ α
symm.
toFun: {α : Sort ?u.2206} → {β : Sort ?u.2205} → α ≃ β → α → β
toFun, 
e: ?m.2160
e.
self_comp_symm: ∀ {α : Sort ?u.2211} {β : Sort ?u.2210} (e : α ≃ β), ↑e ∘ ↑e.symm = id
self_comp_symm, 
e: ?m.2160
e.
symm_comp_self: ∀ {α : Sort ?u.2228} {β : Sort ?u.2227} (e : α ≃ β), ↑e.symm ∘ ↑e = id
symm_comp_self⟩
  invFun 
u: ?m.2237
u :=
    ⟨(
u: ?m.2237
u : 
Function.End: Type ?u.2250 → Type ?u.2250
Function.End 
α: Type u
α), (↑
u: ?m.2237
u⁻¹ : 
Function.End: Type ?u.3453 → Type ?u.3453
Function.End 
α: Type u
α), 
congr_fun: ∀ {α : Sort ?u.4648} {β : α → Sort ?u.4647} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congr_fun 
u: ?m.2237
u.
inv_val: ∀ {α : Type ?u.4661} [inst : Monoid α] (self : αˣ), self.inv * ↑self = 1
inv_val, 
congr_fun: ∀ {α : Sort ?u.4670} {β : α → Sort ?u.4669} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g a
congr_fun 
u: ?m.2237
u.
val_inv: ∀ {α : Type ?u.4681} [inst : Monoid α] (self : αˣ), ↑self * self.inv = 1
val_inv⟩
  left_inv 
_: ?m.4693
_ := 
ext: ∀ {α : Sort ?u.4695} {σ τ : Perm α}, (∀ (x : α), ↑σ x = ↑τ x) → σ = τ
ext fun 
_: ?m.4704
_ => 
rfl: ∀ {α : Sort ?u.4706} {a : α}, a = a
rfl
  right_inv 
_: ?m.4715
_ := 
Units.ext: ∀ {α : Type ?u.4717} [inst : Monoid α], Function.Injective Units.val
Units.ext 
rfl: ∀ {α : Sort ?u.4747} {a : α}, a = a
rfl
  map_mul' 
_: ?m.4752
_ 
_: ?m.4755
_ := 
rfl: ∀ {α : Sort ?u.4757} {a : α}, a = a
rfl
#align equiv.perm.equiv_units_End 
Equiv.Perm.equivUnitsEnd: {α : Type u} → Perm α ≃* (Function.End α)ˣ
Equiv.Perm.equivUnitsEnd
#align equiv.perm.equiv_units_End_symm_apply_apply 
Equiv.Perm.equivUnitsEnd_symm_apply_apply: ∀ {α : Type u} (u : (Function.End α)ˣ), ↑(↑(MulEquiv.symm equivUnitsEnd) u) = ↑u
Equiv.Perm.equivUnitsEnd_symm_apply_apply
#align equiv.perm.equiv_units_End_symm_apply_symm_apply 
Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply: ∀ {α : Type u} (u : (Function.End α)ˣ), ↑(↑(MulEquiv.symm equivUnitsEnd) u).symm = ↑u⁻¹
Equiv.Perm.equivUnitsEnd_symm_apply_symm_apply

/-- Lift a monoid homomorphism `f : G →* Function.End α` to a monoid homomorphism
`f : G →* Equiv.Perm α`. -/
@[simps!]
def 
_root_.MonoidHom.toHomPerm: {α : Type u} → {G : Type u_1} → [inst : Group G] → (G →* Function.End α) → G →* Perm α
_root_.MonoidHom.toHomPerm {
G: Type ?u.5515
G : 
Type _: Type (?u.5515+1)
Type _} [
Group: Type ?u.5518 → Type ?u.5518
Group 
G: Type ?u.5515
G] (
f: G →* Function.End α
f : 
G: Type ?u.5515
G →* 
Function.End: Type ?u.5523 → Type ?u.5523
Function.End 
α: Type u
α) : 
G: Type ?u.5515
G →* 
Perm: Sort ?u.6007 → Sort (max1?u.6007)
Perm 
α: Type u
α :=
  
equivUnitsEnd: {α : Type ?u.6208} → Perm α ≃* (Function.End α)ˣ
equivUnitsEnd.
symm: {M : Type ?u.6211} → {N : Type ?u.6210} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → N ≃* M
symm.
toMonoidHom: {M : Type ?u.6811} → {N : Type ?u.6810} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M ≃* N → M →* N
toMonoidHom.
comp: {M : Type ?u.7017} →
  {N : Type ?u.7016} →
    {P : Type ?u.7015} →
      [inst : MulOneClass M] → [inst_1 : MulOneClass N] → [inst_2 : MulOneClass P] → (N →* P) → (M →* N) → M →* P
comp 
f: G →* Function.End α
f.
toHomUnits: {G : Type ?u.7061} → {M : Type ?u.7060} → [inst : Group G] → [inst_1 : Monoid M] → (G →* M) → G →* Mˣ
toHomUnits
#align monoid_hom.to_hom_perm 
MonoidHom.toHomPerm: {α : Type u} → {G : Type u_1} → [inst : Group G] → (G →* Function.End α) → G →* Perm α
MonoidHom.toHomPerm
#align monoid_hom.to_hom_perm_apply_symm_apply 
MonoidHom.toHomPerm_apply_symm_apply: ∀ {α : Type u} {G : Type u_1} [inst : Group G] (f : G →* Function.End α) (a : G),
  ↑(↑(MonoidHom.toHomPerm f) a).symm = ↑(↑(MonoidHom.toHomUnits f) a)⁻¹
MonoidHom.toHomPerm_apply_symm_apply
#align monoid_hom.to_hom_perm_apply_apply 
MonoidHom.toHomPerm_apply_apply: ∀ {α : Type u} {G : Type u_1} [inst : Group G] (f : G →* Function.End α) (a : G), ↑(↑(MonoidHom.toHomPerm f) a) = ↑f a
MonoidHom.toHomPerm_apply_apply

theorem 
mul_apply: ∀ {α : Type u} (f g : Perm α) (x : α), ↑(f * g) x = ↑f (↑g x)
mul_apply (
f: Perm α
f 
g: Perm α
g : 
Perm: Sort ?u.7725 → Sort (max1?u.7725)
Perm 
α: Type u
α) (
x: α
x) : (
f: Perm α
f * 
g: Perm α
g) 
x: ?m.7731
x = 
f: Perm α
f (
g: Perm α
g 
x: ?m.7731
x) :=
  
Equiv.trans_apply: ∀ {α : Sort ?u.8589} {β : Sort ?u.8588} {γ : Sort ?u.8587} (f : α ≃ β) (g : β ≃ γ) (a : α), ↑(f.trans g) a = ↑g (↑f a)
Equiv.trans_apply 
_: ?m.8590 ≃ ?m.8591
_ 
_: ?m.8591 ≃ ?m.8592
_ 
_: ?m.8590
_
#align equiv.perm.mul_apply 
Equiv.Perm.mul_apply: ∀ {α : Type u} (f g : Perm α) (x : α), ↑(f * g) x = ↑f (↑g x)
Equiv.Perm.mul_apply

theorem 
one_apply: ∀ {α : Type u} (x : α), ↑1 x = x
one_apply (
x: ?m.8625
x) : (
1: ?m.8632
1 : 
Perm: Sort ?u.8630 → Sort (max1?u.8630)
Perm 
α: Type u
α) 
x: ?m.8625
x = 
x: ?m.8625
x :=
  
rfl: ∀ {α : Sort ?u.8989} {a : α}, a = a
rfl
#align equiv.perm.one_apply 
Equiv.Perm.one_apply: ∀ {α : Type u} (x : α), ↑1 x = x
Equiv.Perm.one_apply

@[simp]
theorem 
inv_apply_self: ∀ {α : Type u} (f : Perm α) (x : α), ↑f⁻¹ (↑f x) = x
inv_apply_self (
f: Perm α
f : 
Perm: Sort ?u.9004 → Sort (max1?u.9004)
Perm 
α: Type u
α) (
x: ?m.9007
x) : 
f: Perm α
f⁻¹ (
f: Perm α
f 
x: ?m.9007
x) = 
x: ?m.9007
x :=
  
f: Perm α
f.
symm_apply_apply: ∀ {α : Sort ?u.9235} {β : Sort ?u.9234} (e : α ≃ β) (x : α), ↑e.symm (↑e x) = x
symm_apply_apply 
x: α
x
#align equiv.perm.inv_apply_self 
Equiv.Perm.inv_apply_self: ∀ {α : Type u} (f : Perm α) (x : α), ↑f⁻¹ (↑f x) = x
Equiv.Perm.inv_apply_self

@[simp]
theorem 
apply_inv_self: ∀ {α : Type u} (f : Perm α) (x : α), ↑f (↑f⁻¹ x) = x
apply_inv_self (
f: Perm α
f : 
Perm: Sort ?u.9275 → Sort (max1?u.9275)
Perm 
α: Type u
α) (
x: ?m.9278
x) : 
f: Perm α
f (
f: Perm α
f⁻¹ 
x: ?m.9278
x) = 
x: ?m.9278
x :=
  
f: Perm α
f.
apply_symm_apply: ∀ {α : Sort ?u.9506} {β : Sort ?u.9505} (e : α ≃ β) (x : β), ↑e (↑e.symm x) = x
apply_symm_apply 
x: α
x
#align equiv.perm.apply_inv_self 
Equiv.Perm.apply_inv_self: ∀ {α : Type u} (f : Perm α) (x : α), ↑f (↑f⁻¹ x) = x
Equiv.Perm.apply_inv_self

theorem 
one_def: 1 = Equiv.refl α
one_def : (
1: ?m.9550
1 : 
Perm: Sort ?u.9548 → Sort (max1?u.9548)
Perm 
α: Type u
α) = 
Equiv.refl: (α : Sort ?u.9825) → α ≃ α
Equiv.refl 
α: Type u
α :=
  
rfl: ∀ {α : Sort ?u.9828} {a : α}, a = a
rfl
#align equiv.perm.one_def 
Equiv.Perm.one_def: ∀ {α : Type u}, 1 = Equiv.refl α
Equiv.Perm.one_def

theorem 
mul_def: ∀ {α : Type u} (f g : Perm α), f * g = g.trans f
mul_def (
f: Perm α
f 
g: Perm α
g : 
Perm: Sort ?u.9840 → Sort (max1?u.9840)
Perm 
α: Type u
α) : 
f: Perm α
f * 
g: Perm α
g = 
g: Perm α
g.
trans: {α : Sort ?u.9852} → {β : Sort ?u.9851} → {γ : Sort ?u.9850} → α ≃ β → β ≃ γ → α ≃ γ
trans 
f: Perm α
f :=
  
rfl: ∀ {α : Sort ?u.10505} {a : α}, a = a
rfl
#align equiv.perm.mul_def 
Equiv.Perm.mul_def: ∀ {α : Type u} (f g : Perm α), f * g = g.trans f
Equiv.Perm.mul_def

theorem 
inv_def: ∀ {α : Type u} (f : Perm α), f⁻¹ = f.symm
inv_def (
f: Perm α
f : 
Perm: Sort ?u.10519 → Sort (max1?u.10519)
Perm 
α: Type u
α) : 
f: Perm α
f⁻¹ = 
f: Perm α
f.
symm: {α : Sort ?u.10600} → {β : Sort ?u.10599} → α ≃ β → β ≃ α
symm :=
  
rfl: ∀ {α : Sort ?u.10611} {a : α}, a = a
rfl
#align equiv.perm.inv_def 
Equiv.Perm.inv_def: ∀ {α : Type u} (f : Perm α), f⁻¹ = f.symm
Equiv.Perm.inv_def

@[simp, norm_cast] lemma 
coe_one: ∀ {α : Type u}, ↑1 = id
coe_one : ⇑(
1: ?m.10628
1 : 
Perm: Sort ?u.10626 → Sort (max1?u.10626)
Perm 
α: Type u
α) = 
id: {α : Sort ?u.10982} → α → α
id := 
rfl: ∀ {α : Sort ?u.11021} {a : α}, a = a
rfl
#align equiv.perm.coe_one 
Equiv.Perm.coe_one: ∀ {α : Type u}, ↑1 = id
Equiv.Perm.coe_one
@[simp, norm_cast] lemma 
coe_mul: ∀ {α : Type u} (f g : Perm α), ↑(f * g) = ↑f ∘ ↑g
coe_mul (
f: Perm α
f 
g: Perm α
g : 
Perm: Sort ?u.11111 → Sort (max1?u.11111)
Perm 
α: Type u
α) : ⇑(
f: Perm α
f * 
g: Perm α
g) = 
f: Perm α
f ∘ 
g: Perm α
g := 
rfl: ∀ {α : Sort ?u.11981} {a : α}, a = a
rfl
#align equiv.perm.coe_mul 
Equiv.Perm.coe_mul: ∀ {α : Type u} (f g : Perm α), ↑(f * g) = ↑f ∘ ↑g
Equiv.Perm.coe_mul
@[norm_cast] lemma 
coe_pow: ∀ {α : Type u} (f : Perm α) (n : ℕ), ↑(f ^ n) = ↑f^[n]
coe_pow (
f: Perm α
f : 
Perm: Sort ?u.12147 → Sort (max1?u.12147)
Perm 
α: Type u
α) (
n: ℕ
n : 
ℕ: Type
ℕ) : ⇑(
f: Perm α
f ^ 
n: ℕ
n) = 
f: Perm α
f^[
n: ℕ
n] :=
hom_coe_pow: ∀ {M : Type ?u.16561} {F : Type ?u.16560} [inst : Monoid F] (c : F → M → M),
  c 1 = id → (∀ (f g : F), c (f * g) = c f ∘ c g) → ∀ (f : F) (n : ℕ), c (f ^ n) = c f^[n]
hom_coe_pow 
_: ?m.16563 → ?m.16562 → ?m.16562
_ 
rfl: ∀ {α : Sort ?u.16566} {a : α}, a = a
rfl (fun 
_: ?m.17041
_ 
_: ?m.17044
_ ↦ 
rfl: ∀ {α : Sort ?u.17046} {a : α}, a = a
rfl) 
_: ?m.16563
_ 
_: ℕ
_
#align equiv.perm.coe_pow 
Equiv.Perm.coe_pow: ∀ {α : Type u} (f : Perm α) (n : ℕ), ↑(f ^ n) = ↑f^[n]
Equiv.Perm.coe_pow
@[simp] lemma 
iterate_eq_pow: ∀ (f : Perm α) (n : ℕ), ↑f^[n] = ↑(f ^ n)
iterate_eq_pow (
f: Perm α
f : 
Perm: Sort ?u.17420 → Sort (max1?u.17420)
Perm 
α: Type u
α) (
n: ℕ
n : 
ℕ: Type
ℕ) : 
f: Perm α
f^[
n: ℕ
n] = ⇑(
f: Perm α
f ^ 
n: ℕ
n) := (
coe_pow: ∀ {α : Type ?u.21833} (f : Perm α) (n : ℕ), ↑(f ^ n) = ↑f^[n]
coe_pow 
_: Perm ?m.21834
_ 
_: ℕ
_).
symm: ∀ {α : Sort ?u.21837} {a b : α}, a = b → b = a
symm
#align equiv.perm.iterate_eq_pow 
Equiv.Perm.iterate_eq_pow: ∀ {α : Type u} (f : Perm α) (n : ℕ), ↑f^[n] = ↑(f ^ n)
Equiv.Perm.iterate_eq_pow

theorem 
eq_inv_iff_eq: ∀ {α : Type u} {f : Perm α} {x y : α}, x = ↑f⁻¹ y ↔ ↑f x = y
eq_inv_iff_eq {
f: Perm α
f : 
Perm: Sort ?u.21897 → Sort (max1?u.21897)
Perm 
α: Type u
α} {
x: α
x 
y: α
y : 
α: Type u
α} : 
x: α
x = 
f: Perm α
f⁻¹ 
y: α
y ↔ 
f: Perm α
f 
x: α
x = 
y: α
y :=
  
f: Perm α
f.
eq_symm_apply: ∀ {α : Sort ?u.22131} {β : Sort ?u.22132} (e : α ≃ β) {x : β} {y : (fun x => α) x}, y = ↑e.symm x ↔ ↑e y = x
eq_symm_apply
#align equiv.perm.eq_inv_iff_eq 
Equiv.Perm.eq_inv_iff_eq: ∀ {α : Type u} {f : Perm α} {x y : α}, x = ↑f⁻¹ y ↔ ↑f x = y
Equiv.Perm.eq_inv_iff_eq

theorem 
inv_eq_iff_eq: ∀ {α : Type u} {f : Perm α} {x y : α}, ↑f⁻¹ x = y ↔ x = ↑f y
inv_eq_iff_eq {
f: Perm α
f : 
Perm: Sort ?u.22166 → Sort (max1?u.22166)
Perm 
α: Type u
α} {
x: α
x 
y: α
y : 
α: Type u
α} : 
f: Perm α
f⁻¹ 
x: α
x = 
y: α
y ↔ 
x: α
x = 
f: Perm α
f 
y: α
y :=
  
f: Perm α
f.
symm_apply_eq: ∀ {α : Sort ?u.22400} {β : Sort ?u.22401} (e : α ≃ β) {x : β} {y : (fun x => α) x}, ↑e.symm x = y ↔ x = ↑e y
symm_apply_eq
#align equiv.perm.inv_eq_iff_eq 
Equiv.Perm.inv_eq_iff_eq: ∀ {α : Type u} {f : Perm α} {x y : α}, ↑f⁻¹ x = y ↔ x = ↑f y
Equiv.Perm.inv_eq_iff_eq

theorem 
zpow_apply_comm: ∀ {α : Type u_1} (σ : Perm α) (m n : ℤ) {x : α}, ↑(σ ^ m) (↑(σ ^ n) x) = ↑(σ ^ n) (↑(σ ^ m) x)
zpow_apply_comm {
α: Type ?u.22435
α : 
Type _: Type (?u.22435+1)
Type _} (
σ: Perm α
σ : 
Perm: Sort ?u.22438 → Sort (max1?u.22438)
Perm 
α: Type ?u.22435
α) (
m: ℤ
m 
n: ℤ
n : 
ℤ: Type
ℤ) {
x: α
x : 
α: Type ?u.22435
α} :
    (
σ: Perm α
σ ^ 
m: ℤ
m) ((
σ: Perm α
σ ^ 
n: ℤ
n) 
x: α
x) = (
σ: Perm α
σ ^ 
n: ℤ
n) ((
σ: Perm α
σ ^ 
m: ℤ
m) 
x: α
x) := by
Goals accomplished! 🐙
  
α✝: Type u

β: Type v

α: Type u_1

σ: Perm α

m, n: ℤ

x: α

↑(σ ^ m) (↑(σ ^ n) x) = ↑(σ ^ n) (↑(σ ^ m) x)rw [
α✝: Type u

β: Type v

α: Type u_1

σ: Perm α

m, n: ℤ

x: α

↑(σ ^ m) (↑(σ ^ n) x) = ↑(σ ^ n) (↑(σ ^ m) x)← 
Equiv.Perm.mul_apply: ∀ {α : Type ?u.39141} (f g : Perm α) (x : α), ↑(f * g) x = ↑f (↑g x)
Equiv.Perm.mul_apply,
α✝: Type u

β: Type v

α: Type u_1

σ: Perm α

m, n: ℤ

x: α

↑(σ ^ m * σ ^ n) x = ↑(σ ^ n) (↑(σ ^ m) x) 
α✝: Type u

β: Type v

α: Type u_1

σ: Perm α

m, n: ℤ

x: α

↑(σ ^ m) (↑(σ ^ n) x) = ↑(σ ^ n) (↑(σ ^ m) x)← 
Equiv.Perm.mul_apply: ∀ {α : Type ?u.39202} (f g : Perm α) (x : α), ↑(f * g) x = ↑f (↑g x)
Equiv.Perm.mul_apply,
α✝: Type u

β: Type v

α: Type u_1

σ: Perm α

m, n: ℤ

x: α

↑(σ ^ m * σ ^ n) x = ↑(σ ^ n * σ ^ m) x 
α✝: Type u

β: Type v

α: Type u_1

σ: Perm α

m, n: ℤ

x: α

↑(σ ^ m) (↑(σ ^ n) x) = ↑(σ ^ n) (↑(σ ^ m) x)
zpow_mul_comm: ∀ {G : Type ?u.39231} [inst : Group G] (a : G) (i j : ℤ), a ^ i * a ^ j = a ^ j * a ^ i
zpow_mul_comm
α✝: Type u

β: Type v

α: Type u_1

σ: Perm α

m, n: ℤ

x: α

↑(σ ^ n * σ ^ m) x = ↑(σ ^ n * σ ^ m) x]
Goals accomplished! 🐙
#align equiv.perm.zpow_apply_comm 
Equiv.Perm.zpow_apply_comm: ∀ {α : Type u_1} (σ : Perm α) (m n : ℤ) {x : α}, ↑(σ ^ m) (↑(σ ^ n) x) = ↑(σ ^ n) (↑(σ ^ m) x)
Equiv.Perm.zpow_apply_comm

@[simp] lemma 
image_inv: ∀ (f : Perm α) (s : Set α), ↑f⁻¹ '' s = ↑f ⁻¹' s
image_inv (
f: Perm α
f : 
Perm: Sort ?u.39319 → Sort (max1?u.39319)
Perm 
α: Type u
α) (
s: Set α
s : 
Set: Type ?u.39322 → Type ?u.39322
Set 
α: Type u
α) : ↑
f: Perm α
f⁻¹ '' 
s: Set α
s = 
f: Perm α
f ⁻¹' 
s: Set α
s := 
f: Perm α
f⁻¹.
image_eq_preimage: ∀ {α : Type ?u.39569} {β : Type ?u.39570} (e : α ≃ β) (s : Set α), ↑e '' s = ↑e.symm ⁻¹' s
image_eq_preimage 
_: Set ?m.39575
_
#align equiv.perm.image_inv 
Equiv.Perm.image_inv: ∀ {α : Type u} (f : Perm α) (s : Set α), ↑f⁻¹ '' s = ↑f ⁻¹' s
Equiv.Perm.image_inv
@[simp] lemma 
preimage_inv: ∀ {α : Type u} (f : Perm α) (s : Set α), ↑f⁻¹ ⁻¹' s = ↑f '' s
preimage_inv (
f: Perm α
f : 
Perm: Sort ?u.39627 → Sort (max1?u.39627)
Perm 
α: Type u
α) (
s: Set α
s : 
Set: Type ?u.39630 → Type ?u.39630
Set 
α: Type u
α) : ↑
f: Perm α
f⁻¹ ⁻¹' 
s: Set α
s = 
f: Perm α
f '' 
s: Set α
s :=
(
f: Perm α
f.
image_eq_preimage: ∀ {α : Type ?u.39874} {β : Type ?u.39875} (e : α ≃ β) (s : Set α), ↑e '' s = ↑e.symm ⁻¹' s
image_eq_preimage 
_: Set ?m.39880
_).
symm: ∀ {α : Sort ?u.39885} {a b : α}, a = b → b = a
symm
#align equiv.perm.preimage_inv 
Equiv.Perm.preimage_inv: ∀ {α : Type u} (f : Perm α) (s : Set α), ↑f⁻¹ ⁻¹' s = ↑f '' s
Equiv.Perm.preimage_inv

/-! Lemmas about mixing `Perm` with `Equiv`. Because we have multiple ways to express
`Equiv.refl`, `Equiv.symm`, and `Equiv.trans`, we want simp lemmas for every combination.
The assumption made here is that if you're using the group structure, you want to preserve it after
simp. -/


@[simp]
theorem 
trans_one: ∀ {α : Sort u_1} {β : Type u_2} (e : α ≃ β), e.trans 1 = e
trans_one {
α: Sort u_1
α : 
Sort _: Type ?u.39942
Sort
Sort _: Type ?u.39942
 _} {
β: Type ?u.39945
β : 
Type _: Type (?u.39945+1)
Type _} (
e: α ≃ β
e : 
α: Sort ?u.39942
α ≃ 
β: Type ?u.39945
β) : 
e: α ≃ β
e.
trans: {α : Sort ?u.39955} → {β : Sort ?u.39954} → {γ : Sort ?u.39953} → α ≃ β → β ≃ γ → α ≃ γ
trans (
1: ?m.39969
1 : 
Perm: Sort ?u.39967 → Sort (max1?u.39967)
Perm 
β: Type ?u.39945
β) = 
e: α ≃ β
e :=
  
Equiv.trans_refl: ∀ {α : Sort ?u.40252} {β : Sort ?u.40251} (e : α ≃ β), e.trans (Equiv.refl β) = e
Equiv.trans_refl 
e: α ≃ β
e
#align equiv.perm.trans_one 
Equiv.Perm.trans_one: ∀ {α : Sort u_1} {β : Type u_2} (e : α ≃ β), e.trans 1 = e
Equiv.Perm.trans_one

@[simp]
theorem 
mul_refl: ∀ {α : Type u} (e : Perm α), e * Equiv.refl α = e
mul_refl (
e: Perm α
e : 
Perm: Sort ?u.40294 → Sort (max1?u.40294)
Perm 
α: Type u
α) : 
e: Perm α
e * 
Equiv.refl: (α : Sort ?u.40301) → α ≃ α
Equiv.refl 
α: Type u
α = 
e: Perm α
e :=
  
Equiv.trans_refl: ∀ {α : Sort ?u.40943} {β : Sort ?u.40942} (e : α ≃ β), e.trans (Equiv.refl β) = e
Equiv.trans_refl 
e: Perm α
e
#align equiv.perm.mul_refl 
Equiv.Perm.mul_refl: ∀ {α : Type u} (e : Perm α), e * Equiv.refl α = e
Equiv.Perm.mul_refl

@[simp]
theorem 
one_symm: ∀ {α : Type u}, 1.symm = 1
one_symm : (
1: ?m.41010
1 : 
Perm: Sort ?u.41008 → Sort (max1?u.41008)
Perm 
α: Type u
α).
symm: {α : Sort ?u.41286} → {β : Sort ?u.41285} → α ≃ β → β ≃ α
symm = 
1: ?m.41295
1 :=
  
Equiv.refl_symm: ∀ {α : Sort ?u.41520}, (Equiv.refl α).symm = Equiv.refl α
Equiv.refl_symm
#align equiv.perm.one_symm 
Equiv.Perm.one_symm: ∀ {α : Type u}, 1.symm = 1
Equiv.Perm.one_symm

@[simp]
theorem 
refl_inv: ∀ {α : Type u}, (Equiv.refl α)⁻¹ = 1
refl_inv : (
Equiv.refl: (α : Sort ?u.41550) → α ≃ α
Equiv.refl 
α: Type u
α : 
Perm: Sort ?u.41549 → Sort (max1?u.41549)
Perm 
α: Type u
α)⁻¹ = 
1: ?m.41626
1 :=
  
Equiv.refl_symm: ∀ {α : Sort ?u.41896}, (Equiv.refl α).symm = Equiv.refl α
Equiv.refl_symm
#align equiv.perm.refl_inv 
Equiv.Perm.refl_inv: ∀ {α : Type u}, (Equiv.refl α)⁻¹ = 1
Equiv.Perm.refl_inv

@[simp]
theorem 
one_trans: ∀ {α : Type u_1} {β : Sort u_2} (e : α ≃ β), 1.trans e = e
one_trans {
α: Type u_1
α : 
Type _: Type (?u.41921+1)
Type _} {
β: Sort ?u.41924
β : 
Sort _: Type ?u.41924
Sort
Sort _: Type ?u.41924
 _} (
e: α ≃ β
e : 
α: Type ?u.41921
α ≃ 
β: Sort ?u.41924
β) : (
1: ?m.41935
1 : 
Perm: Sort ?u.41933 → Sort (max1?u.41933)
Perm 
α: Type ?u.41921
α).
trans: {α : Sort ?u.42212} → {β : Sort ?u.42211} → {γ : Sort ?u.42210} → α ≃ β → β ≃ γ → α ≃ γ
trans 
e: α ≃ β
e = 
e: α ≃ β
e :=
  
Equiv.refl_trans: ∀ {α : Sort ?u.42233} {β : Sort ?u.42232} (e : α ≃ β), (Equiv.refl α).trans e = e
Equiv.refl_trans 
e: α ≃ β
e
#align equiv.perm.one_trans 
Equiv.Perm.one_trans: ∀ {α : Type u_1} {β : Sort u_2} (e : α ≃ β), 1.trans e = e
Equiv.Perm.one_trans

@[simp]
theorem 
refl_mul: ∀ {α : Type u} (e : Perm α), Equiv.refl α * e = e
refl_mul (
e: Perm α
e : 
Perm: Sort ?u.42272 → Sort (max1?u.42272)
Perm 
α: Type u
α) : 
Equiv.refl: (α : Sort ?u.42279) → α ≃ α
Equiv.refl 
α: Type u
α * 
e: Perm α
e = 
e: Perm α
e :=
  
Equiv.refl_trans: ∀ {α : Sort ?u.42922} {β : Sort ?u.42921} (e : α ≃ β), (Equiv.refl α).trans e = e
Equiv.refl_trans 
e: Perm α
e
#align equiv.perm.refl_mul 
Equiv.Perm.refl_mul: ∀ {α : Type u} (e : Perm α), Equiv.refl α * e = e
Equiv.Perm.refl_mul

@[simp]
theorem 
inv_trans_self: ∀ (e : Perm α), e⁻¹.trans e = 1
inv_trans_self (
e: Perm α
e : 
Perm: Sort ?u.42985 → Sort (max1?u.42985)
Perm 
α: Type u
α) : 
e: Perm α
e⁻¹.
trans: {α : Sort ?u.43067} → {β : Sort ?u.43066} → {γ : Sort ?u.43065} → α ≃ β → β ≃ γ → α ≃ γ
trans 
e: Perm α
e = 
1: ?m.43081
1 :=
  
Equiv.symm_trans_self: ∀ {α : Sort ?u.43356} {β : Sort ?u.43355} (e : α ≃ β), e.symm.trans e = Equiv.refl β
Equiv.symm_trans_self 
e: Perm α
e
#align equiv.perm.inv_trans_self 
Equiv.Perm.inv_trans_self: ∀ {α : Type u} (e : Perm α), e⁻¹.trans e = 1
Equiv.Perm.inv_trans_self

@[simp]
theorem 
mul_symm: ∀ {α : Type u} (e : Perm α), e * e.symm = 1
mul_symm (
e: Perm α
e : 
Perm: Sort ?u.43390 → Sort (max1?u.43390)
Perm 
α: Type u
α) : 
e: Perm α
e * 
e: Perm α
e.
symm: {α : Sort ?u.43398} → {β : Sort ?u.43397} → α ≃ β → β ≃ α
symm = 
1: ?m.43407
1 :=
  
Equiv.symm_trans_self: ∀ {α : Sort ?u.44293} {β : Sort ?u.44292} (e : α ≃ β), e.symm.trans e = Equiv.refl β
Equiv.symm_trans_self 
e: Perm α
e
#align equiv.perm.mul_symm 
Equiv.Perm.mul_symm: ∀ {α : Type u} (e : Perm α), e * e.symm = 1
Equiv.Perm.mul_symm

@[simp]
theorem 
self_trans_inv: ∀ {α : Type u} (e : Perm α), e.trans e⁻¹ = 1
self_trans_inv (
e: Perm α
e : 
Perm: Sort ?u.44323 → Sort (max1?u.44323)
Perm 
α: Type u
α) : 
e: Perm α
e.
trans: {α : Sort ?u.44329} → {β : Sort ?u.44328} → {γ : Sort ?u.44327} → α ≃ β → β ≃ γ → α ≃ γ
trans 
e: Perm α
e⁻¹ = 
1: ?m.44446
1 :=
  
Equiv.self_trans_symm: ∀ {α : Sort ?u.44718} {β : Sort ?u.44717} (e : α ≃ β), e.trans e.symm = Equiv.refl α
Equiv.self_trans_symm 
e: Perm α
e
#align equiv.perm.self_trans_inv 
Equiv.Perm.self_trans_inv: ∀ {α : Type u} (e : Perm α), e.trans e⁻¹ = 1
Equiv.Perm.self_trans_inv

@[simp]
theorem 
symm_mul: ∀ {α : Type u} (e : Perm α), e.symm * e = 1
symm_mul (
e: Perm α
e : 
Perm: Sort ?u.44752 → Sort (max1?u.44752)
Perm 
α: Type u
α) : 
e: Perm α
e.
symm: {α : Sort ?u.44760} → {β : Sort ?u.44759} → α ≃ β → β ≃ α
symm * 
e: Perm α
e = 
1: ?m.44769
1 :=
  
Equiv.self_trans_symm: ∀ {α : Sort ?u.45657} {β : Sort ?u.45656} (e : α ≃ β), e.trans e.symm = Equiv.refl α
Equiv.self_trans_symm 
e: Perm α
e
#align equiv.perm.symm_mul 
Equiv.Perm.symm_mul: ∀ {α : Type u} (e : Perm α), e.symm * e = 1
Equiv.Perm.symm_mul

/-! Lemmas about `Equiv.Perm.sumCongr` re-expressed via the group structure. -/


@[simp]
theorem 
sumCongr_mul: ∀ {α : Type u_1} {β : Type u_2} (e : Perm α) (f : Perm β) (g : Perm α) (h : Perm β),
  sumCongr e f * sumCongr g h = sumCongr (e * g) (f * h)
sumCongr_mul {
α: Type u_1
α 
β: Type ?u.45690
β : 
Type _: Type (?u.45690+1)
Type _} (
e: Perm α
e : 
Perm: Sort ?u.45693 → Sort (max1?u.45693)
Perm 
α: Type ?u.45687
α) (
f: Perm β
f : 
Perm: Sort ?u.45696 → Sort (max1?u.45696)
Perm 
β: Type ?u.45690
β) (
g: Perm α
g : 
Perm: Sort ?u.45699 → Sort (max1?u.45699)
Perm 
α: Type ?u.45687
α) (
h: Perm β
h : 
Perm: Sort ?u.45702 → Sort (max1?u.45702)
Perm 
β: Type ?u.45690
β) :
    
sumCongr: {α : Type ?u.45710} → {β : Type ?u.45709} → Perm α → Perm β → Perm (α ⊕ β)
sumCongr 
e: Perm α
e 
f: Perm β
f * 
sumCongr: {α : Type ?u.45718} → {β : Type ?u.45717} → Perm α → Perm β → Perm (α ⊕ β)
sumCongr 
g: Perm α
g 
h: Perm β
h = 
sumCongr: {α : Type ?u.45724} → {β : Type ?u.45723} → Perm α → Perm β → Perm (α ⊕ β)
sumCongr (
e: Perm α
e * 
g: Perm α
g) (
f: Perm β
f * 
h: Perm β
h) :=
  
sumCongr_trans: ∀ {α : Type ?u.47158} {β : Type ?u.47159} (e : Perm α) (f : Perm β) (g : Perm α) (h : Perm β),
  (sumCongr e f).trans (sumCongr g h) = sumCongr (e.trans g) (f.trans h)
sumCongr_trans 
g: Perm α
g 
h: Perm β
h 
e: Perm α
e 
f: Perm β
f
#align equiv.perm.sum_congr_mul 
Equiv.Perm.sumCongr_mul: ∀ {α : Type u_1} {β : Type u_2} (e : Perm α) (f : Perm β) (g : Perm α) (h : Perm β),
  sumCongr e f * sumCongr g h = sumCongr (e * g) (f * h)
Equiv.Perm.sumCongr_mul

@[simp]
theorem 
sumCongr_inv: ∀ {α : Type u_1} {β : Type u_2} (e : Perm α) (f : Perm β), (sumCongr e f)⁻¹ = sumCongr e⁻¹ f⁻¹
sumCongr_inv {
α: Type ?u.47225
α 
β: Type ?u.47228
β : 
Type _: Type (?u.47228+1)
Type _} (
e: Perm α
e : 
Perm: Sort ?u.47231 → Sort (max1?u.47231)
Perm 
α: Type ?u.47225
α) (
f: Perm β
f : 
Perm: Sort ?u.47234 → Sort (max1?u.47234)
Perm 
β: Type ?u.47228
β) :
    (
sumCongr: {α : Type ?u.47242} → {β : Type ?u.47241} → Perm α → Perm β → Perm (α ⊕ β)
sumCongr 
e: Perm α
e 
f: Perm β
f)⁻¹ = 
sumCongr: {α : Type ?u.47325} → {β : Type ?u.47324} → Perm α → Perm β → Perm (α ⊕ β)
sumCongr 
e: Perm α
e⁻¹ 
f: Perm β
f⁻¹ :=
  
sumCongr_symm: ∀ {α : Type ?u.47538} {β : Type ?u.47539} (e : Perm α) (f : Perm β), (sumCongr e f).symm = sumCongr e.symm f.symm
sumCongr_symm 
e: Perm α
e 
f: Perm β
f
#align equiv.perm.sum_congr_inv 
Equiv.Perm.sumCongr_inv: ∀ {α : Type u_1} {β : Type u_2} (e : Perm α) (f : Perm β), (sumCongr e f)⁻¹ = sumCongr e⁻¹ f⁻¹
Equiv.Perm.sumCongr_inv

@[simp]
theorem 
sumCongr_one: ∀ {α : Type u_1} {β : Type u_2}, sumCongr 1 1 = 1
sumCongr_one {
α: Type u_1
α 
β: Type ?u.47595
β : 
Type _: Type (?u.47595+1)
Type _} : 
sumCongr: {α : Type ?u.47600} → {β : Type ?u.47599} → Perm α → Perm β → Perm (α ⊕ β)
sumCongr (
1: ?m.47606
1 : 
Perm: Sort ?u.47604 → Sort (max1?u.47604)
Perm 
α: Type ?u.47592
α) (
1: ?m.47884
1 : 
Perm: Sort ?u.47882 → Sort (max1?u.47882)
Perm 
β: Type ?u.47595
β) = 
1: ?m.48160
1 :=
  
sumCongr_refl: ∀ {α : Type ?u.48454} {β : Type ?u.48455}, sumCongr (Equiv.refl α) (Equiv.refl β) = Equiv.refl (α ⊕ β)
sumCongr_refl
#align equiv.perm.sum_congr_one 
Equiv.Perm.sumCongr_one: ∀ {α : Type u_1} {β : Type u_2}, sumCongr 1 1 = 1
Equiv.Perm.sumCongr_one

/-- `Equiv.Perm.sumCongr` as a `MonoidHom`, with its two arguments bundled into a single `prod`.

This is particularly useful for its `MonoidHom.range` projection, which is the subgroup of
permutations which do not exchange elements between `α` and `β`. -/
@[
simps: ∀ (α : Type u_1) (β : Type u_2) (a : Perm α × Perm β), ↑(sumCongrHom α β) a = sumCongr a.fst a.snd
simps]
def 
sumCongrHom: (α : Type u_1) → (β : Type u_2) → Perm α × Perm β →* Perm (α ⊕ β)
sumCongrHom (
α: Type ?u.48498
α 
β: Type ?u.48501
β : 
Type _: Type (?u.48501+1)
Type _) : 
Perm: Sort ?u.48508 → Sort (max1?u.48508)
Perm 
α: Type ?u.48498
α × 
Perm: Sort ?u.48509 → Sort (max1?u.48509)
Perm 
β: Type ?u.48501
β →* 
Perm: Sort ?u.48510 → Sort (max1?u.48510)
Perm (
Sum: Type ?u.48512 → Type ?u.48511 → Type (max?u.48512?u.48511)
Sum 
α: Type ?u.48498
α 
β: Type ?u.48501
β) where
  toFun 
a: ?m.50561
a := 
sumCongr: {α : Type ?u.50564} → {β : Type ?u.50563} → Perm α → Perm β → Perm (α ⊕ β)
sumCongr 
a: ?m.50561
a.
1: {α : Type ?u.50570} → {β : Type ?u.50569} → α × β → α
1 
a: ?m.50561
a.
2: {α : Type ?u.50577} → {β : Type ?u.50576} → α × β → β
2
  map_one' := 
sumCongr_one: ∀ {α : Type ?u.50583} {β : Type ?u.50584}, sumCongr 1 1 = 1
sumCongr_one
  map_mul' 
_: ?m.50598
_ 
_: ?m.50601
_ := (
sumCongr_mul: ∀ {α : Type ?u.50603} {β : Type ?u.50604} (e : Perm α) (f : Perm β) (g : Perm α) (h : Perm β),
  sumCongr e f * sumCongr g h = sumCongr (e * g) (f * h)
sumCongr_mul 
_: Perm ?m.50605
_ 
_: Perm ?m.50606
_ 
_: Perm ?m.50605
_ 
_: Perm ?m.50606
_).
symm: ∀ {α : Sort ?u.50611} {a b : α}, a = b → b = a
symm
#align equiv.perm.sum_congr_hom 
Equiv.Perm.sumCongrHom: (α : Type u_1) → (β : Type u_2) → Perm α × Perm β →* Perm (α ⊕ β)
Equiv.Perm.sumCongrHom
#align equiv.perm.sum_congr_hom_apply 
Equiv.Perm.sumCongrHom_apply: ∀ (α : Type u_1) (β : Type u_2) (a : Perm α × Perm β), ↑(sumCongrHom α β) a = sumCongr a.fst a.snd
Equiv.Perm.sumCongrHom_apply

theorem 
sumCongrHom_injective: ∀ {α : Type u_1} {β : Type u_2}, Function.Injective ↑(sumCongrHom α β)
sumCongrHom_injective {
α: Type ?u.51431
α 
β: Type ?u.51434
β : 
Type _: Type (?u.51431+1)
Type _} : 
Function.Injective: {α : Sort ?u.51438} → {β : Sort ?u.51437} → (α → β) → Prop
Function.Injective (
sumCongrHom: (α : Type ?u.51442) → (β : Type ?u.51441) → Perm α × Perm β →* Perm (α ⊕ β)
sumCongrHom 
α: Type ?u.51431
α 
β: Type ?u.51434
β) := by
Goals accomplished! 🐙
  
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

Function.Injective ↑(sumCongrHom α β)rintro 
⟨⟩: Perm α × Perm β
⟨⟩ 
⟨⟩: Perm α × Perm β
⟨⟩ 
h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
h
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

mk.mk
(fst✝¹, snd✝¹) = (fst✝, snd✝)
  
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

Function.Injective ↑(sumCongrHom α β)rw [
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

mk.mk
(fst✝¹, snd✝¹) = (fst✝, snd✝)
Prod.mk.inj_iff: ∀ {α : Type ?u.52030} {β : Type ?u.52031} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
Prod.mk.inj_iff
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

mk.mk
fst✝¹ = fst✝ ∧ snd✝¹ = snd✝]
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

mk.mk
fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
  
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

Function.Injective ↑(sumCongrHom α β)constructor
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

mk.mk.left
fst✝¹ = fst✝
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

mk.mk.right
snd✝¹ = snd✝ 
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

mk.mk
fst✝¹ = fst✝ ∧ snd✝¹ = snd✝<;>
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

mk.mk.left
fst✝¹ = fst✝
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

mk.mk.right
snd✝¹ = snd✝ 
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

mk.mk
fst✝¹ = fst✝ ∧ snd✝¹ = snd✝ext 
i: ?α
i
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

i: β

mk.mk.right.H
↑snd✝¹ i = ↑snd✝ i
  
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

Function.Injective ↑(sumCongrHom α β)·
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

i: α

mk.mk.left.H
↑fst✝¹ i = ↑fst✝ i 
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

i: α

mk.mk.left.H
↑fst✝¹ i = ↑fst✝ i
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

i: β

mk.mk.right.H
↑snd✝¹ i = ↑snd✝ isimpa using 
Equiv.congr_fun: ∀ {α : Sort ?u.52333} {β : Sort ?u.52332} {f g : α ≃ β}, f = g → ∀ (x : α), ↑f x = ↑g x
Equiv.congr_fun 
h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
h (
Sum.inl: {α : Type ?u.52349} → {β : Type ?u.52348} → α → α ⊕ β
Sum.inl 
i: ?α
i)
Goals accomplished! 🐙
  
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

Function.Injective ↑(sumCongrHom α β)·
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

i: β

mk.mk.right.H
↑snd✝¹ i = ↑snd✝ i 
α✝: Type u

β✝: Type v

α: Type u_1

β: Type u_2

fst✝¹: Perm α

snd✝¹: Perm β

fst✝: Perm α

snd✝: Perm β

h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)

i: β

mk.mk.right.H
↑snd✝¹ i = ↑snd✝ isimpa using 
Equiv.congr_fun: ∀ {α : Sort ?u.53080} {β : Sort ?u.53079} {f g : α ≃ β}, f = g → ∀ (x : α), ↑f x = ↑g x
Equiv.congr_fun 
h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)
h (
Sum.inr: {α : Type ?u.53091} → {β : Type ?u.53090} → β → α ⊕ β
Sum.inr 
i: ?α
i)
Goals accomplished! 🐙
#align equiv.perm.sum_congr_hom_injective 
Equiv.Perm.sumCongrHom_injective: ∀ {α : Type u_1} {β : Type u_2}, Function.Injective ↑(sumCongrHom α β)
Equiv.Perm.sumCongrHom_injective

@[simp]
theorem 
sumCongr_swap_one: ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] (i j : α),
  sumCongr (swap i j) 1 = swap (Sum.inl i) (Sum.inl j)
sumCongr_swap_one {
α: Type u_1
α 
β: Type ?u.53431
β : 
Type _: Type (?u.53431+1)
Type _} [
DecidableEq: Sort ?u.53434 → Sort (max1?u.53434)
DecidableEq 
α: Type ?u.53428
α] [
DecidableEq: Sort ?u.53443 → Sort (max1?u.53443)
DecidableEq 
β: Type ?u.53431
β] (
i: α
i 
j: α
j : 
α: Type ?u.53428
α) :
    
sumCongr: {α : Type ?u.53458} → {β : Type ?u.53457} → Perm α → Perm β → Perm (α ⊕ β)
sumCongr (
Equiv.swap: {α : Sort ?u.53461} → [inst : DecidableEq α] → α → α → Perm α
Equiv.swap 
i: α
i 
j: α
j) (
1: ?m.53562
1 : 
Perm: Sort ?u.53560 → Sort (max1?u.53560)
Perm 
β: Type ?u.53431
β) = 
Equiv.swap: {α : Sort ?u.53837} → [inst : DecidableEq α] → α → α → Perm α
Equiv.swap (
Sum.inl: {α : Type ?u.53841} → {β : Type ?u.53840} → α → α ⊕ β
Sum.inl 
i: α
i) (
Sum.inl: {α : Type ?u.53847} → {β : Type ?u.53846} → α → α ⊕ β
Sum.inl 
j: α
j) :=
  
sumCongr_swap_refl: ∀ {α : Type ?u.54379} {β : Type ?u.54380} [inst : DecidableEq α] [inst_1 : DecidableEq β] (i j : α),
  sumCongr (swap i j) (Equiv.refl β) = swap (Sum.inl i) (Sum.inl j)
sumCongr_swap_refl 
i: α
i 
j: α
j
#align equiv.perm.sum_congr_swap_one 
Equiv.Perm.sumCongr_swap_one: ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] (i j : α),
  sumCongr (swap i j) 1 = swap (Sum.inl i) (Sum.inl j)
Equiv.Perm.sumCongr_swap_one

@[simp]
theorem 
sumCongr_one_swap: ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] (i j : β),
  sumCongr 1 (swap i j) = swap (Sum.inr i) (Sum.inr j)
sumCongr_one_swap {
α: Type ?u.54593
α 
β: Type ?u.54596
β : 
Type _: Type (?u.54596+1)
Type _} [
DecidableEq: Sort ?u.54599 → Sort (max1?u.54599)
DecidableEq 
α: Type ?u.54593
α] [
DecidableEq: Sort ?u.54608 → Sort (max1?u.54608)
DecidableEq 
β: Type ?u.54596
β] (
i: β
i 
j: β
j : 
β: Type ?u.54596
β) :
    
sumCongr: {α : Type ?u.54623} → {β : Type ?u.54622} → Perm α → Perm β → Perm (α ⊕ β)
sumCongr (
1: ?m.54629
1 : 
Perm: Sort ?u.54627 → Sort (max1?u.54627)
Perm 
α: Type ?u.54593
α) (
Equiv.swap: {α : Sort ?u.54904} → [inst : DecidableEq α] → α → α → Perm α
Equiv.swap 
i: β
i 
j: β
j) = 
Equiv.swap: {α : Sort ?u.54996} → [inst : DecidableEq α] → α → α → Perm α
Equiv.swap (
Sum.inr: {α : Type ?u.55000} → {β : Type ?u.54999} → β → α ⊕ β
Sum.inr 
i: β
i) (
Sum.inr: {α : Type ?u.55006} → {β : Type ?u.55005} → β → α ⊕ β
Sum.inr 
j: β
j) :=
  
sumCongr_refl_swap: ∀ {α : Type ?u.55448} {β : Type ?u.55449} [inst : DecidableEq α] [inst_1 : DecidableEq β] (i j : β),
  sumCongr (Equiv.refl α) (swap i j) = swap (Sum.inr i) (Sum.inr j)
sumCongr_refl_swap 
i: β
i 
j: β
j
#align equiv.perm.sum_congr_one_swap 
Equiv.Perm.sumCongr_one_swap: ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq β] (i j : β),
  sumCongr 1 (swap i j) = swap (Sum.inr i) (Sum.inr j)
Equiv.Perm.sumCongr_one_swap

/-! Lemmas about `Equiv.Perm.sigmaCongrRight` re-expressed via the group structure. -/


@[simp]
theorem 
sigmaCongrRight_mul: ∀ {α : Type u_1} {β : α → Type u_2} (F G : (a : α) → Perm (β a)),
  sigmaCongrRight F * sigmaCongrRight G = sigmaCongrRight (F * G)
sigmaCongrRight_mul {
α: Type u_1
α : 
Type _: Type (?u.55662+1)
Type _} {
β: α → Type ?u.55667
β : 
α: Type ?u.55662
α → 
Type _: Type (?u.55667+1)
Type _} (
F: (a : α) → Perm (β a)
F : ∀ 
a: ?m.55671
a, 
Perm: Sort ?u.55674 → Sort (max1?u.55674)
Perm (
β: α → Type ?u.55667
β 
a: ?m.55671
a))
    (
G: (a : α) → Perm (β a)
G : ∀ 
a: ?m.55679
a, 
Perm: Sort ?u.55682 → Sort (max1?u.55682)
Perm (
β: α → Type ?u.55667
β 
a: ?m.55679
a)) : 
sigmaCongrRight: {α : Type ?u.55691} → {β : α → Type ?u.55690} → ((a : α) → Perm (β a)) → Perm ((a : α) × β a)
sigmaCongrRight 
F: (a : α) → Perm (β a)
F * 
sigmaCongrRight: {α : Type ?u.55702} → {β : α → Type ?u.55701} → ((a : α) → Perm (β a)) → Perm ((a : α) × β a)
sigmaCongrRight 
G: (a : α) → Perm (β a)
G = 
sigmaCongrRight: {α : Type ?u.55712} → {β : α → Type ?u.55711} → ((a : α) → Perm (β a)) → Perm ((a : α) × β a)
sigmaCongrRight (
F: (a : α) → Perm (β a)
F * 
G: (a : α) → Perm (β a)
G) :=
  
sigmaCongrRight_trans: ∀ {α : Type ?u.57286} {β : α → Type ?u.57287} (F G : (a : α) → Perm (β a)),
  (sigmaCongrRight F).trans (sigmaCongrRight G) = sigmaCongrRight fun a => (F a).trans (G a)
sigmaCongrRight_trans 
G: (a : α) → Perm (β a)
G 
F: (a : α) → Perm (β a)
F
#align equiv.perm.sigma_congr_right_mul 
Equiv.Perm.sigmaCongrRight_mul: ∀ {α : Type u_1} {β : α → Type u_2} (F G : (a : α) → Perm (β a)),
  sigmaCongrRight F * sigmaCongrRight G = sigmaCongrRight (F * G)
Equiv.Perm.sigmaCongrRight_mul

@[simp]
theorem 
sigmaCongrRight_inv: ∀ {α : Type u_1} {β : α → Type u_2} (F : (a : α) → Perm (β a)), (sigmaCongrRight F)⁻¹ = sigmaCongrRight fun a => (F a)⁻¹
sigmaCongrRight_inv {
α: Type u_1
α : 
Type _: Type (?u.57366+1)
Type _} {
β: α → Type ?u.57371
β : 
α: Type ?u.57366
α → 
Type _: Type (?u.57371+1)
Type _} (
F: (a : α) → Perm (β a)
F : ∀ 
a: ?m.57375
a, 
Perm: Sort ?u.57378 → Sort (max1?u.57378)
Perm (
β: α → Type ?u.57371
β 
a: ?m.57375
a)) :
    (
sigmaCongrRight: {α : Type ?u.57387} → {β : α → Type ?u.57386} → ((a : α) → Perm (β a)) → Perm ((a : α) × β a)
sigmaCongrRight 
F: (a : α) → Perm (β a)
F)⁻¹ = 
sigmaCongrRight: {α : Type ?u.57475} → {β : α → Type ?u.57474} → ((a : α) → Perm (β a)) → Perm ((a : α) × β a)
sigmaCongrRight fun 
a: ?m.57479
a => (
F: (a : α) → Perm (β a)
F 
a: ?m.57479
a)⁻¹ :=
  
sigmaCongrRight_symm: ∀ {α : Type ?u.57593} {β : α → Type ?u.57594} (F : (a : α) → Perm (β a)),
  (sigmaCongrRight F).symm = sigmaCongrRight fun a => (F a).symm
sigmaCongrRight_symm 
F: (a : α) → Perm (β a)
F
#align equiv.perm.sigma_congr_right_inv 
Equiv.Perm.sigmaCongrRight_inv: ∀ {α : Type u_1} {β : α → Type u_2} (F : (a : α) → Perm (β a)), (sigmaCongrRight F)⁻¹ = sigmaCongrRight fun a => (F a)⁻¹
Equiv.Perm.sigmaCongrRight_inv

@[simp]
theorem 
sigmaCongrRight_one: ∀ {α : Type u_1} {β : α → Type u_2}, sigmaCongrRight 1 = 1
sigmaCongrRight_one {
α: Type u_1
α : 
Type _: Type (?u.57658+1)
Type _} {
β: α → Type ?u.57663
β : 
α: Type ?u.57658
α → 
Type _: Type (?u.57663+1)
Type _} :
    
sigmaCongrRight: {α : Type ?u.57668} → {β : α → Type ?u.57667} → ((a : α) → Perm (β a)) → Perm ((a : α) × β a)
sigmaCongrRight (
1: ?m.57678
1 : ∀ 
a: ?m.57673
a, 
Equiv.Perm: Sort ?u.57676 → Sort (max1?u.57676)
Equiv.Perm <| 
β: α → Type ?u.57663
β 
a: ?m.57673
a) = 
1: ?m.58367
1 :=
  
sigmaCongrRight_refl: ∀ {α : Type ?u.58657} {β : α → Type ?u.58658}, (sigmaCongrRight fun a => Equiv.refl (β a)) = Equiv.refl ((a : α) × β a)
sigmaCongrRight_refl
#align equiv.perm.sigma_congr_right_one 
Equiv.Perm.sigmaCongrRight_one: ∀ {α : Type u_1} {β : α → Type u_2}, sigmaCongrRight 1 = 1
Equiv.Perm.sigmaCongrRight_one

/-- `Equiv.Perm.sigmaCongrRight` as a `MonoidHom`.

This is particularly useful for its `MonoidHom.range` projection, which is the subgroup of
permutations which do not exchange elements between fibers. -/
@[
simps: ∀ {α : Type u_1} (β : α → Type u_2) (F : (a : α) → Perm (β a)), ↑(sigmaCongrRightHom β) F = sigmaCongrRight F
simps]
def 
sigmaCongrRightHom: {α : Type u_1} → (β : α → Type u_2) → ((a : α) → Perm (β a)) →* Perm ((a : α) × β a)
sigmaCongrRightHom {
α: Type ?u.58704
α : 
Type _: Type (?u.58704+1)
Type _} (
β: α → Type ?u.58709
β : 
α: Type ?u.58704
α → 
Type _: Type (?u.58709+1)
Type _) : (∀ 
a: ?m.58715
a, 
Perm: Sort ?u.58718 → Sort (max1?u.58718)
Perm (
β: α → Type ?u.58709
β 
a: ?m.58715
a)) →* 
Perm: Sort ?u.58720 → Sort (max1?u.58720)
Perm (Σ
a: ?m.58725
a, 
β: α → Type ?u.58709
β 
a: ?m.58725
a) where
  toFun := 
sigmaCongrRight: {α : Type ?u.61227} → {β : α → Type ?u.61226} → ((a : α) → Perm (β a)) → Perm ((a : α) × β a)
sigmaCongrRight
  map_one' := 
sigmaCongrRight_one: ∀ {α : Type ?u.61241} {β : α → Type ?u.61242}, sigmaCongrRight 1 = 1
sigmaCongrRight_one
  map_mul' 
_: ?m.61266
_ 
_: ?m.61271
_ := (
sigmaCongrRight_mul: ∀ {α : Type ?u.61275} {β : α → Type ?u.61276} (F G : (a : α) → Perm (β a)),
  sigmaCongrRight F * sigmaCongrRight G = sigmaCongrRight (F * G)
sigmaCongrRight_mul 
_: (a : ?m.61277) → Perm (?m.61278 a)
_ 
_: (a : ?m.61277) → Perm (?m.61278 a)
_).
symm: ∀ {α : Sort ?u.61281} {a b : α}, a = b → b = a
symm
#align equiv.perm.sigma_congr_right_hom 
Equiv.Perm.sigmaCongrRightHom: {α : Type u_1} → (β : α → Type u_2) → ((a : α) → Perm (β a)) →* Perm ((a : α) × β a)
Equiv.Perm.sigmaCongrRightHom
#align equiv.perm.sigma_congr_right_hom_apply 
Equiv.Perm.sigmaCongrRightHom_apply: ∀ {α : Type u_1} (β : α → Type u_2) (F : (a : α) → Perm (β a)), ↑(sigmaCongrRightHom β) F = sigmaCongrRight F
Equiv.Perm.sigmaCongrRightHom_apply

theorem 
sigmaCongrRightHom_injective: ∀ {α : Type u_1} {β : α → Type u_2}, Function.Injective ↑(sigmaCongrRightHom β)
sigmaCongrRightHom_injective {
α: Type ?u.61990
α : 
Type _: Type (?u.61990+1)
Type _} {
β: α → Type u_2
β : 
α: Type ?u.61990
α → 
Type _: Type (?u.61995+1)
Type _} :
    
Function.Injective: {α : Sort ?u.61999} → {β : Sort ?u.61998} → (α → β) → Prop
Function.Injective (
sigmaCongrRightHom: {α : Type ?u.62003} → (β : α → Type ?u.62002) → ((a : α) → Perm (β a)) →* Perm ((a : α) × β a)
sigmaCongrRightHom 
β: α → Type ?u.61995
β) := by
Goals accomplished! 🐙
  
α✝: Type u

β✝: Type v

α: Type u_1

β: α → Type u_2

Function.Injective ↑(sigmaCongrRightHom β)intro 
x: (a : α) → Perm (β a)
x 
y: (a : α) → Perm (β a)
y 
h: ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) y
h
α✝: Type u

β✝: Type v

α: Type u_1

β: α → Type u_2

x, y: (a : α) → Perm (β a)

h: ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) y

x = y
  
α✝: Type u

β✝: Type v

α: Type u_1

β: α → Type u_2

Function.Injective ↑(sigmaCongrRightHom β)ext (
a: ?α
a 
b: ?α
b)
α✝: Type u

β✝: Type v

α: Type u_1

β: α → Type u_2

x, y: (a : α) → Perm (β a)

h: ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) y

a: α

b: β a

h.H
↑(x a) b = ↑(y a) b
  
α✝: Type u

β✝: Type v

α: Type u_1

β: α → Type u_2

Function.Injective ↑(sigmaCongrRightHom β)simpa using 
Equiv.congr_fun: ∀ {α : Sort ?u.62856} {β : Sort ?u.62855} {f g : α ≃ β}, f = g → ∀ (x : α), ↑f x = ↑g x
Equiv.congr_fun 
h: ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) y
h ⟨
a: ?α
a, 
b: ?α
b⟩
Goals accomplished! 🐙
#align equiv.perm.sigma_congr_right_hom_injective 
Equiv.Perm.sigmaCongrRightHom_injective: ∀ {α : Type u_1} {β : α → Type u_2}, Function.Injective ↑(sigmaCongrRightHom β)
Equiv.Perm.sigmaCongrRightHom_injective

/-- `Equiv.Perm.subtypeCongr` as a `MonoidHom`. -/
@[
simps: ∀ {α : Type u} (p : α → Prop) [inst : DecidablePred p] (pair : Perm { a // p a } × Perm { a // ¬p a }),
  ↑(subtypeCongrHom p) pair = subtypeCongr pair.fst pair.snd
simps]
def 
subtypeCongrHom: {α : Type u} → (p : α → Prop) → [inst : DecidablePred p] → Perm { a // p a } × Perm { a // ¬p a } →* Perm α
subtypeCongrHom (
p: α → Prop
p : 
α: Type u
α → 
Prop: Type
Prop) [
DecidablePred: {α : Sort ?u.63569} → (α → Prop) → Sort (max1?u.63569)
DecidablePred 
p: α → Prop
p] :
    
Perm: Sort ?u.63583 → Sort (max1?u.63583)
Perm { 
a: ?m.63587
a // 
p: α → Prop
p 
a: ?m.63587
a } × 
Perm: Sort ?u.63591 → Sort (max1?u.63591)
Perm { 
a: ?m.63595
a // ¬
p: α → Prop
p 
a: ?m.63595
a } →* 
Perm: Sort ?u.63599 → Sort (max1?u.63599)
Perm 
α: Type u
α where
  toFun 
pair: ?m.65490
pair := 
Perm.subtypeCongr: {ε : Type ?u.65492} → {p : ε → Prop} → [inst : DecidablePred p] → Perm { a // p a } → Perm { a // ¬p a } → Perm ε
Perm.subtypeCongr 
pair: ?m.65490
pair.
fst: {α : Type ?u.65616} → {β : Type ?u.65615} → α × β → α
fst 
pair: ?m.65490
pair.
snd: {α : Type ?u.65627} → {β : Type ?u.65626} → α × β → β
snd
  map_one' := 
Perm.subtypeCongr.refl: ∀ {ε : Type ?u.65647} {p : ε → Prop} [inst : DecidablePred p],
  subtypeCongr (Equiv.refl { a // p a }) (Equiv.refl { a // ¬p a }) = Equiv.refl ε
Perm.subtypeCongr.refl
  map_mul' 
_: ?m.65787
_ 
_: ?m.65790
_ := (
Perm.subtypeCongr.trans: ∀ {ε : Type ?u.65792} {p : ε → Prop} [inst : DecidablePred p] (ep ep' : Perm { a // p a })
  (en en' : Perm { a // ¬p a }),
  (subtypeCongr ep en).trans (subtypeCongr ep' en') = subtypeCongr (ep.trans ep') (en.trans en')
Perm.subtypeCongr.trans 
_: Perm { a // ?m.65794 a }
_ 
_: Perm { a // ?m.65794 a }
_ 
_: Perm { a // ¬?m.65794 a }
_ 
_: Perm { a // ¬?m.65794 a }
_).
symm: ∀ {α : Sort ?u.65917} {a b : α}, a = b → b = a
symm
#align equiv.perm.subtype_congr_hom 
Equiv.Perm.subtypeCongrHom: {α : Type u} → (p : α → Prop) → [inst : DecidablePred p] → Perm { a // p a } × Perm { a // ¬p a } →* Perm α
Equiv.Perm.subtypeCongrHom
#align equiv.perm.subtype_congr_hom_apply 
Equiv.Perm.subtypeCongrHom_apply: ∀ {α : Type u} (p : α → Prop) [inst : DecidablePred p] (pair : Perm { a // p a } × Perm { a // ¬p a }),
  ↑(subtypeCongrHom p) pair = subtypeCongr pair.fst pair.snd
Equiv.Perm.subtypeCongrHom_apply

theorem 
subtypeCongrHom_injective: ∀ (p : α → Prop) [inst : DecidablePred p], Function.Injective ↑(subtypeCongrHom p)
subtypeCongrHom_injective (
p: α → Prop
p : 
α: Type u
α → 
Prop: Type
Prop) [
DecidablePred: {α : Sort ?u.66145} → (α → Prop) → Sort (max1?u.66145)
DecidablePred 
p: α → Prop
p] :
    
Function.Injective: {α : Sort ?u.66156} → {β : Sort ?u.66155} → (α → β) → Prop
Function.Injective (
subtypeCongrHom: {α : Type ?u.66159} → (p : α → Prop) → [inst : DecidablePred p] → Perm { a // p a } × Perm { a // ¬p a } →* Perm α
subtypeCongrHom 
p: α → Prop
p) := by
Goals accomplished! 🐙
  
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

Function.Injective ↑(subtypeCongrHom p)rintro 
⟨⟩: Perm { a // p a } × Perm { a // ¬p a }
⟨⟩ 
⟨⟩: Perm { a // p a } × Perm { a // ¬p a }
⟨⟩ 
h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)
h
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

mk.mk
(fst✝¹, snd✝¹) = (fst✝, snd✝)
  
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

Function.Injective ↑(subtypeCongrHom p)rw [
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

mk.mk
(fst✝¹, snd✝¹) = (fst✝, snd✝)
Prod.mk.inj_iff: ∀ {α : Type ?u.66753} {β : Type ?u.66754} {a₁ a₂ : α} {b₁ b₂ : β}, (a₁, b₁) = (a₂, b₂) ↔ a₁ = a₂ ∧ b₁ = b₂
Prod.mk.inj_iff
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

mk.mk
fst✝¹ = fst✝ ∧ snd✝¹ = snd✝]
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

mk.mk
fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
  
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

Function.Injective ↑(subtypeCongrHom p)constructor
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

mk.mk.left
fst✝¹ = fst✝
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

mk.mk.right
snd✝¹ = snd✝ 
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

mk.mk
fst✝¹ = fst✝ ∧ snd✝¹ = snd✝<;>
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

mk.mk.left
fst✝¹ = fst✝
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

mk.mk.right
snd✝¹ = snd✝ 
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

mk.mk
fst✝¹ = fst✝ ∧ snd✝¹ = snd✝ext 
i: ?α
i
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

i: { a // ¬p a }

mk.mk.right.H.a
↑(↑snd✝¹ i) = ↑(↑snd✝ i) 
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

mk.mk
fst✝¹ = fst✝ ∧ snd✝¹ = snd✝<;>
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

i: { a // p a }

mk.mk.left.H.a
↑(↑fst✝¹ i) = ↑(↑fst✝ i)
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

i: { a // ¬p a }

mk.mk.right.H.a
↑(↑snd✝¹ i) = ↑(↑snd✝ i) 
α: Type u

β: Type v

p: α → Prop

inst✝: DecidablePred p

fst✝¹: Perm { a // p a }

snd✝¹: Perm { a // ¬p a }

fst✝: Perm { a // p a }

snd✝: Perm { a // ¬p a }

h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)

mk.mk
fst✝¹ = fst✝ ∧ snd✝¹ = snd✝simpa using 
Equiv.congr_fun: ∀ {α : Sort ?u.67034} {β : Sort ?u.67033} {f g : α ≃ β}, f = g → ∀ (x : α), ↑f x = ↑g x
Equiv.congr_fun 
h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)
h 
i: ?α
i
Goals accomplished! 🐙
#align equiv.perm.subtype_congr_hom_injective 
Equiv.Perm.subtypeCongrHom_injective: ∀ {α : Type u} (p : α → Prop) [inst : DecidablePred p], Function.Injective ↑(subtypeCongrHom p)
Equiv.Perm.subtypeCongrHom_injective

/-- If `e` is also a permutation, we can write `permCongr`
completely in terms of the group structure. -/
@[simp]
theorem 
permCongr_eq_mul: ∀ {α : Type u} (e p : Perm α), ↑(permCongr e) p = e * p * e⁻¹
permCongr_eq_mul (
e: Perm α
e 
p: Perm α
p : 
Perm: Sort ?u.69156 → Sort (max1?u.69156)
Perm 
α: Type u
α) : 
e: Perm α
e.
permCongr: {α' : Type ?u.69161} → {β' : Type ?u.69160} → α' ≃ β' → Perm α' ≃ Perm β'
permCongr 
p: Perm α
p = 
e: Perm α
e * 
p: Perm α
p * 
e: Perm α
e⁻¹ :=
  
rfl: ∀ {α : Sort ?u.70243} {a : α}, a = a
rfl
#align equiv.perm.perm_congr_eq_mul 
Equiv.Perm.permCongr_eq_mul: ∀ {α : Type u} (e p : Perm α), ↑(permCongr e) p = e * p * e⁻¹
Equiv.Perm.permCongr_eq_mul

section ExtendDomain

/-! Lemmas about `Equiv.Perm.extendDomain` re-expressed via the group structure. -/


variable (
e: Perm α
e : 
Perm: Sort ?u.70307 → Sort (max1?u.70307)
Perm 
α: Type u
α) {
p: β → Prop
p : 
β: Type v
β → 
Prop: Type
Prop} [
DecidablePred: {α : Sort ?u.70314} → (α → Prop) → Sort (max1?u.70314)
DecidablePred 
p: β → Prop
p] (
f: α ≃ Subtype p
f : 
α: Type u
α ≃ 
Subtype: {α : Sort ?u.70326} → (α → Prop) → Sort (max1?u.70326)
Subtype 
p: β → Prop
p)

@[simp]
theorem 
extendDomain_one: ∀ {α : Type u} {β : Type v} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p), extendDomain 1 f = 1
extendDomain_one : 
extendDomain: {α' : Type ?u.70365} →
  {β' : Type ?u.70364} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'
extendDomain 
1: ?m.70369
1 
f: α ≃ Subtype p
f = 
1: ?m.70666
1 :=
  
extendDomain_refl: ∀ {α' : Type ?u.70956} {β' : Type ?u.70955} {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p),
  extendDomain (Equiv.refl α') f = Equiv.refl β'
extendDomain_refl 
f: α ≃ Subtype p
f
#align equiv.perm.extend_domain_one 
Equiv.Perm.extendDomain_one: ∀ {α : Type u} {β : Type v} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p), extendDomain 1 f = 1
Equiv.Perm.extendDomain_one

@[simp]
theorem 
extendDomain_inv: (extendDomain e f)⁻¹ = extendDomain e⁻¹ f
extendDomain_inv : (
e: Perm α
e.
extendDomain: {α' : Type ?u.71051} →
  {β' : Type ?u.71050} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'
extendDomain 
f: α ≃ Subtype p
f)⁻¹ = 
e: Perm α
e⁻¹.
extendDomain: {α' : Type ?u.71350} →
  {β' : Type ?u.71349} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'
extendDomain 
f: α ≃ Subtype p
f :=
  
rfl: ∀ {α : Sort ?u.71371} {a : α}, a = a
rfl
#align equiv.perm.extend_domain_inv 
Equiv.Perm.extendDomain_inv: ∀ {α : Type u} {β : Type v} (e : Perm α) {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p),
  (extendDomain e f)⁻¹ = extendDomain e⁻¹ f
Equiv.Perm.extendDomain_inv

@[simp]
theorem 
extendDomain_mul: ∀ {α : Type u} {β : Type v} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p) (e e' : Perm α),
  extendDomain e f * extendDomain e' f = extendDomain (e * e') f
extendDomain_mul (
e: Perm α
e 
e': Perm α
e' : 
Perm: Sort ?u.71514 → Sort (max1?u.71514)
Perm 
α: Type u
α) :
    
e: Perm α
e.
extendDomain: {α' : Type ?u.71522} →
  {β' : Type ?u.71521} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'
extendDomain 
f: α ≃ Subtype p
f * 
e': Perm α
e'.
extendDomain: {α' : Type ?u.71556} →
  {β' : Type ?u.71555} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'
extendDomain 
f: α ≃ Subtype p
f = (
e: Perm α
e * 
e': Perm α
e').
extendDomain: {α' : Type ?u.72215} →
  {β' : Type ?u.72214} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'
extendDomain 
f: α ≃ Subtype p
f :=
  
extendDomain_trans: ∀ {α' : Type ?u.72875} {β' : Type ?u.72876} {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p)
  (e e' : Perm α'), (extendDomain e f).trans (extendDomain e' f) = extendDomain (e.trans e') f
extendDomain_trans 
_: ?m.72877 ≃ Subtype ?m.72879
_ 
_: Perm ?m.72877
_ 
_: Perm ?m.72877
_
#align equiv.perm.extend_domain_mul 
Equiv.Perm.extendDomain_mul: ∀ {α : Type u} {β : Type v} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p) (e e' : Perm α),
  extendDomain e f * extendDomain e' f = extendDomain (e * e') f
Equiv.Perm.extendDomain_mul

/-- `extendDomain` as a group homomorphism -/
@[
simps: ∀ {α : Type u} {β : Type v} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p) (e : Perm α),
  ↑(extendDomainHom f) e = extendDomain e f
simps]
def 
extendDomainHom: Perm α →* Perm β
extendDomainHom : 
Perm: Sort ?u.73098 → Sort (max1?u.73098)
Perm 
α: Type u
α →* 
Perm: Sort ?u.73099 → Sort (max1?u.73099)
Perm 
β: Type v
β where
  toFun 
e: ?m.74066
e := 
extendDomain: {α' : Type ?u.74069} →
  {β' : Type ?u.74068} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'
extendDomain 
e: ?m.74066
e 
f: α ≃ Subtype p
f
  map_one' := 
extendDomain_one: ∀ {α : Type ?u.74098} {β : Type ?u.74097} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p),
  extendDomain 1 f = 1
extendDomain_one 
f: α ≃ Subtype p
f
  map_mul' 
e: ?m.74124
e 
e': ?m.74127
e' := (
extendDomain_mul: ∀ {α : Type ?u.74130} {β : Type ?u.74129} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p) (e e' : Perm α),
  extendDomain e f * extendDomain e' f = extendDomain (e * e') f
extendDomain_mul 
f: α ≃ Subtype p
f 
e: ?m.74124
e 
e': ?m.74127
e').
symm: ∀ {α : Sort ?u.74142} {a b : α}, a = b → b = a
symm
#align equiv.perm.extend_domain_hom 
Equiv.Perm.extendDomainHom: {α : Type u} → {β : Type v} → {p : β → Prop} → [inst : DecidablePred p] → α ≃ Subtype p → Perm α →* Perm β
Equiv.Perm.extendDomainHom
#align equiv.perm.extend_domain_hom_apply 
Equiv.Perm.extendDomainHom_apply: ∀ {α : Type u} {β : Type v} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p) (e : Perm α),
  ↑(extendDomainHom f) e = extendDomain e f
Equiv.Perm.extendDomainHom_apply

theorem 
extendDomainHom_injective: Function.Injective ↑(extendDomainHom f)
extendDomainHom_injective : 
Function.Injective: {α : Sort ?u.74334} → {β : Sort ?u.74333} → (α → β) → Prop
Function.Injective (
extendDomainHom: {α : Type ?u.74338} → {β : Type ?u.74337} → {p : β → Prop} → [inst : DecidablePred p] → α ≃ Subtype p → Perm α →* Perm β
extendDomainHom 
f: α ≃ Subtype p
f) :=
  (
injective_iff_map_eq_one: ∀ {F : Type ?u.75005} {G : Type ?u.75003} {H : Type ?u.75004} [inst : Group G] [inst_1 : MulOneClass H]
  [inst_2 : MonoidHomClass F G H] (f : F), Function.Injective ↑f ↔ ∀ (a : G), ↑f a = 1 → a = 1
injective_iff_map_eq_one (
extendDomainHom: {α : Type ?u.75013} → {β : Type ?u.75012} → {p : β → Prop} → [inst : DecidablePred p] → α ≃ Subtype p → Perm α →* Perm β
extendDomainHom 
f: α ≃ Subtype p
f)).
mpr: ∀ {a b : Prop}, (a ↔ b) → b → a
mpr fun 
e: ?m.75236
e 
he: ?m.75239
he =>
    
ext: ∀ {α : Sort ?u.75241} {σ τ : Perm α}, (∀ (x : α), ↑σ x = ↑τ x) → σ = τ
ext fun 
x: ?m.75250
x =>
      
f: α ≃ Subtype p
f.
injective: ∀ {α : Sort ?u.75253} {β : Sort ?u.75252} (e : α ≃ β), Function.Injective ↑e
injective (
Subtype.ext: ∀ {α : Sort ?u.75264} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext ((
extendDomain_apply_image: ∀ {α' : Type ?u.75282} {β' : Type ?u.75281} (e : Perm α') {p : β' → Prop} [inst : DecidablePred p] (f : α' ≃ Subtype p)
  (a : α'), ↑(extendDomain e f) ↑(↑f a) = ↑(↑f (↑e a))
extendDomain_apply_image 
e: ?m.75236
e 
f: α ≃ Subtype p
f 
x: ?m.75250
x).
symm: ∀ {α : Sort ?u.75296} {a b : α}, a = b → b = a
symm.
trans: ∀ {α : Sort ?u.75301} {a b c : α}, a = b → b = c → a = c
trans (
ext_iff: ∀ {α : Sort ?u.75312} {σ τ : Perm α}, σ = τ ↔ ∀ (x : α), ↑σ x = ↑τ x
ext_iff.
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp 
he: ?m.75239
he (
f: α ≃ Subtype p
f 
x: ?m.75250
x))))
#align equiv.perm.extend_domain_hom_injective 
Equiv.Perm.extendDomainHom_injective: ∀ {α : Type u} {β : Type v} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p),
  Function.Injective ↑(extendDomainHom f)
Equiv.Perm.extendDomainHom_injective

@[simp]
theorem 
extendDomain_eq_one_iff: ∀ {α : Type u} {β : Type v} {p : β → Prop} [inst : DecidablePred p] {e : Perm α} {f : α ≃ Subtype p},
  extendDomain e f = 1 ↔ e = 1
extendDomain_eq_one_iff {
e: Perm α
e : 
Perm: Sort ?u.75851 → Sort (max1?u.75851)
Perm 
α: Type u
α} {
f: α ≃ Subtype p
f : 
α: Type u
α ≃ 
Subtype: {α : Sort ?u.75856} → (α → Prop) → Sort (max1?u.75856)
Subtype 
p: β → Prop
p} : 
e: Perm α
e.
extendDomain: {α' : Type ?u.75865} →
  {β' : Type ?u.75864} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'
extendDomain 
f: α ≃ Subtype p
f = 
1: ?m.75899
1 ↔ 
e: Perm α
e = 
1: ?m.76189
1 :=
  (
injective_iff_map_eq_one': ∀ {F : Type ?u.76482} {G : Type ?u.76480} {H : Type ?u.76481} [inst : Group G] [inst_1 : MulOneClass H]
  [inst_2 : MonoidHomClass F G H] (f : F), Function.Injective ↑f ↔ ∀ (a : G), ↑f a = 1 ↔ a = 1
injective_iff_map_eq_one' (
extendDomainHom: {α : Type ?u.76490} → {β : Type ?u.76489} → {p : β → Prop} → [inst : DecidablePred p] → α ≃ Subtype p → Perm α →* Perm β
extendDomainHom 
f: α ≃ Subtype p
f)).
mp: ∀ {a b : Prop}, (a ↔ b) → a → b
mp (
extendDomainHom_injective: ∀ {α : Type ?u.76713} {β : Type ?u.76712} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p),
  Function.Injective ↑(extendDomainHom f)
extendDomainHom_injective 
f: α ≃ Subtype p
f) 
e: Perm α
e
#align equiv.perm.extend_domain_eq_one_iff 
Equiv.Perm.extendDomain_eq_one_iff: ∀ {α : Type u} {β : Type v} {p : β → Prop} [inst : DecidablePred p] {e : Perm α} {f : α ≃ Subtype p},
  extendDomain e f = 1 ↔ e = 1
Equiv.Perm.extendDomain_eq_one_iff

@[simp]
lemma 
extendDomain_pow: ∀ (n : ℕ), extendDomain (e ^ n) f = extendDomain e f ^ n
extendDomain_pow (
n: ℕ
n : 
ℕ: Type
ℕ) : (
e: Perm α
e ^ 
n: ℕ
n).
extendDomain: {α' : Type ?u.81305} →
  {β' : Type ?u.81304} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'
extendDomain 
f: α ≃ Subtype p
f = 
e: Perm α
e.
extendDomain: {α' : Type ?u.81342} →
  {β' : Type ?u.81341} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'
extendDomain 
f: α ≃ Subtype p
f ^ 
n: ℕ
n :=
map_pow: ∀ {G : Type ?u.85571} {H : Type ?u.85572} {F : Type ?u.85573} [inst : Monoid G] [inst_1 : Monoid H]
  [inst_2 : MonoidHomClass F G H] (f : F) (a : G) (n : ℕ), ↑f (a ^ n) = ↑f a ^ n
map_pow (
extendDomainHom: {α : Type ?u.85581} → {β : Type ?u.85580} → {p : β → Prop} → [inst : DecidablePred p] → α ≃ Subtype p → Perm α →* Perm β
extendDomainHom 
f: α ≃ Subtype p
f) 
_: ?m.85574
_ 
_: ℕ
_

@[simp]
lemma 
extendDomain_zpow: ∀ {α : Type u} {β : Type v} (e : Perm α) {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p) (n : ℤ),
  extendDomain (e ^ n) f = extendDomain e f ^ n
extendDomain_zpow (
n: ℤ
n : 
ℤ: Type
ℤ) : (
e: Perm α
e ^ 
n: ℤ
n).
extendDomain: {α' : Type ?u.90467} →
  {β' : Type ?u.90466} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'
extendDomain 
f: α ≃ Subtype p
f = 
e: Perm α
e.
extendDomain: {α' : Type ?u.90504} →
  {β' : Type ?u.90503} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'
extendDomain 
f: α ≃ Subtype p
f ^ 
n: ℤ
n :=
map_zpow: ∀ {G : Type ?u.94654} {H : Type ?u.94655} {F : Type ?u.94656} [inst : Group G] [inst_1 : DivisionMonoid H]
  [inst_2 : MonoidHomClass F G H] (f : F) (g : G) (n : ℤ), ↑f (g ^ n) = ↑f g ^ n
map_zpow (
extendDomainHom: {α : Type ?u.94664} → {β : Type ?u.94663} → {p : β → Prop} → [inst : DecidablePred p] → α ≃ Subtype p → Perm α →* Perm β
extendDomainHom 
f: α ≃ Subtype p
f) 
_: ?m.94657
_ 
_: ℤ
_

end ExtendDomain

section Subtype

variable {
p: α → Prop
p : 
α: Type u
α → 
Prop: Type
Prop} {
f: Perm α
f : 
Perm: Sort ?u.118942 → Sort (max1?u.118942)
Perm 
α: Type u
α}

/-- If the permutation `f` fixes the subtype `{x // p x}`, then this returns the permutation
  on `{x // p x}` induced by `f`. -/
def 
subtypePerm: (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }
subtypePerm (
f: Perm α
f : 
Perm: Sort ?u.95060 → Sort (max1?u.95060)
Perm 
α: Type u
α) (
h: ∀ (x : α), p x ↔ p (↑f x)
h : ∀ 
x: ?m.95064
x, 
p: α → Prop
p 
x: ?m.95064
x ↔ 
p: α → Prop
p (
f: Perm α
f 
x: ?m.95064
x)) : 
Perm: Sort ?u.95149 → Sort (max1?u.95149)
Perm { 
x: ?m.95153
x // 
p: α → Prop
p 
x: ?m.95153
x } where
  toFun := fun 
x: ?m.95169
x => ⟨
f: Perm α
f 
x: ?m.95169
x, (
h: ∀ (x : α), p x ↔ p (↑f x)
h 
_: α
_).
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 
x: ?m.95169
x.
2: ∀ {α : Sort ?u.95371} {p : α → Prop} (self : Subtype p), p ↑self
2⟩
  invFun := fun 
x: ?m.95378
x => ⟨
f: Perm α
f⁻¹ 
x: ?m.95378
x, (
h: ∀ (x : α), p x ↔ p (↑f x)
h (
f: Perm α
f⁻¹ 
x: ?m.95378
x)).
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 <| by
Goals accomplished! 🐙 
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

h: ∀ (x : α), p x ↔ p (↑f x)

x: { x // p x }

p (↑f (↑f⁻¹ ↑x))simpa using 
x: { x // p x }
x.
2: ∀ {α : Sort ?u.95808} {p : α → Prop} (self : Subtype p), p ↑self
2
Goals accomplished! 🐙⟩
  left_inv 
_: ?m.95689
_ := by
Goals accomplished! 🐙 
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

h: ∀ (x : α), p x ↔ p (↑f x)

x✝: { x // p x }

(fun x => { val := ↑f⁻¹ ↑x, property := (_ : p (↑f⁻¹ ↑x)) })
    ((fun x => { val := ↑f ↑x, property := (_ : p (↑f ↑x)) }) x✝) =   x✝simp only [
Perm.inv_apply_self: ∀ {α : Type ?u.95829} (f : Perm α) (x : α), ↑f⁻¹ (↑f x) = x
Perm.inv_apply_self, 
Subtype.coe_eta: ∀ {α : Sort ?u.95839} {p : α → Prop} (a : { a // p a }) (h : p ↑a), { val := ↑a, property := h } = a
Subtype.coe_eta, 
Subtype.coe_mk: ∀ {α : Sort ?u.95854} {p : α → Prop} (a : α) (h : p a), ↑{ val := a, property := h } = a
Subtype.coe_mk]
Goals accomplished! 🐙
  right_inv 
_: ?m.95695
_ := by
Goals accomplished! 🐙 
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

h: ∀ (x : α), p x ↔ p (↑f x)

x✝: { x // p x }

(fun x => { val := ↑f ↑x, property := (_ : p (↑f ↑x)) })
    ((fun x => { val := ↑f⁻¹ ↑x, property := (_ : p (↑f⁻¹ ↑x)) }) x✝) =   x✝simp only [
Perm.apply_inv_self: ∀ {α : Type ?u.95956} (f : Perm α) (x : α), ↑f (↑f⁻¹ x) = x
Perm.apply_inv_self, 
Subtype.coe_eta: ∀ {α : Sort ?u.95964} {p : α → Prop} (a : { a // p a }) (h : p ↑a), { val := ↑a, property := h } = a
Subtype.coe_eta, 
Subtype.coe_mk: ∀ {α : Sort ?u.95974} {p : α → Prop} (a : α) (h : p a), ↑{ val := a, property := h } = a
Subtype.coe_mk]
Goals accomplished! 🐙
#align equiv.perm.subtype_perm 
Equiv.Perm.subtypePerm: {α : Type u} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }
Equiv.Perm.subtypePerm

@[simp]
theorem 
subtypePerm_apply: ∀ {α : Type u} {p : α → Prop} (f : Perm α) (h : ∀ (x : α), p x ↔ p (↑f x)) (x : { x // p x }),
  ↑(subtypePerm f h) x = { val := ↑f ↑x, property := (_ : p (↑f ↑x)) }
subtypePerm_apply (
f: Perm α
f : 
Perm: Sort ?u.96450 → Sort (max1?u.96450)
Perm 
α: Type u
α) (
h: ∀ (x : α), p x ↔ p (↑f x)
h : ∀ 
x: ?m.96454
x, 
p: α → Prop
p 
x: ?m.96454
x ↔ 
p: α → Prop
p (
f: Perm α
f 
x: ?m.96454
x)) (
x: { x // p x }
x : { 
x: ?m.96542
x // 
p: α → Prop
p 
x: ?m.96542
x }) :
    
subtypePerm: {α : Type ?u.96549} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }
subtypePerm 
f: Perm α
f 
h: ∀ (x : α), p x ↔ p (↑f x)
h 
x: { x // p x }
x = ⟨
f: Perm α
f 
x: { x // p x }
x, (
h: ∀ (x : α), p x ↔ p (↑f x)
h 
_: α
_).
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 
x: { x // p x }
x.
2: ∀ {α : Sort ?u.96833} {p : α → Prop} (self : Subtype p), p ↑self
2⟩ :=
  
rfl: ∀ {α : Sort ?u.96841} {a : α}, a = a
rfl
#align equiv.perm.subtype_perm_apply 
Equiv.Perm.subtypePerm_apply: ∀ {α : Type u} {p : α → Prop} (f : Perm α) (h : ∀ (x : α), p x ↔ p (↑f x)) (x : { x // p x }),
  ↑(subtypePerm f h) x = { val := ↑f ↑x, property := (_ : p (↑f ↑x)) }
Equiv.Perm.subtypePerm_apply

@[simp]
theorem 
subtypePerm_one: ∀ {α : Type u} (p : α → Prop) (h : optParam (∀ (x : α), p x ↔ p x) (_ : ∀ (x : α), p x ↔ p x)), subtypePerm 1 h = 1
subtypePerm_one (
p: α → Prop
p : 
α: Type u
α → 
Prop: Type
Prop) (
h: optParam ?m.96913 (_ : ∀ (x : α), p x ↔ p x)
h := fun 
_: ?m.96915
_ => 
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl) : @
subtypePerm: {α : Type ?u.96925} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }
subtypePerm 
α: Type u
α 
p: α → Prop
p 
1: ?m.96928
1 
h: optParam ?m.96913 (_ : ∀ (x : α), p x ↔ p x)
h = 
1: ?m.97212
1 :=
  
rfl: ∀ {α : Sort ?u.97438} {a : α}, a = a
rfl
#align equiv.perm.subtype_perm_one 
Equiv.Perm.subtypePerm_one: ∀ {α : Type u} (p : α → Prop) (h : optParam (∀ (x : α), p x ↔ p x) (_ : ∀ (x : α), p x ↔ p x)), subtypePerm 1 h = 1
Equiv.Perm.subtypePerm_one

@[simp]
theorem 
subtypePerm_mul: ∀ {α : Type u} {p : α → Prop} (f g : Perm α) (hf : ∀ (x : α), p x ↔ p (↑f x)) (hg : ∀ (x : α), p x ↔ p (↑g x)),
  subtypePerm f hf * subtypePerm g hg = subtypePerm (f * g) (_ : ∀ (x : α), p x ↔ p (↑(f * g) x))
subtypePerm_mul (
f: Perm α
f 
g: Perm α
g : 
Perm: Sort ?u.97499 → Sort (max1?u.97499)
Perm 
α: Type u
α) (
hf: ?m.97502
hf 
hg: ∀ (x : α), p x ↔ p (↑g x)
hg) :
    (
f: Perm α
f.
subtypePerm: {α : Type ?u.97521} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }
subtypePerm 
hf: ?m.97502
hf * 
g: Perm α
g.
subtypePerm: {α : Type ?u.97534} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }
subtypePerm 
hg: ?m.97505
hg : 
Perm: Sort ?u.97510 → Sort (max1?u.97510)
Perm { 
x: ?m.97514
x // 
p: α → Prop
p 
x: ?m.97514
x }) =
      (
f: Perm α
f * 
g: Perm α
g).
subtypePerm: {α : Type ?u.98241} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }
subtypePerm fun 
_: ?m.98249
_ => (
hg: ?m.97505
hg 
_: α
_).
trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans <| 
hf: ?m.97502
hf 
_: α
_ :=
  
rfl: ∀ {α : Sort ?u.98683} {a : α}, a = a
rfl
#align equiv.perm.subtype_perm_mul 
Equiv.Perm.subtypePerm_mul: ∀ {α : Type u} {p : α → Prop} (f g : Perm α) (hf : ∀ (x : α), p x ↔ p (↑f x)) (hg : ∀ (x : α), p x ↔ p (↑g x)),
  subtypePerm f hf * subtypePerm g hg = subtypePerm (f * g) (_ : ∀ (x : α), p x ↔ p (↑(f * g) x))
Equiv.Perm.subtypePerm_mul

private theorem 
inv_aux: ∀ {α : Type u} {p : α → Prop} {f : Perm α}, (∀ (x : α), p x ↔ p (↑f x)) ↔ ∀ (x : α), p x ↔ p (↑f⁻¹ x)
inv_aux : (∀ 
x: ?m.98770
x, 
p: α → Prop
p 
x: ?m.98770
x ↔ 
p: α → Prop
p (
f: Perm α
f 
x: ?m.98770
x)) ↔ ∀ 
x: ?m.98855
x, 
p: α → Prop
p 
x: ?m.98855
x ↔ 
p: α → Prop
p (
f: Perm α
f⁻¹ 
x: ?m.98855
x) :=
  
f: Perm α
f⁻¹.
surjective: ∀ {α : Sort ?u.99003} {β : Sort ?u.99002} (e : α ≃ β), Function.Surjective ↑e
surjective.
forall: ∀ {α : Sort ?u.99009} {β : Sort ?u.99010} {f : α → β},
  Function.Surjective f → ∀ {p : β → Prop}, (∀ (y : β), p y) ↔ ∀ (x : α), p (f x)
forall.
trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans <| by
Goals accomplished! 🐙 
α: Type u

β: Type v

p: α → Prop

f: Perm α

(∀ (x : α), p (↑f⁻¹ x) ↔ p (↑f (↑f⁻¹ x))) ↔ ∀ (x : α), p x ↔ p (↑f⁻¹ x)simp_rw [
α: Type u

β: Type v

p: α → Prop

f: Perm α

(∀ (x : α), p (↑f⁻¹ x) ↔ p (↑f (↑f⁻¹ x))) ↔ ∀ (x : α), p x ↔ p (↑f⁻¹ x)
f: Perm α
f.
apply_inv_self: ∀ {α : Type ?u.99164} (f : Perm α) (x : α), ↑f (↑f⁻¹ x) = x
apply_inv_self,
α: Type u

β: Type v

p: α → Prop

f: Perm α

(∀ (x : α), p (↑f⁻¹ x) ↔ p x) ↔ ∀ (x : α), p x ↔ p (↑f⁻¹ x) 
α: Type u

β: Type v

p: α → Prop

f: Perm α

(∀ (x : α), p (↑f⁻¹ x) ↔ p (↑f (↑f⁻¹ x))) ↔ ∀ (x : α), p x ↔ p (↑f⁻¹ x)
Iff.comm: ∀ {a b : Prop}, (a ↔ b) ↔ (b ↔ a)
Iff.comm
Goals accomplished! 🐙]
Goals accomplished! 🐙

/-- See `Equiv.Perm.inv_subtypePerm`-/
theorem 
subtypePerm_inv: ∀ {α : Type u} {p : α → Prop} (f : Perm α) (hf : ∀ (x : α), p x ↔ p (↑f⁻¹ x)),
  subtypePerm f⁻¹ hf = (subtypePerm f (_ : ∀ (x : α), p x ↔ p (↑f x)))⁻¹
subtypePerm_inv (
f: Perm α
f : 
Perm: Sort ?u.99381 → Sort (max1?u.99381)
Perm 
α: Type u
α) (
hf: ∀ (x : α), p x ↔ p (↑f⁻¹ x)
hf) :
    
f: Perm α
f⁻¹.
subtypePerm: {α : Type ?u.99464} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }
subtypePerm 
hf: ?m.99384
hf = (
f: Perm α
f.
subtypePerm: {α : Type ?u.99488} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }
subtypePerm <| 
inv_aux: ∀ {α : Type ?u.99500} {p : α → Prop} {f : Perm α}, (∀ (x : α), p x ↔ p (↑f x)) ↔ ∀ (x : α), p x ↔ p (↑f⁻¹ x)
inv_aux.
2: ∀ {a b : Prop}, (a ↔ b) → b → a
2 
hf: ?m.99384
hf : 
Perm: Sort ?u.99480 → Sort (max1?u.99480)
Perm { 
x: ?m.99484
x // 
p: α → Prop
p 
x: ?m.99484
x })⁻¹ :=
  
rfl: ∀ {α : Sort ?u.99581} {a : α}, a = a
rfl
#align equiv.perm.subtype_perm_inv 
Equiv.Perm.subtypePerm_inv: ∀ {α : Type u} {p : α → Prop} (f : Perm α) (hf : ∀ (x : α), p x ↔ p (↑f⁻¹ x)),
  subtypePerm f⁻¹ hf = (subtypePerm f (_ : ∀ (x : α), p x ↔ p (↑f x)))⁻¹
Equiv.Perm.subtypePerm_inv

/-- See `Equiv.Perm.subtypePerm_inv`-/
@[simp]
theorem 
inv_subtypePerm: ∀ {α : Type u} {p : α → Prop} (f : Perm α) (hf : ∀ (x : α), p x ↔ p (↑f x)),
  (subtypePerm f hf)⁻¹ = subtypePerm f⁻¹ (_ : ∀ (x : α), p x ↔ p (↑f⁻¹ x))
inv_subtypePerm (
f: Perm α
f : 
Perm: Sort ?u.99633 → Sort (max1?u.99633)
Perm 
α: Type u
α) (
hf: ∀ (x : α), p x ↔ p (↑f x)
hf) :
    (
f: Perm α
f.
subtypePerm: {α : Type ?u.99652} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }
subtypePerm 
hf: ?m.99636
hf : 
Perm: Sort ?u.99644 → Sort (max1?u.99644)
Perm { 
x: ?m.99648
x // 
p: α → Prop
p 
x: ?m.99648
x })⁻¹ = 
f: Perm α
f⁻¹.
subtypePerm: {α : Type ?u.99796} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }
subtypePerm (
inv_aux: ∀ {α : Type ?u.99803} {p : α → Prop} {f : Perm α}, (∀ (x : α), p x ↔ p (↑f x)) ↔ ∀ (x : α), p x ↔ p (↑f⁻¹ x)
inv_aux.
1: ∀ {a b : Prop}, (a ↔ b) → a → b
1 
hf: ?m.99636
hf) :=
  
rfl: ∀ {α : Sort ?u.99837} {a : α}, a = a
rfl
#align equiv.perm.inv_subtype_perm 
Equiv.Perm.inv_subtypePerm: ∀ {α : Type u} {p : α → Prop} (f : Perm α) (hf : ∀ (x : α), p x ↔ p (↑f x)),
  (subtypePerm f hf)⁻¹ = subtypePerm f⁻¹ (_ : ∀ (x : α), p x ↔ p (↑f⁻¹ x))
Equiv.Perm.inv_subtypePerm

private theorem 
pow_aux: ∀ {α : Type u} {p : α → Prop} {f : Perm α}, (∀ (x : α), p x ↔ p (↑f x)) → ∀ {n : ℕ} (x : α), p x ↔ p (↑(f ^ n) x)
pow_aux (
hf: ∀ (x : α), p x ↔ p (↑f x)
hf : ∀ 
x: ?m.99912
x, 
p: α → Prop
p 
x: ?m.99912
x ↔ 
p: α → Prop
p (
f: Perm α
f 
x: ?m.99912
x)) : ∀ {
n: ℕ
n : 
ℕ: Type
ℕ} (
x: ?m.100000
x), 
p: α → Prop
p 
x: ?m.100000
x ↔ 
p: α → Prop
p ((
f: Perm α
f ^ 
n: ℕ
n) 
x: ?m.100000
x)
  | 
0: ℕ
0, _ => 
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
  | 
_: ℕ
_ + 1, _ => (
pow_aux: (∀ (x : α), p x ↔ p (↑f x)) → ∀ {n : ℕ} (x : α), p x ↔ p (↑(f ^ n) x)
pow_aux 
hf: ∀ (x : α), p x ↔ p (↑f x)
hf 
_: α
_).
trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
trans (
hf: ∀ (x : α), p x ↔ p (↑f x)
hf 
_: α
_)

@[simp]
theorem 
subtypePerm_pow: ∀ {α : Type u} {p : α → Prop} (f : Perm α) (n : ℕ) (hf : ∀ (x : α), p x ↔ p (↑f x)),
  subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))
subtypePerm_pow (
f: Perm α
f : 
Perm: Sort ?u.104820 → Sort (max1?u.104820)
Perm 
α: Type u
α) (
n: ℕ
n : 
ℕ: Type
ℕ) (
hf: ?m.104825
hf) :
    (
f: Perm α
f.
subtypePerm: {α : Type ?u.104841} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }
subtypePerm 
hf: ?m.104825
hf : 
Perm: Sort ?u.104833 → Sort (max1?u.104833)
Perm { 
x: ?m.104837
x // 
p: α → Prop
p 
x: ?m.104837
x }) ^ 
n: ℕ
n = (
f: Perm α
f ^ 
n: ℕ
n).
subtypePerm: {α : Type ?u.109117} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }
subtypePerm (
pow_aux: ∀ {α : Type ?u.109124} {p : α → Prop} {f : Perm α},
  (∀ (x : α), p x ↔ p (↑f x)) → ∀ {n : ℕ} (x : α), p x ↔ p (↑(f ^ n) x)
pow_aux 
hf: ?m.104825
hf) := by
Goals accomplished! 🐙
  
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

n: ℕ

hf: ∀ (x : α), p x ↔ p (↑f x)

subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))induction' 
n: ℕ
n with 
n: ℕ
n 
ih: ?m.113248 n
ih
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

hf: ∀ (x : α), p x ↔ p (↑f x)

zero
subtypePerm f hf ^ Nat.zero = subtypePerm (f ^ Nat.zero) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.zero) x))
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

hf: ∀ (x : α), p x ↔ p (↑f x)

n: ℕ

ih: subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))

succ
subtypePerm f hf ^ Nat.succ n = subtypePerm (f ^ Nat.succ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.succ n) x))
  
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

n: ℕ

hf: ∀ (x : α), p x ↔ p (↑f x)

subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))·
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

hf: ∀ (x : α), p x ↔ p (↑f x)

zero
subtypePerm f hf ^ Nat.zero = subtypePerm (f ^ Nat.zero) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.zero) x)) 
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

hf: ∀ (x : α), p x ↔ p (↑f x)

zero
subtypePerm f hf ^ Nat.zero = subtypePerm (f ^ Nat.zero) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.zero) x))
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

hf: ∀ (x : α), p x ↔ p (↑f x)

n: ℕ

ih: subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))

succ
subtypePerm f hf ^ Nat.succ n = subtypePerm (f ^ Nat.succ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.succ n) x))simp
Goals accomplished! 🐙
  
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

n: ℕ

hf: ∀ (x : α), p x ↔ p (↑f x)

subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))·
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

hf: ∀ (x : α), p x ↔ p (↑f x)

n: ℕ

ih: subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))

succ
subtypePerm f hf ^ Nat.succ n = subtypePerm (f ^ Nat.succ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.succ n) x)) 
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

hf: ∀ (x : α), p x ↔ p (↑f x)

n: ℕ

ih: subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))

succ
subtypePerm f hf ^ Nat.succ n = subtypePerm (f ^ Nat.succ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.succ n) x))simp_rw [
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

hf: ∀ (x : α), p x ↔ p (↑f x)

n: ℕ

ih: subtypePerm f hf ^ n = subtypePerm (f ^ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ n) x))

succ
subtypePerm f hf ^ Nat.succ n = subtypePerm (f ^ Nat.succ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.succ n) x))
pow_succ': ∀ {M : Type ?u.113805} [inst : Monoid M] (a : M) (n : ℕ), a ^ (n + 1) = a ^ n * a
pow_succ',
α: Type u

β: Type v

p: α → Prop

f✝, f: Perm α

hf: ∀ (x : α), p x ↔ p (↑f x)

n: ℕ

ih: subtypePerm f hf