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

State before:
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g : G
⊢ fixingSubgroup G (g • s) = MulAut.conj g • fixingSubgroup G s
Tactic:
ext k
State after:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
⊢ k ∈ fixingSubgroup G (g • s) ↔ k ∈ MulAut.conj g • fixingSubgroup G s

State before:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
⊢ k ∈ fixingSubgroup G (g • s) ↔ k ∈ MulAut.conj g • fixingSubgroup G s
Tactic:
simp only [mem_fixingSubgroup_iff, Subgroup.mem_pointwise_smul_iff_inv_smul_mem]
State after:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
⊢ (∀ y ∈ g • s, k • y = y) ↔ ∀ y ∈ s, ((MulAut.conj g)⁻¹ • k) • y = y

State before:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
⊢ (∀ y ∈ g • s, k • y = y) ↔ ∀ y ∈ s, ((MulAut.conj g)⁻¹ • k) • y = y
Tactic:
rw [Equiv.forall_congr (toPerm g⁻¹)]
State after:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
⊢ ∀ {x : α}, x ∈ g • s → k • x = x ↔ (toPerm g⁻¹) x ∈ s → ((MulAut.conj g)⁻¹ • k) • (toPerm g⁻¹) x = (toPerm g⁻¹) x

State before:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
⊢ ∀ {x : α}, x ∈ g • s → k • x = x ↔ (toPerm g⁻¹) x ∈ s → ((MulAut.conj g)⁻¹ • k) • (toPerm g⁻¹) x = (toPerm g⁻¹) x
Tactic:
intro x
State after:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
x : α
⊢ x ∈ g • s → k • x = x ↔ (toPerm g⁻¹) x ∈ s → ((MulAut.conj g)⁻¹ • k) • (toPerm g⁻¹) x = (toPerm g⁻¹) x

State before:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
x : α
⊢ x ∈ g • s → k • x = x ↔ (toPerm g⁻¹) x ∈ s → ((MulAut.conj g)⁻¹ • k) • (toPerm g⁻¹) x = (toPerm g⁻¹) x
Tactic:
simp only [toPerm_apply]
State after:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
x : α
⊢ x ∈ g • s → k • x = x ↔ g⁻¹ • x ∈ s → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x

State before:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
x : α
⊢ x ∈ g • s → k • x = x ↔ g⁻¹ • x ∈ s → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x
Tactic:
rw [← Set.mem_smul_set_iff_inv_smul_mem]
State after:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
x : α
⊢ x ∈ g • s → k • x = x ↔ x ∈ g • s → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x

State before:
case h
α✝ : Type ?u.1776
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
g k : G
x : α
⊢ x ∈ g • s → k • x = x ↔ x ∈ g • s → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x
Tactic:
simp only [MulAut.smul_def, MulAut.conj_inv_apply, mul_smul, smul_inv_smul, smul_left_cancel_iff]
State after:
no goals