Theorem: Equiv.Perm.subtypePerm_apply_zpow_of_mem (Jordan/ConjClassCount.lean)

State before:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
i : ℤ
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ i) { val := x, property := hx }) = (g ^ i) x
Tactic:
induction' i with i i
State after:
case ofNat
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ Int.ofNat i) { val := x, property := hx }) = (g ^ Int.ofNat i) x

case negSucc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ Int.negSucc i) { val := x, property := hx }) = (g ^ Int.negSucc i) x

State before:
case ofNat
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ Int.ofNat i) { val := x, property := hx }) = (g ^ Int.ofNat i) x

case negSucc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ Int.negSucc i) { val := x, property := hx }) = (g ^ Int.negSucc i) x
Tactic:
apply Equiv.Perm.subtypePerm_apply_pow_of_mem
State after:
case negSucc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ Int.negSucc i) { val := x, property := hx }) = (g ^ Int.negSucc i) x

State before:
case negSucc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ Int.negSucc i) { val := x, property := hx }) = (g ^ Int.negSucc i) x
Tactic:
simp only [zpow_negSucc]
State after:
case negSucc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) = (g ^ (i + 1))⁻¹ x

State before:
case negSucc
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) = (g ^ (i + 1))⁻¹ x
Tactic:
apply Equiv.injective (g ^ (i + 1))
State after:
case negSucc.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ (g ^ (i + 1)) ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) = (g ^ (i + 1)) ((g ^ (i + 1))⁻¹ x)

State before:
case negSucc.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ (g ^ (i + 1)) ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) = (g ^ (i + 1)) ((g ^ (i + 1))⁻¹ x)
Tactic:
simp only [Equiv.Perm.apply_inv_self]
State after:
case negSucc.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ (g ^ (i + 1)) ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) = x

State before:
case negSucc.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ (g ^ (i + 1)) ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) = x
Tactic:
rw [← Equiv.Perm.subtypePerm_apply_pow_of_mem g s hs]
State after:
case negSucc.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))
        { val := ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }), property := ?negSucc.a.hx }) =
    x

case negSucc.a.hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) ∈ s

State before:
case negSucc.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))
        { val := ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }), property := ?negSucc.a.hx }) =
    x

case negSucc.a.hx
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) ∈ s
Tactic:
rw [Finset.mk_coe, Equiv.Perm.apply_inv_self, Subtype.coe_mk]
State after:
case negSucc.a.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) ∈ ↑s

State before:
case negSucc.a.h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
i : ℕ
⊢ ↑((subtypePerm g hs ^ (i + 1))⁻¹ { val := x, property := hx }) ∈ ↑s
Tactic:
apply Finset.coe_mem
State after:
no goals