Theorem: Tutorial.exists_ratio_hasDerivAt_eq_ratio_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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Tactic:
let h x := (g b - g a) * f x - (f b - f a) * g 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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c

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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Tactic:
have hhc : ContinuousOn h (Icc a b) :=
  (continuousOn_const.mul hfc).sub (continuousOn_const.mul hgc)
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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c

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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Tactic:
have hI : h a = h b := by ring
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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c

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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Tactic:
let h' x := (g b - g a) * f' x - (f b - f a) * g' 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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c

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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Tactic:
have hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x := by
  intro x hx
  apply ((hff' x hx).const_mul (g b - g a)).sub ((hgg' x hx).const_mul (f b - f a))
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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c

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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Tactic:
have ⟨c, cmem, hc⟩ := exists_hasDerivAt_eq_zero hab hhc hI hhh'
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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : h' c = 0
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c

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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : h' c = 0
⊢ ∃ c ∈ Ioo a b, (g b - g a) * f' c = (f b - f a) * g' c
Tactic:
exact ⟨c, cmem, sub_eq_zero.mp 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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
⊢ h a = h b
Tactic:
ring
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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
⊢ ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x
Tactic:
intro x hx
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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt h (h' x) x

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
hgc : ContinuousOn g (Icc a b)
hgg' : ∀ x ∈ Ioo a b, HasDerivAt g (g' x) x
h : ℝ → ℝ := fun x => (g b - g a) * f x - (f b - f a) * g x
hhc : ContinuousOn h (Icc a b)
hI : h a = h b
h' : ℝ → ℝ := fun x => (g b - g a) * f' x - (f b - f a) * g' x
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt h (h' x) x
Tactic:
apply ((hff' x hx).const_mul (g b - g a)).sub ((hgg' x hx).const_mul (f b - f a))
State after:
no goals