Theorem: one_sub_mul_conj_add_mul_conj_ne_zero (RMT4/etape2.lean)

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

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

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