Theorem: Tutorial.exists_hasDerivAt_eq_slope (Solution/Advanced/Analysis/Lecture2.lean)

State before:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)
Tactic:
have ⟨c, cmem, hc⟩ := exists_ratio_hasDerivAt_eq_ratio_slope hab hfc hff'
  continuousOn_id fun x _ ↦ hasDerivAt_id x
State after:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (id b - id a) * f' c = (f b - f a) * 1
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)

State before:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (id b - id a) * f' c = (f b - f a) * 1
⊢ ∃ c ∈ Ioo a b, f' c = (f b - f a) / (b - a)
Tactic:
exact ⟨c, cmem, by rw [eq_div_iff (by linarith), mul_comm]; simpa using hc⟩
State after:
no goals

State before:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (id b - id a) * f' c = (f b - f a) * 1
⊢ f' c = (f b - f a) / (b - a)
Tactic:
rw [eq_div_iff (by linarith), mul_comm]
State after:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (id b - id a) * f' c = (f b - f a) * 1
⊢ (b - a) * f' c = f b - f a

State before:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (id b - id a) * f' c = (f b - f a) * 1
⊢ (b - a) * f' c = f b - f a
Tactic:
simpa using hc
State after:
no goals

State before:
f✝ : ℝ → ℝ
f'✝ x a✝ b✝ : ℝ
f f' g g' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ x ∈ Ioo a b, HasDerivAt f (f' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : (id b - id a) * f' c = (f b - f a) * 1
⊢ b - a ≠ 0
Tactic:
linarith
State after:
no goals