internlm/Lean-Github huggingface dataset:
Theorem: montel
Proof state before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
⊢ range F ⊆ 𝓑 U Q
Tactic:
rintro f ⟨i, rfl⟩
Proof state after:
case intro
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
i : ι
⊢ F i ∈ 𝓑 U Q
Theorem: montel
Proof state before:
case intro
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q✝ : Set ℂ → Set ℂ
hU : IsOpen U
h2 : ∀ (i : ι), DifferentiableOn ℂ (F i) U
Q : Set ℂ → Set ℂ
hQ1 : ∀ K ∈ compacts U, IsCompact (Q K)
hQ2 : ∀ K ∈ compacts U, ∀ (i : ι), MapsTo (F i) K (Q K)
i : ι
⊢ F i ∈ 𝓑 U Q
Tactic:
exact ⟨h2 i, fun K hK => hQ2 K hK i⟩
Proof state after:
no goals
Theorem: isCompact_𝓜
Proof state before:
ι : Type u_1
U K : Set ℂ
z : ℂ
F : ι → 𝓒 U
Q : Set ℂ → Set ℂ
hU : IsOpen U
⊢ IsCompact (𝓜 U)
Tactic:
simpa only [𝓑_const] using isCompact_𝓑 hU (fun _ _ => isCompact_closedBall 0 1)
Proof state after:
no goals
Theorem: neg_in_𝔻
Proof state before:
u : ℂ
U V W : Set ℂ
⊢ u ∈ 𝔻 → -u ∈ 𝔻
Tactic:
simp [𝔻]
Proof state after:
no goals
Theorem: sqrt_𝔻_eq_𝔻
Proof state before:
u : ℂ
U V W : Set ℂ
⊢ {z | z ^ 2 ∈ 𝔻} = 𝔻
Tactic:
simp [𝔻, ball]
Proof state after:
no goals
Theorem: ne_center_of_not_mem_closed_ball
Proof state before:
u : ℂ
U V W : Set ℂ
w : ℂ
r : ℝ
hr : 0 ≤ r
z : ℂ
hz : z ∈ (closedBall w r)ᶜ
⊢ z ≠ w
Tactic:
contrapose! hz
Proof state after:
u : ℂ
U V W : Set ℂ
w : ℂ
r : ℝ
hr : 0 ≤ r
z : ℂ
hz : z = w
⊢ z ∉ (closedBall w r)ᶜ
Theorem: ne_center_of_not_mem_closed_ball
Proof state before:
u : ℂ
U V W : Set ℂ
w : ℂ
r : ℝ
hr : 0 ≤ r
z : ℂ
hz : z = w
⊢ z ∉ (closedBall w r)ᶜ
Tactic:
simp [hz, hr]
Proof state after:
no goals
Theorem: one_sub_mul_conj_ne_zero
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
⊢ 1 - z * (starRingEnd ℂ) u ≠ 0
Tactic:
rw [mem_𝔻_iff] at hu hz
Proof state after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : ‖u‖ < 1
hz : ‖z‖ < 1
⊢ 1 - z * (starRingEnd ℂ) u ≠ 0
Theorem: one_sub_mul_conj_ne_zero
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : ‖u‖ < 1
hz : ‖z‖ < 1
⊢ 1 - z * (starRingEnd ℂ) u ≠ 0
Tactic:
refine sub_ne_zero.mpr (mt (congr_arg Complex.abs) (ne_comm.mp (ne_of_lt ?_)))
Proof state after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : ‖u‖ < 1
hz : ‖z‖ < 1
⊢ Complex.abs (z * (starRingEnd ℂ) u) < Complex.abs 1
Theorem: one_sub_mul_conj_ne_zero
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : ‖u‖ < 1
hz : ‖z‖ < 1
⊢ Complex.abs (z * (starRingEnd ℂ) u) < Complex.abs 1
Tactic:
simpa using mul_lt_mul'' hz hu (norm_nonneg z) (norm_nonneg u)
Proof state after:
no goals
Theorem: one_sub_mul_conj_add_mul_conj_ne_zero
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
⊢ 1 - z * (starRingEnd ℂ) u + (z - u) * (starRingEnd ℂ) u ≠ 0
Tactic:
have h1 := one_sub_mul_conj_ne_zero hu hu
Proof state after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
h1 : 1 - u * (starRingEnd ℂ) u ≠ 0
⊢ 1 - z * (starRingEnd ℂ) u + (z - u) * (starRingEnd ℂ) u ≠ 0
Theorem: one_sub_mul_conj_add_mul_conj_ne_zero
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
h1 : 1 - u * (starRingEnd ℂ) u ≠ 0
⊢ 1 - z * (starRingEnd ℂ) u + (z - u) * (starRingEnd ℂ) u ≠ 0
Tactic:
ring_nf
Proof state after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
h1 : 1 - u * (starRingEnd ℂ) u ≠ 0
⊢ 1 - (starRingEnd ℂ) u * u ≠ 0
Theorem: one_sub_mul_conj_add_mul_conj_ne_zero
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
h1 : 1 - u * (starRingEnd ℂ) u ≠ 0
⊢ 1 - (starRingEnd ℂ) u * u ≠ 0
Tactic:
simp [h1, mul_comm]
Proof state after:
no goals
Theorem: normSq_sub_normSq
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
⊢ normSq (z - u) - normSq (1 - z * (starRingEnd ℂ) u) = (normSq z - 1) * (1 - normSq u)
Tactic:
field_simp [← ofReal_inj, normSq_eq_conj_mul_self]
Proof state after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
⊢ ((starRingEnd ℂ) z - (starRingEnd ℂ) u) * (z - u) - (1 - (starRingEnd ℂ) z * u) * (1 - z * (starRingEnd ℂ) u) =
    ((starRingEnd ℂ) z * z - 1) * (1 - (starRingEnd ℂ) u * u)
Theorem: normSq_sub_normSq
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
⊢ ((starRingEnd ℂ) z - (starRingEnd ℂ) u) * (z - u) - (1 - (starRingEnd ℂ) z * u) * (1 - z * (starRingEnd ℂ) u) =
    ((starRingEnd ℂ) z * z - 1) * (1 - (starRingEnd ℂ) u * u)
Tactic:
ring
Proof state after:
no goals
Theorem: pre_φ_inv
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
⊢ LeftInvOn (pre_φ (-u)) (pre_φ u) 𝔻
Tactic:
rintro z hz
Proof state after:
z✝ u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
z : ℂ
hz : z ∈ 𝔻
⊢ pre_φ (-u) (pre_φ u z) = z
Theorem: pre_φ_inv
Proof state before:
z✝ u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
z : ℂ
hz : z ∈ 𝔻
⊢ pre_φ (-u) (pre_φ u z) = z
Tactic:
field_simp [pre_φ, one_sub_mul_conj_ne_zero hu hz, one_sub_mul_conj_add_mul_conj_ne_zero hu]
Proof state after:
z✝ u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
z : ℂ
hz : z ∈ 𝔻
⊢ z - u + (1 - z * (starRingEnd ℂ) u) * u = z * (1 - z * (starRingEnd ℂ) u + (z - u) * (starRingEnd ℂ) u)
Theorem: pre_φ_inv
Proof state before:
z✝ u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
z : ℂ
hz : z ∈ 𝔻
⊢ z - u + (1 - z * (starRingEnd ℂ) u) * u = z * (1 - z * (starRingEnd ℂ) u + (z - u) * (starRingEnd ℂ) u)
Tactic:
ring
Proof state after:
no goals
Theorem: φ_deriv
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
⊢ deriv (φ hu).to_fun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
Tactic:
have h1 : DifferentiableAt ℂ (fun z => z - u) z := by simp
Proof state after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
⊢ deriv (φ hu).to_fun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
Theorem: φ_deriv
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
⊢ deriv (φ hu).to_fun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
Tactic:
have h2 : DifferentiableAt ℂ (fun z => 1 - z * conj u) z := by simp [DifferentiableAt.mul_const]
Proof state after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
⊢ deriv (φ hu).to_fun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
Theorem: φ_deriv
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
⊢ deriv (φ hu).to_fun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
Tactic:
have h3 : 1 - z * conj u ≠ 0 := one_sub_mul_conj_ne_zero hu hz
Proof state after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
⊢ deriv (φ hu).to_fun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
Theorem: φ_deriv
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
⊢ deriv (φ hu).to_fun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
Tactic:
have h4 : deriv (fun z => z - u) z = 1 := by simp [deriv_sub_const]
Proof state after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
h4 : deriv (fun z => z - u) z = 1
⊢ deriv (φ hu).to_fun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
Theorem: φ_deriv
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
h4 : deriv (fun z => z - u) z = 1
⊢ deriv (φ hu).to_fun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
Tactic:
have h5 : deriv (fun z => 1 - z * conj u) z = - conj u := by simp [deriv_const_sub]
Proof state after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
h4 : deriv (fun z => z - u) z = 1
h5 : deriv (fun z => 1 - z * (starRingEnd ℂ) u) z = -(starRingEnd ℂ) u
⊢ deriv (φ hu).to_fun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
Theorem: φ_deriv
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
h4 : deriv (fun z => z - u) z = 1
h5 : deriv (fun z => 1 - z * (starRingEnd ℂ) u) z = -(starRingEnd ℂ) u
⊢ deriv (φ hu).to_fun z = (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
Tactic:
simp [φ, deriv_div h1 h2 h3, h4, h5]
Proof state after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
h4 : deriv (fun z => z - u) z = 1
h5 : deriv (fun z => 1 - z * (starRingEnd ℂ) u) z = -(starRingEnd ℂ) u
⊢ (1 - z * (starRingEnd ℂ) u + (z - u) * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2 =
    (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
Theorem: φ_deriv
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
h4 : deriv (fun z => z - u) z = 1
h5 : deriv (fun z => 1 - z * (starRingEnd ℂ) u) z = -(starRingEnd ℂ) u
⊢ (1 - z * (starRingEnd ℂ) u + (z - u) * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2 =
    (1 - u * (starRingEnd ℂ) u) / (1 - z * (starRingEnd ℂ) u) ^ 2
Tactic:
field_simp [h3]
Proof state after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
h4 : deriv (fun z => z - u) z = 1
h5 : deriv (fun z => 1 - z * (starRingEnd ℂ) u) z = -(starRingEnd ℂ) u
⊢ 1 - z * (starRingEnd ℂ) u + (z - u) * (starRingEnd ℂ) u = 1 - u * (starRingEnd ℂ) u
Theorem: φ_deriv
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
h4 : deriv (fun z => z - u) z = 1
h5 : deriv (fun z => 1 - z * (starRingEnd ℂ) u) z = -(starRingEnd ℂ) u
⊢ 1 - z * (starRingEnd ℂ) u + (z - u) * (starRingEnd ℂ) u = 1 - u * (starRingEnd ℂ) u
Tactic:
ring
Proof state after:
no goals
Theorem: φ_deriv
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
⊢ DifferentiableAt ℂ (fun z => z - u) z
Tactic:
simp
Proof state after:
no goals
Theorem: φ_deriv
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
⊢ DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
Tactic:
simp [DifferentiableAt.mul_const]
Proof state after:
no goals
Theorem: φ_deriv
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
⊢ deriv (fun z => z - u) z = 1
Tactic:
simp [deriv_sub_const]
Proof state after:
no goals
Theorem: φ_deriv
Proof state before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
h1 : DifferentiableAt ℂ (fun z => z - u) z
h2 : DifferentiableAt ℂ (fun z => 1 - z * (starRingEnd ℂ) u) z
h3 : 1 - z * (starRingEnd ℂ) u ≠ 0
h4 : deriv (fun z => z - u) z = 1
⊢ deriv (fun z => 1 - z * (starRingEnd ℂ) u) z = -(starRingEnd ℂ) u
Tactic:
simp [deriv_const_sub]
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 𝔻
⊢ ‖deriv f 0‖ < 1
Tactic:
set u := f 0
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
⊢ ‖deriv f 0‖ < 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
⊢ ‖deriv f 0‖ < 1
Tactic:
have u_in_𝔻 : u ∈ 𝔻 := f_img (mem_ball_self zero_lt_one)
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 ∈ 𝔻
⊢ ‖deriv f 0‖ < 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 ∈ 𝔻
⊢ ‖deriv f 0‖ < 1
Tactic:
let g := φ u_in_𝔻 ∘ f
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
⊢ ‖deriv f 0‖ < 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
⊢ ‖deriv f 0‖ < 1
Tactic:
have g_diff : DifferentiableOn ℂ g 𝔻 := (φ u_in_𝔻).is_diff.comp f_diff f_img
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 𝔻
⊢ ‖deriv f 0‖ < 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 𝔻
⊢ ‖deriv f 0‖ < 1
Tactic:
have g_maps : MapsTo g 𝔻 𝔻 := (φ u_in_𝔻).maps_to.comp f_img
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 𝔻 𝔻
⊢ ‖deriv f 0‖ < 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 𝔻 𝔻
⊢ ‖deriv f 0‖ < 1
Tactic:
have g_0_eq_0 : g 0 = 0 := by simp [g, φ]
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
⊢ ‖deriv f 0‖ < 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
⊢ ‖deriv f 0‖ < 1
Tactic:
by_cases h : ‖deriv g 0‖ = 1
Proof 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
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 : ‖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)
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 : ¬‖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
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 = 0
Tactic:
simp [g, φ]
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 : ‖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]
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 : ‖deriv g 0‖ = 1
g_lin : EqOn g (fun z => z • deriv g 0) (ball 0 1)
⊢ ‖deriv f 0‖ < 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 : ‖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
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 : ‖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
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 : ‖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]
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 : ‖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
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 : ‖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)
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 : ‖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]
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 : ‖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)