E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.52033
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' g : ℝ → E
derivf : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
derivg : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
fcont : ContinuousOn f (Icc a b)
gcont : ContinuousOn g (Icc a b)
hi : f a - g a = 0
⊢ ∀ (y : ℝ), y ∈ Icc a b → f y - g y = 0
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.52033
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' g : ℝ → E
derivf : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
derivg : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
fcont : ContinuousOn f (Icc a b)
gcont : ContinuousOn g (Icc a b)
hi : f a = g a
⊢ ∀ (y : ℝ), y ∈ Icc a b → f y = g y
simp only [← @sub_eq_zero _ _ (f _)] at hi⊢
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.52033
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' g : ℝ → E
derivf : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
derivg : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
fcont : ContinuousOn f (Icc a b)
gcont : ContinuousOn g (Icc a b)
hi : f a - g a = 0
⊢ ∀ (y : ℝ), y ∈ Icc a b → f y - g y = 0
exact hi ▸ constant_of_has_deriv_right_zero (fcont.sub gcont) fun y hy => by
  simpa only [sub_self] using (derivf y hy).sub (derivg y hy)
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.52033
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' g : ℝ → E
derivf : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt f (f' x) (Ici x) x
derivg : ∀ (x : ℝ), x ∈ Ico a b → HasDerivWithinAt g (f' x) (Ici x) x
fcont : ContinuousOn f (Icc a b)
gcont : ContinuousOn g (Icc a b)
hi : f a - g a = 0
y : ℝ
hy : y ∈ Ico a b
⊢ HasDerivWithinAt (fun y => f y - g y) 0 (Ici y) y
simpa only [sub_self] using (derivf y hy).sub (derivg y hy)