Theorem: EqOn_zero_of_deriv_eq_zero (RMT4/has_sqrt.lean)

State before:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
⊢ EqOn f 0 U
Tactic:
apply (hf.analyticOn hU).eqOn_zero_of_preconnected_of_eventuallyEq_zero hU' hz₀
State after:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
⊢ f =ᶠ[𝓝 z₀] 0

State before:
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
⊢ f =ᶠ[𝓝 z₀] 0
Tactic:
obtain ⟨r, hr, hrU⟩ := nhds_basis_ball.mem_iff.1 (hU.mem_nhds hz₀)
State after:
case intro.intro
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
⊢ f =ᶠ[𝓝 z₀] 0

State before:
case intro.intro
z z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
⊢ f =ᶠ[𝓝 z₀] 0
Tactic:
refine eventually_nhds_iff.2 ⟨r, hr, λ z hz => ?_⟩
State after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
⊢ f z = 0 z

State before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
⊢ f z = 0 z
Tactic:
rw [Pi.zero_apply, ← hfz₀]
State after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
⊢ f z = f z₀

State before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
⊢ f z = f z₀
Tactic:
suffices h : ∀ z ∈ ball z₀ r, fderivWithin ℂ f (ball z₀ r) z = 0
  by exact (convex_ball z₀ r).is_const_of_fderivWithin_eq_zero (hf.mono hrU) h hz (mem_ball_self hr)
State after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
⊢ ∀ z ∈ ball z₀ r, fderivWithin ℂ f (ball z₀ r) z = 0

State before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
⊢ ∀ z ∈ ball z₀ r, fderivWithin ℂ f (ball z₀ r) z = 0
Tactic:
rintro w hw
State after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
⊢ fderivWithin ℂ f (ball z₀ r) w = 0

State before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
⊢ fderivWithin ℂ f (ball z₀ r) w = 0
Tactic:
have : UniqueDiffWithinAt ℂ (ball z₀ r) w := isOpen_ball.uniqueDiffWithinAt hw
State after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
this : UniqueDiffWithinAt ℂ (ball z₀ r) w
⊢ fderivWithin ℂ f (ball z₀ r) w = 0

State before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
this : UniqueDiffWithinAt ℂ (ball z₀ r) w
⊢ fderivWithin ℂ f (ball z₀ r) w = 0
Tactic:
rw [fderivWithin_eq_fderiv this (hf.differentiableAt (hU.mem_nhds (hrU hw)))]
State after:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
this : UniqueDiffWithinAt ℂ (ball z₀ r) w
⊢ fderiv ℂ f w = 0

State before:
case intro.intro
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
this : UniqueDiffWithinAt ℂ (ball z₀ r) w
⊢ fderiv ℂ f w = 0
Tactic:
ext1
State after:
case intro.intro.h
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
this : UniqueDiffWithinAt ℂ (ball z₀ r) w
⊢ (fderiv ℂ f w) 1 = 0 1

State before:
case intro.intro.h
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
w : ℂ
hw : w ∈ ball z₀ r
this : UniqueDiffWithinAt ℂ (ball z₀ r) w
⊢ (fderiv ℂ f w) 1 = 0 1
Tactic:
simpa [fderiv_deriv] using hf' (hrU hw)
State after:
no goals

State before:
z✝ z₀ : ℂ
U : Set ℂ
hU : IsOpen U
hU' : IsPreconnected U
f : ℂ → ℂ
hf : DifferentiableOn ℂ f U
hf' : EqOn (deriv f) 0 U
hz₀ : z₀ ∈ U
hfz₀ : f z₀ = 0
r : ℝ
hr : 0 < r
hrU : ball z₀ r ⊆ U
z : ℂ
hz : dist z z₀ < r
h : ∀ z ∈ ball z₀ r, fderivWithin ℂ f (ball z₀ r) z = 0
⊢ f z = f z₀
Tactic:
exact (convex_ball z₀ r).is_const_of_fderivWithin_eq_zero (hf.mono hrU) h hz (mem_ball_self hr)
State after:
no goals