Theorem: bla (RMT4/deriv_inj.lean)

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
Tactic:
have h1 : ∀ᶠ z in 𝓝 z₀, AnalyticAt ℂ f z := (isOpen_analyticAt ℂ f).mem_nhds hf
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
Tactic:
obtain ⟨ε, hε, h⟩ := Metric.mem_nhds_iff.1 (h1.and hf'.eventually_eq_zero)
State after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀

State before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
⊢ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = f z₀
Tactic:
refine Metric.mem_nhds_iff.2 ⟨ε, hε, λ z hz => ?_⟩
State after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
⊢ z ∈ {x | (fun z => f z = f z₀) x}

State before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
⊢ z ∈ {x | (fun z => f z = f z₀) x}
Tactic:
have h3 : ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0 := by
  rintro z hz
  rw [fderivWithin_eq_fderiv (isOpen_ball.uniqueDiffWithinAt hz) ((h hz).1.differentiableAt)]
  ext1
  simpa [fderiv_deriv] using (h hz).2
State after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
h3 : ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0
⊢ z ∈ {x | (fun z => f z = f z₀) x}

State before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
h3 : ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0
⊢ z ∈ {x | (fun z => f z = f z₀) x}
Tactic:
have h4 : DifferentiableOn ℂ f (ball z₀ ε) := λ z hz => (h hz).1.differentiableWithinAt
State after:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
h3 : ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0
h4 : DifferentiableOn ℂ f (ball z₀ ε)
⊢ z ∈ {x | (fun z => f z = f z₀) x}

State before:
case intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
h3 : ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0
h4 : DifferentiableOn ℂ f (ball z₀ ε)
⊢ z ∈ {x | (fun z => f z = f z₀) x}
Tactic:
exact Convex.is_const_of_fderivWithin_eq_zero (convex_ball z₀ ε) h4 h3 hz (mem_ball_self hε)
State after:
no goals

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z : ℂ
hz : z ∈ ball z₀ ε
⊢ ∀ z ∈ ball z₀ ε, fderivWithin ℂ f (ball z₀ ε) z = 0
Tactic:
rintro z hz
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z✝ : ℂ
hz✝ : z✝ ∈ ball z₀ ε
z : ℂ
hz : z ∈ ball z₀ ε
⊢ fderivWithin ℂ f (ball z₀ ε) z = 0

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z✝ : ℂ
hz✝ : z✝ ∈ ball z₀ ε
z : ℂ
hz : z ∈ ball z₀ ε
⊢ fderivWithin ℂ f (ball z₀ ε) z = 0
Tactic:
rw [fderivWithin_eq_fderiv (isOpen_ball.uniqueDiffWithinAt hz) ((h hz).1.differentiableAt)]
State after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z✝ : ℂ
hz✝ : z✝ ∈ ball z₀ ε
z : ℂ
hz : z ∈ ball z₀ ε
⊢ fderiv ℂ f z = 0

State before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z✝ : ℂ
hz✝ : z✝ ∈ ball z₀ ε
z : ℂ
hz : z ∈ ball z₀ ε
⊢ fderiv ℂ f z = 0
Tactic:
ext1
State after:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z✝ : ℂ
hz✝ : z✝ ∈ ball z₀ ε
z : ℂ
hz : z ∈ ball z₀ ε
⊢ (fderiv ℂ f z) 1 = 0 1

State before:
case h
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r : ℝ
f g : ℂ → ℂ
hf : AnalyticAt ℂ f z₀
hf' : HasFPowerSeriesAt (deriv f) 0 z₀
h1 : ∀ᶠ (z : ℂ) in 𝓝 z₀, AnalyticAt ℂ f z
ε : ℝ
hε : ε > 0
h : ball z₀ ε ⊆ {x | (fun x => AnalyticAt ℂ f x ∧ deriv f x = 0) x}
z✝ : ℂ
hz✝ : z✝ ∈ ball z₀ ε
z : ℂ
hz : z ∈ ball z₀ ε
⊢ (fderiv ℂ f z) 1 = 0 1
Tactic:
simpa [fderiv_deriv] using (h hz).2
State after:
no goals