-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem _root_.IsOpen.isOpen_inter_preimage_of_fderiv_eq_zero
    (hs : IsOpen s) (hf : DifferentiableOn 𝕜 f s)
    (hf' : s.EqOn (fderiv 𝕜 f) 0) (t : Set G) : IsOpen (s ∩ f ⁻¹' t)

Proof state:
case intro.intro.refine_1
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
x : E
hx : x ∈ ball y r
z : E
hz : z ∈ ball y r
⊢ fderivWithin 𝕜 f (ball y r) z = 0

Tactic:
simpa only [fderivWithin_of_isOpen Metric.isOpen_ball hz] using hf' (h hz)

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
⊢ IsOpen (s ∩ f ⁻¹' t)

Tactic:
refine Metric.isOpen_iff.mpr fun y ⟨hy, hy'⟩ ↦ ?_

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
⊢ ∃ ε > 0, ball y ε ⊆ s ∩ f ⁻¹' t

Proof state:
case intro.intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
⊢ ∃ ε > 0, ball y ε ⊆ s ∩ f ⁻¹' t

Tactic:
refine ⟨r, hr, Set.subset_inter h fun x hx ↦ ?_⟩

Result:
case intro.intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
x : E
hx : x ∈ ball y r
⊢ x ∈ f ⁻¹' t

Proof state:
case intro.intro.refine_2
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
x : E
hx : x ∈ ball y r
this : f x = f y
⊢ x ∈ f ⁻¹' t

Tactic:
simpa [this]

Result:
no goals

Proof state:
case intro.intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
x : E
hx : x ∈ ball y r
⊢ x ∈ f ⁻¹' t

Tactic:
have := (convex_ball y r).is_const_of_fderivWithin_eq_zero (hf.mono h) ?_ hx (mem_ball_self hr)

Result:
case intro.intro.refine_2
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
x : E
hx : x ∈ ball y r
this : f x = f y
⊢ x ∈ f ⁻¹' t

case intro.intro.refine_1
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
x : E
hx : x ∈ ball y r
⊢ ∀ x ∈ ball y r, fderivWithin 𝕜 f (ball y r) x = 0

Proof state:
case intro.intro.refine_1
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
x : E
hx : x ∈ ball y r
⊢ ∀ x ∈ ball y r, fderivWithin 𝕜 f (ball y r) x = 0

Tactic:
intro z hz

Result:
case intro.intro.refine_1
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
x : E
hx : x ∈ ball y r
z : E
hz : z ∈ ball y r
⊢ fderivWithin 𝕜 f (ball y r) z = 0

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
⊢ ∃ ε > 0, ball y ε ⊆ s ∩ f ⁻¹' t

Tactic:
obtain ⟨r, hr, h⟩ := Metric.isOpen_iff.mp hs y hy

Result:
case intro.intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
t : Set G
y : E
x✝ : y ∈ s ∩ f ⁻¹' t
hy : y ∈ s
hy' : y ∈ f ⁻¹' t
r : ℝ
hr : r > 0
h : ball y r ⊆ s
⊢ ∃ ε > 0, ball y ε ⊆ s ∩ f ⁻¹' t