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
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
this : Bornology.IsBounded (Euclidean.closedBall x d)
⊢ Bornology.IsBounded (tsupport f)

Tactic:
this.subset (Euclidean.isClosed_closedBall.closure_subset_iff.2 ?_)

Premises used: Iff.mpr, IsClosed.closure_subset_iff, Bornology.IsBounded.subset, Euclidean.isClosed_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
this : Bornology.IsBounded (Euclidean.closedBall x d)
refine_1 : support f ⊆ Euclidean.closedBall x d
⊢ Bornology.IsBounded (tsupport f)

Tactic:
refine this.subset (Euclidean.isClosed_closedBall.closure_subset_iff.2 ?_)

Premises used: Iff.mpr, IsClosed.closure_subset_iff, Bornology.IsBounded.subset, Euclidean.isClosed_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
this : Bornology.IsBounded (Euclidean.closedBall x d)
⊢ support f ⊆ Euclidean.closedBall x d

Tactic:
f_supp.trans Euclidean.ball_subset_closedBall

Premises used: HasSubset.Subset.trans, Euclidean.ball_subset_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
this : Bornology.IsBounded (Euclidean.closedBall x d)
⊢ support f ⊆ Euclidean.closedBall x d

Tactic:
exact f_supp.trans Euclidean.ball_subset_closedBall

Premises used: HasSubset.Subset.trans, Euclidean.ball_subset_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
refine_2 :
  ContDiff.{0, u_1, 0} ℝ (E := E) (F := EuclideanSpace ℝ (Fin (finrank ℝ E))) (↑n : ℕ∞ω)
    (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
⊢ ContDiff ℝ (↑n : ℕ∞ω) f

Tactic:
apply c.contDiff.comp

Premises used: ContDiffBump.contDiff, ContDiff.comp
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ ContDiff.{0, u_1, 0} ℝ (E := E) (F := EuclideanSpace ℝ (Fin (finrank ℝ E))) (↑n : ℕ∞ω)
    (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))

Tactic:
ContinuousLinearEquiv.contDiff _

Premises used: ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ ContDiff.{0, u_1, 0} ℝ (E := E) (F := EuclideanSpace ℝ (Fin (finrank ℝ E))) (↑n : ℕ∞ω)
    (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))

Tactic:
exact ContinuousLinearEquiv.contDiff _

Premises used: ContinuousLinearEquiv.contDiff
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
y : E
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) (f y)

Tactic:
⟨c.nonneg, c.le_one⟩

Premises used: Set.Mem, ContDiffBump.nonneg, setOf, Set.Icc, And.intro, ContDiffBump.le_one
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
y : E
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) (f y)

Tactic:
exact ⟨c.nonneg, c.le_one⟩
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
refine_4 :
  Membership.mem (α := EuclideanSpace ℝ (Fin (finrank ℝ E))) (γ := Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    (closedBall
        (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
          x)
        c.rIn :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
      EuclideanSpace ℝ (Fin (finrank ℝ E)))
⊢ f x = 1

Tactic:
apply c.one_of_mem_closedBall

Premises used: ContDiffBump.one_of_mem_closedBall
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
refine_4 : 0 ≤ c.rIn
⊢ Membership.mem (α := EuclideanSpace ℝ (Fin (finrank ℝ E))) (γ := Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    (closedBall
        (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
          x)
        c.rIn :
      Set (EuclideanSpace ℝ (Fin (finrank ℝ E))))
    (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
      EuclideanSpace ℝ (Fin (finrank ℝ E)))

Tactic:
apply mem_closedBall_self

Premises used: Metric.mem_closedBall_self
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ 0 ≤ c.rIn

Tactic:
(half_pos d_pos).le

Premises used: half_pos, LT.lt.le
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
s : Set E
x : E
n : ℕ∞
hs : s ∈ 𝓝 x
d : ℝ
d_pos : 0 < d
hd : Euclidean.closedBall x d ⊆ s
c : ContDiffBump (E := EuclideanSpace ℝ (Fin (finrank ℝ E)))
  (((toEuclidean : E ≃L[ℝ] EuclideanSpace ℝ (Fin (finrank ℝ E))) : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E))) x :
    EuclideanSpace ℝ (Fin (finrank ℝ E))) :=
  { rIn := d / 2, rOut := d, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }
f : E → ℝ :=
  (↑c : EuclideanSpace ℝ (Fin (finrank ℝ E)) → ℝ) ∘ (⇑toEuclidean : (a : E) → EuclideanSpace ℝ (Fin (finrank ℝ E)))
f_supp : support f ⊆ Euclidean.ball x d
f_tsupp : tsupport f ⊆ Euclidean.closedBall x d
⊢ 0 ≤ c.rIn

Tactic:
exact (half_pos d_pos).le

Premises used: half_pos, LT.lt.le
-- 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
inl :
  ∀ (hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅),
    ∃ (f : E → ℝ), support f = ∅ ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1
inr : ∀ (h's : s.Nonempty), ∃ (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:
rcases eq_empty_or_nonempty s with (rfl | h's)

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 : ℕ∞
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
⊢ Subset (α := Set ℝ) (range fun (x : E) ↦ 0) (Icc 0 1)

Tactic:
simp only [range_const, singleton_subset_iff, left_mem_Icc, zero_le_one]

Premises used: Set.singleton_subset_iff, zero_le_one, Set.left_mem_Icc, Set.range_const
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
n : ℕ∞
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
⊢ ∃ (f : E → ℝ), support f = ∅ ∧ ContDiff ℝ (↑n : ℕ∞ω) f ∧ range f ⊆ Icc 0 1

Tactic:
exact
      ⟨fun _ => 0, Function.support_zero, contDiff_const, by
        simp only [range_const, singleton_subset_iff, left_mem_Icc, zero_le_one]⟩
-- 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 }
⊢ ⋃ (f : ι), support (↑f : E → ℝ) = s

Tactic:
Subset.antisymm (iUnion_subset fun f => f.2.1) ?_

Premises used: Set.Subset.antisymm, Set.iUnion_subset, And.left, Subtype.property
-- 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 }
refine : s ⊆ ⋃ (f : ι), support (↑f : E → ℝ)
⊢ ⋃ (f : ι), support (↑f : E → ℝ) = s

Tactic:
refine Subset.antisymm (iUnion_subset fun f => f.2.1) ?_

Premises used: Set.Subset.antisymm, Set.iUnion_subset
-- 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 }
x : E
hx : x ∈ s
rcases :
  ∀ (f : E → ℝ) (hf : tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1),
    Membership.mem (γ := Set E) (⋃ (f : ι), support (↑f : E → ℝ)) x
⊢ Membership.mem (γ := Set E) (⋃ (f : ι), support (↑f : E → ℝ)) x

Tactic:
rcases exists_contDiff_tsupport_subset (hs.mem_nhds hx) with ⟨f, hf⟩

Premises used: IsOpen.mem_nhds, exists_contDiff_tsupport_subset
-- 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 }
x : E
hx : x ∈ s
f : E → ℝ
hf : tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
g : ι :=
  Subtype.mk (p := fun (f : E → ℝ) ↦ support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1) f ⋯
⊢ x ∈ support (↑g : E → ℝ)

Tactic:
simp only [g, hf.2.2.2.2, mem_support, Ne, one_ne_zero, not_false_iff]

Premises used: Ne, And.right, Function.mem_support, not_false_iff, 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 }
x : E
hx : x ∈ s
f : E → ℝ
hf : tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
g : ι :=
  Subtype.mk (p := fun (f : E → ℝ) ↦ support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1) f ⋯
⊢ x ∈ support (↑g : E → ℝ)

Tactic:
have : x ∈ support (g : E → ℝ) := by
        simp only [g, hf.2.2.2.2, mem_support, Ne, one_ne_zero, not_false_iff]
-- 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 }
x : E
hx : x ∈ s
f : E → ℝ
hf : tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
g : ι :=
  Subtype.mk (p := fun (f : E → ℝ) ↦ support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1) f ⋯
this : x ∈ support (↑g : E → ℝ)
⊢ Membership.mem (γ := Set E) (⋃ (f : ι), support (↑f : E → ℝ)) x

Tactic:
mem_iUnion_of_mem _ this

Premises used: Set.mem_iUnion_of_mem
-- 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 }
x : E
hx : x ∈ s
f : E → ℝ
hf : tsupport f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1 ∧ f x = 1
g : ι :=
  Subtype.mk (p := fun (f : E → ℝ) ↦ support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1) f ⋯
this : x ∈ support (↑g : E → ℝ)
⊢ Membership.mem (γ := Set E) (⋃ (f : ι), support (↑f : E → ℝ)) x

Tactic:
exact mem_iUnion_of_mem _ this

Premises used: Set.mem_iUnion_of_mem
-- 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 }
⊢ ⋃ (f : ι), support (↑f : E → ℝ) = s

Tactic:
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
-- 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 }
this : ⋃ (f : ι), support (↑f : E → ℝ) = s
simp_rw :
  ∃ (T : Set ι),
    T.Countable ∧ Eq.{u_1 + 1} (α := Set E) (⋃ f ∈ T, support (↑f : E → ℝ)) (⋃ (f : ι), support (↑f : E → ℝ))
⊢ ∃ (T : Set ι), T.Countable ∧ ⋃ f ∈ T, support (↑f : E → ℝ) = s

Tactic:
simp_rw [← this]
-- 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 }
this : ⋃ (f : ι), support (↑f : E → ℝ) = s
H : ∀ (i : ι), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (support (↑i : E → ℝ))
⊢ ∃ (T : Set ι),
    T.Countable ∧ Eq.{u_1 + 1} (α := Set E) (⋃ f ∈ T, support (↑f : E → ℝ)) (⋃ (f : ι), support (↑f : E → ℝ))

Tactic:
apply isOpen_iUnion_countable

Premises used: TopologicalSpace.isOpen_iUnion_countable
-- 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 }
this : ⋃ (f : ι), support (↑f : E → ℝ) = s
f : E → ℝ
hf : support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (support
      (↑(Subtype.mk (p := fun (f : E → ℝ) ↦ support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1) f
            hf) :
        E → ℝ))

Tactic:
hf.2.2.1.continuous.isOpen_support

Premises used: ContDiff.continuous, Continuous.isOpen_support, And.right, And.left
-- 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 }
this : ⋃ (f : ι), support (↑f : E → ℝ) = s
f : E → ℝ
hf : support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (support
      (↑(Subtype.mk (p := fun (f : E → ℝ) ↦ support f ⊆ s ∧ HasCompactSupport f ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1) f
            hf) :
        E → ℝ))

Tactic:
exact hf.2.2.1.continuous.isOpen_support

Premises used: ContDiff.continuous, Continuous.isOpen_support, And.right, And.left