Theorem: EqOn_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
⊢ EqOn f (fun x => f z₀) U
Tactic:
set g := λ z => f z - f z₀
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
g : ℂ → ℂ := fun z => f z - f z₀
⊢ EqOn f (fun x => f z₀) U

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
g : ℂ → ℂ := fun z => f z - f z₀
⊢ EqOn f (fun x => f z₀) U
Tactic:
have h2 : EqOn (deriv g) 0 U := λ z hz => by rw [deriv_sub_const, hf' 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
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
⊢ EqOn f (fun x => f z₀) U

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
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
⊢ EqOn f (fun x => f z₀) U
Tactic:
have h3 : g z₀ = 0 := by simp [g]
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
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
h3 : g z₀ = 0
⊢ EqOn f (fun x => f z₀) U

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
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
h3 : g z₀ = 0
⊢ EqOn f (fun x => f z₀) U
Tactic:
have := EqOn_zero_of_deriv_eq_zero hU hU' (hf.sub_const _) h2 hz₀ h3
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
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
h3 : g z₀ = 0
this : EqOn (fun y => f y - f z₀) 0 U
⊢ EqOn f (fun x => f z₀) U

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
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
h3 : g z₀ = 0
this : EqOn (fun y => f y - f z₀) 0 U
⊢ EqOn f (fun x => f z₀) U
Tactic:
exact λ z hz => sub_eq_zero.1 (this hz)
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
g : ℂ → ℂ := fun z => f z - f z₀
z : ℂ
hz : z ∈ U
⊢ deriv g z = 0 z
Tactic:
rw [deriv_sub_const, hf' hz]
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
g : ℂ → ℂ := fun z => f z - f z₀
h2 : EqOn (deriv g) 0 U
⊢ g z₀ = 0
Tactic:
simp [g]
State after:
no goals