Theorem: tendsto_uniformly_on_add_const (RMT4/deriv_inj.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
⊢ TendstoUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
Tactic:
have : Tendsto id (𝓝[≠] (0 : ℂ)) (𝓝 0) := nhdsWithin_le_nhds
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
this : Tendsto id (𝓝[≠] 0) (𝓝 0)
⊢ TendstoUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
this : Tendsto id (𝓝[≠] 0) (𝓝 0)
⊢ TendstoUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
Tactic:
have : TendstoUniformlyOn (λ (ε _ : ℂ) => ε) 0 (𝓝[≠] 0) U := this.tendstoUniformlyOn_const U
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
this✝ : Tendsto id (𝓝[≠] 0) (𝓝 0)
this : TendstoUniformlyOn (fun ε x => ε) 0 (𝓝[≠] 0) U
⊢ TendstoUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
this✝ : Tendsto id (𝓝[≠] 0) (𝓝 0)
this : TendstoUniformlyOn (fun ε x => ε) 0 (𝓝[≠] 0) U
⊢ TendstoUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
Tactic:
simpa using tendsto_uniformly_on_const.add this
State after:
no goals