@@ -49,39 +49,50 @@ theorem isConj_of_support_equiv
4949
5050end Conjugation
5151
52- theorem perm_inv_on_of_perm_on_finset {s : Finset α} {f : Perm α} (h : ∀ x ∈ s, f x ∈ s) {y : α}
53- (hy : y ∈ s) : f⁻¹ y ∈ s := by
52+ theorem perm_symm_on_of_perm_on_finset {s : Finset α} {f : Perm α} (h : ∀ x ∈ s, f x ∈ s) {y : α}
53+ (hy : y ∈ s) : f.symm y ∈ s := by
5454 have h0 : ∀ y ∈ s, ∃ (x : _) (hx : x ∈ s), y = (fun i (_ : i ∈ s) => f i) x hx :=
5555 Finset.surj_on_of_inj_on_of_card_le (fun x hx => (fun i _ => f i) x hx) (fun a ha => h a ha)
5656 (fun a₁ a₂ ha₁ ha₂ heq => (Equiv.apply_eq_iff_eq f).mp heq) rfl.ge
5757 obtain ⟨y2, hy2, rfl⟩ := h0 y hy
5858 simpa using hy2
5959
60- theorem perm_inv_mapsTo_of_mapsTo (f : Perm α) {s : Set α} [Finite s] (h : Set.MapsTo f s s) :
61- Set.MapsTo (f⁻¹ :) s s := by
60+ @[deprecated (since := "2025-11-17")]
61+ alias perm_inv_on_of_perm_on_finset := perm_symm_on_of_perm_on_finset
62+
63+ theorem perm_symm_mapsTo_of_mapsTo (f : Perm α) {s : Set α} [Finite s] (h : Set.MapsTo f s s) :
64+ Set.MapsTo f.symm s s := by
6265 cases nonempty_fintype s
6366 exact fun x hx =>
6467 Set.mem_toFinset.mp <|
65- perm_inv_on_of_perm_on_finset
68+ perm_symm_on_of_perm_on_finset
6669 (fun a ha => Set.mem_toFinset.mpr (h (Set.mem_toFinset.mp ha)))
6770 (Set.mem_toFinset.mpr hx)
6871
72+ @[deprecated (since := "2025-11-17")] alias perm_inv_mapsTo_of_mapsTo := perm_symm_mapsTo_of_mapsTo
73+
6974@[simp]
70- theorem perm_inv_mapsTo_iff_mapsTo {f : Perm α} {s : Set α} [Finite s] :
71- Set.MapsTo (f⁻¹ :) s s ↔ Set.MapsTo f s s :=
72- ⟨perm_inv_mapsTo_of_mapsTo f⁻¹, perm_inv_mapsTo_of_mapsTo f⟩
75+ theorem perm_symm_mapsTo_iff_mapsTo {f : Perm α} {s : Set α} [Finite s] :
76+ Set.MapsTo f.symm s s ↔ Set.MapsTo f s s :=
77+ ⟨perm_symm_mapsTo_of_mapsTo f⁻¹, perm_symm_mapsTo_of_mapsTo f⟩
7378
74- theorem perm_inv_on_of_perm_on_finite {f : Perm α} {p : α → Prop } [Finite { x // p x }]
75- (h : ∀ x, p x → p (f x)) {x : α} (hx : p x) : p (f⁻¹ x) := by
79+ @[deprecated (since := "2025-11-17")]
80+ alias perm_inv_mapsTo_iff_mapsTo := perm_symm_mapsTo_iff_mapsTo
81+
82+ theorem perm_symm_on_of_perm_on_finite {f : Perm α} {p : α → Prop } [Finite { x // p x }]
83+ (h : ∀ x, p x → p (f x)) {x : α} (hx : p x) : p (f.symm x) := by
7684 have : Finite { x | p x } := by simpa
77- simpa using perm_inv_mapsTo_of_mapsTo (s := {x | p x}) f h hx
85+ simpa using perm_symm_mapsTo_of_mapsTo (s := {x | p x}) f h hx
86+
87+ @[deprecated (since := "2025-11-17")]
88+ alias perm_inv_on_of_perm_on_finite := perm_symm_on_of_perm_on_finite
7889
7990/-- If the permutation `f` maps `{x // p x}` into itself, then this returns the permutation
8091 on `{x // p x}` induced by `f`. Note that the `h` hypothesis is weaker than for
8192 `Equiv.Perm.subtypePerm`. -/
8293abbrev subtypePermOfFintype (f : Perm α) {p : α → Prop } [Finite { x // p x }]
8394 (h : ∀ x, p x → p (f x)) : Perm { x // p x } :=
84- f.subtypePerm fun x => ⟨fun h₂ => f.inv_apply_self x ▸ perm_inv_on_of_perm_on_finite h h₂, h x⟩
95+ f.subtypePerm fun x => ⟨fun h₂ => f.symm_apply_apply x ▸ perm_symm_on_of_perm_on_finite h h₂, h x⟩
8596
8697@[simp]
8798theorem subtypePermOfFintype_apply (f : Perm α) {p : α → Prop } [Finite { x // p x }]
@@ -98,19 +109,17 @@ theorem perm_mapsTo_inl_iff_mapsTo_inr {m n : Type*} [Finite m] [Finite n] (σ :
98109 constructor <;>
99110 ( intro h
100111 classical
101- rw [← perm_inv_mapsTo_iff_mapsTo ] at h
112+ rw [← perm_symm_mapsTo_iff_mapsTo ] at h
102113 intro x
103114 rcases hx : σ x with l | r)
104115 · rintro ⟨a, rfl⟩
105116 obtain ⟨y, hy⟩ := h ⟨l, rfl⟩
106- rw [← hx, σ.inv_apply_self] at hy
107- exact absurd hy Sum.inl_ne_inr
117+ grind
108118 · rintro _; exact ⟨r, rfl⟩
109119 · rintro _; exact ⟨l, rfl⟩
110120 · rintro ⟨a, rfl⟩
111121 obtain ⟨y, hy⟩ := h ⟨r, rfl⟩
112- rw [← hx, σ.inv_apply_self] at hy
113- exact absurd hy Sum.inr_ne_inl
122+ grind
114123
115124theorem mem_sumCongrHom_range_of_perm_mapsTo_inl {m n : Type *} [Finite m] [Finite n]
116125 {σ : Perm (m ⊕ n)} (h : Set.MapsTo σ (Set.range Sum.inl) (Set.range Sum.inl)) :
@@ -182,11 +191,11 @@ theorem Disjoint.isConj_mul [Finite α] {σ τ π ρ : Perm α} (hc1 : IsConj σ
182191 · rw [mem_coe, mem_support] at hxσ
183192 rw [Set.union_apply_left, Set.union_apply_left]
184193 · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inl, comp_apply,
185- Set.union_symm_apply_left, Subtype.coe_mk, apply_eq_iff_eq]
194+ Set.union_symm_apply_left, Subtype.coe_mk, apply_eq_iff_eq, coe_inv ]
186195 have h := (hd2 (f x)).resolve_left ?_
187- · rw [mul_apply, mul_apply] at h
188- rw [h, inv_apply_self , (hd1 x).resolve_left hxσ]
189- · rwa [mul_apply, mul_apply, inv_apply_self , apply_eq_iff_eq]
196+ · rw [mul_apply, mul_apply, coe_inv ] at h
197+ rw [h, symm_apply_apply , (hd1 x).resolve_left hxσ]
198+ · rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply , apply_eq_iff_eq]
190199 · rwa [Subtype.coe_mk, mem_coe, mem_support]
191200 · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 x).resolve_left hxσ, mem_coe,
192201 apply_mem_support, mem_support]
@@ -195,9 +204,9 @@ theorem Disjoint.isConj_mul [Finite α] {σ τ π ρ : Perm α} (hc1 : IsConj σ
195204 · simp only [subtypeEquiv_apply, Perm.coe_mul, Sum.map_inr, comp_apply,
196205 Set.union_symm_apply_right, Subtype.coe_mk]
197206 have h := (hd2 (g (τ x))).resolve_right ?_
198- · rw [mul_apply, mul_apply] at h
199- rw [inv_apply_self , h, (hd1 (τ x)).resolve_right hxτ]
200- · rwa [mul_apply, mul_apply, inv_apply_self , apply_eq_iff_eq]
207+ · rw [mul_apply, mul_apply, coe_inv ] at h
208+ rw [coe_inv, coe_inv, symm_apply_apply , h, (hd1 (τ x)).resolve_right hxτ]
209+ · rwa [mul_apply, mul_apply, coe_inv, symm_apply_apply , apply_eq_iff_eq]
201210 · rwa [Subtype.coe_mk, mem_coe, ← apply_mem_support, mem_support]
202211 · rwa [Subtype.coe_mk, Perm.mul_apply, (hd1 (τ x)).resolve_right hxτ,
203212 mem_coe, mem_support]
0 commit comments