-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem y_eq_one_of_mem_closedBall {D : ℝ} {x : E} (Dpos : 0 < D)
    (hx : x ∈ closedBall (0 : E) (1 - D)) : y 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
hx : x ∈ closedBall 0 (1 - D)
C : ball x D ⊆ ball 0 1
y : E
hy : y ∈ ball x D
h'y : 1 < dist y 0
⊢ False

Tactic:
linarith only [mem_ball.1 (C hy), h'y]

Result:
no goals

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
hx : x ∈ closedBall 0 (1 - D)
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1

Tactic:
have B : ∀ y : E, y ∈ ball x D → φ y = 1 := by
  have C : ball x D ⊆ ball 0 1 := by
    apply ball_subset_ball'
    simp only [mem_closedBall] at hx
    linarith only [hx]
  intro y hy
  simp only [φ, indicator, mem_closedBall, ite_eq_left_iff, not_le, zero_ne_one]
  intro h'y
  linarith only [mem_ball.1 (C hy), h'y]

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
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1

Proof state:
case h
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
hx : dist x 0 ≤ 1 - D
⊢ D + dist x 0 ≤ 1

Tactic:
linarith only [hx]

Result:
no goals

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
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
B' : ∀ y ∈ ball x D, φ y = φ x
⊢ ∫ (t : E), ((lsmul ℝ ℝ) (w D t)) (φ x) ∂μ = 1

Tactic:
simp only [lsmul_apply, Algebra.id.smul_eq_mul, integral_mul_right, w_integral E Dpos, Bx,
  one_mul]

Result:
no goals

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
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1

Tactic:
have Bx : φ x = 1 := B _ (mem_ball_self Dpos)

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
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) 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
hx : x ∈ closedBall 0 (1 - D)
⊢ ∀ y ∈ ball x D, φ y = 1

Tactic:
have C : ball x D ⊆ ball 0 1 := by
  apply ball_subset_ball'
  simp only [mem_closedBall] at hx
  linarith only [hx]

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
hx : x ∈ closedBall 0 (1 - D)
C : ball x D ⊆ ball 0 1
⊢ ∀ y ∈ ball x D, φ 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
hx : x ∈ closedBall 0 (1 - D)
C : ball x D ⊆ ball 0 1
y : E
hy : y ∈ ball x D
⊢ 1 < dist y 0 → False

Tactic:
intro h'y

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
hx : x ∈ closedBall 0 (1 - D)
C : ball x D ⊆ ball 0 1
y : E
hy : y ∈ ball x D
h'y : 1 < dist y 0
⊢ False

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
hx : x ∈ closedBall 0 (1 - D)
C : ball x D ⊆ ball 0 1
y : E
hy : y ∈ ball x D
⊢ φ y = 1

Tactic:
simp only [φ, indicator, mem_closedBall, ite_eq_left_iff, not_le, zero_ne_one]

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
hx : x ∈ closedBall 0 (1 - D)
C : ball x D ⊆ ball 0 1
y : E
hy : y ∈ ball x D
⊢ 1 < dist y 0 → False

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
hx : x ∈ closedBall 0 (1 - D)
⊢ y D x = 1

Tactic:
change (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1

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
hx : x ∈ closedBall 0 (1 - D)
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) 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
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
⊢ ∀ y ∈ ball x D, φ y = φ x

Tactic:
rw [Bx]

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
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
⊢ ∀ y ∈ ball x D, φ 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
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
⊢ ∀ y ∈ ball x D, φ y = 1

Tactic:
exact B

Result:
no goals

Proof state:
case h
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
hx : x ∈ closedBall 0 (1 - D)
⊢ D + dist x 0 ≤ 1

Tactic:
simp only [mem_closedBall] at hx

Result:
case h
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
hx : dist x 0 ≤ 1 - D
⊢ D + dist x 0 ≤ 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
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1

Tactic:
have B' : ∀ y, y ∈ ball x D → φ y = φ x := by rw [Bx]; exact B

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
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
B' : ∀ y ∈ ball x D, φ y = φ x
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) 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
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
B' : ∀ y ∈ ball x D, φ y = φ x
⊢ (w D ⋆[lsmul ℝ ℝ, μ] φ) x = 1

Tactic:
rw [convolution_eq_right' _ (le_of_eq (w_support E Dpos)) B']

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
hx : x ∈ closedBall 0 (1 - D)
B : ∀ y ∈ ball x D, φ y = 1
Bx : φ x = 1
B' : ∀ y ∈ ball x D, φ y = φ x
⊢ ∫ (t : E), ((lsmul ℝ ℝ) (w D t)) (φ x) ∂μ = 1