E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.54298
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
A : ∀ (y : ℝ), y ∈ Ico a b → HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
⊢ ∀ (y : ℝ), y ∈ Icc a b → f y = g y
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.54298
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
⊢ ∀ (y : ℝ), y ∈ Icc a b → f y = g y
have A : ∀ y ∈ Ico a b, HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y := fun y hy =>
  (fdiff y (mem_Icc_of_Ico hy)).hasDerivWithinAt.nhdsWithin (Icc_mem_nhdsWithin_Ici hy)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.54298
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
A : ∀ (y : ℝ), y ∈ Ico a b → HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
B : ∀ (y : ℝ), y ∈ Ico a b → HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y
⊢ ∀ (y : ℝ), y ∈ Icc a b → f y = g y
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.54298
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
A : ∀ (y : ℝ), y ∈ Ico a b → HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
⊢ ∀ (y : ℝ), y ∈ Icc a b → f y = g y
have B : ∀ y ∈ Ico a b, HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y := fun y hy =>
  (gdiff y (mem_Icc_of_Ico hy)).hasDerivWithinAt.nhdsWithin (Icc_mem_nhdsWithin_Ici hy)
no goals
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type ?u.54298
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : ℝ → E
a b : ℝ
f' g : ℝ → E
fdiff : DifferentiableOn ℝ f (Icc a b)
gdiff : DifferentiableOn ℝ g (Icc a b)
hderiv : EqOn (derivWithin f (Icc a b)) (derivWithin g (Icc a b)) (Ico a b)
hi : f a = g a
A : ∀ (y : ℝ), y ∈ Ico a b → HasDerivWithinAt f (derivWithin f (Icc a b) y) (Ici y) y
B : ∀ (y : ℝ), y ∈ Ico a b → HasDerivWithinAt g (derivWithin g (Icc a b) y) (Ici y) y
⊢ ∀ (y : ℝ), y ∈ Icc a b → f y = g y
exact
  eq_of_has_deriv_right_eq A (fun y hy => (hderiv hy).symm ▸ B y hy) fdiff.continuousOn
    gdiff.continuousOn hi