Theorem: Equiv.Perm.IwasawaT'_isConj (Jordan/PermIwasawa.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ IwasawaT' (g • s) = MulAut.conj g • IwasawaT' s
Tactic:
ext k
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ k ∈ IwasawaT' (g • s) ↔ k ∈ MulAut.conj g • IwasawaT' s

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ k ∈ IwasawaT' (g • s) ↔ k ∈ MulAut.conj g • IwasawaT' s
Tactic:
unfold IwasawaT'
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ k ∈ fixingSubgroup (Perm α) (↑(g • s))ᶜ ↔ k ∈ MulAut.conj g • fixingSubgroup (Perm α) (↑s)ᶜ

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ k ∈ fixingSubgroup (Perm α) (↑(g • s))ᶜ ↔ k ∈ MulAut.conj g • fixingSubgroup (Perm α) (↑s)ᶜ
Tactic:
simp only [Finset.coe_smul_finset, mem_fixingSubgroup_iff,
  Subgroup.mem_pointwise_smul_iff_inv_smul_mem]
State after:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ (∀ y ∈ (g • ↑s)ᶜ, k • y = y) ↔ ∀ y ∈ (↑s)ᶜ, ((MulAut.conj g)⁻¹ • k) • y = y

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ (∀ 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_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ ∀ {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_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
⊢ ∀ {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_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
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_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
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_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
x : α
⊢ x ∈ (g • ↑s)ᶜ → k • x = x ↔ g⁻¹ • x ∈ (↑s)ᶜ → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
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_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
x : α
⊢ x ∈ (g • ↑s)ᶜ → k • x = x ↔ x ∈ g • (↑s)ᶜ → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x

State before:
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g k : Perm α
x : α
⊢ x ∈ (g • ↑s)ᶜ → k • x = x ↔ x ∈ g • (↑s)ᶜ → ((MulAut.conj g)⁻¹ • k) • g⁻¹ • x = g⁻¹ • x
Tactic:
simp only [Set.mem_compl_iff, Perm.smul_def, smul_compl_set, MulAut.smul_def,
  MulAut.conj_inv_apply, coe_mul, Function.comp_apply, apply_inv_self,
  EmbeddingLike.apply_eq_iff_eq]
State after:
no goals