Theorem: order_eq_zero_iff (RMT4/hurwitz.lean)

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ ∀ᶠ (z : ℂ) in 𝓝 z₀, f z = 0
Tactic:
rw [hp.locally_zero_iff]
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0
Tactic:
by_cases h : p = 0
State after:
case pos
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : p = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0

case neg
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : p = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0
Tactic:
case pos => simp [h]
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0
Tactic:
case neg =>
  simp [FormalMultilinearSeries.order_eq_zero_iff h, h]
  ext1
  rw [hp.coeff_zero, hz₀]; rfl
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : p = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0
Tactic:
simp [h]
State after:
no goals

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
⊢ FormalMultilinearSeries.order p = 0 ↔ p = 0
Tactic:
simp [FormalMultilinearSeries.order_eq_zero_iff h, h]
State after:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
⊢ p 0 = 0

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
⊢ p 0 = 0
Tactic:
ext1
State after:
case H
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
x✝ : Fin 0 → ℂ
⊢ (p 0) x✝ = 0 x✝

State before:
case H
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
x✝ : Fin 0 → ℂ
⊢ (p 0) x✝ = 0 x✝
Tactic:
rw [hp.coeff_zero, hz₀]
State after:
case H
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
x✝ : Fin 0 → ℂ
⊢ 0 = 0 x✝

State before:
case H
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p✝ : Filter ι
r : ℝ
U : Set ℂ
p : FormalMultilinearSeries ℂ ℂ ℂ
hp : HasFPowerSeriesAt f p z₀
hz₀ : f z₀ = 0
h : ¬p = 0
x✝ : Fin 0 → ℂ
⊢ 0 = 0 x✝
Tactic:
rfl
State after:
no goals