Theorem: one_sub_mul_conj_ne_zero (RMT4/etape2.lean)

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
State after:
z u z₀ : ℂ
U : Set ℂ
inst✝ : good_domain U
hu : ‖u‖ < 1
hz : ‖z‖ < 1
⊢ 1 - z * (starRingEnd ℂ) u ≠ 0

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 ?_)))
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

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