Theorem: Function.support_deriv_subset_Icc (PrimeNumberTheoremAnd/MellinCalculus.lean)

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
⊢ support (deriv f) ⊆ Icc a b
Tactic:
have := support_deriv_subset (f := fun x ↦ f x)
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
this : support (deriv fun x => f x) ⊆ tsupport fun x => f x
⊢ support (deriv f) ⊆ Icc a b

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
this : support (deriv fun x => f x) ⊆ tsupport fun x => f x
⊢ support (deriv f) ⊆ Icc a b
Tactic:
dsimp [tsupport] at this
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
this : support (deriv fun x => f x) ⊆ closure (support fun x => f x)
⊢ support (deriv f) ⊆ Icc a b

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
this : support (deriv fun x => f x) ⊆ closure (support fun x => f x)
⊢ support (deriv f) ⊆ Icc a b
Tactic:
have := subset_trans this <| closure_mono fSupp
State after:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
this✝ : support (deriv fun x => f x) ⊆ closure (support fun x => f x)
this : support (deriv fun x => f x) ⊆ closure (Icc a b)
⊢ support (deriv f) ⊆ Icc a b

State before:
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
a b : ℝ
f : ℝ → 𝕂
fSupp : support f ⊆ Icc a b
this✝ : support (deriv fun x => f x) ⊆ closure (support fun x => f x)
this : support (deriv fun x => f x) ⊆ closure (Icc a b)
⊢ support (deriv f) ⊆ Icc a b
Tactic:
rwa [closure_Icc] at this
State after:
no goals