internlm/Lean-Github huggingface dataset:
Theorem: ContDiffOn.integral_eq_sub'
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a < b
⊢ ∫ (y : ℝ) in a..b, derivWithin f (Icc a b) y = f b - f a
Tactic:
apply integral_eq_sub_of_hasDerivAt_of_le hab.le h.continuousOn
Proof state after:
case hderiv
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a < b
⊢ ∀ x ∈ Ioo a b, HasDerivAt f (derivWithin f (Icc a b) x) x

case hint
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a < b
⊢ IntervalIntegrable (fun y => derivWithin f (Icc a b) y) volume a b
Theorem: ContDiffOn.integral_eq_sub'
Proof state before:
case hderiv
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a < b
⊢ ∀ x ∈ Ioo a b, HasDerivAt f (derivWithin f (Icc a b) x) x
Tactic:
intro t ht
Proof state after:
case hderiv
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a < b
t : ℝ
ht : t ∈ Ioo a b
⊢ HasDerivAt f (derivWithin f (Icc a b) t) t
Theorem: ContDiffOn.integral_eq_sub'
Proof state before:
case hderiv
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a < b
t : ℝ
ht : t ∈ Ioo a b
⊢ HasDerivAt f (derivWithin f (Icc a b) t) t
Tactic:
apply ((h.differentiableOn le_rfl) t (Ioo_subset_Icc_self ht)).hasDerivWithinAt.hasDerivAt
Proof state after:
case hderiv
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a < b
t : ℝ
ht : t ∈ Ioo a b
⊢ Icc a b ∈ 𝓝 t
Theorem: ContDiffOn.integral_eq_sub'
Proof state before:
case hderiv
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a < b
t : ℝ
ht : t ∈ Ioo a b
⊢ Icc a b ∈ 𝓝 t
Tactic:
exact Icc_mem_nhds ht.1 ht.2
Proof state after:
no goals
Theorem: ContDiffOn.integral_eq_sub'
Proof state before:
case hint
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a < b
⊢ IntervalIntegrable (fun y => derivWithin f (Icc a b) y) volume a b
Tactic:
apply ContinuousOn.intervalIntegrable_of_Icc hab.le
Proof state after:
case hint
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a < b
⊢ ContinuousOn (fun y => derivWithin f (Icc a b) y) (Icc a b)
Theorem: ContDiffOn.integral_eq_sub'
Proof state before:
case hint
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a < b
⊢ ContinuousOn (fun y => derivWithin f (Icc a b) y) (Icc a b)
Tactic:
exact h.continuousOn_derivWithin (uniqueDiffOn_Icc hab) le_rfl
Proof state after:
no goals
Theorem: ContDiffOn.integral_eq_sub
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (y : ℝ) in a..b, derivWithin f (Icc a b) y = f b - f a
Tactic:
cases lt_or_eq_of_le hab
Proof state after:
case inl
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h✝ : a < b
⊢ ∫ (y : ℝ) in a..b, derivWithin f (Icc a b) y = f b - f a

case inr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
h✝ : a = b
⊢ ∫ (y : ℝ) in a..b, derivWithin f (Icc a b) y = f b - f a
Theorem: ContDiffOn.integral_eq_sub
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab✝ : a ≤ b
hab : a < b
⊢ ∫ (y : ℝ) in a..b, derivWithin f (Icc a b) y = f b - f a
Tactic:
case inl hab => exact h.integral_eq_sub' hab
Proof state after:
no goals
Theorem: ContDiffOn.integral_eq_sub
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab✝ : a ≤ b
hab : a < b
⊢ ∫ (y : ℝ) in a..b, derivWithin f (Icc a b) y = f b - f a
Tactic:
exact h.integral_eq_sub' hab
Proof state after:
no goals
Theorem: ContDiffOn.integral_eq_sub
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab✝ : a ≤ b
hab : a = b
⊢ ∫ (y : ℝ) in a..b, derivWithin f (Icc a b) y = f b - f a
Tactic:
case inr hab => simp [hab]
Proof state after:
no goals
Theorem: ContDiffOn.integral_eq_sub
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab✝ : a ≤ b
hab : a = b
⊢ ∫ (y : ℝ) in a..b, derivWithin f (Icc a b) y = f b - f a
Tactic:
simp [hab]
Proof state after:
no goals
Theorem: ContDiffOn.integral_derivWithin_smul_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
hg : ContDiffOn ℝ 1 g (uIcc a b)
hf : ContinuousOn f (g '' uIcc a b)
⊢ ∫ (x : ℝ) in a..b, derivWithin g (uIcc a b) x • (f ∘ g) x = ∫ (x : ℝ) in g a..g b, f x
Tactic:
refine integral_comp_smul_deriv'' hg.continuousOn (λ t ht => ?_) (hg.continuousOn_derivWithin'' le_rfl) hf
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
hg : ContDiffOn ℝ 1 g (uIcc a b)
hf : ContinuousOn f (g '' uIcc a b)
t : ℝ
ht : t ∈ Ioo (min a b) (max a b)
⊢ HasDerivWithinAt g (derivWithin g (uIcc a b) t) (Ioi t) t
Theorem: ContDiffOn.integral_derivWithin_smul_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
hg : ContDiffOn ℝ 1 g (uIcc a b)
hf : ContinuousOn f (g '' uIcc a b)
t : ℝ
ht : t ∈ Ioo (min a b) (max a b)
⊢ HasDerivWithinAt g (derivWithin g (uIcc a b) t) (Ioi t) t
Tactic:
apply (hg.differentiableOn le_rfl t (uIoo_subset_uIcc ht)).hasDerivWithinAt.mono_of_mem
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
hg : ContDiffOn ℝ 1 g (uIcc a b)
hf : ContinuousOn f (g '' uIcc a b)
t : ℝ
ht : t ∈ Ioo (min a b) (max a b)
⊢ uIcc a b ∈ 𝓝[>] t
Theorem: ContDiffOn.integral_derivWithin_smul_comp
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
hg : ContDiffOn ℝ 1 g (uIcc a b)
hf : ContinuousOn f (g '' uIcc a b)
t : ℝ
ht : t ∈ Ioo (min a b) (max a b)
⊢ uIcc a b ∈ 𝓝[>] t
Tactic:
exact uIcc_mem_nhds_within ht
Proof state after:
no goals
Theorem: ContDiffOn.integral_eq_sub'''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
Tactic:
convert h.integral_eq_sub hab using 1
Proof state after:
case h.e'_2
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (y : ℝ) in a..b, deriv f y = ∫ (y : ℝ) in a..b, derivWithin f (Icc a b) y
Theorem: ContDiffOn.integral_eq_sub'''
Proof state before:
case h.e'_2
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ ∫ (y : ℝ) in a..b, deriv f y = ∫ (y : ℝ) in a..b, derivWithin f (Icc a b) y
Tactic:
apply integral_congr_uIoo
Proof state after:
case h.e'_2.h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ EqOn (fun t => deriv f t) (fun t => derivWithin f (Icc a b) t) (uIoo a b)
Theorem: ContDiffOn.integral_eq_sub'''
Proof state before:
case h.e'_2.h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
⊢ EqOn (fun t => deriv f t) (fun t => derivWithin f (Icc a b) t) (uIoo a b)
Tactic:
intro t ht
Proof state after:
case h.e'_2.h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
t : ℝ
ht : t ∈ uIoo a b
⊢ (fun t => deriv f t) t = (fun t => derivWithin f (Icc a b) t) t
Theorem: ContDiffOn.integral_eq_sub'''
Proof state before:
case h.e'_2.h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
t : ℝ
ht : t ∈ uIoo a b
⊢ (fun t => deriv f t) t = (fun t => derivWithin f (Icc a b) t) t
Tactic:
convert (derivWithin_of_mem_uIoo ht).symm using 3
Proof state after:
case h.e'_3.h.e.h.e'_7
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
t : ℝ
ht : t ∈ uIoo a b
⊢ Icc a b = uIcc a b
Theorem: ContDiffOn.integral_eq_sub'''
Proof state before:
case h.e'_3.h.e.h.e'_7
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
t : ℝ
ht : t ∈ uIoo a b
⊢ Icc a b = uIcc a b
Tactic:
simp [uIcc, hab]
Proof state after:
no goals
Theorem: ContDiffOn.integral_eq_sub_u
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (uIcc a b)
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
Tactic:
cases le_total a b <;> simp only [uIcc_of_le, uIcc_of_ge, *] at h
Proof state after:
case inl
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h✝ : a ≤ b
h : ContDiffOn ℝ 1 f (Icc a b)
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a

case inr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h✝ : b ≤ a
h : ContDiffOn ℝ 1 f (Icc b a)
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
Theorem: ContDiffOn.integral_eq_sub_u
Proof state before:
case inl
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h✝ : a ≤ b
h : ContDiffOn ℝ 1 f (Icc a b)
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
Tactic:
simp [integral_eq_sub''', *]
Proof state after:
no goals
Theorem: ContDiffOn.integral_eq_sub_u
Proof state before:
case inr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h✝ : b ≤ a
h : ContDiffOn ℝ 1 f (Icc b a)
⊢ ∫ (y : ℝ) in a..b, deriv f y = f b - f a
Tactic:
simp [integral_symm b a, integral_eq_sub''', *]
Proof state after:
no goals
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
⊢ ∫ (y : ℝ) in a..t, derivWithin f (Icc a b) y = f t - f a
Tactic:
have l1 : Icc a t ⊆ Icc a b := Icc_subset_Icc_right ht.2
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
⊢ ∫ (y : ℝ) in a..t, derivWithin f (Icc a b) y = f t - f a
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
⊢ ∫ (y : ℝ) in a..t, derivWithin f (Icc a b) y = f t - f a
Tactic:
have l2 := (h.mono l1).integral_eq_sub''' ht.1
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
⊢ ∫ (y : ℝ) in a..t, derivWithin f (Icc a b) y = f t - f a
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
⊢ ∫ (y : ℝ) in a..t, derivWithin f (Icc a b) y = f t - f a
Tactic:
rw [← l2]
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
⊢ ∫ (y : ℝ) in a..t, derivWithin f (Icc a b) y = ∫ (y : ℝ) in a..t, deriv f y
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
⊢ ∫ (y : ℝ) in a..t, derivWithin f (Icc a b) y = ∫ (y : ℝ) in a..t, deriv f y
Tactic:
apply integral_congr_uIoo
Proof state after:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
⊢ EqOn (fun t => derivWithin f (Icc a b) t) (fun t => deriv f t) (uIoo a t)
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
⊢ EqOn (fun t => derivWithin f (Icc a b) t) (fun t => deriv f t) (uIoo a t)
Tactic:
intro u hu
Proof state after:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : u ∈ uIoo a t
⊢ (fun t => derivWithin f (Icc a b) t) u = (fun t => deriv f t) u
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : u ∈ uIoo a t
⊢ (fun t => derivWithin f (Icc a b) t) u = (fun t => deriv f t) u
Tactic:
simp
Proof state after:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : u ∈ uIoo a t
⊢ derivWithin f (Icc a b) u = deriv f u
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
case h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : u ∈ uIoo a t
l3 : u ∈ uIoo a b
⊢ derivWithin f (Icc a b) u = deriv f u
Tactic:
convert (derivWithin_of_mem_uIoo l3) using 2
Proof state after:
case h.e'_2.h.e'_7
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : u ∈ uIoo a t
l3 : u ∈ uIoo a b
⊢ Icc a b = uIcc a b
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
case h.e'_2.h.e'_7
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : u ∈ uIoo a t
l3 : u ∈ uIoo a b
⊢ Icc a b = uIcc a b
Tactic:
simp [uIcc, hab]
Proof state after:
no goals
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : u ∈ uIoo a t
⊢ u ∈ uIoo a b
Tactic:
rw [uIoo_eq_uIoc_sdiff_ends]
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : u ∈ uIoo a t
⊢ u ∈ Ι a b \ {a, b}
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : u ∈ uIoo a t
⊢ u ∈ Ι a b \ {a, b}
Tactic:
simp [uIoo_eq_uIoc_sdiff_ends, mem_uIoc] at hu
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = t)
⊢ u ∈ Ι a b \ {a, b}
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = t)
⊢ u ∈ Ι a b \ {a, b}
Tactic:
cases hu.1
Proof state after:
case inl
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = t)
h✝ : a < u ∧ u ≤ t
⊢ u ∈ Ι a b \ {a, b}

case inr
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = t)
h✝ : t < u ∧ u ≤ a
⊢ u ∈ Ι a b \ {a, b}
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = t)
hh : a < u ∧ u ≤ t
⊢ u ∈ Ι a b \ {a, b}
Tactic:
case inl hh =>
simp [mem_uIoc]
push_neg at hu ⊢
refine ⟨Or.inl ⟨hh.1, hh.2.trans ht.2⟩, hu.2.1, ?_⟩
intro hub
subst_vars
cases hu.2.2 (le_antisymm hh.2 ht.2)
Proof state after:
no goals
Theorem: ContDiffOn.integral_eq_sub''
Proof state before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = t)
hh : a < u ∧ u ≤ t
⊢ u ∈ Ι a b \ {a, b}
Tactic:
simp [mem_uIoc]
Proof state after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
ht : t ∈ Icc a b
l1 : Icc a t ⊆ Icc a b
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = t)
hh : a < u ∧ u ≤ t
⊢ (a < u ∧ u ≤ b ∨ b < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = b)