Theorem: EqOn_of_EqOn_deriv (RMT4/has_sqrt.lean)

State before:
z z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
⊢ EqOn f g U
Tactic:
refine λ z hz => sub_eq_zero.1 ?_
State after:
z✝ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z : ℂ
hz : z ∈ U
⊢ f z - g z = 0

State before:
z✝ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z : ℂ
hz : z ∈ U
⊢ f z - g z = 0
Tactic:
have h2 : EqOn (deriv (λ y => f y - g y)) 0 U := by
  rintro z hz
  have e1 : U ∈ 𝓝 z := hU.mem_nhds hz
  rw [deriv_sub (hf.differentiableAt e1) (hg.differentiableAt e1), hfg hz, sub_self]
  rfl
State after:
z✝ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z : ℂ
hz : z ∈ U
h2 : EqOn (deriv fun y => f y - g y) 0 U
⊢ f z - g z = 0

State before:
z✝ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z : ℂ
hz : z ∈ U
h2 : EqOn (deriv fun y => f y - g y) 0 U
⊢ f z - g z = 0
Tactic:
exact EqOn_zero_of_deriv_eq_zero hU hU' (hf.sub hg) h2 hz₀ (by simp [hfgz₀]) hz
State after:
no goals

State before:
z✝ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z : ℂ
hz : z ∈ U
⊢ EqOn (deriv fun y => f y - g y) 0 U
Tactic:
rintro z hz
State after:
z✝¹ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z✝ : ℂ
hz✝ : z✝ ∈ U
z : ℂ
hz : z ∈ U
⊢ deriv (fun y => f y - g y) z = 0 z

State before:
z✝¹ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z✝ : ℂ
hz✝ : z✝ ∈ U
z : ℂ
hz : z ∈ U
⊢ deriv (fun y => f y - g y) z = 0 z
Tactic:
have e1 : U ∈ 𝓝 z := hU.mem_nhds hz
State after:
z✝¹ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z✝ : ℂ
hz✝ : z✝ ∈ U
z : ℂ
hz : z ∈ U
e1 : U ∈ 𝓝 z
⊢ deriv (fun y => f y - g y) z = 0 z

State before:
z✝¹ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z✝ : ℂ
hz✝ : z✝ ∈ U
z : ℂ
hz : z ∈ U
e1 : U ∈ 𝓝 z
⊢ deriv (fun y => f y - g y) z = 0 z
Tactic:
rw [deriv_sub (hf.differentiableAt e1) (hg.differentiableAt e1), hfg hz, sub_self]
State after:
z✝¹ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z✝ : ℂ
hz✝ : z✝ ∈ U
z : ℂ
hz : z ∈ U
e1 : U ∈ 𝓝 z
⊢ 0 = 0 z

State before:
z✝¹ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z✝ : ℂ
hz✝ : z✝ ∈ U
z : ℂ
hz : z ∈ U
e1 : U ∈ 𝓝 z
⊢ 0 = 0 z
Tactic:
rfl
State after:
no goals

State before:
z✝ z₀ : ℂ
U : Set ℂ
f g : ℂ → ℂ
hU : IsOpen U
hU' : IsPreconnected U
hf : DifferentiableOn ℂ f U
hg : DifferentiableOn ℂ g U
hfg : EqOn (deriv f) (deriv g) U
hz₀ : z₀ ∈ U
hfgz₀ : f z₀ = g z₀
z : ℂ
hz : z ∈ U
h2 : EqOn (deriv fun y => f y - g y) 0 U
⊢ f z₀ - g z₀ = 0
Tactic:
simp [hfgz₀]
State after:
no goals