awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (hypothesis)
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 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
H :
  Eq.{u_4 + 1} (α := W)
    (∫ (x : E' × ℝ),
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
    (-∫ (x : E' × ℝ),
        (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
          (g ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
⊢ Eq.{u_4 + 1} (α := W) (∫ (x : E), (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x) ∂μ)
    (-∫ (x : E), (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x) ∂μ)
have this₁ : μ = map (⇑L.symm : (a : E' × ℝ) → E) ν
Tactic: have : μ = Measure.map L.symm ν := by
      simp [ν, Measure.map_map L.symm.continuous.measurable L.continuous.measurable]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (hypothesis)
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 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
H :
  Eq.{u_4 + 1} (α := W)
    (∫ (x : E' × ℝ),
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
    (-∫ (x : E' × ℝ),
        (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
          (g ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
this : μ = map (⇑L.symm : (a : E' × ℝ) → E) ν
⊢ Eq.{u_4 + 1} (α := W) (∫ (x : E), (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x) ∂μ)
    (-∫ (x : E), (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x) ∂μ)
have hL₁ : IsClosedEmbedding (X := E' × ℝ) (Y := E) (⇑L.symm : (a : E' × ℝ) → E)
Tactic: have hL : IsClosedEmbedding L.symm := L.symm.toHomeomorph.isClosedEmbedding
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (goal)
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 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
⊢ Eq.{u_4 + 1} (α := W) (∫ (x : E), (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x) ∂μ)
    (-∫ (x : E), (((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x) ∂μ)
have pos : Eq.{u_4 + 1} (α := W)
  (∫ (x : E' × ℝ),
    (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
      (g' ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
  (-∫ (x : E' × ℝ),
      (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
Tactic: suffices H : ∫ (x : E' × ℝ), (B (f (L.symm x))) (g' (L.symm x)) ∂ν =
      -∫ (x : E' × ℝ), (B (f' (L.symm x))) (g (L.symm x)) ∂ν by
    have : μ = Measure.map L.symm ν := by
      simp [ν, Measure.map_map L.symm.continuous.measurable L.continuous.measurable]
    have hL : IsClosedEmbedding L.symm := L.symm.toHomeomorph.isClosedEmbedding
    simpa [this, hL.integral_map] using H
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (hypothesis)
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 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
⊢ Eq.{u_4 + 1} (α := W)
    (∫ (x : E' × ℝ),
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
    (-∫ (x : E' × ℝ),
        (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
          (g ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
have L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
Tactic: have L_emb : MeasurableEmbedding L := L.toHomeomorph.measurableEmbedding
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (goal)
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 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
⊢ Eq.{u_4 + 1} (α := W)
    (∫ (x : E' × ℝ),
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
    (-∫ (x : E' × ℝ),
        (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
          (g ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
have pos : Integrable.{u_4, 0} (ε := W)
  (fun (x : E' × ℝ) ↦
    (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
      (g ((L.symm : (a : E' × ℝ) → E) x)))
  ν
Tactic: apply integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (goal)
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 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
pos :
  Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g ((L.symm : (a : E' × ℝ) → E) x)))
    ν
⊢ Eq.{u_4 + 1} (α := W)
    (∫ (x : E' × ℝ),
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
    (-∫ (x : E' × ℝ),
        (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
          (g ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
have pos₁ : Integrable.{u_4, 0} (ε := W)
  (fun (x : E' × ℝ) ↦
    (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
      (g' ((L.symm : (a : E' × ℝ) → E) x)))
  ν
Tactic: apply integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (goal)
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 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
pos :
  Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g ((L.symm : (a : E' × ℝ) → E) x)))
    ν
pos₁ :
  Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)))
    ν
⊢ Eq.{u_4 + 1} (α := W)
    (∫ (x : E' × ℝ),
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
    (-∫ (x : E' × ℝ),
        (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
          (g ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
have pos₂ : Integrable.{u_4, 0} (ε := W)
  (fun (x : E' × ℝ) ↦
    (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
      (g ((L.symm : (a : E' × ℝ) → E) x)))
  ν
Tactic: apply integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (goal)
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 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
pos :
  Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g ((L.symm : (a : E' × ℝ) → E) x)))
    ν
pos₁ :
  Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)))
    ν
pos₂ :
  Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g ((L.symm : (a : E' × ℝ) → E) x)))
    ν
⊢ Eq.{u_4 + 1} (α := W)
    (∫ (x : E' × ℝ),
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
    (-∫ (x : E' × ℝ),
        (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
          (g ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
have pos₃ : ∀ (x : E' × ℝ),
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_3} (α := G) fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x))
      x →
    HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) (f' ((L.symm : (a : E' × ℝ) → E) x)) x
      (0, 1)
Tactic: apply integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (goal)
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 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
pos :
  Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g ((L.symm : (a : E' × ℝ) → E) x)))
    ν
pos₁ :
  Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)))
    ν
pos₂ :
  Integrable.{u_4, 0} (ε := W)
    (fun (x : E' × ℝ) ↦
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g ((L.symm : (a : E' × ℝ) → E) x)))
    ν
pos₃ :
  ∀ (x : E' × ℝ),
    Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_3} (α := G) fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x))
        x →
      HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) (f' ((L.symm : (a : E' × ℝ) → E) x)) x
        (0, 1)
⊢ Eq.{u_4 + 1} (α := W)
    (∫ (x : E' × ℝ),
      (((B : (a : F) → G →L[ℝ] W) (f ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
        (g' ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
    (-∫ (x : E' × ℝ),
        (((B : (a : F) → G →L[ℝ] W) (f' ((L.symm : (a : E' × ℝ) → E) x)) : G →L[ℝ] W) : (a : G) → W)
          (g ((L.symm : (a : E' × ℝ) → E) x)) ∂ν)
have pos₄ : ∀ (x : E' × ℝ),
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_2} (α := F) fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x))
      x →
    HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) (g' ((L.symm : (a : E' × ℝ) → E) x)) x
      (0, 1)
Tactic: apply integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable_aux2
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (goal)
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 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_3} (α := G) fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) x
⊢ f =
    Function.comp (β := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
have h : ∀ (y : E),
  f y =
    Function.comp (β := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts (hypothesis)
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 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f f' : E → F
g g' : E → G
v : E
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 v
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x v
hW : CompleteSpace W
hv : v ≠ 0
this : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
L : E ≃L[ℝ] E' × ℝ
hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
ν : Measure (E' × ℝ) := map (⇑L : (a : E) → E' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_3} (α := G) fun (x : E' × ℝ) ↦ g ((L.symm : (a : E' × ℝ) → E) x)) x
⊢ HasLineDerivAt ℝ (fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) (f' ((L.symm : (a : E' × ℝ) → E) x)) x (0, 1)
have this₁ : f =
  Function.comp (β := E' × ℝ) (f ∘ (⇑L.symm : (a : E' × ℝ) → E))
    (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
Tactic: have : f = (f ∘ L.symm) ∘ (L : E →ₗ[ℝ] (E' × ℝ)) := by ext y; simp