case a
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℂ
hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ᶠ (x : α) in l, f x = 0 → b.re = 0 → b = 0) ↔ b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℂ
hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
⊢ ∀ᶠ (x : α) in l, f x = 0 → b.re = 0 → b = 0
convert hl
case a
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℂ
hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ᶠ (x : α) in l, f x = 0) → b.re = 0 → b = 0 ↔ b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
case a
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℂ
hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∀ᶠ (x : α) in l, f x = 0 → b.re = 0 → b = 0) ↔ b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
rw [eventually_imp_distrib_right]
no goals
case a
α : Type u_1
l : Filter α
f g : α → ℂ
b : ℂ
hl : b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
⊢ (∃ᶠ (x : α) in l, f x = 0) → b.re = 0 → b = 0 ↔ b.re = 0 → b ≠ 0 → ∀ᶠ (x : α) in l, f x ≠ 0
tauto