-- Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
theorem y_smooth : ContDiffOn ℝ ∞ (uncurry y) (Ioo (0 : ℝ) 1 ×ˢ (univ : Set E))

Proof state:
case refine_1.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
p : ℝ
x : E
hp : p ∈ Ioo 0 1
hx : u (p⁻¹ • x) ≠ 0
this : ‖x‖ < p
⊢ ‖x‖ ≤ 1

Tactic:
exact this.le.trans hp.2.le

Result:
no goals

Proof state:
case refine_3.hg
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ (fun x => u (x.1⁻¹ • x.2)) (Ioo 0 1 ×ˢ univ)

Tactic:
apply (u_smooth E).comp_contDiffOn

Result:
case refine_3.hg
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ (fun x => x.1⁻¹ • x.2) (Ioo 0 1 ×ˢ univ)

Proof state:
case refine_3.hg
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ (fun x => x.1⁻¹ • x.2) (Ioo 0 1 ×ˢ univ)

Tactic:
exact ContDiffOn.smul (contDiffOn_fst.inv fun x hx => ne_of_gt hx.1.1) contDiffOn_snd

Result:
no goals

Proof state:
case refine_1.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
p : ℝ
x : E
hp : p ∈ Ioo 0 1
hx : u (p⁻¹ • x) ≠ 0
this : p⁻¹ • x ∈ support u
⊢ x ∈ closedBall 0 1

Tactic:
simp only [u_support, norm_smul, mem_ball_zero_iff, Real.norm_eq_abs, abs_inv,
  abs_of_nonneg hp.1.le, ← div_eq_inv_mul, div_lt_one hp.1] at this

Result:
case refine_1.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
p : ℝ
x : E
hp : p ∈ Ioo 0 1
hx : u (p⁻¹ • x) ≠ 0
this : ‖x‖ < p
⊢ x ∈ closedBall 0 1

Proof state:
case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
p : ℝ
x : E
hp : p ∈ Ioo 0 1
hx : x ∉ closedBall 0 1
⊢ w p x = 0

Tactic:
simp only [w, mul_inv_rev, Algebra.id.smul_eq_mul, mul_eq_zero, inv_eq_zero]

Result:
case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
p : ℝ
x : E
hp : p ∈ Ioo 0 1
hx : x ∉ closedBall 0 1
⊢ (|p| ^ finrank ℝ E = 0 ∨ ∫ (x : E), u x ∂μ = 0) ∨ u (p⁻¹ • x) = 0

Proof state:
case refine_1.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
p : ℝ
x : E
hp : p ∈ Ioo 0 1
hx : u (p⁻¹ • x) ≠ 0
⊢ x ∈ closedBall 0 1

Tactic:
have : p⁻¹ • x ∈ support u := mem_support.2 hx

Result:
case refine_1.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
p : ℝ
x : E
hp : p ∈ Ioo 0 1
hx : u (p⁻¹ • x) ≠ 0
this : p⁻¹ • x ∈ support u
⊢ x ∈ closedBall 0 1

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
⊢ ContDiffOn ℝ ∞ (uncurry y) (Ioo 0 1 ×ˢ univ)

Tactic:
have hs : IsOpen (Ioo (0 : ℝ) (1 : ℝ)) := isOpen_Ioo

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
⊢ ContDiffOn ℝ ∞ (uncurry y) (Ioo 0 1 ×ˢ univ)

Proof state:
case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ∀ (p : ℝ) (x : E), p ∈ Ioo 0 1 → x ∉ closedBall 0 1 → w p x = 0

Tactic:
rintro p x hp hx

Result:
case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
p : ℝ
x : E
hp : p ∈ Ioo 0 1
hx : x ∉ closedBall 0 1
⊢ w p x = 0

Proof state:
case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
p : ℝ
x : E
hp : p ∈ Ioo 0 1
hx : x ∉ closedBall 0 1
⊢ (|p| ^ finrank ℝ E = 0 ∨ ∫ (x : E), u x ∂μ = 0) ∨ u (p⁻¹ • x) = 0

Tactic:
right

Result:
case refine_1.h
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
p : ℝ
x : E
hp : p ∈ Ioo 0 1
hx : x ∉ closedBall 0 1
⊢ u (p⁻¹ • x) = 0

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ (uncurry y) (Ioo 0 1 ×ˢ univ)

Tactic:
refine contDiffOn_convolution_left_with_param (lsmul ℝ ℝ) hs hk ?_ ?_ ?_

Result:
case refine_1
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ∀ (p : ℝ) (x : E), p ∈ Ioo 0 1 → x ∉ closedBall 0 1 → w p x = 0

case refine_2
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ LocallyIntegrable φ μ

case refine_3
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ (↿w) (Ioo 0 1 ×ˢ univ)

Proof state:
case refine_3.hf.hf
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ (fun y => ‖y.1‖) (Ioo 0 1 ×ˢ univ)

Tactic:
apply ContDiffOn.norm ℝ

Result:
case refine_3.hf.hf.hf
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ContDiffOn ℝ ∞ Prod.fst (Ioo 0 1 ×ˢ univ)

case refine_3.hf.hf.h0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hs : IsOpen (Ioo 0 1)
hk : IsCompact (closedBall 0 1)
⊢ ∀ x ∈ Ioo 0 1 ×ˢ univ, x.1 ≠ 0