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

Tactic:
by_cases hU'' : U = {z}

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 : 𝕜
hz : z ∈ U
hU'' : U = {z}
⊢ (∀ 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 : 𝕜
hz : z ∈ U
hU'' : ¬U = {z}
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

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
this : ∃ᶠ (w : 𝕜) in 𝓝[≠] z, f w = 0 ∨ g w = 0
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
cases frequently_or_distrib.mp this with
| inl h => exact Or.inl <| hf.eqOn_zero_of_preconnected_of_frequently_eq_zero hU hz h
| inr h => exact Or.inr <| hg.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
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
have : ∃ᶠ w in 𝓝[≠] z, w ∈ U :=
  frequently_mem_iff_neBot.mpr <| hU.preperfect_of_nontrivial hU'' z hz

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
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

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 = {z}
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0

Tactic:
apply (nontrivial_iff_ne_singleton hz).mpr at hU''

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
⊢ (∀ z ∈ U, f z = 0) ∨ ∀ z ∈ U, g z = 0