awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
μ : Measure E
inst_9 : SigmaFinite μ
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (μ.prod volume)
hfg' :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) (μ.prod volume)
hfg :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) (μ.prod volume)
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
rw :
  Eq.{u_4 + 1} (α := W)
    (-∫ (a : E),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
          (((B : (a : F) → G →L[ℝ] W) (f' (a, t)) : G →L[ℝ] W) : (a : G) → W) (g (a, t)) ∂μ)
    (-@integral _ _ _ _ Prod.instMeasurableSpace (μ.prod volume) fun (x : E × ℝ) ↦
        (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x))
rw₁ rw₂ :
  Eq.{u_4 + 1} (α := W)
    (-∫ (a : E),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
          (((B : (a : F) → G →L[ℝ] W) (f' (a, t)) : G →L[ℝ] W) : (a : G) → W) (g (a, t)) ∂μ)
    (-∫ (x : E),
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (y : ℝ) ↦
          (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y)) ∂μ)
⊢ Eq.{u_4 + 1} (α := W)
    (∫ (x : E),
      -@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
          (((B : (a : F) → G →L[ℝ] W) (f' (x, t)) : G →L[ℝ] W) : (a : G) → W) (g (x, t)) ∂μ)
    (-@integral _ _ _ _ Prod.instMeasurableSpace (μ.prod volume) fun (x : E × ℝ) ↦
        (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x))

Tactic:
rw [integral_neg, integral_prod _ hf'g]

Premises used: MeasureTheory.integral_neg, MeasureTheory.integral_prod
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst_11 : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
⊢ ν.prod volume = addHaarScalarFactor (ν.prod volume) μ • μ

Tactic:
have A : ν.prod volume = (addHaarScalarFactor (ν.prod volume) μ) • μ :=
    isAddLeftInvariant_eq_smul _ _
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst_11 : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = addHaarScalarFactor (ν.prod volume) μ • μ
rw :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x))
    (addHaarScalarFactor (ν.prod volume) μ • μ)
⊢ @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (ν.prod volume)

Tactic:
rw [A]
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst_11 : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = addHaarScalarFactor (ν.prod volume) μ • μ
⊢ Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x))
    (addHaarScalarFactor (ν.prod volume) μ • μ)

Tactic:
hf'g.smul_measure_nnreal

Premises used: MeasureTheory.Integrable.smul_measure_nnreal
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst_11 : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = addHaarScalarFactor (ν.prod volume) μ • μ
⊢ Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x))
    (addHaarScalarFactor (ν.prod volume) μ • μ)

Tactic:
exact hf'g.smul_measure_nnreal

Premises used: MeasureTheory.Integrable.smul_measure_nnreal
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst_11 : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = addHaarScalarFactor (ν.prod volume) μ • μ
⊢ @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (ν.prod volume)

Tactic:
have Hf'g : Integrable (fun x ↦ B (f' x) (g x)) (ν.prod volume) := by
    rw [A]; exact hf'g.smul_measure_nnreal
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst_11 : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = addHaarScalarFactor (ν.prod volume) μ • μ
Hf'g :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (ν.prod volume)
rw :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x))
    (addHaarScalarFactor (ν.prod volume) μ • μ)
⊢ @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) (ν.prod volume)

Tactic:
rw [A]
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst_11 : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = addHaarScalarFactor (ν.prod volume) μ • μ
Hf'g :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (ν.prod volume)
⊢ Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x))
    (addHaarScalarFactor (ν.prod volume) μ • μ)

Tactic:
hfg'.smul_measure_nnreal

Premises used: MeasureTheory.Integrable.smul_measure_nnreal
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst_11 : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = addHaarScalarFactor (ν.prod volume) μ • μ
Hf'g :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (ν.prod volume)
⊢ Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x))
    (addHaarScalarFactor (ν.prod volume) μ • μ)

Tactic:
exact hfg'.smul_measure_nnreal

Premises used: MeasureTheory.Integrable.smul_measure_nnreal
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst_11 : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = addHaarScalarFactor (ν.prod volume) μ • μ
Hf'g :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (ν.prod volume)
⊢ @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) (ν.prod volume)

Tactic:
have Hfg' : Integrable (fun x ↦ B (f x) (g' x)) (ν.prod volume) := by
    rw [A]; exact hfg'.smul_measure_nnreal
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst_11 : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = addHaarScalarFactor (ν.prod volume) μ • μ
Hf'g :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (ν.prod volume)
Hfg' :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) (ν.prod volume)
rw :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    (addHaarScalarFactor (ν.prod volume) μ • μ)
⊢ @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) (ν.prod volume)

Tactic:
rw [A]
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst_11 : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = addHaarScalarFactor (ν.prod volume) μ • μ
Hf'g :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (ν.prod volume)
Hfg' :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) (ν.prod volume)
⊢ Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    (addHaarScalarFactor (ν.prod volume) μ • μ)

Tactic:
hfg.smul_measure_nnreal

Premises used: MeasureTheory.Integrable.smul_measure_nnreal
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst_11 : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = addHaarScalarFactor (ν.prod volume) μ • μ
Hf'g :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (ν.prod volume)
Hfg' :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) (ν.prod volume)
⊢ Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    (addHaarScalarFactor (ν.prod volume) μ • μ)

Tactic:
exact hfg.smul_measure_nnreal

Premises used: MeasureTheory.Integrable.smul_measure_nnreal
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
F : Type u_2
G : Type u_3
W : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace ℝ F
inst_4 : NormedAddCommGroup G
inst_5 : NormedSpace ℝ G
inst_6 : NormedAddCommGroup W
inst_7 : NormedSpace ℝ W
inst_8 : MeasurableSpace E
inst_9 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
μ : Measure (E × ℝ)
inst_11 : μ.IsAddHaarMeasure
f f' : E × ℝ → F
g g' : E × ℝ → G
B : F →L[ℝ] G →L[ℝ] W
hf'g :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) μ
hfg' :
  Integrable.{u_4, u_1} (ε := W)
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) μ
hfg :
  Integrable.{u_4, u_1} (ε := W) (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x))
    μ
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x (0, 1)
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x (0, 1)
ν : Measure E := addHaar
A : ν.prod volume = addHaarScalarFactor (ν.prod volume) μ • μ
Hf'g :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x)) (ν.prod volume)
Hfg' :
  @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x)) (ν.prod volume)
⊢ @Integrable.{u_4, u_1} W _ _ _ Prod.instMeasurableSpace
    (fun (x : E × ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g x)) (ν.prod volume)

Tactic:
have Hfg : Integrable (fun x ↦ B (f x) (g x)) (ν.prod volume) := by
    rw [A]; exact hfg.smul_measure_nnreal