awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module S E
inst_5 : Module S F
inst_6 : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (((L : (a : F) → E →ₗ[S] F) y : E →ₗ[S] F) : (a : E) → F) e = y
x : M
⊢ (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) x = f x
have h : ∑' (ab : (↑(mulFiber x) : Type u_1)),
    (((L : (a : F) → E →ₗ[S] F) (f (↑ab : M × M).1) : E →ₗ[S] F) : (a : E) → F)
      (if Membership.mem (γ := Set M) {1} (↑ab : M × M).2 then e else 0) =
  f x
Tactic: simp only [convolution, Set.indicator_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module S E
inst_5 : Module S F
inst_6 : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (((L : (a : F) → E →ₗ[S] F) y : E →ₗ[S] F) : (a : E) → F) e = y
x : M
⊢ ∑' (ab : (↑(mulFiber x) : Type u_1)),
      (((L : (a : F) → E →ₗ[S] F) (f (↑ab : M × M).1) : E →ₗ[S] F) : (a : E) → F)
        (if Membership.mem (γ := Set M) {1} (↑ab : M × M).2 then e else 0) =
    f x
have h : (((L : (a : F) → E →ₗ[S] F) (f (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (x, 1) sorry) : M × M).1) :
        E →ₗ[S] F) :
      (a : E) → F)
    (if
        Membership.mem (γ := Set M) {1}
          (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (x, 1) sorry) : M × M).2 then
      e
    else 0) =
  f x
Tactic: rw [tsum_eq_single (⟨(x, 1), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module S E
inst_5 : Module S F
inst_6 : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (((L : (a : F) → E →ₗ[S] F) y : E →ₗ[S] F) : (a : E) → F) e = y
⊢ (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) = f
have h : ∀ (x : M), (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) x = f x
Tactic: classical
  ext x; simp only [convolution, Set.indicator_apply]
  rw [tsum_eq_single (⟨(x, 1), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]
  simp [hL]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module S E
inst_5 : Module S F
inst_6 : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (((L : (a : F) → E →ₗ[S] F) y : E →ₗ[S] F) : (a : E) → F) e = y
h h₁ : ∀ (x : M), (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) x = f x
⊢ (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) = f
have h₂ : ∀ (x : M),
  ∑' (ab : (↑(mulFiber x) : Type u_1)),
      (((L : (a : F) → E →ₗ[S] F) (f (↑ab : M × M).1) : E →ₗ[S] F) : (a : E) → F)
        (if Membership.mem (γ := Set M) {1} (↑ab : M × M).2 then e else 0) =
    f x
Tactic: classical
  ext x; simp only [convolution, Set.indicator_apply]
  rw [tsum_eq_single (⟨(x, 1), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]
  simp [hL]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module S E
inst_5 : Module S F
inst_6 : TopologicalSpace F
L : F →ₗ[S] E →ₗ[S] F
f : M → F
e : E
hL : ∀ (y : F), (((L : (a : F) → E →ₗ[S] F) y : E →ₗ[S] F) : (a : E) → F) e = y
h h₁ : ∀ (x : M), (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) x = f x
h₂ :
  ∀ (x : M),
    ∑' (ab : (↑(mulFiber x) : Type u_1)),
        (((L : (a : F) → E →ₗ[S] F) (f (↑ab : M × M).1) : E →ₗ[S] F) : (a : E) → F)
          (if Membership.mem (γ := Set M) {1} (↑ab : M × M).2 then e else 0) =
      f x
⊢ (f ⋆[L] Set.indicator {1} fun (x : M) ↦ e) = f
have h₃ : ∀ (x : M),
  (((L : (a : F) → E →ₗ[S] F) (f (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (x, 1) sorry) : M × M).1) :
          E →ₗ[S] F) :
        (a : E) → F)
      (if
          Membership.mem (γ := Set M) {1}
            (↑(Subtype.mk (p := fun (x_1 : M × M) ↦ x_1 ∈ mulFiber x) (x, 1) sorry) : M × M).2 then
        e
      else 0) =
    f x
Tactic: classical
  ext x; simp only [convolution, Set.indicator_apply]
  rw [tsum_eq_single (⟨(x, 1), by grind⟩ : mulFiber x) (by grind [LinearMap.zero_apply])]
  simp [hL]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid E'
inst_4 : AddCommMonoid F
inst_5 : Module S E
inst_6 : Module S E'
inst_7 : Module S F
inst_8 : TopologicalSpace F
inst_9 : T2Space F
inst_10 : ContinuousAdd F
f : M → E
g g' : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f g'
⊢ f ⋆[L] (g + g') = f ⋆[L] g + f ⋆[L] g'
have h : ∀ (x : M), (f ⋆[L] (g + g')) x = (f ⋆[L] g + f ⋆[L] g') x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
Goal:
M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst : Monoid M
inst_1 : CommSemiring S
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid E'
inst_4 : AddCommMonoid F
inst_5 : Module S E
inst_6 : Module S E'
inst_7 : Module S F
inst_8 : TopologicalSpace F
inst_9 : T2Space F
inst_10 : ContinuousAdd F
f f' : M → E
g : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f' g
⊢ (f + f') ⋆[L] g = f ⋆[L] g + f' ⋆[L] g
have h : ∀ (x : M), ((f + f') ⋆[L] g) x = (f ⋆[L] g + f' ⋆[L] g) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
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)
⊢ Eq (α := M → E)
    (fun (x : M) ↦
      ∑' (ab : (↑(mulFiber x) : Type u_1)),
        (((L : (a : E) → E →ₗ[S] E) (f (↑ab : M × M).1) : E →ₗ[S] E) : (a : E) → E) (g (↑ab : M × M).2))
    fun (x : M) ↦
    ∑' (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)
have h : ∀ (x : M),
  Eq.{u_3 + 1} (α := E)
    (∑' (ab : (↑(mulFiber x) : Type u_1)),
      (((L : (a : E) → E →ₗ[S] E) (f (↑ab : M × M).1) : E →ₗ[S] E) : (a : E) → E) (g (↑ab : M × M).2))
    (∑' (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: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
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
⊢ Eq.{u_3 + 1} (α := E)
    (∑' (ab : (↑(mulFiber x) : Type u_1)),
      (((L : (a : E) → E →ₗ[S] E) (f (↑ab : M × M).1) : E →ₗ[S] E) : (a : E) → E) (g (↑ab : M × M).2))
    (∑' (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))
have h : Eq.{u_3 + 1} (α := E)
  (∑' (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))
  (∑' (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: rw [← (mulFiber_swapEquiv x).tsum_eq]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
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
⊢ Eq.{u_3 + 1} (α := E)
    (∑' (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))
    (∑' (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))
have h : 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: congr 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution (goal)
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
⊢ 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)
have 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)
Tactic: funext ⟨⟨a, b⟩, _⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
r : ℝ≥0
hr : HasSum f r
⊢ (↑(tsum f) : ℝ≥0∞) = ∑' (a : α), (↑(f a) : ℝ≥0∞)
have rw : (↑r : ℝ≥0∞) = ∑' (a : α), (↑(f a) : ℝ≥0∞)
Tactic: rw [hr.tsum_eq, ENNReal.tsum_coe_eq hr]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0
r : ℝ≥0
hr : HasSum f r
rw : (↑r : ℝ≥0∞) = ∑' (a : α), (↑(f a) : ℝ≥0∞)
⊢ (↑(tsum f) : ℝ≥0∞) = ∑' (a : α), (↑(f a) : ℝ≥0∞)
have rw₁ : (↑r : ℝ≥0∞) = (↑r : ℝ≥0∞)
Tactic: rw [hr.tsum_eq, ENNReal.tsum_coe_eq hr]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
β : Type u_2
f : β → ℝ≥0
⊢ Ne (α := ℝ≥0∞) (∑' (b : β), (↑(f b) : ℝ≥0∞)) ∞ ↔ Summable f
have refine : ∀ (h : Ne (α := ℝ≥0∞) (∑' (b : β), (↑(f b) : ℝ≥0∞)) ∞), Summable f
Tactic: refine ⟨fun h => ?_, fun h => ENNReal.coe_tsum h ▸ ENNReal.coe_ne_top⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
β : Type u_2
f : β → ℝ≥0
h : Ne (α := ℝ≥0∞) (∑' (b : β), (↑(f b) : ℝ≥0∞)) ∞
⊢ Summable f
have lift : ∀ (a : ℝ≥0) (ha : (↑a : ℝ≥0∞) = ∑' (b : β), (↑(f b) : ℝ≥0∞)), Summable f
Tactic: lift ∑' b, (f b : ℝ≥0∞) to ℝ≥0 using h with a ha
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : (↑a : ℝ≥0∞) = ∑' (b : β), (↑(f b) : ℝ≥0∞)
⊢ Summable f
have refine : HasSum (fun (a : β) ↦ (↑(f a) : ℝ≥0∞)) (↑a : ℝ≥0∞)
Tactic: refine ⟨a, ENNReal.hasSum_coe.1 ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
β : Type u_2
f : β → ℝ≥0
a : ℝ≥0
ha : (↑a : ℝ≥0∞) = ∑' (b : β), (↑(f b) : ℝ≥0∞)
⊢ HasSum (fun (a : β) ↦ (↑(f a) : ℝ≥0∞)) (↑a : ℝ≥0∞)
have rw : HasSum (α := ℝ≥0∞) (fun (a : β) ↦ (↑(f a) : ℝ≥0∞)) (∑' (b : β), (↑(f b) : ℝ≥0∞))
Tactic: rw [ha]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ (i : ι), t ⊆ s i
⊢ Eq (α := ℝ≥0∞) (∑' (a : α), f a) (⨆ (i : ι), ∑ a ∈ s i, f a)
have rw : Eq (α := ℝ≥0∞) (⨆ (s : Finset α), ∑ a ∈ s, f a) (⨆ (i : ι), ∑ a ∈ s i, f a)
Tactic: rw [ENNReal.tsum_eq_iSup_sum]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
f : α → ℝ≥0∞
ι : Type u_4
s : ι → Finset α
hs : ∀ (t : Finset α), ∃ (i : ι), t ⊆ s i
⊢ Eq (α := ℝ≥0∞) (⨆ (s : Finset α), ∑ a ∈ s, f a) (⨆ (i : ι), ∑ a ∈ s i, f a)
have symm : Eq (α := ℝ≥0∞) (⨆ (i : ι), ∑ a ∈ s i, f a) (⨆ (s : Finset α), ∑ a ∈ s, f a)
Tactic: symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : PairwiseDisjoint univ t
⊢ Eq (α := ℝ≥0∞) (∑' (x : (↑(⋃ (i : ι), t i) : Type u_1)), f (↑x : α))
    (∑' (i : ι) (x : (↑(t i) : Type u_1)), f (↑x : α))
have 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 : α))
Tactic: nth_rw 2 [← tsum_univ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
ι : Type u_4
f : α → ℝ≥0∞
t : ι → Set α
h : PairwiseDisjoint univ t
⊢ 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 : α))
have 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 : α))
Tactic: rw [← ENNReal.tsum_biUnion' h, Set.biUnion_univ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
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 : α))
⊢ 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 : α))
have rw₁ : Eq (α := ℝ≥0∞) (∑' (x : (↑(⋃ (i : ι), t i) : Type u_1)), f (↑x : α))
  (∑' (x : (↑(⋃ (x : ι), t x) : Type u_1)), f (↑x : α))
Tactic: rw [← ENNReal.tsum_biUnion' h, Set.biUnion_univ]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
ι : Type u_4
s : Finset ι
f : ι → ℝ≥0∞
⊢ HAdd.hAdd (α := ℝ≥0∞) (∑ i ∈ s, f i) (∑' (i : (↑(↑s : Set ι)ᶜ : Type u_4)), f (↑i : ι)) = ∑' (i : ι), f i
have rw : HAdd.hAdd (α := ℝ≥0∞) (∑' (x : ι), (↑s : Set ι).indicator f x) (∑' (x : ι), (↑s : Set ι)ᶜ.indicator f x) =
  ∑' (i : ι), f i
Tactic: rw [tsum_subtype, sum_eq_tsum_indicator]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
h : ∀ b < a, ∃ (I : Finset α), b < ∑ i ∈ I, f i
⊢ a ≤ ∑' (i : α), f i
have refine : ∀ (b : ℝ≥0∞) (hb : b < a), b < ∑' (i : α), f i
Tactic: refine le_of_forall_lt fun b hb ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
h : ∀ b < a, ∃ (I : Finset α), b < ∑ i ∈ I, f i
b : ℝ≥0∞
hb : b < a
⊢ b < ∑' (i : α), f i
have obtain : ∀ (I : Finset α) (hI : b < ∑ i ∈ I, f i), b < ∑' (i : α), f i
Tactic: obtain ⟨I, hI⟩ := h b hb
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
a : α → ℝ≥0∞
tsum_ne_top : Ne (α := ℝ≥0∞) (∑' (i : α), a i) ∞
j : α
⊢ a j < ∞
have contrapose! : ∀ (h : ∞ ≤ a j), Eq (α := ℝ≥0∞) (∑' (i : α), a i) ∞
Tactic: contrapose! tsum_ne_top with h
Cleared hypotheses: tsum_ne_top
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_4
inst : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c))
have apply : Ne (α := ℝ≥0∞) ∞ 0 ∨ c ≠ ∞
Tactic: apply ENNReal.Tendsto.mul_const tendsto_nat_nhds_top
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_4
inst : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), c) ∞
have A : 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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
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
have rcases : ∀ (s : Finset α) (hs : #s = n), (↑n : ℝ≥0∞) * c ≤ ∑' (x : α), c
Tactic: rcases Infinite.exists_subset_card_eq α n with ⟨s, hs⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_4
inst : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c))
⊢ Eq (α := ℝ≥0∞) (∑' (x : α), c) ∞
have B : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i
have pos : ∀ (hf : ∀ (i : α), f i = 0), ∑' (i : α), a * f i = a * ∑' (i : α), f i
Tactic: by_cases hf : ∀ i, f i = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
pos : ∀ (hf : ∀ (i : α), f i = 0), ∑' (i : α), a * f i = a * ∑' (i : α), f i
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i
have neg : ∀ (hf : ¬∀ (i : α), f i = 0), ∑' (i : α), a * f i = a * ∑' (i : α), f i
Tactic: by_cases hf : ∀ i, f i = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬∀ (i : α), f i = 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i
have hf₁ : ¬Eq (α := ℝ≥0∞) (∑' (i : α), f i) 0
Tactic: rw [← ENNReal.tsum_eq_zero] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬Eq (α := ℝ≥0∞) (∑' (i : α), f i) 0
⊢ Tendsto (fun (s : Finset α) ↦ ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' (i : α), f i))
have simp : Tendsto (fun (s : Finset α) ↦ a * ∑ i ∈ s, f i) atTop (𝓝 (a * ∑' (i : α), f i))
Tactic: simp only [← Finset.mul_sum]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_1
a : ℝ≥0∞
f : α → ℝ≥0∞
hf : ¬Eq (α := ℝ≥0∞) (∑' (i : α), f i) 0
⊢ ∑' (i : α), a * f i = a * ∑' (i : α), f i
have this : Tendsto (fun (s : Finset α) ↦ ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' (i : α), f i))
Tactic: have : Tendsto (fun s : Finset α => ∑ j ∈ s, a * f j) atTop (𝓝 (a * ∑' i, f i)) := by
      simp only [← Finset.mul_sum]
      exact ENNReal.Tendsto.const_mul ENNReal.summable.hasSum (Or.inl hf)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
⊢ HasSum f r ↔ Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
have refine : ∀ (h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)), HasSum f r
Tactic: refine ⟨HasSum.tendsto_sum_nat, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
⊢ HasSum f r
have rw : HasSum f (∑' (i : ℕ), f i)
Tactic: rw [← iSup_eq_of_tendsto _ h, ← ENNReal.tsum_eq_iSup_nat]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0∞
r : ℝ≥0∞
h : Tendsto (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
rw : HasSum f (∑' (i : ℕ), f i)
⊢ HasSum f r
have rw₁ : Monotone (β := ℝ≥0∞) fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i
Tactic: rw [← iSup_eq_of_tendsto _ h, ← ENNReal.tsum_eq_iSup_nat]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0∞
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
have rw : HasSum f (∑' (n : ℕ), f n)
Tactic: rw [← hasSum_iff_tendsto_nat]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_4
f : α → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
⊢ Tendsto f cofinite (𝓝 0)
have f_ne_top : ∀ (n : α), f n ≠ ∞
Tactic: have f_ne_top : ∀ n, f n ≠ ∞ := ENNReal.ne_top_of_tsum_ne_top hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (hypothesis)
Goal:
α : Type u_4
f : α → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
f_ne_top : ∀ (n : α), f n ≠ ∞
⊢ Tendsto f cofinite (𝓝 0)
have h_f_coe : f = fun (n : α) ↦ (↑(f n).toNNReal : ℝ≥0∞)
Tactic: have h_f_coe : f = fun n => ((f n).toNNReal : ENNReal) :=
    funext fun n => (coe_toNNReal (f_ne_top n)).symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_4
f : α → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
f_ne_top : ∀ (n : α), f n ≠ ∞
h_f_coe : f = fun (n : α) ↦ (↑(f n).toNNReal : ℝ≥0∞)
⊢ Tendsto f cofinite (𝓝 0)
have rw : Tendsto (β := ℝ≥0) (fun (n : α) ↦ (f n).toNNReal) cofinite (𝓝 0)
Tactic: rw [h_f_coe, ← @coe_zero, tendsto_coe]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
f : ℕ → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : ℕ), f x) ∞
⊢ Tendsto f atTop (𝓝 0)
have rw : Tendsto f cofinite (𝓝 0)
Tactic: rw [← Nat.cofinite_eq_atTop]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.ENNReal (goal)
Goal:
α : Type u_4
f : α → ℝ≥0∞
hf : Ne (α := ℝ≥0∞) (∑' (x : α), f x) ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (s : Finset α) ↦ ∑' (b : { x : α // x ∉ s }), f (↑b : α)) atTop (𝓝 0)
have lift : ∀ (f : (i : α) → ℝ≥0) (hf : Ne (α := ℝ≥0∞) (∑' (x : α), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) x) ∞),
  Tendsto (β := ℝ≥0∞) (fun (s : Finset α) ↦ ∑' (b : { x : α // x ∉ s }), (fun (i : α) ↦ (↑(f i) : ℝ≥0∞)) (↑b : α)) atTop
    (𝓝 0)
Tactic: lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hf
Cleared hypotheses: f, hf