awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst : Semiring R
inst_1 : Finite ι
inst_2 : Finite ι'
F : Type u_8
inst_3 : FunLike F R ℝ
inst_4 : NonnegHomClass F R ℝ
inst_5 : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
h : Nonempty ι
h_1 : Nonempty ι'
⊢ ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
have inr : Eq (α := ℝ) (⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2))
  (⨆ (i : ι), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : R) → ℝ) (x i) : ℝ) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j) : ℝ))
Tactic: simp_rw [Real.iSup_mul_of_nonneg (iSup_nonneg fun i ↦ apply_nonneg v (y i)),
    Real.mul_iSup_of_nonneg (apply_nonneg v _), map_mul, Finite.ciSup_prod]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst : Semiring R
inst_1 : Finite ι
inst_2 : Finite ι'
F : Type u_8
inst_3 : FunLike F R ℝ
inst_4 : NonnegHomClass F R ℝ
inst_5 : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
h : Nonempty ι
h_1 : Nonempty ι'
inr :
  Eq (α := ℝ) (⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2))
    (⨆ (i : ι), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : R) → ℝ) (x i) : ℝ) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j) : ℝ))
⊢ ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
have inr₁ : Eq (α := ℝ) (⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2))
  (⨆ (i : ι), ⨆ (i_1 : ι'), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : R) → ℝ) (x i) : ℝ) ((v : (a : R) → ℝ) (y i_1) : ℝ))
Tactic: simp_rw [Real.iSup_mul_of_nonneg (iSup_nonneg fun i ↦ apply_nonneg v (y i)),
    Real.mul_iSup_of_nonneg (apply_nonneg v _), map_mul, Finite.ciSup_prod]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
R : Type u_5
ι : Type u_6
ι' : Type u_7
inst : Semiring R
inst_1 : Finite ι
inst_2 : Finite ι'
F : Type u_8
inst_3 : FunLike F R ℝ
inst_4 : NonnegHomClass F R ℝ
inst_5 : MulHomClass F R ℝ
v : F
x : ι → R
y : ι' → R
h : Nonempty ι
h_1 : Nonempty ι'
inr :
  Eq (α := ℝ) (⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2))
    (⨆ (i : ι), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : R) → ℝ) (x i) : ℝ) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j) : ℝ))
inr₁ :
  Eq (α := ℝ) (⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2))
    (⨆ (i : ι), ⨆ (i_1 : ι'), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : R) → ℝ) (x i) : ℝ) ((v : (a : R) → ℝ) (y i_1) : ℝ))
⊢ ⨆ (a : ι × ι'), (v : (a : R) → ℝ) (x a.1 * y a.2) =
    HMul.hMul (α := ℝ) (⨆ (i : ι), (v : (a : R) → ℝ) (x i)) (⨆ (j : ι'), (v : (a : R) → ℝ) (y j))
have inr₂ : Eq (α := ℝ)
  (⨆ (a : ι × ι'), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : R) → ℝ) (x a.1) : ℝ) ((v : (a : R) → ℝ) (y a.2) : ℝ))
  (⨆ (i : ι), ⨆ (i_1 : ι'), HMul.hMul (α := ℝ) (β := ℝ) ((v : (a : R) → ℝ) (x i) : ℝ) ((v : (a : R) → ℝ) (y i_1) : ℝ))
Tactic: simp_rw [Real.iSup_mul_of_nonneg (iSup_nonneg fun i ↦ apply_nonneg v (y i)),
    Real.mul_iSup_of_nonneg (apply_nonneg v _), map_mul, Finite.ciSup_prod]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
⊢ Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)
have inl : ∀ (h : IsEmpty ((a : α) → ι a)), Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)
Tactic: rcases isEmpty_or_nonempty ((a : α) → ι a) with h | h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
inl :
  ∀ (h : IsEmpty ((a : α) → ι a)), Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)
⊢ Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)
have inr : ∀ (h : Nonempty ((a : α) → ι a)), Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)
Tactic: rcases isEmpty_or_nonempty ((a : α) → ι a) with h | h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : IsEmpty ((a : α) → ι a)
⊢ Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)
have inl : ∃ (a : α), Membership.mem (γ := Finset α) Finset.univ a ∧ Eq (α := ℝ) (⨆ (i : ι a), f a i) 0
Tactic: rw [iSup_of_isEmpty, eq_comm, Finset.prod_eq_zero_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : IsEmpty ((a : α) → ι a)
⊢ ∃ (a : α), Membership.mem (γ := Finset α) Finset.univ a ∧ Eq (α := ℝ) (⨆ (i : ι a), f a i) 0
have inl : ∀ (a : α) (ha : IsEmpty.{u + 1} (ι a)),
  ∃ (a : α), Membership.mem (γ := Finset α) Finset.univ a ∧ Eq (α := ℝ) (⨆ (i : ι a), f a i) 0
Tactic: obtain ⟨a, ha⟩ := isEmpty_pi.mp h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
⊢ Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)
have inr : LE.le (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
inr : LE.le (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)
⊢ Eq (α := ℝ) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a)) (∏ a : α, ⨆ (i : ι a), f a i)
have inr₁ : LE.le (α := ℝ) (∏ a : α, ⨆ (i : ι a), f a i) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (hypothesis)
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : Nonempty ((a : α) → ι a)
⊢ LE.le (α := ℝ) (∏ a : α, ⨆ (i : ι a), f a i) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))
have h₁ : ∀ (i : α), Nonempty.{u + 1} (ι i)
Tactic: rw [Classical.nonempty_pi] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (hypothesis)
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : ∀ (i : α), Nonempty.{u + 1} (ι i)
⊢ LE.le (α := ℝ) (∏ a : α, ⨆ (i : ι a), f a i) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))
have H : ∀ (a : α), ∃ (i : ι a), f a i = ⨆ (i : ι a), f a i
Tactic: have H a : ∃ i : ι a, f a i = ⨆ i, f a i := exists_eq_ciSup_of_finite
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : ∀ (i : α), Nonempty.{u + 1} (ι i)
H : ∀ (a : α), ∃ (i : ι a), f a i = ⨆ (i : ι a), f a i
⊢ LE.le (α := ℝ) (∏ a : α, ⨆ (i : ι a), f a i) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))
have inr : ∀ (i : (a : α) → ι a) (hi : ∀ (a : α), f a (i a) = ⨆ (i : ι a), f a i),
  LE.le (α := ℝ) (∏ a : α, ⨆ (i : ι a), f a i) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))
Tactic: choose i hi using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.Basic (goal)
Goal:
α : Type u_5
inst : Fintype α
ι : α → Type u
inst_1 : ∀ (a : α), Finite.{u + 1} (ι a)
f : (a : α) → ι a → ℝ
hf₀ : ∀ (a : α) (i : ι a), 0 ≤ f a i
h : ∀ (i : α), Nonempty.{u + 1} (ι i)
i : (a : α) → ι a
hi : ∀ (a : α), f a (i a) = ⨆ (i : ι a), f a i
⊢ LE.le (α := ℝ) (∏ a : α, ⨆ (i : ι a), f a i) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))
have inr : LE.le (α := ℝ) (∏ x : α, f x (i x)) (⨆ (i : (a : α) → ι a), ∏ a : α, f a (i a))
Tactic: simp only [← hi]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteProd (goal)
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∏' (k : β), (1 + g k)))
have inl : ∀ (hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) ⊥ (𝓝 (g k)))
  (h_bound : ∀ᶠ (n : α) in ⊥, ∀ (k : β), ‖f n k‖ ≤ bound k),
  Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) ⊥ (𝓝 (∏' (k : β), (1 + g k)))
Tactic: rcases eq_or_neBot 𝓕 with rfl | _
Cleared hypotheses: 𝓕, hab, h_bound
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteProd (goal)
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
inl :
  ∀ (hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) ⊥ (𝓝 (g k)))
    (h_bound : ∀ᶠ (n : α) in ⊥, ∀ (k : β), ‖f n k‖ ≤ bound k),
    Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) ⊥ (𝓝 (∏' (k : β), (1 + g k)))
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∏' (k : β), (1 + g k)))
have inr : 𝓕.NeBot → Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∏' (k : β), (1 + g k)))
Tactic: rcases eq_or_neBot 𝓕 with rfl | _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteProd (hypothesis)
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∏' (k : β), (1 + g k)))
have h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
Tactic: have h_bound_g (k) : ‖g k‖ ≤ bound k :=
    le_of_tendsto ((hab k).norm) (h_bound.mono fun n hn ↦ hn k)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteProd (hypothesis)
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∏' (k : β), (1 + g k)))
have hsum_g : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
Tactic: have hsum_g : Summable (‖g ·‖) := h_sum.of_nonneg_of_le (fun _ ↦ norm_nonneg _) h_bound_g
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteProd (goal)
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
hsum_g : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∏' (k : β), (1 + g k)))
have inr : Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∑' (s : Finset β), ∏ i ∈ s, g i))
Tactic: rw [show ∏' k, (1 + g k) = ∑' s, ∏ i ∈ s, g i from
    tprod_one_add (summable_finsetProd_of_summable_norm hsum_g)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteProd (hypothesis)
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
hsum_g : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∑' (s : Finset β), ∏ i ∈ s, g i))
have this : Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ ∑' (k : Finset β), ∏ c ∈ k, f x c) 𝓕 (𝓝 (∑' (k : Finset β), ∏ c ∈ k, g c))
Tactic: have : Tendsto (∑' k, ∏ c ∈ k, f · c) 𝓕 (𝓝 (∑' k, ∏ c ∈ k, g c)) :=
    tendsto_tsum_of_dominated_convergence (summable_finsetProd_of_summable_nonneg
      (fun i ↦ (norm_nonneg (g i)).trans (h_bound_g i)) h_sum)
      (tendsto_finsetProd · fun i _ ↦ hab i)
      (h_bound.mono fun n hn s ↦ (Finset.norm_prod_le s (f n)).trans
      (Finset.prod_le_prod (by grind) (by grind)))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteProd (goal)
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
hsum_g : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
this :
  Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ ∑' (k : Finset β), ∏ c ∈ k, f x c) 𝓕 (𝓝 (∑' (k : Finset β), ∏ c ∈ k, g c))
⊢ Tendsto.{u_1, u_2} (β := R) (fun (n : α) ↦ ∏' (k : β), (1 + f n k)) 𝓕 (𝓝 (∑' (s : Finset β), ∏ i ∈ s, g i))
have apply : ∀ (n : α) (hn : ∀ (k : β), ‖f n k‖ ≤ bound k),
  Eq.{u_2 + 1} (α := R) (∑' (k : Finset β), ∏ c ∈ k, f n c) (∏' (k : β), (1 + f n k))
Tactic: apply this.congr' (h_bound.mono fun n hn ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteProd (goal)
Goal:
α : Type u_1
R : Type u_2
β : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
g : β → R
bound : β → ℝ
𝓕 : Filter α
f : α → β → R
h_sum : Summable bound
hab : ∀ (k : β), Tendsto (fun (x : α) ↦ f x k) 𝓕 (𝓝 (g k))
h_bound : ∀ᶠ (n : α) in 𝓕, ∀ (k : β), ‖f n k‖ ≤ bound k
h : 𝓕.NeBot
h_bound_g : ∀ (k : β), ‖g k‖ ≤ bound k
hsum_g : Summable (α := ℝ) fun (x : β) ↦ ‖g x‖
this :
  Tendsto.{u_1, u_2} (β := R) (fun (x : α) ↦ ∑' (k : Finset β), ∏ c ∈ k, f x c) 𝓕 (𝓝 (∑' (k : Finset β), ∏ c ∈ k, g c))
n : α
hn : ∀ (k : β), ‖f n k‖ ≤ bound k
⊢ Eq.{u_2 + 1} (α := R) (∑' (k : Finset β), ∏ c ∈ k, f n c) (∏' (k : β), (1 + f n k))
have rw : Summable.{u_2, u_3} (α := R) fun (x : Finset β) ↦ ∏ i ∈ x, f n i
Tactic: rw [tprod_one_add]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
Goal:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst : NormedRing R
f : ι → R
g : ι' → R
hf : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ι') ↦ ‖g x‖
h'g : Summable g
⊢ Summable (α := R) fun (x : ι × ι') ↦ f x.1 * g x.2
have suffices : HasSum (fun (x : ι × ι') ↦ f x.1 * g x.2) (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j))
Tactic: suffices HasSum (fun x : ι × ι' => f x.1 * g x.2) ((∑' i, f i) * (∑' j, g j)) from this.summable
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
Goal:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst : NormedRing R
f : ι → R
g : ι' → R
hf : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ι') ↦ ‖g x‖
h'g : Summable g
s : Prod.{u_2, u_3} (Finset ι) (Finset ι') → Finset (ι × ι') :=
  fun (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
⊢ HasSum (fun (x : ι × ι') ↦ f x.1 * g x.2) (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j))
have apply : Tendsto (fun (b : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) atTop
  (𝓝 (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j)))
Tactic: apply hasSum_of_subseq_of_summable (hf.mul_norm hg) tendsto_finsetProd_atTop
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
Goal:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst : NormedRing R
f : ι → R
g : ι' → R
hf : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ι') ↦ ‖g x‖
h'g : Summable g
s : Prod.{u_2, u_3} (Finset ι) (Finset ι') → Finset (ι × ι') :=
  fun (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
⊢ Tendsto (fun (b : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) atTop
    (𝓝 (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j)))
have rw : Tendsto (fun (b : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2)
  (SProd.sprod (α := Filter (Finset ι)) (β := Filter (Finset ι')) atTop atTop)
  (𝓝 (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j)))
Tactic: rw [← prod_atTop_atTop_eq]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (hypothesis)
Goal:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst : NormedRing R
f : ι → R
g : ι' → R
hf : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ι') ↦ ‖g x‖
h'g : Summable g
s : Prod.{u_2, u_3} (Finset ι) (Finset ι') → Finset (ι × ι') :=
  fun (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
⊢ Tendsto (fun (b : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2)
    (SProd.sprod (α := Filter (Finset ι)) (β := Filter (Finset ι')) atTop atTop)
    (𝓝 (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j)))
have this : Tendsto (Prod.map (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) fun (s : Finset ι') ↦ ∑ b ∈ s, g b)
  ((SummationFilter.unconditional ι).filter ×ˢ (SummationFilter.unconditional ι').filter)
  (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 (∑' (b : ι), f b)) (𝓝 (∑' (b : ι'), g b)))
Tactic: have := Tendsto.prodMap h'f.hasSum h'g.hasSum
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (hypothesis)
Goal:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst : NormedRing R
f : ι → R
g : ι' → R
hf : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ι') ↦ ‖g x‖
h'g : Summable g
s : Prod.{u_2, u_3} (Finset ι) (Finset ι') → Finset (ι × ι') :=
  fun (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
this :
  Tendsto (Prod.map (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) fun (s : Finset ι') ↦ ∑ b ∈ s, g b)
    ((SummationFilter.unconditional ι).filter ×ˢ (SummationFilter.unconditional ι').filter)
    (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 (∑' (b : ι), f b)) (𝓝 (∑' (b : ι'), g b)))
⊢ Tendsto (fun (b : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2)
    (SProd.sprod (α := Filter (Finset ι)) (β := Filter (Finset ι')) atTop atTop)
    (𝓝 (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j)))
have this₁ : Tendsto (β := R × R) (Prod.map (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) fun (s : Finset ι') ↦ ∑ b ∈ s, g b)
  ((SummationFilter.unconditional ι).filter ×ˢ (SummationFilter.unconditional ι').filter)
  (𝓝 (∑' (b : ι), f b, ∑' (b : ι'), g b))
Tactic: rw [← nhds_prod_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
Goal:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst : NormedRing R
f : ι → R
g : ι' → R
hf : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ι') ↦ ‖g x‖
h'g : Summable g
s : Prod.{u_2, u_3} (Finset ι) (Finset ι') → Finset (ι × ι') :=
  fun (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ p.1 ×ˢ p.2
this :
  Tendsto (β := R × R) (Prod.map (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) fun (s : Finset ι') ↦ ∑ b ∈ s, g b)
    ((SummationFilter.unconditional ι).filter ×ˢ (SummationFilter.unconditional ι').filter)
    (𝓝 (∑' (b : ι), f b, ∑' (b : ι'), g b))
⊢ Tendsto (fun (b : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2)
    (SProd.sprod (α := Filter (Finset ι)) (β := Filter (Finset ι')) atTop atTop)
    (𝓝 (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j)))
have h : ∀ (p : Prod.{u_2, u_3} (Finset ι) (Finset ι')),
  Eq.{u_1 + 1} (α := R) (∑ i ∈ p.1 ×ˢ p.2, f i.1 * g i.2)
    (((fun (p : R × R) ↦ p.1 * p.2) ∘ Prod.map (fun (s : Finset ι) ↦ ∑ b ∈ s, f b) fun (s : Finset ι') ↦ ∑ b ∈ s, g b)
      p)
Tactic: convert!
    ((continuous_mul (M := R)).continuousAt (x := (∑' (i : ι), f i, ∑' (j : ι'), g j))).tendsto.comp
      this with
    p
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
Goal:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst : NormedRing R
f : ι → R
g : ι' → R
hf : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ι') ↦ ‖g x‖
h'g : Summable g
⊢ Summable (α := R) fun (x : ι × ι') ↦ f x.1 * g x.2
have suffices : HasSum (fun (x : ι × ι') ↦ f x.1 * g x.2) (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j))
Tactic: classical
  suffices HasSum (fun x : ι × ι' => f x.1 * g x.2) ((∑' i, f i) * (∑' j, g j)) from this.summable
  let s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2
  apply hasSum_of_subseq_of_summable (hf.mul_norm hg) tendsto_finsetProd_atTop
  rw [← prod_atTop_atTop_eq]
  have := Tendsto.prodMap h'f.hasSum h'g.hasSum
  rw [← nhds_prod_eq] at this
  convert!
    ((continuous_mul (M := R)).continuousAt (x := (∑' (i : ι), f i, ∑' (j : ι'), g j))).tendsto.comp
      this with
    p
  simp [sum_product, ← mul_sum, ← sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Ring.InfiniteSum (goal)
Goal:
R : Type u_1
ι : Type u_2
ι' : Type u_3
inst : NormedRing R
f : ι → R
g : ι' → R
hf : Summable (α := ℝ) fun (x : ι) ↦ ‖f x‖
h'f : Summable f
hg : Summable (α := ℝ) fun (x : ι') ↦ ‖g x‖
h'g : Summable g
suffices suffices₁ suffices₂ :
  HasSum (fun (x : ι × ι') ↦ f x.1 * g x.2) (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j))
suffices₃ : HasSum (fun (x : ι × ι') ↦ f x.1 * g x.2) (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j))
⊢ Summable (α := R) fun (x : ι × ι') ↦ f x.1 * g x.2
have suffices₄ : Tendsto (fun (b : Prod.{u_2, u_3} (Finset ι) (Finset ι')) ↦ ∑ i ∈ b.1 ×ˢ b.2, f i.1 * g i.2) atTop
  (𝓝 (HMul.hMul (α := R) (∑' (i : ι), f i) (∑' (j : ι'), g j)))
Tactic: classical
  suffices HasSum (fun x : ι × ι' => f x.1 * g x.2) ((∑' i, f i) * (∑' j, g j)) from this.summable
  let s : Finset ι × Finset ι' → Finset (ι × ι') := fun p ↦ p.1 ×ˢ p.2
  apply hasSum_of_subseq_of_summable (hf.mul_norm hg) tendsto_finsetProd_atTop
  rw [← prod_atTop_atTop_eq]
  have := Tendsto.prodMap h'f.hasSum h'g.hasSum
  rw [← nhds_prod_eq] at this
  convert!
    ((continuous_mul (M := R)).continuousAt (x := (∑' (i : ι), f i, ∑' (j : ι'), g j))).tendsto.comp
      this with
    p
  simp [sum_product, ← mul_sum, ← sum_mul]