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)
x : E
hf'gx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
hfg'x :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume
hfgx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (tsupport.{0, u_3} (α := G) fun (x_1 : ℝ) ↦ g (x, x_1)) t
⊢ Continuous[_, instTopologicalSpaceProd] fun (y : ℝ) ↦ (x, y)

Tactic:
fun_prop
-- 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)
x : E
hf'gx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
hfg'x :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume
hfgx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (tsupport.{0, u_3} (α := G) fun (x_1 : ℝ) ↦ g (x, x_1)) t
⊢ (x, t) ∈ tsupport g

Tactic:
have : (x, t) ∈ tsupport g :=
        tsupport_comp_subset_preimage (f := fun y ↦ (x, y)) g (by fun_prop) ht
-- 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)
x : E
hf'gx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
hfg'x :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume
hfgx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (tsupport.{0, u_3} (α := G) fun (x_1 : ℝ) ↦ g (x, x_1)) t
this : (x, t) ∈ tsupport g
⊢ 0 = HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) id (fun (x : ℝ) ↦ -t) t

Tactic:
simp
-- 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)
x : E
hf'gx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
hfg'x :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume
hfgx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (tsupport.{0, u_3} (α := G) fun (x_1 : ℝ) ↦ g (x, x_1)) t
this : (x, t) ∈ tsupport g
h :
  ∀ (x_1 : ℝ),
    f (x, x_1) =
      ((fun (t_1 : ℝ) ↦ f ((x, t) + HSMul.hSMul (β := E × ℝ) t_1 (0, 1))) ∘ HAdd.hAdd (α := ℝ → ℝ) id fun (x : ℝ) ↦ -t)
        x_1
h₁ : f' (x, t) = HAdd.hAdd (α := ℝ) 1 0 • f' (x, t)
⊢ HasDerivAt (fun (x_1 : ℝ) ↦ f (x, x_1)) (f' (x, t)) t

Tactic:
convert! (hf (x, t) this).scomp_of_eq t ((hasDerivAt_id t).add (hasDerivAt_const t (-t)))
        (by simp)

Premises used: HasDerivAt.add, hasDerivAt_const, Prod.mk, hasDerivAt_id, HasDerivAt.scomp_of_eq, Neg.neg
-- 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)
x : E
hf'gx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
hfg'x :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume
hfgx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (tsupport.{0, u_3} (α := G) fun (x_2 : ℝ) ↦ g (x, x_2)) t
this : (x, t) ∈ tsupport g
x_1 : ℝ
⊢ f (x, x_1) =
    ((fun (t_1 : ℝ) ↦ f ((x, t) + HSMul.hSMul (β := E × ℝ) t_1 (0, 1))) ∘ HAdd.hAdd (α := ℝ → ℝ) id fun (x : ℝ) ↦ -t)
      x_1

Tactic:
simp
-- 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)
x : E
hf'gx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
hfg'x :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume
hfgx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (tsupport.{0, u_3} (α := G) fun (x_1 : ℝ) ↦ g (x, x_1)) t
this : (x, t) ∈ tsupport g
⊢ f' (x, t) = HAdd.hAdd (α := ℝ) 1 0 • f' (x, t)

Tactic:
simp
-- 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)
x : E
hf'gx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
hfg'x :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume
hfgx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (tsupport.{0, u_2} (α := F) fun (x_1 : ℝ) ↦ f (x, x_1)) t
⊢ Continuous[_, instTopologicalSpaceProd] fun (y : ℝ) ↦ (x, y)

Tactic:
fun_prop
-- 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)
x : E
hf'gx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
hfg'x :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume
hfgx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (tsupport.{0, u_2} (α := F) fun (x_1 : ℝ) ↦ f (x, x_1)) t
⊢ (x, t) ∈ tsupport f

Tactic:
have : (x, t) ∈ tsupport f :=
        tsupport_comp_subset_preimage (f := fun y ↦ (x, y)) f (by fun_prop) ht
-- 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)
x : E
hf'gx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
hfg'x :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume
hfgx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (tsupport.{0, u_2} (α := F) fun (x_1 : ℝ) ↦ f (x, x_1)) t
this : (x, t) ∈ tsupport f
⊢ 0 = HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) id (fun (x : ℝ) ↦ -t) t

Tactic:
simp
-- 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)
x : E
hf'gx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
hfg'x :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume
hfgx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (tsupport.{0, u_2} (α := F) fun (x_1 : ℝ) ↦ f (x, x_1)) t
this : (x, t) ∈ tsupport f
h :
  ∀ (x_1 : ℝ),
    g (x, x_1) =
      ((fun (t_1 : ℝ) ↦ g ((x, t) + HSMul.hSMul (β := E × ℝ) t_1 (0, 1))) ∘ HAdd.hAdd (α := ℝ → ℝ) id fun (x : ℝ) ↦ -t)
        x_1
h₁ : g' (x, t) = HAdd.hAdd (α := ℝ) 1 0 • g' (x, t)
⊢ HasDerivAt (fun (x_1 : ℝ) ↦ g (x, x_1)) (g' (x, t)) t

Tactic:
convert!
        (hg (x, t) this).scomp_of_eq t ((hasDerivAt_id t).add (hasDerivAt_const t (-t)))
          (by simp)

Premises used: HasDerivAt.add, hasDerivAt_const, Prod.mk, hasDerivAt_id, HasDerivAt.scomp_of_eq, Neg.neg
-- 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)
x : E
hf'gx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
hfg'x :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume
hfgx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (tsupport.{0, u_2} (α := F) fun (x_2 : ℝ) ↦ f (x, x_2)) t
this : (x, t) ∈ tsupport f
x_1 : ℝ
⊢ g (x, x_1) =
    ((fun (t_1 : ℝ) ↦ g ((x, t) + HSMul.hSMul (β := E × ℝ) t_1 (0, 1))) ∘ HAdd.hAdd (α := ℝ → ℝ) id fun (x : ℝ) ↦ -t)
      x_1

Tactic:
simp
-- 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)
x : E
hf'gx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f' (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
hfg'x :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g' (x, y))) volume
hfgx :
  @Integrable.{u_4, 0} W _ _ _ MeasureSpace.toMeasurableSpace
    (fun (y : ℝ) ↦ (((B : (a : F) → G →L[ℝ] W) (f (x, y)) : G →L[ℝ] W) : (a : G) → W) (g (x, y))) volume
t : ℝ
ht : Membership.mem (γ := Set ℝ) (tsupport.{0, u_2} (α := F) fun (x_1 : ℝ) ↦ f (x, x_1)) t
this : (x, t) ∈ tsupport f
⊢ g' (x, t) = HAdd.hAdd (α := ℝ) 1 0 • g' (x, t)

Tactic:
simp