Theorem: φ_deriv (RMT4/etape2.lean)

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

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

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

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

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

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

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

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

State before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
hz : z ∈ 𝔻
⊢ DifferentiableAt ℂ (fun z => z - u) z
Tactic:
simp
State after:
no goals

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

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

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