case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
⊢ ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ Nat.zero) x = ↑(g ^ Nat.zero) x

case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
hk : ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
⊢ ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ Nat.succ k) x = ↑(g ^ Nat.succ k) x
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
⊢ ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
induction' k with k hk
no goals
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
⊢ ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ Nat.zero) x = ↑(g ^ Nat.zero) x
simp
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
hk : ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
x : α
hx : x ∈ support f ∩ support g
⊢ ↑(f ^ Nat.succ k) x = ↑(g ^ Nat.succ k) x
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
hk : ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
⊢ ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ Nat.succ k) x = ↑(g ^ Nat.succ k) x
intro x hx
case succ.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
hk : ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
x : α
hx : x ∈ support f ∩ support g
⊢ ↑g x ∈ support f ∩ support g
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
hk : ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
x : α
hx : x ∈ support f ∩ support g
⊢ ↑(f ^ Nat.succ k) x = ↑(g ^ Nat.succ k) x
rw [pow_succ', mul_apply, pow_succ', mul_apply, h _ hx, hk]
no goals
case succ.a
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
h : ∀ (x : α), x ∈ support f ∩ support g → ↑f x = ↑g x
k : ℕ
hk : ∀ (x : α), x ∈ support f ∩ support g → ↑(f ^ k) x = ↑(g ^ k) x
x : α
hx : x ∈ support f ∩ support g
⊢ ↑g x ∈ support f ∩ support g
rwa [mem_inter, apply_mem_support, ← h _ hx, apply_mem_support, ← mem_inter]