Theorem: integral_symm (ForML/Dirac.lean)

State before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ), f x
Tactic:
have hs : MeasurableSet (Set.Ioi 0 : Set ℝ) := measurableSet_Ioi
State after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ), f x

State before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ), f x
Tactic:
rw [← integral_add_compl hs hf]
State after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f x ∂volume + ∫ (x : ℝ) in (Set.Ioi 0)ᶜ, f x ∂volume

State before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f x ∂volume + ∫ (x : ℝ) in (Set.Ioi 0)ᶜ, f x ∂volume
Tactic:
simp
State after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f x ∂volume + ∫ (x : ℝ) in Set.Iic 0, f x ∂volume

State before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 2 * ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f x ∂volume + ∫ (x : ℝ) in Set.Iic 0, f x ∂volume
Tactic:
simp only [@two_mul ℝ]
State after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ (∫ (x : ℝ) in Set.Ioi 0, f x) + ∫ (x : ℝ) in Set.Ioi 0, f x =
    ∫ (x : ℝ) in Set.Ioi 0, f x ∂volume + ∫ (x : ℝ) in Set.Iic 0, f x ∂volume

State before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ (∫ (x : ℝ) in Set.Ioi 0, f x) + ∫ (x : ℝ) in Set.Ioi 0, f x =
    ∫ (x : ℝ) in Set.Ioi 0, f x ∂volume + ∫ (x : ℝ) in Set.Iic 0, f x ∂volume
Tactic:
simp
State after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Iic 0, f x ∂volume

State before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Iic 0, f x ∂volume
Tactic:
have h0 : (0 : ℝ) = -0 := by norm_num
State after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Iic 0, f x ∂volume

State before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Iic 0, f x ∂volume
Tactic:
rw [h0]
State after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi (-0), f x = ∫ (x : ℝ) in Set.Iic (-0), f x ∂volume

State before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi (-0), f x = ∫ (x : ℝ) in Set.Iic (-0), f x ∂volume
Tactic:
rw [← integral_comp_neg_Ioi]
State after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi (-0), f x = ∫ (x : ℝ) in Set.Ioi 0, f (-x)

State before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi (-0), f x = ∫ (x : ℝ) in Set.Ioi 0, f (-x)
Tactic:
simp
State after:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f (-x)

State before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ ∫ (x : ℝ) in Set.Ioi 0, f x = ∫ (x : ℝ) in Set.Ioi 0, f (-x)
Tactic:
congr
State after:
case e_f
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ (fun x => f x) = fun x => f (-x)

State before:
case e_f
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
⊢ (fun x => f x) = fun x => f (-x)
Tactic:
ext x
State after:
case e_f.h
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
x : ℝ
⊢ f x = f (-x)

State before:
case e_f.h
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
h0 : 0 = -0
x : ℝ
⊢ f x = f (-x)
Tactic:
rw [h_symm]
State after:
no goals

State before:
f : ℝ → ℝ
hf : Integrable f
h_symm : ∀ (x : ℝ), f (-x) = f x
hs : MeasurableSet (Set.Ioi 0)
⊢ 0 = -0
Tactic:
norm_num
State after:
no goals