case intro.intro
E : Type ?u.317721
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.317817
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hfd : DifferentiableOn ℝ f (Ioo a b)
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hgd : DifferentiableOn ℝ g (Ioo a b)
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
⊢ ∃ c, c ∈ Ioo a b ∧ f' c = (f b - f a) / (b - a)
E : Type ?u.317721
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.317817
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hfd : DifferentiableOn ℝ f (Ioo a b)
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hgd : DifferentiableOn ℝ g (Ioo a b)
⊢ ∃ c, c ∈ Ioo a b ∧ f' c = (f b - f a) / (b - a)
obtain ⟨c, cmem, hc⟩ : ∃ c ∈ Ioo a b, (b - a) * f' c = (f b - f a) * 1 :=
  exists_ratio_hasDerivAt_eq_ratio_slope f f' hab hfc hff' id 1 continuousOn_id
    fun x _ => hasDerivAt_id x
case intro.intro
E : Type ?u.317721
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.317817
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hfd : DifferentiableOn ℝ f (Ioo a b)
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hgd : DifferentiableOn ℝ g (Ioo a b)
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
⊢ f' c = (f b - f a) / (b - a)
case intro.intro
E : Type ?u.317721
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.317817
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hfd : DifferentiableOn ℝ f (Ioo a b)
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hgd : DifferentiableOn ℝ g (Ioo a b)
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
⊢ ∃ c, c ∈ Ioo a b ∧ f' c = (f b - f a) / (b - a)
use c, cmem
no goals
case intro.intro
E : Type ?u.317721
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.317817
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
a b : ℝ
hab : a < b
hfc : ContinuousOn f (Icc a b)
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hfd : DifferentiableOn ℝ f (Ioo a b)
g g' : ℝ → ℝ
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hgd : DifferentiableOn ℝ g (Ioo a b)
c : ℝ
cmem : c ∈ Ioo a b
hc : (b - a) * f' c = (f b - f a) * 1
⊢ f' c = (f b - f a) / (b - a)
rwa [mul_one, mul_comm, ← eq_div_iff (sub_ne_zero.2 hab.ne')] at hc