Theorem: deriv_ne_zero_of_inj (RMT4/deriv_inj.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f✝ g f : ℂ → ℂ
hU : IsOpen U
hf : DifferentiableOn ℂ f U
hi : InjOn f U
hz₀ : z₀ ∈ U
⊢ deriv f z₀ ≠ 0
Tactic:
have : InjOn (λ z => f z - f z₀) U := λ z₁ hz₁ z₂ hz₂ h => hi hz₁ hz₂ (sub_left_inj.1 h)
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f✝ g f : ℂ → ℂ
hU : IsOpen U
hf : DifferentiableOn ℂ f U
hi : InjOn f U
hz₀ : z₀ ∈ U
this : InjOn (fun z => f z - f z₀) U
⊢ deriv f z₀ ≠ 0

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f✝ g f : ℂ → ℂ
hU : IsOpen U
hf : DifferentiableOn ℂ f U
hi : InjOn f U
hz₀ : z₀ ∈ U
this : InjOn (fun z => f z - f z₀) U
⊢ deriv f z₀ ≠ 0
Tactic:
simpa [deriv_sub_const] using deriv_ne_zero_of_inj_aux hU (hf.sub_const _) this hz₀ (sub_self _)
State after:
no goals