internlm/Lean-Github huggingface dataset:
Theorem: non_injective_schwarz
Proof 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
Proof 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
Theorem: non_injective_schwarz
Proof 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]
Proof 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
Theorem: non_injective_schwarz
Proof 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 ⟨?_, ?_⟩
Proof 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
Theorem: non_injective_schwarz
Proof 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
Proof state after:
no goals
Theorem: non_injective_schwarz
Proof 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_𝔻
Proof state after:
no goals
Theorem: non_injective_schwarz
Proof 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
Proof 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))
Theorem: non_injective_schwarz
Proof 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
Proof 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))
Theorem: non_injective_schwarz
Proof 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]
Proof 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
Theorem: non_injective_schwarz
Proof 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
Proof 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
Theorem: non_injective_schwarz
Proof 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
Proof state after:
no goals
Theorem: non_injective_schwarz
Proof 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
Proof state after:
no goals
Theorem: non_injective_schwarz
Proof 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]
Proof 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
Theorem: non_injective_schwarz
Proof 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_𝔻
Proof 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
Theorem: non_injective_schwarz
Proof 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]
Proof state after:
no goals
Theorem: non_injective_schwarz
Proof 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
Proof state after:
no goals
Theorem: step_2
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hz₀ : z₀ ∈ U
f : embedding U 𝔻
hf : f.to_fun '' U ⊂ 𝔻
⊢ ∃ 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
Proof 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₀‖
Theorem: step_2
Proof 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_𝔻
Proof 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₀‖
Theorem: step_2
Proof 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
Proof 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₀‖
Theorem: step_2
Proof 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 [φᵤ, φ]
Proof 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₀‖
Theorem: step_2
Proof 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
Proof 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₀‖
Theorem: step_2
Proof 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₀
Proof 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₀‖
Theorem: step_2
Proof 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₀
Proof 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₀‖
Theorem: step_2
Proof 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
Proof 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₀‖
Theorem: step_2
Proof 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, φ]
Proof 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₀‖