Theorem: pre_φ_inv (RMT4/etape2.lean)

State before:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
⊢ LeftInvOn (pre_φ (-u)) (pre_φ u) 𝔻
Tactic:
rintro z hz
State after:
z✝ u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : u ∈ 𝔻
z : ℂ
hz : z ∈ 𝔻
⊢ pre_φ (-u) (pre_φ u z) = z

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

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