awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
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
⊢ Summable f ↔ ¬Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop
have rw₂ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop ↔
  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]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
Goal:
α : Type u_4
β : α → Type u_3
f : (x : α) × β x → ℝ
hf : ∀ (x : (x : α) × β x), 0 ≤ f x
⊢ 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)
have 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)
Tactic: lift f to (Σ x, β x) → ℝ≥0 using hf
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
Goal:
f : ℕ → ℝ
c : ℝ
hf : ∀ (n : ℕ), 0 ≤ f n
h : ∀ (n : ℕ), ∑ i ∈ range n, f i ≤ c
⊢ Summable f
have refine : ∀ (H : Tendsto (β := ℝ) (fun (n : ℕ) ↦ ∑ i ∈ range n, f i) atTop atTop), False
Tactic: refine (summable_iff_not_tendsto_nat_atTop_of_nonneg hf).2 fun H => ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Real (goal)
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
⊢ False
have rcases : ∀ (n : ℕ) (hn : c < ∑ i ∈ range n, f i), False
Tactic: rcases exists_lt_of_tendsto_atTop H 0 c with ⟨n, -, hn⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b
have pos : ∀ (hf : Summable f L), SemiconjBy (∑'[L] (i : ι), f i) a b
Tactic: by_cases hf : Summable f L
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b
have neg : ∀ (hf : ¬Summable f L), SemiconjBy (∑'[L] (i : ι), f i) a b
Tactic: by_cases hf : Summable f L
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
have pos : (∑'[L] (i : ι), f i) * a = b * ∑'[L] (i : ι), f i
Tactic: rw [SemiconjBy, ← hf.tsum_mul_right a, ← hf.tsum_mul_left b, tsum_congr h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b
have pos₁ : ∑'[L] (i : ι), f i * a = b * ∑'[L] (i : ι), f i
Tactic: rw [SemiconjBy, ← hf.tsum_mul_right a, ← hf.tsum_mul_left b, tsum_congr h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b
have pos₂ : Eq.{u_3 + 1} (α := α) (∑'[L] (i : ι), f i * a) (∑'[L] (i : ι), b * f i)
Tactic: rw [SemiconjBy, ← hf.tsum_mul_right a, ← hf.tsum_mul_left b, tsum_congr h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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)
⊢ SemiconjBy (∑'[L] (i : ι), f i) a b
have pos₃ : Eq.{u_3 + 1} (α := α) (∑'[L] (b_1 : ι), b * f b_1) (∑'[L] (i : ι), b * f i)
Tactic: rw [SemiconjBy, ← hf.tsum_mul_right a, ← hf.tsum_mul_left b, tsum_congr h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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)
⊢ SemiconjBy a (∑'[L] (i : ι), f i) (∑'[L] (i : ι), g i)
have rw : Eq.{u_3 + 1} (α := α) (∑'[L] (i : ι), a * f i) (∑'[L] (i : ι), g i * a)
Tactic: rw [SemiconjBy, ← hf.tsum_mul_left a, ← hg.tsum_mul_right a]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
L : SummationFilter ι
inst : DivisionSemiring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalSemiring α
f : ι → α
a : α
inst_3 : T2Space α
⊢ ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x
have pos : ∀ (ha : a = 0), ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
⊢ ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x
have neg : ∀ (ha : ¬a = 0), ∑'[L] (x : ι), a * f x = a * ∑'[L] (x : ι), f x
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
have pos : ∀ (ha : a = 0), ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
⊢ ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a
have neg : ∀ (ha : ¬a = 0), ∑'[L] (x : ι), f x * a = (∑'[L] (x : ι), f x) * a
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (hypothesis)
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 / f i) (b * a) L
have this : HasSum (fun (i : ι) ↦ b * (1 / f i)) (b * a) L
Tactic: have := h.mul_left b
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (hypothesis)
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 (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
have 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
Tactic: rw [summable_mul_prod_iff_summable_mul_sigma_antidiagonal] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
| Summable.{u_3, u_4} (α := α) fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
have f₁ : fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
| Summable.{u_3, u_4} (α := α) fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
have L : SummationFilter.unconditional A
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
| fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
have f₁ : ∀ (x : A), ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ x, f kl.1 * g kl.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
| ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ x, f kl.1 * g kl.2
have f₁ : ∑' (b : (↑(↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ x) : Set (A × A)) : Type u_4)),
  f (↑b : A × A).1 * g (↑b : A × A).2
Tactic: rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
| Summable.{u_3, u_4} (α := α) fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
have f₁ : ∀ (x : A),
  ∑' (b : (↑(↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ x) : Set (A × A)) : Type u_4)),
    f (↑b : A × A).1 * g (↑b : A × A).2
Tactic: congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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),
    ∑' (b : (↑(↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ x) : Set (A × A)) : Type u_4)),
      f (↑b : A × A).1 * g (↑b : A × A).2
| Summable.{u_3, u_4} (α := α) fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
have L : SummationFilter.unconditional A
Tactic: congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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
⊢ Summable.{u_3, u_4} (α := α) fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
have conv : Summable.{u_3, u_4} (α := α) fun (x : A) ↦
  ∑' (b : (↑(↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ x) : Set (A × A)) : Type u_4)),
    f (↑b : A × A).1 * g (↑b : A × A).2
Tactic: conv => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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 α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2
| ∑' (n : A), ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
have f₁ : fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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 α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2
f₁ : fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
| ∑' (n : A), ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
have L : SummationFilter.unconditional A
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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 α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2
| fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
have f₁ : ∀ (x : A), ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ x, f kl.1 * g kl.2
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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 α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2
x : A
| ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ x, f kl.1 * g kl.2
have f₁ : ∑' (b : (↑(↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ x) : Set (A × A)) : Type u_4)),
  f (↑b : A × A).1 * g (↑b : A × A).2
Tactic: rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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 α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2
| ∑' (n : A), ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
have f₁ : ∀ (x : A),
  ∑' (b : (↑(↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ x) : Set (A × A)) : Type u_4)),
    f (↑b : A × A).1 * g (↑b : A × A).2
Tactic: congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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 α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2
f₁ :
  ∀ (x : A),
    ∑' (b : (↑(↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ x) : Set (A × A)) : Type u_4)),
      f (↑b : A × A).1 * g (↑b : A × A).2
| ∑' (n : A), ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
have L : SummationFilter.unconditional A
Tactic: congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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 α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2
⊢ HMul.hMul (α := α) (∑' (n : A), f n) (∑' (n : A), g n) =
    ∑' (n : A), ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2
have conv_rhs : HMul.hMul (α := α) (∑' (n : A), f n) (∑' (n : A), g n) =
  ∑' (x : A) (b : (↑(↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ x) : Set (A × A)) : Type u_4)),
    f (↑b : A × A).1 * g (↑b : A × A).2
Tactic: conv_rhs => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
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 α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2
⊢ HMul.hMul (α := α) (∑' (n : A), f n) (∑' (n : A), g n) =
    ∑' (x : A) (b : (↑(↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ x) : Set (A × A)) : Type u_4)),
      f (↑b : A × A).1 * g (↑b : A × A).2
have rw : Eq.{u_3 + 1} (α := α)
  (∑' (c : (n : A) × ↥(@antidiagonal _ AddCommMonoid.toAddMonoid _ n)),
    f ((sigmaAntidiagonalEquivProd : (a : (n : A) × ↥(antidiagonal n)) → A × A) c).1 *
      g ((sigmaAntidiagonalEquivProd : (a : (n : A) × ↥(antidiagonal n)) → A × A) c).2)
  (∑' (x : A) (b : (↑(↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ x) : Set (A × A)) : Type u_4)),
    f (↑b : A × A).1 * g (↑b : A × A).2)
Tactic: rw [hf.tsum_mul_tsum hg hfg, ← sigmaAntidiagonalEquivProd.tsum_eq (_ : A × A → α)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst_2 : T3Space α
inst_3 : IsTopologicalSemiring α
h : Summable.{u_3, 0} (α := α) fun (x : ℕ × ℕ) ↦ f x.1 * g x.2
⊢ Summable.{u_3, 0} (α := α) fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), f k * g (n - k)
have simp_rw : Summable.{u_3, 0} (α := α) fun (n : ℕ) ↦ ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2
Tactic: simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l ↦ f k * g l]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
α : Type u_3
inst : TopologicalSpace α
inst_1 : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst_2 : T3Space α
inst_3 : IsTopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, 0} (α := α) fun (x : ℕ × ℕ) ↦ f x.1 * g x.2
⊢ HMul.hMul (α := α) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)
have simp_rw : HMul.hMul (α := α) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) =
  ∑' (n : ℕ), ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2
Tactic: simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l ↦ f k * g l]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
α : Type u_3
inst : Ring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalRing α
inst_3 : T2Space α
x : α
h : Summable.{u_3, 0} (α := α) fun (x_1 : ℕ) ↦ x ^ x_1
⊢ (∑' (i : ℕ), x ^ i) * (1 - x) = 1
have refine : Tendsto.{0, u_3} (β := α) (fun (n : ℕ) ↦ ∑ i ∈ range n, x ^ i * (1 - x)) atTop (nhds 1)
Tactic: refine tendsto_nhds_unique (h.hasSum.mul_right (1 - x)).tendsto_sum_nat ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
α : Type u_3
inst : Ring α
inst_1 : TopologicalSpace α
inst_2 : IsTopologicalRing α
inst_3 : T2Space α
x : α
h : Summable.{u_3, 0} (α := α) fun (x_1 : ℕ) ↦ x ^ x_1
⊢ (1 - x) * ∑' (i : ℕ), x ^ i = 1
have refine : Tendsto.{0, u_3} (β := α) (fun (n : ℕ) ↦ ∑ i ∈ range n, (1 - x) * x ^ i) atTop (nhds 1)
Tactic: refine tendsto_nhds_unique (h.hasSum.mul_left (1 - x)).tendsto_sum_nat ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun (x : Finset ι) ↦ ∏ i ∈ x, f i) a
⊢ HasProd (fun (x : ι) ↦ 1 + f x) a
have simp_rw : Tendsto (fun (s : Finset ι) ↦ ∑ t ∈ s.powerset, ∏ i ∈ t, f i) (SummationFilter.unconditional ι).filter (nhds a)
Tactic: simp_rw [HasProd, prod_one_add]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Ring (goal)
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
h : Summable.{u_3, u_1} (α := α) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
⊢ Multipliable.{u_3, u_1} (α := α) fun (x : ι) ↦ 1 + f x
have obtain : ∀ (a : α) (h : HasSum (fun (x : Finset ι) ↦ ∏ i ∈ x, f i) a), Multipliable.{u_3, u_1} (α := α) fun (x : ι) ↦ 1 + f x
Tactic: obtain ⟨a, h⟩ := h
Cleared hypotheses: h