Theorem: ContDiffOn.integral_eq_sub (RMT4/to_mathlib.lean)

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
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

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
State after:
no goals

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
State after:
no goals

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]
State after:
no goals

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]
State after:
no goals