internlm/Lean-Github huggingface dataset:
Theorem: step_2
Proof state before:
case refine_1
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ DifferentiableOn ℂ (σ ∘ (φ ⋯).to_fun) 𝔻
Tactic:
apply DifferentiableOn.comp
Proof state after:
case refine_1.hg
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ DifferentiableOn ℂ σ ?refine_1.t

case refine_1.hf
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ DifferentiableOn ℂ (φ ⋯).to_fun 𝔻

case refine_1.st
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ MapsTo (φ ⋯).to_fun 𝔻 ?refine_1.t

case refine_1.t
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ Set ℂ
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ Set ℂ
Tactic:
case t => exact 𝔻
Proof state after:
no goals
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ DifferentiableOn ℂ σ 𝔻
Tactic:
case hg =>
  apply DifferentiableOn.pow
  exact differentiable_id.differentiableOn
Proof state after:
no goals
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ DifferentiableOn ℂ (φ ⋯).to_fun 𝔻
Tactic:
case hf =>
  exact (φ (neg_in_𝔻 v_in_𝔻)).is_diff
Proof state after:
no goals
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ MapsTo (φ ⋯).to_fun 𝔻 𝔻
Tactic:
case st =>
  exact (φ (neg_in_𝔻 v_in_𝔻)).maps_to
Proof state after:
no goals
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ Set ℂ
Tactic:
exact 𝔻
Proof state after:
no goals
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ DifferentiableOn ℂ σ 𝔻
Tactic:
apply DifferentiableOn.pow
Proof state after:
case ha
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ DifferentiableOn ℂ (fun x => x) 𝔻
Theorem: step_2
Proof state before:
case ha
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ DifferentiableOn ℂ (fun x => x) 𝔻
Tactic:
exact differentiable_id.differentiableOn
Proof state after:
no goals
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ DifferentiableOn ℂ (φ ⋯).to_fun 𝔻
Tactic:
exact (φ (neg_in_𝔻 v_in_𝔻)).is_diff
Proof state after:
no goals
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ MapsTo (φ ⋯).to_fun 𝔻 𝔻
Tactic:
exact (φ (neg_in_𝔻 v_in_𝔻)).maps_to
Proof state after:
no goals
Theorem: step_2
Proof state before:
case refine_2
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ MapsTo (σ ∘ (φ ⋯).to_fun) 𝔻 𝔻
Tactic:
refine MapsTo.comp ?_ (φ (neg_in_𝔻 v_in_𝔻)).maps_to
Proof state after:
case refine_2
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ MapsTo σ 𝔻 𝔻
Theorem: step_2
Proof state before:
case refine_2
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
⊢ MapsTo σ 𝔻 𝔻
Tactic:
intros z hz
Proof state after:
case refine_2
z✝ u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
z : ℂ
hz : z ∈ 𝔻
⊢ σ z ∈ 𝔻
Theorem: step_2
Proof state before:
case refine_2
z✝ u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
z : ℂ
hz : z ∈ 𝔻
⊢ σ z ∈ 𝔻
Tactic:
simpa [σ, 𝔻] using hz
Proof state after:
no goals
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
⊢ deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
Tactic:
have e1 : U ∈ 𝓝 z₀ := good_domain.is_open.mem_nhds hz₀
Proof state after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
e1 : U ∈ 𝓝 z₀
⊢ deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
e1 : U ∈ 𝓝 z₀
⊢ deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
Tactic:
have e2 : 𝔻 ∈ 𝓝 (0 : ℂ) := ball_mem_nhds _ zero_lt_one
Proof state after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
e1 : U ∈ 𝓝 z₀
e2 : 𝔻 ∈ 𝓝 0
⊢ deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
e1 : U ∈ 𝓝 z₀
e2 : 𝔻 ∈ 𝓝 0
⊢ deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
Tactic:
have e3 : deriv f z₀ = deriv (ψ ∘ h) z₀ := (eventuallyEq_of_mem e1 f_eq_ψ_h).deriv_eq
Proof state after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
e1 : U ∈ 𝓝 z₀
e2 : 𝔻 ∈ 𝓝 0
e3 : deriv f.to_fun z₀ = deriv (ψ ∘ h.to_fun) z₀
⊢ deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
e1 : U ∈ 𝓝 z₀
e2 : 𝔻 ∈ 𝓝 0
e3 : deriv f.to_fun z₀ = deriv (ψ ∘ h.to_fun) z₀
⊢ deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
Tactic:
rw [e3, ← h_z₀_eq_0]
Proof state after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
e1 : U ∈ 𝓝 z₀
e2 : 𝔻 ∈ 𝓝 0
e3 : deriv f.to_fun z₀ = deriv (ψ ∘ h.to_fun) z₀
⊢ deriv (ψ ∘ h.to_fun) z₀ = deriv ψ (h.to_fun z₀) * deriv h.to_fun z₀
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
e1 : U ∈ 𝓝 z₀
e2 : 𝔻 ∈ 𝓝 0
e3 : deriv f.to_fun z₀ = deriv (ψ ∘ h.to_fun) z₀
⊢ deriv (ψ ∘ h.to_fun) z₀ = deriv ψ (h.to_fun z₀) * deriv h.to_fun z₀
Tactic:
refine deriv.comp z₀ ?_ (h.is_diff.differentiableAt e1)
Proof state after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
e1 : U ∈ 𝓝 z₀
e2 : 𝔻 ∈ 𝓝 0
e3 : deriv f.to_fun z₀ = deriv (ψ ∘ h.to_fun) z₀
⊢ DifferentiableAt ℂ ψ (h.to_fun z₀)
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
e1 : U ∈ 𝓝 z₀
e2 : 𝔻 ∈ 𝓝 0
e3 : deriv f.to_fun z₀ = deriv (ψ ∘ h.to_fun) z₀
⊢ DifferentiableAt ℂ ψ (h.to_fun z₀)
Tactic:
rw [h_z₀_eq_0]
Proof state after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
e1 : U ∈ 𝓝 z₀
e2 : 𝔻 ∈ 𝓝 0
e3 : deriv f.to_fun z₀ = deriv (ψ ∘ h.to_fun) z₀
⊢ DifferentiableAt ℂ ψ 0
Theorem: step_2
Proof state before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
e1 : U ∈ 𝓝 z₀
e2 : 𝔻 ∈ 𝓝 0
e3 : deriv f.to_fun z₀ = deriv (ψ ∘ h.to_fun) z₀
⊢ DifferentiableAt ℂ ψ 0
Tactic:
exact ψ_is_diff.differentiableAt e2
Proof state after:
no goals
Theorem: step_2
Proof state before:
case intro.intro.mk.refine_1
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
u : ℂ
u_in_𝔻 : u ∈ 𝔻
u_not_in_f_U : u ∉ f.to_fun '' U
φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
φᵤf : embedding U 𝔻 := embedding.comp φᵤ f
φᵤf_ne_zero : ∀ z ∈ U, φᵤf.to_fun z ≠ 0
g : embedding U 𝔻
hg : EqOn φᵤf.to_fun (g.to_fun ^ 2) U
v : ℂ := g.to_fun z₀
v_in_𝔻 : v ∈ 𝔻
h : embedding U 𝔻 := embedding.comp (φ v_in_𝔻) g
h_z₀_eq_0 : h.to_fun z₀ = 0
σ : ℂ → ℂ := fun z => z ^ 2
ψ : ℂ → ℂ := (φ ⋯).to_fun ∘ σ ∘ (φ ⋯).to_fun
f_eq_ψ_h : EqOn f.to_fun (ψ ∘ h.to_fun) U
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
deriv_eq_mul : deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
⊢ 0 < ‖deriv h.to_fun z₀‖
Tactic:
exact norm_pos_iff.2 (embedding.deriv_ne_zero good_domain.is_open hz₀)
Proof state after:
no goals