-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem _root_.IsOpen.exists_is_const_of_fderiv_eq_zero
    (hs : IsOpen s) (hs' : IsPreconnected s) (hf : DifferentiableOn 𝕜 f s)
    (hf' : s.EqOn (fderiv 𝕜 f) 0) : ∃ a, ∀ x ∈ s, f x = a

Proof state:
case inr.intro.mk.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
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen (s ∩ f ⁻¹' {f y})
h₂ : Continuous (f ∘ Subtype.val)
h₃ : ¬f x = f y
t : Set E
ht : IsOpen t
ht' : Subtype.val ⁻¹' t = (f ∘ Subtype.val ⁻¹' {f y})ᶜ
ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y
⊢ False

Tactic:
obtain ⟨z, H₁, H₂, H₃⟩ := hs' _ _ h₁ ht (fun x h ↦ by simp [h, ht'', eq_or_ne]) ⟨y, by simpa⟩
  ⟨x, by simp [ht'' _ hx, hx, h₃]⟩

Result:
case inr.intro.mk.intro.intro.intro.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
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen (s ∩ f ⁻¹' {f y})
h₂ : Continuous (f ∘ Subtype.val)
h₃ : ¬f x = f y
t : Set E
ht : IsOpen t
ht' : Subtype.val ⁻¹' t = (f ∘ Subtype.val ⁻¹' {f y})ᶜ
ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y
z : E
H₁ : z ∈ s
H₂ : z ∈ s ∩ f ⁻¹' {f y}
H₃ : z ∈ t
⊢ False

Proof state:
case inl
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
hs : IsOpen ∅
hs' : IsPreconnected ∅
hf : DifferentiableOn 𝕜 f ∅
hf' : EqOn (fderiv 𝕜 f) 0 ∅
⊢ ∃ a, ∀ x ∈ ∅, f x = a

Tactic:
exact ⟨0, by simp⟩

Result:
no goals

Proof state:
case inr.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
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
⊢ ∃ a, ∀ x ∈ s, f x = a

Tactic:
refine ⟨f y, fun x hx ↦ ?_⟩

Result:
case inr.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
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
⊢ f x = f y

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
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen (s ∩ f ⁻¹' {f y})
h₂ : Continuous (f ∘ Subtype.val)
h₃ : ¬f x = f y
t : Set E
ht : IsOpen t
ht' : Subtype.val ⁻¹' t = (f ∘ Subtype.val ⁻¹' {f y})ᶜ
⊢ ∀ a ∈ s, a ∈ t ↔ f a ≠ f y

Tactic:
simpa [Set.ext_iff] using ht'

Result:
no goals

Proof state:
case inr.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
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
⊢ f x = f y

Tactic:
have h₁ := hs.isOpen_inter_preimage_of_fderiv_eq_zero hf hf' {f y}

Result:
case inr.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
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen (s ∩ f ⁻¹' {f y})
⊢ f x = f y

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
hs : IsOpen ∅
hs' : IsPreconnected ∅
hf : DifferentiableOn 𝕜 f ∅
hf' : EqOn (fderiv 𝕜 f) 0 ∅
⊢ ∀ x ∈ ∅, f x = 0

Tactic:
simp

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
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x✝ : E
hx : x✝ ∈ s
h₁ : IsOpen (s ∩ f ⁻¹' {f y})
h₂ : Continuous (f ∘ Subtype.val)
h₃ : ¬f x✝ = f y
t : Set E
ht : IsOpen t
ht' : Subtype.val ⁻¹' t = (f ∘ Subtype.val ⁻¹' {f y})ᶜ
ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y
x : E
h : x ∈ s
⊢ x ∈ s ∩ f ⁻¹' {f y} ∪ t

Tactic:
simp [h, ht'', eq_or_ne]

Result:
no goals

Proof state:
case inr.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
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen (s ∩ f ⁻¹' {f y})
h₂ : Continuous (f ∘ Subtype.val)
h₃ : ¬f x = f y
⊢ False

Tactic:
obtain ⟨t, ht, ht'⟩ := (isClosed_singleton (x := f y)).preimage h₂

Result:
case inr.intro.mk.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
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen (s ∩ f ⁻¹' {f y})
h₂ : Continuous (f ∘ Subtype.val)
h₃ : ¬f x = f y
t : Set E
ht : IsOpen t
ht' : Subtype.val ⁻¹' t = (f ∘ Subtype.val ⁻¹' {f y})ᶜ
⊢ False