-- Mathlib/Analysis/Normed/Group/Continuity.lean
theorem controlled_prod_of_mem_closure_range {j : E →* F} {b : F}
    (hb : b ∈ closure (j.range : Set F)) {f : ℕ → ℝ} (b_pos : ∀ n, 0 < f n) :
    ∃ a : ℕ → E,
      Tendsto (fun n => ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧
        ‖j (a 0) / b‖ < f 0 ∧ ∀ n, 0 < n → ‖j (a n)‖ < f n

Proof state:
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
hv₀ : ‖v 0 / b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
g : ℕ → E
hg : ∀ (n : ℕ), j (g n) = v n
⊢ Tendsto (fun n => ∏ i ∈ range (n + 1), j (g i)) atTop (𝓝 b)

Tactic:
simpa [← hg] using sum_v

Result:
no goals

Proof state:
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
hv₀ : ‖v 0 / b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
g : ℕ → E
hg : ∀ (n : ℕ), j (g n) = v n
⊢ ‖j (g 0) / b‖ < f 0

Tactic:
simpa [hg 0] using hv₀

Result:
no goals

Proof state:
case intro.intro.intro.intro
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
hv₀ : ‖v 0 / b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
g : ℕ → E
hg : ∀ (n : ℕ), j (g n) = v n
⊢ ∃ a,
    Tendsto (fun n => ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧
      ‖j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n

Tactic:
exact
  ⟨g, by simpa [← hg] using sum_v, by simpa [hg 0] using hv₀,
    fun n hn => by simpa [hg] using hv_pos n hn⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
v_in : ∀ (n : ℕ), v n ∈ j.range
hv₀ : ‖v 0 / b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
⊢ ∃ a,
    Tendsto (fun n => ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧
      ‖j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n

Tactic:
choose g hg using v_in

Result:
case intro.intro.intro.intro
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
hv₀ : ‖v 0 / b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
g : ℕ → E
hg : ∀ (n : ℕ), j (g n) = v n
⊢ ∃ a,
    Tendsto (fun n => ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧
      ‖j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n

Proof state:
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
⊢ ∃ a,
    Tendsto (fun n => ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧
      ‖j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n

Tactic:
obtain ⟨v, sum_v, v_in, hv₀, hv_pos⟩ := controlled_prod_of_mem_closure hb b_pos

Result:
case intro.intro.intro.intro
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
v_in : ∀ (n : ℕ), v n ∈ j.range
hv₀ : ‖v 0 / b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
⊢ ∃ a,
    Tendsto (fun n => ∏ i ∈ range (n + 1), j (a i)) atTop (𝓝 b) ∧
      ‖j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖j (a n)‖ < f n

Proof state:
E : Type u_5
F : Type u_6
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
j : E →* F
b : F
hb : b ∈ closure ↑j.range
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i ∈ range (n + 1), v i) atTop (𝓝 b)
hv₀ : ‖v 0 / b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
g : ℕ → E
hg : ∀ (n : ℕ), j (g n) = v n
n : ℕ
hn : 0 < n
⊢ ‖j (g n)‖ < f n

Tactic:
simpa [hg] using hv_pos n hn

Result:
no goals