-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
theorem tendsto_prod_nat_add [T2Space G] (f : ℕ → G) :
    Tendsto (fun i ↦ ∏' k, f (k + i)) atTop (𝓝 1)

Proof state:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
⊢ (fun i => (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j) = fun i => ∏' (k : ℕ), f (k + i)

Tactic:
ext1 i

Result:
case h
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
i : ℕ
⊢ (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j = ∏' (k : ℕ), f (k + i)

Proof state:
case pos
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
⊢ Tendsto (fun i => ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
have h₀ : (fun i ↦ (∏' i, f i) / ∏ j ∈ range i, f j) = fun i ↦ ∏' k : ℕ, f (k + i) := by
  ext1 i
  rw [div_eq_iff_eq_mul, mul_comm, prod_mul_tprod_nat_add i hf]

Result:
case pos
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
h₀ : (fun i => (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j) = fun i => ∏' (k : ℕ), f (k + i)
⊢ Tendsto (fun i => ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Proof state:
case pos
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
h₀ : (fun i => (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j) = fun i => ∏' (k : ℕ), f (k + i)
⊢ Tendsto (fun i => ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
have h₁ : Tendsto (fun _ : ℕ ↦ ∏' i, f i) atTop (𝓝 (∏' i, f i)) := tendsto_const_nhds

Result:
case pos
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
h₀ : (fun i => (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j) = fun i => ∏' (k : ℕ), f (k + i)
h₁ : Tendsto (fun x => ∏' (i : ℕ), f i) atTop (𝓝 (∏' (i : ℕ), f i))
⊢ Tendsto (fun i => ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Proof state:
case pos
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
h₀ : (fun i => (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j) = fun i => ∏' (k : ℕ), f (k + i)
h₁ : Tendsto (fun x => ∏' (i : ℕ), f i) atTop (𝓝 (∏' (i : ℕ), f i))
⊢ Tendsto (fun i => ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
simpa only [h₀, div_self'] using Tendsto.div' h₁ hf.hasProd.tendsto_prod_nat

Result:
no goals

Proof state:
case h
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
i : ℕ
⊢ (∏' (i : ℕ), f i) / ∏ j ∈ range i, f j = ∏' (k : ℕ), f (k + i)

Tactic:
rw [div_eq_iff_eq_mul, mul_comm, prod_mul_tprod_nat_add i hf]

Result:
no goals

Proof state:
case neg
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : ¬Multipliable f
⊢ Tendsto (fun i => ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
refine tendsto_const_nhds.congr fun n ↦ (tprod_eq_one_of_not_multipliable ?_).symm

Result:
case neg
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : ¬Multipliable f
n : ℕ
⊢ ¬Multipliable fun k => f (k + n)

Proof state:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
⊢ Tendsto (fun i => ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Tactic:
by_cases hf : Multipliable f

Result:
case pos
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : Multipliable f
⊢ Tendsto (fun i => ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

case neg
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : ¬Multipliable f
⊢ Tendsto (fun i => ∏' (k : ℕ), f (k + i)) atTop (𝓝 1)

Proof state:
case neg
G : Type u_2
inst✝³ : CommGroup G
inst✝² : TopologicalSpace G
inst✝¹ : IsTopologicalGroup G
inst✝ : T2Space G
f : ℕ → G
hf : ¬Multipliable f
n : ℕ
⊢ ¬Multipliable fun k => f (k + n)

Tactic:
rwa [multipliable_nat_add_iff n]

Result:
no goals