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 }
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
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
y : E
inr : (fun (x : E) ↦ (∑' (n : ℕ), (r n • g n) x : ℝ)) y ≤ (↑c : ℝ)
⊢ Membership.mem (γ := Set ℝ) (Icc 0 1) ((fun (x : E) ↦ (∑' (n : ℕ), (r n • g n) x : ℝ)) y)

Tactic:
refine ⟨tsum_nonneg fun n => mul_nonneg (rpos n).le (g_nonneg n y), le_trans ?_ c_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
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
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
y : E
⊢ HasSum (fun (n : ℕ) ↦ (↑(δ n) : ℝ)) (↑c : ℝ)

Tactic:
have A : HasSum (fun n => (δ n : ℝ)) c := NNReal.hasSum_coe.2 δc
-- 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
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
y : E
A : HasSum (fun (n : ℕ) ↦ (↑(δ n) : ℝ)) (↑c : ℝ)
inr : LE.le (α := ℝ) (∑' (n : ℕ), r n * g n y) (∑' (b : ℕ), (↑(δ b) : ℝ))
⊢ (fun (x : E) ↦ (∑' (n : ℕ), (r n • g n) x : ℝ)) y ≤ (↑c : ℝ)

Tactic:
simp only [Pi.smul_apply, smul_eq_mul, NNReal.val_eq_coe, ← A.tsum_eq]

Premises used: NNReal.val_eq_coe, HasSum.tsum_eq, smul_eq_mul, Pi.smul_apply
-- 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
δpos : ∀ (i : ℕ), 0 < δ i
c : ℝ≥0
δc : HasSum δ c
c_lt : c < 1
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
y : E
A : HasSum (fun (n : ℕ) ↦ (↑(δ n) : ℝ)) (↑c : ℝ)
apply : ∀ (i : ℕ), (r i • g i) y ≤ (↑(δ i) : ℝ)
⊢ LE.le (α := ℝ) (∑' (n : ℕ), r n * g n y) (∑' (b : ℕ), (↑(δ b) : ℝ))

Tactic:
apply Summable.tsum_le_tsum _ (S y) A.summable

Premises used: Summable.tsum_le_tsum, HasSum.summable
-- 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
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
y : E
A : HasSum (fun (n : ℕ) ↦ (↑(δ n) : ℝ)) (↑c : ℝ)
n : ℕ
apply : |(r n • g n) y| ≤ (↑(δ n) : ℝ)
⊢ (r n • g n) y ≤ (↑(δ n) : ℝ)

Tactic:
apply (le_abs_self _).trans

Premises used: le_abs_self, LE.le.trans
-- 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
r : (n : ℕ) → ℝ
rpos : ∀ (n : ℕ), 0 < r n
hr :
  ∀ (n i : ℕ),
    i ≤ n →
      ∀ (x : E),
        norm (E := ContinuousMultilinearMap ℝ (fun (i : Fin i) ↦ E) ℝ) (iteratedFDeriv ℝ i (r n • g n) x) ≤ (↑(δ n) : ℝ)
S : ∀ (x : E), Summable (α := ℝ) fun (n : ℕ) ↦ (r n • g n) x
y : E
A : HasSum (fun (n : ℕ) ↦ (↑(δ n) : ℝ)) (↑c : ℝ)
n : ℕ
⊢ |(r n • g n) y| ≤ (↑(δ n) : ℝ)

Tactic:
simpa only [norm_iteratedFDeriv_zero] using hr n 0 zero_le y

Premises used: zero_le, OfNat.ofNat, norm_iteratedFDeriv_zero
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)

Tactic:
have A : IsOpen (ball (0 : E) 1) := isOpen_ball
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
⊢ ∃ (f : E → ℝ), support f = ball 0 1 ∧ ContDiff ℝ ∞ f ∧ range f ⊆ Icc 0 1

Tactic:
A.exists_contDiff_support_eq

Premises used: IsOpen.exists_contDiff_support_eq
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
obtain :
  ∀ (f : E → ℝ) (f_support : support f = ball 0 1) (f_smooth : ContDiff ℝ ∞ f) (f_range : range f ⊆ Icc 0 1),
    ∃ (u : E → ℝ),
      ContDiff ℝ ∞ u ∧
        (∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (u x)) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x
⊢ ∃ (u : E → ℝ),
    ContDiff ℝ ∞ u ∧
      (∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (u x)) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x

Tactic:
obtain ⟨f, f_support, f_smooth, f_range⟩ :
      ∃ f : E → ℝ, f.support = ball (0 : E) 1 ∧ ContDiff ℝ ∞ f ∧ Set.range f ⊆ Set.Icc 0 1 :=
    A.exists_contDiff_support_eq

Premises used: Metric.ball, Set.Icc, IsOpen.exists_contDiff_support_eq, OfNat.ofNat
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
⊢ ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)

Tactic:
have B : ∀ x, f x ∈ Icc (0 : ℝ) 1 := fun x => f_range (mem_range_self x)
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
⊢ ∃ (u : E → ℝ),
    ContDiff ℝ ∞ u ∧
      (∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (u x)) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x

Tactic:
⟨fun x => (f x + f (-x)) / 2, ?_, ?_, ?_, ?_⟩

Premises used: HDiv.hDiv, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
refine_1 : ContDiff ℝ (F := ℝ) ∞ fun (x : E) ↦ (f x + f (-x)) / 2
refine_2 : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) ((fun (x : E) ↦ (f x + f (-x)) / 2) x)
refine_3 : Eq.{u_1 + 1} (α := Set E) (support (M := ℝ) fun (x : E) ↦ (f x + f (-x)) / 2) (ball 0 1)
refine_4 : ∀ (x : E), Eq (α := ℝ) ((fun (x : E) ↦ (f x + f (-x)) / 2) (-x)) ((fun (x : E) ↦ (f x + f (-x)) / 2) x)
⊢ ∃ (u : E → ℝ),
    ContDiff ℝ ∞ u ∧
      (∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (u x)) ∧ support u = ball 0 1 ∧ ∀ (x : E), u (-x) = u x

Tactic:
refine ⟨fun x => (f x + f (-x)) / 2, ?_, ?_, ?_, ?_⟩
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
⊢ ContDiff ℝ (F := ℝ) ∞ fun (x : E) ↦ (f x + f (-x)) / 2

Tactic:
(f_smooth.add (f_smooth.comp contDiff_neg)).div_const _

Premises used: ContDiff.div_const, contDiff_neg, ContDiff.comp, ContDiff.add
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
⊢ ContDiff ℝ (F := ℝ) ∞ fun (x : E) ↦ (f x + f (-x)) / 2

Tactic:
exact (f_smooth.add (f_smooth.comp contDiff_neg)).div_const _

Premises used: ContDiff.div_const, contDiff_neg, ContDiff.comp, ContDiff.add
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
refine_2 : 0 ≤ (f x + f (-x)) / 2
refine_2₁ : (f x + f (-x)) / 2 ≤ 1
⊢ 0 ≤ (f x + f (-x)) / 2 ∧ (f x + f (-x)) / 2 ≤ 1

Tactic:
constructor
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
linarith : (f x + f (-x)) / 2 < 0 → 2 / 2 = 1
linarith₁ : (f x + f (-x)) / 2 < 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (f x + f (-x)) / 2 < 0 → GT.gt (α := ℝ) 2 0
linarith₃ : (f x + f (-x)) / 2 < 0 → 1 * f x + 1 * f (-x) - HMul.hMul (α := ℝ) 2 0 + (0 - f x) + (0 - f (-x)) = 0
⊢ 0 ≤ (f x + f (-x)) / 2

Tactic:
linarith [(B x).1, (B (-x)).1]

Premises used: And.left, Neg.neg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
linarith : 1 < (f x + f (-x)) / 2 → 2 / 2 = 1
linarith₁ : 1 < (f x + f (-x)) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 < (f x + f (-x)) / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : 1 < (f x + f (-x)) / 2 → HMul.hMul (α := ℝ) 2 1 - (1 * f x + 1 * f (-x)) + (f x - 1) + (f (-x) - 1) = 0
⊢ (f x + f (-x)) / 2 ≤ 1

Tactic:
linarith [(B x).2, (B (-x)).2]

Premises used: And.right, Neg.neg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
⊢ Eq.{u_1 + 1} (α := Set E) (support (M := ℝ) fun (x : E) ↦ (f x + f (-x)) / 2) (ball 0 1)

Tactic:
support_eq_iff.2 ⟨fun x hx => ?_, fun x hx => ?_⟩

Premises used: Iff.mpr, Function.support_eq_iff, And.intro
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
refine_3 : ∀ (x : E) (hx : Membership.mem (γ := Set E) (ball 0 1) x), (f x + f (-x)) / 2 ≠ 0
refine_3₁ : ∀ (x : E) (hx : x ∉ ball 0 1), (f x + f (-x)) / 2 = 0
⊢ Eq.{u_1 + 1} (α := Set E) (support (M := ℝ) fun (x : E) ↦ (f x + f (-x)) / 2) (ball 0 1)

Tactic:
refine support_eq_iff.2 ⟨fun x hx => ?_, fun x hx => ?_⟩

Premises used: Iff.mpr, Function.support_eq_iff, And.intro
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
refine_3 : 0 < (f x + f (-x)) / 2
⊢ (f x + f (-x)) / 2 ≠ 0

Tactic:
apply ne_of_gt

Premises used: ne_of_gt
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
apply : f x ≠ 0
⊢ 0 < f x

Tactic:
apply lt_of_le_of_ne (B x).1 (Ne.symm _)

Premises used: Ne.symm, And.left, lt_of_le_of_ne
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
rwa rwa₁ rwa₂ rwa₃ : ∀ (hx : x ∈ support f), f x ≠ 0
⊢ f x ≠ 0

Tactic:
rwa [← f_support] at hx
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
⊢ 0 < f x

Tactic:
have : 0 < f x := by
        apply lt_of_le_of_ne (B x).1 (Ne.symm _)
        rwa [← f_support] at hx
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : Membership.mem (γ := Set E) (ball 0 1) x
this : 0 < f x
linarith : (f x + f (-x)) / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : (f x + f (-x)) / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (f x + f (-x)) / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
linarith₃ : (f x + f (-x)) / 2 ≤ 0 → 0 - f x + (1 * f x + 1 * f (-x) - HMul.hMul (α := ℝ) 2 0) + (0 - f (-x)) = 0
⊢ 0 < (f x + f (-x)) / 2

Tactic:
linarith [(B (-x)).1]

Premises used: And.left, Neg.neg
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx rwa rwa₁ rwa₂ rwa₃ : x ∉ ball 0 1
⊢ x ∉ support f

Tactic:
rwa [f_support]
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : x ∉ ball 0 1
⊢ x ∉ support f

Tactic:
have I1 : x ∉ support f := by rwa [f_support]
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : x ∉ ball 0 1
I1 : x ∉ support f
rw : -x ∉ ball 0 1
⊢ -x ∉ support f

Tactic:
rw [f_support]
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : x ∉ ball 0 1
I1 : x ∉ support f
⊢ -x ∉ ball 0 1

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : x ∉ ball 0 1
I1 : x ∉ support f
⊢ -x ∉ support f

Tactic:
have I2 : -x ∉ support f := by
        rw [f_support]
        simpa using hx
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : x ∉ ball 0 1
I1 : x ∉ support f
I2 : -x ∉ support f
⊢ f x = 0

Tactic:
simp only [mem_support, Classical.not_not] at I1 I2

Premises used: Classical.not_not, Function.mem_support
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : x ∉ ball 0 1
I1 : x ∉ support f
I2 : -x ∉ support f
I1₁ : f x = 0
⊢ f (-x) = 0

Tactic:
simp only [mem_support, Classical.not_not] at I1 I2

Premises used: Classical.not_not, Function.mem_support
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
hx : x ∉ ball 0 1
I1 : f x = 0
I2 : f (-x) = 0
⊢ (f x + f (-x)) / 2 = 0

Tactic:
simp only [I1, I2, add_zero, zero_div]

Premises used: zero_div, add_zero
-- Module: Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : FiniteDimensional ℝ E
A : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (ball 0 1)
f : E → ℝ
f_support : support f = ball 0 1
f_smooth : ContDiff ℝ ∞ f
f_range : range f ⊆ Icc 0 1
B : ∀ (x : E), Membership.mem (γ := Set ℝ) (Icc 0 1) (f x)
x : E
⊢ Eq (α := ℝ) ((fun (x : E) ↦ (f x + f (-x)) / 2) (-x)) ((fun (x : E) ↦ (f x + f (-x)) / 2) x)

Tactic:
simp only [add_comm, neg_neg]

Premises used: neg_neg, add_comm