awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
h₁ : ‖(b none).1‖ ≤ ‖b none‖
⊢ ‖B‖ * ‖(b none).1‖ ≤ ‖B‖ * ‖b none‖

Tactic:
gcongr
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
⊢ ‖(b none).1‖ ≤ ‖b none‖

Tactic:
norm_fst_le _

Premises used: norm_fst_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
⊢ ‖(b none).1‖ ≤ ‖b none‖

Tactic:
exact norm_fst_le _

Premises used: norm_fst_le
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ ‖(b (some i)).2 i‖ ≤ ‖b (some i)‖

Tactic:
(norm_le_pi_norm _ _).trans (norm_snd_le _)

Premises used: norm_snd_le, norm_le_pi_norm, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
ι' : Type v'
n : ℕ
E : ι → Type wE
Ei : Fin n.succ → Type wEi
G_1 : Type wG
G' : Type wG'
inst : Fintype ι
inst_1 : Fintype ι'
inst_2 : NontriviallyNormedField 𝕜
inst_3 : (i : ι) → NormedAddCommGroup (E i)
inst_4 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
inst_5 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)
inst_6 : (i : Fin n.succ) → NormedSpace.{u, wEi} 𝕜 (Ei i)
inst_7 : NormedAddCommGroup G_1
inst_8 : NormedSpace 𝕜 G_1
inst_9 : NormedAddCommGroup G'
inst_10 : NormedSpace 𝕜 G'
F : Type u_1
G : Type u_2
inst_11 : NormedAddCommGroup F
inst_12 : NormedSpace 𝕜 F
inst_13 : NormedAddCommGroup G
inst_14 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
b : (i : Option ι) → G × ((i : ι) → E i)
i : ι
h : Membership.mem (γ := Finset ι) univ i
⊢ ‖(b (some i)).2 i‖ ≤ ‖b (some i)‖

Tactic:
exact (norm_le_pi_norm _ _).trans (norm_snd_le _)

Premises used: norm_snd_le, norm_le_pi_norm, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Module.Multilinear.Curry
Goal:
𝕜 : Type u
ι : Type v
E : ι → Type wE
inst : Fintype ι
inst_1 : NontriviallyNormedField 𝕜
inst_2 : (i : ι) → NormedAddCommGroup (E i)
inst_3 : (i : ι) → NormedSpace.{u, wE} 𝕜 (E i)
F : Type u_1
G : Type u_2
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : NormedAddCommGroup G
inst_7 : NormedSpace 𝕜 G
B : G →L[𝕜] ContinuousMultilinearMap 𝕜 E F
a : G
v : (i : ι) → E i
⊢ Eq.{u_1 + 1} (α := F)
    ((B.continuousMultilinearMapOption (E := E) : (a : (i : Option ι) → G × ((i : ι) → E i)) → F) fun (x : Option ι) ↦
        (a, v) :
      F)
    ((((B : (a : G) → ContinuousMultilinearMap 𝕜 E F) a : ContinuousMultilinearMap 𝕜 E F) : (a : (i : ι) → E i) → F) v :
      F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ (g x).re) '' K)
⊢ ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (upperBounds ((fun (x : α) ↦ (g x).re) '' K)) a → ∀ x ∈ K, (g x).re ≤ a

Tactic:
simp [mem_upperBounds]

Premises used: mem_upperBounds
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ (g x).re) '' K)
obtain : ∀ (v : ℝ) (hv : ∀ x ∈ K, (g x).re ≤ v), TendstoUniformlyOn (fun (x : ι) ↦ cexp ∘ f x) (cexp ∘ g) p K
⊢ TendstoUniformlyOn (fun (x : ι) ↦ cexp ∘ f x) (cexp ∘ g) p K

Tactic:
obtain ⟨v, hv⟩ : ∃ v, ∀ x ∈ K, (g x).re ≤ v := hg.imp <| by simp [mem_upperBounds]

Premises used: Exists.imp
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ (g x).re) '' K)
v : ℝ
hv : ∀ x ∈ K, (g x).re ≤ v
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ K, (f i x).re ≤ v + 1

Tactic:
have : ∀ᶠ i in p, ∀ x ∈ K, (f i x).re ≤ v + 1 := hf.re.eventually_forall_le (lt_add_one v) hv
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ (g x).re) '' K)
v : ℝ
hv : ∀ x ∈ K, (g x).re ≤ v
this : ∀ᶠ (i : ι) in p, ∀ x ∈ K, (f i x).re ≤ v + 1
⊢ ∀ᶠ (i : ι) in p, ∀ x ∈ K, Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ v + 1} (f i x)

Tactic:
simpa
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ (g x).re) '' K)
v : ℝ
hv : ∀ x ∈ K, (g x).re ≤ v
this : ∀ᶠ (i : ι) in p, ∀ x ∈ K, (f i x).re ≤ v + 1
refine : ∀ x ∈ K, Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ v + 1} (g x)
⊢ TendstoUniformlyOn (fun (x : ι) ↦ cexp ∘ f x) (cexp ∘ g) p K

Tactic:
refine (UniformContinuousOn.cexp _).comp_tendstoUniformlyOn_eventually (by simpa) ?_ hf

Premises used: UniformContinuousOn.cexp, UniformContinuousOn.comp_tendstoUniformlyOn_eventually
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ (g x).re) '' K)
v : ℝ
hv : ∀ x ∈ K, (g x).re ≤ v
this : ∀ᶠ (i : ι) in p, ∀ x ∈ K, (f i x).re ≤ v + 1
⊢ ∀ x ∈ K, Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ v + 1} (g x)

Tactic:
fun x hx ↦ (hv x hx).trans (lt_add_one v).le

Premises used: Set.Mem, lt_add_one, setOf, LT.lt.le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
K : Set α
f : ι → α → ℂ
p : Filter ι
g : α → ℂ
hf : TendstoUniformlyOn f g p K
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ (g x).re) '' K)
v : ℝ
hv : ∀ x ∈ K, (g x).re ≤ v
this : ∀ᶠ (i : ι) in p, ∀ x ∈ K, (f i x).re ≤ v + 1
⊢ ∀ x ∈ K, Membership.mem (γ := Set ℂ) {x : ℂ | x.re ≤ v + 1} (g x)

Tactic:
exact fun x hx ↦ (hv x hx).trans (lt_add_one v).le

Premises used: lt_add_one, LT.lt.le, LE.le.trans
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
f : ι → α → ℂ
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
simp :
  TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ι) (x2 : α) ↦ ∑ i ∈ x1, log (1 + f i x2))
    (fun (x : α) ↦ ∑' (i : ι), log (1 + f i x)) atTop K
⊢ HasSumUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (1 + f i x)) (fun (x : α) ↦ ∑' (i : ι), log (1 + f i x)) K

Tactic:
simp only [hasSumUniformlyOn_iff_tendstoUniformlyOn]

Premises used: hasSumUniformlyOn_iff_tendstoUniformlyOn
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
f : ι → α → ℂ
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
apply : ∀ᶠ (n : ι) in cofinite, ∀ x ∈ K, ‖log (1 + f n x)‖ ≤ 3 / 2 * u n
⊢ TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ι) (x2 : α) ↦ ∑ i ∈ x1, log (1 + f i x2))
    (fun (x : α) ↦ ∑' (i : ι), log (1 + f i x)) atTop K

Tactic:
apply tendstoUniformlyOn_tsum_of_cofinite_eventually <| hu.mul_left (3 / 2)

Premises used: HDiv.hDiv, tendstoUniformlyOn_tsum_of_cofinite_eventually, Summable.mul_left, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
f : ι → α → ℂ
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
i : ι
hi : ∀ x ∈ K, ‖f i x‖ ≤ u i
hi' : u i ≤ 1 / 2
x : α
hx : x ∈ K
⊢ 3 / 2 * ‖f i x‖ ≤ 3 / 2 * u i

Tactic:
simpa using hi x hx
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
f : ι → α → ℂ
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
h₁ :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x : ι |
        Membership.mem (γ := Set ι) {x : ι | (fun (i : ι) ↦ ∀ x ∈ K, ‖f i x‖ ≤ u i) x} x →
          Membership.mem (γ := Set ι)
            {x : ι |
              Membership.mem (γ := Set ι) {x : ι | (fun (a : ι) ↦ u a ≤ 1 / 2) x} x →
                Membership.mem (γ := Set ι) {x : ι | (fun (n : ι) ↦ ∀ x ∈ K, ‖log (1 + f n x)‖ ≤ 3 / 2 * u n) x} x}
            x}
      a
h₂ h₃ :
  ∀ (i : ι) (hi : ∀ x ∈ K, ‖f i x‖ ≤ u i) (hi' : u i ≤ 1 / 2) (x : α) (hx : x ∈ K), ‖log (1 + f i x)‖ ≤ 3 / 2 * u i
⊢ ∀ᶠ (n : ι) in cofinite, ∀ x ∈ K, ‖log (1 + f n x)‖ ≤ 3 / 2 * u n

Tactic:
filter_upwards [h, hu.tendsto_cofinite_zero.eventually_le_const one_half_pos] with i hi hi' x hx
    using (norm_log_one_add_half_le_self <| (hi x hx).trans hi').trans (by simpa using hi x hx)

Premises used: Filter.Tendsto.eventually_le_const, Summable.tendsto_cofinite_zero, one_half_pos
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
K : Set α
f : ℕ → α → ℂ
u : ℕ → ℝ
hu : Summable u
h : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n
⊢ ∀ᶠ (n : ℕ) in cofinite, ∀ x ∈ K, ‖f n x‖ ≤ u n

Tactic:
rw [← Nat.cofinite_eq_atTop] at h

Premises used: Nat.cofinite_eq_atTop
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
K : Set α
f : ℕ → α → ℂ
u : ℕ → ℝ
hu : Summable u
h : ∀ᶠ (n : ℕ) in cofinite, ∀ x ∈ K, ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (β := ℂ) (fun (n : ℕ) (x : α) ↦ ∑ m ∈ range n, log (1 + f m x))
    (fun (x : α) ↦ ∑' (n : ℕ), log (1 + f n x)) atTop K

Tactic:
(hu.hasSumUniformlyOn_log_one_add h).tendstoUniformlyOn_finsetRange

Premises used: HasSumUniformlyOn.tendstoUniformlyOn_finsetRange, Summable.hasSumUniformlyOn_log_one_add
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
K : Set α
f : ℕ → α → ℂ
u : ℕ → ℝ
hu : Summable u
h : ∀ᶠ (n : ℕ) in cofinite, ∀ x ∈ K, ‖f n x‖ ≤ u n
⊢ TendstoUniformlyOn (β := ℂ) (fun (n : ℕ) (x : α) ↦ ∑ m ∈ range n, log (1 + f m x))
    (fun (x : α) ↦ ∑' (n : ℕ), log (1 + f n x)) atTop K

Tactic:
exact (hu.hasSumUniformlyOn_log_one_add h).tendstoUniformlyOn_finsetRange

Premises used: HasSumUniformlyOn.tendstoUniformlyOn_finsetRange, Summable.hasSumUniformlyOn_log_one_add
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
simp :
  TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ι) (x2 : α) ↦ ∏ i ∈ x1, f i x2) (fun (x : α) ↦ ∏' (i : ι), f i x) atTop
    s
⊢ HasProdUniformlyOn f (fun (x : α) ↦ ∏' (i : ι), f i x) s

Tactic:
simp only [hasProdUniformlyOn_iff_tendstoUniformlyOn]

Premises used: hasProdUniformlyOn_iff_tendstoUniformlyOn
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
obtain :
  ∀ (r : α → ℂ) (hr : HasSumUniformlyOn (fun (i : ι) (x : α) ↦ log (f i x)) r s),
    TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ι) (x2 : α) ↦ ∏ i ∈ x1, f i x2) (fun (x : α) ↦ ∏' (i : ι), f i x)
      atTop s
⊢ TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ι) (x2 : α) ↦ ∏ i ∈ x1, f i x2) (fun (x : α) ↦ ∏' (i : ι), f i x) atTop
    s

Tactic:
obtain ⟨r, hr⟩ := hf.exists

Premises used: SummableUniformlyOn.exists
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
r : α → ℂ
hr : HasSumUniformlyOn (fun (i : ι) (x : α) ↦ log (f i x)) r s
H : TendstoUniformlyOn (fun (s : Finset ι) (x : α) ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop s
⊢ TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ι) (x2 : α) ↦ ∏ i ∈ x1, f i x2) (fun (x : α) ↦ ∏' (i : ι), f i x) atTop
    s

Tactic:
H.congr_right (hr.tsum_eqOn.comp_left.symm.trans ?_)

Premises used: TendstoUniformlyOn.congr_right, Set.EqOn.trans, Set.EqOn.comp_left, HasSumUniformlyOn.tsum_eqOn, Set.EqOn.symm
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
r : α → ℂ
hr : HasSumUniformlyOn (fun (i : ι) (x : α) ↦ log (f i x)) r s
H : TendstoUniformlyOn (fun (s : Finset ι) (x : α) ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop s
refine : Set.EqOn (cexp ∘ fun (x : α) ↦ ∑' (b : ι), log (f b x)) (fun (x : α) ↦ ∏' (i : ι), f i x) s
⊢ TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ι) (x2 : α) ↦ ∏ i ∈ x1, f i x2) (fun (x : α) ↦ ∏' (i : ι), f i x) atTop
    s

Tactic:
refine H.congr_right (hr.tsum_eqOn.comp_left.symm.trans ?_)

Premises used: TendstoUniformlyOn.congr_right, Set.EqOn.trans, Set.EqOn.comp_left, HasSumUniformlyOn.tsum_eqOn, Set.EqOn.symm
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
r : α → ℂ
hr : HasSumUniformlyOn (fun (i : ι) (x : α) ↦ log (f i x)) r s
H : TendstoUniformlyOn (fun (s : Finset ι) (x : α) ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop s
⊢ Set.EqOn (cexp ∘ fun (x : α) ↦ ∑' (b : ι), log (f b x)) (fun (x : α) ↦ ∏' (i : ι), f i x) s

Tactic:
fun x hx ↦ (cexp_tsum_eq_tprod (hfn x hx) (hf.summable hx))

Premises used: Complex.cexp_tsum_eq_tprod, Set.EqOn, SummableUniformlyOn.summable
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
r : α → ℂ
hr : HasSumUniformlyOn (fun (i : ι) (x : α) ↦ log (f i x)) r s
H : TendstoUniformlyOn (fun (s : Finset ι) (x : α) ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop s
⊢ Set.EqOn (cexp ∘ fun (x : α) ↦ ∑' (b : ι), log (f b x)) (fun (x : α) ↦ ∏' (i : ι), f i x) s

Tactic:
exact fun x hx ↦ (cexp_tsum_eq_tprod (hfn x hx) (hf.summable hx))

Premises used: Complex.cexp_tsum_eq_tprod, SummableUniformlyOn.summable
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
r : α → ℂ
hr : HasSumUniformlyOn (fun (i : ι) (x : α) ↦ log (f i x)) r s
suffices : TendstoUniformlyOn (fun (s : Finset ι) (x : α) ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop s
⊢ TendstoUniformlyOn (β := ℂ) (fun (x1 : Finset ι) (x2 : α) ↦ ∏ i ∈ x1, f i x2) (fun (x : α) ↦ ∏' (i : ι), f i x) atTop
    s

Tactic:
suffices H : TendstoUniformlyOn (fun s x ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop s by
    refine H.congr_right (hr.tsum_eqOn.comp_left.symm.trans ?_)
    exact fun x hx ↦ (cexp_tsum_eq_tprod (hfn x hx) (hf.summable hx))
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
r : α → ℂ
hr : HasSumUniformlyOn (fun (i : ι) (x : α) ↦ log (f i x)) r s
⊢ TendstoUniformlyOn (fun (s : Finset ι) (x : α) ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop s

Tactic:
(hr.tendstoUniformlyOn.comp_cexp ?_).congr ?_

Premises used: TendstoUniformlyOn.congr, TendstoUniformlyOn.comp_cexp, HasSumUniformlyOn.tendstoUniformlyOn
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
r : α → ℂ
hr : HasSumUniformlyOn (fun (i : ι) (x : α) ↦ log (f i x)) r s
refine_1 : BddAbove (α := ℝ) ((fun (x : α) ↦ (r x).re) '' s)
refine_2 :
  ∀ᶠ (n : Finset ι) in atTop, Set.EqOn (cexp ∘ fun (x2 : α) ↦ ∑ i ∈ n, log (f i x2)) (fun (x : α) ↦ ∏ i ∈ n, f i x) s
⊢ TendstoUniformlyOn (fun (s : Finset ι) (x : α) ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop s

Tactic:
refine (hr.tendstoUniformlyOn.comp_cexp ?_).congr ?_

Premises used: TendstoUniformlyOn.congr, TendstoUniformlyOn.comp_cexp, HasSumUniformlyOn.tendstoUniformlyOn
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
r : α → ℂ
hr : HasSumUniformlyOn (fun (i : ι) (x : α) ↦ log (f i x)) r s
⊢ BddAbove (α := ℝ) ((fun (x : α) ↦ (r x).re) '' s)

Tactic:
simpa +contextual [← hr.tsum_eqOn _] using hg

Premises used: HasSumUniformlyOn.tsum_eqOn
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
s_1 : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s_1
hfn : ∀ x ∈ s_1, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s_1)
r : α → ℂ
hr : HasSumUniformlyOn (fun (i : ι) (x : α) ↦ log (f i x)) r s_1
s : Finset ι
i : α
hi : i ∈ s_1
⊢ (cexp ∘ fun (x2 : α) ↦ ∑ i ∈ s, log (f i x2)) i = (fun (x : α) ↦ (∏ i ∈ s, f i x : ℂ)) i

Tactic:
simp [exp_sum, fun y ↦ exp_log (hfn i hi y)]

Premises used: Complex.exp_sum, Complex.exp_log
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
r : α → ℂ
hr : HasSumUniformlyOn (fun (i : ι) (x : α) ↦ log (f i x)) r s
refine_2 :
  ∀ (a : Finset ι),
    Membership.mem (γ := Set (Finset ι))
      {x : Finset ι |
        (fun (n : Finset ι) ↦ Set.EqOn (cexp ∘ fun (x2 : α) ↦ ∑ i ∈ n, log (f i x2)) (fun (x : α) ↦ ∏ i ∈ n, f i x) s)
          x}
      a
refine_2₁ : ∀ (a : Finset ι), Set.EqOn (cexp ∘ fun (x2 : α) ↦ ∑ i ∈ a, log (f i x2)) (fun (x : α) ↦ ∏ i ∈ a, f i x) s
refine_2₂ :
  ∀ (s_1 : Finset ι) ⦃i : α⦄ (hi : i ∈ s),
    (cexp ∘ fun (x2 : α) ↦ ∑ i ∈ s_1, log (f i x2)) i = (fun (x : α) ↦ (∏ i ∈ s_1, f i x : ℂ)) i
⊢ ∀ᶠ (n : Finset ι) in atTop, Set.EqOn (cexp ∘ fun (x2 : α) ↦ ∑ i ∈ n, log (f i x2)) (fun (x : α) ↦ ∏ i ∈ n, f i x) s

Tactic:
filter_upwards with s i hi using by simp [exp_sum, fun y ↦ exp_log (hfn i hi y)]
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
s : Set α
f : ι → α → ℂ
hf : SummableUniformlyOn (α := ℂ) (fun (i : ι) (x : α) ↦ log (f i x)) s
hfn : ∀ x ∈ s, ∀ (i : ι), f i x ≠ 0
hg : BddAbove (α := ℝ) ((fun (x : α) ↦ re (∑' (i : ι), log (f i x))) '' s)
⊢ MultipliableUniformlyOn f s

Tactic:
⟨_, hasProdUniformlyOn_of_clog hf hfn hg⟩

Premises used: Multipliable, Exists.intro, hasProdUniformlyOn_of_clog, MultipliableUniformlyOn
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
inst_3 : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
simp :
  TendstoUniformly.{u_1, u_3, u_2} (β := R) (fun (i : Finset ι) (x : (↑K : Type u_1)) ↦ ∏ i ∈ i, (1 + f i (↑x : α)))
    ((fun (x : α) ↦ ∏' (i : ι), (1 + f i x)) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ K)) atTop
⊢ HasProdUniformlyOn.{u_3, u_1, u_2} (α := R) (fun (i : ι) (x : α) ↦ 1 + f i x) (fun (x : α) ↦ ∏' (i : ι), (1 + f i x))
    K

Tactic:
simp only [hasProdUniformlyOn_iff_tendstoUniformlyOn,
    tendstoUniformlyOn_iff_tendstoUniformly_comp_coe]

Premises used: tendstoUniformlyOn_iff_tendstoUniformly_comp_coe, hasProdUniformlyOn_iff_tendstoUniformlyOn
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
ι : Type u_2
K : Set α
u : ι → ℝ
R : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
inst_3 : TopologicalSpace α
f : ι → α → R
hK : IsCompact K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
pos :
  ∀ (hKe : K = ∅),
    TendstoUniformly.{u_1, u_3, u_2} (β := R) (fun (i : Finset ι) (x : (↑K : Type u_1)) ↦ ∏ i ∈ i, (1 + f i (↑x : α)))
      ((fun (x : α) ↦ ∏' (i : ι), (1 + f i x)) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ K)) atTop
neg :
  ∀ (hKe : ¬K = ∅),
    TendstoUniformly.{u_1, u_3, u_2} (β := R) (fun (i : Finset ι) (x : (↑K : Type u_1)) ↦ ∏ i ∈ i, (1 + f i (↑x : α)))
      ((fun (x : α) ↦ ∏' (i : ι), (1 + f i x)) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ K)) atTop
⊢ TendstoUniformly.{u_1, u_3, u_2} (β := R) (fun (i : Finset ι) (x : (↑K : Type u_1)) ↦ ∏ i ∈ i, (1 + f i (↑x : α)))
    ((fun (x : α) ↦ ∏' (i : ι), (1 + f i x)) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ K)) atTop

Tactic:
by_cases hKe : K = ∅