awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst_3 : Finite ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val : Fintype ι
⊢ ¬LinearIndependent ℝ (Option.elim' φ' f')
have intro : ¬∀ (g : Option ι → ℝ),
    Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 → ∀ (i : Option ι), g i = 0
Tactic: rw [Fintype.linearIndependent_iff]
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst_3 : Finite ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val : Fintype ι
⊢ ¬∀ (g : Option ι → ℝ),
      Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 → ∀ (i : Option ι), g i = 0
have intro : ∃ (g : Option ι → ℝ),
  Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 ∧ ∃ (i : Option ι), g i ≠ 0
Tactic: push Not
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst_3 : Finite ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val : Fintype ι
⊢ ∃ (g : Option ι → ℝ),
    Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 ∧ ∃ (i : Option ι), g i ≠ 0
have intro : ∀ (Λ : ι → ℝ) (Λ₀ : ℝ) (hΛ : (Λ, Λ₀) ≠ 0) (hΛf : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0),
  ∃ (g : Option ι → ℝ),
    Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 ∧ ∃ (i : Option ι), g i ≠ 0
Tactic: rcases hextr.exists_multipliers_of_hasStrictFDerivAt hf' hφ' with ⟨Λ, Λ₀, hΛ, hΛf⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst_3 : Finite ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val : Fintype ι
Λ : ι → ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hΛf : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
⊢ ∃ (g : Option ι → ℝ),
    Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 ∧ ∃ (i : Option ι), g i ≠ 0
have intro : Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, Option.elim' Λ₀ Λ i • Option.elim' φ' f' i) 0
Tactic: refine ⟨Option.elim' Λ₀ Λ, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Calculus.LagrangeMultipliers (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
φ : E → ℝ
x₀ : E
φ' : StrongDual ℝ E
ι : Type u_3
inst_3 : Finite ι
f : ι → E → ℝ
f' : ι → StrongDual ℝ E
hextr : IsLocalExtrOn φ {x : E | ∀ (i : ι), f i x = f i x₀} x₀
hf' : ∀ (i : ι), HasStrictFDerivAt (f i) (f' i) x₀
hφ' : HasStrictFDerivAt φ φ' x₀
val : Fintype ι
Λ : ι → ℝ
Λ₀ : ℝ
hΛ : (Λ, Λ₀) ≠ 0
hΛf : ∑ i : ι, Λ i • f' i + Λ₀ • φ' = 0
intro : Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, Option.elim' Λ₀ Λ i • Option.elim' φ' f' i) 0
⊢ ∃ (g : Option ι → ℝ),
    Eq.{u_1 + 1} (α := StrongDual ℝ E) (∑ i : Option ι, g i • Option.elim' φ' f' i) 0 ∧ ∃ (i : Option ι), g i ≠ 0
have intro₁ : ∃ (i : Option ι), Option.elim' Λ₀ Λ i ≠ 0
Tactic: refine ⟨Option.elim' Λ₀ Λ, ?_, ?_⟩
-- 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 : 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)
⊢ 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)) ∂μ)
    (∫ (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)) ∂μ)
have h : Filter.EventuallyEq.{u_1, u_4} (β := W) (ae μ)
  (fun (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)))
  fun (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))
Tactic: apply integral_congr_ae
-- 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 : 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)
⊢ Filter.EventuallyEq.{u_1, u_4} (β := W) (ae μ)
    (fun (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)))
    fun (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))
have h : ∀ (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),
  Eq.{u_4 + 1} (α := W)
    (@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 _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
        (((B : (a : F) → G →L[ℝ] W) (f' (x, t)) : G →L[ℝ] W) : (a : G) → W) (g (x, t)))
Tactic: filter_upwards [hf'g.prod_right_ae, hfg'.prod_right_ae, hfg.prod_right_ae]
      with x hf'gx hfg'x hfgx
-- 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 : 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
⊢ Eq.{u_4 + 1} (α := W)
    (@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 _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
        (((B : (a : F) → G →L[ℝ] W) (f' (x, t)) : G →L[ℝ] W) : (a : G) → W) (g (x, t)))
have apply : ∀ (x_1 : ℝ),
  Membership.mem (γ := Set ℝ) (tsupport.{0, u_3} (α := G) fun (x_2 : ℝ) ↦ g (x, x_2)) x_1 →
    HasDerivAt (fun (x_2 : ℝ) ↦ f (x, x_2)) (f' (x, x_1)) x_1
Tactic: apply integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable ?_ ?_ hfg'x hf'gx hfgx
-- 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 : 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
apply :
  ∀ (x_1 : ℝ),
    Membership.mem (γ := Set ℝ) (tsupport.{0, u_3} (α := G) fun (x_2 : ℝ) ↦ g (x, x_2)) x_1 →
      HasDerivAt (fun (x_2 : ℝ) ↦ f (x, x_2)) (f' (x, x_1)) x_1
⊢ Eq.{u_4 + 1} (α := W)
    (@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 _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : ℝ) ↦
        (((B : (a : F) → G →L[ℝ] W) (f' (x, t)) : G →L[ℝ] W) : (a : G) → W) (g (x, t)))
have apply₁ : ∀ (x_1 : ℝ),
  Membership.mem (γ := Set ℝ) (tsupport.{0, u_2} (α := F) fun (x_2 : ℝ) ↦ f (x, x_2)) x_1 →
    HasDerivAt (fun (x_2 : ℝ) ↦ g (x, x_2)) (g' (x, x_1)) x_1
Tactic: apply integral_bilinear_hasDerivAt_right_eq_neg_left_of_integrable ?_ ?_ hfg'x hf'gx hfgx
-- 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 : 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
⊢ HasDerivAt (fun (x_1 : ℝ) ↦ f (x, x_1)) (f' (x, t)) t
have this : (x, t) ∈ tsupport g
Tactic: have : (x, t) ∈ tsupport g :=
        tsupport_comp_subset_preimage (f := fun y ↦ (x, y)) g (by fun_prop) ht
-- 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 : 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
⊢ HasDerivAt (fun (x_1 : ℝ) ↦ f (x, x_1)) (f' (x, t)) t
have 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
Tactic: convert! (hf (x, t) this).scomp_of_eq t ((hasDerivAt_id t).add (hasDerivAt_const t (-t)))
        (by 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 : 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
⊢ HasDerivAt (fun (x_1 : ℝ) ↦ f (x, x_1)) (f' (x, t)) t
have h₁ : f' (x, t) = HAdd.hAdd (α := ℝ) 1 0 • f' (x, t)
Tactic: convert! (hf (x, t) this).scomp_of_eq t ((hasDerivAt_id t).add (hasDerivAt_const t (-t)))
        (by simp)
-- 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 : 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
⊢ HasDerivAt (fun (x_1 : ℝ) ↦ g (x, x_1)) (g' (x, t)) t
have this : (x, t) ∈ tsupport f
Tactic: have : (x, t) ∈ tsupport f :=
        tsupport_comp_subset_preimage (f := fun y ↦ (x, y)) f (by fun_prop) ht
-- 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 : 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
⊢ HasDerivAt (fun (x_1 : ℝ) ↦ g (x, x_1)) (g' (x, t)) t
have 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
Tactic: convert!
        (hg (x, t) this).scomp_of_eq t ((hasDerivAt_id t).add (hasDerivAt_const t (-t)))
          (by simp)