awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
f : C(α, E)
⊢ ‖f‖ₑ = ⨆ (x : α), enorm.{u_3} (E := E) ((f : (a : α) → E) x : E)

Tactic:
(mkOfCompact f).enorm_eq_iSup_enorm

Premises used: setOf, BoundedContinuousFunction.mkOfCompact, BoundedContinuousFunction.enorm_eq_iSup_enorm
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
f : C(α, E)
X : Type u_4
inst_4 : TopologicalSpace X
K : TopologicalSpace.Compacts X
⊢ CompactSpace.{u_4} (↑(↑K : Set X) : Type u_4)

Tactic:
TopologicalSpace.Compacts.instCompactSpaceSubtypeMem ..

Premises used: TopologicalSpace.Compacts.instCompactSpaceSubtypeMem
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
E : Type u_3
inst : SeminormedAddCommGroup E
X : Type u_4
inst_1 : TopologicalSpace X
f : C(X, E)
K L : TopologicalSpace.Compacts X
hKL : K ≤ L
⊢ ‖restrict (↑K : Set X) f‖ ≤ ‖restrict (↑L : Set X) f‖

Tactic:
(norm_le _ (norm_nonneg _)).mpr fun x => norm_coe_le_norm (f.restrict L) <| Set.inclusion hKL x

Premises used: Iff.mpr, ContinuousMap.norm_le, norm_nonneg
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
𝕜 : Type u_4
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : IsBoundedSMul 𝕜 E
c : 𝕜
f : C(α, E)
h :
  ∀ (x : α),
    Eq.{u_3 + 1} (α := E)
      ((Equiv.toFun (AddEquiv.toEquiv (addEquivBoundedOfCompact α E : C(α, E) ≃+ (α →ᵇ E))) (c • f) : (a : α) → E) x :
        E)
      ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
              (Equiv.toFun (AddEquiv.toEquiv (addEquivBoundedOfCompact α E : C(α, E) ≃+ (α →ᵇ E))) f) :
            (a : α) → E)
          x :
        E)
⊢ Equiv.toFun (AddEquiv.toEquiv (addEquivBoundedOfCompact α E : C(α, E) ≃+ (α →ᵇ E))) (c • f) =
    HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (Equiv.toFun (AddEquiv.toEquiv (addEquivBoundedOfCompact α E : C(α, E) ≃+ (α →ᵇ E))) f)

Tactic:
ext
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
𝕜 : Type u_4
inst_4 : NormedRing 𝕜
inst_5 : Module 𝕜 E
inst_6 : IsBoundedSMul 𝕜 E
c : 𝕜
f : C(α, E)
x : α
h h₁ h₂ h₃ :
  Eq.{u_3 + 1} (α := E)
    ((Equiv.toFun (AddEquiv.toEquiv (addEquivBoundedOfCompact α E : C(α, E) ≃+ (α →ᵇ E))) (c • f) : (a : α) → E) x : E)
    ((id c • Equiv.toFun (AddEquiv.toEquiv (addEquivBoundedOfCompact α E : C(α, E) ≃+ (α →ᵇ E))) f : (a : α) → E) x : E)
⊢ Eq.{u_3 + 1} (α := E)
    ((Equiv.toFun (AddEquiv.toEquiv (addEquivBoundedOfCompact α E : C(α, E) ≃+ (α →ᵇ E))) (c • f) : (a : α) → E) x : E)
    ((HSMul.hSMul (α := 𝕜) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
            (Equiv.toFun (AddEquiv.toEquiv (addEquivBoundedOfCompact α E : C(α, E) ≃+ (α →ᵇ E))) f) :
          (a : α) → E)
        x :
      E)

Tactic:
norm_cast
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
𝕜 : Type u_4
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
f : α →ᵇ E
⊢ (LinearIsometryEquiv.symm (linearIsometryBoundedOfCompact α E 𝕜) : (a : α →ᵇ E) → C(α, E)) f = f.toContinuousMap

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
𝕜 : Type u_4
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
f : C(α, E)
a : α
⊢ Eq.{u_3 + 1} (α := E)
    ((((linearIsometryBoundedOfCompact α E 𝕜 : (a : C(α, E)) → α →ᵇ E) f : α →ᵇ E) : (a : α) → E) a : E)
    ((f : (a : α) → E) a : E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
𝕜 : Type u_4
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
⊢ Eq (α := C(α, E) ≃ᵢ (α →ᵇ E)) (LinearIsometryEquiv.toIsometryEquiv (linearIsometryBoundedOfCompact α E 𝕜))
    (isometryEquivBoundedOfCompact α E)

Tactic:
rfl

Premises used: ContinuousMap.equivBoundedOfCompact, BoundedContinuousFunction.mkOfCompact, LinearIsometryEquiv.toIsometryEquiv, LinearEquiv.toEquiv, ContinuousMap.isometryEquivBoundedOfCompact, rfl
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
𝕜 : Type u_4
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
⊢ Eq (α := C(α, E) ≃+ (α →ᵇ E))
    ((↑(LinearIsometryEquiv.toLinearEquiv (E := C(α, E)) (linearIsometryBoundedOfCompact α E 𝕜)) :
        C(α, E) ≃+ (α →ᵇ E)) :
      C(α, E) ≃+ (α →ᵇ E))
    (addEquivBoundedOfCompact α E : C(α, E) ≃+ (α →ᵇ E))

Tactic:
rfl

Premises used: ContinuousMap.addEquivBoundedOfCompact, BoundedContinuousFunction.mkOfCompact, AddEquivClass.toAddEquiv, Equiv.symm, EquivLike.toEquiv, rfl, AddEquiv.symm
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : SeminormedAddCommGroup E
𝕜 : Type u_4
inst_3 : NormedRing 𝕜
inst_4 : Module 𝕜 E
inst_5 : IsBoundedSMul 𝕜 E
⊢ Eq (α := C(α, E) ≃ (α →ᵇ E))
    (LinearEquiv.toEquiv (modM := module) (modM₂ := instModule)
      (LinearIsometryEquiv.toLinearEquiv (E := C(α, E)) (linearIsometryBoundedOfCompact α E 𝕜)))
    (equivBoundedOfCompact α E)

Tactic:
rfl

Premises used: ContinuousMap.equivBoundedOfCompact, BoundedContinuousFunction.mkOfCompact, LinearEquiv.toEquiv, rfl
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
β : Type u_5
inst_2 : SeminormedAddCommGroup β
inst_3 : SeminormedRing R
inst_4 : Module R β
inst_5 : NormSMulClass R β
f : C(α, R)
b : β
⊢ ‖HSMul.hSMul (β := C(α, β)) f (const α b)‖₊ = ‖f‖₊ * ‖b‖₊

Tactic:
simp only [nnnorm_eq_iSup_nnnorm, smul_apply', const_apply, nnnorm_smul, iSup_mul]

Premises used: nnnorm_smul, ContinuousMap.nnnorm_eq_iSup_nnnorm, ContinuousMap.smul_apply', ContinuousMap.const_apply, NNReal.iSup_mul
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
β : Type u_5
inst_2 : SeminormedAddCommGroup β
inst_3 : SeminormedRing R
inst_4 : Module R β
inst_5 : NormSMulClass R β
f : C(α, R)
b : β
⊢ ‖HSMul.hSMul (β := C(α, β)) f (const α b)‖ = ‖f‖ * ‖b‖

Tactic:
simp only [← coe_nnnorm, NNReal.coe_mul, nnnorm_smul_const]

Premises used: ContinuousMap.nnnorm_smul_const, coe_nnnorm, NNReal.coe_mul
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
f g : C(α, R)
h : f * g = 0
h₁ : ∀ (x : α), Eq.{u_4 + 1} (α := R) ((mkOfCompact f * mkOfCompact g : (a : α) → R) x : R) ((0 : (a : α) → R) x : R)
⊢ mkOfCompact f * mkOfCompact g = 0

Tactic:
ext x
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
f g : C(α, R)
h : f * g = 0
x : α
⊢ Eq.{u_4 + 1} (α := R) ((mkOfCompact f * mkOfCompact g : (a : α) → R) x : R) ((0 : (a : α) → R) x : R)

Tactic:
simpa using congr($h x)
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
f g : C(α, R)
h : f * g = 0
⊢ mkOfCompact f * mkOfCompact g = 0

Tactic:
replace h : mkOfCompact f * mkOfCompact g = 0 := by ext x; simpa using congr($h x)
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
f g : C(α, R)
h : mkOfCompact f * mkOfCompact g = 0
⊢ ‖f + g‖ = max ‖f‖ ‖g‖

Tactic:
simpa using BoundedContinuousFunction.norm_add_eq_max h

Premises used: BoundedContinuousFunction.norm_add_eq_max
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
f g : C(α, R)
h : f * g = 0
⊢ ‖f + g‖₊ = max ‖f‖₊ ‖g‖₊

Tactic:
NNReal.eq <| norm_add_eq_max h

Premises used: ContinuousMap.norm_add_eq_max, NNReal.eq
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
f g : C(α, R)
h : f * g = 0
⊢ f * -g = 0

Tactic:
simpa
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
f g : C(α, R)
h : f * g = 0
⊢ ‖f - g‖ = max ‖f‖ ‖g‖

Tactic:
simpa [sub_eq_add_neg] using norm_add_eq_max (f := f) (g := -g) (by simpa)

Premises used: ContinuousMap.norm_add_eq_max, sub_eq_add_neg
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
f g : C(α, R)
h : f * g = 0
⊢ ‖f - g‖₊ = max ‖f‖₊ ‖g‖₊

Tactic:
NNReal.eq <| norm_sub_eq_max h

Premises used: NNReal.eq, ContinuousMap.norm_sub_eq_max
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
ι : Type u_5
f : ι → C(α, R)
h : Pairwise ((fun (x1 x2 : C(α, R)) ↦ x1 * x2 = 0) on f)
⊢ NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊

Tactic:
simp
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
ι : Type u_5
f : ι → C(α, R)
h : Pairwise ((fun (x1 x2 : C(α, R)) ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
this : f j * ∑ i ∈ s, f i = 0
⊢ NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊

Tactic:
simpa [hj, ← ih] using nnnorm_add_eq_max this

Premises used: ContinuousMap.nnnorm_add_eq_max
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
ι : Type u_5
f : ι → C(α, R)
h : Pairwise ((fun (x1 x2 : C(α, R)) ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
insert : f j * ∑ i ∈ s, f i = 0
⊢ NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ Insert.insert j s, f i) = (Insert.insert j s).sup fun (x : ι) ↦ ‖f x‖₊

Tactic:
suffices f j * ∑ i ∈ s, f i = 0 by simpa [hj, ← ih] using nnnorm_add_eq_max this
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
ι : Type u_5
f : ι → C(α, R)
h : Pairwise ((fun (x1 x2 : C(α, R)) ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
i : ι
hi : i ∈ s
⊢ j ≠ i

Tactic:
grind
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
ι : Type u_5
f : ι → C(α, R)
h : Pairwise ((fun (x1 x2 : C(α, R)) ↦ x1 * x2 = 0) on f)
j : ι
s : Finset ι
hj : j ∉ s
ih : NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
⊢ f j * ∑ i ∈ s, f i = 0

Tactic:
simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h (by grind)

Premises used: Finset.mul_sum, Finset.sum_eq_zero
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
ι : Type u_5
f : ι → C(α, R)
s : Finset ι
h : Pairwise ((fun (x1 x2 : C(α, R)) ↦ x1 * x2 = 0) on f)
empty : NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
insert :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s) (ih : NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊),
    NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ Insert.insert j s, f i) = (Insert.insert j s).sup fun (x : ι) ↦ ‖f x‖₊
⊢ NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by simpa [hj, ← ih] using nnnorm_add_eq_max this
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h (by grind)

Premises used: Finset.mul_sum, Finset.sum_eq_zero, Insert.insert
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : CompactSpace α
R : Type u_4
inst_2 : NonUnitalSeminormedRing R
inst_3 : IsCancelMulZero R
ι : Type u_5
f : ι → C(α, R)
s : Finset ι
h : Pairwise ((fun (x1 x2 : C(α, R)) ↦ x1 * x2 = 0) on f)
empty : NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ ∅, f i) = Finset.sup ∅ fun (x : ι) ↦ ‖f x‖₊
insert :
  ∀ (j : ι) (s : Finset ι) (hj : j ∉ s) (ih : NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊),
    NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ Insert.insert j s, f i) = (Insert.insert j s).sup fun (x : ι) ↦ ‖f x‖₊
⊢ NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert j s hj ih =>
    suffices f j * ∑ i ∈ s, f i = 0 by simpa [hj, ← ih] using nnnorm_add_eq_max this
    simpa [Finset.mul_sum] using Finset.sum_eq_zero fun i hi ↦ h (by grind)

Premises used: Finset.mul_sum, Finset.sum_eq_zero, Insert.insert
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f : C(α, β)
ε : ℝ
h : 0 < ε
⊢ ∃ δ > 0, ∀ {x y : α}, dist x y < δ → dist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((f : (a : α) → β) y : β) < ε

Tactic:
Metric.uniformContinuous_iff.mp (CompactSpace.uniformContinuous_of_continuous f.continuous) ε h

Premises used: ContinuousMap.continuous, CompactSpace.uniformContinuous_of_continuous, Iff.mp, Metric.uniformContinuous_iff
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f : C(α, β)
ε : ℝ
h : 0 < ε
⊢ 0 < f.modulus ε h

Tactic:
(Classical.choose_spec (uniform_continuity f ε h)).1

Premises used: ContinuousMap.modulus, Classical.choose_spec, And.left, ContinuousMap.uniform_continuity
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : PseudoMetricSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f : C(α, β)
ε : ℝ
h : 0 < ε
a b : α
w : dist a b < f.modulus ε h
⊢ dist.{u_2} (α := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) < ε

Tactic:
(Classical.choose_spec (uniform_continuity f ε h)).2 w

Premises used: Classical.choose_spec, And.right, ContinuousMap.uniform_continuity
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable (α := ℝ) fun (i : ι) ↦ ‖restrict (↑K : Set X) (F i)‖
⊢ Summable F

Tactic:
(ContinuousMap.exists_tendsto_compactOpen_iff_forall _).2 fun K hK => ?_

Premises used: Iff.mpr, HasSum, ContinuousMap.exists_tendsto_compactOpen_iff_forall, Summable
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable (α := ℝ) fun (i : ι) ↦ ‖restrict (↑K : Set X) (F i)‖
refine :
  ∀ (K : Set X) (hK : IsCompact K),
    ∃ (f : ContinuousMap.{u_1, u_2} (↑K : Type u_1) E),
      Filter.Tendsto (fun (i : Finset ι) ↦ restrict K (∑ b ∈ i, F b)) (SummationFilter.unconditional ι).filter (nhds f)
⊢ Summable F

Tactic:
refine (ContinuousMap.exists_tendsto_compactOpen_iff_forall _).2 fun K hK => ?_

Premises used: Iff.mpr, ContinuousMap.exists_tendsto_compactOpen_iff_forall
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable (α := ℝ) fun (i : ι) ↦ ‖restrict (↑K : Set X) (F i)‖
K : Set X
hK : IsCompact K
⊢ IsCompact K

Tactic:
hK
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable (α := ℝ) fun (i : ι) ↦ ‖restrict (↑K : Set X) (F i)‖
K : Set X
hK : IsCompact K
lift :
  ∀ (K : Compacts X),
    ∃ (f : ContinuousMap.{u_1, u_2} (↑(↑K : Set X) : Type u_1) E),
      Filter.Tendsto (fun (i : Finset ι) ↦ restrict (↑K : Set X) (∑ b ∈ i, F b))
        (SummationFilter.unconditional ι).filter (nhds f)
⊢ ∃ (f : ContinuousMap.{u_1, u_2} (↑K : Type u_1) E),
    Filter.Tendsto (fun (i : Finset ι) ↦ restrict K (∑ b ∈ i, F b)) (SummationFilter.unconditional ι).filter (nhds f)

Tactic:
lift K to Compacts X using hK

Premises used: TopologicalSpace.Compacts
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable (α := ℝ) fun (i : ι) ↦ ‖restrict (↑K : Set X) (F i)‖
K : Compacts X
s : Finset ι
h :
  ∀ (x : (↑(↑K : Set X) : Type u_1)),
    Eq.{u_2 + 1} (α := E) ((restrict (↑K : Set X) (∑ i ∈ s, F i) : (a : (↑(↑K : Set X) : Type u_1)) → E) x : E)
      ((∑ i ∈ s, restrict (↑K : Set X) (F i) : (a : (↑(↑K : Set X) : Type u_1)) → E) x : E)
⊢ Eq (α := ContinuousMap.{u_1, u_2} (↑(↑K : Set X) : Type u_1) E) (restrict (↑K : Set X) (∑ i ∈ s, F i))
    (∑ i ∈ s, restrict (↑K : Set X) (F i))

Tactic:
ext1 x
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable (α := ℝ) fun (i : ι) ↦ ‖restrict (↑K : Set X) (F i)‖
K : Compacts X
s : Finset ι
x : (↑(↑K : Set X) : Type u_1)
⊢ Eq.{u_2 + 1} (α := E) ((restrict (↑K : Set X) (∑ i ∈ s, F i) : (a : (↑(↑K : Set X) : Type u_1)) → E) x : E)
    ((∑ i ∈ s, restrict (↑K : Set X) (F i) : (a : (↑(↑K : Set X) : Type u_1)) → E) x : E)

Tactic:
simp [-SetLike.coe_sort_coe]

Premises used: SetLike.coe_sort_coe
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable (α := ℝ) fun (i : ι) ↦ ‖restrict (↑K : Set X) (F i)‖
K : Compacts X
⊢ ∀ (s : Finset ι),
    Eq (α := ContinuousMap.{u_1, u_2} (↑(↑K : Set X) : Type u_1) E) (restrict (↑K : Set X) (∑ i ∈ s, F i))
      (∑ i ∈ s, restrict (↑K : Set X) (F i))

Tactic:
have A : ∀ s : Finset ι, restrict K (∑ i ∈ s, F i) = ∑ i ∈ s, restrict K (F i) := by
    intro s
    ext1 x
    -- TODO: there is a non-confluence problem in the lemmas here,
    -- and `SetLike.coe_sort_coe` prevents `restrict_apply` from being used.
    simp [-SetLike.coe_sort_coe]
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable (α := ℝ) fun (i : ι) ↦ ‖restrict (↑K : Set X) (F i)‖
K : Compacts X
A :
  ∀ (s : Finset ι),
    Eq (α := ContinuousMap.{u_1, u_2} (↑(↑K : Set X) : Type u_1) E) (restrict (↑K : Set X) (∑ i ∈ s, F i))
      (∑ i ∈ s, restrict (↑K : Set X) (F i))
⊢ ∃ (f : ContinuousMap.{u_1, u_2} (↑(↑K : Set X) : Type u_1) E),
    Filter.Tendsto (fun (i : Finset ι) ↦ restrict (↑K : Set X) (∑ b ∈ i, F b)) (SummationFilter.unconditional ι).filter
      (nhds f)

Tactic:
simpa only [HasSum, A] using (hF K).of_norm

Premises used: Summable.of_norm, HasSum, SummationFilter.unconditional
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : LocallyCompactSpace X
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : CompleteSpace E
ι : Type u_3
F : ι → C(X, E)
hF : ∀ (K : Compacts X), Summable (α := ℝ) fun (i : ι) ↦ ‖restrict (↑K : Set X) (F i)‖
refine :
  ∀ (K : Set X) (hK : IsCompact K),
    ∃ (f : ContinuousMap.{u_1, u_2} (↑K : Type u_1) E),
      Filter.Tendsto (fun (i : Finset ι) ↦ restrict K (∑ b ∈ i, F b)) (SummationFilter.unconditional ι).filter (nhds f)
refine₁ :
  ∀ (K : Compacts X),
    ∃ (f : ContinuousMap.{u_1, u_2} (↑(↑K : Set X) : Type u_1) E),
      Filter.Tendsto (fun (i : Finset ι) ↦ restrict (↑K : Set X) (∑ b ∈ i, F b))
        (SummationFilter.unconditional ι).filter (nhds f)
refine₂ :
  ∀ (K : Compacts X)
    (A :
      ∀ (s : Finset ι),
        Eq (α := ContinuousMap.{u_1, u_2} (↑(↑K : Set X) : Type u_1) E) (restrict (↑K : Set X) (∑ i ∈ s, F i))
          (∑ i ∈ s, restrict (↑K : Set X) (F i))),
    ∃ (f : ContinuousMap.{u_1, u_2} (↑(↑K : Set X) : Type u_1) E),
      Filter.Tendsto (fun (i : Finset ι) ↦ restrict (↑K : Set X) (∑ b ∈ i, F b))
        (SummationFilter.unconditional ι).filter (nhds f)
⊢ Summable F

Tactic:
classical
  refine (ContinuousMap.exists_tendsto_compactOpen_iff_forall _).2 fun K hK => ?_
  lift K to Compacts X using hK
  have A : ∀ s : Finset ι, restrict K (∑ i ∈ s, F i) = ∑ i ∈ s, restrict K (F i) := by
    intro s
    ext1 x
    -- TODO: there is a non-confluence problem in the lemmas here,
    -- and `SetLike.coe_sort_coe` prevents `restrict_apply` from being used.
    simp [-SetLike.coe_sort_coe]
  simpa only [HasSum, A] using (hF K).of_norm

Premises used: Iff.mpr, HasSum, ContinuousMap.exists_tendsto_compactOpen_iff_forall, SummationFilter.unconditional, TopologicalSpace.Compacts
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : StarAddMonoid β
inst_3 : NormedStarGroup β
inst_4 : CompactSpace α
f : C(α, β)
⊢ mkOfCompact (star f) = star (mkOfCompact f)

Tactic:
rfl

Premises used: BoundedContinuousFunction.comp, ContinuousMap.comp, BoundedContinuousFunction.mkOfCompact, rfl
-- Module: Mathlib.Topology.ContinuousMap.Compact
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : SeminormedAddCommGroup β
inst_2 : StarAddMonoid β
inst_3 : NormedStarGroup β
inst_4 : CompactSpace α
f : C(α, β)
rw : ‖mkOfCompact (star f)‖ ≤ ‖f‖
rw₁ : ‖star (mkOfCompact f)‖ ≤ ‖f‖
rw₂ : ‖mkOfCompact f‖ ≤ ‖f‖
rw₃ rw₄ : ‖f‖ ≤ ‖f‖
⊢ ‖star f‖ ≤ ‖f‖

Tactic:
rw [← BoundedContinuousFunction.norm_mkOfCompact, BoundedContinuousFunction.mkOfCompact_star,
      norm_star, BoundedContinuousFunction.norm_mkOfCompact]

Premises used: norm_star, BoundedContinuousFunction.mkOfCompact_star, BoundedContinuousFunction.norm_mkOfCompact