Theorem: tendsto_integral_bump_mul_deltaSeq (ForML/Dirac.lean)

State before:
φ : ℝ → ℝ
hφ : IsBump φ
⊢ Tendsto (fun n => ∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) atTop (nhds (φ 0))
Tactic:
suffices h_tendsto : Tendsto (fun (n : ℕ+) => ∫ x, (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
State after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) atTop (nhds (φ 0))

case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) atTop (nhds (φ 0))

case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. conv => arg 1; intro n; rw [← sub_add_cancel (∫ x, _) (φ 0)]
  conv => arg 3; rw [← sub_add_cancel (φ 0) (φ 0)]
  refine Tendsto.add_const _ ?_
  simp
  refine Filter.Tendsto.congr ?_ h_tendsto
  intro n
  simp [sub_mul]
  rw [integral_sub]
  rotate_left
  . exact IsBump.integrable_mul_continuous hφ DiracSeq.continuous
  . refine Integrable.const_mul ?_ _
    exact DiracSeq.integrable (by simp)
  simp [integral_mul_left, DiracSeq.integral]
State after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
have h_integrable {n : ℕ+} := @integrable_bump_sub_const_mul_diracSeq _ hφ (φ 0) n (by simp)
State after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
have hδ : Tendsto (fun (x : ℝ) => |φ x - φ 0|) (nhds 0) (nhds 0)
State after:
case hδ
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)

case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case hδ
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)

case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. refine Continuous.tendsto' ?_ _ _ (by simp)
  refine Continuous.abs ?_
  exact Continuous.sub hφ.continuous continuous_const
State after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
rw [Metric.tendsto_nhds_nhds] at hδ
State after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, dist x 0 < δ → dist |φ x - φ 0| 0 < ε
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ ε > 0, ∃ δ > 0, ∀ {x : ℝ}, dist x 0 < δ → dist |φ x - φ 0| 0 < ε
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
simp at hδ
State after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε
⊢ Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
simp [Metric.tendsto_atTop]
State after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

State before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε
⊢ ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
intro ε hε
State after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

State before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
hδ : ∀ (ε : ℝ), 0 < ε → ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε
ε : ℝ
hε : 0 < ε
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
specialize hδ (ε/2) (half_pos hε)
State after:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
hδ : ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

State before:
case h_tendsto
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
hδ : ∃ δ, 0 < δ ∧ ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
rcases hδ with ⟨δ, ⟨hδ, hδε⟩⟩
State after:
case h_tendsto.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

State before:
case h_tendsto.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
suffices : (∃ N, ∀ (n : ℕ+), N ≤ n → |∫ x in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε/2) ∧
    Tendsto (fun (n : ℕ+) => ∫ x in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
State after:
case h_tendsto.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
this :
  (∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2) ∧
    Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ (∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2) ∧
    Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case h_tendsto.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
this :
  (∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2) ∧
    Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ (∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2) ∧
    Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. rcases this with ⟨h_center, h_sides⟩
  simp [Metric.tendsto_atTop] at h_sides
  specialize h_sides (ε/2) (half_pos hε)
  rcases h_center with ⟨N_center, h_center⟩
  rcases h_sides with ⟨N_sides, h_sides⟩
  exists max N_center N_sides
  intro n hn
  specialize h_center n (le_of_max_le_left hn)
  specialize h_sides n (le_of_max_le_right hn)
  rw [← add_halves' ε]
  refine lt_of_le_of_lt ?_ (add_lt_add h_center h_sides)
  clear h_center h_sides hn N_center N_sides  have hδδ : -δ ≤ δ := by simp [hδ.le]
  simp [integral_eq_add_Iic_Ioc_Ioi h_integrable hδδ]
  conv =>
    lhs; arg 1
    conv => lhs; rw [add_comm]
    rw [add_assoc]
  refine le_trans (abs_add _ _) ?_
  simp
  refine le_of_eq ?_
  congr
  simp [integral_union, Set.Iic_disjoint_Ioi hδδ, h_integrable.integrableOn]
State after:
case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ (∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2) ∧
    Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ (∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2) ∧
    Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
apply And.intro
State after:
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2

case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2

case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. exists 1  intro n
  simp
  rw [integral_Ioc_eq_integral_Ioo]
  rw [← norm_eq_abs]
  refine lt_of_le_of_lt (@norm_integral_le_of_norm_le _ _ _ _ _ _ _
    (fun x => ε / 2 * DiracSeq n x) ?_ ?_) ?_
  . refine Integrable.integrableOn ?_
    exact Integrable.const_mul DiracSeq.integrable_pnat _
  . simp
    rw [eventually_inf_principal]
    refine ae_of_all _ ?_
    intro x hx
    simp [abs_of_nonneg, DiracSeq.nonneg_nat]
    refine mul_le_mul_of_nonneg_right ?_ (DiracSeq.nonneg_nat _)
    refine le_of_lt ?_
    apply hδε
    simp [abs_lt]
    exact hx
  . simp [integral_mul_left]
    rw [mul_lt_iff_lt_one_right (half_pos hε)]
    rw [← @DiracSeq.integral_pnat n]
    refine Ne.lt_of_le ?_ ?_
    . symm
      rw [← sub_ne_zero]
      rw [← integral_add_compl (by simp : MeasurableSet (Set.Ioo (-δ) δ)) DiracSeq.integrable_pnat]
      rw [@add_sub_cancel']
      simp
      rw [← ne_eq]
      refine DiracSeq.set_integral_ne_zero (by simp) ?_
      suffices : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
      . exact lt_of_lt_of_le (by simp) (measure_mono this)
      rw [Set.subset_def]
      simp
      intro x hx _
      exact hx
    . refine set_integral_le_integral (DiracSeq.integrable_pnat) ?_
      exact Filter.eventually_of_forall DiracSeq.nonneg_nat
State after:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. have hI₂ {a} (ha : 0 < a) : Tendsto (fun (n : ℕ+) => ∫ x in Set.Ioi a, (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
  . exact tendsto_integral_Ioi_bump_sub_const_mul ha hφ (φ 0)
  have hI₁ {a} (ha : 0 < a) : Tendsto (fun (n : ℕ+) => ∫ x in Set.Iic (-a), (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
  . exact tendsto_integral_Iic_bump_sub_const_mul ha hφ (φ 0)
  clear hδε hε ε  simp [integral_union, hδ.le, h_integrable.integrableOn]
  conv => rhs; rw [← add_zero 0]
  exact Tendsto.add (hI₁ hδ) (hI₂ hδ)
State after:
no goals

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) atTop (nhds (φ 0))
Tactic:
conv => arg 1; intro n; rw [← sub_add_cancel (∫ x, _) (φ 0)]
State after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0 + φ 0) atTop (nhds (φ 0))

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0 + φ 0) atTop (nhds (φ 0))
Tactic:
conv => arg 3; rw [← sub_add_cancel (φ 0) (φ 0)]
State after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0 + φ 0) atTop (nhds (φ 0 - φ 0 + φ 0))

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0 + φ 0) atTop (nhds (φ 0 - φ 0 + φ 0))
Tactic:
refine Tendsto.add_const _ ?_
State after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun k => (∫ (x : ℝ), φ x * DiracSeq (↑↑k) x) - φ 0) atTop (nhds (φ 0 - φ 0))

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun k => (∫ (x : ℝ), φ x * DiracSeq (↑↑k) x) - φ 0) atTop (nhds (φ 0 - φ 0))
Tactic:
simp
State after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun k => (∫ (x : ℝ), φ x * DiracSeq (↑↑k) x) - φ 0) atTop (nhds 0)

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun k => (∫ (x : ℝ), φ x * DiracSeq (↑↑k) x) - φ 0) atTop (nhds 0)
Tactic:
refine Filter.Tendsto.congr ?_ h_tendsto
State after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ ∀ (x : ℕ+), ∫ (x_1 : ℝ), (φ x_1 - φ 0) * DiracSeq (↑↑x) x_1 = (∫ (x_1 : ℝ), φ x_1 * DiracSeq (↑↑x) x_1) - φ 0

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ ∀ (x : ℕ+), ∫ (x_1 : ℝ), (φ x_1 - φ 0) * DiracSeq (↑↑x) x_1 = (∫ (x_1 : ℝ), φ x_1 * DiracSeq (↑↑x) x_1) - φ 0
Tactic:
intro n
State after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0
Tactic:
simp [sub_mul]
State after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ ∫ (x : ℝ), φ x * DiracSeq (↑↑n) x - φ 0 * DiracSeq (↑↑n) x = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ ∫ (x : ℝ), φ x * DiracSeq (↑↑n) x - φ 0 * DiracSeq (↑↑n) x = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0
Tactic:
rw [integral_sub]
State after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ (∫ (a : ℝ), φ a * DiracSeq (↑↑n) a) - ∫ (a : ℝ), φ 0 * DiracSeq (↑↑n) a = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0

case hf
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ x * DiracSeq (↑↑n) x

case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ (∫ (a : ℝ), φ a * DiracSeq (↑↑n) a) - ∫ (a : ℝ), φ 0 * DiracSeq (↑↑n) a = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0

case hf
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ x * DiracSeq (↑↑n) x

case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x
Tactic:
rotate_left
State after:
case hf
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ x * DiracSeq (↑↑n) x

case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x

φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ (∫ (a : ℝ), φ a * DiracSeq (↑↑n) a) - ∫ (a : ℝ), φ 0 * DiracSeq (↑↑n) a = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0

State before:
case hf
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ x * DiracSeq (↑↑n) x

case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x

φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ (∫ (a : ℝ), φ a * DiracSeq (↑↑n) a) - ∫ (a : ℝ), φ 0 * DiracSeq (↑↑n) a = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0
Tactic:
. exact IsBump.integrable_mul_continuous hφ DiracSeq.continuous
State after:
case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x

φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ (∫ (a : ℝ), φ a * DiracSeq (↑↑n) a) - ∫ (a : ℝ), φ 0 * DiracSeq (↑↑n) a = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0

State before:
case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x

φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ (∫ (a : ℝ), φ a * DiracSeq (↑↑n) a) - ∫ (a : ℝ), φ 0 * DiracSeq (↑↑n) a = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0
Tactic:
. refine Integrable.const_mul ?_ _
  exact DiracSeq.integrable (by simp)
State after:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ (∫ (a : ℝ), φ a * DiracSeq (↑↑n) a) - ∫ (a : ℝ), φ 0 * DiracSeq (↑↑n) a = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ (∫ (a : ℝ), φ a * DiracSeq (↑↑n) a) - ∫ (a : ℝ), φ 0 * DiracSeq (↑↑n) a = (∫ (x : ℝ), φ x * DiracSeq (↑↑n) x) - φ 0
Tactic:
simp [integral_mul_left, DiracSeq.integral]
State after:
no goals

State before:
case hf
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ x * DiracSeq (↑↑n) x
Tactic:
exact IsBump.integrable_mul_continuous hφ DiracSeq.continuous
State after:
no goals

State before:
case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => φ 0 * DiracSeq (↑↑n) x
Tactic:
refine Integrable.const_mul ?_ _
State after:
case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x

State before:
case hg
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ Integrable fun x => DiracSeq (↑↑n) x
Tactic:
exact DiracSeq.integrable (by simp)
State after:
no goals

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_tendsto : Tendsto (fun n => ∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
n : ℕ+
⊢ 0 < ↑↑n
Tactic:
simp
State after:
no goals

State before:
φ : ℝ → ℝ
hφ : IsBump φ
n : ℕ+
⊢ 0 < ↑↑n
Tactic:
simp
State after:
no goals

State before:
case hδ
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Tendsto (fun x => |φ x - φ 0|) (nhds 0) (nhds 0)
Tactic:
refine Continuous.tendsto' ?_ _ _ (by simp)
State after:
case hδ
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Continuous fun x => |φ x - φ 0|

State before:
case hδ
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Continuous fun x => |φ x - φ 0|
Tactic:
refine Continuous.abs ?_
State after:
case hδ
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Continuous fun x => φ x - φ 0

State before:
case hδ
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ Continuous fun x => φ x - φ 0
Tactic:
exact Continuous.sub hφ.continuous continuous_const
State after:
no goals

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
⊢ |φ 0 - φ 0| = 0
Tactic:
simp
State after:
no goals

State before:
case h_tendsto.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
this :
  (∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2) ∧
    Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
rcases this with ⟨h_center, h_sides⟩
State after:
case h_tendsto.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
h_center : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

State before:
case h_tendsto.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
h_center : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
simp [Metric.tendsto_atTop] at h_sides
State after:
case h_tendsto.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
h_center : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides :
  ∀ (ε : ℝ),
    0 < ε → ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

State before:
case h_tendsto.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
h_center : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides :
  ∀ (ε : ℝ),
    0 < ε → ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
specialize h_sides (ε/2) (half_pos hε)
State after:
case h_tendsto.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
h_center : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

State before:
case h_tendsto.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
h_center : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
rcases h_center with ⟨N_center, h_center⟩
State after:
case h_tendsto.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
h_sides : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
N_center : ℕ+
h_center : ∀ (n : ℕ+), N_center ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

State before:
case h_tendsto.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
h_sides : ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
N_center : ℕ+
h_center : ∀ (n : ℕ+), N_center ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
rcases h_sides with ⟨N_sides, h_sides⟩
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center : ℕ+
h_center : ∀ (n : ℕ+), N_center ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
N_sides : ℕ+
h_sides : ∀ (n : ℕ+), N_sides ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center : ℕ+
h_center : ∀ (n : ℕ+), N_center ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
N_sides : ℕ+
h_sides : ∀ (n : ℕ+), N_sides ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
exists max N_center N_sides
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center : ℕ+
h_center : ∀ (n : ℕ+), N_center ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
N_sides : ℕ+
h_sides : ∀ (n : ℕ+), N_sides ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ ∀ (n : ℕ+), max N_center N_sides ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center : ℕ+
h_center : ∀ (n : ℕ+), N_center ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
N_sides : ℕ+
h_sides : ∀ (n : ℕ+), N_sides ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ ∀ (n : ℕ+), max N_center N_sides ≤ n → |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
intro n hn
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center : ℕ+
h_center : ∀ (n : ℕ+), N_center ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
N_sides : ℕ+
h_sides : ∀ (n : ℕ+), N_sides ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
n : ℕ+
hn : max N_center N_sides ≤ n
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center : ℕ+
h_center : ∀ (n : ℕ+), N_center ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
N_sides : ℕ+
h_sides : ∀ (n : ℕ+), N_sides ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
n : ℕ+
hn : max N_center N_sides ≤ n
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
specialize h_center n (le_of_max_le_left hn)
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center N_sides : ℕ+
h_sides : ∀ (n : ℕ+), N_sides ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center N_sides : ℕ+
h_sides : ∀ (n : ℕ+), N_sides ≤ n → |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
specialize h_sides n (le_of_max_le_right hn)
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center N_sides n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center N_sides n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε
Tactic:
rw [← add_halves' ε]
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center N_sides n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2 + ε / 2

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center N_sides n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2 + ε / 2
Tactic:
refine lt_of_le_of_lt ?_ (add_lt_add h_center h_sides)
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center N_sides n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
N_center N_sides n : ℕ+
hn : max N_center N_sides ≤ n
h_center : |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
h_sides : |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
clear h_center h_sides hn N_center N_sides
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
have hδδ : -δ ≤ δ := by simp [hδ.le]
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ |∫ (x : ℝ), (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
simp [integral_eq_add_Iic_Ioc_Ioi h_integrable hδδ]
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ |((∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
          ∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ |((∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
          ∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
conv =>
  lhs; arg 1
  conv => lhs; rw [add_comm]
  rw [add_assoc]
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ |(∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ((∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
          ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ |(∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ((∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
          ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
refine le_trans (abs_add _ _) ?_
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |(∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
          ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |(∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
          ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| +
      |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
simp
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ |(∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ |(∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| ≤
    |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
refine le_of_eq ?_
State after:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ |(∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| =
    |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|

State before:
case h_tendsto.intro.intro.intro.intro.intro
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ |(∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x| =
    |∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x|
Tactic:
congr
State after:
case h_tendsto.intro.intro.intro.intro.intro.e_a
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) + ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x =
    ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x

State before:
case h_tendsto.intro.intro.intro.intro.intro.e_a
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
hδδ : -δ ≤ δ
⊢ (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) + ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x =
    ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x
Tactic:
simp [integral_union, Set.Iic_disjoint_Ioi hδδ, h_integrable.integrableOn]
State after:
no goals

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ -δ ≤ δ
Tactic:
simp [hδ.le]
State after:
no goals

State before:
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∃ N, ∀ (n : ℕ+), N ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
Tactic:
exists 1
State after:
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∀ (n : ℕ+), 1 ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2

State before:
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ ∀ (n : ℕ+), 1 ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
Tactic:
intro n
State after:
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ 1 ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2

State before:
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ 1 ≤ n → |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
Tactic:
simp
State after:
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2

State before:
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ |∫ (x : ℝ) in Set.Ioc (-δ) δ, (φ x - φ 0) * DiracSeq (↑↑n) x| < ε / 2
Tactic:
rw [integral_Ioc_eq_integral_Ioo]
State after:
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ |∫ (t : ℝ) in Set.Ioo (-δ) δ, (φ t - φ 0) * DiracSeq (↑↑n) t| < ε / 2

State before:
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ |∫ (t : ℝ) in Set.Ioo (-δ) δ, (φ t - φ 0) * DiracSeq (↑↑n) t| < ε / 2
Tactic:
rw [← norm_eq_abs]
State after:
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ‖∫ (t : ℝ) in Set.Ioo (-δ) δ, (φ t - φ 0) * DiracSeq (↑↑n) t‖ < ε / 2

State before:
case this.left
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ‖∫ (t : ℝ) in Set.Ioo (-δ) δ, (φ t - φ 0) * DiracSeq (↑↑n) t‖ < ε / 2
Tactic:
refine lt_of_le_of_lt (@norm_integral_le_of_norm_le _ _ _ _ _ _ _
  (fun x => ε / 2 * DiracSeq n x) ?_ ?_) ?_
State after:
case this.left.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ Integrable fun x => ε / 2 * DiracSeq (↑↑n) x

case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Set.Ioo (-δ) δ),
    ‖(φ x - φ 0) * DiracSeq (↑↑n) x‖ ≤ (fun x => ε / 2 * DiracSeq (↑↑n) x) x

case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, ε / 2 * DiracSeq (↑↑n) x < ε / 2

State before:
case this.left.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ Integrable fun x => ε / 2 * DiracSeq (↑↑n) x

case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Set.Ioo (-δ) δ),
    ‖(φ x - φ 0) * DiracSeq (↑↑n) x‖ ≤ (fun x => ε / 2 * DiracSeq (↑↑n) x) x

case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, ε / 2 * DiracSeq (↑↑n) x < ε / 2
Tactic:
. refine Integrable.integrableOn ?_
  exact Integrable.const_mul DiracSeq.integrable_pnat _
State after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Set.Ioo (-δ) δ),
    ‖(φ x - φ 0) * DiracSeq (↑↑n) x‖ ≤ (fun x => ε / 2 * DiracSeq (↑↑n) x) x

case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, ε / 2 * DiracSeq (↑↑n) x < ε / 2

State before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Set.Ioo (-δ) δ),
    ‖(φ x - φ 0) * DiracSeq (↑↑n) x‖ ≤ (fun x => ε / 2 * DiracSeq (↑↑n) x) x

case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, ε / 2 * DiracSeq (↑↑n) x < ε / 2
Tactic:
. simp
  rw [eventually_inf_principal]
  refine ae_of_all _ ?_
  intro x hx
  simp [abs_of_nonneg, DiracSeq.nonneg_nat]
  refine mul_le_mul_of_nonneg_right ?_ (DiracSeq.nonneg_nat _)
  refine le_of_lt ?_
  apply hδε
  simp [abs_lt]
  exact hx
State after:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, ε / 2 * DiracSeq (↑↑n) x < ε / 2

State before:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, ε / 2 * DiracSeq (↑↑n) x < ε / 2
Tactic:
. simp [integral_mul_left]
  rw [mul_lt_iff_lt_one_right (half_pos hε)]
  rw [← @DiracSeq.integral_pnat n]
  refine Ne.lt_of_le ?_ ?_
  . symm
    rw [← sub_ne_zero]
    rw [← integral_add_compl (by simp : MeasurableSet (Set.Ioo (-δ) δ)) DiracSeq.integrable_pnat]
    rw [@add_sub_cancel']
    simp
    rw [← ne_eq]
    refine DiracSeq.set_integral_ne_zero (by simp) ?_
    suffices : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
    . exact lt_of_lt_of_le (by simp) (measure_mono this)
    rw [Set.subset_def]
    simp
    intro x hx _
    exact hx
  . refine set_integral_le_integral (DiracSeq.integrable_pnat) ?_
    exact Filter.eventually_of_forall DiracSeq.nonneg_nat
State after:
no goals

State before:
case this.left.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ Integrable fun x => ε / 2 * DiracSeq (↑↑n) x
Tactic:
exact Integrable.const_mul DiracSeq.integrable_pnat _
State after:
no goals

State before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (Set.Ioo (-δ) δ),
    ‖(φ x - φ 0) * DiracSeq (↑↑n) x‖ ≤ (fun x => ε / 2 * DiracSeq (↑↑n) x) x
Tactic:
simp
State after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᶠ (x : ℝ) in Measure.ae volume ⊓ 𝓟 (Set.Ioo (-δ) δ), |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x

State before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᶠ (x : ℝ) in Measure.ae volume ⊓ 𝓟 (Set.Ioo (-δ) δ), |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x
Tactic:
rw [eventually_inf_principal]
State after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᵐ (x : ℝ), x ∈ Set.Ioo (-δ) δ → |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x

State before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ᵐ (x : ℝ), x ∈ Set.Ioo (-δ) δ → |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x
Tactic:
refine ae_of_all _ ?_
State after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ a ∈ Set.Ioo (-δ) δ, |φ a - φ 0| * |DiracSeq (↑↑n) a| ≤ ε / 2 * DiracSeq (↑↑n) a

State before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ a ∈ Set.Ioo (-δ) δ, |φ a - φ 0| * |DiracSeq (↑↑n) a| ≤ ε / 2 * DiracSeq (↑↑n) a
Tactic:
intro x hx
State after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x

State before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| * |DiracSeq (↑↑n) x| ≤ ε / 2 * DiracSeq (↑↑n) x
Tactic:
simp [abs_of_nonneg, DiracSeq.nonneg_nat]
State after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| * DiracSeq (↑↑n) x ≤ ε / 2 * DiracSeq (↑↑n) x

State before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| * DiracSeq (↑↑n) x ≤ ε / 2 * DiracSeq (↑↑n) x
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (DiracSeq.nonneg_nat _)
State after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| ≤ ε / 2

State before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| ≤ ε / 2
Tactic:
refine le_of_lt ?_
State after:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| < ε / 2

State before:
case this.left.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |φ x - φ 0| < ε / 2
Tactic:
apply hδε
State after:
case this.left.refine_2.a
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |x| < δ

State before:
case this.left.refine_2.a
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ |x| < δ
Tactic:
simp [abs_lt]
State after:
case this.left.refine_2.a
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ -δ < x ∧ x < δ

State before:
case this.left.refine_2.a
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : x ∈ Set.Ioo (-δ) δ
⊢ -δ < x ∧ x < δ
Tactic:
exact hx
State after:
no goals

State before:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, ε / 2 * DiracSeq (↑↑n) x < ε / 2
Tactic:
simp [integral_mul_left]
State after:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ε / 2 * ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a < ε / 2

State before:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ε / 2 * ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a < ε / 2
Tactic:
rw [mul_lt_iff_lt_one_right (half_pos hε)]
State after:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a < 1

State before:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a < 1
Tactic:
rw [← @DiracSeq.integral_pnat n]
State after:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a < ∫ (x : ℝ), DiracSeq (↑↑n) x

State before:
case this.left.refine_3
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a < ∫ (x : ℝ), DiracSeq (↑↑n) x
Tactic:
refine Ne.lt_of_le ?_ ?_
State after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠ ∫ (x : ℝ), DiracSeq (↑↑n) x

case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≤ ∫ (x : ℝ), DiracSeq (↑↑n) x

State before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠ ∫ (x : ℝ), DiracSeq (↑↑n) x

case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≤ ∫ (x : ℝ), DiracSeq (↑↑n) x
Tactic:
. symm
  rw [← sub_ne_zero]
  rw [← integral_add_compl (by simp : MeasurableSet (Set.Ioo (-δ) δ)) DiracSeq.integrable_pnat]
  rw [@add_sub_cancel']
  simp
  rw [← ne_eq]
  refine DiracSeq.set_integral_ne_zero (by simp) ?_
  suffices : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
  . exact lt_of_lt_of_le (by simp) (measure_mono this)
  rw [Set.subset_def]
  simp
  intro x hx _
  exact hx
State after:
case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≤ ∫ (x : ℝ), DiracSeq (↑↑n) x

State before:
case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≤ ∫ (x : ℝ), DiracSeq (↑↑n) x
Tactic:
. refine set_integral_le_integral (DiracSeq.integrable_pnat) ?_
  exact Filter.eventually_of_forall DiracSeq.nonneg_nat
State after:
no goals

State before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠ ∫ (x : ℝ), DiracSeq (↑↑n) x
Tactic:
symm
State after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ), DiracSeq (↑↑n) x ≠ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a

State before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ), DiracSeq (↑↑n) x ≠ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a
Tactic:
rw [← sub_ne_zero]
State after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ (∫ (x : ℝ), DiracSeq (↑↑n) x) - ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠ 0

State before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ (∫ (x : ℝ), DiracSeq (↑↑n) x) - ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠ 0
Tactic:
rw [← integral_add_compl (by simp : MeasurableSet (Set.Ioo (-δ) δ)) DiracSeq.integrable_pnat]
State after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) x ∂volume + ∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume -
      ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠
    0

State before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) x ∂volume + ∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume -
      ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≠
    0
Tactic:
rw [@add_sub_cancel']
State after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume ≠ 0

State before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume ≠ 0
Tactic:
simp
State after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ¬∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume = 0

State before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ¬∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume = 0
Tactic:
rw [← ne_eq]
State after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume ≠ 0

State before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (x : ℝ) in (Set.Ioo (-δ) δ)ᶜ, DiracSeq (↑↑n) x ∂volume ≠ 0
Tactic:
refine DiracSeq.set_integral_ne_zero (by simp) ?_
State after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ 0 < ↑↑volume (Set.Ioo (-δ) δ)ᶜ

State before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ 0 < ↑↑volume (Set.Ioo (-δ) δ)ᶜ
Tactic:
suffices : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
State after:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
this : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
⊢ 0 < ↑↑volume (Set.Ioo (-δ) δ)ᶜ

case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ

State before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
this : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
⊢ 0 < ↑↑volume (Set.Ioo (-δ) δ)ᶜ

case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
Tactic:
. exact lt_of_lt_of_le (by simp) (measure_mono this)
State after:
case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ

State before:
case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
Tactic:
rw [Set.subset_def]
State after:
case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ x ∈ Set.Ici δ, x ∈ (Set.Ioo (-δ) δ)ᶜ

State before:
case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ x ∈ Set.Ici δ, x ∈ (Set.Ioo (-δ) δ)ᶜ
Tactic:
simp
State after:
case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ (x : ℝ), δ ≤ x → -δ < x → δ ≤ x

State before:
case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∀ (x : ℝ), δ ≤ x → -δ < x → δ ≤ x
Tactic:
intro x hx _
State after:
case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : δ ≤ x
a✝ : -δ < x
⊢ δ ≤ x

State before:
case this
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
x : ℝ
hx : δ ≤ x
a✝ : -δ < x
⊢ δ ≤ x
Tactic:
exact hx
State after:
no goals

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ MeasurableSet (Set.Ioo (-δ) δ)
Tactic:
simp
State after:
no goals

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ 0 < ↑↑n
Tactic:
simp
State after:
no goals

State before:
case this.left.refine_3.refine_1
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
this : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
⊢ 0 < ↑↑volume (Set.Ioo (-δ) δ)ᶜ
Tactic:
exact lt_of_lt_of_le (by simp) (measure_mono this)
State after:
no goals

State before:
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
this : Set.Ici δ ⊆ (Set.Ioo (-δ) δ)ᶜ
⊢ 0 < ↑↑volume (Set.Ici δ)
Tactic:
simp
State after:
no goals

State before:
case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ ∫ (a : ℝ) in Set.Ioo (-δ) δ, DiracSeq (↑↑n) a ≤ ∫ (x : ℝ), DiracSeq (↑↑n) x
Tactic:
refine set_integral_le_integral (DiracSeq.integrable_pnat) ?_
State after:
case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ 0 ≤ᵐ[volume] fun a => DiracSeq (↑↑n) a

State before:
case this.left.refine_3.refine_2
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
n : ℕ+
⊢ 0 ≤ᵐ[volume] fun a => DiracSeq (↑↑n) a
Tactic:
exact Filter.eventually_of_forall DiracSeq.nonneg_nat
State after:
no goals

State before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
have hI₂ {a} (ha : 0 < a) : Tendsto (fun (n : ℕ+) => ∫ x in Set.Ioi a, (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
State after:
case hI₂
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case hI₂
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. exact tendsto_integral_Ioi_bump_sub_const_mul ha hφ (φ 0)
State after:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
have hI₁ {a} (ha : 0 < a) : Tendsto (fun (n : ℕ+) => ∫ x in Set.Iic (-a), (φ x - φ 0) * DiracSeq n x) atTop (nhds 0)
State after:
case hI₁
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case hI₁
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
. exact tendsto_integral_Iic_bump_sub_const_mul ha hφ (φ 0)
State after:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
clear hδε hε ε
State after:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)

State before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-δ) ∪ Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
simp [integral_union, hδ.le, h_integrable.integrableOn]
State after:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto
    (fun n =>
      (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)
    atTop (nhds 0)

State before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto
    (fun n =>
      (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)
    atTop (nhds 0)
Tactic:
conv => rhs; rw [← add_zero 0]
State after:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto
    (fun n =>
      (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)
    atTop (nhds (0 + 0))

State before:
case this.right
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
δ : ℝ
hδ : 0 < δ
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
hI₁ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
⊢ Tendsto
    (fun n =>
      (∫ (x : ℝ) in Set.Iic (-δ), (φ x - φ 0) * DiracSeq (↑↑n) x) +
        ∫ (x : ℝ) in Set.Ioi δ, (φ x - φ 0) * DiracSeq (↑↑n) x)
    atTop (nhds (0 + 0))
Tactic:
exact Tendsto.add (hI₁ hδ) (hI₂ hδ)
State after:
no goals

State before:
case hI₂
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
exact tendsto_integral_Ioi_bump_sub_const_mul ha hφ (φ 0)
State after:
no goals

State before:
case hI₁
φ : ℝ → ℝ
hφ : IsBump φ
h_integrable : ∀ {n : ℕ+}, Integrable fun x => (φ x - φ 0) * DiracSeq (↑↑n) x
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
hδε : ∀ {x : ℝ}, |x| < δ → |φ x - φ 0| < ε / 2
hI₂ : ∀ {a : ℝ}, 0 < a → Tendsto (fun n => ∫ (x : ℝ) in Set.Ioi a, (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
a : ℝ
ha : 0 < a
⊢ Tendsto (fun n => ∫ (x : ℝ) in Set.Iic (-a), (φ x - φ 0) * DiracSeq (↑↑n) x) atTop (nhds 0)
Tactic:
exact tendsto_integral_Iic_bump_sub_const_mul ha hφ (φ 0)
State after:
no goals