internlm/Lean-Github huggingface dataset:
Theorem: IsClosed_𝓜
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
hU : IsOpen U
h : IsClosed {f | MapsTo f U (closedBall 0 1)}
⊢ IsClosed (𝓜 U)
Tactic:
exact (isClosed_𝓗 hU).inter h
Proof state after:
no goals
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
⊢ Set.Nonempty (𝓘 U)
Tactic:
obtain ⟨u, hu⟩ := nonempty_compl.mpr (good_domain.ne_univ : U ≠ univ)
Proof state after:
case intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
⊢ Set.Nonempty (𝓘 U)
Theorem: 𝓘_nonempty
Proof state before:
case intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
⊢ Set.Nonempty (𝓘 U)
Tactic:
let f : ℂ → ℂ := λ z => z - u
Proof state after:
case intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
⊢ Set.Nonempty (𝓘 U)
Theorem: 𝓘_nonempty
Proof state before:
case intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
⊢ Set.Nonempty (𝓘 U)
Tactic:
have f_inj : Injective f := λ _ _ h => sub_left_inj.mp h
Proof state after:
case intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
⊢ Set.Nonempty (𝓘 U)
Theorem: 𝓘_nonempty
Proof state before:
case intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
⊢ Set.Nonempty (𝓘 U)
Tactic:
have f_hol : DifferentiableOn ℂ f U := differentiableOn_id.sub (differentiableOn_const u)
Proof state after:
case intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
⊢ Set.Nonempty (𝓘 U)
Theorem: 𝓘_nonempty
Proof state before:
case intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
⊢ Set.Nonempty (𝓘 U)
Tactic:
have f_noz : ∀ ⦃z : ℂ⦄, z ∈ U -> f z ≠ 0 := λ z hz f0 => hu (sub_eq_zero.mp f0 ▸ hz)
Proof state after:
case intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
⊢ Set.Nonempty (𝓘 U)
Theorem: 𝓘_nonempty
Proof state before:
case intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
⊢ Set.Nonempty (𝓘 U)
Tactic:
obtain ⟨g, g_hol, g_sqf⟩ := good_domain.has_sqrt f f_noz f_hol
Proof state after:
case intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
⊢ Set.Nonempty (𝓘 U)
Theorem: 𝓘_nonempty
Proof state before:
case intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
⊢ Set.Nonempty (𝓘 U)
Tactic:
obtain ⟨z₀, hz₀⟩ := (good_domain.is_nonempty : U.Nonempty)
Proof state after:
case intro.intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ Set.Nonempty (𝓘 U)
Theorem: 𝓘_nonempty
Proof state before:
case intro.intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ Set.Nonempty (𝓘 U)
Tactic:
have gU_nhd : g '' U ∈ 𝓝 (g z₀) := by
  have e1 : U ∈ 𝓝 z₀ := good_domain.is_open.mem_nhds hz₀
  have e2 := g_hol.analyticAt e1
  have f_eq_comp := (good_domain.is_open.eventually_mem hz₀).mono g_sqf
  have dg_nonzero : deriv g z₀ ≠ 0 := by
    have e3 := e2.differentiableAt.deriv_eq_deriv_pow_div_pow zero_lt_two f_eq_comp (f_noz hz₀)
    simp [e3, deriv_sub_const, f]
    intro h
    have := g_sqf hz₀
    rw [Pi.pow_apply, h, zero_pow two_ne_zero] at this
    cases f_noz hz₀ this
  refine e2.eventually_constant_or_nhds_le_map_nhds.resolve_left (λ h => ?_) (image_mem_map e1)
  simp [EventuallyEq.deriv_eq h] at dg_nonzero
Proof state after:
case intro.intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
⊢ Set.Nonempty (𝓘 U)
Theorem: 𝓘_nonempty
Proof state before:
case intro.intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
⊢ Set.Nonempty (𝓘 U)
Tactic:
obtain ⟨r, r_pos, hr⟩ := Metric.mem_nhds_iff.mp gU_nhd
Proof state after:
case intro.intro.intro.intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
⊢ Set.Nonempty (𝓘 U)
Theorem: 𝓘_nonempty
Proof state before:
case intro.intro.intro.intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
⊢ Set.Nonempty (𝓘 U)
Tactic:
let gg : embedding U ((closedBall (- g z₀) (r / 2))ᶜ) :=
{ to_fun := g,
  is_diff := g_hol,
  is_inj := λ z₁ hz₁ z₂ hz₂ hgz => f_inj (by simp [g_sqf _, hz₁, hz₂, hgz]),
  maps_to := λ z hz hgz => by {
    apply f_noz hz
    rw [mem_closed_ball_neg_iff_mem_neg_closed_ball] at hgz
    obtain ⟨z', hz', hgz'⟩ := (closedBall_subset_ball (by linarith)).trans hr hgz
    have hzz' : z = z' := f_inj (by simp [g_sqf hz, g_sqf hz', hgz'])
    simpa [hzz', neg_eq_self_iff, g_sqf hz'] using hgz'.symm } }
Proof state after:
case intro.intro.intro.intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
gg : embedding U (closedBall (-g z₀) (r / 2))ᶜ := { to_fun := g, is_diff := g_hol, is_inj := ⋯, maps_to := ⋯ }
⊢ Set.Nonempty (𝓘 U)
Theorem: 𝓘_nonempty
Proof state before:
case intro.intro.intro.intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
gg : embedding U (closedBall (-g z₀) (r / 2))ᶜ := { to_fun := g, is_diff := g_hol, is_inj := ⋯, maps_to := ⋯ }
⊢ Set.Nonempty (𝓘 U)
Tactic:
let ggg := (embedding.inv _ (by linarith)).comp gg
Proof state after:
case intro.intro.intro.intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
gg : embedding U (closedBall (-g z₀) (r / 2))ᶜ := { to_fun := g, is_diff := g_hol, is_inj := ⋯, maps_to := ⋯ }
ggg : embedding U 𝔻 := embedding.comp (embedding.inv (-g z₀) ⋯) gg
⊢ Set.Nonempty (𝓘 U)
Theorem: 𝓘_nonempty
Proof state before:
case intro.intro.intro.intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
gg : embedding U (closedBall (-g z₀) (r / 2))ᶜ := { to_fun := g, is_diff := g_hol, is_inj := ⋯, maps_to := ⋯ }
ggg : embedding U 𝔻 := embedding.comp (embedding.inv (-g z₀) ⋯) gg
⊢ Set.Nonempty (𝓘 U)
Tactic:
refine ⟨ggg.to_fun, ⟨ggg.is_diff, ?_⟩, ggg.is_inj⟩
Proof state after:
case intro.intro.intro.intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
gg : embedding U (closedBall (-g z₀) (r / 2))ᶜ := { to_fun := g, is_diff := g_hol, is_inj := ⋯, maps_to := ⋯ }
ggg : embedding U 𝔻 := embedding.comp (embedding.inv (-g z₀) ⋯) gg
⊢ MapsTo ggg.to_fun U (closedBall 0 1)
Theorem: 𝓘_nonempty
Proof state before:
case intro.intro.intro.intro.intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
gg : embedding U (closedBall (-g z₀) (r / 2))ᶜ := { to_fun := g, is_diff := g_hol, is_inj := ⋯, maps_to := ⋯ }
ggg : embedding U 𝔻 := embedding.comp (embedding.inv (-g z₀) ⋯) gg
⊢ MapsTo ggg.to_fun U (closedBall 0 1)
Tactic:
exact λ z hz => ball_subset_closedBall (ggg.maps_to hz)
Proof state after:
no goals
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
⊢ g '' U ∈ 𝓝 (g z₀)
Tactic:
have e1 : U ∈ 𝓝 z₀ := good_domain.is_open.mem_nhds hz₀
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
⊢ g '' U ∈ 𝓝 (g z₀)
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
⊢ g '' U ∈ 𝓝 (g z₀)
Tactic:
have e2 := g_hol.analyticAt e1
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
⊢ g '' U ∈ 𝓝 (g z₀)
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
⊢ g '' U ∈ 𝓝 (g z₀)
Tactic:
have f_eq_comp := (good_domain.is_open.eventually_mem hz₀).mono g_sqf
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
⊢ g '' U ∈ 𝓝 (g z₀)
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
⊢ g '' U ∈ 𝓝 (g z₀)
Tactic:
have dg_nonzero : deriv g z₀ ≠ 0 := by
  have e3 := e2.differentiableAt.deriv_eq_deriv_pow_div_pow zero_lt_two f_eq_comp (f_noz hz₀)
  simp [e3, deriv_sub_const, f]
  intro h
  have := g_sqf hz₀
  rw [Pi.pow_apply, h, zero_pow two_ne_zero] at this
  cases f_noz hz₀ this
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
dg_nonzero : deriv g z₀ ≠ 0
⊢ g '' U ∈ 𝓝 (g z₀)
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
dg_nonzero : deriv g z₀ ≠ 0
⊢ g '' U ∈ 𝓝 (g z₀)
Tactic:
refine e2.eventually_constant_or_nhds_le_map_nhds.resolve_left (λ h => ?_) (image_mem_map e1)
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
dg_nonzero : deriv g z₀ ≠ 0
h : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z = g z₀
⊢ False
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
dg_nonzero : deriv g z₀ ≠ 0
h : ∀ᶠ (z : ℂ) in 𝓝 z₀, g z = g z₀
⊢ False
Tactic:
simp [EventuallyEq.deriv_eq h] at dg_nonzero
Proof state after:
no goals
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
⊢ deriv g z₀ ≠ 0
Tactic:
have e3 := e2.differentiableAt.deriv_eq_deriv_pow_div_pow zero_lt_two f_eq_comp (f_noz hz₀)
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
e3 : deriv (fun z => g z) z₀ = deriv (fun z => f z) z₀ / (↑2 * g z₀ ^ (2 - 1))
⊢ deriv g z₀ ≠ 0
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
e3 : deriv (fun z => g z) z₀ = deriv (fun z => f z) z₀ / (↑2 * g z₀ ^ (2 - 1))
⊢ deriv g z₀ ≠ 0
Tactic:
simp [e3, deriv_sub_const, f]
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
e3 : deriv (fun z => g z) z₀ = deriv (fun z => f z) z₀ / (↑2 * g z₀ ^ (2 - 1))
⊢ ¬g z₀ = 0
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
e3 : deriv (fun z => g z) z₀ = deriv (fun z => f z) z₀ / (↑2 * g z₀ ^ (2 - 1))
⊢ ¬g z₀ = 0
Tactic:
intro h
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
e3 : deriv (fun z => g z) z₀ = deriv (fun z => f z) z₀ / (↑2 * g z₀ ^ (2 - 1))
h : g z₀ = 0
⊢ False
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
e3 : deriv (fun z => g z) z₀ = deriv (fun z => f z) z₀ / (↑2 * g z₀ ^ (2 - 1))
h : g z₀ = 0
⊢ False
Tactic:
have := g_sqf hz₀
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
e3 : deriv (fun z => g z) z₀ = deriv (fun z => f z) z₀ / (↑2 * g z₀ ^ (2 - 1))
h : g z₀ = 0
this : f z₀ = (g ^ 2) z₀
⊢ False
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
e3 : deriv (fun z => g z) z₀ = deriv (fun z => f z) z₀ / (↑2 * g z₀ ^ (2 - 1))
h : g z₀ = 0
this : f z₀ = (g ^ 2) z₀
⊢ False
Tactic:
rw [Pi.pow_apply, h, zero_pow two_ne_zero] at this
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
e3 : deriv (fun z => g z) z₀ = deriv (fun z => f z) z₀ / (↑2 * g z₀ ^ (2 - 1))
h : g z₀ = 0
this : f z₀ = 0
⊢ False
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
e1 : U ∈ 𝓝 z₀
e2 : AnalyticAt ℂ g z₀
f_eq_comp : ∀ᶠ (x : ℂ) in 𝓝 z₀, f x = (g ^ 2) x
e3 : deriv (fun z => g z) z₀ = deriv (fun z => f z) z₀ / (↑2 * g z₀ ^ (2 - 1))
h : g z₀ = 0
this : f z₀ = 0
⊢ False
Tactic:
cases f_noz hz₀ this
Proof state after:
no goals
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
z₁ : ℂ
hz₁ : z₁ ∈ U
z₂ : ℂ
hz₂ : z₂ ∈ U
hgz : g z₁ = g z₂
⊢ f z₁ = f z₂
Tactic:
simp [g_sqf _, hz₁, hz₂, hgz]
Proof state after:
no goals
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
z : ℂ
hz : z ∈ U
hgz : g z ∈ closedBall (-g z₀) (r / 2)
⊢ False
Tactic:
apply f_noz hz
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
z : ℂ
hz : z ∈ U
hgz : g z ∈ closedBall (-g z₀) (r / 2)
⊢ f z = 0