-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem _root_.eq_of_fderiv_eq
    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : E → G}
    (hf : Differentiable 𝕜 f) (hg : Differentiable 𝕜 g)
    (hf' : ∀ x, fderiv 𝕜 f x = fderiv 𝕜 g x) (x : E) (hfgx : f x = g x) : f = g

Proof state:
𝕜 : Type u_3
G : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x
x : E
hfgx : f x = g x
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ f = g

Tactic:
let A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E

Result:
𝕜 : Type u_3
G : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x
x : E
hfgx : f x = g x
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E
⊢ f = g

Proof state:
𝕜 : Type u_3
G : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x
x : E
hfgx : f x = g x
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E
⊢ f = g

Tactic:
suffices Set.univ.EqOn f g from funext fun x => this <| mem_univ x

Result:
𝕜 : Type u_3
G : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x
x : E
hfgx : f x = g x
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E
⊢ EqOn f g univ

Proof state:
𝕜 : Type u_3
G : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x
x : E
hfgx : f x = g x
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E
⊢ EqOn f g univ

Tactic:
exact convex_univ.eqOn_of_fderivWithin_eq hf.differentiableOn hg.differentiableOn
  uniqueDiffOn_univ (fun x _ => by simpa using hf' _) (mem_univ _) hfgx

Result:
no goals

Proof state:
𝕜 : Type u_3
G : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x
x : E
hfgx : f x = g x
⊢ f = g

Tactic:
letI : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜

Result:
𝕜 : Type u_3
G : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x
x : E
hfgx : f x = g x
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
⊢ f = g

Proof state:
𝕜 : Type u_3
G : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
E : Type u_5
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : E → G
hf : Differentiable 𝕜 f
hg : Differentiable 𝕜 g
hf' : ∀ (x : E), fderiv 𝕜 f x = fderiv 𝕜 g x
x✝¹ : E
hfgx : f x✝¹ = g x✝¹
this : RCLike 𝕜 := IsRCLikeNormedField.rclike 𝕜
A : NormedSpace ℝ E := RestrictScalars.normedSpace ℝ 𝕜 E
x : E
x✝ : x ∈ univ
⊢ fderivWithin 𝕜 f univ x = fderivWithin 𝕜 g univ x

Tactic:
simpa using hf' _

Result:
no goals