-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable
    (hu : ∀ x, HasDerivAt u (u' x) x) (hv : ∀ x, HasDerivAt v (v' x) x)
    (huv' : Integrable (fun x ↦ L (u x) (v' x))) (hu'v : Integrable (fun x ↦ L (u' x) (v x)))
    (huv : Integrable (fun x ↦ L (u x) (v x))) :
    ∫ (x : ℝ), L (u x) (v' x) = - ∫ (x : ℝ), L (u' x) (v x)

Proof state:
case pos
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
huv : Integrable (fun x => (L (u x)) (v x)) volume
hG : CompleteSpace G
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)

Tactic:
have I : Tendsto (fun x ↦ L (u x) (v x)) atBot (𝓝 0) :=
  tendsto_zero_of_hasDerivAt_of_integrableOn_Iic (a := 0)
    (fun x _hx ↦ L.hasDerivAt_of_bilinear (hu x) (hv x))
    (huv'.add hu'v).integrableOn huv.integrableOn

Result:
case pos
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
huv : Integrable (fun x => (L (u x)) (v x)) volume
hG : CompleteSpace G
I : Tendsto (fun x => (L (u x)) (v x)) atBot (𝓝 0)
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)

Proof state:
case pos
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
huv : Integrable (fun x => (L (u x)) (v x)) volume
hG : CompleteSpace G
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)

case neg
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
huv : Integrable (fun x => (L (u x)) (v x)) volume
hG : ¬CompleteSpace G
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)

Tactic:
swap

Result:
case neg
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
huv : Integrable (fun x => (L (u x)) (v x)) volume
hG : ¬CompleteSpace G
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)

case pos
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
huv : Integrable (fun x => (L (u x)) (v x)) volume
hG : CompleteSpace G
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)

Proof state:
case neg
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
huv : Integrable (fun x => (L (u x)) (v x)) volume
hG : ¬CompleteSpace G
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)

Tactic:
simp [integral, hG]

Result:
no goals

Proof state:
case pos
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
huv : Integrable (fun x => (L (u x)) (v x)) volume
hG : CompleteSpace G
I : Tendsto (fun x => (L (u x)) (v x)) atBot (𝓝 0)
J : Tendsto (fun x => (L (u x)) (v x)) atTop (𝓝 0)
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)

Tactic:
simp [integral_bilinear_hasDerivAt_right_eq_sub hu hv huv' hu'v I J]

Result:
no goals

Proof state:
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
huv : Integrable (fun x => (L (u x)) (v x)) volume
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
huv : Integrable (fun x => (L (u x)) (v x)) volume
hG : CompleteSpace G
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)

case neg
E : Type u_1
F : Type u_2
G : Type u_3
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
L : E →L[ℝ] F →L[ℝ] G
u : ℝ → E
v : ℝ → F
u' : ℝ → E
v' : ℝ → F
hu : ∀ (x : ℝ), HasDerivAt u (u' x) x
hv : ∀ (x : ℝ), HasDerivAt v (v' x) x
huv' : Integrable (fun x => (L (u x)) (v' x)) volume
hu'v : Integrable (fun x => (L (u' x)) (v x)) volume
huv : Integrable (fun x => (L (u x)) (v x)) volume
hG : ¬CompleteSpace G
⊢ ∫ (x : ℝ), (L (u x)) (v' x) = -∫ (x : ℝ), (L (u' x)) (v x)