internlm/Lean-Github huggingface dataset:
Theorem: step_2
Proof state before:
case intro.intro.mk.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
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
deriv_eq_mul : deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
⊢ ‖deriv ψ 0‖ < 1
Tactic:
apply non_injective_schwarz ψ_is_diff
Proof state after:
case intro.intro.mk.refine_2.f_img
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₀
⊢ MapsTo ψ 𝔻 𝔻

case intro.intro.mk.refine_2.f_noninj
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₀
⊢ ¬InjOn ψ 𝔻
Theorem: step_2
Proof state before:
case intro.intro.mk.refine_2.f_img
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₀
⊢ MapsTo ψ 𝔻 𝔻
Tactic:
refine λ z hz => (φ (neg_in_𝔻 u_in_𝔻)).maps_to (mem_𝔻_iff.mpr ?_)
Proof state after:
case intro.intro.mk.refine_2.f_img
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₀
z : ℂ
hz : z ∈ 𝔻
⊢ ‖(σ ∘ (φ ⋯).to_fun) z‖ < 1
Theorem: step_2
Proof state before:
case intro.intro.mk.refine_2.f_img
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₀
z : ℂ
hz : z ∈ 𝔻
⊢ ‖(σ ∘ (φ ⋯).to_fun) z‖ < 1
Tactic:
simpa [σ] using mem_𝔻_iff.mp ((φ (neg_in_𝔻 v_in_𝔻)).maps_to hz)
Proof state after:
no goals
Theorem: step_2
Proof state before:
case intro.intro.mk.refine_2.f_noninj
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₀
⊢ ¬InjOn ψ 𝔻
Tactic:
simp only [InjOn, not_forall, exists_prop]
Proof state after:
case intro.intro.mk.refine_2.f_noninj
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₀
⊢ ∃ x ∈ 𝔻, ∃ x_1 ∈ 𝔻, ψ x = ψ x_1 ∧ ¬x = x_1
Theorem: step_2
Proof state before:
case intro.intro.mk.refine_2.f_noninj
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₀
⊢ ∃ x ∈ 𝔻, ∃ x_1 ∈ 𝔻, ψ x = ψ x_1 ∧ ¬x = x_1
Tactic:
have e1 : (2⁻¹ : ℂ) ∈ 𝔻 := by apply mem_𝔻_iff.mpr; norm_num
Proof state after:
case intro.intro.mk.refine_2.f_noninj
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₀
e1 : 2⁻¹ ∈ 𝔻
⊢ ∃ x ∈ 𝔻, ∃ x_1 ∈ 𝔻, ψ x = ψ x_1 ∧ ¬x = x_1
Theorem: step_2
Proof state before:
case intro.intro.mk.refine_2.f_noninj
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₀
e1 : 2⁻¹ ∈ 𝔻
⊢ ∃ x ∈ 𝔻, ∃ x_1 ∈ 𝔻, ψ x = ψ x_1 ∧ ¬x = x_1
Tactic:
have e2 : (-2⁻¹ : ℂ) ∈ 𝔻 := neg_in_𝔻 e1
Proof state after:
case intro.intro.mk.refine_2.f_noninj
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₀
e1 : 2⁻¹ ∈ 𝔻
e2 : -2⁻¹ ∈ 𝔻
⊢ ∃ x ∈ 𝔻, ∃ x_1 ∈ 𝔻, ψ x = ψ x_1 ∧ ¬x = x_1
Theorem: step_2
Proof state before:
case intro.intro.mk.refine_2.f_noninj
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₀
e1 : 2⁻¹ ∈ 𝔻
e2 : -2⁻¹ ∈ 𝔻
⊢ ∃ x ∈ 𝔻, ∃ x_1 ∈ 𝔻, ψ x = ψ x_1 ∧ ¬x = x_1
Tactic:
refine ⟨φ v_in_𝔻 2⁻¹, (φ v_in_𝔻).maps_to e1, φ v_in_𝔻 (-2⁻¹), (φ v_in_𝔻).maps_to e2, ?_, ?_⟩
Proof state after:
case intro.intro.mk.refine_2.f_noninj.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₀
e1 : 2⁻¹ ∈ 𝔻
e2 : -2⁻¹ ∈ 𝔻
⊢ ψ ((φ v_in_𝔻).to_fun 2⁻¹) = ψ ((φ v_in_𝔻).to_fun (-2⁻¹))

case intro.intro.mk.refine_2.f_noninj.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
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
deriv_eq_mul : deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
e1 : 2⁻¹ ∈ 𝔻
e2 : -2⁻¹ ∈ 𝔻
⊢ ¬(φ v_in_𝔻).to_fun 2⁻¹ = (φ v_in_𝔻).to_fun (-2⁻¹)
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_eq_mul : deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
⊢ 2⁻¹ ∈ 𝔻
Tactic:
apply mem_𝔻_iff.mpr
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 ℂ ψ 𝔻
deriv_eq_mul : deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
⊢ ‖2⁻¹‖ < 1
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_eq_mul : deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
⊢ ‖2⁻¹‖ < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: step_2
Proof state before:
case intro.intro.mk.refine_2.f_noninj.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₀
e1 : 2⁻¹ ∈ 𝔻
e2 : -2⁻¹ ∈ 𝔻
⊢ ψ ((φ v_in_𝔻).to_fun 2⁻¹) = ψ ((φ v_in_𝔻).to_fun (-2⁻¹))
Tactic:
unfold_let
Proof state after:
case intro.intro.mk.refine_2.f_noninj.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₀
e1 : 2⁻¹ ∈ 𝔻
e2 : -2⁻¹ ∈ 𝔻
⊢ ((φ ⋯).to_fun ∘ (fun z => z ^ 2) ∘ (φ ⋯).to_fun) ((φ v_in_𝔻).to_fun 2⁻¹) =
    ((φ ⋯).to_fun ∘ (fun z => z ^ 2) ∘ (φ ⋯).to_fun) ((φ v_in_𝔻).to_fun (-2⁻¹))
Theorem: step_2
Proof state before:
case intro.intro.mk.refine_2.f_noninj.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₀
e1 : 2⁻¹ ∈ 𝔻
e2 : -2⁻¹ ∈ 𝔻
⊢ ((φ ⋯).to_fun ∘ (fun z => z ^ 2) ∘ (φ ⋯).to_fun) ((φ v_in_𝔻).to_fun 2⁻¹) =
    ((φ ⋯).to_fun ∘ (fun z => z ^ 2) ∘ (φ ⋯).to_fun) ((φ v_in_𝔻).to_fun (-2⁻¹))
Tactic:
simp [φ_inv v_in_𝔻 e1, φ_inv v_in_𝔻 e2]
Proof state after:
no goals
Theorem: step_2
Proof state before:
case intro.intro.mk.refine_2.f_noninj.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
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
deriv_eq_mul : deriv f.to_fun z₀ = deriv ψ 0 * deriv h.to_fun z₀
e1 : 2⁻¹ ∈ 𝔻
e2 : -2⁻¹ ∈ 𝔻
⊢ ¬(φ v_in_𝔻).to_fun 2⁻¹ = (φ v_in_𝔻).to_fun (-2⁻¹)
Tactic:
intro h
Proof state after:
case intro.intro.mk.refine_2.f_noninj.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
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
deriv_eq_mul : deriv f.to_fun z₀ = deriv ψ 0 * deriv h✝.to_fun z₀
e1 : 2⁻¹ ∈ 𝔻
e2 : -2⁻¹ ∈ 𝔻
h : (φ v_in_𝔻).to_fun 2⁻¹ = (φ v_in_𝔻).to_fun (-2⁻¹)
⊢ False
Theorem: step_2
Proof state before:
case intro.intro.mk.refine_2.f_noninj.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
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
deriv_eq_mul : deriv f.to_fun z₀ = deriv ψ 0 * deriv h✝.to_fun z₀
e1 : 2⁻¹ ∈ 𝔻
e2 : -2⁻¹ ∈ 𝔻
h : (φ v_in_𝔻).to_fun 2⁻¹ = (φ v_in_𝔻).to_fun (-2⁻¹)
⊢ False
Tactic:
have := (φ v_in_𝔻).is_inj e1 e2 h
Proof state after:
case intro.intro.mk.refine_2.f_noninj.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
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
deriv_eq_mul : deriv f.to_fun z₀ = deriv ψ 0 * deriv h✝.to_fun z₀
e1 : 2⁻¹ ∈ 𝔻
e2 : -2⁻¹ ∈ 𝔻
h : (φ v_in_𝔻).to_fun 2⁻¹ = (φ v_in_𝔻).to_fun (-2⁻¹)
this : 2⁻¹ = -2⁻¹
⊢ False
Theorem: step_2
Proof state before:
case intro.intro.mk.refine_2.f_noninj.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
ψ_is_diff : DifferentiableOn ℂ ψ 𝔻
deriv_eq_mul : deriv f.to_fun z₀ = deriv ψ 0 * deriv h✝.to_fun z₀
e1 : 2⁻¹ ∈ 𝔻
e2 : -2⁻¹ ∈ 𝔻
h : (φ v_in_𝔻).to_fun 2⁻¹ = (φ v_in_𝔻).to_fun (-2⁻¹)
this : 2⁻¹ = -2⁻¹
⊢ False
Tactic:
norm_num at this
Proof state after:
no goals
Theorem: isCompact_segment
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : TopologicalAddGroup 𝕜
inst✝⁵ : CompactIccSpace 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ IsCompact (segment 𝕜 x y)
Tactic:
simpa only [segment_eq_image] using isCompact_Icc.image (by continuity)
Proof state after:
no goals
Theorem: isCompact_segment
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝⁸ : OrderedRing 𝕜
inst✝⁷ : TopologicalSpace 𝕜
inst✝⁶ : TopologicalAddGroup 𝕜
inst✝⁵ : CompactIccSpace 𝕜
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : ContinuousAdd E
inst✝¹ : Module 𝕜 E
inst✝ : ContinuousSMul 𝕜 E
x y : E
⊢ Continuous fun θ => (1 - θ) • x + θ • y
Tactic:
continuity
Proof state after:
no goals
Theorem: mem_closed_ball_neg_iff_mem_neg_closed_ball
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝ : SeminormedAddCommGroup V
u v : V
⊢ u ∈ closedBall (-v) r ↔ -u ∈ closedBall v r
Tactic:
rw [← neg_closedBall r v]
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝ : SeminormedAddCommGroup V
u v : V
⊢ u ∈ -closedBall v r ↔ -u ∈ closedBall v r
Theorem: mem_closed_ball_neg_iff_mem_neg_closed_ball
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝ : SeminormedAddCommGroup V
u v : V
⊢ u ∈ -closedBall v r ↔ -u ∈ closedBall v r
Tactic:
rfl
Proof state after:
no goals
Theorem: DifferentiableAt.deriv_eq_deriv_pow_div_pow
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
⊢ deriv g z = deriv f z / (↑n * g z ^ (n - 1))
Tactic:
have h1 : g z ≠ 0 := λ h => fz_nonzero (by simp [Eventually.self_of_nhds hg, h, n_pos.ne.symm])
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
⊢ deriv g z = deriv f z / (↑n * g z ^ (n - 1))
Theorem: DifferentiableAt.deriv_eq_deriv_pow_div_pow
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
⊢ deriv g z = deriv f z / (↑n * g z ^ (n - 1))
Tactic:
have h2 : n * (g z) ^ (n - 1) ≠ 0 := by simp [pow_ne_zero, h1, n_pos.ne.symm]
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
h2 : ↑n * g z ^ (n - 1) ≠ 0
⊢ deriv g z = deriv f z / (↑n * g z ^ (n - 1))