awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f) ⦃x₀ : E⦄,
    x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_6_iff_5 :
  (∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|) ↔
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
h : ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|
x : E
hx : x ∈ C
obtain :
  ∀ (r : ℝ) (hr : ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r),
    ∃ (K : NNReal), ∃ t ∈ 𝓝[C] x, LipschitzOnWith K f t
⊢ ∃ (K : NNReal), ∃ t ∈ 𝓝[C] x, LipschitzOnWith K f t

Tactic:
obtain ⟨r, hr⟩ := h hx
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f) ⦃x₀ : E⦄,
    x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_6_iff_5 :
  (∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|) ↔
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
h : ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|
x : E
hx : x ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
obtain :
  ∀ (ε : ℝ) (hε : ε > 0)
    (hεD : ball x ε ⊆ C ∩ |f| ⁻¹' {x : ℝ | (fun (x : ℝ) ↦ ((fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r : Prop)) x}),
    ∃ (K : NNReal), ∃ t ∈ 𝓝[C] x, LipschitzOnWith K f t
⊢ ∃ (K : NNReal), ∃ t ∈ 𝓝[C] x, LipschitzOnWith K f t

Tactic:
obtain ⟨ε, hε, hεD⟩ := Metric.mem_nhds_iff.1 <| Filter.inter_mem (hC.mem_nhds hx) hr

Premises used: Filter.inter_mem, Metric.mem_nhds_iff, IsOpen.mem_nhds, Iff.mp
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f) ⦃x₀ : E⦄,
    x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_6_iff_5 :
  (∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|) ↔
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
h : ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|
x : E
hx : x ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
ε : ℝ
hε : ε > 0
hεD : ball x ε ⊆ C ∩ |f| ⁻¹' {x : ℝ | (fun (x : ℝ) ↦ ((fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r : Prop)) x}
simp : ∀ (hεD : ball x ε ⊆ C ∧ ball x ε ⊆ {a : E | |f a| ≤ r}), ∃ (K : NNReal), ∃ t ∈ 𝓝 x, LipschitzOnWith K f t
⊢ ∃ (K : NNReal), ∃ t ∈ 𝓝[C] x, LipschitzOnWith K f t

Tactic:
simp only [preimage_setOf_eq, Pi.abs_apply, subset_inter_iff, hC.nhdsWithin_eq hx] at hεD ⊢

Premises used: IsOpen.nhdsWithin_eq, Pi.abs_apply, Set.subset_inter_iff, Set.preimage_setOf_eq
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f) ⦃x₀ : E⦄,
    x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_6_iff_5 :
  (∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|) ↔
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
h : ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|
x : E
hx : x ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
ε : ℝ
hε : ε > 0
hεD : ball x ε ⊆ C ∧ ball x ε ⊆ {a : E | |f a| ≤ r}
⊢ ∀ x_1 ∈ f '' ball x ε, ‖x_1‖ ≤ r

Tactic:
simpa using hεD.2

Premises used: And.right
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f) ⦃x₀ : E⦄,
    x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_6_iff_5 :
  (∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|) ↔
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
h : ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|
x : E
hx : x ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
ε : ℝ
hε : ε > 0
hεD : ball x ε ⊆ C ∧ ball x ε ⊆ {a : E | |f a| ≤ r}
obtain : ∀ (K : NNReal) (hK : LipschitzOnWith K f (ball x (ε / 2))), ∃ (K : NNReal), ∃ t ∈ 𝓝 x, LipschitzOnWith K f t
⊢ ∃ (K : NNReal), ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

Tactic:
obtain ⟨K, hK⟩ := exists_lipschitzOnWith_of_isBounded (hf.subset hεD.1 (convex_ball ..))
      (half_lt_self hε) <| isBounded_iff_forall_norm_le.2 ⟨r, by simpa using hεD.2⟩

Premises used: half_lt_self, Iff.mpr, convex_ball, isBounded_iff_forall_norm_le, And.left, Exists.intro, ConvexOn.exists_lipschitzOnWith_of_isBounded, ConvexOn.subset
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f) ⦃x₀ : E⦄,
    x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_6_iff_5 :
  (∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|) ↔
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
h : ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|
x : E
hx : x ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
ε : ℝ
hε : ε > 0
hεD : ball x ε ⊆ C ∧ ball x ε ⊆ {a : E | |f a| ≤ r}
K : NNReal
hK : LipschitzOnWith K f (ball x (ε / 2))
⊢ 0 < ε / 2

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f) ⦃x₀ : E⦄,
    x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_6_iff_5 :
  (∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|) ↔
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
h : ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|
x : E
hx : x ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map |f| (𝓝 x), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
ε : ℝ
hε : ε > 0
hεD : ball x ε ⊆ C ∧ ball x ε ⊆ {a : E | |f a| ≤ r}
K : NNReal
hK : LipschitzOnWith K f (ball x (ε / 2))
⊢ ∃ (K : NNReal), ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

Tactic:
exact ⟨K, _, ball_mem_nhds _ (by simpa), hK⟩
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f) ⦃x₀ : E⦄,
    x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_6_iff_5 :
  (∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|) ↔
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
⊢ ∀ (a : ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|), LocallyLipschitzOn C f

Tactic:
tfae_have 6 → 1
  | h, x, hx => by
    obtain ⟨r, hr⟩ := h hx
    obtain ⟨ε, hε, hεD⟩ := Metric.mem_nhds_iff.1 <| Filter.inter_mem (hC.mem_nhds hx) hr
    simp only [preimage_setOf_eq, Pi.abs_apply, subset_inter_iff, hC.nhdsWithin_eq hx] at hεD ⊢
    obtain ⟨K, hK⟩ := exists_lipschitzOnWith_of_isBounded (hf.subset hεD.1 (convex_ball ..))
      (half_lt_self hε) <| isBounded_iff_forall_norm_le.2 ⟨r, by simpa using hεD.2⟩
    exact ⟨K, _, ball_mem_nhds _ (by simpa), hK⟩
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
tfae_2_to_3 : ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
tfae_3_to_4 : ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_4_to_5 :
  ∀ (a : ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f) ⦃x₀ : E⦄,
    x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_6_iff_5 :
  (∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|) ↔
    ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
tfae_6_to_1 :
  ∀ (a : ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|), LocallyLipschitzOn C f
⊢ [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ C f
⊢ [LocallyLipschitzOn C (-f), ContinuousOn (-f) C, ∃ x₀ ∈ C, ContinuousAt (-f) x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |(-f)|].TFAE

Tactic:
have := hf.neg.continuousOn_tfae hC hC'
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ C f
this :
  [LocallyLipschitzOn C (-f), ContinuousOn (-f) C, ∃ x₀ ∈ C, ContinuousAt (-f) x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |(-f)|].TFAE
⊢ [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE

Tactic:
simp only [locallyLipschitzOn_neg_iff, continuousOn_neg_iff, continuousAt_neg_iff, abs_neg]
    at this

Premises used: abs_neg, locallyLipschitzOn_neg_iff, continuousAt_neg_iff, continuousOn_neg_iff
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ C f
this :
  [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE
⊢ [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE

Tactic:
this
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ C f
this :
  [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE
h :
  ∀ (x : E),
    Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) (𝓝 x) f ↔
      Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x) (-f)
h₁ :
  ∀ a ∈ C,
    Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) (𝓝 a) f ↔
      Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 a) (-f)
⊢ [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) (𝓝 x₀) f,
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE

Tactic:
convert! this using 8
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ C f
this :
  [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE
x : E
⊢ ∀ (a : ℝ),
    (∀ᶠ (x : ℝ) in Filter.map f (𝓝 x), (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) x a) ↔
      ∀ᶠ (x : ℝ) in Filter.map (-f) (𝓝 x), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x ((Equiv.neg ℝ : (a : ℝ) → ℝ) a)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ C f
this :
  [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE
x : E
⊢ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) (𝓝 x) f ↔
    Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x) (-f)

Tactic:
exact (Equiv.neg ℝ).exists_congr (by simp)

Premises used: Real, Equiv.neg, Equiv.exists_congr
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ C f
this :
  [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE
a : E
h : a ∈ C
⊢ ∀ (a_1 : ℝ),
    (∀ᶠ (x : ℝ) in Filter.map f (𝓝 a), (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) x a_1) ↔
      ∀ᶠ (x : ℝ) in Filter.map (-f) (𝓝 a), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x ((Equiv.neg ℝ : (a : ℝ) → ℝ) a_1)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hC' : C.Nonempty
hf : ConcaveOn ℝ C f
this :
  [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀,
      ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) (-f),
      ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f|].TFAE
a : E
h : a ∈ C
⊢ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) (𝓝 a) f ↔
    Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 a) (-f)

Tactic:
exact (Equiv.neg ℝ).exists_congr (by simp)

Premises used: Real, Equiv.neg, Equiv.exists_congr
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConvexOn ℝ C f
inl :
  ∀ (hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) (hf : ConvexOn ℝ ∅ f),
    LocallyLipschitzOn ∅ f ↔ ContinuousOn f ∅
inr : ∀ (hC' : C.Nonempty), LocallyLipschitzOn C f ↔ ContinuousOn f C
⊢ LocallyLipschitzOn C f ↔ ContinuousOn f C

Tactic:
obtain rfl | hC' := C.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hf : ConvexOn ℝ ∅ f
⊢ LocallyLipschitzOn ∅ f ↔ ContinuousOn f ∅

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConvexOn ℝ C f
hC' : C.Nonempty
⊢ LocallyLipschitzOn C f ↔ ContinuousOn f C

Tactic:
(hf.continuousOn_tfae hC hC').out 0 1

Premises used: ConvexOn.continuousOn_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConvexOn ℝ C f
hC' : C.Nonempty
⊢ LocallyLipschitzOn C f ↔ ContinuousOn f C

Tactic:
exact (hf.continuousOn_tfae hC hC').out 0 1

Premises used: ConvexOn.continuousOn_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConcaveOn ℝ C f
⊢ LocallyLipschitzOn C f ↔ ContinuousOn f C

Tactic:
simpa using hf.neg.locallyLipschitzOn_iff_continuousOn hC

Premises used: ConvexOn.locallyLipschitzOn_iff_continuousOn, ConcaveOn.neg
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
inst_2 : FiniteDimensional ℝ E
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConvexOn ℝ C f
inl :
  ∀ (hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) (hf : ConvexOn ℝ ∅ f), LocallyLipschitzOn ∅ f
inr : ∀ (x₀ : E) (hx₀ : x₀ ∈ C), LocallyLipschitzOn C f
⊢ LocallyLipschitzOn C f

Tactic:
obtain rfl | ⟨x₀, hx₀⟩ := C.eq_empty_or_nonempty

Premises used: Set.eq_empty_or_nonempty, rfl
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
inst_2 : FiniteDimensional ℝ E
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hf : ConvexOn ℝ ∅ f
⊢ LocallyLipschitzOn ∅ f

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
inst_2 : FiniteDimensional ℝ E
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConvexOn ℝ C f
x₀ : E
hx₀ : x₀ ∈ C
inr :
  ∀ (b : AffineBasis (Fin (Module.finrank ℝ E + 1)) ℝ E)
    (hx₀b :
      Membership.mem (γ := Set E)
        (interior
          ((convexHull ℝ : (a : Set E) → Set E)
            (Set.range (ι := Fin (Module.finrank ℝ E + 1)) (⇑b : (a : Fin (Module.finrank ℝ E + 1)) → E))))
        x₀)
    (hbC :
      (convexHull ℝ : (a : Set E) → Set E)
          (Set.range (ι := Fin (Module.finrank ℝ E + 1)) (⇑b : (a : Fin (Module.finrank ℝ E + 1)) → E)) ⊆
        C),
    LocallyLipschitzOn C f
⊢ LocallyLipschitzOn C f

Tactic:
obtain ⟨b, hx₀b, hbC⟩ := exists_mem_interior_convexHull_affineBasis (hC.mem_nhds hx₀)

Premises used: exists_mem_interior_convexHull_affineBasis, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
inst_2 : FiniteDimensional ℝ E
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConvexOn ℝ C f
x₀ : E
hx₀ : x₀ ∈ C
b : AffineBasis (Fin (Module.finrank ℝ E + 1)) ℝ E
hx₀b :
  Membership.mem (γ := Set E)
    (interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (Set.range (ι := Fin (Module.finrank ℝ E + 1)) (⇑b : (a : Fin (Module.finrank ℝ E + 1)) → E))))
    x₀
hbC :
  (convexHull ℝ : (a : Set E) → Set E)
      (Set.range (ι := Fin (Module.finrank ℝ E + 1)) (⇑b : (a : Fin (Module.finrank ℝ E + 1)) → E)) ⊆
    C
⊢ LocallyLipschitzOn C f

Tactic:
((hf.continuousOn_tfae hC ⟨x₀, hx₀⟩).out 3 0).mp ?_

Premises used: ConvexOn.continuousOn_tfae, List.TFAE.out, Exists.intro, Iff.mp, OfNat.ofNat