awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CocompactMap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
g : CocompactMap α β
toFun : α → β
continuous_toFun : Continuous toFun
cocompact_tendsto' :
  Tendsto { toFun := toFun, continuous_toFun := continuous_toFun : C(α, β) }.toFun (cocompact α) (cocompact β)
h :
  Eq (α := (a : α) → β)
    ((fun (f : CocompactMap α β) ↦ f.toFun)
      { toFun := toFun, continuous_toFun := continuous_toFun, cocompact_tendsto' := cocompact_tendsto' })
    ((fun (f : CocompactMap α β) ↦ f.toFun) g)
⊢ { toFun := toFun, continuous_toFun := continuous_toFun, cocompact_tendsto' := cocompact_tendsto' :
      CocompactMap α β } =
    g
have obtain : ∀ (toFun_1 : α → β) (continuous_toFun_1 : Continuous toFun_1)
  (cocompact_tendsto'_1 :
    Tendsto { toFun := toFun_1, continuous_toFun := continuous_toFun_1 : C(α, β) }.toFun (cocompact α) (cocompact β))
  (h :
    Eq (α := (a : α) → β)
      ((fun (f : CocompactMap α β) ↦ f.toFun)
        { toFun := toFun, continuous_toFun := continuous_toFun, cocompact_tendsto' := cocompact_tendsto' })
      ((fun (f : CocompactMap α β) ↦ f.toFun)
        { toFun := toFun_1, continuous_toFun := continuous_toFun_1, cocompact_tendsto' := cocompact_tendsto'_1 })),
  { toFun := toFun, continuous_toFun := continuous_toFun, cocompact_tendsto' := cocompact_tendsto' :
      CocompactMap α β } =
    { toFun := toFun_1, continuous_toFun := continuous_toFun_1, cocompact_tendsto' := cocompact_tendsto'_1 }
Tactic: obtain ⟨⟨_, _⟩, _⟩ := g
Cleared hypotheses: g, h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CocompactMap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Continuous f'
have rw : Continuous.{u_1, u_2} (X := α) (Y := β) (⇑f : (a : α) → β)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CocompactMap (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
inst_2 : TopologicalSpace γ
inst_3 : TopologicalSpace δ
f : CocompactMap α β
f' : α → β
h : f' = (⇑f : (a : α) → β)
⊢ Tendsto f' (cocompact α) (cocompact β)
have simp_rw : Tendsto (⇑f : (a : α) → β) (cocompact α) (cocompact β)
Tactic: simp_rw [h]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CocompactMap (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : CocompactMap α β
s : Set β
hs : IsCompact s
h's : IsClosed s
⊢ IsCompact.{u_1} (X := α) ((⇑f : (a : α) → β) ⁻¹' s)
have obtain : ∀ (t : Set α) (ht : IsCompact t) (hts : ((⇑f : (a : α) → β) ⁻¹' s)ᶜᶜ ⊆ t),
  IsCompact.{u_1} (X := α) ((⇑f : (a : α) → β) ⁻¹' s)
Tactic: obtain ⟨t, ht, hts⟩ :=
    mem_cocompact'.mp
      (by
        simpa only [preimage_image_preimage, preimage_compl] using
          mem_map.mp
            (cocompact_tendsto f <|
              mem_cocompact.mpr ⟨s, hs, compl_subset_compl.mpr (image_preimage_subset f _)⟩))
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CocompactMap (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
⊢ Tendsto (⇑f : (a : α) → β) (cocompact α) (cocompact β)
have refine : ∀ (K : Set β) (hK : IsCompact K), IsCompact.{u_1} (X := α) ((⇑f : (a : α) → β) ⁻¹' K)
Tactic: refine CocompactMap.tendsto_of_forall_preimage fun K hK => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CocompactMap (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
⊢ IsCompact.{u_1} (X := α) ((⇑f : (a : α) → β) ⁻¹' K)
have this : Eq.{u_1 + 1} (α := Set α) ((⇑f.symm : (a : β) → α) '' K) ((⇑f.toEquiv : (a : α) → β) ⁻¹' K)
Tactic: have := f.toEquiv.image_symm_eq_preimage K
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.CocompactMap (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : TopologicalSpace β
f : α ≃ₜ β
K : Set β
hK : IsCompact K
this : Eq.{u_1 + 1} (α := Set α) ((⇑f.symm : (a : β) → α) '' K) ((⇑f : (a : α) → β) ⁻¹' K)
⊢ IsCompact.{u_1} (X := α) ((⇑f : (a : α) → β) ⁻¹' K)
have rw : IsCompact.{u_1} (X := α) ((⇑f.symm : (a : β) → α) '' K)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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(α, β)
⊢ (mkOfCompact f).toContinuousMap = f
have h : ∀ (a : α), Eq.{u_2 + 1} (α := β) (((mkOfCompact f).toContinuousMap : (a : α) → β) a : β) ((f : (a : α) → β) a : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
f : α →ᵇ β
⊢ mkOfCompact f.toContinuousMap = f
have h : ∀ (x : α), Eq.{u_2 + 1} (α := β) ((mkOfCompact f.toContinuousMap : (a : α) → β) x : β) ((f : (a : α) → β) x : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
⊢ ∀ (s : Set (C(α, β) × C(α, β))),
    Membership.mem (γ := Filter (C(α, β) × C(α, β))) (uniformity C(α, β)) s ↔
      ∃ (t : Set ((α →ᵇ β) × (α →ᵇ β))),
        Membership.mem (γ := Filter ((α →ᵇ β) × (α →ᵇ β))) (uniformity (α →ᵇ β)) t ∧
          ∀ (x y : C(α, β)),
            Membership.mem (α := (α →ᵇ β) × (α →ᵇ β)) t
                (((equivBoundedOfCompact α β : (a : C(α, β)) → α →ᵇ β) x,
                    (equivBoundedOfCompact α β : (a : C(α, β)) → α →ᵇ β) y) :
                  (α →ᵇ β) × (α →ᵇ β)) →
              (x, y) ∈ s
have simp : ∀ (s : Set (C(α, β) × C(α, β))),
  (∃ (i : Prod.{u_1, u_2} (Set α) (Set (β × β))),
      (IsCompact i.1 ∧ ∃ (i_1 : ℝ), 0 < i_1 ∧ {p : β × β | dist p.1 p.2 ≤ i_1} ⊆ i.2) ∧
        {fg : C(α, β) × C(α, β) |
            ∀ x ∈ i.1, Membership.mem (α := β × β) i.2 (((fg.1 : (a : α) → β) x, (fg.2 : (a : α) → β) x) : β × β)} ⊆
          s) ↔
    ∃ (t : Set ((α →ᵇ β) × (α →ᵇ β))),
      (∃ (i : ℝ), 0 < i ∧ {p : (α →ᵇ β) × (α →ᵇ β) | dist p.1 p.2 ≤ i} ⊆ t) ∧
        ∀ (x y : C(α, β)),
          Membership.mem (α := (α →ᵇ β) × (α →ᵇ β)) t
              (((equivBoundedOfCompact α β : (a : C(α, β)) → α →ᵇ β) x,
                  (equivBoundedOfCompact α β : (a : C(α, β)) → α →ᵇ β) y) :
                (α →ᵇ β) × (α →ᵇ β)) →
            (x, y) ∈ s
Tactic: simp only [hasBasis_compactConvergenceUniformity.mem_iff, uniformity_basis_dist_le.mem_iff]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
C0 : 0 < C
⊢ dist f g < C ↔ ∀ (x : α), dist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C
have rw : (∀ (x : α), dist.{u_2} (α := β) ((mkOfCompact f : (a : α) → β) x : β) ((mkOfCompact g : (a : α) → β) x : β) < C) ↔
  ∀ (x : α), dist.{u_2} (α := β) ((f : (a : α) → β) x : β) ((g : (a : α) → β) x : β) < C
Tactic: rw [← dist_mkOfCompact, dist_lt_iff_of_compact C0]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
x y : C(α, E)
⊢ dist x y = ‖-x + y‖
have rw : dist x y = ‖mkOfCompact (-x + y)‖
Tactic: rw [← norm_mkOfCompact, ← dist_mkOfCompact, dist_eq_norm_neg_add,
    mkOfCompact_add, mkOfCompact_neg]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
x y : C(α, E)
rw : dist x y = ‖mkOfCompact (-x + y)‖
⊢ dist x y = ‖-x + y‖
have rw₁ : dist (mkOfCompact x) (mkOfCompact y) = ‖mkOfCompact (-x + y)‖
Tactic: rw [← norm_mkOfCompact, ← dist_mkOfCompact, dist_eq_norm_neg_add,
    mkOfCompact_add, mkOfCompact_neg]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
x y : C(α, E)
rw : dist x y = ‖mkOfCompact (-x + y)‖
rw₁ : dist (mkOfCompact x) (mkOfCompact y) = ‖mkOfCompact (-x + y)‖
⊢ dist x y = ‖-x + y‖
have rw₂ : ‖-mkOfCompact x + mkOfCompact y‖ = ‖mkOfCompact (-x + y)‖
Tactic: rw [← norm_mkOfCompact, ← dist_mkOfCompact, dist_eq_norm_neg_add,
    mkOfCompact_add, mkOfCompact_neg]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
x y : C(α, E)
rw : dist x y = ‖mkOfCompact (-x + y)‖
rw₁ : dist (mkOfCompact x) (mkOfCompact y) = ‖mkOfCompact (-x + y)‖
rw₂ : ‖-mkOfCompact x + mkOfCompact y‖ = ‖mkOfCompact (-x + y)‖
⊢ dist x y = ‖-x + y‖
have rw₃ : ‖-mkOfCompact x + mkOfCompact y‖ = ‖mkOfCompact (-x) + mkOfCompact y‖
Tactic: rw [← norm_mkOfCompact, ← dist_mkOfCompact, dist_eq_norm_neg_add,
    mkOfCompact_add, mkOfCompact_neg]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : TopologicalSpace α
inst_1 : CompactSpace α
inst_2 : PseudoMetricSpace β
inst_3 : SeminormedAddCommGroup E
x y : C(α, E)
rw : dist x y = ‖mkOfCompact (-x + y)‖
rw₁ : dist (mkOfCompact x) (mkOfCompact y) = ‖mkOfCompact (-x + y)‖
rw₂ : ‖-mkOfCompact x + mkOfCompact y‖ = ‖mkOfCompact (-x + y)‖
rw₃ : ‖-mkOfCompact x + mkOfCompact y‖ = ‖mkOfCompact (-x) + mkOfCompact y‖
⊢ dist x y = ‖-x + y‖
have rw₄ : ‖-mkOfCompact x + mkOfCompact y‖ = ‖-mkOfCompact x + mkOfCompact y‖
Tactic: rw [← norm_mkOfCompact, ← dist_mkOfCompact, dist_eq_norm_neg_add,
    mkOfCompact_add, mkOfCompact_neg]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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)
⊢ 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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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 : α
⊢ 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)
have 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)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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
have h₁ : ∀ (x : α), Eq.{u_4 + 1} (α := R) ((mkOfCompact f * mkOfCompact g : (a : α) → R) x : R) ((0 : (a : α) → R) x : R)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (hypothesis)
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‖
have h₁ : mkOfCompact f * mkOfCompact g = 0
Tactic: replace h : mkOfCompact f * mkOfCompact g = 0 := by ext x; simpa using congr($h x)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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‖₊
⊢ NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ insert j s, f i) = (insert j s).sup fun (x : ι) ↦ ‖f x‖₊
have insert : f j * ∑ i ∈ s, f i = 0
Tactic: suffices f j * ∑ i ∈ s, f i = 0 by simpa [hj, ← ih] using nnnorm_add_eq_max this
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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)
⊢ NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have empty : NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ ∅, f i) = Finset.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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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‖₊
⊢ NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have 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 j s, f i) = (insert j 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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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)
⊢ NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have empty : NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ ∅, f i) = Finset.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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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‖₊
⊢ NNNorm.nnnorm (E := C(α, R)) (∑ i ∈ s, f i) = s.sup fun (x : ι) ↦ ‖f x‖₊
have 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 j s, f i) = (insert j 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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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
have 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)
Tactic: refine (ContinuousMap.exists_tendsto_compactOpen_iff_forall _).2 fun K hK => ?_
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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
⊢ ∃ (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)
have 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)
Tactic: lift K to Compacts X using hK
Cleared hypotheses: K, hK
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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))
have 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)
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (hypothesis)
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
⊢ ∃ (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)
have 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))
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]
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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
have 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)
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
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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
have 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)
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
-- Lean 4 proof step from Mathlib.Topology.ContinuousMap.Compact (goal)
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)
⊢ Summable F
have 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)
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