-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_eq_zero_of_hasDerivAt_of_integrable
    (hderiv : ∀ x, HasDerivAt f (f' x) x) (hf' : Integrable f') (hf : Integrable f) :
    ∫ x, f' x = 0

Proof state:
case pos
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : CompleteSpace E
A : Tendsto f atBot (𝓝 0)
⊢ ∫ (x : ℝ), f' x = 0

Tactic:
have B : Tendsto f atTop (𝓝 0) :=
  tendsto_zero_of_hasDerivAt_of_integrableOn_Ioi (a := 0) (fun x _hx ↦ hderiv x)
    hf'.integrableOn hf.integrableOn

Result:
case pos
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : CompleteSpace E
A : Tendsto f atBot (𝓝 0)
B : Tendsto f atTop (𝓝 0)
⊢ ∫ (x : ℝ), f' x = 0

Proof state:
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
⊢ ∫ (x : ℝ), f' x = 0

Tactic:
by_cases hE : CompleteSpace E

Result:
case pos
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : CompleteSpace E
⊢ ∫ (x : ℝ), f' x = 0

case neg
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : ¬CompleteSpace E
⊢ ∫ (x : ℝ), f' x = 0

Proof state:
case pos
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : CompleteSpace E
⊢ ∫ (x : ℝ), f' x = 0

Tactic:
have A : Tendsto f atBot (𝓝 0) :=
  tendsto_zero_of_hasDerivAt_of_integrableOn_Iic (a := 0) (fun x _hx ↦ hderiv x)
    hf'.integrableOn hf.integrableOn

Result:
case pos
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : CompleteSpace E
A : Tendsto f atBot (𝓝 0)
⊢ ∫ (x : ℝ), f' x = 0

Proof state:
case pos
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : CompleteSpace E
⊢ ∫ (x : ℝ), f' x = 0

case neg
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : ¬CompleteSpace E
⊢ ∫ (x : ℝ), f' x = 0

Tactic:
swap

Result:
case neg
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : ¬CompleteSpace E
⊢ ∫ (x : ℝ), f' x = 0

case pos
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : CompleteSpace E
⊢ ∫ (x : ℝ), f' x = 0

Proof state:
case pos
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : CompleteSpace E
A : Tendsto f atBot (𝓝 0)
B : Tendsto f atTop (𝓝 0)
⊢ ∫ (x : ℝ), f' x = 0

Tactic:
simpa using integral_of_hasDerivAt_of_tendsto hderiv hf' A B

Result:
no goals

Proof state:
case neg
E : Type u_1
f f' : ℝ → E
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
hderiv : ∀ (x : ℝ), HasDerivAt f (f' x) x
hf' : Integrable f' volume
hf : Integrable f volume
hE : ¬CompleteSpace E
⊢ ∫ (x : ℝ), f' x = 0

Tactic:
simp [integral, hE]

Result:
no goals