case intro.intro.intro.intro
𝓕 : Type ?u.1035259
𝕜 : Type ?u.1035262
α : Type ?u.1035265
ι : Type ?u.1035268
κ : Type ?u.1035271
E : Type u_1
F : Type u_2
G : Type ?u.1035280
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
j : E →* F
b : F
hb : b ∈ closure ↑(MonoidHom.range j)
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i in range (n + 1), v i) atTop (𝓝 b)
v_in : ∀ (n : ℕ), v n ∈ MonoidHom.range j
hv₀ : ‖v 0 / b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
⊢ ∃ a,
    Tendsto (fun n => ∏ i in range (n + 1), ↑j (a i)) atTop (𝓝 b) ∧
      ‖↑j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖↑j (a n)‖ < f n
𝓕 : Type ?u.1035259
𝕜 : Type ?u.1035262
α : Type ?u.1035265
ι : Type ?u.1035268
κ : Type ?u.1035271
E : Type u_1
F : Type u_2
G : Type ?u.1035280
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
j : E →* F
b : F
hb : b ∈ closure ↑(MonoidHom.range j)
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
⊢ ∃ a,
    Tendsto (fun n => ∏ i in range (n + 1), ↑j (a i)) atTop (𝓝 b) ∧
      ‖↑j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖↑j (a n)‖ < f n
obtain ⟨v, sum_v, v_in, hv₀, hv_pos⟩ := controlled_prod_of_mem_closure hb b_pos
case intro.intro.intro.intro
𝓕 : Type ?u.1035259
𝕜 : Type ?u.1035262
α : Type ?u.1035265
ι : Type ?u.1035268
κ : Type ?u.1035271
E : Type u_1
F : Type u_2
G : Type ?u.1035280
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
j : E →* F
b : F
hb : b ∈ closure ↑(MonoidHom.range j)
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i in 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 in range (n + 1), ↑j (a i)) atTop (𝓝 b) ∧
      ‖↑j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖↑j (a n)‖ < f n
case intro.intro.intro.intro
𝓕 : Type ?u.1035259
𝕜 : Type ?u.1035262
α : Type ?u.1035265
ι : Type ?u.1035268
κ : Type ?u.1035271
E : Type u_1
F : Type u_2
G : Type ?u.1035280
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
j : E →* F
b : F
hb : b ∈ closure ↑(MonoidHom.range j)
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i in range (n + 1), v i) atTop (𝓝 b)
v_in : ∀ (n : ℕ), v n ∈ MonoidHom.range j
hv₀ : ‖v 0 / b‖ < f 0
hv_pos : ∀ (n : ℕ), 0 < n → ‖v n‖ < f n
⊢ ∃ a,
    Tendsto (fun n => ∏ i in range (n + 1), ↑j (a i)) atTop (𝓝 b) ∧
      ‖↑j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖↑j (a n)‖ < f n
choose g hg using v_in
no goals
case intro.intro.intro.intro
𝓕 : Type ?u.1035259
𝕜 : Type ?u.1035262
α : Type ?u.1035265
ι : Type ?u.1035268
κ : Type ?u.1035271
E : Type u_1
F : Type u_2
G : Type ?u.1035280
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
j : E →* F
b : F
hb : b ∈ closure ↑(MonoidHom.range j)
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i in 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 in range (n + 1), ↑j (a i)) atTop (𝓝 b) ∧
      ‖↑j (a 0) / b‖ < f 0 ∧ ∀ (n : ℕ), 0 < n → ‖↑j (a n)‖ < f n
refine'
  ⟨g, by simpa [← hg] using sum_v, by simpa [hg 0] using hv₀, fun n hn => by
    simpa [hg] using hv_pos n hn⟩
no goals
𝓕 : Type ?u.1035259
𝕜 : Type ?u.1035262
α : Type ?u.1035265
ι : Type ?u.1035268
κ : Type ?u.1035271
E : Type u_1
F : Type u_2
G : Type ?u.1035280
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
j : E →* F
b : F
hb : b ∈ closure ↑(MonoidHom.range j)
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i in 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 in range (n + 1), ↑j (g i)) atTop (𝓝 b)
simpa [← hg] using sum_v
no goals
𝓕 : Type ?u.1035259
𝕜 : Type ?u.1035262
α : Type ?u.1035265
ι : Type ?u.1035268
κ : Type ?u.1035271
E : Type u_1
F : Type u_2
G : Type ?u.1035280
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
j : E →* F
b : F
hb : b ∈ closure ↑(MonoidHom.range j)
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i in 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
simpa [hg 0] using hv₀
no goals
𝓕 : Type ?u.1035259
𝕜 : Type ?u.1035262
α : Type ?u.1035265
ι : Type ?u.1035268
κ : Type ?u.1035271
E : Type u_1
F : Type u_2
G : Type ?u.1035280
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b✝ b₁ b₂ : E
r r₁ r₂ : ℝ
j : E →* F
b : F
hb : b ∈ closure ↑(MonoidHom.range j)
f : ℕ → ℝ
b_pos : ∀ (n : ℕ), 0 < f n
v : ℕ → F
sum_v : Tendsto (fun n => ∏ i in 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
simpa [hg] using hv_pos n hn