E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.256230
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x y✝ : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : ∀ (x : E), x ∈ s → fderivWithin 𝕜 f s x = fderivWithin 𝕜 g s x
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
⊢ f x - g x = f y - g y
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.256230
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x y✝ : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : ∀ (x : E), x ∈ s → fderivWithin 𝕜 f s x = fderivWithin 𝕜 g s x
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
⊢ f y = g y
suffices f x - g x = f y - g y by rwa [hfgx, sub_self, eq_comm, sub_eq_zero] at this
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.256230
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x y✝ : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : ∀ (x : E), x ∈ s → fderivWithin 𝕜 f s x = fderivWithin 𝕜 g s x
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
⊢ fderivWithin 𝕜 (fun y => f y - g y) s z = 0
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.256230
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x y✝ : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : ∀ (x : E), x ∈ s → fderivWithin 𝕜 f s x = fderivWithin 𝕜 g s x
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
⊢ f x - g x = f y - g y
refine' hs.is_const_of_fderivWithin_eq_zero (hf.sub hg) (fun z hz => _) hx hy
no goals
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.256230
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x y✝ : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : ∀ (x : E), x ∈ s → fderivWithin 𝕜 f s x = fderivWithin 𝕜 g s x
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
⊢ fderivWithin 𝕜 (fun y => f y - g y) s z = 0
rw [fderivWithin_sub (hs' _ hz) (hf _ hz) (hg _ hz), sub_eq_zero, hf' _ hz]
no goals
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.256230
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_2
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x y✝ : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hs : Convex ℝ s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hs' : UniqueDiffOn 𝕜 s
hf' : ∀ (x : E), x ∈ s → fderivWithin 𝕜 f s x = fderivWithin 𝕜 g s x
hx : x ∈ s
hfgx : f x = g x
y : E
hy : y ∈ s
this : f x - g x = f y - g y
⊢ f y = g y
rwa [hfgx, sub_self, eq_comm, sub_eq_zero] at this