awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
inr :
  ∀ (T : Set ι) (T_count : T.Countable) (hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s),
    ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
⊢ ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1

Tactic:
obtain ⟨T, T_count, hT⟩ : ∃ T : Set ι, T.Countable ∧ ⋃ f ∈ T, support (f : E → ℝ) = s := by
    have : ⋃ f : ι, (f : E → ℝ).support = s := by
      refine Subset.antisymm (iUnion_subset fun f => f.2.1) ?_
      intro x hx
      rcases exists_contDiff_tsupport_subset (hs.mem_nhds hx) with ⟨f, hf⟩
      let g : ι := ⟨f, (subset_tsupport f).trans hf.1, hf.2.1, hf.2.2.1, hf.2.2.2.1⟩
      have : x ∈ support (g : E → ℝ) := by
        simp only [g, hf.2.2.2.2, mem_support, Ne, one_ne_zero, not_false_iff]
      exact mem_iUnion_of_mem _ this
    simp_rw [← this]
    apply isOpen_iUnion_countable
    rintro ⟨f, hf⟩
    exact hf.2.2.1.continuous.isOpen_support

Premises used: Set
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
apply : T.Nonempty
⊢ ∃ (g0 : ℕ → ι), T = range g0

Tactic:
apply Countable.exists_eq_range T_count

Premises used: Set.Countable.exists_eq_range
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
inl :
  ∀ (T_count : Set.Countable.{u_1} (α := ι) ∅)
    (hT : ⋃ (f : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ f), support (↑f : E → ℝ) = s), Set.Nonempty.{u_1} (α := ι) ∅
inr : ∀ (hT : T.Nonempty), T.Nonempty
⊢ T.Nonempty

Tactic:
rcases eq_empty_or_nonempty T with (rfl | hT)

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T_count : Set.Countable.{u_1} (α := ι) ∅
hT : ⋃ (f : ι), ⋃ (_ : Membership.mem (γ := Set ι) ∅ f), support (↑f : E → ℝ) = s
⊢ Set.Nonempty.{u_1} (α := ι) ∅

Tactic:
simp only [← hT, mem_empty_iff_false, iUnion_of_empty, iUnion_empty, Set.not_nonempty_empty]
        at h's

Premises used: Set.not_nonempty_empty, Set.iUnion_of_empty, Set.mem_empty_iff_false, Set.iUnion_empty
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT_1 : ⋃ f ∈ T, support (↑f : E → ℝ) = s
hT : T.Nonempty
⊢ T.Nonempty

Tactic:
hT
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT_1 : ⋃ f ∈ T, support (↑f : E → ℝ) = s
hT : T.Nonempty
⊢ T.Nonempty

Tactic:
exact hT
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
inr : ∀ (g0 : ℕ → ι) (hg : T = range g0), ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
⊢ ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1

Tactic:
obtain ⟨g0, hg⟩ : ∃ g0 : ℕ → ι, T = range g0 := by
    apply Countable.exists_eq_range T_count
    rcases eq_empty_or_nonempty T with (rfl | hT)
    · simp only [← hT, mem_empty_iff_false, iUnion_of_empty, iUnion_empty, Set.not_nonempty_empty]
        at h's
    · exact hT
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
⊢ ∀ (n : ℕ), support (g n) ⊆ s

Tactic:
have g_s : ∀ n, support (g n) ⊆ s := fun n => (g0 n).2.1
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
x : E
hx : x ∈ s
⊢ Membership.mem (γ := Set E) (⋃ f ∈ T, support (↑f : E → ℝ)) x

Tactic:
rw [← hT] at hx
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
x : E
hx : Membership.mem (γ := Set E) (⋃ f ∈ T, support (↑f : E → ℝ)) x
⊢ ∃ i ∈ T, x ∈ support (↑i : E → ℝ)

Tactic:
simpa only [mem_iUnion, exists_prop] using hx

Premises used: Set.mem_iUnion, exists_prop
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
x : E
hx : Membership.mem (γ := Set E) (⋃ f ∈ T, support (↑f : E → ℝ)) x
obtain : ∀ (i : ι) (iT : i ∈ T) (hi : x ∈ support (↑i : E → ℝ)), ∃ (n : ℕ), x ∈ support (g n)
⊢ ∃ (n : ℕ), x ∈ support (g n)

Tactic:
obtain ⟨i, iT, hi⟩ : ∃ i ∈ T, x ∈ support (i : E → ℝ) := by
      simpa only [mem_iUnion, exists_prop] using hx
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
x : E
hx : Membership.mem (γ := Set E) (⋃ f ∈ T, support (↑f : E → ℝ)) x
i : ι
iT : i ∈ T
hi : x ∈ support (↑i : E → ℝ)
obtain : ∀ (n : ℕ) (hn : g0 n = i), ∃ (n : ℕ), x ∈ support (g n)
⊢ ∃ (n : ℕ), x ∈ support (g n)

Tactic:
obtain ⟨n, hn⟩ := hg ▸ iT
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n_1 : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
x : E
hx : Membership.mem (γ := Set E) (⋃ f ∈ T, support (↑f : E → ℝ)) x
i : ι
iT : i ∈ T
hi : x ∈ support (↑i : E → ℝ)
n : ℕ
hn : g0 n = i
⊢ ∃ (n : ℕ), x ∈ support (g n)

Tactic:
grind
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
⊢ ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)

Tactic:
have s_g : ∀ x ∈ s, ∃ n, x ∈ support (g n) := fun x hx ↦ by
    rw [← hT] at hx
    obtain ⟨i, iT, hi⟩ : ∃ i ∈ T, x ∈ support (i : E → ℝ) := by
      simpa only [mem_iUnion, exists_prop] using hx
    #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
    (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this goal
    without the `obtain` on the next line. It is not yet clear whether this is due to defeq
    abuse in Mathlib or a problem in the new canonicalizer; a minimization would help. -/
    obtain ⟨n, hn⟩ := hg ▸ iT
    grind
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
⊢ ∀ (n : ℕ), ContDiff ℝ ∞ (g n)

Tactic:
have g_smooth : ∀ n, ContDiff ℝ ∞ (g n) := fun n => (g0 n).2.2.2.1
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
⊢ ∀ (n : ℕ), HasCompactSupport (g n)

Tactic:
have g_comp_supp : ∀ n, HasCompactSupport (g n) := fun n => (g0 n).2.2.1
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
⊢ ∀ (n : ℕ) (x : E), 0 ≤ g n x

Tactic:
have g_nonneg : ∀ n x, 0 ≤ g n x := fun n x => ((g0 n).2.2.2.2 (mem_range_self x)).1
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
⊢ ∃ (δ : ℕ → ℝ≥0), (∀ (i : ℕ), 0 < δ i) ∧ ∃ (c : ℝ≥0), HasSum δ c ∧ c < 1

Tactic:
NNReal.exists_pos_sum_of_countable one_ne_zero ℕ

Premises used: NNReal.exists_pos_sum_of_countable, Nat, one_ne_zero
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
inr :
  ∀ (δ : ℕ → ℝ≥0) (δpos : ∀ (i : ℕ), 0 < δ i) (c : ℝ≥0) (δc : HasSum δ c) (c_lt : c < 1),
    ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
⊢ ∃ (f : E → ℝ), support f = s ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1

Tactic:
obtain ⟨δ, δpos, c, δc, c_lt⟩ :
      ∃ δ : ℕ → ℝ≥0, (∀ i : ℕ, 0 < δ i) ∧ ∃ c : NNReal, HasSum δ c ∧ c < 1 :=
    NNReal.exists_pos_sum_of_countable one_ne_zero ℕ

Premises used: NNReal, NNReal.exists_pos_sum_of_countable, Nat, one_ne_zero
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n_1 : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n i : ℕ
apply :
  HasCompactSupport (β := ℝ) fun (x : E) ↦
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (g n) x)
⊢ BddAbove (α := ℝ)
    (range fun (x : E) ↦
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x))

Tactic:
apply ((g_smooth n).continuous_iteratedFDeriv
          (mod_cast le_top)).norm.bddAbove_range_of_hasCompactSupport

Premises used: Continuous.norm, ContDiff.continuous_iteratedFDeriv, Continuous.bddAbove_range_of_hasCompactSupport
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n_1 : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n i : ℕ
apply : HasCompactSupport (β := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (g n))
⊢ HasCompactSupport (β := ℝ) fun (x : E) ↦
    norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (g n) x)

Tactic:
apply HasCompactSupport.comp_left _ norm_zero

Premises used: norm_zero, HasCompactSupport.comp_left
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n_1 : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n i : ℕ
⊢ HasCompactSupport (β := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (g n))

Tactic:
apply (g_comp_supp n).iteratedFDeriv

Premises used: HasCompactSupport.iteratedFDeriv
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n_1 : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n i : ℕ
⊢ BddAbove (α := ℝ)
    (range fun (x : E) ↦
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x))

Tactic:
have : BddAbove (range fun x => ‖iteratedFDeriv ℝ i (fun x : E => g n x) x‖) := by
        apply ((g_smooth n).continuous_iteratedFDeriv
          (mod_cast le_top)).norm.bddAbove_range_of_hasCompactSupport
        apply HasCompactSupport.comp_left _ norm_zero
        apply (g_comp_supp n).iteratedFDeriv
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n_1 : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n i : ℕ
this :
  BddAbove (α := ℝ)
    (range fun (x : E) ↦
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x))
rcases :
  ∀ (R : ℝ)
    (hR :
      Membership.mem (γ := Set ℝ)
        (upperBounds
          (range fun (x : E) ↦
            norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ)
              (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x)))
        R),
    ∃ (R : ℝ),
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R
⊢ ∃ (R : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R

Tactic:
rcases this with ⟨R, hR⟩
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n_1 : ℕ∞
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h's : s.Nonempty
ι : Type (max 0 u_1) := { f : E → ℝ // support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 }
T : Set ι
T_count : T.Countable
hT : ⋃ f ∈ T, support (↑f : E → ℝ) = s
g0 : ℕ → ι
hg : T = range g0
g : ℕ → E → ℝ := fun (n : ℕ) ↦ (↑(g0 n) : E → ℝ)
g_s : ∀ (n : ℕ), support (g n) ⊆ s
s_g : ∀ x ∈ s, ∃ (n : ℕ), x ∈ support (g n)
g_smooth : ∀ (n : ℕ), ContDiff ℝ ∞ (g n)
g_comp_supp : ∀ (n : ℕ), HasCompactSupport (g n)
g_nonneg : ∀ (n : ℕ) (x : E), 0 ≤ g n x
δ : ℕ → ℝ≥0
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
n i : ℕ
R : ℝ
hR :
  Membership.mem (γ := Set ℝ)
    (upperBounds
      (range fun (x : E) ↦
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x)))
    R
⊢ ∃ (R : ℝ),
    ∀ (x : E),
      norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (fun (x : E) ↦ g n x) x) ≤ R

Tactic:
⟨R, fun x => hR (mem_range_self _)⟩

Premises used: Set.mem_range_self, Exists.intro