awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
t : Set G
y : E
h_1 : 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
refine_2 : ∀ (this : f x = f y), x ∈ f ⁻¹' t
refine_1 : ∀ x ∈ ball y r, Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 f (ball y r) x) 0
⊢ x ∈ f ⁻¹' t

Tactic:
have := (convex_ball y r).is_const_of_fderivWithin_eq_zero (hf.mono h) ?_ hx (mem_ball_self hr)
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
t : Set G
y : E
h_1 : 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]
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
t : Set G
y : E
h_1 : 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
⊢ Eq (α := E →L[𝕜] G) (fderivWithin 𝕜 f (ball y r) z) 0

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

Premises used: fderivWithin_of_isOpen, Metric.isOpen_ball
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
h₁ : Differentiable 𝕜 f
h₂ : ∀ (x : E), Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) 0
⊢ IsLocallyConstant f

Tactic:
simpa using isOpen_univ.isOpen_inter_preimage_of_fderiv_eq_zero h₁.differentiableOn fun _ _ ↦ h₂ _

Premises used: isOpen_univ, IsOpen.isOpen_inter_preimage_of_fderiv_eq_zero, Differentiable.differentiableOn
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
inl :
  ∀ (hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) (hs' : IsPreconnected.{u_1} (α := E) ∅)
    (hf : DifferentiableOn 𝕜 f ∅) (hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 ∅),
    ∃ (a : G), ∀ (x : E), Membership.mem (γ := Set E) ∅ x → f x = a
inr : ∀ (y : E) (hy : y ∈ s), ∃ (a : G), ∀ x ∈ s, f x = a
⊢ ∃ (a : G), ∀ x ∈ s, f x = a

Tactic:
obtain (rfl | ⟨y, hy⟩) := s.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hs' : IsPreconnected.{u_1} (α := E) ∅
hf : DifferentiableOn 𝕜 f ∅
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 ∅
⊢ ∀ (x : E), Membership.mem (γ := Set E) ∅ x → f x = 0

Tactic:
simp
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hs' : IsPreconnected.{u_1} (α := E) ∅
hf : DifferentiableOn 𝕜 f ∅
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 ∅
⊢ ∃ (a : G), ∀ (x : E), Membership.mem (γ := Set E) ∅ x → f x = a

Tactic:
exact ⟨0, by simp⟩
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
⊢ ∃ (a : G), ∀ x ∈ s, f x = a

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

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
inr : ∀ (x : E) (hx : x ∈ s), f x = f y
⊢ ∃ (a : G), ∀ x ∈ s, f x = a

Tactic:
refine ⟨f y, fun x hx ↦ ?_⟩
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
⊢ IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})

Tactic:
have h₁ := hs.isOpen_inter_preimage_of_fderiv_eq_zero hf hf' {f y}
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
⊢ Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))

Tactic:
have h₂ := hf.continuousOn.comp_continuous continuous_subtype_val (fun x ↦ x.2)
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
inr : ∀ (h₃ : ¬f x = f y), False
⊢ f x = f y

Tactic:
by_contra h₃
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
h₃ : ¬f x = f y
inr :
  ∀ (t : Set E) (ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t)
    (ht' :
      Eq (α := Set (Subtype (Membership.mem s))) (Subtype.val (p := Membership.mem s) ⁻¹' t)
        (f ∘ Subtype.val (p := Membership.mem s) ⁻¹' {f y})ᶜ),
    False
⊢ False

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

Premises used: IsClosed.preimage, isClosed_singleton
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
h₃ : ¬f x = f y
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
ht' :
  Eq (α := Set (Subtype (Membership.mem s))) (Subtype.val (p := Membership.mem s) ⁻¹' t)
    (f ∘ Subtype.val (p := Membership.mem s) ⁻¹' {f y})ᶜ
⊢ ∀ a ∈ s, a ∈ t ↔ f a ≠ f y

Tactic:
simpa [Set.ext_iff] using ht'

Premises used: Set.ext_iff
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
h₃ : ¬f x = f y
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
ht' :
  Eq (α := Set (Subtype (Membership.mem s))) (Subtype.val (p := Membership.mem s) ⁻¹' t)
    (f ∘ Subtype.val (p := Membership.mem s) ⁻¹' {f y})ᶜ
⊢ ∀ a ∈ s, a ∈ t ↔ f a ≠ f y

Tactic:
have ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y := by simpa [Set.ext_iff] using ht'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x_1 : E
hx : x_1 ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
h₃ : ¬f x_1 = f y
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
ht' :
  Eq (α := Set (Subtype (Membership.mem s))) (Subtype.val (p := Membership.mem s) ⁻¹' t)
    (f ∘ Subtype.val (p := Membership.mem s) ⁻¹' {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]

Premises used: eq_or_ne
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
h₃ : ¬f x = f y
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
ht' :
  Eq (α := Set (Subtype (Membership.mem s))) (Subtype.val (p := Membership.mem s) ⁻¹' t)
    (f ∘ Subtype.val (p := Membership.mem s) ⁻¹' {f y})ᶜ
ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y
⊢ y ∈ s ∩ (s ∩ f ⁻¹' {f y})

Tactic:
simpa
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
h₃ : ¬f x = f y
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
ht' :
  Eq (α := Set (Subtype (Membership.mem s))) (Subtype.val (p := Membership.mem s) ⁻¹' t)
    (f ∘ Subtype.val (p := Membership.mem s) ⁻¹' {f y})ᶜ
ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y
⊢ x ∈ s ∩ t

Tactic:
simp [ht'' _ hx, hx, h₃]
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
h₃ : ¬f x = f y
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
ht' :
  Eq (α := Set (Subtype (Membership.mem s))) (Subtype.val (p := Membership.mem s) ⁻¹' t)
    (f ∘ Subtype.val (p := Membership.mem s) ⁻¹' {f y})ᶜ
ht'' : ∀ a ∈ s, a ∈ t ↔ f a ≠ f y
inr : ∀ (z : E) (H₁ : z ∈ s) (H₂ : z ∈ s ∩ f ⁻¹' {f y}) (H₃ : z ∈ t), False
⊢ 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₃]⟩

Premises used: Exists.intro
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
h₃ : ¬f x = f y
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
ht' :
  Eq (α := Set (Subtype (Membership.mem s))) (Subtype.val (p := Membership.mem s) ⁻¹' t)
    (f ∘ Subtype.val (p := Membership.mem s) ⁻¹' {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

Tactic:
(ht'' _ H₁).mp H₃ H₂.2

Premises used: And.right, Iff.mp
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
y : E
hy : y ∈ s
x : E
hx : x ∈ s
h₁ : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (s ∩ f ⁻¹' {f y})
h₂ :
  Continuous[instTopologicalSpaceSubtype, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    (f ∘ Subtype.val (p := Membership.mem s))
h₃ : ¬f x = f y
t : Set E
ht : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] t
ht' :
  Eq (α := Set (Subtype (Membership.mem s))) (Subtype.val (p := Membership.mem s) ⁻¹' t)
    (f ∘ Subtype.val (p := Membership.mem s) ⁻¹' {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

Tactic:
exact (ht'' _ H₁).mp H₃ H₂.2

Premises used: And.right, Iff.mp
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
x y : E
hx : x ∈ s
hy : y ∈ s
obtain : ∀ (a : G) (ha : ∀ x ∈ s, f x = a), f x = f y
⊢ f x = f y

Tactic:
obtain ⟨a, ha⟩ := hs.exists_is_const_of_fderiv_eq_zero hs' hf hf'

Premises used: IsOpen.exists_is_const_of_fderiv_eq_zero
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) 0 s
x y : E
hx : x ∈ s
hy : y ∈ s
a : G
ha : ∀ x ∈ s, f x = a
rw : a = f y
rw₁ rw₂ : a = a
⊢ f x = f y

Tactic:
rw [ha x hx, ha y hy]
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) (fderiv 𝕜 g) s
simp_rw : ∃ (a : G), ∀ ⦃x : E⦄, x ∈ s → f x - g x = a
⊢ ∃ (a : G), EqOn f (fun (x : E) ↦ g x + a) s

Tactic:
simp_rw [Set.EqOn, ← sub_eq_iff_eq_add']

Premises used: Set.EqOn, sub_eq_iff_eq_add'
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) (fderiv 𝕜 g) s
⊢ ∃ (a : G), ∀ ⦃x : E⦄, x ∈ s → f x - g x = a

Tactic:
hs.exists_is_const_of_fderiv_eq_zero hs' (hf.sub hg) fun x hx ↦ ?_

Premises used: DifferentiableOn.sub, IsOpen.exists_is_const_of_fderiv_eq_zero
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) (fderiv 𝕜 g) s
refine : ∀ (x : E) (hx : x ∈ s), Eq (α := E →L[𝕜] G) (fderiv 𝕜 (fun (x : E) ↦ f x - g x) x) (0 x)
⊢ ∃ (a : G), ∀ ⦃x : E⦄, x ∈ s → f x - g x = a

Tactic:
refine hs.exists_is_const_of_fderiv_eq_zero hs' (hf.sub hg) fun x hx ↦ ?_

Premises used: DifferentiableOn.sub, IsOpen.exists_is_const_of_fderiv_eq_zero
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f g : E → G
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : EqOn (β := E →L[𝕜] G) (fderiv 𝕜 f) (fderiv 𝕜 g) s
x : E
hx : x ∈ s
rw : HSub.hSub (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x) = 0 x
rw₁ : HSub.hSub (α := E →L[𝕜] G) (fderiv 𝕜 g x) (fderiv 𝕜 g x) = 0 x
rw₂ : Eq (α := E →L[𝕜] G) 0 (0 x)
rw₃ rw₄ : Eq (α := E →L[𝕜] G) 0 0
⊢ Eq (α := E →L[𝕜] G) (fderiv 𝕜 (fun (x : E) ↦ f x - g x) x) (0 x)

Tactic:
rw [fderiv_fun_sub (hf.differentiableAt (hs.mem_nhds hx)) (hg.differentiableAt (hs.mem_nhds hx)),
    hf' hx, sub_self, Pi.zero_apply]

Premises used: sub_self, fderiv_fun_sub, DifferentiableOn.differentiableAt, Pi.zero_apply, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Calculus.MeanValue
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst_2 : NontriviallyNormedField 𝕜
inst_3 : IsRCLikeNormedField 𝕜
inst_4 : NormedSpace 𝕜 E
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f g : E → G
s : Set E
x : E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : ∀ x ∈ s, Eq (α := E →L[𝕜] G) (fderiv 𝕜 f x) (fderiv 𝕜 g x)
hx : x ∈ s
hfgx : f x = g x
obtain : ∀ (a : G) (ha : EqOn f (fun (x : E) ↦ g x + a) s), EqOn f g s
⊢ EqOn f g s

Tactic:
obtain ⟨a, ha⟩ := hs.exists_eq_add_of_fderiv_eq hs' hf hg hf'

Premises used: IsOpen.exists_eq_add_of_fderiv_eq