Theorem: Equiv.Perm.IwasawaT_is_conj' (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:
unfold IwasawaT
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ MonoidHom.range (Iwt (g • s)) = MulAut.conj g • MonoidHom.range (Iwt s)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ MonoidHom.range (Iwt (g • s)) = MulAut.conj g • MonoidHom.range (Iwt s)
Tactic:
unfold Iwt
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ MonoidHom.range ofSubtype = MulAut.conj g • MonoidHom.range ofSubtype

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ MonoidHom.range ofSubtype = MulAut.conj g • MonoidHom.range ofSubtype
Tactic:
simp only [Equiv.Perm.ofSubtype_range_eq]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ fixingSubgroup (Perm α) (↑(g • s))ᶜ = MulAut.conj g • fixingSubgroup (Perm α) (↑s)ᶜ

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ fixingSubgroup (Perm α) (↑(g • s))ᶜ = MulAut.conj g • fixingSubgroup (Perm α) (↑s)ᶜ
Tactic:
simp only [Finset.coe_smul_finset, ← smul_compl_set]
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ fixingSubgroup (Perm α) (g • (↑s)ᶜ) = MulAut.conj g • fixingSubgroup (Perm α) (↑s)ᶜ

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
g : Perm α
⊢ fixingSubgroup (Perm α) (g • (↑s)ᶜ) = MulAut.conj g • fixingSubgroup (Perm α) (↑s)ᶜ
Tactic:
apply Equiv.Perm.fixingSubgroup_conj
State after:
no goals