awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ 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 : ∀ (hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x 0) (hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x 0),
  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) ∂μ)
Tactic: rcases eq_or_ne v 0 with rfl | hv
Cleared hypotheses: v, hf, hg
-- 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
pos :
  ∀ (hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x 0) (hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x 0),
    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) ∂μ)
⊢ 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₁ : ∀ (hv : v ≠ 0),
  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) ∂μ)
Tactic: rcases eq_or_ne v 0 with rfl | hv
-- 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
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)) μ
hW : CompleteSpace W
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x 0
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x 0
x : E
⊢ Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x) : W) (0 : W)
have pos : ∀ (hx : x ∈ tsupport g),
  Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x) : W) (0 : W)
Tactic: by_cases hx : x ∈ tsupport g
-- 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
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)) μ
hW : CompleteSpace W
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x 0
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x 0
x : E
pos :
  ∀ (hx : x ∈ tsupport g),
    Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x) : W) (0 : W)
⊢ Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x) : W) (0 : W)
have neg : ∀ (hx : x ∉ tsupport g),
  Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x) : W) (0 : W)
Tactic: by_cases hx : x ∈ tsupport g
-- 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
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)) μ
hW : CompleteSpace W
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x 0
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x 0
⊢ 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 Hf' : ∀ (x : E), Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x) : W) (0 : W)
Tactic: have Hf' x : B (f' x) (g x) = 0 := by
      by_cases hx : x ∈ tsupport g
      · simp [(hasLineDerivAt_zero (f := f) (x := x)).lineDeriv, (hf x hx).lineDeriv.symm]
      · simp [image_eq_zero_of_notMem_tsupport hx]
-- 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
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)) μ
hW : CompleteSpace W
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x 0
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x 0
Hf' :
  ∀ (x : E), Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x) : W) (0 : W)
x : E
⊢ Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x) : W) (0 : W)
have pos : ∀ (hx : x ∈ tsupport f),
  Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x) : W) (0 : W)
Tactic: by_cases hx : x ∈ tsupport f
-- 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
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)) μ
hW : CompleteSpace W
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x 0
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x 0
Hf' :
  ∀ (x : E), Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x) : W) (0 : W)
x : E
pos :
  ∀ (hx : x ∈ tsupport f),
    Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x) : W) (0 : W)
⊢ Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x) : W) (0 : W)
have neg : ∀ (hx : x ∉ tsupport f),
  Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x) : W) (0 : W)
Tactic: by_cases hx : x ∈ tsupport f
-- 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
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)) μ
hW : CompleteSpace W
hf : ∀ x ∈ tsupport g, HasLineDerivAt ℝ f (f' x) x 0
hg : ∀ x ∈ tsupport f, HasLineDerivAt ℝ g (g' x) x 0
Hf' :
  ∀ (x : E), Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f' x) : G →L[ℝ] W) : (a : G) → W) (g x) : W) (0 : W)
⊢ 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 Hg' : ∀ (x : E), Eq.{u_4 + 1} (α := W) ((((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) (g' x) : W) (0 : W)
Tactic: have Hg' x : B (f x) (g' x) = 0 := by
      by_cases hx : x ∈ tsupport f
      · simp [(hasLineDerivAt_zero (f := g) (x := x)).lineDeriv, (hg x hx).lineDeriv.symm]
      · simp [image_eq_zero_of_notMem_tsupport hx]
-- 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
⊢ 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 : Nontrivial E
Tactic: have : Nontrivial E := nontrivial_iff.2 ⟨v, 0, hv⟩
-- 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' × ℝ), Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
have this₁ : finrank ℝ (E' × ℝ) = n
Tactic: have : finrank ℝ (E' × ℝ) = n := by simpa [this, E'] using Nat.sub_add_cancel finrank_pos
-- 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_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
this : finrank ℝ (E' × ℝ) = n
⊢ ∃ (L : E ≃L[ℝ] E' × ℝ), Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
have have : ∀ (L₀ : E ≃L[ℝ] E' × ℝ), ∃ (L : E ≃L[ℝ] E' × ℝ), Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
Tactic: have L₀ : E ≃L[ℝ] (E' × ℝ) := (ContinuousLinearEquiv.ofFinrankEq this).symm
-- 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_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
this : finrank ℝ (E' × ℝ) = n
L₀ : E ≃L[ℝ] E' × ℝ
⊢ ∃ (M : (E' × ℝ) ≃L[ℝ] E' × ℝ),
    Eq (α := E' × ℝ) ((M : (a : E' × ℝ) → E' × ℝ) ((L₀ : (a : E) → E' × ℝ) v : E' × ℝ) : E' × ℝ) ((0, 1) : E' × ℝ)
have hx : Ne (α := E' × ℝ) ((L₀ : (a : E) → E' × ℝ) v : E' × ℝ) (0 : E' × ℝ)
Tactic: apply SeparatingDual.exists_continuousLinearEquiv_apply_eq
-- 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_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
this : finrank ℝ (E' × ℝ) = n
L₀ : E ≃L[ℝ] E' × ℝ
hx : Ne (α := E' × ℝ) ((L₀ : (a : E) → E' × ℝ) v : E' × ℝ) (0 : E' × ℝ)
⊢ ∃ (M : (E' × ℝ) ≃L[ℝ] E' × ℝ),
    Eq (α := E' × ℝ) ((M : (a : E' × ℝ) → E' × ℝ) ((L₀ : (a : E) → E' × ℝ) v : E' × ℝ) : E' × ℝ) ((0, 1) : E' × ℝ)
have hy : Ne (α := E' × ℝ) (0, 1) 0
Tactic: apply SeparatingDual.exists_continuousLinearEquiv_apply_eq
-- 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_1 : Nontrivial E
n : ℕ := finrank ℝ E
E' : Type := Fin (n - 1) → ℝ
this : finrank ℝ (E' × ℝ) = n
L₀ : E ≃L[ℝ] E' × ℝ
⊢ ∃ (L : E ≃L[ℝ] E' × ℝ), Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
have obtain : ∀ (M : (E' × ℝ) ≃L[ℝ] E' × ℝ)
  (hM : Eq (α := E' × ℝ) ((M : (a : E' × ℝ) → E' × ℝ) ((L₀ : (a : E) → E' × ℝ) v : E' × ℝ) : E' × ℝ) ((0, 1) : E' × ℝ)),
  ∃ (L : E ≃L[ℝ] E' × ℝ), Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : E' × ℝ)
Tactic: obtain ⟨M, hM⟩ : ∃ M : (E' × ℝ) ≃L[ℝ] (E' × ℝ), M (L₀ v) = (0, 1) := by
      apply SeparatingDual.exists_continuousLinearEquiv_apply_eq
      · simpa using hv
      · simp
-- 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) → ℝ
⊢ 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 : ∀ (L : E ≃L[ℝ] E' × ℝ) (hL : Eq (α := E' × ℝ) ((L : (a : E) → E' × ℝ) v : E' × ℝ) ((0, 1) : 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) ∂μ)
Tactic: obtain ⟨L, hL⟩ : ∃ L : E ≃L[ℝ] (E' × ℝ), L v = (0, 1) := by
    have : finrank ℝ (E' × ℝ) = n := by simpa [this, E'] using Nat.sub_add_cancel finrank_pos
    have L₀ : E ≃L[ℝ] (E' × ℝ) := (ContinuousLinearEquiv.ofFinrankEq this).symm
    obtain ⟨M, hM⟩ : ∃ M : (E' × ℝ) ≃L[ℝ] (E' × ℝ), M (L₀ v) = (0, 1) := by
      apply SeparatingDual.exists_continuousLinearEquiv_apply_eq
      · simpa using hv
      · simp
    exact ⟨L₀.trans M, by simp [hM]⟩