Theorem: IsBump.comp_neg (ForML/Bump.lean)

State before:
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ IsBump fun x => f (-x)
Tactic:
constructor
State after:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ HasCompactSupport fun x => f (-x)

case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ ContDiff ℝ ⊤ fun x => f (-x)

State before:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ HasCompactSupport fun x => f (-x)

case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ ContDiff ℝ ⊤ fun x => f (-x)
Tactic:
. have h_neg {x : α} : -x = (Homeomorph.neg α) x := by simp [Homeomorph.neg]
  simp_rw [h_neg]
  exact HasCompactSupport.comp_homeomorph hf.left _
State after:
case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ ContDiff ℝ ⊤ fun x => f (-x)

State before:
case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ ContDiff ℝ ⊤ fun x => f (-x)
Tactic:
. exact ContDiff.comp hf.right contDiff_neg
State after:
no goals

State before:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ HasCompactSupport fun x => f (-x)
Tactic:
have h_neg {x : α} : -x = (Homeomorph.neg α) x := by simp [Homeomorph.neg]
State after:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
h_neg : ∀ {x : α}, -x = (Homeomorph.neg α) x
⊢ HasCompactSupport fun x => f (-x)

State before:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
h_neg : ∀ {x : α}, -x = (Homeomorph.neg α) x
⊢ HasCompactSupport fun x => f (-x)
Tactic:
simp_rw [h_neg]
State after:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
h_neg : ∀ {x : α}, -x = (Homeomorph.neg α) x
⊢ HasCompactSupport fun x => f ((Homeomorph.neg α) x)

State before:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
h_neg : ∀ {x : α}, -x = (Homeomorph.neg α) x
⊢ HasCompactSupport fun x => f ((Homeomorph.neg α) x)
Tactic:
exact HasCompactSupport.comp_homeomorph hf.left _
State after:
no goals

State before:
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
x : α
⊢ -x = (Homeomorph.neg α) x
Tactic:
simp [Homeomorph.neg]
State after:
no goals

State before:
case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f : α → ℝ
hf : IsBump f
⊢ ContDiff ℝ ⊤ fun x => f (-x)
Tactic:
exact ContDiff.comp hf.right contDiff_neg
State after:
no goals