-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem y_pos_of_mem_ball {D : ℝ} {x : E} (Dpos : 0 < D) (D_lt_one : D < 1)
    (hx : x ∈ ball (0 : E) (1 + D)) : 0 < y D x

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ y ∈ ball 0 D ∧ ‖x - y‖ ≤ 1

Tactic:
constructor

Result:
case left
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ y ∈ ball 0 D

case right
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ ‖x - y‖ ≤ 1

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ -(D / (1 + D) - 1) = 1 / (1 + D)

Tactic:
simp only [B.ne', Ne, not_false_iff, mul_one, neg_sub, add_tsub_cancel_right,
  field_simps]

Result:
no goals

Proof state:
case refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
⊢ 0 < μ (support fun i => w D i * φ (x - i))

Tactic:
set z := (D / (1 + D)) • x with hz

Result:
case refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
⊢ 0 < μ (support fun i => w D i * φ (x - i))

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ D * (1 + D - ‖x‖) + D * ‖x‖ ≤ D * (1 + D)

Tactic:
ring_nf

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ D + D ^ 2 ≤ D + D ^ 2

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ D * (1 + D - ‖x‖) / (1 + D) + dist z 0 ≤ D

Tactic:
simp only [hz, norm_smul, abs_of_nonneg Dpos.le, abs_of_nonneg B.le, dist_zero_right,
  Real.norm_eq_abs, abs_div]

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
⊢ D * (1 + D - ‖x‖) / (1 + D) + D / (1 + D) * ‖x‖ ≤ D

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D)
⊢ D * (1 + D - ‖x‖) / (1 + D) + dist z x ≤ 1

Tactic:
rw [← one_smul ℝ x, dist_eq_norm, hz, ← sub_smul, one_smul, norm_smul, ID]

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D)
⊢ D * (1 + D - ‖x‖) / (1 + D) + 1 / (1 + D) * ‖x‖ ≤ 1

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D)
⊢ D * (1 + D - ‖x‖) / (1 + D) + 1 / (1 + D) * ‖x‖ ≤ 1

Tactic:
simp only [B.ne', div_le_iff₀ B, field_simps]

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
y : E
hy : y ∈ ball z (D * (1 + D - ‖x‖) / (1 + D))
ID : ‖D / (1 + D) - 1‖ = 1 / (1 + D)
⊢ D * (1 + D - ‖x‖) + 1 * ‖x‖ ≤ 1 * (1 + D)

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
C : ball z (D * (1 + D - ‖x‖) / (1 + D)) ⊆ support fun y => w D y * φ (x - y)
⊢ 0 < μ (ball z (D * (1 + D - ‖x‖) / (1 + D)))

Tactic:
apply measure_ball_pos

Result:
case hr
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
z : E := (D / (1 + D)) • x
hz : z = (D / (1 + D)) • x
B : 0 < 1 + D
C : ball z (D * (1 + D - ‖x‖) / (1 + D)) ⊆ support fun y => w D y * φ (x - y)
⊢ 0 < D * (1 + D - ‖x‖) / (1 + D)

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
⊢ 0 < y D x

Tactic:
refine (integral_pos_iff_support_of_nonneg (w_mul_φ_nonneg D x) ?_).2 ?_

Result:
case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
⊢ Integrable (fun i => w D i * φ (x - i)) μ

case refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
D : ℝ
x : E
Dpos : 0 < D
D_lt_one : D < 1
hx : ‖x‖ < 1 + D
⊢ 0 < μ (support fun i => w D i * φ (x - i))