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 : 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
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' × ℝ) μ
L_emb : MeasurableEmbedding (α := E) (β := E' × ℝ) (⇑L : (a : E) → E' × ℝ)
x : E' × ℝ
hx :
  Membership.mem (γ := Set (E' × ℝ)) (tsupport.{0, u_2} (α := F) fun (x : E' × ℝ) ↦ f ((L.symm : (a : E' × ℝ) → E) x)) x
this :
  g =
    Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ)
h2x : Membership.mem (α := E) (tsupport f) ((L.symm : (a : E' × ℝ) → E) x : E)
hg :
  HasLineDerivAt ℝ
    (Function.comp (β := E' × ℝ) (g ∘ (⇑L.symm : (a : E' × ℝ) → E))
      (⇑(↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ))
    (g' ((L.symm : (a : E' × ℝ) → E) x)) ((L.symm : (a : E' × ℝ) → E) x) v
⊢ Eq (α := E' × ℝ) (0, 1) (((↑(↑L : E ≃ₗ[ℝ] E' × ℝ) : E →ₗ[ℝ] E' × ℝ) : (a : E) → E' × ℝ) v)

Tactic:
simp [← hL]
-- 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 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f : E → F
f' : E → E →L[ℝ] F
g : E → G
g' : E → E →L[ℝ] 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 : (a : E) → F) v) : 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 : (a : E) → G) v : G)) μ
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, HasFDerivAt f (f' x) x
hg : ∀ x ∈ tsupport f, HasFDerivAt g (g' x) x
⊢ Eq.{u_4 + 1} (α := W)
    (∫ (x : E), (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) ((g' x : (a : E) → G) v : G) ∂μ)
    (-∫ (x : E), (((B : (a : F) → G →L[ℝ] W) ((f' x : (a : E) → F) v) : G →L[ℝ] W) : (a : G) → W) (g x) ∂μ)

Tactic:
integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable hf'g hfg' hfg
    (hf · · |>.hasLineDerivAt v) (hg · · |>.hasLineDerivAt v)

Premises used: integral_bilinear_hasLineDerivAt_right_eq_neg_left_of_integrable, HasFDerivAt.hasLineDerivAt
-- 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 : BorelSpace E
inst_10 : FiniteDimensional ℝ E
inst_11 : μ.IsAddHaarMeasure
f : E → F
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) ((fderiv ℝ f x : (a : E) → F) v) : 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) ((fderiv ℝ g x : (a : E) → G) v : G)) μ
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, DifferentiableAt ℝ f x
hg : ∀ x ∈ tsupport f, DifferentiableAt ℝ g x
⊢ Eq.{u_4 + 1} (α := W)
    (∫ (x : E), (((B : (a : F) → G →L[ℝ] W) (f x) : G →L[ℝ] W) : (a : G) → W) ((fderiv ℝ g x : (a : E) → G) v : G) ∂μ)
    (-∫ (x : E), (((B : (a : F) → G →L[ℝ] W) ((fderiv ℝ f x : (a : E) → F) v) : G →L[ℝ] W) : (a : G) → W) (g x) ∂μ)

Tactic:
integral_bilinear_hasFDerivAt_right_eq_neg_left_of_integrable hf'g hfg' hfg
    (hf · · |>.hasFDerivAt) (hg · · |>.hasFDerivAt)

Premises used: DifferentiableAt.hasFDerivAt, integral_bilinear_hasFDerivAt_right_eq_neg_left_of_integrable
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
G : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : NormedAddCommGroup G
inst_3 : NormedSpace ℝ G
inst_4 : MeasurableSpace E
μ : Measure E
inst_5 : BorelSpace E
inst_6 : FiniteDimensional ℝ E
inst_7 : μ.IsAddHaarMeasure
𝕜 : Type u_5
inst_8 : NormedField 𝕜
inst_9 : NormedAlgebra ℝ 𝕜
inst_10 : NormedSpace 𝕜 G
inst_11 : IsScalarTower ℝ 𝕜 G
f : E → 𝕜
g : E → G
v : E
hf'g :
  Integrable.{u_3, u_1} (ε := G)
    (fun (x : E) ↦ HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) ((fderiv ℝ f x : (a : E) → 𝕜) v : 𝕜) (g x)) μ
hfg' : Integrable.{u_3, u_1} (ε := G) (fun (x : E) ↦ HSMul.hSMul (β := G) (f x) ((fderiv ℝ g x : (a : E) → G) v : G)) μ
hfg : Integrable.{u_3, u_1} (ε := G) (fun (x : E) ↦ f x • g x) μ
hf : ∀ x ∈ tsupport g, DifferentiableAt ℝ f x
hg : ∀ x ∈ tsupport f, DifferentiableAt ℝ g x
⊢ Eq.{u_3 + 1} (α := G) (∫ (x : E), HSMul.hSMul (β := G) (f x) ((fderiv ℝ g x : (a : E) → G) v : G) ∂μ)
    (-∫ (x : E), HSMul.hSMul.{u_5, u_3, u_3} (α := 𝕜) ((fderiv ℝ f x : (a : E) → 𝕜) v : 𝕜) (g x) ∂μ)

Tactic:
integral_bilinear_fderiv_right_eq_neg_left_of_integrable
    (B := ContinuousLinearMap.lsmul ℝ 𝕜) hf'g hfg' hfg hf hg

Premises used: integral_bilinear_fderiv_right_eq_neg_left_of_integrable
-- Module: Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
μ : Measure E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
inst_5 : μ.IsAddHaarMeasure
𝕜 : Type u_5
inst_6 : NormedField 𝕜
inst_7 : NormedAlgebra ℝ 𝕜
f g : E → 𝕜
v : E
hf'g : Integrable.{u_5, u_1} (ε := 𝕜) (fun (x : E) ↦ HMul.hMul (α := 𝕜) ((fderiv ℝ f x : (a : E) → 𝕜) v : 𝕜) (g x)) μ
hfg' : Integrable.{u_5, u_1} (ε := 𝕜) (fun (x : E) ↦ HMul.hMul (β := 𝕜) (f x) ((fderiv ℝ g x : (a : E) → 𝕜) v : 𝕜)) μ
hfg : Integrable.{u_5, u_1} (ε := 𝕜) (fun (x : E) ↦ f x * g x) μ
hf : ∀ x ∈ tsupport g, DifferentiableAt ℝ f x
hg : ∀ x ∈ tsupport f, DifferentiableAt ℝ g x
⊢ Eq.{u_5 + 1} (α := 𝕜) (∫ (x : E), HMul.hMul (β := 𝕜) (f x) ((fderiv ℝ g x : (a : E) → 𝕜) v : 𝕜) ∂μ)
    (-∫ (x : E), HMul.hMul (α := 𝕜) ((fderiv ℝ f x : (a : E) → 𝕜) v : 𝕜) (g x) ∂μ)

Tactic:
integral_bilinear_fderiv_right_eq_neg_left_of_integrable
    (B := ContinuousLinearMap.mul ℝ 𝕜) hf'g hfg' hfg hf hg

Premises used: integral_bilinear_fderiv_right_eq_neg_left_of_integrable
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
hf : Continuous f
⊢ let this := borel 𝕜;
  BorelSpace 𝕜

Tactic:
borelize 𝕜
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
⊢ Continuous (Function.uncurry g)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
⊢ Continuous (Function.uncurry g)

Tactic:
have hg : Continuous g.uncurry := by fun_prop
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
hg : Continuous (Function.uncurry g)
⊢ MeasurableSet.{u_2} (α := E) {x : E | LineDifferentiableAt 𝕜 f x v}

Tactic:
measurable_prodMk_right (measurableSet_of_differentiableAt_with_param 𝕜 hg)

Premises used: LineDifferentiableAt, Set.Mem, DifferentiableAt, setOf, measurable_prodMk_right, Set.preimage, measurableSet_of_differentiableAt_with_param
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
hg : Continuous (Function.uncurry g)
⊢ MeasurableSet.{u_2} (α := E) {x : E | LineDifferentiableAt 𝕜 f x v}

Tactic:
exact measurable_prodMk_right (measurableSet_of_differentiableAt_with_param 𝕜 hg)

Premises used: measurable_prodMk_right, measurableSet_of_differentiableAt_with_param
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : MeasurableSpace F
inst_10 : BorelSpace F
hf : Continuous f
⊢ let this := borel 𝕜;
  BorelSpace 𝕜

Tactic:
borelize 𝕜
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : MeasurableSpace F
inst_10 : BorelSpace F
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
⊢ Continuous (Function.uncurry g)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : MeasurableSpace F
inst_10 : BorelSpace F
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
⊢ Continuous (Function.uncurry g)

Tactic:
have hg : Continuous g.uncurry := by fun_prop
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : MeasurableSpace F
inst_10 : BorelSpace F
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
hg : Continuous (Function.uncurry g)
⊢ Measurable.{u_2, u_3} (β := F) fun (x : E) ↦ lineDeriv 𝕜 f x v

Tactic:
(measurable_deriv_with_param hg).comp measurable_prodMk_right

Premises used: measurable_deriv_with_param, Measurable.comp, deriv, measurable_prodMk_right, lineDeriv
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : MeasurableSpace F
inst_10 : BorelSpace F
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
hg : Continuous (Function.uncurry g)
⊢ Measurable.{u_2, u_3} (β := F) fun (x : E) ↦ lineDeriv 𝕜 f x v

Tactic:
exact (measurable_deriv_with_param hg).comp measurable_prodMk_right

Premises used: measurable_deriv_with_param, Measurable.comp, measurable_prodMk_right
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : SecondCountableTopologyEither E F
hf : Continuous f
⊢ let this := borel 𝕜;
  BorelSpace 𝕜

Tactic:
borelize 𝕜
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : SecondCountableTopologyEither E F
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
⊢ Continuous (Function.uncurry g)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : SecondCountableTopologyEither E F
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
⊢ Continuous (Function.uncurry g)

Tactic:
have hg : Continuous g.uncurry := by fun_prop
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : SecondCountableTopologyEither E F
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
hg : Continuous (Function.uncurry g)
⊢ StronglyMeasurable.{u_2, u_3} (β := F) fun (x : E) ↦ lineDeriv 𝕜 f x v

Tactic:
(stronglyMeasurable_deriv_with_param hg).comp_measurable measurable_prodMk_right

Premises used: deriv, measurable_prodMk_right, MeasureTheory.StronglyMeasurable.comp_measurable, stronglyMeasurable_deriv_with_param, lineDeriv
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : SecondCountableTopologyEither E F
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E → 𝕜 → F := fun (x : E) (t : 𝕜) ↦ f (x + t • v)
hg : Continuous (Function.uncurry g)
⊢ StronglyMeasurable.{u_2, u_3} (β := F) fun (x : E) ↦ lineDeriv 𝕜 f x v

Tactic:
exact (stronglyMeasurable_deriv_with_param hg).comp_measurable measurable_prodMk_right

Premises used: measurable_prodMk_right, MeasureTheory.StronglyMeasurable.comp_measurable, stronglyMeasurable_deriv_with_param
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : MeasurableSpace F
inst_10 : BorelSpace F
hf : Continuous f
μ : Measure E
⊢ AEMeasurable.{u_2, u_3} (β := F) (fun (x : E) ↦ lineDeriv 𝕜 f x v) μ

Tactic:
(measurable_lineDeriv hf).aemeasurable

Premises used: measurable_lineDeriv, Measurable.aemeasurable
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
v : E
inst_9 : SecondCountableTopologyEither E F
hf : Continuous f
μ : Measure E
⊢ AEStronglyMeasurable.{u_2, u_3} (β := F) (fun (x : E) ↦ lineDeriv 𝕜 f x v) μ

Tactic:
(stronglyMeasurable_lineDeriv hf).aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, stronglyMeasurable_lineDeriv
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
hf : Continuous f
⊢ let this := borel 𝕜;
  BorelSpace 𝕜

Tactic:
borelize 𝕜
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun (p : E × E) (t : 𝕜) ↦ f (p.1 + t • p.2)
⊢ Continuous (Function.uncurry g)

Tactic:
have : Continuous g.uncurry :=
    hf.comp <| (continuous_fst.comp continuous_fst).add
    <| continuous_snd.smul (continuous_snd.comp continuous_fst)
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
hf : Continuous f
this_1 : MeasurableSpace 𝕜 := borel 𝕜
this_2 : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun (p : E × E) (t : 𝕜) ↦ f (p.1 + t • p.2)
this : Continuous (Function.uncurry g)
⊢ MeasurableSet (α := Prod.{u_2, u_1} (E × E) 𝕜) {q : Prod.{u_2, u_1} (E × E) 𝕜 | DifferentiableAt 𝕜 (g q.1) q.2}

Tactic:
have M_meas : MeasurableSet {q : (E × E) × 𝕜 | DifferentiableAt 𝕜 (g q.1) q.2} :=
    measurableSet_of_differentiableAt_with_param 𝕜 this
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
hf : Continuous f
this_1 : MeasurableSpace 𝕜 := borel 𝕜
this_2 : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun (p : E × E) (t : 𝕜) ↦ f (p.1 + t • p.2)
this : Continuous (Function.uncurry g)
M_meas : MeasurableSet (α := Prod.{u_2, u_1} (E × E) 𝕜) {q : Prod.{u_2, u_1} (E × E) 𝕜 | DifferentiableAt 𝕜 (g q.1) q.2}
⊢ MeasurableSet.{u_2} (α := E × E) {p : E × E | LineDifferentiableAt 𝕜 f p.1 p.2}

Tactic:
measurable_prodMk_right M_meas

Premises used: LineDifferentiableAt, Set.Mem, DifferentiableAt, setOf, measurable_prodMk_right, Set.preimage
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
hf : Continuous f
this_1 : MeasurableSpace 𝕜 := borel 𝕜
this_2 : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun (p : E × E) (t : 𝕜) ↦ f (p.1 + t • p.2)
this : Continuous (Function.uncurry g)
M_meas : MeasurableSet (α := Prod.{u_2, u_1} (E × E) 𝕜) {q : Prod.{u_2, u_1} (E × E) 𝕜 | DifferentiableAt 𝕜 (g q.1) q.2}
⊢ MeasurableSet.{u_2} (α := E × E) {p : E × E | LineDifferentiableAt 𝕜 f p.1 p.2}

Tactic:
exact measurable_prodMk_right M_meas

Premises used: measurable_prodMk_right
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
inst_10 : MeasurableSpace F
inst_11 : BorelSpace F
hf : Continuous f
⊢ let this := borel 𝕜;
  BorelSpace 𝕜

Tactic:
borelize 𝕜
-- Module: Mathlib.Analysis.Calculus.LineDeriv.Measurable
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
inst_1 : LocallyCompactSpace 𝕜
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : MeasurableSpace E
inst_5 : OpensMeasurableSpace E
F : Type u_3
inst_6 : NormedAddCommGroup F
inst_7 : NormedSpace 𝕜 F
inst_8 : CompleteSpace F
f : E → F
inst_9 : SecondCountableTopology E
inst_10 : MeasurableSpace F
inst_11 : BorelSpace F
hf : Continuous f
this : MeasurableSpace 𝕜 := borel 𝕜
this_1 : BorelSpace 𝕜
g : E × E → 𝕜 → F := fun (p : E × E) (t : 𝕜) ↦ f (p.1 + t • p.2)
⊢ Continuous (Function.uncurry g)

Tactic:
have : Continuous g.uncurry :=
    hf.comp <| (continuous_fst.comp continuous_fst).add
    <| continuous_snd.smul (continuous_snd.comp continuous_fst)