internlm/Lean-Github huggingface dataset:
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case h.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
e1 : z ≠ z₀
e2 : deriv (fun z => g z + ε) z ≠ 0
⊢ (cindex z₀ r fun z => g z + ε) = 1
Tactic:
refine crucial hU h20 hz (h18 ε) hgz e2 (λ w hw hwz => ?_)
Proof state after:
case h.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
e1 : z ≠ z₀
e2 : deriv (fun z => g z + ε) z ≠ 0
w : ℂ
hw : w ∈ closedBall z₀ r
hwz : w ≠ z
⊢ g w + ε ≠ 0
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case h.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
e1 : z ≠ z₀
e2 : deriv (fun z => g z + ε) z ≠ 0
w : ℂ
hw : w ∈ closedBall z₀ r
hwz : w ≠ z
⊢ g w + ε ≠ 0
Tactic:
contrapose! hwz
Proof state after:
case h.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
e1 : z ≠ z₀
e2 : deriv (fun z => g z + ε) z ≠ 0
w : ℂ
hw : w ∈ closedBall z₀ r
hwz : g w + ε = 0
⊢ w = z
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
case h.intro.intro
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
e1 : z ≠ z₀
e2 : deriv (fun z => g z + ε) z ≠ 0
w : ℂ
hw : w ∈ closedBall z₀ r
hwz : g w + ε = 0
⊢ w = z
Tactic:
exact hi (h20 hw) ((ball_subset_closedBall.trans h20) hz) (add_right_cancel (hwz.trans hgz.symm))
Proof state after:
no goals
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
⊢ FormalMultilinearSeries.order p ≠ 0
Tactic:
linarith
Proof state after:
no goals
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
⊢ cindex z₀ r g ≠ 0
Tactic:
simp [h8, h24]
Proof state after:
no goals
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
⊢ z ≠ z₀
Tactic:
rintro rfl
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
p : FormalMultilinearSeries ℂ ℂ ℂ
h17 : p ≠ 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
ε : ℂ
hε : ε ∈ {0}ᶜ
z : ℂ
hgz : g z + ε = 0
hz₀ : z ∈ U
hgz₀ : g z = 0
hp : HasFPowerSeriesAt g p z
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z, g z ≠ 0
h✝ : deriv g z = 0
h8 : cindex z r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → deriv g z_1 ≠ 0
h21 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → g z_1 ≠ 0
h20 : closedBall z r ⊆ U
h22 : ∀ z_1 ∈ sphere z r, g z_1 ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + x = 0
h : ε ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + ε = 0
hz : z ∈ ball z r
⊢ False
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
p : FormalMultilinearSeries ℂ ℂ ℂ
h17 : p ≠ 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
ε : ℂ
hε : ε ∈ {0}ᶜ
z : ℂ
hgz : g z + ε = 0
hz₀ : z ∈ U
hgz₀ : g z = 0
hp : HasFPowerSeriesAt g p z
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z, g z ≠ 0
h✝ : deriv g z = 0
h8 : cindex z r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → deriv g z_1 ≠ 0
h21 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → g z_1 ≠ 0
h20 : closedBall z r ⊆ U
h22 : ∀ z_1 ∈ sphere z r, g z_1 ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + x = 0
h : ε ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + ε = 0
hz : z ∈ ball z r
⊢ False
Tactic:
rw [hgz₀, zero_add] at hgz
Proof state after:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
p : FormalMultilinearSeries ℂ ℂ ℂ
h17 : p ≠ 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
ε : ℂ
hε : ε ∈ {0}ᶜ
z : ℂ
hgz : ε = 0
hz₀ : z ∈ U
hgz₀ : g z = 0
hp : HasFPowerSeriesAt g p z
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z, g z ≠ 0
h✝ : deriv g z = 0
h8 : cindex z r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → deriv g z_1 ≠ 0
h21 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → g z_1 ≠ 0
h20 : closedBall z r ⊆ U
h22 : ∀ z_1 ∈ sphere z r, g z_1 ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + x = 0
h : ε ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + ε = 0
hz : z ∈ ball z r
⊢ False
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
p : FormalMultilinearSeries ℂ ℂ ℂ
h17 : p ≠ 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
ε : ℂ
hε : ε ∈ {0}ᶜ
z : ℂ
hgz : ε = 0
hz₀ : z ∈ U
hgz₀ : g z = 0
hp : HasFPowerSeriesAt g p z
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z, g z ≠ 0
h✝ : deriv g z = 0
h8 : cindex z r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → deriv g z_1 ≠ 0
h21 : ∀ z_1 ∈ closedBall z r, z_1 ≠ z → g z_1 ≠ 0
h20 : closedBall z r ⊆ U
h22 : ∀ z_1 ∈ sphere z r, g z_1 ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + x = 0
h : ε ∈ {0}ᶜ → ∃ z_1 ∈ ball z r, g z_1 + ε = 0
hz : z ∈ ball z r
⊢ False
Tactic:
exact hε hgz
Proof state after:
no goals
Theorem: deriv_ne_zero_of_inj_aux
Proof state before:
ι : Type u_1
α : Type u_2
β : Type u_3
U : Set ℂ
c z₀ : ℂ
r✝ : ℝ
f g✝ g : ℂ → ℂ
hU : IsOpen U
hg : DifferentiableOn ℂ g U
hi : InjOn g U
hz₀ : z₀ ∈ U
hgz₀ : g z₀ = 0
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt g p z₀
h25 : ∀ᶠ (z : ℂ) in 𝓝[≠] z₀, g z ≠ 0
h17 : p ≠ 0
h✝ : deriv g z₀ = 0
h6 : 2 ≤ FormalMultilinearSeries.order p
r : ℝ
h7 : r > 0
h8 : cindex z₀ r g = ↑(FormalMultilinearSeries.order p)
h14 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → deriv g z ≠ 0
h21 : ∀ z ∈ closedBall z₀ r, z ≠ z₀ → g z ≠ 0
h20 : closedBall z₀ r ⊆ U
h22 : ∀ z ∈ sphere z₀ r, g z ≠ 0
h18 : ∀ (ε : ℂ), DifferentiableOn ℂ (fun z => g z + ε) U
h19 : TendstoLocallyUniformlyOn (fun ε z => g z + ε) g (𝓝[≠] 0) U
h24 : FormalMultilinearSeries.order p ≠ 0
this : ∀ᶠ (x : ℂ) in 𝓝 0, x ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + x = 0
ε : ℂ
h : ε ∈ {0}ᶜ → ∃ z ∈ ball z₀ r, g z + ε = 0
hε : ε ∈ {0}ᶜ
z : ℂ
hz : z ∈ ball z₀ r
hgz : g z + ε = 0
e1 : z ≠ z₀
⊢ deriv (fun z => g z + ε) z ≠ 0
Tactic:
simpa using h14 z (ball_subset_closedBall hz) e1
Proof state after:
no goals
Theorem: deriv_ne_zero_of_inj
Proof 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)
Proof 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
Theorem: deriv_ne_zero_of_inj
Proof 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 _)
Proof state after:
no goals
Theorem: tendsto_𝓒_iff
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
F : ι → 𝓒 U
f : 𝓒 U
⊢ Tendsto F l (𝓝 f) ↔ TendstoLocallyUniformlyOn F f l U
Tactic:
simp [UniformOnFun.tendsto_iff_tendstoUniformlyOn, _root_.compacts]
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
F : ι → 𝓒 U
f : 𝓒 U
⊢ (∀ s ⊆ U,
      IsCompact s →
        TendstoUniformlyOn (⇑(UniformOnFun.toFun {K | K ⊆ U ∧ IsCompact K}) ∘ F)
          ((UniformOnFun.toFun {K | K ⊆ U ∧ IsCompact K}) f) l s) ↔
    TendstoLocallyUniformlyOn F f l U
Theorem: tendsto_𝓒_iff
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
F : ι → 𝓒 U
f : 𝓒 U
⊢ (∀ s ⊆ U,
      IsCompact s →
        TendstoUniformlyOn (⇑(UniformOnFun.toFun {K | K ⊆ U ∧ IsCompact K}) ∘ F)
          ((UniformOnFun.toFun {K | K ⊆ U ∧ IsCompact K}) f) l s) ↔
    TendstoLocallyUniformlyOn F f l U
Tactic:
exact (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).symm
Proof state after:
no goals
Theorem: isClosed_𝓗
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed (𝓗 U)
Tactic:
refine isClosed_iff_clusterPt.2 (λ f hf => ?_)
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ f ∈ 𝓗 U
Theorem: isClosed_𝓗
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ f ∈ 𝓗 U
Tactic:
refine @TendstoLocallyUniformlyOn.differentiableOn _ _ _ _ _ _ _ id f hf ?_ ?_ hU
Proof state after:
case refine_1
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ TendstoLocallyUniformlyOn id f (𝓝 f ⊓ 𝓟 (𝓗 U)) U

case refine_2
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ ∀ᶠ (n : ℂ → ℂ) in 𝓝 f ⊓ 𝓟 (𝓗 U), DifferentiableOn ℂ (id n) U
Theorem: isClosed_𝓗
Proof state before:
case refine_1
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ TendstoLocallyUniformlyOn id f (𝓝 f ⊓ 𝓟 (𝓗 U)) U
Tactic:
simp [← tendsto_𝓒_iff hU, Tendsto]
Proof state after:
no goals
Theorem: isClosed_𝓗
Proof state before:
case refine_2
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ ∀ᶠ (n : ℂ → ℂ) in 𝓝 f ⊓ 𝓟 (𝓗 U), DifferentiableOn ℂ (id n) U
Tactic:
simp [eventually_inf_principal, 𝓗]
Proof state after:
case refine_2
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ ∀ᶠ (x : ℂ → ℂ) in 𝓝 f, x ∈ {f | DifferentiableOn ℂ f U} → DifferentiableOn ℂ x U
Theorem: isClosed_𝓗
Proof state before:
case refine_2
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
hf : ClusterPt f (𝓟 (𝓗 U))
⊢ ∀ᶠ (x : ℂ → ℂ) in 𝓝 f, x ∈ {f | DifferentiableOn ℂ f U} → DifferentiableOn ℂ x U
Tactic:
exact eventually_of_forall (λ g => id)
Proof state after:
no goals
Theorem: ContinuousOn_uderiv
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ ContinuousOn uderiv (𝓗 U)
Tactic:
rintro f -
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ ContinuousWithinAt uderiv (𝓗 U) f
Theorem: ContinuousOn_uderiv
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ ContinuousWithinAt uderiv (𝓗 U) f
Tactic:
refine (tendsto_𝓒_iff hU).2 ?_
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ TendstoLocallyUniformlyOn uderiv (uderiv f) (𝓝[𝓗 U] f) U
Theorem: ContinuousOn_uderiv
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ TendstoLocallyUniformlyOn uderiv (uderiv f) (𝓝[𝓗 U] f) U
Tactic:
refine TendstoLocallyUniformlyOn.deriv ?_ eventually_mem_nhdsWithin hU
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ TendstoLocallyUniformlyOn (fun f => f) f (𝓝[𝓗 U] f) U
Theorem: ContinuousOn_uderiv
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ TendstoLocallyUniformlyOn (fun f => f) f (𝓝[𝓗 U] f) U
Tactic:
apply (tendsto_𝓒_iff hU).1
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ Tendsto (fun f => f) (𝓝[𝓗 U] f) (𝓝 f)
Theorem: ContinuousOn_uderiv
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
f : 𝓒 U
⊢ Tendsto (fun f => f) (𝓝[𝓗 U] f) (𝓝 f)
Tactic:
exact nhdsWithin_le_nhds
Proof state after:
no goals
Theorem: 𝓑_const
Proof state before:
U : Set ℂ
Q✝ : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
Q : Set ℂ
⊢ (𝓑 U fun x => Q) = {f | f ∈ 𝓗 U ∧ MapsTo f U Q}
Tactic:
simp [𝓑, ← mapsTo_sUnion]
Proof state after:
no goals
Theorem: isClosed_𝓑
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed (𝓑 U Q)
Tactic:
rw [𝓑, setOf_and]
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed ({a | a ∈ 𝓗 U} ∩ {a | ∀ K ∈ compacts U, MapsTo a K (Q K)})
Theorem: isClosed_𝓑
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed ({a | a ∈ 𝓗 U} ∩ {a | ∀ K ∈ compacts U, MapsTo a K (Q K)})
Tactic:
apply (isClosed_𝓗 hU).inter
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed {a | ∀ K ∈ compacts U, MapsTo a K (Q K)}
Theorem: isClosed_𝓑
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed {a | ∀ K ∈ compacts U, MapsTo a K (Q K)}
Tactic:
simp only [setOf_forall, MapsTo]
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed (⋂ i ∈ compacts U, ⋂ i_1 ∈ i, {x | x i_1 ∈ Q i})
Theorem: isClosed_𝓑
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ IsClosed (⋂ i ∈ compacts U, ⋂ i_1 ∈ i, {x | x i_1 ∈ Q i})
Tactic:
apply isClosed_biInter
Proof state after:
case h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ ∀ i ∈ compacts U, IsClosed (⋂ i_1 ∈ i, {x | x i_1 ∈ Q i})
Theorem: isClosed_𝓑
Proof state before:
case h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
⊢ ∀ i ∈ compacts U, IsClosed (⋂ i_1 ∈ i, {x | x i_1 ∈ Q i})
Tactic:
intro K hK
Proof state after:
case h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
⊢ IsClosed (⋂ i ∈ K, {x | x i ∈ Q K})
Theorem: isClosed_𝓑
Proof state before:
case h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
⊢ IsClosed (⋂ i ∈ K, {x | x i ∈ Q K})
Tactic:
apply isClosed_biInter
Proof state after:
case h.h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
⊢ ∀ i ∈ K, IsClosed {x | x i ∈ Q K}
Theorem: isClosed_𝓑
Proof state before:
case h.h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
⊢ ∀ i ∈ K, IsClosed {x | x i ∈ Q K}
Tactic:
intro z hz
Proof state after:
case h.h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
⊢ IsClosed {x | x z ∈ Q K}
Theorem: isClosed_𝓑
Proof state before:
case h.h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
⊢ IsClosed {x | x z ∈ Q K}
Tactic:
apply (hQ K hK).isClosed.preimage
Proof state after:
case h.h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
⊢ Continuous fun x => x z
Theorem: isClosed_𝓑
Proof state before:
case h.h
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
hQ : ∀ K ∈ compacts U, IsCompact (Q K)
K : Set ℂ
hK : K ∈ compacts U
z : ℂ
hz : z ∈ K
⊢ Continuous fun x => x z
Tactic:
exact ((UniformOnFun.uniformContinuous_eval_of_mem ℂ (compacts U)
  (mem_singleton z) ⟨singleton_subset_iff.2 (hK.1 hz), isCompact_singleton⟩).continuous)
Proof state after:
no goals
Theorem: IsClosed_𝓜
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed (𝓜 U)
Tactic:
suffices h : IsClosed {f : 𝓒 U | MapsTo f U (closedBall 0 1)} by
  exact (isClosed_𝓗 hU).inter h
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed {f | MapsTo f U (closedBall 0 1)}
Theorem: IsClosed_𝓜
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed {f | MapsTo f U (closedBall 0 1)}
Tactic:
simp_rw [MapsTo, setOf_forall]
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed (⋂ i ∈ U, {x | x i ∈ closedBall 0 1})
Theorem: IsClosed_𝓜
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
⊢ IsClosed (⋂ i ∈ U, {x | x i ∈ closedBall 0 1})
Tactic:
refine isClosed_biInter (λ z hz => isClosed_ball.preimage ?_)
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
z : ℂ
hz : z ∈ U
⊢ Continuous fun x => x z
Theorem: IsClosed_𝓜
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
z : ℂ
hz : z ∈ U
⊢ Continuous fun x => x z
Tactic:
exact ((UniformOnFun.uniformContinuous_eval_of_mem ℂ (compacts U)
  (mem_singleton z) ⟨singleton_subset_iff.2 hz, isCompact_singleton⟩).continuous)
Proof state after:
no goals