awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
n : ℕ
hn : c < ∑ i ∈ range n, f i
⊢ False

Tactic:
lt_irrefl _ (hn.trans_le (h n))

Premises used: lt_irrefl, LT.lt.trans_le
-- 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
n : ℕ
hn : c < ∑ i ∈ range n, f i
⊢ False

Tactic:
exact lt_irrefl _ (hn.trans_le (h n))

Premises used: lt_irrefl, LT.lt.trans_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
ι : Type u_3
f : ι → ℝ
c : ℝ
hf : 0 ≤ f
h : ∀ (u : Finset ι), ∑ x ∈ u, f x ≤ c
⊢ ∑' (x : ι), f x ≤ c

Tactic:
(summable_of_sum_le hf h).tsum_le_of_sum_le h

Premises used: Summable.tsum_le_of_sum_le, summable_of_sum_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
⊢ ∑' (n : ℕ), f n ≤ c

Tactic:
(summable_of_sum_range_le hf h).tsum_le_of_sum_range_le h

Premises used: Summable.tsum_le_of_sum_range_le, summable_of_sum_range_le
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Real
Goal:
i : ℕ
f g : ℕ → ℝ
h0 : ∀ (b : ℕ), 0 ≤ f b
h : ∀ (b : ℕ), f b ≤ g b
hi : f i < g i
hg : Summable g
⊢ LT.lt (α := ℝ) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n)

Tactic:
Summable.tsum_lt_tsum h hi (.of_nonneg_of_le h0 h hg) hg

Premises used: Summable.of_nonneg_of_le, Summable.tsum_lt_tsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : HasSum f a₁ L
⊢ HasSum (fun (i : ι) ↦ a₂ * f i) (a₂ * a₁) L

Tactic:
simpa only using h.map (AddMonoidHom.mulLeft a₂) (continuous_const.mul continuous_id)

Premises used: HasSum.map, continuous_const, Continuous.mul, continuous_id, AddMonoidHom.mulLeft
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
hf : HasSum f a₁ L
⊢ HasSum (fun (i : ι) ↦ f i * a₂) (a₁ * a₂) L

Tactic:
simpa only using hf.map (AddMonoidHom.mulRight a₂) (continuous_id.mul continuous_const)

Premises used: HasSum.map, continuous_const, Continuous.mul, AddMonoidHom.mulRight, continuous_id
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
hf : Summable f L
⊢ Summable.{u_3, u_1} (α := α) (fun (i : ι) ↦ a * f i) L

Tactic:
(hf.hasSum.mul_left _).summable

Premises used: HasSum.mul_left, HasSum.summable, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
hf : Summable f L
⊢ Summable.{u_3, u_1} (α := α) (fun (i : ι) ↦ f i * a) L

Tactic:
(hf.hasSum.mul_right _).summable

Premises used: HasSum.summable, Summable.hasSum, HasSum.mul_right
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
inst_3 : T2Space α
inst_4 : L.NeBot
a : α
hf : Summable f L
⊢ ∑'[L] (i : ι), a * f i = a * ∑'[L] (i : ι), f i

Tactic:
(hf.hasSum.mul_left _).tsum_eq

Premises used: HasSum.mul_left, HasSum.tsum_eq, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
inst_3 : T2Space α
inst_4 : L.NeBot
a : α
hf : Summable f L
⊢ ∑'[L] (i : ι), f i * a = (∑'[L] (i : ι), f i) * a

Tactic:
(hf.hasSum.mul_right _).tsum_eq

Premises used: HasSum.tsum_eq, Summable.hasSum, HasSum.mul_right
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
inst_3 : T2Space α
inst_4 : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
pos : ∀ (hf : Summable f L), SemiconjBy (∑'[L] (i : ι), f i) a b
neg : ∀ (hf : ¬Summable f L), SemiconjBy (∑'[L] (i : ι), f i) a b
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b

Tactic:
by_cases hf : Summable f L

Premises used: Summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
inst_3 : T2Space α
inst_4 : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
hf : Summable f L
pos : (∑'[L] (i : ι), f i) * a = b * ∑'[L] (i : ι), f i
pos₁ : ∑'[L] (i : ι), f i * a = b * ∑'[L] (i : ι), f i
pos₂ : Eq.{u_3 + 1} (α := α) (∑'[L] (i : ι), f i * a) (∑'[L] (i : ι), b * f i)
pos₃ pos₄ : Eq.{u_3 + 1} (α := α) (∑'[L] (b_1 : ι), b * f b_1) (∑'[L] (i : ι), b * f i)
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b

Tactic:
rw [SemiconjBy, ← hf.tsum_mul_right a, ← hf.tsum_mul_left b, tsum_congr h]

Premises used: tsum_congr, SemiconjBy, Summable.tsum_mul_left, Summable.tsum_mul_right
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
inst_3 : T2Space α
inst_4 : L.NeBot
a b : α
h : ∀ (i : ι), SemiconjBy (f i) a b
hf : ¬Summable f L
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b

Tactic:
simp [tsum_eq_zero_of_not_summable hf]

Premises used: tsum_eq_zero_of_not_summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
inst_3 : T2Space α
inst_4 : L.NeBot
f g : ι → α
a : α
hf : Summable f L
hg : Summable g L
h : ∀ (i : ι), SemiconjBy a (f i) (g i)
rw : Eq.{u_3 + 1} (α := α) (∑'[L] (i : ι), a * f i) (∑'[L] (i : ι), g i * a)
⊢ SemiconjBy a (∑'[L] (i : ι), f i) (∑'[L] (i : ι), g i)

Tactic:
rw [SemiconjBy, ← hf.tsum_mul_left a, ← hg.tsum_mul_right a]

Premises used: SemiconjBy, Summable.tsum_mul_left, Summable.tsum_mul_right
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
inst_3 : T2Space α
inst_4 : L.NeBot
f g : ι → α
a : α
hf : Summable f L
hg : Summable g L
h : ∀ (i : ι), SemiconjBy a (f i) (g i)
⊢ Eq.{u_3 + 1} (α := α) (∑'[L] (i : ι), a * f i) (∑'[L] (i : ι), g i * a)

Tactic:
tsum_congr h

Premises used: tsum_congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
inst_3 : T2Space α
inst_4 : L.NeBot
f g : ι → α
a : α
hf : Summable f L
hg : Summable g L
h : ∀ (i : ι), SemiconjBy a (f i) (g i)
⊢ Eq.{u_3 + 1} (α := α) (∑'[L] (i : ι), a * f i) (∑'[L] (i : ι), g i * a)

Tactic:
exact tsum_congr h

Premises used: tsum_congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
inst_3 : T2Space α
inst_4 : L.NeBot
a : α
h : ∀ (i : ι), Commute (f i) a
⊢ Commute (∑'[L] (i : ι), f i) a

Tactic:
SemiconjBy.tsum_left h

Premises used: Commute, SemiconjBy.tsum_left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : NonUnitalNonAssocSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
inst_3 : T2Space α
inst_4 : L.NeBot
a : α
h : ∀ (i : ι), Commute a (f i)
⊢ Commute a (∑'[L] (i : ι), f i)

Tactic:
(Commute.tsum_left _ fun i ↦ (h i).symm).symm

Premises used: Commute.symm, Commute.tsum_left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
h : HasSum f a L
b : α
⊢ HasSum (fun (i : ι) ↦ f i / b) (a / b) L

Tactic:
simp only [div_eq_mul_inv, h.mul_right b⁻¹]

Premises used: div_eq_mul_inv, Inv.inv, HasSum.mul_right
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
h : Summable f L
b : α
⊢ Summable.{u_3, u_1} (α := α) (fun (i : ι) ↦ f i / b) L

Tactic:
(h.hasSum.div_const _).summable

Premises used: HasSum.div_const, HasSum.summable, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : a₂ ≠ 0
H : HasSum (fun (i : ι) ↦ a₂ * f i) (a₂ * a₁) L
⊢ HasSum f a₁ L

Tactic:
simpa only [inv_mul_cancel_left₀ h] using H.mul_left a₂⁻¹

Premises used: inv_mul_cancel_left₀, HasSum.mul_left, Inv.inv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : a₂ ≠ 0
H : HasSum (fun (i : ι) ↦ f i * a₂) (a₁ * a₂) L
⊢ HasSum f a₁ L

Tactic:
simpa only [mul_inv_cancel_right₀ h] using H.mul_right a₂⁻¹

Premises used: mul_inv_cancel_right₀, Inv.inv, HasSum.mul_right
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : a₂ ≠ 0
⊢ HasSum (fun (i : ι) ↦ f i / a₂) (a₁ / a₂) L ↔ HasSum f a₁ L

Tactic:
simpa only [div_eq_mul_inv] using hasSum_mul_right_iff (inv_ne_zero h)

Premises used: div_eq_mul_inv, hasSum_mul_right_iff, inv_ne_zero
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
h : a ≠ 0
H : Summable.{u_3, u_1} (α := α) (fun (i : ι) ↦ a * f i) L
⊢ Summable f L

Tactic:
simpa only [inv_mul_cancel_left₀ h] using H.mul_left a⁻¹

Premises used: inv_mul_cancel_left₀, Summable.mul_left, Inv.inv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
h : a ≠ 0
H : Summable.{u_3, u_1} (α := α) (fun (i : ι) ↦ f i * a) L
⊢ Summable f L

Tactic:
simpa only [mul_inv_cancel_right₀ h] using H.mul_right a⁻¹

Premises used: Summable.mul_right, mul_inv_cancel_right₀, Inv.inv
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
h : a ≠ 0
⊢ Summable.{u_3, u_1} (α := α) (fun (i : ι) ↦ f i / a) L ↔ Summable f L

Tactic:
simpa only [div_eq_mul_inv] using summable_mul_right_iff (inv_ne_zero h)

Premises used: div_eq_mul_inv, inv_ne_zero, summable_mul_right_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
inst_3 : T2Space α
pos : ∀ (ha : a = 0), ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x
neg : ∀ (ha : ¬a = 0), ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x
⊢ ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
inst_3 : T2Space α
ha : a = 0
⊢ ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x

Tactic:
simp [ha]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
inst_3 : T2Space α
ha : ¬a = 0
⊢ ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x

Tactic:
((Homeomorph.mulLeft₀ a ha).isClosedEmbedding.map_tsum f
      (g := AddMonoidHom.mulLeft a)).symm

Premises used: Homeomorph.mulLeft₀, Topology.IsClosedEmbedding.map_tsum, Homeomorph.isClosedEmbedding, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
inst_3 : T2Space α
ha : ¬a = 0
⊢ ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x

Tactic:
exact ((Homeomorph.mulLeft₀ a ha).isClosedEmbedding.map_tsum f
      (g := AddMonoidHom.mulLeft a)).symm

Premises used: Homeomorph.mulLeft₀, Topology.IsClosedEmbedding.map_tsum, Homeomorph.isClosedEmbedding, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
inst_3 : T2Space α
pos : ∀ (ha : a = 0), ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a
neg : ∀ (ha : ¬a = 0), ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a
⊢ ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a

Tactic:
by_cases ha : a = 0
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
inst_3 : T2Space α
ha : a = 0
⊢ ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a

Tactic:
simp [ha]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
inst_3 : T2Space α
ha : ¬a = 0
⊢ ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a

Tactic:
((Homeomorph.mulRight₀ a ha).isClosedEmbedding.map_tsum f
      (g := AddMonoidHom.mulRight a)).symm

Premises used: Homeomorph.mulRight₀, Topology.IsClosedEmbedding.map_tsum, Homeomorph.isClosedEmbedding, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
inst_3 : T2Space α
ha : ¬a = 0
⊢ ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a

Tactic:
exact ((Homeomorph.mulRight₀ a ha).isClosedEmbedding.map_tsum f
      (g := AddMonoidHom.mulRight a)).symm

Premises used: Homeomorph.mulRight₀, Topology.IsClosedEmbedding.map_tsum, Homeomorph.isClosedEmbedding, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
inst_3 : T2Space α
⊢ ∑'[L] (x : ι), f x / a = (∑'[L] (x : ι), f x) / a

Tactic:
simpa only [div_eq_mul_inv] using tsum_mul_right

Premises used: div_eq_mul_inv, tsum_mul_right
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
h : HasSum (fun (x : ι) ↦ 1 / f x) a L
b : α
⊢ HasSum (fun (i : ι) ↦ b * (1 / f i)) (b * a) L

Tactic:
have := h.mul_left b
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
h : HasSum (fun (x : ι) ↦ 1 / f x) a L
b : α
this : HasSum (fun (i : ι) ↦ b * (1 / f i)) (b * a) L
⊢ HasSum (fun (i : ι) ↦ b / f i) (b * a) L

Tactic:
simpa only [div_eq_mul_inv, one_mul] using this

Premises used: div_eq_mul_inv, one_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
h : Summable.{u_3, u_1} (α := α) (fun (x : ι) ↦ 1 / f x) L
b : α
⊢ Summable.{u_3, u_1} (α := α) (fun (i : ι) ↦ b / f i) L

Tactic:
(h.hasSum.const_div b).summable

Premises used: HasSum.summable, Summable.hasSum, HasSum.const_div
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a₁ a₂ : α
h : a₂ ≠ 0
⊢ HasSum (fun (i : ι) ↦ a₂ / f i) (a₂ * a₁) L ↔ HasSum (1 / f) a₁ L

Tactic:
simpa only [div_eq_mul_inv, one_mul] using hasSum_mul_left_iff h

Premises used: hasSum_mul_left_iff, div_eq_mul_inv, one_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
h : a ≠ 0
⊢ Summable.{u_3, u_1} (α := α) (fun (i : ι) ↦ a / f i) L ↔ Summable (1 / f) L

Tactic:
simpa only [div_eq_mul_inv, one_mul] using summable_mul_left_iff h

Premises used: div_eq_mul_inv, summable_mul_left_iff, one_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : T3Space α
inst_2 : NonUnitalNonAssocSemiring α
inst_3 : IsTopologicalSemiring α
f : ι → α
g : κ → α
s t u : α
hf : HasSum f s
hg : HasSum g t
hfg : HasSum (fun (x : ι × κ) ↦ f x.1 * g x.2) u
⊢ s * t = u

Tactic:
have key₁ : HasSum (fun i ↦ f i * t) (s * t) := hf.mul_right t
  have this : ∀ i : ι, HasSum (fun c : κ ↦ f i * g c) (f i * t) := fun i ↦ hg.mul_left (f i)
  have key₂ : HasSum (fun i ↦ f i * t) u := HasSum.prod_fiberwise hfg this
  key₁.unique key₂

Premises used: HasSum.mul_left, HasSum.prod_fiberwise, HasSum.unique, HasSum.mul_right
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : T3Space α
inst_2 : NonUnitalNonAssocSemiring α
inst_3 : IsTopologicalSemiring α
f : ι → α
g : κ → α
s t : α
hf : HasSum f s
hg : HasSum g t
hfg : Summable (α := α) fun (x : ι × κ) ↦ f x.1 * g x.2
⊢ HasSum (fun (x : ι × κ) ↦ f x.1 * g x.2) (s * t)

Tactic:
let ⟨_u, hu⟩ := hfg
  (hf.mul_eq hg hu).symm ▸ hu

Premises used: HMul.hMul, Eq.rec, _private.0.HasSum.mul.match_1, Prod.fst, HasSum.mul_eq, HasSum, Prod, Eq.symm, Prod.snd, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst : TopologicalSpace α
inst_1 : T3Space α
inst_2 : NonUnitalNonAssocSemiring α
inst_3 : IsTopologicalSemiring α
f : ι → α
g : κ → α
hf : Summable f
hg : Summable g
hfg : Summable (α := α) fun (x : ι × κ) ↦ f x.1 * g x.2
⊢ HMul.hMul (α := α) (∑' (x : ι), f x) (∑' (y : κ), g y) = ∑' (z : ι × κ), f z.1 * g z.2

Tactic:
hf.hasSum.mul_eq hg.hasSum hfg.hasSum

Premises used: HasSum.mul_eq, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
α : Type u_3
A : Type u_4
inst : AddCommMonoid A
inst_1 : HasAntidiagonal A
inst_2 : TopologicalSpace α
inst_3 : NonUnitalNonAssocSemiring α
f g : A → α
⊢ (Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2) ↔
    Summable.{u_3, u_4} (α := α) fun (x : (n : A) × ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n)) ↦
      f (↑(x.snd (β := fun (n : A) ↦ ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n))) : A × A).1 *
        g (↑(x.snd (β := fun (n : A) ↦ ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n))) : A × A).2

Tactic:
Finset.sigmaAntidiagonalEquivProd.summable_iff.symm

Premises used: Finset.sigmaAntidiagonalEquivProd, Equiv.summable_iff, Iff.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
α : Type u_3
A : Type u_4
inst : AddCommMonoid A
inst_1 : HasAntidiagonal A
inst_2 : TopologicalSpace α
inst_3 : NonUnitalNonAssocSemiring α
f g : A → α
inst_4 : T3Space α
inst_5 : IsTopologicalSemiring α
h : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2
⊢ Summable.{u_3, u_4} (α := α) fun (x : (n : A) × ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n)) ↦
    f (↑(x.snd (β := fun (n : A) ↦ ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n))) : A × A).1 *
      g (↑(x.snd (β := fun (n : A) ↦ ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n))) : A × A).2

Tactic:
rw [summable_mul_prod_iff_summable_mul_sigma_antidiagonal] at h

Premises used: summable_mul_prod_iff_summable_mul_sigma_antidiagonal
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
α : Type u_3
A : Type u_4
inst : AddCommMonoid A
inst_1 : HasAntidiagonal A
inst_2 : TopologicalSpace α
inst_3 : NonUnitalNonAssocSemiring α
f g : A → α
inst_4 : T3Space α
inst_5 : IsTopologicalSemiring α
h :
  Summable.{u_3, u_4} (α := α) fun (x : (n : A) × ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n)) ↦
    f (↑(x.snd (β := fun (n : A) ↦ ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n))) : A × A).1 *
      g (↑(x.snd (β := fun (n : A) ↦ ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n))) : A × A).2
f₁ : fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
L : SummationFilter.unconditional A
| Summable.{u_3, u_4} (α := α) fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2

Tactic:
congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
α : Type u_3
A : Type u_4
inst : AddCommMonoid A
inst_1 : HasAntidiagonal A
inst_2 : TopologicalSpace α
inst_3 : NonUnitalNonAssocSemiring α
f g : A → α
inst_4 : T3Space α
inst_5 : IsTopologicalSemiring α
h :
  Summable.{u_3, u_4} (α := α) fun (x : (n : A) × ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n)) ↦
    f (↑(x.snd (β := fun (n : A) ↦ ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n))) : A × A).1 *
      g (↑(x.snd (β := fun (n : A) ↦ ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n))) : A × A).2
f₁ : ∀ (x : A), ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ x, f kl.1 * g kl.2
| fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
α : Type u_3
A : Type u_4
inst : AddCommMonoid A
inst_1 : HasAntidiagonal A
inst_2 : TopologicalSpace α
inst_3 : NonUnitalNonAssocSemiring α
f g : A → α
inst_4 : T3Space α
inst_5 : IsTopologicalSemiring α
h :
  Summable.{u_3, u_4} (α := α) fun (x : (n : A) × ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n)) ↦
    f (↑(x.snd (β := fun (n : A) ↦ ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n))) : A × A).1 *
      g (↑(x.snd (β := fun (n : A) ↦ ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n))) : A × A).2
x : A
f₁ :
  ∑' (b : (↑(↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ x) : Set (A × A)) : Type u_4)),
    f (↑b : A × A).1 * g (↑b : A × A).2
| ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ x, f kl.1 * g kl.2

Tactic:
rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]

Premises used: tsum_fintype, Finset.sum_finset_coe