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

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

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

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

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

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

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

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

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

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

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

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
⊢ (a < u ∧ u ≤ b ∨ b < u ∧ u ≤ a) ∧ ¬(u = a ∨ u = b)
Tactic:
push_neg at hu ⊢
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 : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
⊢ (a < u ∧ u ≤ b ∨ b < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ b

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 : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
⊢ (a < u ∧ u ≤ b ∨ b < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ b
Tactic:
refine ⟨Or.inl ⟨hh.1, hh.2.trans ht.2⟩, hu.2.1, ?_⟩
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 : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
⊢ u ≠ b

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 : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
⊢ u ≠ b
Tactic:
intro hub
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 : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
hub : u = b
⊢ False

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 : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
hub : u = b
⊢ False
Tactic:
subst_vars
State after:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
h : ContDiffOn ℝ 1 f (Icc a u)
hab : a ≤ u
ht : t ∈ Icc a u
l1 : Icc a t ⊆ Icc a u
⊢ False

State before:
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a t : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
l2 : ∫ (y : ℝ) in a..t, deriv f y = f t - f a
u : ℝ
hh : a < u ∧ u ≤ t
hu : (a < u ∧ u ≤ t ∨ t < u ∧ u ≤ a) ∧ u ≠ a ∧ u ≠ t
h : ContDiffOn ℝ 1 f (Icc a u)
hab : a ≤ u
ht : t ∈ Icc a u
l1 : Icc a t ⊆ Icc a u
⊢ False
Tactic:
cases hu.2.2 (le_antisymm hh.2 ht.2)
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
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 : t < u ∧ u ≤ a
⊢ u ∈ Ι a b \ {a, b}
Tactic:
case inr hh => linarith [ht.1]
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
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 : t < u ∧ u ≤ a
⊢ u ∈ Ι a b \ {a, b}
Tactic:
linarith [ht.1]
State after:
no goals