awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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:
simp [TendstoUniformly, hKe]

Premises used: TendstoUniformly
-- 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
hKe : ¬K = ∅
⊢ CompactSpace.{u_1} (↑K : Type u_1)

Tactic:
haveI hCK : CompactSpace K := isCompact_iff_compactSpace.mp hK
-- 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
hKe : ¬K = ∅
hCK : CompactSpace.{u_1} (↑K : Type u_1)
rwa : K.Nonempty
rwa₁ rwa₂ rwa₃ rwa₄ : K ≠ ∅
⊢ Nonempty.{u_1 + 1} (↑K : Type u_1)

Tactic:
rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty]

Premises used: Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty
-- 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
hKe : ¬K = ∅
hCK : CompactSpace.{u_1} (↑K : Type u_1)
⊢ Nonempty.{u_1 + 1} (↑K : Type u_1)

Tactic:
haveI hne : Nonempty K := by rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty]
-- 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
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 := ⋯ }
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
⊢ ∀ᶠ (i : ι) in cofinite, ‖f' i‖ ≤ u i

Tactic:
simp only [ContinuousMap.norm_le_of_nonempty]

Premises used: ContinuousMap.norm_le_of_nonempty
-- 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
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 : ι
hi : ∀ x ∈ K, ‖f i x‖ ≤ u i
⊢ ∀ (x : (↑K : Type u_1)), Norm.norm.{u_3} (E := R) ((f' i : (a : (↑K : Type u_1)) → R) x : R) ≤ u i

Tactic:
fun x ↦ hi x x.2

Premises used: Set.restrict, Subtype.val, Subtype.property
-- 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
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
h₂ h₃ :
  ∀ (i : ι) (hi : ∀ x ∈ K, ‖f i x‖ ≤ u i) (x : (↑K : Type u_1)),
    Norm.norm.{u_3} (E := R) ((f' i : (a : (↑K : Type u_1)) → R) x : R) ≤ u i
⊢ ∀ᶠ (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:
filter_upwards [h] with i hi using fun x ↦ hi x x.2
-- 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
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

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
-- 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
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
⊢ ∀ᶠ (i : ι) in cofinite, ‖‖f' i‖‖ ≤ u i

Tactic:
simpa using hf'_bd
-- 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
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
⊢ 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))
-- 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
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 ι) (a : (↑K : Type u_1)) ↦ (∏ b ∈ i, (fun (i : ι) ↦ 1 + f' i) b : (a : (↑K : Type u_1)) → R) a)
    (⇑(∏' (b : ι), (1 + f' b)) : (a : (↑K : Type u_1)) → R) (SummationFilter.unconditional ι).filter

Tactic:
ContinuousMap.tendsto_iff_tendstoUniformly.mp hM.hasProd

Premises used: ContinuousMap.tendsto_iff_tendstoUniformly, Multipliable.hasProd, Iff.mp
-- 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
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)
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)
⊢ 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:
convert! ContinuousMap.tendsto_iff_tendstoUniformly.mp hM.hasProd

Premises used: ContinuousMap.tendsto_iff_tendstoUniformly, Multipliable.hasProd, Iff.mp
-- 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
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
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:
simp [f']
-- 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
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
⊢ 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:
funext fun k ↦ ContinuousMap.tprod_apply hM k

Premises used: ContinuousMap.tprod_apply, funext
-- 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
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
⊢ 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:
exact funext fun k ↦ ContinuousMap.tprod_apply hM k

Premises used: ContinuousMap.tprod_apply, funext
-- 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
⊢ MultipliableUniformlyOn.{u_3, u_1, u_2} (α := R) (fun (i : ι) (x : α) ↦ 1 + f i x) K

Tactic:
⟨_, hasProdUniformlyOn_one_add hK hu h hcts⟩

Premises used: Multipliable, Exists.intro, Summable.hasProdUniformlyOn_one_add, MultipliableUniformlyOn
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
K : Set α
R : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
inst_3 : TopologicalSpace α
f : ℕ → α → R
hK : IsCompact K
u : ℕ → ℝ
hu : Summable u
h : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n
hcts : ∀ (n : ℕ), ContinuousOn (f n) K
⊢ HasProdUniformlyOn.{u_3, u_1, 0} (α := R) (fun (n : ℕ) (x : α) ↦ 1 + f n x) (fun (x : α) ↦ ∏' (i : ℕ), (1 + f i x)) K

Tactic:
hasProdUniformlyOn_one_add hK hu (Nat.cofinite_eq_atTop ▸ h) hcts

Premises used: Eq.rec, Summable.hasProdUniformlyOn_one_add, Nat.cofinite_eq_atTop, Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
K : Set α
R : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
inst_3 : TopologicalSpace α
f : ℕ → α → R
hK : IsCompact K
u : ℕ → ℝ
hu : Summable u
h : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n
hcts : ∀ (n : ℕ), ContinuousOn (f n) K
⊢ MultipliableUniformlyOn.{u_3, u_1, 0} (α := R) (fun (n : ℕ) (x : α) ↦ 1 + f n x) K

Tactic:
⟨_, hasProdUniformlyOn_nat_one_add hK hu h hcts⟩

Premises used: Summable.hasProdUniformlyOn_nat_one_add, Multipliable, Exists.intro, 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
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
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
⊢ HasProdLocallyUniformlyOn.{u_3, u_1, u_2} (α := R) (fun (i : ι) (x : α) ↦ 1 + f i x)
    (fun (x : α) ↦ ∏' (i : ι), (1 + f i x)) K

Tactic:
apply hasProdLocallyUniformlyOn_of_forall_compact hK

Premises used: hasProdLocallyUniformlyOn_of_forall_compact
-- 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
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

Tactic:
fun S hS hC ↦ hasProdUniformlyOn_one_add hC hu ?_ fun i ↦ (hcts i).mono hS

Premises used: ContinuousOn.mono, Summable.hasProdUniformlyOn_one_add
-- 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
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
refine : ∀ (S : Set α) (hS : S ⊆ K) (hC : IsCompact S), ∀ᶠ (i : ι) in cofinite, ∀ x ∈ S, ‖f i x‖ ≤ u i
⊢ ∀ 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:
refine fun S hS hC ↦ hasProdUniformlyOn_one_add hC hu ?_ fun i ↦ (hcts i).mono hS

Premises used: ContinuousOn.mono, Summable.hasProdUniformlyOn_one_add
-- 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
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 : ι
hi : ∀ x ∈ K, ‖f i x‖ ≤ u i
a : α
ha : a ∈ S
⊢ ‖f i a‖ ≤ u i

Tactic:
hi a (hS ha)
-- 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
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
h₂ h₃ : ∀ (i : ι) (hi : ∀ x ∈ K, ‖f i x‖ ≤ u i) (a : α) (ha : a ∈ S), ‖f i a‖ ≤ u i
⊢ ∀ᶠ (i : ι) in cofinite, ∀ x ∈ S, ‖f i x‖ ≤ u i

Tactic:
filter_upwards [h] with i hi a ha using hi a (hS ha)
-- 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
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
⊢ MultipliableLocallyUniformlyOn.{u_3, u_1, u_2} (α := R) (fun (i : ι) (x : α) ↦ 1 + f i x) K

Tactic:
⟨_, hasProdLocallyUniformlyOn_one_add hK hu h hcts⟩

Premises used: Summable.hasProdLocallyUniformlyOn_one_add, Exists.intro, MultipliableLocallyUniformlyOn
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
K : Set α
R : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
inst_3 : TopologicalSpace α
inst_4 : LocallyCompactSpace α
f : ℕ → α → R
hK : IsOpen[inst_3] K
u : ℕ → ℝ
hu : Summable u
h : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n
hcts : ∀ (n : ℕ), ContinuousOn (f n) K
⊢ HasProdLocallyUniformlyOn.{u_3, u_1, 0} (α := R) (fun (n : ℕ) (x : α) ↦ 1 + f n x)
    (fun (x : α) ↦ ∏' (i : ℕ), (1 + f i x)) K

Tactic:
hasProdLocallyUniformlyOn_one_add hK hu (Nat.cofinite_eq_atTop ▸ h) hcts

Premises used: Eq.rec, Summable.hasProdLocallyUniformlyOn_one_add, Nat.cofinite_eq_atTop, Eq.symm
-- Module: Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Goal:
α : Type u_1
K : Set α
R : Type u_3
inst : NormedCommRing R
inst_1 : NormOneClass R
inst_2 : CompleteSpace R
inst_3 : TopologicalSpace α
inst_4 : LocallyCompactSpace α
f : ℕ → α → R
hK : IsOpen[inst_3] K
u : ℕ → ℝ
hu : Summable u
h : ∀ᶠ (n : ℕ) in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n
hcts : ∀ (n : ℕ), ContinuousOn (f n) K
⊢ MultipliableLocallyUniformlyOn.{u_3, u_1, 0} (α := R) (fun (n : ℕ) (x : α) ↦ 1 + f n x) K

Tactic:
⟨_, hasProdLocallyUniformlyOn_nat_one_add hK hu h hcts⟩

Premises used: Exists.intro, Summable.hasProdLocallyUniformlyOn_nat_one_add, MultipliableLocallyUniformlyOn
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
⊢ Eq.{u_1 + 1} (α := V) (normalize 0) 0

Tactic:
simp [normalize]

Premises used: NormedSpace.normalize
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
pos : ∀ (hx : x = 0), normalize x = 0 ↔ x = 0
neg : ∀ (hx : ¬x = 0), normalize x = 0 ↔ x = 0
⊢ normalize x = 0 ↔ x = 0

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
hx : x = 0
⊢ normalize x = 0 ↔ x = 0

Tactic:
simp [normalize, hx]

Premises used: NormedSpace.normalize
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
hx : ¬x = 0
⊢ normalize x = 0 ↔ x = 0

Tactic:
simp [normalize, hx]

Premises used: NormedSpace.normalize
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
pos : ∀ (hx : x = 0), ‖x‖ • normalize x = x
neg : ∀ (hx : ¬x = 0), ‖x‖ • normalize x = x
⊢ ‖x‖ • normalize x = x

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
hx : x = 0
⊢ ‖x‖ • normalize x = x

Tactic:
simp [normalize, hx]

Premises used: NormedSpace.normalize
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
hx : ¬x = 0
⊢ ‖x‖ • normalize x = x

Tactic:
simp [normalize, hx]

Premises used: NormedSpace.normalize
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
pos : ∀ (hx : x = 0), ‖normalize x‖ = 1 ↔ x ≠ 0
neg : ∀ (hx : ¬x = 0), ‖normalize x‖ = 1 ↔ x ≠ 0
⊢ ‖normalize x‖ = 1 ↔ x ≠ 0

Tactic:
by_cases hx : x = 0
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
hx : x = 0
⊢ ‖normalize x‖ = 1 ↔ x ≠ 0

Tactic:
simp [normalize, hx, norm_smul]

Premises used: norm_smul, NormedSpace.normalize
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
hx : ¬x = 0
⊢ ‖normalize x‖ = 1 ↔ x ≠ 0

Tactic:
simp [normalize, hx, norm_smul]

Premises used: norm_smul, NormedSpace.normalize
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
h : ‖x‖ = 1
⊢ normalize x = x

Tactic:
simp [normalize, h]

Premises used: NormedSpace.normalize
-- Module: Mathlib.Analysis.Normed.Module.Normalize
Goal:
V : Type u_1
inst : NormedAddCommGroup V
inst_1 : NormedSpace ℝ V
x : V
pos : ∀ (hx : x = 0), normalize (normalize x) = normalize x
neg : ∀ (hx : ¬x = 0), normalize (normalize x) = normalize x
⊢ normalize (normalize x) = normalize x

Tactic:
by_cases hx : x = 0