Theorem: fast_products_converge' (Ray/Analytic/Products.lean)

State before:
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
⊢ ProdExistsOn f s ∧ AnalyticOn ℂ (tprodOn f) s ∧ ∀ z ∈ s, tprodOn f z ≠ 0
Tactic:
rcases fast_products_converge o c12 a0 a1 h hf with ⟨g, gp, ga, g0⟩
State after:
case intro.intro.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ ProdExistsOn f s ∧ AnalyticOn ℂ (tprodOn f) s ∧ ∀ z ∈ s, tprodOn f z ≠ 0

State before:
case intro.intro.intro
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ ProdExistsOn f s ∧ AnalyticOn ℂ (tprodOn f) s ∧ ∀ z ∈ s, tprodOn f z ≠ 0
Tactic:
refine ⟨?_, ?_, ?_⟩
State after:
case intro.intro.intro.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ ProdExistsOn f s

case intro.intro.intro.refine_2
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ AnalyticOn ℂ (tprodOn f) s

case intro.intro.intro.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ ∀ z ∈ s, tprodOn f z ≠ 0

State before:
case intro.intro.intro.refine_1
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ ProdExistsOn f s
Tactic:
exact fun z zs ↦ ⟨g z, gp z zs⟩
State after:
no goals

State before:
case intro.intro.intro.refine_2
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ AnalyticOn ℂ (tprodOn f) s
Tactic:
rwa [← analyticOn_congr o fun z zs ↦ (gp.tprodOn_eq z zs).symm]
State after:
no goals

State before:
case intro.intro.intro.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
⊢ ∀ z ∈ s, tprodOn f z ≠ 0
Tactic:
intro z zs
State after:
case intro.intro.intro.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
z : ℂ
zs : z ∈ s
⊢ tprodOn f z ≠ 0

State before:
case intro.intro.intro.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
z : ℂ
zs : z ∈ s
⊢ tprodOn f z ≠ 0
Tactic:
rw [gp.tprodOn_eq z zs]
State after:
case intro.intro.intro.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
z : ℂ
zs : z ∈ s
⊢ g z ≠ 0

State before:
case intro.intro.intro.refine_3
f : ℕ → ℂ → ℂ
s : Set ℂ
c a : ℝ
o : IsOpen s
c12 : c ≤ 1 / 2
a0 : 0 ≤ a
a1 : a < 1
h : ∀ (n : ℕ), AnalyticOn ℂ (f n) s
hf : ∀ (n : ℕ), ∀ z ∈ s, Complex.abs (f n z - 1) ≤ c * a ^ n
g : ℂ → ℂ
gp : HasProdOn (fun n => f n) g s
ga : AnalyticOn ℂ g s
g0 : ∀ z ∈ s, g z ≠ 0
z : ℂ
zs : z ∈ s
⊢ g z ≠ 0
Tactic:
exact g0 z zs
State after:
no goals