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 → ℝ
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
inr : ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f
⊢ LocallyLipschitzOn C f

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

Premises used: ConvexOn.continuousOn_tfae, List.TFAE.out, Exists.intro, Iff.mp, OfNat.ofNat
-- 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
⊢ ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f

Tactic:
⟨x₀, hx₀, BddAbove.isBoundedUnder (IsOpen.mem_nhds isOpen_interior hx₀b) ?_⟩

Premises used: isOpen_interior, BddAbove.isBoundedUnder, And.intro, IsOpen.mem_nhds, Exists.intro
-- 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
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))))
⊢ ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) ↦ x1 ≤ x2) (𝓝 x₀) f

Tactic:
refine ⟨x₀, hx₀, BddAbove.isBoundedUnder (IsOpen.mem_nhds isOpen_interior hx₀b) ?_⟩
-- 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
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)))
⊢ 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))

Tactic:
gcongr
-- 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
⊢ 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:
interior_subset

Premises used: interior_subset
-- 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
⊢ 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:
exact interior_subset

Premises used: interior_subset
-- 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
⊢ 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:
exact (hf.bddAbove_convexHull ((subset_convexHull ..).trans hbC)
      ((finite_range _).image _).bddAbove).mono (by gcongr; exact interior_subset)

Premises used: subset_convexHull, ConvexOn.bddAbove_convexHull, HasSubset.Subset.trans, Set.finite_range, Set.Finite.image, Set.Finite.bddAbove, BddAbove.mono
-- 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 : ConcaveOn ℝ C f
⊢ LocallyLipschitzOn C f

Tactic:
simpa using hf.neg.locallyLipschitzOn hC

Premises used: ConvexOn.locallyLipschitzOn, 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
⊢ ContinuousOn f C

Tactic:
(hf.locallyLipschitzOn hC).continuousOn

Premises used: LocallyLipschitzOn.continuousOn, ConvexOn.locallyLipschitzOn
-- 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 : ConcaveOn ℝ C f
⊢ ContinuousOn f C

Tactic:
(hf.locallyLipschitzOn hC).continuousOn

Premises used: LocallyLipschitzOn.continuousOn, ConcaveOn.locallyLipschitzOn
-- 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
hf : ConvexOn ℝ C f
⊢ LocallyLipschitzOn (interior C) f

Tactic:
(hf.subset interior_subset hf.1.interior).locallyLipschitzOn isOpen_interior

Premises used: interior_subset, isOpen_interior, Convex.interior, And.left, ConvexOn.locallyLipschitzOn, ConvexOn.subset
-- 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
hf : ConcaveOn ℝ C f
⊢ LocallyLipschitzOn (interior C) f

Tactic:
(hf.subset interior_subset hf.1.interior).locallyLipschitzOn isOpen_interior

Premises used: interior_subset, isOpen_interior, ConcaveOn.subset, Convex.interior, And.left, ConcaveOn.locallyLipschitzOn
-- 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
hf : ConvexOn ℝ C f
⊢ ContinuousOn f (interior C)

Tactic:
hf.locallyLipschitzOn_interior.continuousOn

Premises used: LocallyLipschitzOn.continuousOn, ConvexOn.locallyLipschitzOn_interior
-- 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
hf : ConcaveOn ℝ C f
⊢ ContinuousOn f (interior C)

Tactic:
hf.locallyLipschitzOn_interior.continuousOn

Premises used: ConcaveOn.locallyLipschitzOn_interior, LocallyLipschitzOn.continuousOn
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
inst_2 : FiniteDimensional ℝ E
hf : ConvexOn ℝ univ f
⊢ LocallyLipschitz f

Tactic:
simpa using hf.locallyLipschitzOn_interior

Premises used: ConvexOn.locallyLipschitzOn_interior
-- Module: Mathlib.Analysis.Convex.Continuous
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
inst_2 : FiniteDimensional ℝ E
hf : ConcaveOn ℝ univ f
⊢ LocallyLipschitz f

Tactic:
simpa using hf.locallyLipschitzOn_interior

Premises used: ConcaveOn.locallyLipschitzOn_interior
-- Module: Mathlib.Analysis.Convex.ContinuousLinearEquiv
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 F
e : E ≃L[𝕜] F
⊢ StrictConvex.{u_1, u_2} 𝕜 (E := E) ((⇑e : (a : E) → F) ⁻¹' s) ↔ StrictConvex 𝕜 s

Tactic:
⟨fun h ↦ Function.LeftInverse.preimage_preimage e.right_inv s ▸
    h.linear_preimage e.symm.toLinearMap e.symm.continuous e.symm.injective,
    fun h ↦ h.linear_preimage e.toLinearMap e.continuous e.injective⟩

Premises used: ContinuousLinearEquiv.symm, Function.LeftInverse.preimage_preimage, LinearEquiv.right_inv, ContinuousLinearEquiv.toLinearEquiv, Eq.rec, ContinuousLinearEquiv.injective, StrictConvex.linear_preimage, LinearEquiv.toLinearMap, ContinuousLinearEquiv.continuous, Iff.intro
-- Module: Mathlib.Analysis.Convex.ContinuousLinearEquiv
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
rw₁ rw₂ : StrictConvex 𝕜 s ↔ StrictConvex 𝕜 s
⊢ StrictConvex.{u_1, u_3} 𝕜 (E := F) ((⇑e : (a : E) → F) '' s) ↔ StrictConvex 𝕜 s

Tactic:
rw [e.image_eq_preimage_symm, e.symm.strictConvex_preimage]

Premises used: ContinuousLinearEquiv.symm, ContinuousLinearEquiv.image_eq_preimage_symm, ContinuousLinearEquiv.strictConvex_preimage
-- Module: Mathlib.Analysis.Convex.Contractible
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_1 : E
h : StarConvex ℝ x_1 s
hne : s.Nonempty
x : (↑s : Type u_1)
⊢ Eq (α := (↑s : Type u_1))
    (ContinuousMap.toFun (X := (↑unitInterval : Type) × (↑s : Type u_1))
      {
        toFun := fun (p : (↑unitInterval : Type) × (↑s : Type u_1)) ↦
          Subtype.mk (p := fun (x : E) ↦ x ∈ s) ((↑p.1 : ℝ) • x_1 + (1 - (↑p.1 : ℝ)) • (↑p.2 : E)) ⋯,
        continuous_toFun := ⋯ }
      (0, x))
    ((ContinuousMap.id (↑s : Type u_1) : (a : (↑s : Type u_1)) → (↑s : Type u_1)) x)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Contractible
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_1 : E
h : StarConvex ℝ x_1 s
hne : s.Nonempty
x : (↑s : Type u_1)
⊢ Eq (α := (↑s : Type u_1))
    (ContinuousMap.toFun (X := (↑unitInterval : Type) × (↑s : Type u_1))
      {
        toFun := fun (p : (↑unitInterval : Type) × (↑s : Type u_1)) ↦
          Subtype.mk (p := fun (x : E) ↦ x ∈ s) ((↑p.1 : ℝ) • x_1 + (1 - (↑p.1 : ℝ)) • (↑p.2 : E)) ⋯,
        continuous_toFun := ⋯ }
      (1, x))
    ((ContinuousMap.const (↑s : Type u_1) (Subtype.mk (p := fun (x : E) ↦ x ∈ s) x_1 ⋯) :
        (a : (↑s : Type u_1)) → (↑s : Type u_1))
      x)

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Contractible
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
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)) ⋯
⊢ ContractibleSpace.{u_1} (↑s : Type u_1)

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⟩⟩⟩

Premises used: Iff.mpr, ContinuousMap.mk, HSub.hSub, Set.Elem, contractible_iff_id_nullhomotopic, Nonempty.intro, Prod.fst, Subtype.mk, HAdd.hAdd, Exists.intro, HSMul.hSMul, OfNat.ofNat, Subtype.val, ContinuousMap.Homotopy.mk, Prod.snd, StarConvex.mem
-- Module: Mathlib.Analysis.Convex.Contractible
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
p : (↑unitInterval : Type) × (↑s : Type u_1)
⊢ (↑p.1 : ℝ) • x + (1 - (↑p.1 : ℝ)) • (↑p.2 : E) ∈ s

Tactic:
h p.2.2 p.1.2.1 (sub_nonneg.2 p.1.2.2) (add_sub_cancel _ _)

Premises used: Iff.mpr, Prod.fst, And.right, add_sub_cancel, And.left, sub_nonneg, Prod.snd, Subtype.property
-- Module: Mathlib.Analysis.Convex.Contractible
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
p : (↑unitInterval : Type) × (↑s : Type u_1)
⊢ (↑p.1 : ℝ) • x + (1 - (↑p.1 : ℝ)) • (↑p.2 : E) ∈ s

Tactic:
exact h p.2.2 p.1.2.1 (sub_nonneg.2 p.1.2.2) (add_sub_cancel _ _)

Premises used: Iff.mpr, Prod.fst, And.right, add_sub_cancel, And.left, sub_nonneg, Prod.snd, Subtype.property
-- Module: Mathlib.Analysis.Convex.Contractible
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
⊢ Continuous (Y := E) fun (p : (↑unitInterval : Type) × (↑s : Type u_1)) ↦
    (↑p.1 : ℝ) • x + (1 - (↑p.1 : ℝ)) • (↑p.2 : E)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Convex.Contractible
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
⊢ 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)) ⋯

Tactic:
exact Continuous.subtype_mk (by fun_prop) _

Premises used: Continuous.subtype_mk
-- Module: Mathlib.Analysis.Convex.Contractible
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
hs : Convex ℝ s
hne : s.Nonempty
⊢ ContractibleSpace.{u_1} (↑s : Type u_1)

Tactic:
let ⟨_, hx⟩ := hne
  (hs.starConvex hx).contractibleSpace hne

Premises used: StarConvex.contractibleSpace, Set.Elem, ContractibleSpace, _private.0.Convex.contractibleSpace.match_1, Convex.starConvex
-- Module: Mathlib.Analysis.Convex.Contractible
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
⊢ ContractibleSpace E

Tactic:
(Homeomorph.Set.univ E).contractibleSpace_iff.mp <|
    convex_univ.contractibleSpace Set.univ_nonempty

Premises used: Homeomorph.Set.univ, Homeomorph.contractibleSpace_iff, Set.univ_nonempty, Convex.contractibleSpace, convex_univ, Iff.mp
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ Icc x z ⊆ D

Tactic:
have hxzD : Icc x z ⊆ D := hD.ordConnected.out hx hz
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ Icc x y ⊆ D

Tactic:
have hxyD : Icc x y ⊆ D := (Icc_subset_Icc_right hyz.le).trans hxzD
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ 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⟩
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ Icc y z ⊆ D

Tactic:
have hyzD : Icc y z ⊆ D := (Icc_subset_Icc_left hxy.le).trans hxzD
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ 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⟩
-- Module: Mathlib.Analysis.Convex.Deriv
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 ∈ Ioo x y, deriv f a = (f y - f x) / (y - x)

Tactic:
exists_deriv_eq_slope f hxy (hf.mono hxyD) (hf'.mono hxyD')

Premises used: ContinuousOn.mono, DifferentiableOn.mono, exists_deriv_eq_slope
-- Module: Mathlib.Analysis.Convex.Deriv
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
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)
⊢ (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')

Premises used: HSub.hSub, ContinuousOn.mono, DifferentiableOn.mono, exists_deriv_eq_slope, Set.Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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 ∈ Ioo y z, deriv f b = (f z - f y) / (z - y)

Tactic:
exists_deriv_eq_slope f hyz (hf.mono hyzD) (hf'.mono hyzD')

Premises used: ContinuousOn.mono, DifferentiableOn.mono, exists_deriv_eq_slope
-- Module: Mathlib.Analysis.Convex.Deriv
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
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)
⊢ (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')

Premises used: HSub.hSub, ContinuousOn.mono, DifferentiableOn.mono, exists_deriv_eq_slope, Set.Ioo
-- Module: Mathlib.Analysis.Convex.Deriv
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
rw : deriv f a ≤ deriv f b
⊢ (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)

Tactic:
rw [← ha, ← hb]
-- Module: Mathlib.Analysis.Convex.Deriv
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
⊢ deriv f a ≤ deriv f b

Tactic:
hf'_mono (hxyD' ⟨hxa, hay⟩) (hyzD' ⟨hyb, hbz⟩) (hay.trans hyb).le

Premises used: LT.lt.le, And.intro, LT.lt.trans