-- Mathlib/Analysis/Analytic/IsolatedZeros.lean
/-- If `f, g` are analytic on a neighbourhood of the preconnected open set `U`, and `f • g = 0`
on `U`, then either `f = 0` on `U` or `g = 0` on `U`. -/
lemma eq_zero_or_eq_zero_of_smul_eq_zero [NoZeroSMulDivisors A B]
    {f : 𝕜 → A} {g : 𝕜 → B} (hf : AnalyticOnNhd 𝕜 f U) (hg : AnalyticOnNhd 𝕜 g U)
    (hfg : ∀ z ∈ U, f z • g z = 0) (hU : IsPreconnected U) :
    (∀ z ∈ U, f z = 0) ∨ (∀ z ∈ U, g z = 0)

Proof state:
case pos
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : NoZeroSMulDivisors A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U = {z}
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
simpa [hU''] using hfg z hz

Result:
no goals

Proof state:
case pos
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : NoZeroSMulDivisors A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : U = ∅
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
simp [hU']

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : NoZeroSMulDivisors A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
obtain ⟨z, hz⟩ : ∃ z, z ∈ U := nonempty_iff_ne_empty.mpr hU'

Result:
case neg.intro
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : NoZeroSMulDivisors A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : NoZeroSMulDivisors A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
by_cases hU' : U = ∅

Result:
case pos
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : NoZeroSMulDivisors A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : U = ∅
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

case neg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : NoZeroSMulDivisors A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Proof state:
case neg.inr
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : NoZeroSMulDivisors A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this✝ : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, f w = 0 ∨ g w = 0
h : ∃ᶠ (x : 𝕜) in 𝓝[≠] z, g x = 0
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
exact Or.inr <| hg.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : NoZeroSMulDivisors A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
⊢ ∀ᶠ (x : 𝕜) in 𝓝[≠] z, x ∈ U → f x = 0 ∨ g x = 0

Tactic:
filter_upwards with w hw using smul_eq_zero.mp (hfg w hw)

Result:
no goals

Proof state:
case neg.inl
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : NoZeroSMulDivisors A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this✝ : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, f w = 0 ∨ g w = 0
h : ∃ᶠ (x : 𝕜) in 𝓝[≠] z, f x = 0
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
exact Or.inl <| hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h

Result:
no goals

Proof state:
case neg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : NoZeroSMulDivisors A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
have : ∃ᶠ w in 𝓝[≠] z, f w = 0 ∨ g w = 0 :=
  this.mp <| by filter_upwards with w hw using smul_eq_zero.mp (hfg w hw)

Result:
case neg
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
U : Set 𝕜
A : Type u_3
inst✝⁵ : NormedRing A
inst✝⁴ : NormedAlgebra 𝕜 A
B : Type u_4
inst✝³ : NormedAddCommGroup B
inst✝² : NormedSpace 𝕜 B
inst✝¹ : Module A B
inst✝ : NoZeroSMulDivisors A B
f : 𝕜 → A
g : 𝕜 → B
hf : AnalyticOnNhd 𝕜 f U
hg : AnalyticOnNhd 𝕜 g U
hfg : ∀ z ∈ U, f z • g z = 0
hU : IsPreconnected U
hU' : ¬U = ∅
z : 𝕜
hz : z ∈ U
hU'' : U.Nontrivial
this✝ : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, w ∈ U
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, f w = 0 ∨ g w = 0
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0