Theorem: nnabla_cast (PrimeNumberTheoremAnd/Wiener.lean)

State before:
n : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
u : ℝ → E
inst✝ : Sub E
⊢ nnabla u ∘ Nat.cast = nnabla (u ∘ Nat.cast)
Tactic:
ext n
State after:
case h
n✝ : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
u : ℝ → E
inst✝ : Sub E
n : ℕ
⊢ (nnabla u ∘ Nat.cast) n = nnabla (u ∘ Nat.cast) n

State before:
case h
n✝ : ℕ
A a b c d u✝¹ x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝⁴ : _root_.RCLike 𝕜
α : Type u_1
E : Type u_2
inst✝³ : OfNat α 1
inst✝² : Add α
inst✝¹ : Sub α
u✝ : α → ℂ
u : ℝ → E
inst✝ : Sub E
n : ℕ
⊢ (nnabla u ∘ Nat.cast) n = nnabla (u ∘ Nat.cast) n
Tactic:
simp [nnabla]
State after:
no goals