awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (hypothesis)
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
have 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
Tactic: simp only [locallyLipschitzOn_neg_iff, continuousOn_neg_iff, continuousAt_neg_iff, abs_neg]
    at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
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
have h : ∀ (x : E),
  Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) (𝓝 x) f ↔
    Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x) (-f)
Tactic: convert! this using 8
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
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)
⊢ [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
have h₁ : ∀ a ∈ C,
  Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≥ x2) (𝓝 a) f ↔
    Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 a) (-f)
Tactic: convert! this using 8
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
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
⊢ LocallyLipschitzOn C f ↔ ContinuousOn f C
have inl : ∀ (hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) (hf : ConvexOn ℝ ∅ f),
  LocallyLipschitzOn ∅ f ↔ ContinuousOn f ∅
Tactic: obtain rfl | hC' := C.eq_empty_or_nonempty
Cleared hypotheses: C, hC, hf
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
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 ∅
⊢ LocallyLipschitzOn C f ↔ ContinuousOn f C
have inr : ∀ (hC' : C.Nonempty), LocallyLipschitzOn C f ↔ ContinuousOn f C
Tactic: obtain rfl | hC' := C.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
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
⊢ LocallyLipschitzOn C f
have inl : ∀ (hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅) (hf : ConvexOn ℝ ∅ f), LocallyLipschitzOn ∅ f
Tactic: obtain rfl | ⟨x₀, hx₀⟩ := C.eq_empty_or_nonempty
Cleared hypotheses: C, hC, hf
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
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
⊢ LocallyLipschitzOn C f
have inr : ∀ (x₀ : E) (hx₀ : x₀ ∈ C), LocallyLipschitzOn C f
Tactic: obtain rfl | ⟨x₀, hx₀⟩ := C.eq_empty_or_nonempty
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
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
⊢ LocallyLipschitzOn C f
have 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
Tactic: obtain ⟨b, hx₀b, hbC⟩ := exists_mem_interior_convexHull_affineBasis (hC.mem_nhds hx₀)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
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
have inr : ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
Tactic: refine ((hf.continuousOn_tfae hC ⟨x₀, hx₀⟩).out 3 0).mp ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
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
⊢ ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
have inr : BddAbove
  (f ''
    interior
      ((convexHull ℝ : (a : Set E) → Set E)
        (Set.range (ι := Fin (Module.finrank ℝ E + 1)) (⇑b : (a : Fin (Module.finrank ℝ E + 1)) → E))))
Tactic: refine ⟨x₀, hx₀, BddAbove.isBoundedUnder (IsOpen.mem_nhds isOpen_interior hx₀b) ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Continuous (goal)
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
⊢ f ''
      interior
        ((convexHull ℝ : (a : Set E) → Set E)
          (Set.range (ι := Fin (Module.finrank ℝ E + 1)) (⇑b : (a : Fin (Module.finrank ℝ E + 1)) → E))) ⊆
    f ''
      (convexHull ℝ : (a : Set E) → Set E)
        (Set.range (ι := Fin (Module.finrank ℝ E + 1)) (⇑b : (a : Fin (Module.finrank ℝ E + 1)) → E))
have h : Subset.{u_1} (α := Set E)
  (interior
    ((convexHull ℝ : (a : Set E) → Set E)
      (Set.range (ι := Fin (Module.finrank ℝ E + 1)) (⇑b : (a : Fin (Module.finrank ℝ E + 1)) → E))))
  ((convexHull ℝ : (a : Set E) → Set E)
    (Set.range (ι := Fin (Module.finrank ℝ E + 1)) (⇑b : (a : Fin (Module.finrank ℝ E + 1)) → E)))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.ContinuousLinearEquiv (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Field 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
s : Set E
e : E ≃L[𝕜] F
⊢ StrictConvex.{u_1, u_3} 𝕜 (E := F) ((⇑e : (a : E) → F) '' s) ↔ StrictConvex 𝕜 s
have rw : StrictConvex.{u_1, u_3} 𝕜 (E := F) ((⇑e.symm : (a : F) → E) ⁻¹' s) ↔ StrictConvex 𝕜 s
Tactic: rw [e.image_eq_preimage_symm, e.symm.strictConvex_preimage]
-- Lean 4 proof step from Mathlib.Analysis.Convex.ContinuousLinearEquiv (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Field 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 F
inst_7 : TopologicalSpace F
s : Set E
e : E ≃L[𝕜] F
rw : StrictConvex.{u_1, u_3} 𝕜 (E := F) ((⇑e.symm : (a : F) → E) ⁻¹' s) ↔ StrictConvex 𝕜 s
⊢ StrictConvex.{u_1, u_3} 𝕜 (E := F) ((⇑e : (a : E) → F) '' s) ↔ StrictConvex 𝕜 s
have rw₁ : StrictConvex 𝕜 s ↔ StrictConvex 𝕜 s
Tactic: rw [e.image_eq_preimage_symm, e.symm.strictConvex_preimage]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Contractible (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
s : Set E
x : E
h : StarConvex ℝ x s
hne : s.Nonempty
⊢ ContractibleSpace.{u_1} (↑s : Type u_1)
have refine_1 : ∀ (p : (↑unitInterval : Type) × (↑s : Type u_1)), (↑p.1 : ℝ) • x + (1 - (↑p.1 : ℝ)) • (↑p.2 : E) ∈ s
Tactic: refine
    (contractible_iff_id_nullhomotopic s).2 ⟨⟨x, h.mem hne⟩,
      ⟨⟨⟨fun p ↦ ⟨p.1.1 • x + (1 - p.1.1) • (p.2 : E), ?_⟩, ?_⟩, fun x ↦ by simp, fun x ↦ by simp⟩⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Contractible (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
s : Set E
x : E
h : StarConvex ℝ x s
hne : s.Nonempty
refine_1 : ∀ (p : (↑unitInterval : Type) × (↑s : Type u_1)), (↑p.1 : ℝ) • x + (1 - (↑p.1 : ℝ)) • (↑p.2 : E) ∈ s
⊢ ContractibleSpace.{u_1} (↑s : Type u_1)
have refine_2 : Continuous (Y := (↑s : Type u_1)) fun (p : (↑unitInterval : Type) × (↑s : Type u_1)) ↦
  Subtype.mk (p := fun (x : E) ↦ x ∈ s) ((↑p.1 : ℝ) • x + (1 - (↑p.1 : ℝ)) • (↑p.2 : E)) sorry
Tactic: refine
    (contractible_iff_id_nullhomotopic s).2 ⟨⟨x, h.mem hne⟩,
      ⟨⟨⟨fun p ↦ ⟨p.1.1 • x + (1 - p.1.1) • (p.2 : E), ?_⟩, ?_⟩, fun x ↦ by simp, fun x ↦ by simp⟩⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have hxzD : Icc x z ⊆ D
Tactic: have hxzD : Icc x z ⊆ D := hD.ordConnected.out hx hz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have hxyD : Icc x y ⊆ D
Tactic: have hxyD : Icc x y ⊆ D := (Icc_subset_Icc_right hyz.le).trans hxzD
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have hxyD' : Ioo x y ⊆ interior D
Tactic: have hxyD' : Ioo x y ⊆ interior D :=
        subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hxyD⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have hyzD : Icc y z ⊆ D
Tactic: have hyzD : Icc y z ⊆ D := (Icc_subset_Icc_left hxy.le).trans hxzD
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
hyzD : Icc y z ⊆ D
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have hyzD' : Ioo y z ⊆ interior D
Tactic: have hyzD' : Ioo y z ⊆ interior D :=
        subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hyzD⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
hyzD : Icc y z ⊆ D
hyzD' : Ioo y z ⊆ interior D
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have obtain : ∀ (a : ℝ) (ha : deriv f a = (f y - f x) / (y - x)) (hxa : x < a) (hay : a < y),
  (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
Tactic: obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x) :=
        exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD')
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
hyzD : Icc y z ⊆ D
hyzD' : Ioo y z ⊆ interior D
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have obtain : ∀ (b : ℝ) (hb : deriv f b = (f z - f y) / (z - y)) (hyb : y < b) (hbz : b < z),
  (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
Tactic: obtain ⟨b, ⟨hyb, hbz⟩, hb⟩ : ∃ b ∈ Ioo y z, deriv f b = (f z - f y) / (z - y) :=
        exists_deriv_eq_slope f hyz (hf.mono hyzD) (hf'.mono hyzD')
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_mono : MonotoneOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
hyzD : Icc y z ⊆ D
hyzD' : Ioo y z ⊆ interior D
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hb : deriv f b = (f z - f y) / (z - y)
hyb : y < b
hbz : b < z
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
have rw : deriv f a ≤ deriv f b
Tactic: rw [← ha, ← hb]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (hypothesis)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
have A : DifferentiableOn ℝ f (Ioo x y)
Tactic: have A : DifferentiableOn ℝ f (Ioo x y) := fun w wmem =>
    (differentiableAt_of_deriv_ne_zero (h w wmem)).differentiableWithinAt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
have obtain : ∀ (a : ℝ) (ha : deriv f a = (f y - f x) / (y - x)) (hxa : x < a) (hay : a < y),
  ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
Tactic: obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, deriv f a = (f y - f x) / (y - x) :=
    exists_deriv_eq_slope f hxy hf A
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
have rcases : ∀ (b : ℝ) (hab : a < b) (hby : b < y), ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
Tactic: rcases nonempty_Ioo.2 hay with ⟨b, ⟨hab, hby⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hab : a < b
hby : b < y
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
have refine : (f y - f x) / (y - x) < deriv f b
Tactic: refine ⟨b, ⟨hxa.trans hab, hby⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
A : DifferentiableOn ℝ f (Ioo x y)
a : ℝ
ha : deriv f a = (f y - f x) / (y - x)
hxa : x < a
hay : a < y
b : ℝ
hab : a < b
hby : b < y
⊢ (f y - f x) / (y - x) < deriv f b
have rw : deriv f a < deriv f b
Tactic: rw [← ha]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
have pos : ∀ (h : ∀ w ∈ Ioo x y, deriv f w ≠ 0), ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
Tactic: by_cases! h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
pos : ∀ (h : ∀ w ∈ Ioo x y, deriv f w ≠ 0), ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
have neg : ∀ (h : ∃ w ∈ Ioo x y, deriv f w = 0), ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
Tactic: by_cases! h : ∀ w ∈ Ioo x y, deriv f w ≠ 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
h : ∃ w ∈ Ioo x y, deriv f w = 0
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
have neg : ∀ (w : ℝ) (hw : deriv f w = 0) (hxw : x < w) (hwy : w < y), ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
Tactic: rcases h with ⟨w, ⟨hxw, hwy⟩, hw⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ∃ a ∈ Ioo x w, (f w - f x) / (w - x) < deriv f a
have apply : ContinuousOn f (Icc x w)
Tactic: apply StrictMonoOn.exists_slope_lt_deriv_aux _ hxw _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
apply : ContinuousOn f (Icc x w)
⊢ ∃ a ∈ Ioo x w, (f w - f x) / (w - x) < deriv f a
have apply₁ : StrictMonoOn (deriv f) (Ioo x w)
Tactic: apply StrictMonoOn.exists_slope_lt_deriv_aux _ hxw _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
apply : ContinuousOn f (Icc x w)
apply₁ : StrictMonoOn (deriv f) (Ioo x w)
⊢ ∃ a ∈ Ioo x w, (f w - f x) / (w - x) < deriv f a
have apply₂ : ∀ w_1 ∈ Ioo x w, deriv f w_1 ≠ 0
Tactic: apply StrictMonoOn.exists_slope_lt_deriv_aux _ hxw _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
z : ℝ
hz : z ∈ Ioo x w
⊢ deriv f z ≠ 0
have rw : deriv f z ≠ deriv f w
Tactic: rw [← hw]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
z : ℝ
hz : z ∈ Ioo x w
⊢ deriv f z ≠ deriv f w
have h : deriv f z < deriv f w
Tactic: apply ne_of_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
⊢ ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
have neg : ∀ (a : ℝ) (ha : (f w - f x) / (w - x) < deriv f a) (hxa : x < a) (haw : a < w),
  ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a
Tactic: obtain ⟨a, ⟨hxa, haw⟩, ha⟩ : ∃ a ∈ Ioo x w, (f w - f x) / (w - x) < deriv f a := by
      apply StrictMonoOn.exists_slope_lt_deriv_aux _ hxw _ _
      · exact hf.mono (Icc_subset_Icc le_rfl hwy.le)
      · exact hf'_mono.mono (Ioo_subset_Ioo le_rfl hwy.le)
      · intro z hz
        rw [← hw]
        apply ne_of_lt
        exact hf'_mono ⟨hz.1, hz.2.trans hwy⟩ ⟨hxw, hwy⟩ hz.2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Deriv (goal)
Goal:
x y : ℝ
f : ℝ → ℝ
hf : ContinuousOn f (Icc x y)
hxy : x < y
hf'_mono : StrictMonoOn (deriv f) (Ioo x y)
w : ℝ
hw : deriv f w = 0
hxw : x < w
hwy : w < y
a : ℝ
ha : (f w - f x) / (w - x) < deriv f a
hxa : x < a
haw : a < w
⊢ ∃ b ∈ Ioo w y, (f y - f w) / (y - w) < deriv f b
have apply : ContinuousOn f (Icc w y)
Tactic: apply StrictMonoOn.exists_slope_lt_deriv_aux _ hwy _ _