awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CanonicallyOrderedMul α
inst_4 : TopologicalSpace α
inst_5 : OrderClosedTopology α
f : ι → α
⊢ HasProd f 1 ↔ ∀ (x : ι), f x = 1

Tactic:
(hasProd_one_iff_of_one_le fun _ ↦ one_le).trans funext_iff

Premises used: funext_iff, hasProd_one_iff_of_one_le, Iff.trans, one_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CanonicallyOrderedMul α
inst_4 : TopologicalSpace α
inst_5 : OrderClosedTopology α
f : ι → α
hf : Multipliable f
rw : Eq.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ HasProd f 1
rw₁ rw₂ : Eq.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ Eq.{u_3 + 1} (α := α) (∏' (b : ι), f b) 1
⊢ Eq.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ ∀ (x : ι), f x = 1

Tactic:
rw [← hasProd_one_iff, hf.hasProd_iff]

Premises used: Multipliable.hasProd_iff, hasProd_one_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : IsOrderedMonoid α
inst_3 : CanonicallyOrderedMul α
inst_4 : TopologicalSpace α
inst_5 : OrderClosedTopology α
f : ι → α
hf : Multipliable f
rw : ¬Eq.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ ∃ (x : ι), f x ≠ 1
rw₁ : (¬∀ (x : ι), f x = 1) ↔ ∃ (x : ι), f x ≠ 1
rw₂ rw₃ : (∃ (x : ι), ¬f x = 1) ↔ ∃ (x : ι), f x ≠ 1
⊢ Ne.{u_3 + 1} (α := α) (∏' (i : ι), f i) 1 ↔ ∃ (x : ι), f x ≠ 1

Tactic:
rw [Ne, hf.tprod_eq_one_iff, not_forall]

Premises used: Ne, Classical.not_forall, Multipliable.tprod_eq_one_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a : α
hf : HasProd f a
⊢ IsLUB (Set.range fun (s : Finset ι) ↦ ∏ i ∈ s, f i) a

Tactic:
isLUB_of_tendsto_atTop (Finset.prod_mono_set' f) hf

Premises used: Finset.prod_mono_set', isLUB_of_tendsto_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a : α
hf : HasProd f a
⊢ IsLUB (Set.range fun (s : Finset ι) ↦ ∏ i ∈ s, f i) a

Tactic:
exact isLUB_of_tendsto_atTop (Finset.prod_mono_set' f) hf

Premises used: Finset.prod_mono_set', isLUB_of_tendsto_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedMul α
inst_3 : TopologicalSpace α
inst_4 : OrderClosedTopology α
f : ι → α
a : α
hf : HasProd f a
⊢ IsLUB (Set.range fun (s : Finset ι) ↦ ∏ i ∈ s, f i) a

Tactic:
classical
  exact isLUB_of_tendsto_atTop (Finset.prod_mono_set' f) hf

Premises used: Finset.prod_mono_set', isLUB_of_tendsto_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : ι → α
i : α
h : ∀ (i : ι), 1 ≤ f i
hf : IsLUB (Set.range fun (s : Finset ι) ↦ ∏ i ∈ s, f i) i
⊢ HasProd f i

Tactic:
tendsto_atTop_isLUB (Finset.prod_mono_set_of_one_le' h) hf

Premises used: iInf, HasProd, Filter.atTop, tendsto_atTop_isLUB, Finset.prod_mono_set_of_one_le'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : ι → α
i : α
h₀ : ∀ (i : ι), f i ≤ 1
hf : IsGLB (Set.range fun (s : Finset ι) ↦ ∏ i ∈ s, f i) i
⊢ HasProd f i

Tactic:
tendsto_atTop_isGLB (Finset.prod_anti_set_of_le_one' h₀) hf

Premises used: iInf, HasProd, Finset.prod_anti_set_of_le_one', tendsto_atTop_isGLB, Filter.atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommMonoid α
inst_1 : LinearOrder α
inst_2 : CanonicallyOrderedMul α
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : ι → α
b : α
hf : IsLUB (Set.range fun (s : Finset ι) ↦ ∏ i ∈ s, f i) b
⊢ HasProd f b

Tactic:
tendsto_atTop_isLUB (Finset.prod_mono_set' f) hf

Premises used: iInf, HasProd, Filter.atTop, Finset.prod_mono_set', tendsto_atTop_isLUB
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : UniformSpace α
inst_4 : IsUniformGroup α
inst_5 : CompleteSpace α
f : ι → α
s : Set ι := {x : ι | 1 ≤ f x}
h1 : ∀ (x : (↑s : Type u_1)), |f (↑x : ι)|ₘ = f (↑x : ι)
h2 : ∀ (x : (↑sᶜ : Type u_1)), |f (↑x : ι)|ₘ = (f (↑x : ι))⁻¹
⊢ ((Multipliable.{u_3, u_1} (α := α) fun (x : (↑s : Type u_1)) ↦ |f (↑x : ι)|ₘ) ∧
      Multipliable.{u_3, u_1} (α := α) fun (x : (↑sᶜ : Type u_1)) ↦ |f (↑x : ι)|ₘ) ↔
    (Multipliable.{u_3, u_1} (α := α) fun (x : (↑s : Type u_1)) ↦ f (↑x : ι)) ∧
      Multipliable.{u_3, u_1} (α := α) fun (x : (↑sᶜ : Type u_1)) ↦ (f (↑x : ι))⁻¹

Tactic:
simp only [h1, h2]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedMonoid α
inst_3 : UniformSpace α
inst_4 : IsUniformGroup α
inst_5 : CompleteSpace α
f : ι → α
s : Set ι := {x : ι | 1 ≤ f x}
h1 : ∀ (x : (↑s : Type u_1)), |f (↑x : ι)|ₘ = f (↑x : ι)
h2 : ∀ (x : (↑sᶜ : Type u_1)), |f (↑x : ι)|ₘ = (f (↑x : ι))⁻¹
⊢ ((Multipliable.{u_3, u_1} (α := α) fun (x : (↑s : Type u_1)) ↦ f (↑x : ι)) ∧
      Multipliable.{u_3, u_1} (α := α) fun (x : (↑sᶜ : Type u_1)) ↦ (f (↑x : ι))⁻¹) ↔
    Multipliable f

Tactic:
simp only [multipliable_inv_iff, multipliable_subtype_and_compl]

Premises used: multipliable_subtype_and_compl, multipliable_inv_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : TopologicalSpace α
inst_4 : Archimedean α
inst_5 : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable.{u_3, u_1} (α := α) fun (x : ι) ↦ b
s : Finset ι
⊢ #s • b ≤ ∑' (x : ι), b

Tactic:
simpa using sum_le_hasSum s (fun a _ ↦ hb.le) hf.hasSum

Premises used: LT.lt.le, sum_le_hasSum, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : TopologicalSpace α
inst_4 : Archimedean α
inst_5 : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable.{u_3, u_1} (α := α) fun (x : ι) ↦ b
⊢ ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b

Tactic:
have H : ∀ s : Finset ι, #s • b ≤ ∑' _ : ι, b := fun s ↦ by
    simpa using sum_le_hasSum s (fun a _ ↦ hb.le) hf.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : TopologicalSpace α
inst_4 : Archimedean α
inst_5 : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable.{u_3, u_1} (α := α) fun (x : ι) ↦ b
H : ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b
obtain : ∀ (n : ℕ) (hn : ∑' (x : ι), b ≤ n • b), Finite ι
⊢ Finite ι

Tactic:
obtain ⟨n, hn⟩ := Archimedean.arch (∑' _ : ι, b) hb

Premises used: tsum, Archimedean.arch, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : TopologicalSpace α
inst_4 : Archimedean α
inst_5 : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable.{u_3, u_1} (α := α) fun (x : ι) ↦ b
H : ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
s : Finset ι
⊢ #s ≤ n

Tactic:
simpa [nsmul_le_nsmul_iff_left hb] using (H s).trans hn

Premises used: nsmul_le_nsmul_iff_left, LE.le.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : TopologicalSpace α
inst_4 : Archimedean α
inst_5 : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable.{u_3, u_1} (α := α) fun (x : ι) ↦ b
H : ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
⊢ ∀ (s : Finset ι), #s ≤ n

Tactic:
have : ∀ s : Finset ι, #s ≤ n := fun s ↦ by
    simpa [nsmul_le_nsmul_iff_left hb] using (H s).trans hn
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : TopologicalSpace α
inst_4 : Archimedean α
inst_5 : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable.{u_3, u_1} (α := α) fun (x : ι) ↦ b
H : ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
this : ∀ (s : Finset ι), #s ≤ n
have : ∀ (this : Fintype ι), Finite ι
⊢ Finite ι

Tactic:
have : Fintype ι := fintypeOfFinsetCardLe n this
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : TopologicalSpace α
inst_4 : Archimedean α
inst_5 : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable.{u_3, u_1} (α := α) fun (x : ι) ↦ b
H : ∀ (s : Finset ι), #s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
this_1 : ∀ (s : Finset ι), #s ≤ n
this : Fintype ι
⊢ Finite ι

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
inst_3 : TopologicalSpace α
inst_4 : Archimedean α
inst_5 : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable.{u_3, u_1} (α := α) fun (x : ι) ↦ b
⊢ Set.Finite.{u_1} (α := ι) univ

Tactic:
finite_univ_iff.2 <| .of_summable_const hb hf

Premises used: Iff.mpr, Finite.of_summable_const, Set.finite_univ_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : ι → α
x : α
hfx : HasProd f x
⊢ HasProd (fun (x : ι) ↦ |f x|) |x|

Tactic:
simpa only [HasProd, ← abs_prod] using hfx.abs

Premises used: HasProd, HasProd.abs, Finset.abs_prod, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : ι → α
hf : Multipliable f
⊢ Multipliable.{u_3, u_1} (α := α) fun (x : ι) ↦ |f x|

Tactic:
let ⟨x, hx⟩ := hf; ⟨|x|, hx.abs⟩

Premises used: _private.0.Multipliable.abs.match_1, abs, HasProd.abs, Multipliable, Exists.intro, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Order
Goal:
ι : Type u_1
α : Type u_3
inst : CommRing α
inst_1 : LinearOrder α
inst_2 : IsStrictOrderedRing α
inst_3 : TopologicalSpace α
inst_4 : OrderTopology α
f : ι → α
hf : Multipliable f
⊢ Eq.{u_3 + 1} (α := α) |∏' (i : ι), f i| (∏' (i : ι), |f i|)

Tactic:
hf.hasProd.abs.tprod_eq.symm

Premises used: HasProd.abs, HasProd.tprod_eq, Multipliable.hasProd, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
⊢ ∀ (i : ℕ), 0 ≤ d i

Tactic:
fun n ↦ dist_nonneg.trans (hf n)

Premises used: dist_nonneg, LE.le.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
lift :
  ∀ (d : (i : ℕ) → ℝ≥0) (hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun (i : ℕ) ↦ (↑(d i) : ℝ)) n)
    (hd : Summable (α := ℝ) fun (i : ℕ) ↦ (↑(d i) : ℝ)), CauchySeq f
⊢ CauchySeq f

Tactic:
lift d to ℕ → ℝ≥0 using fun n ↦ dist_nonneg.trans (hf n)

Premises used: dist_nonneg, LE.le.trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : (i : ℕ) → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun (i : ℕ) ↦ (↑(d i) : ℝ)) n
hd : Summable (α := ℝ) fun (i : ℕ) ↦ (↑(d i) : ℝ)
hf₁ : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (↑(d n) : ENNReal)
hd₁ : Summable d
⊢ CauchySeq f

Tactic:
apply cauchySeq_of_edist_le_of_summable d (α := α) (f := f)

Premises used: cauchySeq_of_edist_le_of_summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : (i : ℕ) → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun (i : ℕ) ↦ (↑(d i) : ℝ)) n
hd : Summable (α := ℝ) fun (i : ℕ) ↦ (↑(d i) : ℝ)
⊢ ∀ (n : ℕ), edist (f n) (f n.succ) ≤ (↑(d n) : ENNReal)

Tactic:
exact_mod_cast hf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : (i : ℕ) → ℝ≥0
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ (fun (i : ℕ) ↦ (↑(d i) : ℝ)) n
hd : Summable (α := ℝ) fun (i : ℕ) ↦ (↑(d i) : ℝ)
⊢ Summable d

Tactic:
exact_mod_cast hd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
h : Summable (α := ℝ) fun (n : ℕ) ↦ dist (f n) (f n.succ)
⊢ CauchySeq f

Tactic:
cauchySeq_of_dist_le_of_summable _ (fun _ ↦ le_rfl) h

Premises used: le_rfl, cauchySeq_of_dist_le_of_summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ ∑' (m : ℕ), d (n + m)

Tactic:
le_of_tendsto (tendsto_const_nhds.dist ha) (eventually_atTop.2 ⟨n, fun m hnm ↦ ?_⟩)

Premises used: Iff.mpr, tendsto_const_nhds, Filter.Tendsto.dist, le_of_tendsto, Exists.intro, Filter.eventually_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
refine : ∀ (m : ℕ) (hnm : m ≥ n), dist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)
⊢ dist (f n) a ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine le_of_tendsto (tendsto_const_nhds.dist ha) (eventually_atTop.2 ⟨n, fun m hnm ↦ ?_⟩)

Premises used: Iff.mpr, tendsto_const_nhds, Filter.Tendsto.dist, le_of_tendsto, Exists.intro, Filter.eventually_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ dist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)

Tactic:
le_trans (dist_le_Ico_sum_of_dist_le hnm fun _ _ ↦ hf _) ?_

Premises used: dist_le_Ico_sum_of_dist_le, le_trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
refine : LE.le (α := ℝ) (∑ i ∈ Ico n m, d i) (∑' (m : ℕ), d (n + m))
⊢ dist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)

Tactic:
refine le_trans (dist_le_Ico_sum_of_dist_le hnm fun _ _ ↦ hf _) ?_

Premises used: HAdd.hAdd, dist_le_Ico_sum_of_dist_le, OfNat.ofNat, le_trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
rw : LE.le (α := ℝ) (∑ k ∈ range (m - n), d (n + k)) (∑' (m : ℕ), d (n + m))
⊢ LE.le (α := ℝ) (∑ i ∈ Ico n m, d i) (∑' (m : ℕ), d (n + m))

Tactic:
rw [sum_Ico_eq_sum_range]

Premises used: Finset.sum_Ico_eq_sum_range
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ LE.le (α := ℝ) (∑ k ∈ range (m - n), d (n + k)) (∑' (m : ℕ), d (n + m))

Tactic:
Summable.sum_le_tsum (range _) (fun _ _ ↦ le_trans dist_nonneg (hf _)) ?_

Premises used: dist_nonneg, Finset.range, Summable.sum_le_tsum, HAdd.hAdd, le_trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
refine : Summable (α := ℝ) fun (k : ℕ) ↦ d (n + k)
⊢ LE.le (α := ℝ) (∑ k ∈ range (m - n), d (n + k)) (∑' (m : ℕ), d (n + m))

Tactic:
refine Summable.sum_le_tsum (range _) (fun _ _ ↦ le_trans dist_nonneg (hf _)) ?_

Premises used: dist_nonneg, Finset.range, Summable.sum_le_tsum, le_trans
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ Summable (α := ℝ) fun (k : ℕ) ↦ d (n + k)

Tactic:
hd.comp_injective (add_right_injective n)

Premises used: add_right_injective, Summable.comp_injective
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ Summable (α := ℝ) fun (k : ℕ) ↦ d (n + k)

Tactic:
exact hd.comp_injective (add_right_injective n)

Premises used: add_right_injective, Summable.comp_injective
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ tsum d

Tactic:
simpa only [zero_add] using dist_le_tsum_of_dist_le_of_tendsto d hf hd ha 0

Premises used: zero_add, dist_le_tsum_of_dist_le_of_tendsto, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
a : α
h : Summable (α := ℝ) fun (n : ℕ) ↦ dist (f n) (f n.succ)
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ ∑' (m : ℕ), dist (f (n + m)) (f (n + m).succ)

Tactic:
show dist (f n) a ≤ ∑' m, (fun x ↦ dist (f x) (f x.succ)) (n + m) from
    dist_le_tsum_of_dist_le_of_tendsto (fun n ↦ dist (f n) (f n.succ)) (fun _ ↦ le_rfl) h ha n

Premises used: le_rfl, dist_le_tsum_of_dist_le_of_tendsto, Dist.dist, Nat.succ
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_1
inst : PseudoMetricSpace α
f : ℕ → α
a : α
h : Summable (α := ℝ) fun (n : ℕ) ↦ dist (f n) (f n.succ)
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ ∑' (n : ℕ), dist (f n) (f n.succ)

Tactic:
simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0

Premises used: zero_add, dist_le_tsum_dist_of_tendsto, OfNat.ofNat
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
⊢ ∀ (i : ℕ), 0 ≤ f i

Tactic:
hf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
lift :
  ∀ (f : (i : ℕ) → ℝ≥0),
    (¬Summable (α := ℝ) fun (i : ℕ) ↦ (↑(f i) : ℝ)) ↔
      Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, (fun (i : ℕ) ↦ (↑(f i) : ℝ)) i) atTop atTop
⊢ ¬Summable f ↔ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop

Tactic:
lift f to ℕ → ℝ≥0 using hf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
f : (i : ℕ) → ℝ≥0
⊢ (¬Summable (α := ℝ) fun (i : ℕ) ↦ (↑(f i) : ℝ)) ↔
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, (fun (i : ℕ) ↦ (↑(f i) : ℝ)) i) atTop atTop

Tactic:
simpa using mod_cast NNReal.not_summable_iff_tendsto_nat_atTop

Premises used: NNReal.not_summable_iff_tendsto_nat_atTop
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
f : ℕ → ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
rw : ¬Summable f ↔ ¬¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop
rw₁ : ¬Summable f ↔ Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop
rw₂ rw₃ :
  Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop ↔
    Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop
⊢ Summable f ↔ ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop

Tactic:
rw [← not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop_of_nonneg hf]

Premises used: not_iff_not, Classical.not_not, not_summable_iff_tendsto_nat_atTop_of_nonneg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_4
β : α → Type u_3
f : (x : α) × β x → ℝ
hf : ∀ (x : (x : α) × β x), 0 ≤ f x
⊢ ∀ (i : (x : α) × β x), 0 ≤ f i

Tactic:
hf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_4
β : α → Type u_3
f : (x : α) × β x → ℝ
hf : ∀ (x : (x : α) × β x), 0 ≤ f x
lift :
  ∀ (f : (i : (x : α) × β x) → ℝ≥0),
    (Summable (α := ℝ) fun (i : (x : α) × β x) ↦ (↑(f i) : ℝ)) ↔
      (∀ (x : α),
          Summable (α := ℝ) fun (y : β x) ↦
            (fun (i : (x : α) × β x) ↦ (↑(f i) : ℝ)) (Sigma.mk (β := fun (x : α) ↦ β x) x y)) ∧
        Summable (α := ℝ) fun (x : α) ↦
          ∑' (y : β x), (fun (i : (x : α) × β x) ↦ (↑(f i) : ℝ)) (Sigma.mk (β := fun (x : α) ↦ β x) x y)
⊢ Summable f ↔
    (∀ (x : α), Summable (α := ℝ) fun (y : β x) ↦ f (Sigma.mk (β := fun (x : α) ↦ β x) x y)) ∧
      Summable (α := ℝ) fun (x : α) ↦ ∑' (y : β x), f (Sigma.mk (β := fun (x : α) ↦ β x) x y)

Tactic:
lift f to (Σ x, β x) → ℝ≥0 using hf
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_4
β : α → Type u_3
f : (i : (x : α) × β x) → ℝ≥0
⊢ (Summable (α := ℝ) fun (i : (x : α) × β x) ↦ (↑(f i) : ℝ)) ↔
    (∀ (x : α),
        Summable (α := ℝ) fun (y : β x) ↦
          (fun (i : (x : α) × β x) ↦ (↑(f i) : ℝ)) (Sigma.mk (β := fun (x : α) ↦ β x) x y)) ∧
      Summable (α := ℝ) fun (x : α) ↦
        ∑' (y : β x), (fun (i : (x : α) × β x) ↦ (↑(f i) : ℝ)) (Sigma.mk (β := fun (x : α) ↦ β x) x y)

Tactic:
simpa using mod_cast NNReal.summable_sigma

Premises used: NNReal.summable_sigma
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_3
β : Type u_4
f : β → ℝ
hf : 0 ≤ f
s : α → Set β
hs : ∀ (i : β), ∃! j : α, i ∈ s j
⊢ Summable f ↔
    (∀ (j : α), Summable (α := ℝ) fun (i : (↑(s j) : Type u_4)) ↦ f (↑i : β)) ∧
      Summable (α := ℝ) fun (j : α) ↦ ∑' (i : (↑(s j) : Type u_4)), f (↑i : β)

Tactic:
simpa only [← (Set.sigmaEquiv s hs).summable_iff] using summable_sigma_of_nonneg (fun _ ↦ hf _)

Premises used: summable_sigma_of_nonneg, Equiv.summable_iff, Set.sigmaEquiv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
α : Type u_3
β : Type u_4
f : α × β → ℝ
hf : 0 ≤ f
⊢ Summable f ↔
    (∀ (x : α), Summable (α := ℝ) fun (y : β) ↦ f (x, y)) ∧ Summable (α := ℝ) fun (x : α) ↦ ∑' (y : β), f (x, y)

Tactic:
(Equiv.sigmaEquivProd _ _).summable_iff.symm.trans <| summable_sigma_of_nonneg fun _ ↦ hf _

Premises used: summable_sigma_of_nonneg, Equiv.summable_iff, Iff.trans, DFunLike.coe, Iff.symm, Equiv.sigmaEquivProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
ι : Type u_3
f : ι → ℝ
c : ℝ
hf : 0 ≤ f
h : ∀ (u : Finset ι), ∑ x ∈ u, f x ≤ c
⊢ Summable f

Tactic:
⟨⨆ u : Finset ι, ∑ x ∈ u, f x,
    tendsto_atTop_ciSup (Finset.sum_mono_set_of_nonneg hf) ⟨c, fun _ ⟨u, hu⟩ => hu ▸ h u⟩⟩

Premises used: _private.0.summable_of_sum_le.match_1, iSup, tendsto_atTop_ciSup, Eq.rec, LE.le, Exists.intro, Summable, Finset.sum_mono_set_of_nonneg, Finset.sum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
⊢ Summable f

Tactic:
(summable_iff_not_tendsto_nat_atTop_of_nonneg hf).2 fun H => ?_

Premises used: Iff.mpr, summable_iff_not_tendsto_nat_atTop_of_nonneg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
refine : ∀ (H : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop), False
⊢ Summable f

Tactic:
refine (summable_iff_not_tendsto_nat_atTop_of_nonneg hf).2 fun H => ?_

Premises used: Iff.mpr, summable_iff_not_tendsto_nat_atTop_of_nonneg
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
H : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop
rcases : ∀ (n : ℕ) (hn : c < ∑ i ∈ range n, f i), False
⊢ False

Tactic:
rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩

Premises used: Filter.exists_lt_of_tendsto_atTop, OfNat.ofNat