E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
⊢ ∃ c, c ∈ Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
⊢ ∃ c, c ∈ Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c
let h x := (lgb - lga) * f x - (lfb - lfa) * g x
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
⊢ ∃ c, c ∈ Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
⊢ ∃ c, c ∈ Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c
have hha : Tendsto h (𝓝[>] a) (𝓝 <| lgb * lfa - lfb * lga) := by
  have : Tendsto h (𝓝[>] a) (𝓝 <| (lgb - lga) * lfa - (lfb - lfa) * lga) :=
    (tendsto_const_nhds.mul hfa).sub (tendsto_const_nhds.mul hga)
  convert this using 2
  ring
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
⊢ ∃ c, c ∈ Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
⊢ ∃ c, c ∈ Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c
have hhb : Tendsto h (𝓝[<] b) (𝓝 <| lgb * lfa - lfb * lga) := by
  have : Tendsto h (𝓝[<] b) (𝓝 <| (lgb - lga) * lfb - (lfb - lfa) * lgb) :=
    (tendsto_const_nhds.mul hfb).sub (tendsto_const_nhds.mul hgb)
  convert this using 2
  ring
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x => (lgb - lga) * f' x - (lfb - lfa) * g' x
⊢ ∃ c, c ∈ Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
⊢ ∃ c, c ∈ Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c
let h' x := (lgb - lga) * f' x - (lfb - lfa) * g' x
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x => (lgb - lga) * f' x - (lfb - lfa) * g' x
hhh' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt h (h' x) x
⊢ ∃ c, c ∈ Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x => (lgb - lga) * f' x - (lfb - lfa) * g' x
⊢ ∃ c, c ∈ Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c
have hhh' : ∀ x ∈ Ioo a b, HasDerivAt h (h' x) x := by
  intro x hx
  exact ((hff' x hx).const_mul _).sub ((hgg' x hx).const_mul _)
case intro.intro
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x => (lgb - lga) * f' x - (lfb - lfa) * g' x
hhh' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt h (h' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : h' c = 0
⊢ ∃ c, c ∈ Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x => (lgb - lga) * f' x - (lfb - lfa) * g' x
hhh' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt h (h' x) x
⊢ ∃ c, c ∈ Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c
rcases exists_hasDerivAt_eq_zero' hab hha hhb hhh' with ⟨c, cmem, hc⟩
no goals
case intro.intro
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x => (lgb - lga) * f' x - (lfb - lfa) * g' x
hhh' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt h (h' x) x
c : ℝ
cmem : c ∈ Ioo a b
hc : h' c = 0
⊢ ∃ c, c ∈ Ioo a b ∧ (lgb - lga) * f' c = (lfb - lfa) * g' c
exact ⟨c, cmem, sub_eq_zero.1 hc⟩
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
this : Tendsto h (𝓝[Ioi a] a) (𝓝 ((lgb - lga) * lfa - (lfb - lfa) * lga))
⊢ Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
⊢ Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
have : Tendsto h (𝓝[>] a) (𝓝 <| (lgb - lga) * lfa - (lfb - lfa) * lga) :=
  (tendsto_const_nhds.mul hfa).sub (tendsto_const_nhds.mul hga)
case h.e'_5.h.e'_3
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
this : Tendsto h (𝓝[Ioi a] a) (𝓝 ((lgb - lga) * lfa - (lfb - lfa) * lga))
⊢ lgb * lfa - lfb * lga = (lgb - lga) * lfa - (lfb - lfa) * lga
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
this : Tendsto h (𝓝[Ioi a] a) (𝓝 ((lgb - lga) * lfa - (lfb - lfa) * lga))
⊢ Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
convert this using 2
no goals
case h.e'_5.h.e'_3
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
this : Tendsto h (𝓝[Ioi a] a) (𝓝 ((lgb - lga) * lfa - (lfb - lfa) * lga))
⊢ lgb * lfa - lfb * lga = (lgb - lga) * lfa - (lfb - lfa) * lga
ring
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
this : Tendsto h (𝓝[Iio b] b) (𝓝 ((lgb - lga) * lfb - (lfb - lfa) * lgb))
⊢ Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
⊢ Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
have : Tendsto h (𝓝[<] b) (𝓝 <| (lgb - lga) * lfb - (lfb - lfa) * lgb) :=
  (tendsto_const_nhds.mul hfb).sub (tendsto_const_nhds.mul hgb)
case h.e'_5.h.e'_3
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
this : Tendsto h (𝓝[Iio b] b) (𝓝 ((lgb - lga) * lfb - (lfb - lfa) * lgb))
⊢ lgb * lfa - lfb * lga = (lgb - lga) * lfb - (lfb - lfa) * lgb
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
this : Tendsto h (𝓝[Iio b] b) (𝓝 ((lgb - lga) * lfb - (lfb - lfa) * lgb))
⊢ Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
convert this using 2
no goals
case h.e'_5.h.e'_3
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
this : Tendsto h (𝓝[Iio b] b) (𝓝 ((lgb - lga) * lfb - (lfb - lfa) * lgb))
⊢ lgb * lfa - lfb * lga = (lgb - lga) * lfb - (lfb - lfa) * lgb
ring
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x => (lgb - lga) * f' x - (lfb - lfa) * g' x
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt h (h' x) x
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x => (lgb - lga) * f' x - (lfb - lfa) * g' x
⊢ ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt h (h' x) x
intro x hx
no goals
E : Type ?u.311271
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.311367
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)
lfa lga lfb lgb : ℝ
hff' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt f (f' x) x
hgg' : ∀ (x : ℝ), x ∈ Ioo a b → HasDerivAt g (g' x) x
hfa : Tendsto f (𝓝[Ioi a] a) (𝓝 lfa)
hga : Tendsto g (𝓝[Ioi a] a) (𝓝 lga)
hfb : Tendsto f (𝓝[Iio b] b) (𝓝 lfb)
hgb : Tendsto g (𝓝[Iio b] b) (𝓝 lgb)
h : ℝ → ℝ := fun x => (lgb - lga) * f x - (lfb - lfa) * g x
hha : Tendsto h (𝓝[Ioi a] a) (𝓝 (lgb * lfa - lfb * lga))
hhb : Tendsto h (𝓝[Iio b] b) (𝓝 (lgb * lfa - lfb * lga))
h' : ℝ → ℝ := fun x => (lgb - lga) * f' x - (lfb - lfa) * g' x
x : ℝ
hx : x ∈ Ioo a b
⊢ HasDerivAt h (h' x) x
exact ((hff' x hx).const_mul _).sub ((hgg' x hx).const_mul _)