awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
inst : CommMonoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : Module S E
inst_4 : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL :
  ∀ (x y : E),
    Eq (α := E) ((((L : (a : E) → E →ₗ[S] E) x : E →ₗ[S] E) : (a : E) → E) y : E)
      ((((L : (a : E) → E →ₗ[S] E) y : E →ₗ[S] E) : (a : E) → E) x : E)
x : M
h :
  ∀ (a b : M) (property : (a, b) ∈ mulFiber x),
    Eq (α := E)
      ((((L : (a : E) → E →ₗ[S] E)
                (f
                  (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1))
                          (Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (a, b) property)) :
                      M × M).1) :
              E →ₗ[S] E) :
            (a : E) → E)
          (g
            (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1))
                    (Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (a, b) property)) :
                M × M).2) :
        E)
      ((((L : (a : E) → E →ₗ[S] E)
                (g (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (a, b) property) : M × M).1) :
              E →ₗ[S] E) :
            (a : E) → E)
          (f (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (a, b) property) : M × M).2) :
        E)
⊢ Eq (α := (↑(mulFiber x) : Type u_1) → E)
    (fun (c : (↑(mulFiber x) : Type u_1)) ↦
      (((L : (a : E) → E →ₗ[S] E)
              (f
                (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1)) c) :
                    M × M).1) :
            E →ₗ[S] E) :
          (a : E) → E)
        (g (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1)) c) : M × M).2))
    fun (ab : (↑(mulFiber x) : Type u_1)) ↦
    (((L : (a : E) → E →ₗ[S] E) (g (↑ab : M × M).1) : E →ₗ[S] E) : (a : E) → E) (f (↑ab : M × M).2)

Tactic:
funext ⟨⟨a, b⟩, _⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
inst : CommMonoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : Module S E
inst_4 : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL :
  ∀ (x y : E),
    Eq (α := E) ((((L : (a : E) → E →ₗ[S] E) x : E →ₗ[S] E) : (a : E) → E) y : E)
      ((((L : (a : E) → E →ₗ[S] E) y : E →ₗ[S] E) : (a : E) → E) x : E)
x a b : M
property : (a, b) ∈ mulFiber x
⊢ Eq (α := E)
    ((((L : (a : E) → E →ₗ[S] E)
              (f
                (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1))
                        (Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (a, b) property)) :
                    M × M).1) :
            E →ₗ[S] E) :
          (a : E) → E)
        (g
          (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1))
                  (Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (a, b) property)) :
              M × M).2) :
      E)
    ((((L : (a : E) → E →ₗ[S] E)
              (g (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (a, b) property) : M × M).1) :
            E →ₗ[S] E) :
          (a : E) → E)
        (f (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (a, b) property) : M × M).2) :
      E)

Tactic:
hL (f b) (g a)
-- Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
inst : CommMonoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : Module S E
inst_4 : TopologicalSpace E
L : E →ₗ[S] E →ₗ[S] E
f g : M → E
hL :
  ∀ (x y : E),
    Eq (α := E) ((((L : (a : E) → E →ₗ[S] E) x : E →ₗ[S] E) : (a : E) → E) y : E)
      ((((L : (a : E) → E →ₗ[S] E) y : E →ₗ[S] E) : (a : E) → E) x : E)
x a b : M
property : (a, b) ∈ mulFiber x
⊢ Eq (α := E)
    ((((L : (a : E) → E →ₗ[S] E)
              (f
                (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1))
                        (Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (a, b) property)) :
                    M × M).1) :
            E →ₗ[S] E) :
          (a : E) → E)
        (g
          (↑((mulFiber_swapEquiv x : (a : (↑(mulFiber x) : Type u_1)) → (↑(mulFiber x) : Type u_1))
                  (Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (a, b) property)) :
              M × M).2) :
      E)
    ((((L : (a : E) → E →ₗ[S] E)
              (g (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (a, b) property) : M × M).1) :
            E →ₗ[S] E) :
          (a : E) → E)
        (f (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (a, b) property) : M × M).2) :
      E)

Tactic:
exact hL (f b) (g a)
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
r : ℝ≥0
⊢ HasSum (fun (a : α) ↦ (↑(f a) : ℝ≥0∞)) (↑r : ℝ≥0∞) ↔ HasSum f r

Tactic:
simp only [HasSum, ← coe_finsetSum, tendsto_coe]

Premises used: ENNReal.coe_finsetSum, ENNReal.tendsto_coe, HasSum, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
r : ℝ≥0
f : α → ℝ≥0
h : HasSum f r
⊢ ∑' (a : α), (↑(f a) : ℝ≥0∞) = (↑r : ℝ≥0∞)

Tactic:
(ENNReal.hasSum_coe.2 h).tsum_eq

Premises used: Iff.mpr, HasSum.tsum_eq, ENNReal.hasSum_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0
r : ℝ≥0
hr : HasSum f r
rw : (↑r : ℝ≥0∞) = ∑' (a : α), (↑(f a) : ℝ≥0∞)
rw₁ rw₂ : (↑r : ℝ≥0∞) = (↑r : ℝ≥0∞)
⊢ (↑(tsum f) : ℝ≥0∞) = ∑' (a : α), (↑(f a) : ℝ≥0∞)

Tactic:
rw [hr.tsum_eq, ENNReal.tsum_coe_eq hr]

Premises used: HasSum.tsum_eq, ENNReal.tsum_coe_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
⊢ HasSum f (⨆ (s : Finset α), ∑ a ∈ s, f a)

Tactic:
tendsto_atTop_iSup fun _ _ => Finset.sum_le_sum_of_subset

Premises used: iInf, Finset.sum_le_sum_of_subset, Filter.atTop, tendsto_atTop_iSup, HasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
⊢ Summable f

Tactic:
⟨_, ENNReal.hasSum⟩

Premises used: ENNReal.hasSum, Exists.intro, Summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
⊢ Ne (α := ℝ≥0∞) (∑' (b : β), (↑(f b) : ℝ≥0∞)) ∞ ↔ Summable f

Tactic:
⟨fun h => ?_, fun h => ENNReal.coe_tsum h ▸ ENNReal.coe_ne_top⟩

Premises used: ENNReal.coe_tsum, Eq.rec, Iff.intro, ENNReal.coe_ne_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
refine : ∀ (h : Ne (α := ℝ≥0∞) (∑' (b : β), (↑(f b) : ℝ≥0∞)) ∞), Summable f
⊢ Ne (α := ℝ≥0∞) (∑' (b : β), (↑(f b) : ℝ≥0∞)) ∞ ↔ Summable f

Tactic:
refine ⟨fun h => ?_, fun h => ENNReal.coe_tsum h ▸ ENNReal.coe_ne_top⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
h : Ne (α := ℝ≥0∞) (∑' (b : β), (↑(f b) : ℝ≥0∞)) ∞
⊢ Ne (α := ℝ≥0∞) (∑' (b : β), (↑(f b) : ℝ≥0∞)) ∞

Tactic:
h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
h : Ne (α := ℝ≥0∞) (∑' (b : β), (↑(f b) : ℝ≥0∞)) ∞
lift : ∀ (a : ℝ≥0) (ha : (↑a : ℝ≥0∞) = ∑' (b : β), (↑(f b) : ℝ≥0∞)), Summable f
⊢ Summable f

Tactic:
lift ∑' b, (f b : ℝ≥0∞) to ℝ≥0 using h with a ha
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : (↑a : ℝ≥0∞) = ∑' (b : β), (↑(f b) : ℝ≥0∞)
⊢ Summable f

Tactic:
⟨a, ENNReal.hasSum_coe.1 ?_⟩

Premises used: Exists.intro, Iff.mp, Summable, ENNReal.hasSum_coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : (↑a : ℝ≥0∞) = ∑' (b : β), (↑(f b) : ℝ≥0∞)
refine : HasSum (fun (a : β) ↦ (↑(f a) : ℝ≥0∞)) (↑a : ℝ≥0∞)
⊢ Summable f

Tactic:
refine ⟨a, ENNReal.hasSum_coe.1 ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : (↑a : ℝ≥0∞) = ∑' (b : β), (↑(f b) : ℝ≥0∞)
rw : HasSum (α := ℝ≥0∞) (fun (a : β) ↦ (↑(f a) : ℝ≥0∞)) (∑' (b : β), (↑(f b) : ℝ≥0∞))
⊢ HasSum (fun (a : β) ↦ (↑(f a) : ℝ≥0∞)) (↑a : ℝ≥0∞)

Tactic:
rw [ha]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : (↑a : ℝ≥0∞) = ∑' (b : β), (↑(f b) : ℝ≥0∞)
⊢ HasSum (α := ℝ≥0∞) (fun (a : β) ↦ (↑(f a) : ℝ≥0∞)) (∑' (b : β), (↑(f b) : ℝ≥0∞))

Tactic:
ENNReal.summable.hasSum

Premises used: ENNReal.summable, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : (↑a : ℝ≥0∞) = ∑' (b : β), (↑(f b) : ℝ≥0∞)
⊢ HasSum (α := ℝ≥0∞) (fun (a : β) ↦ (↑(f a) : ℝ≥0∞)) (∑' (b : β), (↑(f b) : ℝ≥0∞))

Tactic:
exact ENNReal.summable.hasSum

Premises used: ENNReal.summable, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑' (a : α), f a) (⨆ (s : Finset α), ∑ a ∈ s, f a)

Tactic:
ENNReal.hasSum.tsum_eq

Premises used: HasSum.tsum_eq, ENNReal.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ (i : ι), t ⊆ s i
rw : Eq (α := ℝ≥0∞) (⨆ (s : Finset α), ∑ a ∈ s, f a) (⨆ (i : ι), ∑ a ∈ s i, f a)
⊢ Eq (α := ℝ≥0∞) (∑' (a : α), f a) (⨆ (i : ι), ∑ a ∈ s i, f a)

Tactic:
rw [ENNReal.tsum_eq_iSup_sum]

Premises used: ENNReal.tsum_eq_iSup_sum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ (i : ι), t ⊆ s i
symm : Eq (α := ℝ≥0∞) (⨆ (i : ι), ∑ a ∈ s i, f a) (⨆ (s : Finset α), ∑ a ∈ s, f a)
⊢ Eq (α := ℝ≥0∞) (⨆ (s : Finset α), ∑ a ∈ s, f a) (⨆ (i : ι), ∑ a ∈ s i, f a)

Tactic:
symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ (i : ι), t ⊆ s i
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ι), (fun (t : Finset α) ↦ (∑ a ∈ t, f a : ℝ≥0∞)) (s i)) (⨆ (s : Finset α), ∑ a ∈ s, f a)

Tactic:
(Finset.sum_mono_set f).iSup_comp_eq hs

Premises used: Finset.sum_mono_set, Monotone.iSup_comp_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ (i : ι), t ⊆ s i
⊢ Eq (α := ℝ≥0∞) (⨆ (i : ι), (fun (t : Finset α) ↦ (∑ a ∈ t, f a : ℝ≥0∞)) (s i)) (⨆ (s : Finset α), ∑ a ∈ s, f a)

Tactic:
exact (Finset.sum_mono_set f).iSup_comp_eq hs

Premises used: Finset.sum_mono_set, Monotone.iSup_comp_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : α → Type u_4
f : (a : α) → β a → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑' (p : (a : α) × β a), f (p.fst (β := fun (a : α) ↦ β a)) (p.snd (β := fun (a : α) ↦ β a)))
    (∑' (a : α) (b : β a), f a b)

Tactic:
ENNReal.summable.tsum_sigma' fun _ => ENNReal.summable

Premises used: ENNReal.summable, Summable.tsum_sigma'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : α → Type u_4
f : (a : α) × β a → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑' (p : (a : α) × β a), f p) (∑' (a : α) (b : β a), f (Sigma.mk (β := fun (a : α) ↦ β a) a b))

Tactic:
ENNReal.summable.tsum_sigma' fun _ => ENNReal.summable

Premises used: ENNReal.summable, Summable.tsum_sigma'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
ι : Type u_4
S : Set ι
f : α → ℝ≥0∞
t : ι → Set α
h : S.PairwiseDisjoint t
⊢ Eq (α := ℝ≥0∞) (∑' (x : (↑(⋃ i ∈ S, t i) : Type u_1)), f (↑x : α))
    (∑' (i : (↑S : Type u_4)) (x : (↑(t (↑i : ι)) : Type u_1)), f (↑x : α))

Tactic:
simp [← ENNReal.tsum_sigma, ← (Set.biUnionEqSigmaOfDisjoint h).tsum_eq]

Premises used: Equiv.tsum_eq, Set.biUnionEqSigmaOfDisjoint, ENNReal.tsum_sigma
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : PairwiseDisjoint univ t
nth_rw :
  Eq (α := ℝ≥0∞) (∑' (x : (↑(⋃ (i : ι), t i) : Type u_1)), f (↑x : α))
    (∑' (x : (↑univ : Type u_4)) (x_1 : (↑(t (↑x : ι)) : Type u_1)), f (↑x_1 : α))
⊢ Eq (α := ℝ≥0∞) (∑' (x : (↑(⋃ (i : ι), t i) : Type u_1)), f (↑x : α))
    (∑' (i : ι) (x : (↑(t i) : Type u_1)), f (↑x : α))

Tactic:
nth_rw 2 [← tsum_univ]

Premises used: tsum_univ
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : PairwiseDisjoint univ t
rw :
  Eq (α := ℝ≥0∞) (∑' (x : (↑(⋃ (i : ι), t i) : Type u_1)), f (↑x : α))
    (∑' (x : (↑(⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Set ι) univ i), t i) : Type u_1)), f (↑x : α))
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (∑' (x : (↑(⋃ (i : ι), t i) : Type u_1)), f (↑x : α))
    (∑' (x : (↑(⋃ (x : ι), t x) : Type u_1)), f (↑x : α))
⊢ Eq (α := ℝ≥0∞) (∑' (x : (↑(⋃ (i : ι), t i) : Type u_1)), f (↑x : α))
    (∑' (x : (↑univ : Type u_4)) (x_1 : (↑(t (↑x : ι)) : Type u_1)), f (↑x_1 : α))

Tactic:
rw [← ENNReal.tsum_biUnion' h, Set.biUnion_univ]

Premises used: Set.biUnion_univ, ENNReal.tsum_biUnion'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : Type u_2
f : α → β → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑' (p : α × β), f p.1 p.2) (∑' (a : α) (b : β), f a b)

Tactic:
ENNReal.summable.tsum_prod' fun _ => ENNReal.summable

Premises used: Summable.tsum_prod', ENNReal.summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : Type u_2
f : α × β → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑' (p : α × β), f p) (∑' (a : α) (b : β), f (a, b))

Tactic:
ENNReal.summable.tsum_prod' fun _ => ENNReal.summable

Premises used: Summable.tsum_prod', ENNReal.summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
β : Type u_2
f : α → β → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑' (a : α) (b : β), f a b) (∑' (b : β) (a : α), f a b)

Tactic:
ENNReal.summable.tsum_comm' (fun _ => ENNReal.summable) fun _ => ENNReal.summable

Premises used: ENNReal.summable, Summable.tsum_comm'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f g : α → ℝ≥0∞
⊢ ∑' (a : α), (f a + g a) = HAdd.hAdd (α := ℝ≥0∞) (∑' (a : α), f a) (∑' (a : α), g a)

Tactic:
ENNReal.summable.tsum_add ENNReal.summable

Premises used: ENNReal.summable, Summable.tsum_add
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
ι : Type u_4
s : Finset ι
f : ι → ℝ≥0∞
rw :
  HAdd.hAdd (α := ℝ≥0∞) (∑' (x : ι), (↑s : Set ι).indicator f x) (∑' (x : ι), (↑s : Set ι)ᶜ.indicator f x) =
    ∑' (i : ι), f i
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ s, f i) (∑' (i : (↑(↑s : Set ι)ᶜ : Type u_4)), f (↑i : ι)) = ∑' (i : ι), f i

Tactic:
rw [tsum_subtype, sum_eq_tsum_indicator]

Premises used: tsum_subtype, sum_eq_tsum_indicator, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
ι : Type u_4
s : Finset ι
f : ι → ℝ≥0∞
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑' (x : ι), (↑s : Set ι).indicator f x) (∑' (x : ι), (↑s : Set ι)ᶜ.indicator f x) =
    ∑' (i : ι), f i

Tactic:
simp [← ENNReal.tsum_add]

Premises used: ENNReal.tsum_add
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f g : α → ℝ≥0∞
h : ∀ (a : α), f a ≤ g a
⊢ LE.le (α := ℝ≥0∞) (∑' (a : α), f a) (∑' (a : α), g a)

Tactic:
ENNReal.summable.tsum_le_tsum h ENNReal.summable

Premises used: ENNReal.summable, Summable.tsum_le_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
s : Finset α
⊢ LE.le (α := ℝ≥0∞) (∑ x ∈ s, f x) (∑' (x : α), f x)

Tactic:
ENNReal.summable.sum_le_tsum s (fun _ _ => zero_le)

Premises used: zero_le, ENNReal.summable, Summable.sum_le_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
h : ∀ b < a, ∃ (I : Finset α), b < ∑ i ∈ I, f i
⊢ a ≤ ∑' (i : α), f i

Tactic:
le_of_forall_lt fun b hb ↦ ?_

Premises used: le_of_forall_lt
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
h : ∀ b < a, ∃ (I : Finset α), b < ∑ i ∈ I, f i
refine : ∀ (b : ℝ≥0∞) (hb : b < a), b < ∑' (i : α), f i
⊢ a ≤ ∑' (i : α), f i

Tactic:
refine le_of_forall_lt fun b hb ↦ ?_

Premises used: le_of_forall_lt
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
h : ∀ b < a, ∃ (I : Finset α), b < ∑ i ∈ I, f i
b : ℝ≥0∞
hb : b < a
obtain : ∀ (I : Finset α) (hI : b < ∑ i ∈ I, f i), b < ∑' (i : α), f i
⊢ b < ∑' (i : α), f i

Tactic:
obtain ⟨I, hI⟩ := h b hb
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
h : ∀ b < a, ∃ (I : Finset α), b < ∑ i ∈ I, f i
b : ℝ≥0∞
hb : b < a
I : Finset α
hI : b < ∑ i ∈ I, f i
⊢ b < ∑' (i : α), f i

Tactic:
lt_of_lt_of_le hI (ENNReal.sum_le_tsum I)

Premises used: ENNReal.sum_le_tsum, lt_of_lt_of_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
h : ∀ b < a, ∃ (I : Finset α), b < ∑ i ∈ I, f i
b : ℝ≥0∞
hb : b < a
I : Finset α
hI : b < ∑ i ∈ I, f i
⊢ b < ∑' (i : α), f i

Tactic:
exact lt_of_lt_of_le hI (ENNReal.sum_le_tsum I)

Premises used: ENNReal.sum_le_tsum, lt_of_lt_of_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
N : ℕ → ℕ
hN : Tendsto N atTop atTop
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), f i) (⨆ (i : ℕ), ∑ a ∈ Finset.range (N i), f a)

Tactic:
ENNReal.tsum_eq_iSup_sum' _ fun t =>
    let ⟨n, hn⟩ := t.exists_nat_subset_range
    let ⟨k, _, hk⟩ := exists_le_of_tendsto_atTop hN 0 n
    ⟨k, Finset.Subset.trans hn (Finset.range_mono hk)⟩

Premises used: Filter.exists_le_of_tendsto_atTop, Finset.Subset.trans, _private.0.ENNReal.tsum_eq_iSup_nat'.match_2, Exists, HasSubset.Subset, ENNReal.tsum_eq_iSup_sum', Finset.range, _private.0.ENNReal.tsum_eq_iSup_nat'.match_1, Exists.intro, Finset.range_mono, OfNat.ofNat, Finset.exists_nat_subset_range
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), f i) (⨆ (i : ℕ), ∑ a ∈ Finset.range i, f a)

Tactic:
ENNReal.tsum_eq_iSup_sum' _ Finset.exists_nat_subset_range

Premises used: ENNReal.tsum_eq_iSup_sum', Finset.exists_nat_subset_range
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), f i) (liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop)

Tactic:
ENNReal.summable.hasSum.tendsto_sum_nat.liminf_eq.symm

Premises used: HasSum.tendsto_sum_nat, ENNReal.summable, Filter.Tendsto.liminf_eq, Summable.hasSum, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
f : ℕ → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑' (i : ℕ), f i) (limsup (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop)

Tactic:
ENNReal.summable.hasSum.tendsto_sum_nat.limsup_eq.symm

Premises used: Filter.Tendsto.limsup_eq, HasSum.tendsto_sum_nat, ENNReal.summable, Summable.hasSum, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
a : α
⊢ f a ≤ ∑' (a : α), f a

Tactic:
ENNReal.summable.le_tsum' a

Premises used: ENNReal.summable, Summable.le_tsum'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
⊢ Eq (α := ℝ≥0∞) (∑' (i : α), f i) 0 ↔ ∀ (i : α), f i = 0

Tactic:
ENNReal.summable.tsum_eq_zero_iff

Premises used: ENNReal.summable, Summable.tsum_eq_zero_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : α → ℝ≥0∞
tsum_ne_top : Ne (α := ℝ≥0∞) (∑' (i : α), a i) ∞
j : α
contrapose! : ∀ (h : ∞ ≤ a j), Eq (α := ℝ≥0∞) (∑' (i : α), a i) ∞
⊢ a j < ∞

Tactic:
contrapose! tsum_ne_top with h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : α → ℝ≥0∞
j : α
h : ∞ ≤ a j
⊢ Eq (α := ℝ≥0∞) (∑' (i : α), a i) ∞

Tactic:
ENNReal.tsum_eq_top_of_eq_top ⟨j, top_unique h⟩

Premises used: ENNReal.tsum_eq_top_of_eq_top, top_unique, Exists.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : α → ℝ≥0∞
j : α
h : ∞ ≤ a j
⊢ Eq (α := ℝ≥0∞) (∑' (i : α), a i) ∞

Tactic:
exact ENNReal.tsum_eq_top_of_eq_top ⟨j, top_unique h⟩

Premises used: ENNReal.tsum_eq_top_of_eq_top, top_unique, Exists.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
inst : Nonempty α
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), ∞) ∞

Tactic:
let ⟨a⟩ := ‹Nonempty α›
  ENNReal.tsum_eq_top_of_eq_top ⟨a, rfl⟩

Premises used: ENNReal.tsum_eq_top_of_eq_top, tsum, Exists.intro, Top.top, _private.0.ENNReal.tsum_top.match_1, Eq, rfl, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
inst : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
apply : Ne (α := ℝ≥0∞) ∞ 0 ∨ c ≠ ∞
⊢ Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c))

Tactic:
apply ENNReal.Tendsto.mul_const tendsto_nat_nhds_top

Premises used: ENNReal.Tendsto.mul_const, ENNReal.tendsto_nat_nhds_top
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
inst : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ Ne (α := ℝ≥0∞) ∞ 0 ∨ c ≠ ∞

Tactic:
simp only [true_or, top_ne_zero, Ne, not_false_iff]

Premises used: true_or, Ne, not_false_iff, ENNReal.top_ne_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
inst : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c))

Tactic:
have A : Tendsto (fun n : ℕ => (n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c)) := by
    apply ENNReal.Tendsto.mul_const tendsto_nat_nhds_top
    simp only [true_or, top_ne_zero, Ne, not_false_iff]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
inst : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c))
n : ℕ
rcases : ∀ (s : Finset α) (hs : #s = n), (↑n : ℝ≥0∞) * c ≤ ∑' (x : α), c
⊢ (↑n : ℝ≥0∞) * c ≤ ∑' (x : α), c

Tactic:
rcases Infinite.exists_subset_card_eq α n with ⟨s, hs⟩

Premises used: Infinite.exists_subset_card_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
inst : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c))
n : ℕ
s : Finset α
hs : #s = n
⊢ (↑n : ℝ≥0∞) * c ≤ ∑' (x : α), c

Tactic:
simpa [hs] using @ENNReal.sum_le_tsum α (fun _ => c) s

Premises used: ENNReal.sum_le_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
inst : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c))
⊢ ∀ (n : ℕ), (↑n : ℝ≥0∞) * c ≤ ∑' (x : α), c

Tactic:
have B : ∀ n : ℕ, (n : ℝ≥0∞) * c ≤ ∑' _ : α, c := fun n => by
    rcases Infinite.exists_subset_card_eq α n with ⟨s, hs⟩
    simpa [hs] using @ENNReal.sum_le_tsum α (fun _ => c) s
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_4
inst : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c))
B : ∀ (n : ℕ), (↑n : ℝ≥0∞) * c ≤ ∑' (x : α), c
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), c) ∞

Tactic:
simpa [hc] using le_of_tendsto' A B

Premises used: le_of_tendsto'
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
f : α → ℝ≥0∞
h : Ne (α := ℝ≥0∞) (∑' (a : α), f a) ∞
a : α
⊢ f a ≠ ∞

Tactic:
fun ha =>
  h <| ENNReal.tsum_eq_top_of_eq_top ⟨a, ha⟩

Premises used: ENNReal.tsum_eq_top_of_eq_top, Exists.intro, Not
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
pos : ∀ (hf : ∀ (i : α), f i = 0), ∑' (i : α), a * f i = a * ∑' (i : α), f i
neg : ∀ (hf : ¬∀ (i : α), f i = 0), ∑' (i : α), a * f i = a * ∑' (i : α), f i
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
by_cases hf : ∀ i, f i = 0
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ∀ (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i

Tactic:
simp [hf]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∀ (i : α), f i = 0
⊢ ¬Eq (α := ℝ≥0∞) (∑' (i : α), f i) 0

Tactic:
rw [← ENNReal.tsum_eq_zero] at hf

Premises used: ENNReal.tsum_eq_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬Eq (α := ℝ≥0∞) (∑' (i : α), f i) 0
simp : Tendsto (fun (s : Finset α) ↦ a * ∑ i ∈ s, f i) atTop (𝓝 (a * ∑' (i : α), f i))
⊢ Tendsto (fun (s : Finset α) ↦ ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' (i : α), f i))

Tactic:
simp only [← Finset.mul_sum]

Premises used: Finset.mul_sum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.ENNReal
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬Eq (α := ℝ≥0∞) (∑' (i : α), f i) 0
⊢ Tendsto (fun (s : Finset α) ↦ a * ∑ i ∈ s, f i) atTop (𝓝 (a * ∑' (i : α), f i))

Tactic:
ENNReal.Tendsto.const_mul ENNReal.summable.hasSum (Or.inl hf)

Premises used: ENNReal.Tendsto.const_mul, ENNReal.summable, Summable.hasSum, Or.inl