Theorem: step_2 (RMT4/etape2.lean)

State before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
obtain ⟨u, u_in_𝔻, u_not_in_f_U⟩ := exists_of_ssubset hf
State after:
case intro.intro
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖

State before:
case intro.intro
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
let φᵤ : embedding 𝔻 𝔻 := φ u_in_𝔻
State after:
case intro.intro
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_𝔻
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖

State before:
case intro.intro
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_𝔻
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
let φᵤf : embedding U 𝔻 := φᵤ.comp f
State after:
case intro.intro
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖

State before:
case intro.intro
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
have φᵤf_ne_zero : ∀ z ∈ U, φᵤf z ≠ 0 := λ z z_in_U hz => by
  refine u_not_in_f_U ⟨z, z_in_U, ?_⟩
  apply φᵤ.is_inj (f.maps_to z_in_U) u_in_𝔻
  dsimp [φᵤf] at hz
  rw [hz]
  simp [φᵤ, φ]
State after:
case intro.intro
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖

State before:
case intro.intro
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
obtain ⟨g, hg⟩ := φᵤf.sqrt' φᵤf_ne_zero
State after:
case intro.intro.mk
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖

State before:
case intro.intro.mk
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
let v : ℂ := g z₀
State after:
case intro.intro.mk
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₀
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖

State before:
case intro.intro.mk
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₀
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
have v_in_𝔻 : v ∈ 𝔻 := g.maps_to hz₀
State after:
case intro.intro.mk
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, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖

State before:
case intro.intro.mk
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, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
let h : embedding U 𝔻 := (φ v_in_𝔻).comp g
State after:
case intro.intro.mk
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, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖

State before:
case intro.intro.mk
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, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
have h_z₀_eq_0 : h z₀ = 0 := by simp [h, φ]
State after:
case intro.intro.mk
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖

State before:
case intro.intro.mk
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
let σ : ℂ → ℂ := λ z => z ^ 2
State after:
case intro.intro.mk
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖

State before:
case intro.intro.mk
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
let ψ : ℂ → ℂ := φ (neg_in_𝔻 u_in_𝔻) ∘ σ ∘ φ (neg_in_𝔻 v_in_𝔻)
State after:
case intro.intro.mk
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖

State before:
case intro.intro.mk
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
have f_eq_ψ_h : EqOn f (ψ ∘ h) U := λ z hz => by
  have e1 := φ_inv v_in_𝔻 (g.maps_to hz)
  have e2 := hg hz
  have e3 := φ_inv u_in_𝔻 (f.maps_to hz)
  dsimp [φᵤf] at e2
  simp [ψ, σ, h, e1, ← e2, e3]
State after:
case intro.intro.mk
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
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖

State before:
case intro.intro.mk
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 ℂ ψ 𝔻
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
have deriv_eq_mul : deriv f z₀ = deriv ψ 0 * deriv h z₀ := by
  have e1 : U ∈ 𝓝 z₀ := good_domain.is_open.mem_nhds hz₀
  have e2 : 𝔻 ∈ 𝓝 (0 : ℂ) := ball_mem_nhds _ zero_lt_one
  have e3 : deriv f z₀ = deriv (ψ ∘ h) z₀ := (eventuallyEq_of_mem e1 f_eq_ψ_h).deriv_eq
  rw [e3, ← h_z₀_eq_0]
  refine deriv.comp z₀ ?_ (h.is_diff.differentiableAt e1)
  rw [h_z₀_eq_0]
  exact ψ_is_diff.differentiableAt e2
State after:
case intro.intro.mk
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₀
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖

State before:
case intro.intro.mk
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₀
⊢ ∃ h, ‖deriv f.to_fun z₀‖ < ‖deriv h.to_fun z₀‖
Tactic:
rw [deriv_eq_mul, norm_mul]
State after:
case intro.intro.mk
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₀
⊢ ∃ h_1, ‖deriv ψ 0‖ * ‖deriv h.to_fun z₀‖ < ‖deriv h_1.to_fun z₀‖

State before:
case intro.intro.mk
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₀
⊢ ∃ h_1, ‖deriv ψ 0‖ * ‖deriv h.to_fun z₀‖ < ‖deriv h_1.to_fun z₀‖
Tactic:
refine ⟨h, mul_lt_of_lt_one_left ?_ ?_⟩
State after:
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₀‖

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

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
z : ℂ
z_in_U : z ∈ U
hz : φᵤf.to_fun z = 0
⊢ False
Tactic:
refine u_not_in_f_U ⟨z, z_in_U, ?_⟩
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
z : ℂ
z_in_U : z ∈ U
hz : φᵤf.to_fun z = 0
⊢ f.to_fun z = u

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
z : ℂ
z_in_U : z ∈ U
hz : φᵤf.to_fun z = 0
⊢ f.to_fun z = u
Tactic:
apply φᵤ.is_inj (f.maps_to z_in_U) u_in_𝔻
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
z : ℂ
z_in_U : z ∈ U
hz : φᵤf.to_fun z = 0
⊢ φᵤ.to_fun (f.to_fun z) = φᵤ.to_fun u

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
z : ℂ
z_in_U : z ∈ U
hz : φᵤf.to_fun z = 0
⊢ φᵤ.to_fun (f.to_fun z) = φᵤ.to_fun u
Tactic:
dsimp [φᵤf] at hz
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
z : ℂ
z_in_U : z ∈ U
hz : φᵤ.to_fun (f.to_fun z) = 0
⊢ φᵤ.to_fun (f.to_fun z) = φᵤ.to_fun u

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
z : ℂ
z_in_U : z ∈ U
hz : φᵤ.to_fun (f.to_fun z) = 0
⊢ φᵤ.to_fun (f.to_fun z) = φᵤ.to_fun u
Tactic:
rw [hz]
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
z : ℂ
z_in_U : z ∈ U
hz : φᵤ.to_fun (f.to_fun z) = 0
⊢ 0 = φᵤ.to_fun u

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
z : ℂ
z_in_U : z ∈ U
hz : φᵤ.to_fun (f.to_fun z) = 0
⊢ 0 = φᵤ.to_fun u
Tactic:
simp [φᵤ, φ]
State after:
no goals

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.to_fun z₀ = 0
Tactic:
simp [h, φ]
State after:
no goals

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
z : ℂ
hz : z ∈ U
⊢ f.to_fun z = (ψ ∘ h.to_fun) z
Tactic:
have e1 := φ_inv v_in_𝔻 (g.maps_to hz)
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
z : ℂ
hz : z ∈ U
e1 : (φ ⋯).to_fun ((φ v_in_𝔻).to_fun (g.to_fun z)) = g.to_fun z
⊢ f.to_fun z = (ψ ∘ h.to_fun) z

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
z : ℂ
hz : z ∈ U
e1 : (φ ⋯).to_fun ((φ v_in_𝔻).to_fun (g.to_fun z)) = g.to_fun z
⊢ f.to_fun z = (ψ ∘ h.to_fun) z
Tactic:
have e2 := hg hz
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
z : ℂ
hz : z ∈ U
e1 : (φ ⋯).to_fun ((φ v_in_𝔻).to_fun (g.to_fun z)) = g.to_fun z
e2 : φᵤf.to_fun z = (g.to_fun ^ 2) z
⊢ f.to_fun z = (ψ ∘ h.to_fun) z

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
z : ℂ
hz : z ∈ U
e1 : (φ ⋯).to_fun ((φ v_in_𝔻).to_fun (g.to_fun z)) = g.to_fun z
e2 : φᵤf.to_fun z = (g.to_fun ^ 2) z
⊢ f.to_fun z = (ψ ∘ h.to_fun) z
Tactic:
have e3 := φ_inv u_in_𝔻 (f.maps_to hz)
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
z : ℂ
hz : z ∈ U
e1 : (φ ⋯).to_fun ((φ v_in_𝔻).to_fun (g.to_fun z)) = g.to_fun z
e2 : φᵤf.to_fun z = (g.to_fun ^ 2) z
e3 : (φ ⋯).to_fun ((φ u_in_𝔻).to_fun (f.to_fun z)) = f.to_fun z
⊢ f.to_fun z = (ψ ∘ h.to_fun) z

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
z : ℂ
hz : z ∈ U
e1 : (φ ⋯).to_fun ((φ v_in_𝔻).to_fun (g.to_fun z)) = g.to_fun z
e2 : φᵤf.to_fun z = (g.to_fun ^ 2) z
e3 : (φ ⋯).to_fun ((φ u_in_𝔻).to_fun (f.to_fun z)) = f.to_fun z
⊢ f.to_fun z = (ψ ∘ h.to_fun) z
Tactic:
dsimp [φᵤf] at e2
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
z : ℂ
hz : z ∈ U
e1 : (φ ⋯).to_fun ((φ v_in_𝔻).to_fun (g.to_fun z)) = g.to_fun z
e2 : φᵤ.to_fun (f.to_fun z) = g.to_fun z ^ 2
e3 : (φ ⋯).to_fun ((φ u_in_𝔻).to_fun (f.to_fun z)) = f.to_fun z
⊢ f.to_fun z = (ψ ∘ h.to_fun) z

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
z : ℂ
hz : z ∈ U
e1 : (φ ⋯).to_fun ((φ v_in_𝔻).to_fun (g.to_fun z)) = g.to_fun z
e2 : φᵤ.to_fun (f.to_fun z) = g.to_fun z ^ 2
e3 : (φ ⋯).to_fun ((φ u_in_𝔻).to_fun (f.to_fun z)) = f.to_fun z
⊢ f.to_fun z = (ψ ∘ h.to_fun) z
Tactic:
simp [ψ, σ, h, e1, ← e2, e3]
State after:
no goals

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:
refine (φ (neg_in_𝔻 u_in_𝔻)).is_diff.comp ?_ ?_
State after:
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) 𝔻

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) 𝔻 𝔻

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
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 ℂ

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 𝔻
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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 𝔻
State after:
no goals

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
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) 𝔻

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
State after:
no goals

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
State after:
no goals

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
State after:
no goals

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
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 σ 𝔻 𝔻

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
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 ∈ 𝔻

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
State after:
no goals

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₀
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₀

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
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₀

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
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₀

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]
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₀

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)
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₀)

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]
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

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
State after:
no goals

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₀)
State after:
no goals

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
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 ψ 𝔻

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 ?_)
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

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)
State after:
no goals

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]
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

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
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

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
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

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, ?_, ?_⟩
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⁻¹)

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
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

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
State after:
no goals

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
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⁻¹))

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]
State after:
no goals

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
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

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
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

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
State after:
no goals