awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
obtain :
  ∀ (X : ℂ) (HX2 : IsMaxOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x‖) (sphere z R) X),
    ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B
⊢ ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B

Tactic:
obtain ⟨X, -, HX2⟩ := (isCompact_sphere z R).exists_isMaxOn
    (NormedSpace.sphere_nonempty.2 hR.le) hf.norm

Premises used: Iff.mpr, LT.lt.le, isCompact_sphere, NormedSpace.sphere_nonempty, ContinuousOn.norm, IsCompact.exists_isMaxOn
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
HX2 : IsMaxOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x‖) (sphere z R) X
⊢ ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B

Tactic:
⟨‖V b a‖ * ‖f X‖, ε', hε', H.trans (ball_subset_ball hr.le), fun y v hv ↦ ?_⟩

Premises used: Norm.norm, HMul.hMul, HasSubset.Subset.trans, LT.lt.le, Metric.ball_subset_ball, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
HX2 : IsMaxOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x‖) (sphere z R) X
refine : ∀ (y : ℝ) (v : ℂ) (hv : v ∈ ball x ε'), ‖circleTransformDeriv R z v f y‖ ≤ ‖V b a‖ * ‖f X‖
⊢ ∃ (B : ℝ) (ε : ℝ), 0 < ε ∧ ball x ε ⊆ ball z R ∧ ∀ (t : ℝ), ∀ y ∈ ball x ε, ‖circleTransformDeriv R z y f t‖ ≤ B

Tactic:
refine ⟨‖V b a‖ * ‖f X‖, ε', hε', H.trans (ball_subset_ball hr.le), fun y v hv ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
HX2 : IsMaxOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x‖) (sphere z R) X
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
obtain :
  ∀ (y1 : ℝ) (hy1 : y1 ∈ Ico 0 (2 * π)) (hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1),
    ‖circleTransformDeriv R z v f y‖ ≤ ‖V b a‖ * ‖f X‖
⊢ ‖circleTransformDeriv R z v f y‖ ≤ ‖V b a‖ * ‖f X‖

Tactic:
obtain ⟨y1, hy1, hfun⟩ :=
    Periodic.exists_mem_Ico₀ (circleTransformDeriv_periodic R z v f) Real.two_pi_pos y

Premises used: Real.two_pi_pos, Complex.circleTransformDeriv_periodic, Function.Periodic.exists_mem_Ico₀
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
HX2 : IsMaxOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x‖) (sphere z R) X
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
⊢ y1 ∈ [[0, 2 * π]]

Tactic:
have hy2 : y1 ∈ [[0, 2 * π]] := Icc_subset_uIcc <| Ico_subset_Icc_self hy1
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
HX2 : IsMaxOn (β := ℝ) (fun (x : ℂ) ↦ ‖f x‖) (sphere z R) X
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
⊢ ∀ (x : ℂ), ‖x - z‖ = R → ‖f x‖ ≤ ‖f X‖

Tactic:
simp only [isMaxOn_iff, mem_sphere_iff_norm] at HX2

Premises used: isMaxOn_iff, mem_sphere_iff_norm
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
HX2 : ∀ (x : ℂ), ‖x - z‖ = R → ‖f x‖ ≤ ‖f X‖
⊢ ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (v, y1) ⋯) : ℂ × ℝ)‖ *
      ‖f (circleMap z R y1)‖ ≤
    ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖ *
      ‖f X‖

Tactic:
have := mul_le_mul (hab ⟨⟨v, y1⟩, ⟨ball_subset_closedBall (H hv), hy2⟩⟩)
    (HX2 (circleMap z R y1) (mem_sphere_iff_norm.1 (circleMap_mem_sphere z hR.le y1)))
    (norm_nonneg _) (norm_nonneg _)
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
HX2 : ∀ (x : ℂ), ‖x - z‖ = R → ‖f x‖ ≤ ‖f X‖
this :
  ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (v, y1) ⋯) : ℂ × ℝ)‖ *
      ‖f (circleMap z R y1)‖ ≤
    ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖ *
      ‖f X‖
rw : ‖circleTransformDeriv R z v f y1‖ ≤ ‖V b a‖ * ‖f X‖
⊢ ‖circleTransformDeriv R z v f y‖ ≤ ‖V b a‖ * ‖f X‖

Tactic:
rw [hfun]
-- Module: Mathlib.MeasureTheory.Integral.CircleTransform
Goal:
R : ℝ
hR : 0 < R
z x : ℂ
f : ℂ → ℂ
hx : x ∈ ball z R
hf : ContinuousOn f (sphere z R)
r : ℝ
hr : r < R
hrx : x ∈ ball z r
ε' : ℝ
hε' : ε' > 0
H : ball x ε' ⊆ ball z r
a : ℂ
b : ℝ
ha : (a, b).1 ∈ closedBall z r
hb : (a, b).2 ∈ [[0, 2 * π]]
hab :
  ∀ (y : (↑(closedBall z r ×ˢ [[0, 2 * π]]) : Type)),
    ‖circleTransformBoundingFunction R z (↑y : ℂ × ℝ)‖ ≤
      ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖
V : ℝ → ℂ → ℂ := fun (θ : ℝ) (w : ℂ) ↦ circleTransformDeriv R z w (fun (x : ℂ) ↦ 1) θ
X : ℂ
y : ℝ
v : ℂ
hv : v ∈ ball x ε'
y1 : ℝ
hy1 : y1 ∈ Ico 0 (2 * π)
hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1
hy2 : y1 ∈ [[0, 2 * π]]
HX2 : ∀ (x : ℂ), ‖x - z‖ = R → ‖f x‖ ≤ ‖f X‖
this :
  ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (v, y1) ⋯) : ℂ × ℝ)‖ *
      ‖f (circleMap z R y1)‖ ≤
    ‖circleTransformBoundingFunction R z
          (↑(Subtype.mk (p := fun (x : ℂ × ℝ) ↦ x ∈ closedBall z r ×ˢ [[0, 2 * π]]) (a, b) ⋯) : ℂ × ℝ)‖ *
      ‖f X‖
⊢ ‖circleTransformDeriv R z v f y1‖ ≤ ‖V b a‖ * ‖f X‖

Tactic:
simpa [V, circleTransformBoundingFunction, circleTransformDeriv, mul_assoc] using this

Premises used: mul_assoc, Complex.circleTransformBoundingFunction, Complex.circleTransformDeriv
-- Module: Mathlib.MeasureTheory.Integral.CompactlySupported
Goal:
X : Type u_1
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : OpensMeasurableSpace X
E : Type u_2
inst_3 : NormedAddCommGroup E
f : X →C_c E
μ : Measure X
inst_4 : IsFiniteMeasureOnCompacts μ
⊢ Integrable.{u_2, u_1} (ε := E) (⇑f : (a : X) → E) μ

Tactic:
f.continuous.integrable_of_hasCompactSupport f.hasCompactSupport

Premises used: ContinuousMap.continuous, CompactlySupportedContinuousMap.hasCompactSupport, Continuous.integrable_of_hasCompactSupport, CompactlySupportedContinuousMap.toContinuousMap
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
h : ¬CompleteSpace F
ω : E → E →L[𝕜] F
γ : Path a b
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in γ, ω x) 0

Tactic:
simp [curveIntegral, intervalIntegral, integral, h]

Premises used: curveIntegral, intervalIntegral, MeasureTheory.integral
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
inst_5 : NormedSpace ℝ E
ω : E → E →L[𝕜] F
γ : Path a b
t : ℝ
⊢ curveIntegralFun ω γ t = (ω ((γ.extend : (a : ℝ) → E) t) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I t)

Tactic:
simp +instances only [curveIntegralFun, NormedSpace.restrictScalars_eq]

Premises used: curveIntegralFun, NormedSpace.restrictScalars_eq
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
inst_5 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
⊢ curveIntegral ω γ = ∫ (t : ℝ) in 0..1, curveIntegralFun ω γ t

Tactic:
simp +instances only [curveIntegral, NormedSpace.restrictScalars_eq]

Premises used: curveIntegral, NormedSpace.restrictScalars_eq
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
simp :
  Eq.{u_3 + 1} (α := F)
    (∫ (t : ℝ) in 0..1, (ω ((γ.extend : (a : ℝ) → E) t) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I t))
    (∫ (t : ℝ) in 0..1, (ω ((γ.extend : (a : ℝ) → E) t) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) t))
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in γ, ω x)
    (∫ (t : ℝ) in 0..1, (ω ((γ.extend : (a : ℝ) → E) t) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) t))

Tactic:
simp only [curveIntegral_def, curveIntegralFun_def]

Premises used: curveIntegral_def, curveIntegralFun_def
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
h :
  EventuallyEq.{0, u_3} (β := F) (ae (F := Measure ℝ) (Measure.restrict volume (Ι 0 1)))
    (fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x))
    fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x)
⊢ Eq.{u_3 + 1} (α := F)
    (∫ (t : ℝ) in 0..1, (ω ((γ.extend : (a : ℝ) → E) t) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I t))
    (∫ (t : ℝ) in 0..1, (ω ((γ.extend : (a : ℝ) → E) t) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) t))

Tactic:
apply intervalIntegral.integral_congr_ae_restrict

Premises used: intervalIntegral.integral_congr_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
h :
  EventuallyEq.{0, u_3} (β := F) (ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 1)))
    (fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x))
    fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x)
⊢ EventuallyEq.{0, u_3} (β := F) (ae (F := Measure ℝ) (Measure.restrict volume (Ι 0 1)))
    (fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x))
    fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x)

Tactic:
rw [uIoc_of_le zero_le_one, ← restrict_Ioo_eq_restrict_Ioc]

Premises used: zero_le_one, MeasureTheory.restrict_Ioo_eq_restrict_Ioc, Set.uIoc_of_le
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
⊢ MeasurableSet (α := ℝ) (Ioo 0 1)

Tactic:
measurability
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
h :
  ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x),
    Eq.{u_3 + 1} (α := F)
      ((ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x) : F)
      ((ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x) : F)
⊢ EventuallyEq.{0, u_3} (β := F) (ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 1)))
    (fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x))
    fun (x : ℝ) ↦ (ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x)

Tactic:
filter_upwards [ae_restrict_mem (by measurability)] with x hx

Premises used: MeasureTheory.ae_restrict_mem
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ I ∈ 𝓝 x

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
inst_5 : NormedSpace ℝ E
inst_6 : NormedSpace ℝ F
ω : E → E →L[𝕜] F
γ : Path a b
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
h h₁ :
  Eq.{u_3 + 1} (α := F) ((ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x) : F)
    ((ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x) : F)
⊢ Eq.{u_3 + 1} (α := F) ((ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (derivWithin (⇑γ.extend : (a : ℝ) → E) I x) : F)
    ((ω ((γ.extend : (a : ℝ) → E) x) : (a : E) → F) (deriv (⇑γ.extend : (a : ℝ) → E) x) : F)

Tactic:
rw [derivWithin_of_mem_nhds (by simpa)]

Premises used: derivWithin_of_mem_nhds
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
ω : E → E →L[𝕜] F
a : E
h : ∀ (x : ℝ), curveIntegralFun ω (Path.refl a) x = 0 x
⊢ curveIntegralFun ω (Path.refl a) = 0

Tactic:
ext
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
ω : E → E →L[𝕜] F
a : E
x : ℝ
⊢ curveIntegralFun ω (Path.refl a) x = 0 x

Tactic:
simp [curveIntegralFun, ← Function.const_def]

Premises used: Function.const_def, curveIntegralFun
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
ω : E → E →L[𝕜] F
a : E
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in Path.refl a, ω x) 0

Tactic:
simp [curveIntegral]

Premises used: curveIntegral
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
ω : E → E →L[𝕜] F
a : E
⊢ CurveIntegrable ω (Path.refl a)

Tactic:
simp [CurveIntegrable, Pi.zero_def]

Premises used: Pi.zero_def, CurveIntegrable
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b c d : E
ω : E → E →L[𝕜] F
γ : Path a b
hc : c = a
hd : d = b
h : ∀ (t : ℝ), curveIntegralFun ω (γ.cast hc hd) t = curveIntegralFun ω γ t
⊢ curveIntegralFun ω (γ.cast hc hd) = curveIntegralFun ω γ

Tactic:
ext t
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b c d : E
ω : E → E →L[𝕜] F
γ : Path a b
hc : c = a
hd : d = b
t : ℝ
⊢ curveIntegralFun ω (γ.cast hc hd) t = curveIntegralFun ω γ t

Tactic:
simp only [curveIntegralFun_def', Path.extend_cast]

Premises used: curveIntegralFun_def', Path.extend_cast
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b c d : E
ω : E → E →L[𝕜] F
γ : Path a b
hc : c = a
hd : d = b
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in γ.cast hc hd, ω x) (∫ᶜ (x : E) in γ, ω x)

Tactic:
simp [curveIntegral]

Premises used: curveIntegral
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b c d : E
ω : E → E →L[𝕜] F
γ : Path a b
hc : c = a
hd : d = b
⊢ CurveIntegrable ω (γ.cast hc hd) ↔ CurveIntegrable ω γ

Tactic:
simp [CurveIntegrable]

Premises used: CurveIntegrable
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
t : ℝ
⊢ curveIntegralFun ω γ.symm t = -curveIntegralFun ω γ (1 - t)

Tactic:
simp [curveIntegralFun, γ.extend_symm, derivWithin_comp_const_sub]

Premises used: derivWithin_comp_const_sub, Path.extend_symm, curveIntegralFun
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
⊢ curveIntegralFun ω γ.symm = fun (x : ℝ) ↦ (-curveIntegralFun ω γ) (1 - x)

Tactic:
funext <| curveIntegralFun_symm_apply ω γ

Premises used: curveIntegralFun_symm_apply, funext
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
h : CurveIntegrable ω γ
⊢ CurveIntegrable ω γ.symm

Tactic:
simpa [CurveIntegrable] using (h.comp_sub_left 1).neg.symm

Premises used: IntervalIntegrable.neg, IntervalIntegrable.comp_sub_left, IntervalIntegrable.symm, CurveIntegrable, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
h : CurveIntegrable ω γ.symm
⊢ CurveIntegrable ω γ

Tactic:
simpa using h.symm

Premises used: CurveIntegrable.symm
-- Module: Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
a b : E
ω : E → E →L[𝕜] F
γ : Path a b
⊢ Eq.{u_3 + 1} (α := F) (∫ᶜ (x : E) in γ.symm, ω x) (-∫ᶜ (x : E) in γ, ω x)

Tactic:
simp [curveIntegral, curveIntegralFun_symm]

Premises used: curveIntegral, curveIntegralFun_symm