Theorem: bounded_bump_sub_const (ForML/Dirac.lean)

State before:
φ : ℝ → ℝ
hφ : IsBump φ
y : ℝ
⊢ ∃ M, ∀ (x : ℝ), ‖φ x - y‖ ≤ M
Tactic:
rcases hφ.bounded with ⟨C, hC⟩
State after:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
⊢ ∃ M, ∀ (x : ℝ), ‖φ x - y‖ ≤ M

State before:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
⊢ ∃ M, ∀ (x : ℝ), ‖φ x - y‖ ≤ M
Tactic:
exists C + ‖y‖
State after:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
⊢ ∀ (x : ℝ), ‖φ x - y‖ ≤ C + ‖y‖

State before:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
⊢ ∀ (x : ℝ), ‖φ x - y‖ ≤ C + ‖y‖
Tactic:
intro x
State after:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
x : ℝ
⊢ ‖φ x - y‖ ≤ C + ‖y‖

State before:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
x : ℝ
⊢ ‖φ x - y‖ ≤ C + ‖y‖
Tactic:
refine le_trans (norm_sub_le _ _) ?_
State after:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
x : ℝ
⊢ ‖φ x‖ + ‖y‖ ≤ C + ‖y‖

State before:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
x : ℝ
⊢ ‖φ x‖ + ‖y‖ ≤ C + ‖y‖
Tactic:
simp
State after:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
x : ℝ
⊢ |φ x| ≤ C

State before:
case intro
φ : ℝ → ℝ
hφ : IsBump φ
y C : ℝ
hC : ∀ (x : ℝ), ‖φ x‖ ≤ C
x : ℝ
⊢ |φ x| ≤ C
Tactic:
exact hC x
State after:
no goals