Theorem: Equiv.Perm.subtypePerm_apply_pow_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
n : ℕ
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
Tactic:
revert x
State after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
⊢ ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x

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

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

State before:
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
⊢ ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ Nat.zero) { val := x, property := hx }) = (g ^ Nat.zero) x
Tactic:
intro x hx
State after:
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ Nat.zero) { val := x, property := hx }) = (g ^ Nat.zero) x

State before:
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ Nat.zero) { val := x, property := hx }) = (g ^ Nat.zero) x
Tactic:
simp only [pow_zero, Equiv.Perm.coe_one, id.def, Subtype.coe_mk]
State after:
no goals

State before:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
hrec : ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
⊢ ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ Nat.succ n) { val := x, property := hx }) = (g ^ Nat.succ n) x
Tactic:
intro x hx
State after:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
hrec : ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ Nat.succ n) { val := x, property := hx }) = (g ^ Nat.succ n) x

State before:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
hrec : ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ Nat.succ n) { val := x, property := hx }) = (g ^ Nat.succ n) x
Tactic:
simp only [pow_succ, Equiv.Perm.coe_mul, Function.comp_apply]
State after:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
hrec : ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ n) ((subtypePerm g hs) { val := x, property := hx })) = (g ^ n) (g x)

State before:
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
s : Finset α
hs : ∀ (x : α), x ∈ s ↔ g x ∈ s
n : ℕ
hrec : ∀ (x : α) (hx : x ∈ s), ↑((subtypePerm g hs ^ n) { val := x, property := hx }) = (g ^ n) x
x : α
hx : x ∈ s
⊢ ↑((subtypePerm g hs ^ n) ((subtypePerm g hs) { val := x, property := hx })) = (g ^ n) (g x)
Tactic:
apply hrec
State after:
no goals