Theorem: integral_point (PnP2023/Lec_03_10/FormalCalculus.lean)

State before:
f : ℝ → ℝ
int : Integrable f
a : ℝ
⊢ integral f a a = 0
Tactic:
unfold integral
State after:
f : ℝ → ℝ
int : Integrable f
a : ℝ
⊢ Integrable.integral f a a = 0

State before:
f : ℝ → ℝ
int : Integrable f
a : ℝ
⊢ Integrable.integral f a a = 0
Tactic:
have l := int.interval_union a a a
State after:
f : ℝ → ℝ
int : Integrable f
a : ℝ
l : Integrable.integral f a a = Integrable.integral f a a + Integrable.integral f a a
⊢ Integrable.integral f a a = 0

State before:
f : ℝ → ℝ
int : Integrable f
a : ℝ
l : Integrable.integral f a a = Integrable.integral f a a + Integrable.integral f a a
⊢ Integrable.integral f a a = 0
Tactic:
simp  at l
State after:
f : ℝ → ℝ
int : Integrable f
a : ℝ
l : Integrable.integral f a a = 0
⊢ Integrable.integral f a a = 0

State before:
f : ℝ → ℝ
int : Integrable f
a : ℝ
l : Integrable.integral f a a = 0
⊢ Integrable.integral f a a = 0
Tactic:
assumption
State after:
no goals