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

State before:
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ IsBump (f * g)
Tactic:
simp [IsBump]
State after:
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ HasCompactSupport (f * g) ∧ ContDiff ℝ ⊤ (f * g)

State before:
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ HasCompactSupport (f * g) ∧ ContDiff ℝ ⊤ (f * g)
Tactic:
apply And.intro
State after:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ HasCompactSupport (f * g)

case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ ContDiff ℝ ⊤ (f * g)

State before:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ HasCompactSupport (f * g)

case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ ContDiff ℝ ⊤ (f * g)
Tactic:
. apply HasCompactSupport.mul_right hf.left
State after:
case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ ContDiff ℝ ⊤ (f * g)

State before:
case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ ContDiff ℝ ⊤ (f * g)
Tactic:
. exact ContDiff.mul hf.right hg.right
State after:
no goals

State before:
case left
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ HasCompactSupport (f * g)
Tactic:
apply HasCompactSupport.mul_right hf.left
State after:
no goals

State before:
case right
α : Type u_1
inst✝¹ : NormedAddCommGroup α
inst✝ : NormedSpace ℝ α
f g : α → ℝ
hf : IsBump f
hg : IsBump g
⊢ ContDiff ℝ ⊤ (f * g)
Tactic:
exact ContDiff.mul hf.right hg.right
State after:
no goals