Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Leonardo de Moura, Mario Carneiro

! This file was ported from Lean 3 source module 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.10Group (Perm: Sort ?u.11 → Sort (max1?u.11)Perm α: Type uα) where
mul f: ?m.29f g: ?m.32g := Equiv.trans: {α : Sort ?u.36} → {β : Sort ?u.35} → {γ : Sort ?u.34} → α ≃ β → β ≃ γ → α ≃ γEquiv.trans g: ?m.32g f: ?m.29f
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.49f g: ?m.52g h: ?m.55h := (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 = asymm
one_mul := trans_refl: ∀ {α : Sort ?u.98} {β : Sort ?u.97} (e : α ≃ β), e.trans (Equiv.refl β) = etrans_refl
mul_one := refl_trans: ∀ {α : Sort ?u.105} {β : Sort ?u.104} (e : α ≃ β), (Equiv.refl α).trans e = erefl_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 = 1default_eq : (default: {α : Sort ?u.1070} → [self : Inhabited α] → αdefault : Perm: Sort ?u.1069 → Sort (max1?u.1069)Perm α: Type uα) = 1: ?m.12281 :=
rfl: ∀ {α : Sort ?u.1517} {a : α}, a = arfl
#align equiv.perm.default_eq Equiv.Perm.default_eq: ∀ {α : Type u}, default = 1Equiv.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 asimps]
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.1538Units (Function.End: Type ?u.1539 → Type ?u.1539Function.End α: Type uα) where
-- Porting note: needed to add `.toFun`.
toFun e: ?m.2160e := ⟨e: ?m.2160e.toFun: {α : Sort ?u.2197} → {β : Sort ?u.2196} → α ≃ β → α → βtoFun, e: ?m.2160e.symm: {α : Sort ?u.2202} → {β : Sort ?u.2201} → α ≃ β → β ≃ αsymm.toFun: {α : Sort ?u.2206} → {β : Sort ?u.2205} → α ≃ β → α → βtoFun, e: ?m.2160e.self_comp_symm: ∀ {α : Sort ?u.2211} {β : Sort ?u.2210} (e : α ≃ β), ↑e ∘ ↑e.symm = idself_comp_symm, e: ?m.2160e.symm_comp_self: ∀ {α : Sort ?u.2228} {β : Sort ?u.2227} (e : α ≃ β), ↑e.symm ∘ ↑e = idsymm_comp_self⟩
invFun u: ?m.2237u :=
⟨(u: ?m.2237u : Function.End: Type ?u.2250 → Type ?u.2250Function.End α: Type uα), (↑u: ?m.2237u⁻¹ : Function.End: Type ?u.3453 → Type ?u.3453Function.End α: Type uα), congr_fun: ∀ {α : Sort ?u.4648} {β : α → Sort ?u.4647} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g acongr_fun u: ?m.2237u.inv_val: ∀ {α : Type ?u.4661} [inst : Monoid α] (self : αˣ), self.inv * ↑self = 1inv_val, congr_fun: ∀ {α : Sort ?u.4670} {β : α → Sort ?u.4669} {f g : (x : α) → β x}, f = g → ∀ (a : α), f a = g acongr_fun u: ?m.2237u.val_inv: ∀ {α : Type ?u.4681} [inst : Monoid α] (self : αˣ), ↑self * self.inv = 1val_inv⟩
left_inv _: ?m.4693_ := ext: ∀ {α : Sort ?u.4695} {σ τ : Perm α}, (∀ (x : α), ↑σ x = ↑τ x) → σ = τext fun _: ?m.4704_ => rfl: ∀ {α : Sort ?u.4706} {a : α}, a = arfl
right_inv _: ?m.4715_ := Units.ext: ∀ {α : Type ?u.4717} [inst : Monoid α], Function.Injective Units.valUnits.ext rfl: ∀ {α : Sort ?u.4747} {a : α}, a = arfl
map_mul' _: ?m.4752_ _: ?m.4755_ := rfl: ∀ {α : Sort ?u.4757} {a : α}, a = arfl
#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) = ↑uEquiv.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.5515G : Type _: Type (?u.5515+1)Type _} [Group: Type ?u.5518 → Type ?u.5518Group G: Type ?u.5515G] (f: G →* Function.End αf : G: Type ?u.5515G →* Function.End: Type ?u.5523 → Type ?u.5523Function.End α: Type uα) : G: Type ?u.5515G →* 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 ≃* Msymm.toMonoidHom: {M : Type ?u.6811} → {N : Type ?u.6810} → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M ≃* N → M →* NtoMonoidHom.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 →* Pcomp 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 aMonoidHom.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.7731x = f: Perm αf (g: Perm αg x: ?m.7731x) :=
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 = xone_apply (x: ?m.8625x) : (1: ?m.86321 : Perm: Sort ?u.8630 → Sort (max1?u.8630)Perm α: Type uα) x: ?m.8625x = x: ?m.8625x :=
rfl: ∀ {α : Sort ?u.8989} {a : α}, a = arfl
#align equiv.perm.one_apply Equiv.Perm.one_apply: ∀ {α : Type u} (x : α), ↑1 x = xEquiv.Perm.one_apply

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

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

theorem one_def: 1 = Equiv.refl αone_def : (1: ?m.95501 : 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 = arfl
#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 fmul_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 = arfl
#align equiv.perm.mul_def Equiv.Perm.mul_def: ∀ {α : Type u} (f g : Perm α), f * g = g.trans fEquiv.Perm.mul_def

theorem inv_def: ∀ {α : Type u} (f : Perm α), f⁻¹ = f.symminv_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 = arfl
#align equiv.perm.inv_def Equiv.Perm.inv_def: ∀ {α : Type u} (f : Perm α), f⁻¹ = f.symmEquiv.Perm.inv_def

@[simp, norm_cast] lemma coe_one: ∀ {α : Type u}, ↑1 = idcoe_one : ⇑(1: ?m.106281 : Perm: Sort ?u.10626 → Sort (max1?u.10626)Perm α: Type uα) = id: {α : Sort ?u.10982} → α → αid := rfl: ∀ {α : Sort ?u.11021} {a : α}, a = arfl
#align equiv.perm.coe_one Equiv.Perm.coe_one: ∀ {α : Type u}, ↑1 = idEquiv.Perm.coe_one
@[simp, norm_cast] lemma coe_mul: ∀ {α : Type u} (f g : Perm α), ↑(f * g) = ↑f ∘ ↑gcoe_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 = arfl
#align equiv.perm.coe_mul Equiv.Perm.coe_mul: ∀ {α : Type u} (f g : Perm α), ↑(f * g) = ↑f ∘ ↑gEquiv.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 = arfl (fun _: ?m.17041_ _: ?m.17044_ ↦ rfl: ∀ {α : Sort ?u.17046} {a : α}, a = arfl) _: ?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 = asymm
#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 = yeq_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 = xeq_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 = yEquiv.Perm.eq_inv_iff_eq

theorem inv_eq_iff_eq: ∀ {α : Type u} {f : Perm α} {x y : α}, ↑f⁻¹ x = y ↔ x = ↑f yinv_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 ysymm_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 yEquiv.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) := byGoals 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 ^ izpow_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 ⁻¹' simage_inv (f: Perm αf : Perm: Sort ?u.39319 → Sort (max1?u.39319)Perm α: Type uα) (s: Set αs : Set: Type ?u.39322 → Type ?u.39322Set α: 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 ⁻¹' simage_eq_preimage _: Set ?m.39575_
#align equiv.perm.image_inv Equiv.Perm.image_inv: ∀ {α : Type u} (f : Perm α) (s : Set α), ↑f⁻¹ '' s = ↑f ⁻¹' sEquiv.Perm.image_inv
@[simp] lemma preimage_inv: ∀ {α : Type u} (f : Perm α) (s : Set α), ↑f⁻¹ ⁻¹' s = ↑f '' spreimage_inv (f: Perm αf : Perm: Sort ?u.39627 → Sort (max1?u.39627)Perm α: Type uα) (s: Set αs : Set: Type ?u.39630 → Type ?u.39630Set α: 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 ⁻¹' simage_eq_preimage _: Set ?m.39880_).symm: ∀ {α : Sort ?u.39885} {a b : α}, a = b → b = asymm
#align equiv.perm.preimage_inv Equiv.Perm.preimage_inv: ∀ {α : Type u} (f : Perm α) (s : Set α), ↑f⁻¹ ⁻¹' s = ↑f '' sEquiv.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 = etrans_one {α: Sort u_1α : Sort _: Type ?u.39942SortSort _: 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.399691 : 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 β) = eEquiv.trans_refl e: α ≃ βe
#align equiv.perm.trans_one Equiv.Perm.trans_one: ∀ {α : Sort u_1} {β : Type u_2} (e : α ≃ β), e.trans 1 = eEquiv.Perm.trans_one

@[simp]
theorem mul_refl: ∀ {α : Type u} (e : Perm α), e * Equiv.refl α = emul_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 β) = eEquiv.trans_refl e: Perm αe
#align equiv.perm.mul_refl Equiv.Perm.mul_refl: ∀ {α : Type u} (e : Perm α), e * Equiv.refl α = eEquiv.Perm.mul_refl

@[simp]
theorem one_symm: ∀ {α : Type u}, 1.symm = 1one_symm : (1: ?m.410101 : Perm: Sort ?u.41008 → Sort (max1?u.41008)Perm α: Type uα).symm: {α : Sort ?u.41286} → {β : Sort ?u.41285} → α ≃ β → β ≃ αsymm = 1: ?m.412951 :=
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 = 1Equiv.Perm.one_symm

@[simp]
theorem refl_inv: ∀ {α : Type u}, (Equiv.refl α)⁻¹ = 1refl_inv : (Equiv.refl: (α : Sort ?u.41550) → α ≃ αEquiv.refl α: Type uα : Perm: Sort ?u.41549 → Sort (max1?u.41549)Perm α: Type uα)⁻¹ = 1: ?m.416261 :=
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 α)⁻¹ = 1Equiv.Perm.refl_inv

@[simp]
theorem one_trans: ∀ {α : Type u_1} {β : Sort u_2} (e : α ≃ β), 1.trans e = eone_trans {α: Type u_1α : Type _: Type (?u.41921+1)Type _} {β: Sort ?u.41924β : Sort _: Type ?u.41924SortSort _: Type ?u.41924 _} (e: α ≃ βe : α: Type ?u.41921α ≃ β: Sort ?u.41924β) : (1: ?m.419351 : 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 = eEquiv.refl_trans e: α ≃ βe
#align equiv.perm.one_trans Equiv.Perm.one_trans: ∀ {α : Type u_1} {β : Sort u_2} (e : α ≃ β), 1.trans e = eEquiv.Perm.one_trans

@[simp]
theorem refl_mul: ∀ {α : Type u} (e : Perm α), Equiv.refl α * e = erefl_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 = eEquiv.refl_trans e: Perm αe
#align equiv.perm.refl_mul Equiv.Perm.refl_mul: ∀ {α : Type u} (e : Perm α), Equiv.refl α * e = eEquiv.Perm.refl_mul

@[simp]
theorem inv_trans_self: ∀ (e : Perm α), e⁻¹.trans e = 1inv_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.430811 :=
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 = 1Equiv.Perm.inv_trans_self

@[simp]
theorem mul_symm: ∀ {α : Type u} (e : Perm α), e * e.symm = 1mul_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.434071 :=
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 = 1Equiv.Perm.mul_symm

@[simp]
theorem self_trans_inv: ∀ {α : Type u} (e : Perm α), e.trans e⁻¹ = 1self_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.444461 :=
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⁻¹ = 1Equiv.Perm.self_trans_inv

@[simp]
theorem symm_mul: ∀ {α : Type u} (e : Perm α), e.symm * e = 1symm_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.447691 :=
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 = 1Equiv.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.symmsumCongr_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 = 1sumCongr_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.476061 : Perm: Sort ?u.47604 → Sort (max1?u.47604)Perm α: Type ?u.47592α) (1: ?m.478841 : Perm: Sort ?u.47882 → Sort (max1?u.47882)Perm β: Type ?u.47595β) = 1: ?m.481601 :=
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 = 1Equiv.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.sndsimps]
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.50561a := sumCongr: {α : Type ?u.50564} → {β : Type ?u.50563} → Perm α → Perm β → Perm (α ⊕ β)sumCongr a: ?m.50561a.1: {α : Type ?u.50570} → {β : Type ?u.50569} → α × β → α1 a: ?m.50561a.2: {α : Type ?u.50577} → {β : Type ?u.50576} → α × β → β2
map_one' := sumCongr_one: ∀ {α : Type ?u.50583} {β : Type ?u.50584}, sumCongr 1 1 = 1sumCongr_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 = asymm
#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.sndEquiv.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} → (α → β) → PropFunction.Injective (sumCongrHom: (α : Type ?u.51442) → (β : Type ?u.51441) → Perm α × Perm β →* Perm (α ⊕ β)sumCongrHom α: Type ?u.51431α β: Type ?u.51434β) := byGoals accomplished! 🐙
α✝: Type uβ✝: Type vα: Type u_1β: Type u_2Function.Injective ↑(sumCongrHom α β)rintro ⟨⟩: Perm α × Perm β⟨⟩ ⟨⟩: Perm α × Perm β⟨⟩ h: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)hα✝: Type uβ✝: Type vα: Type u_1β: Type u_2fst✝¹: 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_2Function.Injective ↑(sumCongrHom α β)rw [α✝: Type uβ✝: Type vα: Type u_1β: Type u_2fst✝¹: 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_2fst✝¹: Perm αsnd✝¹: Perm βfst✝: Perm αsnd✝: Perm βh: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)mk.mkfst✝¹ = fst✝ ∧ snd✝¹ = snd✝]α✝: Type uβ✝: Type vα: Type u_1β: Type u_2fst✝¹: Perm αsnd✝¹: Perm βfst✝: Perm αsnd✝: Perm βh: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)mk.mkfst✝¹ = fst✝ ∧ snd✝¹ = snd✝
α✝: Type uβ✝: Type vα: Type u_1β: Type u_2Function.Injective ↑(sumCongrHom α β)constructorα✝: Type uβ✝: Type vα: Type u_1β: Type u_2fst✝¹: Perm αsnd✝¹: Perm βfst✝: Perm αsnd✝: Perm βh: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)mk.mk.leftfst✝¹ = fst✝α✝: Type uβ✝: Type vα: Type u_1β: Type u_2fst✝¹: Perm αsnd✝¹: Perm βfst✝: Perm αsnd✝: Perm βh: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)mk.mk.rightsnd✝¹ = snd✝ α✝: Type uβ✝: Type vα: Type u_1β: Type u_2fst✝¹: Perm αsnd✝¹: Perm βfst✝: Perm αsnd✝: Perm βh: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)mk.mkfst✝¹ = fst✝ ∧ snd✝¹ = snd✝<;>α✝: Type uβ✝: Type vα: Type u_1β: Type u_2fst✝¹: Perm αsnd✝¹: Perm βfst✝: Perm αsnd✝: Perm βh: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)mk.mk.leftfst✝¹ = fst✝α✝: Type uβ✝: Type vα: Type u_1β: Type u_2fst✝¹: Perm αsnd✝¹: Perm βfst✝: Perm αsnd✝: Perm βh: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)mk.mk.rightsnd✝¹ = snd✝ α✝: Type uβ✝: Type vα: Type u_1β: Type u_2fst✝¹: Perm αsnd✝¹: Perm βfst✝: Perm αsnd✝: Perm βh: ↑(sumCongrHom α β) (fst✝¹, snd✝¹) = ↑(sumCongrHom α β) (fst✝, snd✝)mk.mkfst✝¹ = fst✝ ∧ snd✝¹ = snd✝ext i: ?αiα✝: Type uβ✝: Type vα: Type u_1β: Type u_2fst✝¹: 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_2Function.Injective ↑(sumCongrHom α β)·α✝: Type uβ✝: Type vα: Type u_1β: Type u_2fst✝¹: 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_2fst✝¹: 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_2fst✝¹: 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 xEquiv.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_2Function.Injective ↑(sumCongrHom α β)·α✝: Type uβ✝: Type vα: Type u_1β: Type u_2fst✝¹: 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_2fst✝¹: 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 xEquiv.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.535621 : 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.546291 : 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.55671a, Perm: Sort ?u.55674 → Sort (max1?u.55674)Perm (β: α → Type ?u.55667β a: ?m.55671a))
(G: (a : α) → Perm (β a)G : ∀ a: ?m.55679a, Perm: Sort ?u.55682 → Sort (max1?u.55682)Perm (β: α → Type ?u.55667β a: ?m.55679a)) : 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.57375a, Perm: Sort ?u.57378 → Sort (max1?u.57378)Perm (β: α → Type ?u.57371β a: ?m.57375a)) :
(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.57479a => (F: (a : α) → Perm (β a)F a: ?m.57479a)⁻¹ :=
sigmaCongrRight_symm: ∀ {α : Type ?u.57593} {β : α → Type ?u.57594} (F : (a : α) → Perm (β a)),
(sigmaCongrRight F).symm = sigmaCongrRight fun a => (F a).symmsigmaCongrRight_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 = 1sigmaCongrRight_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.576781 : ∀ a: ?m.57673a, Equiv.Perm: Sort ?u.57676 → Sort (max1?u.57676)Equiv.Perm <| β: α → Type ?u.57663β a: ?m.57673a) = 1: ?m.583671 :=
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 = 1Equiv.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 Fsimps]
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.58715a, Perm: Sort ?u.58718 → Sort (max1?u.58718)Perm (β: α → Type ?u.58709β a: ?m.58715a)) →* Perm: Sort ?u.58720 → Sort (max1?u.58720)Perm (Σa: ?m.58725a, β: α → Type ?u.58709β a: ?m.58725a) 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 = 1sigmaCongrRight_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 = asymm
#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 FEquiv.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} → (α → β) → PropFunction.Injective (sigmaCongrRightHom: {α : Type ?u.62003} → (β : α → Type ?u.62002) → ((a : α) → Perm (β a)) →* Perm ((a : α) × β a)sigmaCongrRightHom β: α → Type ?u.61995β) := byGoals accomplished! 🐙
α✝: Type uβ✝: Type vα: Type u_1β: α → Type u_2Function.Injective ↑(sigmaCongrRightHom β)intro x: (a : α) → Perm (β a)x y: (a : α) → Perm (β a)y h: ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) yhα✝: Type uβ✝: Type vα: Type u_1β: α → Type u_2x, y: (a : α) → Perm (β a)h: ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) yx = y
α✝: Type uβ✝: Type vα: Type u_1β: α → Type u_2Function.Injective ↑(sigmaCongrRightHom β)ext (a: ?αa b: ?αb)α✝: Type uβ✝: Type vα: Type u_1β: α → Type u_2x, y: (a : α) → Perm (β a)h: ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) ya: αb: β ah.H↑(x a) b = ↑(y a) b
α✝: Type uβ✝: Type vα: Type u_1β: α → Type u_2Function.Injective ↑(sigmaCongrRightHom β)simpa using Equiv.congr_fun: ∀ {α : Sort ?u.62856} {β : Sort ?u.62855} {f g : α ≃ β}, f = g → ∀ (x : α), ↑f x = ↑g xEquiv.congr_fun h: ↑(sigmaCongrRightHom β) x = ↑(sigmaCongrRightHom β) yh ⟨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.sndsimps]
def subtypeCongrHom: {α : Type u} → (p : α → Prop) → [inst : DecidablePred p] → Perm { a // p a } × Perm { a // ¬p a } →* Perm αsubtypeCongrHom (p: α → Propp : α: Type uα → Prop: TypeProp) [DecidablePred: {α : Sort ?u.63569} → (α → Prop) → Sort (max1?u.63569)DecidablePred p: α → Propp] :
Perm: Sort ?u.63583 → Sort (max1?u.63583)Perm { a: ?m.63587a // p: α → Propp a: ?m.63587a } × Perm: Sort ?u.63591 → Sort (max1?u.63591)Perm { a: ?m.63595a // ¬p: α → Propp a: ?m.63595a } →* Perm: Sort ?u.63599 → Sort (max1?u.63599)Perm α: Type uα where
toFun pair: ?m.65490pair := Perm.subtypeCongr: {ε : Type ?u.65492} → {p : ε → Prop} → [inst : DecidablePred p] → Perm { a // p a } → Perm { a // ¬p a } → Perm εPerm.subtypeCongr pair: ?m.65490pair.fst: {α : Type ?u.65616} → {β : Type ?u.65615} → α × β → αfst pair: ?m.65490pair.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 = asymm
#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.sndEquiv.Perm.subtypeCongrHom_apply

theorem subtypeCongrHom_injective: ∀ (p : α → Prop) [inst : DecidablePred p], Function.Injective ↑(subtypeCongrHom p)subtypeCongrHom_injective (p: α → Propp : α: Type uα → Prop: TypeProp) [DecidablePred: {α : Sort ?u.66145} → (α → Prop) → Sort (max1?u.66145)DecidablePred p: α → Propp] :
Function.Injective: {α : Sort ?u.66156} → {β : Sort ?u.66155} → (α → β) → PropFunction.Injective (subtypeCongrHom: {α : Type ?u.66159} → (p : α → Prop) → [inst : DecidablePred p] → Perm { a // p a } × Perm { a // ¬p a } →* Perm αsubtypeCongrHom p: α → Propp) := byGoals accomplished! 🐙
α: Type uβ: Type vp: α → Propinst✝: DecidablePred pFunction.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 vp: α → Propinst✝: DecidablePred pfst✝¹: 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 vp: α → Propinst✝: DecidablePred pFunction.Injective ↑(subtypeCongrHom p)rw [α: Type uβ: Type vp: α → Propinst✝: DecidablePred pfst✝¹: 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 vp: α → Propinst✝: DecidablePred pfst✝¹: 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.mkfst✝¹ = fst✝ ∧ snd✝¹ = snd✝]α: Type uβ: Type vp: α → Propinst✝: DecidablePred pfst✝¹: 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.mkfst✝¹ = fst✝ ∧ snd✝¹ = snd✝
α: Type uβ: Type vp: α → Propinst✝: DecidablePred pFunction.Injective ↑(subtypeCongrHom p)constructorα: Type uβ: Type vp: α → Propinst✝: DecidablePred pfst✝¹: 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.leftfst✝¹ = fst✝α: Type uβ: Type vp: α → Propinst✝: DecidablePred pfst✝¹: 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.rightsnd✝¹ = snd✝ α: Type uβ: Type vp: α → Propinst✝: DecidablePred pfst✝¹: 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.mkfst✝¹ = fst✝ ∧ snd✝¹ = snd✝<;>α: Type uβ: Type vp: α → Propinst✝: DecidablePred pfst✝¹: 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.leftfst✝¹ = fst✝α: Type uβ: Type vp: α → Propinst✝: DecidablePred pfst✝¹: 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.rightsnd✝¹ = snd✝ α: Type uβ: Type vp: α → Propinst✝: DecidablePred pfst✝¹: 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.mkfst✝¹ = fst✝ ∧ snd✝¹ = snd✝ext i: ?αiα: Type uβ: Type vp: α → Propinst✝: DecidablePred pfst✝¹: 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 vp: α → Propinst✝: DecidablePred pfst✝¹: 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.mkfst✝¹ = fst✝ ∧ snd✝¹ = snd✝<;>α: Type uβ: Type vp: α → Propinst✝: DecidablePred pfst✝¹: 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 vp: α → Propinst✝: DecidablePred pfst✝¹: 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 vp: α → Propinst✝: DecidablePred pfst✝¹: 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.mkfst✝¹ = fst✝ ∧ snd✝¹ = snd✝simpa using Equiv.congr_fun: ∀ {α : Sort ?u.67034} {β : Sort ?u.67033} {f g : α ≃ β}, f = g → ∀ (x : α), ↑f x = ↑g xEquiv.congr_fun h: ↑(subtypeCongrHom p) (fst✝¹, snd✝¹) = ↑(subtypeCongrHom p) (fst✝, snd✝)h i: ?αiGoals 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 = arfl
#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: β → Propp : β: Type vβ → Prop: TypeProp} [DecidablePred: {α : Sort ?u.70314} → (α → Prop) → Sort (max1?u.70314)DecidablePred p: β → Propp] (f: α ≃ Subtype pf : α: Type uα ≃ Subtype: {α : Sort ?u.70326} → (α → Prop) → Sort (max1?u.70326)Subtype p: β → Propp)

@[simp]
theorem extendDomain_one: ∀ {α : Type u} {β : Type v} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p), extendDomain 1 f = 1extendDomain_one : extendDomain: {α' : Type ?u.70365} →
{β' : Type ?u.70364} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'extendDomain 1: ?m.703691 f: α ≃ Subtype pf = 1: ?m.706661 :=
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 pf
#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 = 1Equiv.Perm.extendDomain_one

@[simp]
theorem extendDomain_inv: (extendDomain e f)⁻¹ = extendDomain e⁻¹ fextendDomain_inv : (e: Perm αe.extendDomain: {α' : Type ?u.71051} →
{β' : Type ?u.71050} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'extendDomain f: α ≃ Subtype pf)⁻¹ = e: Perm αe⁻¹.extendDomain: {α' : Type ?u.71350} →
{β' : Type ?u.71349} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'extendDomain f: α ≃ Subtype pf :=
rfl: ∀ {α : Sort ?u.71371} {a : α}, a = arfl
#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⁻¹ fEquiv.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') fextendDomain_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 pf * e': Perm αe'.extendDomain: {α' : Type ?u.71556} →
{β' : Type ?u.71555} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'extendDomain f: α ≃ Subtype pf = (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 pf :=
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') fextendDomain_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') fEquiv.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 fsimps]
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.74066e := extendDomain: {α' : Type ?u.74069} →
{β' : Type ?u.74068} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'extendDomain e: ?m.74066e f: α ≃ Subtype pf
map_one' := extendDomain_one: ∀ {α : Type ?u.74098} {β : Type ?u.74097} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p),
extendDomain 1 f = 1extendDomain_one f: α ≃ Subtype pf
map_mul' e: ?m.74124e e': ?m.74127e' := (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') fextendDomain_mul f: α ≃ Subtype pf e: ?m.74124e e': ?m.74127e').symm: ∀ {α : Sort ?u.74142} {a b : α}, a = b → b = asymm
#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 fEquiv.Perm.extendDomainHom_apply

theorem extendDomainHom_injective: Function.Injective ↑(extendDomainHom f)extendDomainHom_injective : Function.Injective: {α : Sort ?u.74334} → {β : Sort ?u.74333} → (α → β) → PropFunction.Injective (extendDomainHom: {α : Type ?u.74338} → {β : Type ?u.74337} → {p : β → Prop} → [inst : DecidablePred p] → α ≃ Subtype p → Perm α →* Perm βextendDomainHom f: α ≃ Subtype pf) :=
(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 = 1injective_iff_map_eq_one (extendDomainHom: {α : Type ?u.75013} → {β : Type ?u.75012} → {p : β → Prop} → [inst : DecidablePred p] → α ≃ Subtype p → Perm α →* Perm βextendDomainHom f: α ≃ Subtype pf)).mpr: ∀ {a b : Prop}, (a ↔ b) → b → ampr fun e: ?m.75236e he: ?m.75239he =>
ext: ∀ {α : Sort ?u.75241} {σ τ : Perm α}, (∀ (x : α), ↑σ x = ↑τ x) → σ = τext fun x: ?m.75250x =>
f: α ≃ Subtype pf.injective: ∀ {α : Sort ?u.75253} {β : Sort ?u.75252} (e : α ≃ β), Function.Injective ↑einjective (Subtype.ext: ∀ {α : Sort ?u.75264} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2Subtype.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.75236e f: α ≃ Subtype pf x: ?m.75250x).symm: ∀ {α : Sort ?u.75296} {a b : α}, a = b → b = asymm.trans: ∀ {α : Sort ?u.75301} {a b c : α}, a = b → b = c → a = ctrans (ext_iff: ∀ {α : Sort ?u.75312} {σ τ : Perm α}, σ = τ ↔ ∀ (x : α), ↑σ x = ↑τ xext_iff.mp: ∀ {a b : Prop}, (a ↔ b) → a → bmp he: ?m.75239he (f: α ≃ Subtype pf x: ?m.75250x))))
#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 = 1extendDomain_eq_one_iff {e: Perm αe : Perm: Sort ?u.75851 → Sort (max1?u.75851)Perm α: Type uα} {f: α ≃ Subtype pf : α: Type uα ≃ Subtype: {α : Sort ?u.75856} → (α → Prop) → Sort (max1?u.75856)Subtype p: β → Propp} : e: Perm αe.extendDomain: {α' : Type ?u.75865} →
{β' : Type ?u.75864} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'extendDomain f: α ≃ Subtype pf = 1: ?m.758991 ↔ e: Perm αe = 1: ?m.761891 :=
(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 = 1injective_iff_map_eq_one' (extendDomainHom: {α : Type ?u.76490} → {β : Type ?u.76489} → {p : β → Prop} → [inst : DecidablePred p] → α ≃ Subtype p → Perm α →* Perm βextendDomainHom f: α ≃ Subtype pf)).mp: ∀ {a b : Prop}, (a ↔ b) → a → bmp (extendDomainHom_injective: ∀ {α : Type ?u.76713} {β : Type ?u.76712} {p : β → Prop} [inst : DecidablePred p] (f : α ≃ Subtype p),
Function.Injective ↑(extendDomainHom f)extendDomainHom_injective f: α ≃ Subtype pf) 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 = 1Equiv.Perm.extendDomain_eq_one_iff

@[simp]
lemma extendDomain_pow: ∀ (n : ℕ), extendDomain (e ^ n) f = extendDomain e f ^ nextendDomain_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 pf = e: Perm αe.extendDomain: {α' : Type ?u.81342} →
{β' : Type ?u.81341} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'extendDomain f: α ≃ Subtype pf ^ 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 ^ nmap_pow (extendDomainHom: {α : Type ?u.85581} → {β : Type ?u.85580} → {p : β → Prop} → [inst : DecidablePred p] → α ≃ Subtype p → Perm α →* Perm βextendDomainHom f: α ≃ Subtype pf) _: ?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 ^ nextendDomain_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 pf = e: Perm αe.extendDomain: {α' : Type ?u.90504} →
{β' : Type ?u.90503} → Perm α' → {p : β' → Prop} → [inst : DecidablePred p] → α' ≃ Subtype p → Perm β'extendDomain f: α ≃ Subtype pf ^ 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 ^ nmap_zpow (extendDomainHom: {α : Type ?u.94664} → {β : Type ?u.94663} → {p : β → Prop} → [inst : DecidablePred p] → α ≃ Subtype p → Perm α →* Perm βextendDomainHom f: α ≃ Subtype pf) _: ?m.94657_ _: ℤ_

end ExtendDomain

section Subtype

variable {p: α → Propp : α: Type uα → Prop: TypeProp} {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.95064x, p: α → Propp x: ?m.95064x ↔ p: α → Propp (f: Perm αf x: ?m.95064x)) : Perm: Sort ?u.95149 → Sort (max1?u.95149)Perm { x: ?m.95153x // p: α → Propp x: ?m.95153x } where
toFun := fun x: ?m.95169x => ⟨f: Perm αf x: ?m.95169x, (h: ∀ (x : α), p x ↔ p (↑f x)h _: α_).1: ∀ {a b : Prop}, (a ↔ b) → a → b1 x: ?m.95169x.2: ∀ {α : Sort ?u.95371} {p : α → Prop} (self : Subtype p), p ↑self2⟩
invFun := fun x: ?m.95378x => ⟨f: Perm αf⁻¹ x: ?m.95378x, (h: ∀ (x : α), p x ↔ p (↑f x)h (f: Perm αf⁻¹ x: ?m.95378x)).2: ∀ {a b : Prop}, (a ↔ b) → b → a2 <| byGoals accomplished! 🐙 α: Type uβ: Type vp: α → Propf✝, 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 ↑self2Goals accomplished! 🐙⟩
left_inv _: ?m.95689_ := byGoals accomplished! 🐙 α: Type uβ: Type vp: α → Propf✝, 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) = xPerm.inv_apply_self, Subtype.coe_eta: ∀ {α : Sort ?u.95839} {p : α → Prop} (a : { a // p a }) (h : p ↑a), { val := ↑a, property := h } = aSubtype.coe_eta, Subtype.coe_mk: ∀ {α : Sort ?u.95854} {p : α → Prop} (a : α) (h : p a), ↑{ val := a, property := h } = aSubtype.coe_mk]Goals accomplished! 🐙
right_inv _: ?m.95695_ := byGoals accomplished! 🐙 α: Type uβ: Type vp: α → Propf✝, 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) = xPerm.apply_inv_self, Subtype.coe_eta: ∀ {α : Sort ?u.95964} {p : α → Prop} (a : { a // p a }) (h : p ↑a), { val := ↑a, property := h } = aSubtype.coe_eta, Subtype.coe_mk: ∀ {α : Sort ?u.95974} {p : α → Prop} (a : α) (h : p a), ↑{ val := a, property := h } = aSubtype.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.96454x, p: α → Propp x: ?m.96454x ↔ p: α → Propp (f: Perm αf x: ?m.96454x)) (x: { x // p x }x : { x: ?m.96542x // p: α → Propp x: ?m.96542x }) :
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 → b1 x: { x // p x }x.2: ∀ {α : Sort ?u.96833} {p : α → Prop} (self : Subtype p), p ↑self2⟩ :=
rfl: ∀ {α : Sort ?u.96841} {a : α}, a = arfl
#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 = 1subtypePerm_one (p: α → Propp : α: Type uα → Prop: TypeProp) (h: optParam ?m.96913 (_ : ∀ (x : α), p x ↔ p x)h := fun _: ?m.96915_ => Iff.rfl: ∀ {a : Prop}, a ↔ aIff.rfl) : @subtypePerm: {α : Type ?u.96925} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }subtypePerm α: Type uα p: α → Propp 1: ?m.969281 h: optParam ?m.96913 (_ : ∀ (x : α), p x ↔ p x)h = 1: ?m.972121 :=
rfl: ∀ {α : Sort ?u.97438} {a : α}, a = arfl
#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 = 1Equiv.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.97502hf 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.97502hf * g: Perm αg.subtypePerm: {α : Type ?u.97534} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }subtypePerm hg: ?m.97505hg : Perm: Sort ?u.97510 → Sort (max1?u.97510)Perm { x: ?m.97514x // p: α → Propp x: ?m.97514x }) =
(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.97505hg _: α_).trans: ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)trans <| hf: ?m.97502hf _: α_ :=
rfl: ∀ {α : Sort ?u.98683} {a : α}, a = arfl
#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.98770x, p: α → Propp x: ?m.98770x ↔ p: α → Propp (f: Perm αf x: ?m.98770x)) ↔ ∀ x: ?m.98855x, p: α → Propp x: ?m.98855x ↔ p: α → Propp (f: Perm αf⁻¹ x: ?m.98855x) :=
f: Perm αf⁻¹.surjective: ∀ {α : Sort ?u.99003} {β : Sort ?u.99002} (e : α ≃ β), Function.Surjective ↑esurjective.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 <| byGoals accomplished! 🐙 α: Type uβ: Type vp: α → Propf: Perm α(∀ (x : α), p (↑f⁻¹ x) ↔ p (↑f (↑f⁻¹ x))) ↔ ∀ (x : α), p x ↔ p (↑f⁻¹ x)simp_rw [α: Type uβ: Type vp: α → Propf: 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) = xapply_inv_self,α: Type uβ: Type vp: α → Propf: Perm α(∀ (x : α), p (↑f⁻¹ x) ↔ p x) ↔ ∀ (x : α), p x ↔ p (↑f⁻¹ x) α: Type uβ: Type vp: α → Propf: 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.commGoals 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.99384hf = (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 → a2 hf: ?m.99384hf : Perm: Sort ?u.99480 → Sort (max1?u.99480)Perm { x: ?m.99484x // p: α → Propp x: ?m.99484x })⁻¹ :=
rfl: ∀ {α : Sort ?u.99581} {a : α}, a = arfl
#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.99636hf : Perm: Sort ?u.99644 → Sort (max1?u.99644)Perm { x: ?m.99648x // p: α → Propp x: ?m.99648x })⁻¹ = 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 → b1 hf: ?m.99636hf) :=
rfl: ∀ {α : Sort ?u.99837} {a : α}, a = arfl
#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.99912x, p: α → Propp x: ?m.99912x ↔ p: α → Propp (f: Perm αf x: ?m.99912x)) : ∀ {n: ℕn : ℕ: Typeℕ} (x: ?m.100000x), p: α → Propp x: ?m.100000x ↔ p: α → Propp ((f: Perm αf ^ n: ℕn) x: ?m.100000x)
| 0: ℕ0, _ => Iff.rfl: ∀ {a : Prop}, a ↔ aIff.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.104825hf) :
(f: Perm αf.subtypePerm: {α : Type ?u.104841} → {p : α → Prop} → (f : Perm α) → (∀ (x : α), p x ↔ p (↑f x)) → Perm { x // p x }subtypePerm hf: ?m.104825hf : Perm: Sort ?u.104833 → Sort (max1?u.104833)Perm { x: ?m.104837x // p: α → Propp x: ?m.104837x }) ^ 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.104825hf) := byGoals accomplished! 🐙
α: Type uβ: Type vp: α → Propf✝, 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 nihα: Type uβ: Type vp: α → Propf✝, f: Perm αhf: ∀ (x : α), p x ↔ p (↑f x)zerosubtypePerm f hf ^ Nat.zero = subtypePerm (f ^ Nat.zero) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.zero) x))α: Type uβ: Type vp: α → Propf✝, 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))succsubtypePerm f hf ^ Nat.succ n = subtypePerm (f ^ Nat.succ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.succ n) x))
α: Type uβ: Type vp: α → Propf✝, 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 vp: α → Propf✝, f: Perm αhf: ∀ (x : α), p x ↔ p (↑f x)zerosubtypePerm f hf ^ Nat.zero = subtypePerm (f ^ Nat.zero) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.zero) x)) α: Type uβ: Type vp: α → Propf✝, f: Perm αhf: ∀ (x : α), p x ↔ p (↑f x)zerosubtypePerm f hf ^ Nat.zero = subtypePerm (f ^ Nat.zero) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.zero) x))α: Type uβ: Type vp: α → Propf✝, 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))succsubtypePerm f hf ^ Nat.succ n = subtypePerm (f ^ Nat.succ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.succ n) x))simpGoals accomplished! 🐙
α: Type uβ: Type vp: α → Propf✝, 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 vp: α → Propf✝, 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))succsubtypePerm f hf ^ Nat.succ n = subtypePerm (f ^ Nat.succ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.succ n) x)) α: Type uβ: Type vp: α → Propf✝, 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))succsubtypePerm f hf ^ Nat.succ n = subtypePerm (f ^ Nat.succ n) (_ : ∀ (x : α), p x ↔ p (↑(f ^ Nat.succ n) x))simp_rw [α: Type uβ: Type vp: α → Propf✝, 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))succsubtypePerm 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 * apow_succ',α: Type uβ: Type vp: α → Propf✝, f: Perm αhf: ∀ (x : α), p x ↔ p (↑f x)n: ℕih: subtypePerm f hf ```