Theorem: Equiv.Perm.Equiv.Perm.ofSubtype_range_eq (Jordan/PermIwasawa.lean)

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
⊢ MonoidHom.range ofSubtype = fixingSubgroup (Perm α) sᶜ
Tactic:
ext k
State after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ k ∈ MonoidHom.range ofSubtype ↔ k ∈ fixingSubgroup (Perm α) sᶜ

State before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ k ∈ MonoidHom.range ofSubtype ↔ k ∈ fixingSubgroup (Perm α) sᶜ
Tactic:
simp only [mem_fixingSubgroup_iff, Set.mem_compl_iff, Finset.mem_coe, Perm.smul_def, Finset.coe_sort_coe,
  MonoidHom.mem_range]
State after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ (∃ x, ofSubtype x = k) ↔ ∀ y ∉ s, k y = y

State before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ (∃ x, ofSubtype x = k) ↔ ∀ y ∉ s, k y = y
Tactic:
constructor
State after:
case h.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ (∃ x, ofSubtype x = k) → ∀ y ∉ s, k y = y

case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ (∀ y ∉ s, k y = y) → ∃ x, ofSubtype x = k

State before:
case h.mp
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ (∃ x, ofSubtype x = k) → ∀ y ∉ s, k y = y
Tactic:
rintro ⟨k, rfl⟩
State after:
case h.mp.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm { x // x ∈ s }
⊢ ∀ y ∉ s, (ofSubtype k) y = y

State before:
case h.mp.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm { x // x ∈ s }
⊢ ∀ y ∉ s, (ofSubtype k) y = y
Tactic:
intro y hy
State after:
case h.mp.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm { x // x ∈ s }
y : α
hy : y ∉ s
⊢ (ofSubtype k) y = y

State before:
case h.mp.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm { x // x ∈ s }
y : α
hy : y ∉ s
⊢ (ofSubtype k) y = y
Tactic:
rw [ofSubtype_apply_of_not_mem k hy]
State after:
no goals

State before:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
⊢ (∀ y ∉ s, k y = y) → ∃ x, ofSubtype x = k
Tactic:
intro h
State after:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ ∃ x, ofSubtype x = k

State before:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
⊢ ∃ x, ofSubtype x = k
Tactic:
suffices hk' : _ by
  use Equiv.Perm.subtypePerm k hk'
  rw [Equiv.Perm.ofSubtype_subtypePerm]
  simp only [ne_eq, Finset.mem_coe]
  intro x
  rw [not_imp_comm]
  exact h x
State after:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
⊢ ∀ (x : α), x ∈ s ↔ k x ∈ s

State before:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
⊢ ∀ (x : α), x ∈ s ↔ k x ∈ s
Tactic:
intro x
State after:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
x : α
⊢ x ∈ s ↔ k x ∈ s

State before:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
x : α
⊢ x ∈ s ↔ k x ∈ s
Tactic:
rw [← Equiv.Perm.smul_def]
State after:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
x : α
⊢ x ∈ s ↔ k • x ∈ s

State before:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
x : α
⊢ x ∈ s ↔ k • x ∈ s
Tactic:
nth_rewrite 2 [hks]
State after:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
x : α
⊢ x ∈ s ↔ k • x ∈ k • s

State before:
case h.mpr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
x : α
⊢ x ∈ s ↔ k • x ∈ k • s
Tactic:
rw [Set.smul_mem_smul_set_iff]
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ s = k • s
Tactic:
apply le_antisymm
State after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ s ≤ k • s

case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ k • s ≤ s

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ s ≤ k • s

case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ k • s ≤ s
Tactic:
. intro x hx
  rw [Set.mem_smul_set_iff_inv_smul_mem, Perm.smul_def]
  by_contra hx'
  rw [← h _ hx', apply_inv_self] at hx'
  exact hx' hx
State after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ k • s ≤ s

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ s ≤ k • s
Tactic:
intro x hx
State after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
⊢ x ∈ k • s

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
⊢ x ∈ k • s
Tactic:
rw [Set.mem_smul_set_iff_inv_smul_mem, Perm.smul_def]
State after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
⊢ k⁻¹ x ∈ s

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
⊢ k⁻¹ x ∈ s
Tactic:
by_contra hx'
State after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
hx' : k⁻¹ x ∉ s
⊢ False

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
hx' : k⁻¹ x ∉ s
⊢ False
Tactic:
rw [← h _ hx', apply_inv_self] at hx'
State after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
hx' : x ∉ s
⊢ False

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
x : α
hx : x ∈ s
hx' : x ∉ s
⊢ False
Tactic:
exact hx' hx
State after:
no goals

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
⊢ k • s ≤ s
Tactic:
intro a ha
State after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
a : α
ha : a ∈ k • s
⊢ a ∈ s

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
a : α
ha : a ∈ k • s
⊢ a ∈ s
Tactic:
by_contra ha'
State after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
a : α
ha : a ∈ k • s
ha' : a ∉ s
⊢ False

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
a : α
ha : a ∈ k • s
ha' : a ∉ s
⊢ False
Tactic:
rw [← h _ ha', ← Perm.smul_def, Set.smul_mem_smul_set_iff] at ha
State after:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
a : α
ha : a ∈ s
ha' : a ∉ s
⊢ False

State before:
case a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
a : α
ha : a ∈ s
ha' : a ∉ s
⊢ False
Tactic:
exact ha' ha
State after:
no goals

State before:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
hk' : ?m.15812
⊢ ∃ x, ofSubtype x = k
Tactic:
use Equiv.Perm.subtypePerm k hk'
State after:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
⊢ ofSubtype (subtypePerm k hk') = k

State before:
case h
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
⊢ ofSubtype (subtypePerm k hk') = k
Tactic:
rw [Equiv.Perm.ofSubtype_subtypePerm]
State after:
case h.h₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
⊢ ∀ (x : α), k x ≠ x → x ∈ s

State before:
case h.h₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
⊢ ∀ (x : α), k x ≠ x → x ∈ s
Tactic:
simp only [ne_eq, Finset.mem_coe]
State after:
case h.h₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
⊢ ∀ (x : α), ¬k x = x → x ∈ s

State before:
case h.h₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
⊢ ∀ (x : α), ¬k x = x → x ∈ s
Tactic:
intro x
State after:
case h.h₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
x : α
⊢ ¬k x = x → x ∈ s

State before:
case h.h₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
x : α
⊢ ¬k x = x → x ∈ s
Tactic:
rw [not_imp_comm]
State after:
case h.h₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
x : α
⊢ x ∉ s → k x = x

State before:
case h.h₂
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
s : Set α
inst✝ : DecidablePred fun a => a ∈ s
k : Perm α
h : ∀ y ∉ s, k y = y
hks : s = k • s
hk' : ∀ (x : α), x ∈ s ↔ k x ∈ s
x : α
⊢ x ∉ s → k x = x
Tactic:
exact h x
State after:
no goals