𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
⊢ CauchySeq fun n => ∏ k in range (n + 1), u k
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
⊢ CauchySeq fun n => ∏ k in range (n + 1), u k
let d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
⊢ CauchySeq (d * fun n => ∏ k in range (n + 1), v k)
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
⊢ CauchySeq fun n => ∏ k in range (n + 1), u k
rw [show (fun n => ∏ k in range (n + 1), u k) = d * fun n => ∏ k in range (n + 1), v k
    by ext n; simp]
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
⊢ ∀ (n : ℕ), n ≥ N → d n = d N
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
⊢ CauchySeq (d * fun n => ∏ k in range (n + 1), v k)
suffices ∀ n ≥ N, d n = d N by exact (tendsto_atTop_of_eventually_const this).cauchySeq.mul hv
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
⊢ d n = d N
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
⊢ ∀ (n : ℕ), n ≥ N → d n = d N
intro n hn
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
⊢ ∏ k in range (n + 1), u k / v k = ∏ k in range (N + 1), u k / v k
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
⊢ d n = d N
dsimp
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
⊢ ∀ (n : ℕ), n ≥ N → u n / v n = 1
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
⊢ ∏ k in range (n + 1), u k / v k = ∏ k in range (N + 1), u k / v k
rw [eventually_constant_prod _ hn]
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
m : ℕ
hm : m ≥ N
⊢ u m / v m = 1
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
⊢ ∀ (n : ℕ), n ≥ N → u n / v n = 1
intro m hm
no goals
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
n : ℕ
hn : n ≥ N
m : ℕ
hm : m ≥ N
⊢ u m / v m = 1
simp [huv m hm]
case h
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
n : ℕ
⊢ ∏ k in range (n + 1), u k = (d * fun n => ∏ k in range (n + 1), v k) n
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
⊢ (fun n => ∏ k in range (n + 1), u k) = d * fun n => ∏ k in range (n + 1), v k
ext n
no goals
case h
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
n : ℕ
⊢ ∏ k in range (n + 1), u k = (d * fun n => ∏ k in range (n + 1), v k) n
simp
no goals
𝓕 : Type ?u.1218103
𝕜 : Type ?u.1218106
α : Type ?u.1218109
ι : Type ?u.1218112
κ : Type ?u.1218115
E : Type u_1
F : Type ?u.1218121
G : Type ?u.1218124
inst✝¹ : SeminormedCommGroup E
inst✝ : SeminormedCommGroup F
a a₁ a₂ b b₁ b₂ : E
r r₁ r₂ : ℝ
u v : ℕ → E
N : ℕ
huv : ∀ (n : ℕ), n ≥ N → u n = v n
hv : CauchySeq fun n => ∏ k in range (n + 1), v k
d : ℕ → E := fun n => ∏ k in range (n + 1), u k / v k
this : ∀ (n : ℕ), n ≥ N → d n = d N
⊢ CauchySeq (d * fun n => ∏ k in range (n + 1), v k)
exact (tendsto_atTop_of_eventually_const this).cauchySeq.mul hv