awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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),
    ∑' (b : (↑(↑(@antidiagonal _ AddCommMonoid.toAddMonoid _ x) : Set (A × A)) : Type u_4)),
      f (↑b : A × A).1 * g (↑b : A × A).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; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]

Premises used: tsum_fintype, Finset.sum_finset_coe
-- 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
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
⊢ Summable.{u_3, u_4} (α := α) fun (n : A) ↦ ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2

Tactic:
conv => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]

Premises used: tsum_fintype, Finset.sum_finset_coe
-- 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
⊢ 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:
h.sigma' fun n ↦ (hasSum_fintype _).summable

Premises used: HMul.hMul, Membership.mem, Subtype, hasSum_fintype, Prod.fst, HasSum.summable, Summable.sigma', Sigma.mk, Sigma.snd, Subtype.val, Prod.snd, Finset.HasAntidiagonal.antidiagonal, SummationFilter.unconditional
-- 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
⊢ 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:
exact h.sigma' fun n ↦ (hasSum_fintype _).summable

Premises used: HMul.hMul, Membership.mem, Subtype, hasSum_fintype, Prod.fst, HasSum.summable, Summable.sigma', Sigma.mk, Sigma.snd, Subtype.val, Prod.snd, Finset.HasAntidiagonal.antidiagonal, SummationFilter.unconditional
-- 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 α
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
L : SummationFilter.unconditional A
| ∑' (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 α
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), ∑ 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 α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.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
-- 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 α
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
L : SummationFilter.unconditional A
| ∑' (n : A), ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2

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

Premises used: tsum_fintype, Finset.sum_finset_coe
-- 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 α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2
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
⊢ HMul.hMul (α := α) (∑' (n : A), f n) (∑' (n : A), g n) =
    ∑' (n : A), ∑ kl ∈ @antidiagonal _ AddCommMonoid.toAddMonoid _ n, f kl.1 * g kl.2

Tactic:
conv_rhs => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype (L := .unconditional _)]

Premises used: tsum_fintype, Finset.sum_finset_coe
-- 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 α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2
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)
⊢ 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:
rw [hf.tsum_mul_tsum hg hfg, ← sigmaAntidiagonalEquivProd.tsum_eq (_ : A × A → α)]

Premises used: Summable.tsum_mul_tsum, Finset.sigmaAntidiagonalEquivProd, Equiv.tsum_eq
-- 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 α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2
⊢ 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:
(summable_mul_prod_iff_summable_mul_sigma_antidiagonal.mp hfg).tsum_sigma'
    (fun n ↦ (hasSum_fintype _).summable)

Premises used: HMul.hMul, summable_mul_prod_iff_summable_mul_sigma_antidiagonal, Finset.sigmaAntidiagonalEquivProd, Membership.mem, Subtype, hasSum_fintype, Prod.fst, HasSum.summable, Summable.tsum_sigma', Iff.mp, Sigma.mk, Prod.snd, DFunLike.coe, Finset.HasAntidiagonal.antidiagonal, SummationFilter.unconditional
-- 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 α
hf : Summable f
hg : Summable g
hfg : Summable.{u_3, u_4} (α := α) fun (x : A × A) ↦ f x.1 * g x.2
⊢ 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:
exact (summable_mul_prod_iff_summable_mul_sigma_antidiagonal.mp hfg).tsum_sigma'
    (fun n ↦ (hasSum_fintype _).summable)

Premises used: summable_mul_prod_iff_summable_mul_sigma_antidiagonal, hasSum_fintype, HasSum.summable, Summable.tsum_sigma', Iff.mp, Sigma.mk, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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
simp_rw : Summable.{u_3, 0} (α := α) fun (n : ℕ) ↦ ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2
⊢ Summable.{u_3, 0} (α := α) fun (n : ℕ) ↦ ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l ↦ f k * g l]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, HMul.hMul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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 : ℕ) ↦ ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2

Tactic:
summable_sum_mul_antidiagonal_of_summable_mul h

Premises used: summable_sum_mul_antidiagonal_of_summable_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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 : ℕ) ↦ ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2

Tactic:
exact summable_sum_mul_antidiagonal_of_summable_mul h

Premises used: summable_sum_mul_antidiagonal_of_summable_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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
simp_rw :
  HMul.hMul (α := α) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) =
    ∑' (n : ℕ), ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2
⊢ HMul.hMul (α := α) (∑' (n : ℕ), f n) (∑' (n : ℕ), g n) = ∑' (n : ℕ), ∑ k ∈ range (n + 1), f k * g (n - k)

Tactic:
simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l ↦ f k * g l]

Premises used: Finset.Nat.sum_antidiagonal_eq_sum_range_succ, HMul.hMul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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 : ℕ), ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2

Tactic:
hf.tsum_mul_tsum_eq_tsum_sum_antidiagonal hg hfg

Premises used: Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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 : ℕ), ∑ ij ∈ @antidiagonal _ Nat.instAddMonoid _ n, f ij.1 * g ij.2

Tactic:
exact hf.tsum_mul_tsum_eq_tsum_sum_antidiagonal hg hfg

Premises used: Summable.tsum_mul_tsum_eq_tsum_sum_antidiagonal
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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

Tactic:
tendsto_nhds_unique (h.hasSum.mul_right (1 - x)).tendsto_sum_nat ?_

Premises used: HasSum.tendsto_sum_nat, HSub.hSub, Summable.hasSum, HasSum.mul_right, OfNat.ofNat, tendsto_nhds_unique
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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
refine : Tendsto.{0, u_3} (β := α) (fun (n : ℕ) ↦ ∑ i ∈ range n, x ^ i * (1 - x)) atTop (nhds 1)
⊢ (∑' (i : ℕ), x ^ i) * (1 - x) = 1

Tactic:
refine tendsto_nhds_unique (h.hasSum.mul_right (1 - x)).tendsto_sum_nat ?_

Premises used: HasSum.tendsto_sum_nat, HSub.hSub, Summable.hasSum, HasSum.mul_right, OfNat.ofNat, tendsto_nhds_unique
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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
⊢ Tendsto.{0, u_3} (β := α) (fun (n : ℕ) ↦ ∑ i ∈ range n, x ^ i * (1 - x)) atTop (nhds 1)

Tactic:
simpa [← Finset.sum_mul, geom_sum_mul_neg] using tendsto_const_nhds.sub h.tendsto_atTop_zero

Premises used: tendsto_const_nhds, Summable.tendsto_atTop_zero, geom_sum_mul_neg, Filter.Tendsto.sub, Finset.sum_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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

Tactic:
tendsto_nhds_unique (h.hasSum.mul_left (1 - x)).tendsto_sum_nat ?_

Premises used: HasSum.tendsto_sum_nat, HSub.hSub, HasSum.mul_left, Summable.hasSum, OfNat.ofNat, tendsto_nhds_unique
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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
refine : Tendsto.{0, u_3} (β := α) (fun (n : ℕ) ↦ ∑ i ∈ range n, (1 - x) * x ^ i) atTop (nhds 1)
⊢ (1 - x) * ∑' (i : ℕ), x ^ i = 1

Tactic:
refine tendsto_nhds_unique (h.hasSum.mul_left (1 - x)).tendsto_sum_nat ?_

Premises used: HasSum.tendsto_sum_nat, HSub.hSub, HasSum.mul_left, Summable.hasSum, OfNat.ofNat, tendsto_nhds_unique
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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
⊢ Tendsto.{0, u_3} (β := α) (fun (n : ℕ) ↦ ∑ i ∈ range n, (1 - x) * x ^ i) atTop (nhds 1)

Tactic:
simpa [← Finset.mul_sum, mul_neg_geom_sum] using tendsto_const_nhds.sub h.tendsto_atTop_zero

Premises used: Finset.mul_sum, tendsto_const_nhds, mul_neg_geom_sum, Summable.tendsto_atTop_zero, Filter.Tendsto.sub
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun (x : Finset ι) ↦ ∏ i ∈ x, f i) a
simp_rw :
  Tendsto (fun (s : Finset ι) ↦ ∑ t ∈ s.powerset, ∏ i ∈ t, f i) (SummationFilter.unconditional ι).filter (nhds a)
⊢ HasProd (fun (x : ι) ↦ 1 + f x) a

Tactic:
simp_rw [HasProd, prod_one_add]

Premises used: HasProd, Finset.prod_one_add, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun (x : Finset ι) ↦ ∏ i ∈ x, f i) a
⊢ Tendsto (fun (s : Finset ι) ↦ ∑ t ∈ s.powerset, ∏ i ∈ t, f i) (SummationFilter.unconditional ι).filter (nhds a)

Tactic:
h.comp tendsto_finset_powerset_atTop_atTop

Premises used: Multiset.sum, Multiset.foldr, Multiset.powerset, Filter.tendsto_finset_powerset_atTop_atTop, Filter.Tendsto.comp, Finset.sum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun (x : Finset ι) ↦ ∏ i ∈ x, f i) a
⊢ Tendsto (fun (s : Finset ι) ↦ ∑ t ∈ s.powerset, ∏ i ∈ t, f i) (SummationFilter.unconditional ι).filter (nhds a)

Tactic:
exact h.comp tendsto_finset_powerset_atTop_atTop

Premises used: Filter.tendsto_finset_powerset_atTop_atTop, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
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
obtain :
  ∀ (a : α) (h : HasSum (fun (x : Finset ι) ↦ ∏ i ∈ x, f i) a), Multipliable.{u_3, u_1} (α := α) fun (x : ι) ↦ 1 + f x
⊢ Multipliable.{u_3, u_1} (α := α) fun (x : ι) ↦ 1 + f x

Tactic:
obtain ⟨a, h⟩ := h
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun (x : Finset ι) ↦ ∏ i ∈ x, f i) a
⊢ Multipliable.{u_3, u_1} (α := α) fun (x : ι) ↦ 1 + f x

Tactic:
⟨a, hasProd_one_add_of_hasSum_prod h⟩

Premises used: hasProd_one_add_of_hasSum_prod, Multipliable, Exists.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
a : α
h : HasSum (fun (x : Finset ι) ↦ ∏ i ∈ x, f i) a
⊢ Multipliable.{u_3, u_1} (α := α) fun (x : ι) ↦ 1 + f x

Tactic:
exact ⟨a, hasProd_one_add_of_hasSum_prod h⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : T2Space α
h : Summable.{u_3, u_1} (α := α) fun (x : Finset ι) ↦ ∏ i ∈ x, f i
⊢ Eq.{u_3 + 1} (α := α) (∏' (i : ι), (1 + f i)) (∑' (s : Finset ι), ∏ i ∈ s, f i)

Tactic:
HasProd.tprod_eq <| hasProd_one_add_of_hasSum_prod h.hasSum

Premises used: hasProd_one_add_of_hasSum_prod, HasProd.tprod_eq, Summable.hasSum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
hsum : Summable.{u_3, u_1} (α := α) fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)
hprod : Multipliable.{u_3, u_1} (α := α) fun (x : ι) ↦ 1 + f x
inl : IsEmpty ι → ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
inr : Nonempty ι → ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
⊢ ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))

Tactic:
rcases isEmpty_or_nonempty ι with _ | _

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
hsum : Summable.{u_3, u_1} (α := α) fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)
hprod : Multipliable.{u_3, u_1} (α := α) fun (x : ι) ↦ 1 + f x
h : IsEmpty ι
⊢ ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
hsum : Summable.{u_3, u_1} (α := α) fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)
hprod : Multipliable.{u_3, u_1} (α := α) fun (x : ι) ↦ 1 + f x
h : Nonempty ι
inr :
  ∀ (x : α) (hx : HasProd (fun (x : ι) ↦ 1 + f x) x),
    ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
⊢ ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))

Tactic:
obtain ⟨x, hx⟩ := hprod
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
hsum : Summable.{u_3, u_1} (α := α) fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)
h : Nonempty ι
x : α
hx : HasProd (fun (x : ι) ↦ 1 + f x) x
inr :
  ∀ (a : α) (ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a),
    ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))
⊢ ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))

Tactic:
obtain ⟨a, ha⟩ := hsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
h : Nonempty ι
x : α
hx : HasProd (fun (x : ι) ↦ 1 + f x) x
a : α
ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a
⊢ ∏' (b : ι), (1 + f b) = x

Tactic:
hx.tprod_eq

Premises used: HasProd.tprod_eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Ring
Goal:
ι : Type u_1
α : Type u_3
inst : CommSemiring α
inst_1 : TopologicalSpace α
f : ι → α
inst_2 : LinearOrder ι
inst_3 : LocallyFiniteOrderBot ι
inst_4 : T2Space α
inst_5 : ContinuousAdd α
h_1 : Nonempty ι
x : α
hx : HasProd (fun (x : ι) ↦ 1 + f x) x
a : α
ha : HasSum (fun (i : ι) ↦ f i * ∏ j ∈ Iio i, (1 + f j)) a
h : HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j)) = x
⊢ ∏' (i : ι), (1 + f i) = HAdd.hAdd (α := α) 1 (∑' (i : ι), f i * ∏ j ∈ Iio i, (1 + f j))

Tactic:
convert! hx.tprod_eq

Premises used: HasProd.tprod_eq