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 → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this_1 : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
this : f x₀ ≤ 2⁻¹ * f y + 2⁻¹ * f (HSMul.hSMul (α := ℝ) 2 x₀ - y)
⊢ 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℝ) 2 x₀ - y)

Tactic:
cancel_denoms at this
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this_1 : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
this : 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℝ) 2 x₀ - y)
rwa :
  ∀ (this : (↑2 : ℝ) * f x₀ ≤ f y + f (HSMul.hSMul (α := ℝ) (↑2 : ℝ) x₀ - y)),
    2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : (↑2 : ℝ) * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)),
    2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
⊢ 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)

Tactic:
rwa [← Nat.cast_two, Nat.cast_smul_eq_nsmul] at this

Premises used: Nat.cast_smul_eq_nsmul, Nat.cast_two
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
bc : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ |r|
⊢ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ f y + |r|

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
⊢ f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ |r|

Tactic:
hfr'.trans (le_abs_self _)

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
⊢ f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ |r|

Tactic:
exact hfr'.trans (le_abs_self _)

Premises used: le_abs_self, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConvexOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
r : ℝ
this : Filter.Tendsto (fun (y : E) ↦ HSMul.hSMul (α := ℕ) 2 x₀ - y) (𝓝 x₀) (𝓝 x₀)
hr : ∀ᶠ (a : E) in 𝓝 x₀, f a ≤ r
y : E
hx : HSMul.hSMul (α := ℕ) 2 x₀ - y ∈ C
hx' : y ∈ C
hfr : f y ≤ r
hfr' : f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ r
f₁ : 2 * f x₀ ≤ f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y)
f₂ : f y + f (HSMul.hSMul (α := ℕ) 2 x₀ - y) ≤ f y + |r|
⊢ -|2 * f x₀| ≤ f y + |r|

Tactic:
calc
    -|2 * f x₀| ≤ 2 * f x₀ := neg_abs_le _
    _ ≤ f y + f (2 • x₀ - y) := by
      have := hf.2 hx' hx (by positivity) (by positivity) (add_halves _)
      simp only [one_div, ← Nat.cast_smul_eq_nsmul ℝ, Nat.cast_ofNat, smul_sub, ne_eq,
        OfNat.ofNat_ne_zero, not_false_eq_true, inv_smul_smul₀, add_sub_cancel, smul_eq_mul] at this
      cancel_denoms at this
      rwa [← Nat.cast_two, Nat.cast_smul_eq_nsmul] at this
    _ ≤ f y + |r| := by gcongr; exact hfr'.trans (le_abs_self _)

Premises used: neg_abs_le, HSub.hSub, HSMul.hSMul, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
C : Set E
f : E → ℝ
hf : ConcaveOn ℝ C f
x₀ : E
hC : C ∈ 𝓝 x₀
⊢ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) |f| ↔
    Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) (𝓝 x₀) f

Tactic:
simpa [Pi.neg_def, Pi.abs_def] using hf.neg.isBoundedUnder_abs hC

Premises used: Pi.abs_def, ConvexOn.isBoundedUnder_abs, ConcaveOn.neg, Pi.neg_def
-- 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
⊢ LocallyLipschitzOn C f

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ContinuousOn f C

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C

Tactic:
tfae_have 1 → 2 := LocallyLipschitzOn.continuousOn

Premises used: LocallyLipschitzOn.continuousOn
-- 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
⊢ ContinuousOn f C

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∃ x₀ ∈ C, ContinuousAt f x₀

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀

Tactic:
2 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
obtain : ∀ (x₀ : E) (hx₀ : x₀ ∈ C) (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀
⊢ ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀

Tactic:
obtain ⟨x₀, hx₀⟩ := 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
hf : ConvexOn ℝ C f
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
x₀ : E
hx₀ : x₀ ∈ C
⊢ ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀

Tactic:
fun h ↦ ⟨x₀, hx₀, h.continuousAt <| hC.mem_nhds hx₀⟩

Premises used: And.intro, IsOpen.mem_nhds, Exists.intro, ContinuousOn.continuousAt
-- 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
tfae_1_to_2 : ∀ (a : LocallyLipschitzOn C f), ContinuousOn f C
x₀ : E
hx₀ : x₀ ∈ C
⊢ ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀

Tactic:
exact fun h ↦ ⟨x₀, hx₀, h.continuousAt <| hC.mem_nhds 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
⊢ ∀ (a : ContinuousOn f C), ∃ x₀ ∈ C, ContinuousAt f x₀

Tactic:
tfae_have 2 → 3 := by
    obtain ⟨x₀, hx₀⟩ := hC'
    exact fun h ↦ ⟨x₀, hx₀, h.continuousAt <| hC.mem_nhds 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₀
⊢ ∃ x₀ ∈ C, ContinuousAt f x₀

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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₀
⊢ ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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₀
⊢ ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f

Tactic:
3 → 4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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₀
x₀ : E
hx₀ : x₀ ∈ C
h : ContinuousAt f x₀
⊢ f x₀ < f x₀ + 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 : 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₀
x₀ : E
hx₀ : x₀ ∈ C
h : ContinuousAt f x₀
⊢ ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (f x₀ + 1)

Tactic:
simpa using h.eventually (eventually_le_nhds (by simp))

Premises used: eventually_le_nhds, Filter.Tendsto.eventually
-- 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₀
⊢ ∀ (a : ∃ x₀ ∈ C, ContinuousAt f x₀), ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f

Tactic:
tfae_have 3 → 4
  | ⟨x₀, hx₀, h⟩ =>
    ⟨x₀, hx₀, f x₀ + 1, by simpa using h.eventually (eventually_le_nhds (by 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 : 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
⊢ ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f

Tactic:
4

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f

Tactic:
5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
⊢ ∀ (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

Tactic:
4 → 5

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- 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
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
⊢ HSub.hSub (α := ℝ) 1 0 ≠ 0

Tactic:
norm_num
-- 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
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
funProp : HSub.hSub (α := ℝ) 1 0 ≠ 0
funProp₁ : HSub.hSub (α := ℝ) 1 0 ≠ 0
⊢ ContinuousAt.{0, u_1} (Y := E) (fun (δ : ℝ) ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0

Tactic:
fun_prop (disch := norm_num)
-- 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
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
⊢ ContinuousAt.{0, u_1} (Y := E) (fun (δ : ℝ) ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0

Tactic:
have h : ContinuousAt (fun δ : ℝ ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0 := by
        fun_prop (disch := norm_num)
-- 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
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
h : ContinuousAt.{0, u_1} (Y := E) (fun (δ : ℝ) ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0
⊢ Membership.mem (γ := Filter E) (𝓝 ((fun (δ : ℝ) ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0)) C

Tactic:
simpa using hC.mem_nhds hx

Premises used: 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 → ℝ
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
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
h : ContinuousAt.{0, u_1} (Y := E) (fun (δ : ℝ) ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C

Tactic:
exact h (by simpa using hC.mem_nhds 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
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
⊢ ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C

Tactic:
have : ∀ᶠ δ in 𝓝 (0 : ℝ), (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C := by
      have h : ContinuousAt (fun δ : ℝ ↦ (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀) 0 := by
        fun_prop (disch := norm_num)
      exact h (by simpa using hC.mem_nhds 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
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
this : ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C
obtain :
  ∀ (δ : ℝ) (hδ₀ : 0 < δ) (hy : (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C) (hδ₁ : δ < 1),
    Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x) f
⊢ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x) f

Tactic:
obtain ⟨δ, hδ₀, hy, hδ₁⟩ := (this.and <| eventually_lt_nhds zero_lt_one).exists_gt

Premises used: eventually_lt_nhds, Filter.Eventually.and, zero_lt_one, Filter.Eventually.exists_gt
-- 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
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
this : ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C
δ : ℝ
hδ₀ : 0 < δ
hy : (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C
hδ₁ : δ < 1
⊢ let y := (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀;
  y ∈ C

Tactic:
set y := (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀

Premises used: HSub.hSub, HDiv.hDiv, 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
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
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
this : ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C
δ : ℝ
hδ₀ : 0 < δ
hδ₁ : δ < 1
y : E := (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀
hy : y ∈ C
⊢ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x) f

Tactic:
⟨max r (f y), ?_⟩

Premises used: Filter.IsBounded, Max.max, Exists.intro, Filter.IsBoundedUnder
-- 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
x₀ : E
hx₀ : x₀ ∈ C
r : ℝ
hr : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x₀), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x r
x : E
hx : x ∈ C
this : ∀ᶠ (δ : ℝ) in 𝓝 0, (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀ ∈ C
δ : ℝ
hδ₀ : 0 < δ
hδ₁ : δ < 1
y : E := (1 - δ)⁻¹ • x - (δ / (1 - δ)) • x₀
hy : y ∈ C
refine : ∀ᶠ (x : ℝ) in Filter.map f (𝓝 x), (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) x (max r (f y))
⊢ Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x) f

Tactic:
refine ⟨max r (f y), ?_⟩