ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
⊢ (∫ (y : ℝ) in a..b, f' y) = fb - fa
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
⊢ (∫ (y : ℝ) in a..b, f' y) = fb - fa
set F : ℝ → E := update (update f a fa) b fb
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
⊢ (∫ (y : ℝ) in a..b, f' y) = fb - fa
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
⊢ (∫ (y : ℝ) in a..b, f' y) = fb - fa
have Fderiv : ∀ x ∈ Ioo a b, HasDerivAt F (f' x) x := by
  refine' fun x hx => (hderiv x hx).congr_of_eventuallyEq _
  filter_upwards [Ioo_mem_nhds hx.1 hx.2] with _ hy; simp only
  rw [update_noteq hy.2.ne, update_noteq hy.1.ne']
no goals
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
hcont : ContinuousOn F (Icc a b)
⊢ (∫ (y : ℝ) in a..b, f' y) = fb - fa
simpa [hab.ne, hab.ne'] using integral_eq_sub_of_hasDerivAt_of_le hab.le hcont Fderiv hint
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
x : ℝ
hx : x ∈ Ioo a b
⊢ F =ᶠ[𝓝 x] f
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
⊢ ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
refine' fun x hx => (hderiv x hx).congr_of_eventuallyEq _
case h
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
x : ℝ
hx : x ∈ Ioo a b
a✝ : ℝ
hy : a✝ ∈ Ioo a b
⊢ update (update f a fa) b fb a✝ = f a✝
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
x : ℝ
hx : x ∈ Ioo a b
⊢ F =ᶠ[𝓝 x] f
filter_upwards [Ioo_mem_nhds hx.1 hx.2] with _ hy
case h
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
x : ℝ
hx : x ∈ Ioo a b
a✝ : ℝ
hy : a✝ ∈ Ioo a b
⊢ update (update f a fa) b fb a✝ = f a✝
case h
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
x : ℝ
hx : x ∈ Ioo a b
a✝ : ℝ
hy : a✝ ∈ Ioo a b
⊢ update (update f a fa) b fb a✝ = f a✝
simp only
no goals
case h
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
x : ℝ
hx : x ∈ Ioo a b
a✝ : ℝ
hy : a✝ ∈ Ioo a b
⊢ update (update f a fa) b fb a✝ = f a✝
rw [update_noteq hy.2.ne, update_noteq hy.1.ne']
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
⊢ (ContinuousOn f (Ioo a b) ∧ (a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa))) ∧
    (b ∈ Icc a b → Tendsto (update f a fa) (𝓝[Ico a b] b) (𝓝 fb))
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
⊢ ContinuousOn F (Icc a b)
rw [continuousOn_update_iff, continuousOn_update_iff, Icc_diff_right, Ico_diff_left]
case refine'_1
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
⊢ a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa)

case refine'_2
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
⊢ b ∈ Icc a b → Tendsto (update f a fa) (𝓝[Ico a b] b) (𝓝 fb)
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
⊢ (ContinuousOn f (Ioo a b) ∧ (a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa))) ∧
    (b ∈ Icc a b → Tendsto (update f a fa) (𝓝[Ico a b] b) (𝓝 fb))
refine' ⟨⟨fun z hz => (hderiv z hz).continuousAt.continuousWithinAt, _⟩, _⟩
no goals
case refine'_1
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
⊢ a ∈ Ico a b → Tendsto f (𝓝[Ioo a b] a) (𝓝 fa)
exact fun _ => ha.mono_left (nhdsWithin_mono _ Ioo_subset_Ioi_self)
case refine'_2
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
⊢ Tendsto (update f a fa) (𝓝[Ico a b] b) (𝓝 fb)
case refine'_2
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
⊢ b ∈ Icc a b → Tendsto (update f a fa) (𝓝[Ico a b] b) (𝓝 fb)
rintro -
case refine'_2
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
⊢ f =ᶠ[𝓝[Iio b] b] update f a fa
case refine'_2
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
⊢ Tendsto (update f a fa) (𝓝[Ico a b] b) (𝓝 fb)
refine' (hb.congr' _).mono_left (nhdsWithin_mono _ Ico_subset_Iio_self)
no goals
case refine'_2
ι : Type ?u.1849419
𝕜 : Type ?u.1849422
E : Type u_1
F✝ : Type ?u.1849428
A : Type ?u.1849431
inst✝² : NormedAddCommGroup E
inst✝¹ : CompleteSpace E
inst✝ : NormedSpace ℝ E
f✝ : ℝ → E
g' g φ : ℝ → ℝ
f f' : ℝ → E
a b : ℝ
hab : a < b
fa fb : E
hderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hint : IntervalIntegrable f' volume a b
ha : Tendsto f (𝓝[Ioi a] a) (𝓝 fa)
hb : Tendsto f (𝓝[Iio b] b) (𝓝 fb)
F : ℝ → E := update (update f a fa) b fb
Fderiv : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt F (f' x) x
⊢ f =ᶠ[𝓝[Iio b] b] update f a fa
filter_upwards [Ioo_mem_nhdsWithin_Iio (right_mem_Ioc.2 hab)] with _ hz using
  (update_noteq hz.1.ne' _ _).symm