awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
have refine : Set.EqOn (cexp ∘ fun (x : α) ↦ ∑' (b : ι), log (f b x)) (fun (x : α) ↦ ∏' (i : ι), f i x) s
Tactic: refine H.congr_right (hr.tsum_eqOn.comp_left.symm.trans ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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 (x1 : Finset ι) (x2 : α) ↦ ∏ i ∈ x1, f i x2) (fun (x : α) ↦ ∏' (i : ι), f i x) atTop
    s
have suffices : TendstoUniformlyOn (fun (s : Finset ι) (x : α) ↦ ∏ i ∈ s, f i x) (cexp ∘ r) 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))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
have refine_1 : BddAbove (α := ℝ) ((fun (x : α) ↦ (r x).re) '' s)
Tactic: refine (hr.tendstoUniformlyOn.comp_cexp ?_).congr ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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)
⊢ TendstoUniformlyOn (fun (s : Finset ι) (x : α) ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop s
have 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
Tactic: refine (hr.tendstoUniformlyOn.comp_cexp ?_).congr ?_
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
⊢ ∀ᶠ (n : Finset ι) in atTop, Set.EqOn (cexp ∘ fun (x2 : α) ↦ ∑ i ∈ n, log (f i x2)) (fun (x : α) ↦ ∏ i ∈ n, f i x) s
have 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
Tactic: filter_upwards with s i hi using by simp [exp_sum, fun y ↦ exp_log (hfn i hi y)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
⊢ ∀ᶠ (n : Finset ι) in atTop, Set.EqOn (cexp ∘ fun (x2 : α) ↦ ∑ i ∈ n, log (f i x2)) (fun (x : α) ↦ ∏ i ∈ n, f i x) s
have refine_2₁ : ∀ (a : Finset ι), Set.EqOn (cexp ∘ fun (x2 : α) ↦ ∑ i ∈ a, log (f i x2)) (fun (x : α) ↦ ∏ i ∈ a, f i x) s
Tactic: filter_upwards with s i hi using by simp [exp_sum, fun y ↦ exp_log (hfn i hi y)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
⊢ ∀ᶠ (n : Finset ι) in atTop, Set.EqOn (cexp ∘ fun (x2 : α) ↦ ∑ i ∈ n, log (f i x2)) (fun (x : α) ↦ ∏ i ∈ n, f i x) s
have 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
Tactic: filter_upwards with s i hi using by simp [exp_sum, fun y ↦ exp_log (hfn i hi y)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
⊢ HasProdUniformlyOn.{u_3, u_1, u_2} (α := R) (fun (i : ι) (x : α) ↦ 1 + f i x) (fun (x : α) ↦ ∏' (i : ι), (1 + f i x))
    K
have 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
Tactic: simp only [hasProdUniformlyOn_iff_tendstoUniformlyOn,
    tendstoUniformlyOn_iff_tendstoUniformly_comp_coe]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
⊢ 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
have 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
Tactic: by_cases hKe : K = ∅
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
⊢ 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
have 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
Tactic: by_cases hKe : K = ∅
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (hypothesis)
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
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
have hCK : CompactSpace.{u_1} (↑K : Type u_1)
Tactic: haveI hCK : CompactSpace K := isCompact_iff_compactSpace.mp hK
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
hKe : ¬K = ∅
hCK : CompactSpace.{u_1} (↑K : Type u_1)
⊢ Nonempty.{u_1 + 1} (↑K : Type u_1)
have rwa : K.Nonempty
Tactic: rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
hKe : ¬K = ∅
hCK : CompactSpace.{u_1} (↑K : Type u_1)
rwa : K.Nonempty
⊢ Nonempty.{u_1 + 1} (↑K : Type u_1)
have rwa₁ : K ≠ ∅
Tactic: rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (hypothesis)
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
hKe : ¬K = ∅
hCK : CompactSpace.{u_1} (↑K : Type u_1)
⊢ 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
have hne : Nonempty.{u_1 + 1} (↑K : Type u_1)
Tactic: haveI hne : Nonempty K := by rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
hKe : ¬K = ∅
hCK : CompactSpace.{u_1} (↑K : Type u_1)
hne : Nonempty.{u_1 + 1} (↑K : Type u_1)
f' : (i : ι) → ContinuousMap.{u_1, u_3} (↑K : Type u_1) R :=
  fun (i : ι) ↦ { toFun := K.restrict (π := fun (a : α) ↦ R) (f i), continuous_toFun := ⋯ }
⊢ ∀ᶠ (i : ι) in cofinite, ‖f' i‖ ≤ u i
have simp : ∀ᶠ (i : ι) in cofinite,
  ∀ (x : (↑K : Type u_1)), Norm.norm.{u_3} (E := R) ((f' i : (a : (↑K : Type u_1)) → R) x : R) ≤ u i
Tactic: simp only [ContinuousMap.norm_le_of_nonempty]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
hKe : ¬K = ∅
hCK : CompactSpace.{u_1} (↑K : Type u_1)
hne : Nonempty.{u_1 + 1} (↑K : Type u_1)
f' : (i : ι) → ContinuousMap.{u_1, u_3} (↑K : Type u_1) R :=
  fun (i : ι) ↦ { toFun := K.restrict (π := fun (a : α) ↦ R) (f i), continuous_toFun := ⋯ }
⊢ ∀ᶠ (i : ι) in cofinite,
    ∀ (x : (↑K : Type u_1)), Norm.norm.{u_3} (E := R) ((f' i : (a : (↑K : Type u_1)) → R) x : R) ≤ u i
have 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 : ι |
            (fun (i : ι) ↦
                ∀ (x : (↑K : Type u_1)), Norm.norm.{u_3} (E := R) ((f' i : (a : (↑K : Type u_1)) → R) x : R) ≤ u i)
              x}
          x}
    a
Tactic: filter_upwards [h] with i hi using fun x ↦ hi x x.2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
hKe : ¬K = ∅
hCK : CompactSpace.{u_1} (↑K : Type u_1)
hne : Nonempty.{u_1 + 1} (↑K : Type u_1)
f' : (i : ι) → ContinuousMap.{u_1, u_3} (↑K : Type u_1) R :=
  fun (i : ι) ↦ { toFun := K.restrict (π := fun (a : α) ↦ R) (f i), continuous_toFun := ⋯ }
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 : ι |
              (fun (i : ι) ↦
                  ∀ (x : (↑K : Type u_1)), Norm.norm.{u_3} (E := R) ((f' i : (a : (↑K : Type u_1)) → R) x : R) ≤ u i)
                x}
            x}
      a
⊢ ∀ᶠ (i : ι) in cofinite,
    ∀ (x : (↑K : Type u_1)), Norm.norm.{u_3} (E := R) ((f' i : (a : (↑K : Type u_1)) → R) x : R) ≤ u i
have h₂ : ∀ (a : ι),
  (∀ x ∈ K, ‖f a x‖ ≤ u a) →
    ∀ (x : (↑K : Type u_1)), Norm.norm.{u_3} (E := R) ((f' a : (a : (↑K : Type u_1)) → R) x : R) ≤ u a
Tactic: filter_upwards [h] with i hi using fun x ↦ hi x x.2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (hypothesis)
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
hKe : ¬K = ∅
hCK : CompactSpace.{u_1} (↑K : Type u_1)
hne : Nonempty.{u_1 + 1} (↑K : Type u_1)
f' : (i : ι) → ContinuousMap.{u_1, u_3} (↑K : Type u_1) R :=
  fun (i : ι) ↦ { toFun := K.restrict (π := fun (a : α) ↦ R) (f i), continuous_toFun := ⋯ }
⊢ 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
have hf'_bd : ∀ᶠ (i : ι) in cofinite, ‖f' i‖ ≤ u i
Tactic: have hf'_bd : ∀ᶠ i in cofinite, ‖f' i‖ ≤ u i := by
      simp only [ContinuousMap.norm_le_of_nonempty]
      filter_upwards [h] with i hi using fun x ↦ hi x x.2
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (hypothesis)
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
hKe : ¬K = ∅
hCK : CompactSpace.{u_1} (↑K : Type u_1)
hne : Nonempty.{u_1 + 1} (↑K : Type u_1)
f' : (i : ι) → ContinuousMap.{u_1, u_3} (↑K : Type u_1) R :=
  fun (i : ι) ↦ { toFun := K.restrict (π := fun (a : α) ↦ R) (f i), continuous_toFun := ⋯ }
hf'_bd : ∀ᶠ (i : ι) in cofinite, ‖f' i‖ ≤ u i
⊢ 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
have hM : Multipliable (α := ContinuousMap.{u_1, u_3} (↑K : Type u_1) R) fun (i : ι) ↦ 1 + f' i
Tactic: have hM : Multipliable fun i ↦ 1 + f' i :=
      multipliable_one_add_of_summable (hu.of_norm_bounded_eventually (by simpa using hf'_bd))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
hKe : ¬K = ∅
hCK : CompactSpace.{u_1} (↑K : Type u_1)
hne : Nonempty.{u_1 + 1} (↑K : Type u_1)
f' : (i : ι) → ContinuousMap.{u_1, u_3} (↑K : Type u_1) R :=
  fun (i : ι) ↦ { toFun := K.restrict (π := fun (a : α) ↦ R) (f i), continuous_toFun := ⋯ }
hf'_bd : ∀ᶠ (i : ι) in cofinite, ‖f' i‖ ≤ u i
hM : Multipliable (α := ContinuousMap.{u_1, u_3} (↑K : Type u_1) R) fun (i : ι) ↦ 1 + f' i
⊢ 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
have h₁ : ∀ (x : Finset ι) (x_1 : (↑K : Type u_1)),
  Eq.{u_3 + 1} (α := R) (∏ i ∈ x, (1 + f i (↑x_1 : α)) : R)
    ((∏ b ∈ x, (fun (i : ι) ↦ 1 + f' i) b : (a : (↑K : Type u_1)) → R) x_1 : R)
Tactic: convert! ContinuousMap.tendsto_iff_tendstoUniformly.mp hM.hasProd
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
hKe : ¬K = ∅
hCK : CompactSpace.{u_1} (↑K : Type u_1)
hne : Nonempty.{u_1 + 1} (↑K : Type u_1)
f' : (i : ι) → ContinuousMap.{u_1, u_3} (↑K : Type u_1) R :=
  fun (i : ι) ↦ { toFun := K.restrict (π := fun (a : α) ↦ R) (f i), continuous_toFun := ⋯ }
hf'_bd : ∀ᶠ (i : ι) in cofinite, ‖f' i‖ ≤ u i
hM : Multipliable (α := ContinuousMap.{u_1, u_3} (↑K : Type u_1) R) fun (i : ι) ↦ 1 + f' i
h₁ :
  ∀ (x : Finset ι) (x_1 : (↑K : Type u_1)),
    Eq.{u_3 + 1} (α := R) (∏ i ∈ x, (1 + f i (↑x_1 : α)) : R)
      ((∏ b ∈ x, (fun (i : ι) ↦ 1 + f' i) b : (a : (↑K : Type u_1)) → R) x_1 : R)
⊢ 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
have h₂ : Eq (α := (↑K : Type u_1) → R) ((fun (x : α) ↦ ∏' (i : ι), (1 + f i x)) ∘ Subtype.val (p := fun (x : α) ↦ x ∈ K))
  (⇑(∏' (b : ι), (1 + f' b)) : (a : (↑K : Type u_1)) → R)
Tactic: convert! ContinuousMap.tendsto_iff_tendstoUniformly.mp hM.hasProd
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
inst_4 : LocallyCompactSpace α
hK : IsOpen[inst_3] K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
⊢ HasProdLocallyUniformlyOn.{u_3, u_1, u_2} (α := R) (fun (i : ι) (x : α) ↦ 1 + f i x)
    (fun (x : α) ↦ ∏' (i : ι), (1 + f i x)) K
have apply : ∀ K_1 ⊆ K,
  IsCompact K_1 →
    HasProdUniformlyOn.{u_3, u_1, u_2} (α := R) (fun (i : ι) (x : α) ↦ 1 + f i x)
      (fun (x : α) ↦ ∏' (i : ι), (1 + f i x)) K_1
Tactic: apply hasProdLocallyUniformlyOn_of_forall_compact hK
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
inst_4 : LocallyCompactSpace α
hK : IsOpen[inst_3] K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
⊢ ∀ K_1 ⊆ K,
    IsCompact K_1 →
      HasProdUniformlyOn.{u_3, u_1, u_2} (α := R) (fun (i : ι) (x : α) ↦ 1 + f i x)
        (fun (x : α) ↦ ∏' (i : ι), (1 + f i x)) K_1
have refine : ∀ (S : Set α) (hS : S ⊆ K) (hC : IsCompact S), ∀ᶠ (i : ι) in cofinite, ∀ x ∈ S, ‖f i x‖ ≤ u i
Tactic: refine fun S hS hC ↦ hasProdUniformlyOn_one_add hC hu ?_ fun i ↦ (hcts i).mono hS
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
inst_4 : LocallyCompactSpace α
hK : IsOpen[inst_3] K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
S : Set α
hS : S ⊆ K
hC : IsCompact S
⊢ ∀ᶠ (i : ι) in cofinite, ∀ x ∈ S, ‖f i x‖ ≤ u i
have 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 : ι | (fun (i : ι) ↦ ∀ x ∈ S, ‖f i x‖ ≤ u i) x} x}
    a
Tactic: filter_upwards [h] with i hi a ha using hi a (hS ha)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn (goal)
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
inst_4 : LocallyCompactSpace α
hK : IsOpen[inst_3] K
hu : Summable u
h : ∀ᶠ (i : ι) in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i
hcts : ∀ (i : ι), ContinuousOn (f i) K
S : Set α
hS : S ⊆ K
hC : IsCompact S
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 : ι | (fun (i : ι) ↦ ∀ x ∈ S, ‖f i x‖ ≤ u i) x} x}
      a
⊢ ∀ᶠ (i : ι) in cofinite, ∀ x ∈ S, ‖f i x‖ ≤ u i
have h₂ : ∀ (a : ι), (∀ x ∈ K, ‖f a x‖ ≤ u a) → ∀ x ∈ S, ‖f a x‖ ≤ u a
Tactic: filter_upwards [h] with i hi a ha using hi a (hS ha)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Normalize (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
⊢ normalize x = 0 ↔ x = 0
have pos : ∀ (hx : x = 0), normalize x = 0 ↔ x = 0
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Normalize (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
pos : ∀ (hx : x = 0), normalize x = 0 ↔ x = 0
⊢ normalize x = 0 ↔ x = 0
have neg : ∀ (hx : ¬x = 0), normalize x = 0 ↔ x = 0
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Normalize (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
⊢ ‖x‖ • normalize x = x
have pos : ∀ (hx : x = 0), ‖x‖ • normalize x = x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Normalize (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
pos : ∀ (hx : x = 0), ‖x‖ • normalize x = x
⊢ ‖x‖ • normalize x = x
have neg : ∀ (hx : ¬x = 0), ‖x‖ • normalize x = x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Module.Normalize (goal)
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
⊢ ‖normalize x‖ = 1 ↔ x ≠ 0
have pos : ∀ (hx : x = 0), ‖normalize x‖ = 1 ↔ x ≠ 0
Tactic: by_cases hx : x = 0