Theorem: non_injective_schwarz (RMT4/etape2.lean)

State before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
⊢ ‖deriv f 0‖ < 1
Tactic:
set u := f 0
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
⊢ ‖deriv f 0‖ < 1
Tactic:
have u_in_𝔻 : u ∈ 𝔻 := f_img (mem_ball_self zero_lt_one)
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
⊢ ‖deriv f 0‖ < 1
Tactic:
let g := φ u_in_𝔻 ∘ f
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
⊢ ‖deriv f 0‖ < 1
Tactic:
have g_diff : DifferentiableOn ℂ g 𝔻 := (φ u_in_𝔻).is_diff.comp f_diff f_img
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
⊢ ‖deriv f 0‖ < 1
Tactic:
have g_maps : MapsTo g 𝔻 𝔻 := (φ u_in_𝔻).maps_to.comp f_img
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
⊢ ‖deriv f 0‖ < 1
Tactic:
have g_0_eq_0 : g 0 = 0 := by simp [g, φ]
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
⊢ ‖deriv f 0‖ < 1
Tactic:
by_cases h : ‖deriv g 0‖ = 1
State after:
case pos
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
⊢ ‖deriv f 0‖ < 1

case neg
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬‖deriv g 0‖ = 1
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
⊢ ‖deriv f 0‖ < 1
Tactic:
case pos =>
  have g_lin : EqOn g (λ (z : ℂ) => z • deriv g 0) (ball 0 1) := by
    have h2 : MapsTo g (ball 0 1) (ball (g 0) 1) := by rwa [g_0_eq_0]
    have h1 : Set.EqOn g (fun z => g 0 + (z - 0) • dslope g 0 0) (Metric.ball 0 1) := by
      apply affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div g_diff h2 (mem_ball_self zero_lt_one)
      rwa [dslope_same, div_one]
    convert h1 using 1
    ext1 z
    rw [g_0_eq_0, zero_add, sub_zero, dslope_same]
  have g'0_ne_0 : deriv g 0 ≠ 0 := λ h' => by simp [h'] at h
  have g_inj : InjOn g 𝔻 := λ x hx y hy => by
    rw [g_lin hx, g_lin hy]
    simp [g'0_ne_0]
  cases f_noninj (injOn_of_injOn_comp g_inj)
State after:
no goals

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬‖deriv g 0‖ = 1
⊢ ‖deriv f 0‖ < 1
Tactic:
case neg =>
  rw [norm_eq_abs] at h
  have g'0_le_1 := abs_deriv_le_one_of_mapsTo_ball g_diff g_maps g_0_eq_0 zero_lt_one
  have g'0_lt_1 : abs (deriv g 0) < 1 := Ne.lt_of_le h g'0_le_1
  have g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻) u * deriv f 0 :=
    deriv.comp 0 ((φ u_in_𝔻).is_diff.differentiableAt (isOpen_ball.mem_nhds u_in_𝔻))
      (f_diff.differentiableAt (ball_mem_nhds _ zero_lt_one))
  have e1 : 1 - (normSq u : ℂ) ≠ 0 := by
    simpa [normSq_eq_conj_mul_self, mul_comm] using one_sub_mul_conj_ne_zero u_in_𝔻 u_in_𝔻
  have φ'u_u : deriv (φ u_in_𝔻) u = 1 / (1 - normSq u) := by
    set w := 1 - conj u * u with hw
    have : w ≠ 0 := by simpa [normSq_eq_conj_mul_self, mul_comm u] using e1
    rw [φ_deriv u_in_𝔻 u_in_𝔻, normSq_eq_conj_mul_self, mul_comm u, ← hw]
    field_simp; ring
  have e2 : 0 ≤ normSq u := normSq_nonneg _
  have e3 : normSq u < 1 := by
    rw [normSq_eq_abs]
    have : abs u < 1 := mem_𝔻_iff.mp u_in_𝔻
    simp only [sq_lt_one_iff_abs_lt_one, Complex.abs_abs, this]
  simp [normSq_eq_abs, ← mem_𝔻_iff]
  simp only [φ'u_u, one_div] at g'0_eq_mul
  rw [eq_comm, inv_mul_eq_iff_eq_mul₀ e1] at g'0_eq_mul
  rw [← norm_eq_abs, g'0_eq_mul, norm_mul, mul_comm, ← one_mul (1 : ℝ)]
  refine mul_lt_mul g'0_lt_1 ?_ (norm_pos_iff.mpr e1) zero_le_one
  simp at e2 e3 ⊢
  norm_cast
  rw [abs_sub_le_iff]
  refine ⟨?_, ?_⟩; repeat linarith
State after:
no goals

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
⊢ g 0 = 0
Tactic:
simp [g, φ]
State after:
no goals

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
⊢ ‖deriv f 0‖ < 1
Tactic:
have g_lin : EqOn g (λ (z : ℂ) => z • deriv g 0) (ball 0 1) := by
  have h2 : MapsTo g (ball 0 1) (ball (g 0) 1) := by rwa [g_0_eq_0]
  have h1 : Set.EqOn g (fun z => g 0 + (z - 0) • dslope g 0 0) (Metric.ball 0 1) := by
    apply affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div g_diff h2 (mem_ball_self zero_lt_one)
    rwa [dslope_same, div_one]
  convert h1 using 1
  ext1 z
  rw [g_0_eq_0, zero_add, sub_zero, dslope_same]
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
g_lin : EqOn g (fun z => z • deriv g 0) (ball 0 1)
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
g_lin : EqOn g (fun z => z • deriv g 0) (ball 0 1)
⊢ ‖deriv f 0‖ < 1
Tactic:
have g'0_ne_0 : deriv g 0 ≠ 0 := λ h' => by simp [h'] at h
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
g_lin : EqOn g (fun z => z • deriv g 0) (ball 0 1)
g'0_ne_0 : deriv g 0 ≠ 0
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
g_lin : EqOn g (fun z => z • deriv g 0) (ball 0 1)
g'0_ne_0 : deriv g 0 ≠ 0
⊢ ‖deriv f 0‖ < 1
Tactic:
have g_inj : InjOn g 𝔻 := λ x hx y hy => by
  rw [g_lin hx, g_lin hy]
  simp [g'0_ne_0]
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
g_lin : EqOn g (fun z => z • deriv g 0) (ball 0 1)
g'0_ne_0 : deriv g 0 ≠ 0
g_inj : InjOn g 𝔻
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
g_lin : EqOn g (fun z => z • deriv g 0) (ball 0 1)
g'0_ne_0 : deriv g 0 ≠ 0
g_inj : InjOn g 𝔻
⊢ ‖deriv f 0‖ < 1
Tactic:
cases f_noninj (injOn_of_injOn_comp g_inj)
State after:
no goals

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
⊢ EqOn g (fun z => z • deriv g 0) (ball 0 1)
Tactic:
have h2 : MapsTo g (ball 0 1) (ball (g 0) 1) := by rwa [g_0_eq_0]
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
h2 : MapsTo g (ball 0 1) (ball (g 0) 1)
⊢ EqOn g (fun z => z • deriv g 0) (ball 0 1)

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
h2 : MapsTo g (ball 0 1) (ball (g 0) 1)
⊢ EqOn g (fun z => z • deriv g 0) (ball 0 1)
Tactic:
have h1 : Set.EqOn g (fun z => g 0 + (z - 0) • dslope g 0 0) (Metric.ball 0 1) := by
  apply affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div g_diff h2 (mem_ball_self zero_lt_one)
  rwa [dslope_same, div_one]
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
h2 : MapsTo g (ball 0 1) (ball (g 0) 1)
h1 : EqOn g (fun z => g 0 + (z - 0) • dslope g 0 0) (ball 0 1)
⊢ EqOn g (fun z => z • deriv g 0) (ball 0 1)

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
h2 : MapsTo g (ball 0 1) (ball (g 0) 1)
h1 : EqOn g (fun z => g 0 + (z - 0) • dslope g 0 0) (ball 0 1)
⊢ EqOn g (fun z => z • deriv g 0) (ball 0 1)
Tactic:
convert h1 using 1
State after:
case h.e'_4
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
h2 : MapsTo g (ball 0 1) (ball (g 0) 1)
h1 : EqOn g (fun z => g 0 + (z - 0) • dslope g 0 0) (ball 0 1)
⊢ (fun z => z • deriv g 0) = fun z => g 0 + (z - 0) • dslope g 0 0

State before:
case h.e'_4
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
h2 : MapsTo g (ball 0 1) (ball (g 0) 1)
h1 : EqOn g (fun z => g 0 + (z - 0) • dslope g 0 0) (ball 0 1)
⊢ (fun z => z • deriv g 0) = fun z => g 0 + (z - 0) • dslope g 0 0
Tactic:
ext1 z
State after:
case h.e'_4.h
z✝ u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
h2 : MapsTo g (ball 0 1) (ball (g 0) 1)
h1 : EqOn g (fun z => g 0 + (z - 0) • dslope g 0 0) (ball 0 1)
z : ℂ
⊢ z • deriv g 0 = g 0 + (z - 0) • dslope g 0 0

State before:
case h.e'_4.h
z✝ u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
h2 : MapsTo g (ball 0 1) (ball (g 0) 1)
h1 : EqOn g (fun z => g 0 + (z - 0) • dslope g 0 0) (ball 0 1)
z : ℂ
⊢ z • deriv g 0 = g 0 + (z - 0) • dslope g 0 0
Tactic:
rw [g_0_eq_0, zero_add, sub_zero, dslope_same]
State after:
no goals

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
⊢ MapsTo g (ball 0 1) (ball (g 0) 1)
Tactic:
rwa [g_0_eq_0]
State after:
no goals

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
h2 : MapsTo g (ball 0 1) (ball (g 0) 1)
⊢ EqOn g (fun z => g 0 + (z - 0) • dslope g 0 0) (ball 0 1)
Tactic:
apply affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div g_diff h2 (mem_ball_self zero_lt_one)
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
h2 : MapsTo g (ball 0 1) (ball (g 0) 1)
⊢ ‖dslope g 0 0‖ = 1 / 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
h2 : MapsTo g (ball 0 1) (ball (g 0) 1)
⊢ ‖dslope g 0 0‖ = 1 / 1
Tactic:
rwa [dslope_same, div_one]
State after:
no goals

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
g_lin : EqOn g (fun z => z • deriv g 0) (ball 0 1)
h' : deriv g 0 = 0
⊢ False
Tactic:
simp [h'] at h
State after:
no goals

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
g_lin : EqOn g (fun z => z • deriv g 0) (ball 0 1)
g'0_ne_0 : deriv g 0 ≠ 0
x : ℂ
hx : x ∈ 𝔻
y : ℂ
hy : y ∈ 𝔻
⊢ g x = g y → x = y
Tactic:
rw [g_lin hx, g_lin hy]
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
g_lin : EqOn g (fun z => z • deriv g 0) (ball 0 1)
g'0_ne_0 : deriv g 0 ≠ 0
x : ℂ
hx : x ∈ 𝔻
y : ℂ
hy : y ∈ 𝔻
⊢ (fun z => z • deriv g 0) x = (fun z => z • deriv g 0) y → x = y

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ‖deriv g 0‖ = 1
g_lin : EqOn g (fun z => z • deriv g 0) (ball 0 1)
g'0_ne_0 : deriv g 0 ≠ 0
x : ℂ
hx : x ∈ 𝔻
y : ℂ
hy : y ∈ 𝔻
⊢ (fun z => z • deriv g 0) x = (fun z => z • deriv g 0) y → x = y
Tactic:
simp [g'0_ne_0]
State after:
no goals

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬‖deriv g 0‖ = 1
⊢ ‖deriv f 0‖ < 1
Tactic:
rw [norm_eq_abs] at h
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
⊢ ‖deriv f 0‖ < 1
Tactic:
have g'0_le_1 := abs_deriv_le_one_of_mapsTo_ball g_diff g_maps g_0_eq_0 zero_lt_one
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
⊢ ‖deriv f 0‖ < 1
Tactic:
have g'0_lt_1 : abs (deriv g 0) < 1 := Ne.lt_of_le h g'0_le_1
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
⊢ ‖deriv f 0‖ < 1
Tactic:
have g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻) u * deriv f 0 :=
  deriv.comp 0 ((φ u_in_𝔻).is_diff.differentiableAt (isOpen_ball.mem_nhds u_in_𝔻))
    (f_diff.differentiableAt (ball_mem_nhds _ zero_lt_one))
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
⊢ ‖deriv f 0‖ < 1
Tactic:
have e1 : 1 - (normSq u : ℂ) ≠ 0 := by
  simpa [normSq_eq_conj_mul_self, mul_comm] using one_sub_mul_conj_ne_zero u_in_𝔻 u_in_𝔻
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
⊢ ‖deriv f 0‖ < 1
Tactic:
have φ'u_u : deriv (φ u_in_𝔻) u = 1 / (1 - normSq u) := by
  set w := 1 - conj u * u with hw
  have : w ≠ 0 := by simpa [normSq_eq_conj_mul_self, mul_comm u] using e1
  rw [φ_deriv u_in_𝔻 u_in_𝔻, normSq_eq_conj_mul_self, mul_comm u, ← hw]
  field_simp; ring
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
⊢ ‖deriv f 0‖ < 1
Tactic:
have e2 : 0 ≤ normSq u := normSq_nonneg _
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
⊢ ‖deriv f 0‖ < 1
Tactic:
have e3 : normSq u < 1 := by
  rw [normSq_eq_abs]
  have : abs u < 1 := mem_𝔻_iff.mp u_in_𝔻
  simp only [sq_lt_one_iff_abs_lt_one, Complex.abs_abs, this]
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
⊢ ‖deriv f 0‖ < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
⊢ ‖deriv f 0‖ < 1
Tactic:
simp [normSq_eq_abs, ← mem_𝔻_iff]
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
⊢ Complex.abs (deriv f 0) < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
⊢ Complex.abs (deriv f 0) < 1
Tactic:
simp only [φ'u_u, one_div] at g'0_eq_mul
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv g 0 = (1 - ↑(normSq u))⁻¹ * deriv f 0
⊢ Complex.abs (deriv f 0) < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv g 0 = (1 - ↑(normSq u))⁻¹ * deriv f 0
⊢ Complex.abs (deriv f 0) < 1
Tactic:
rw [eq_comm, inv_mul_eq_iff_eq_mul₀ e1] at g'0_eq_mul
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ Complex.abs (deriv f 0) < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ Complex.abs (deriv f 0) < 1
Tactic:
rw [← norm_eq_abs, g'0_eq_mul, norm_mul, mul_comm, ← one_mul (1 : ℝ)]
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ ‖deriv g 0‖ * ‖1 - ↑(normSq u)‖ < 1 * 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ ‖deriv g 0‖ * ‖1 - ↑(normSq u)‖ < 1 * 1
Tactic:
refine mul_lt_mul g'0_lt_1 ?_ (norm_pos_iff.mpr e1) zero_le_one
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ ‖1 - ↑(normSq u)‖ ≤ 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ ‖1 - ↑(normSq u)‖ ≤ 1
Tactic:
simp at e2 e3 ⊢
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ Complex.abs (1 - ↑(normSq u)) ≤ 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ Complex.abs (1 - ↑(normSq u)) ≤ 1
Tactic:
norm_cast
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ |1 - normSq u| ≤ 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ |1 - normSq u| ≤ 1
Tactic:
rw [abs_sub_le_iff]
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ 1 - normSq u ≤ 1 ∧ normSq u - 1 ≤ 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ 1 - normSq u ≤ 1 ∧ normSq u - 1 ≤ 1
Tactic:
refine ⟨?_, ?_⟩
State after:
case refine_1
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ 1 - normSq u ≤ 1

case refine_2
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ normSq u - 1 ≤ 1

State before:
case refine_1
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ 1 - normSq u ≤ 1

case refine_2
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ normSq u - 1 ≤ 1
Tactic:
repeat linarith
State after:
no goals

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
⊢ 1 - ↑(normSq u) ≠ 0
Tactic:
simpa [normSq_eq_conj_mul_self, mul_comm] using one_sub_mul_conj_ne_zero u_in_𝔻 u_in_𝔻
State after:
no goals

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
⊢ deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
Tactic:
set w := 1 - conj u * u with hw
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
w : ℂ := 1 - (starRingEnd ℂ) u * u
hw : w = 1 - (starRingEnd ℂ) u * u
⊢ deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
w : ℂ := 1 - (starRingEnd ℂ) u * u
hw : w = 1 - (starRingEnd ℂ) u * u
⊢ deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
Tactic:
have : w ≠ 0 := by simpa [normSq_eq_conj_mul_self, mul_comm u] using e1
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
w : ℂ := 1 - (starRingEnd ℂ) u * u
hw : w = 1 - (starRingEnd ℂ) u * u
this : w ≠ 0
⊢ deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
w : ℂ := 1 - (starRingEnd ℂ) u * u
hw : w = 1 - (starRingEnd ℂ) u * u
this : w ≠ 0
⊢ deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
Tactic:
rw [φ_deriv u_in_𝔻 u_in_𝔻, normSq_eq_conj_mul_self, mul_comm u, ← hw]
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
w : ℂ := 1 - (starRingEnd ℂ) u * u
hw : w = 1 - (starRingEnd ℂ) u * u
this : w ≠ 0
⊢ w / w ^ 2 = 1 / w

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
w : ℂ := 1 - (starRingEnd ℂ) u * u
hw : w = 1 - (starRingEnd ℂ) u * u
this : w ≠ 0
⊢ w / w ^ 2 = 1 / w
Tactic:
field_simp
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
w : ℂ := 1 - (starRingEnd ℂ) u * u
hw : w = 1 - (starRingEnd ℂ) u * u
this : w ≠ 0
⊢ w * w = w ^ 2

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
w : ℂ := 1 - (starRingEnd ℂ) u * u
hw : w = 1 - (starRingEnd ℂ) u * u
this : w ≠ 0
⊢ w * w = w ^ 2
Tactic:
ring
State after:
no goals

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
w : ℂ := 1 - (starRingEnd ℂ) u * u
hw : w = 1 - (starRingEnd ℂ) u * u
⊢ w ≠ 0
Tactic:
simpa [normSq_eq_conj_mul_self, mul_comm u] using e1
State after:
no goals

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
⊢ normSq u < 1
Tactic:
rw [normSq_eq_abs]
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
⊢ Complex.abs u ^ 2 < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
⊢ Complex.abs u ^ 2 < 1
Tactic:
have : abs u < 1 := mem_𝔻_iff.mp u_in_𝔻
State after:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
this : Complex.abs u < 1
⊢ Complex.abs u ^ 2 < 1

State before:
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
g'0_eq_mul : deriv g 0 = deriv (φ u_in_𝔻).to_fun u * deriv f 0
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
this : Complex.abs u < 1
⊢ Complex.abs u ^ 2 < 1
Tactic:
simp only [sq_lt_one_iff_abs_lt_one, Complex.abs_abs, this]
State after:
no goals

State before:
case refine_2
z u✝ z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
f : ℂ → ℂ
f_diff : DifferentiableOn ℂ f 𝔻
f_img : MapsTo f 𝔻 𝔻
f_noninj : ¬InjOn f 𝔻
u : ℂ := f 0
u_in_𝔻 : u ∈ 𝔻
g : ℂ → ℂ := (φ u_in_𝔻).to_fun ∘ f
g_diff : DifferentiableOn ℂ g 𝔻
g_maps : MapsTo g 𝔻 𝔻
g_0_eq_0 : g 0 = 0
h : ¬Complex.abs (deriv g 0) = 1
g'0_le_1 : Complex.abs (deriv g 0) ≤ 1
g'0_lt_1 : Complex.abs (deriv g 0) < 1
e1 : 1 - ↑(normSq u) ≠ 0
φ'u_u : deriv (φ u_in_𝔻).to_fun u = 1 / (1 - ↑(normSq u))
e2 : 0 ≤ normSq u
e3 : normSq u < 1
g'0_eq_mul : deriv f 0 = (1 - ↑(normSq u)) * deriv g 0
⊢ normSq u - 1 ≤ 1
Tactic:
linarith
State after:
no goals