mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: 𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : IsHomeomorph e
he : ∀ (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
⊢ f ∘ Subtype.val ⁻¹' f '' s = Subtype.val ⁻¹' s

Tactic:
ext x
  refine ⟨fun ⟨_, hy, hfy⟩ ↦ ?_ , fun hx ↦ ⟨_, hx, rfl⟩⟩
  change (x : P) ∈ s
  rwa [exists_eq_subtype_mk_iff.mp ⟨subset_affineSpan 𝕜 s hy, he_homeo.injective <| Subtype.ext <|
      by simpa [he] using hfy.symm⟩]

Goal state after:
Module: Mathlib.Analysis.Convex.Measure

Goal state before:
pp: case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s ≠ ⊤
⊢ μ (frontier s) = 0

pp: case inr
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s = ⊤
⊢ μ (frontier s) = 0

Tactic:
·

Goal state after:
case inl
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
hspan : affineSpan ℝ s ≠ ⊤
⊢ μ (frontier s) = 0
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inl
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
e : [Nonempty ↑∅] → ↥(affineSpan 𝕜 ∅) → ↥(affineSpan 𝕜 (f '' ∅))
he_homeo : ∀ [inst : Nonempty ↑∅], IsHomeomorph e
he : ∀ [inst : Nonempty ↑∅] (x : ↥(affineSpan 𝕜 ∅)), ↑(e x) = f ↑x
⊢ intrinsicInterior 𝕜 (f '' ∅) = f '' intrinsicInterior 𝕜 ∅

pp: case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
⊢ intrinsicInterior 𝕜 (f '' s) = f '' intrinsicInterior 𝕜 s

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
e : [Nonempty ↑∅] → ↥(affineSpan 𝕜 ∅) → ↥(affineSpan 𝕜 (f '' ∅))
he_homeo : ∀ [inst : Nonempty ↑∅], IsHomeomorph e
he : ∀ [inst : Nonempty ↑∅] (x : ↥(affineSpan 𝕜 ∅)), ↑(e x) = f ↑x
⊢ intrinsicInterior 𝕜 (f '' ∅) = f '' intrinsicInterior 𝕜 ∅
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
⊢ intrinsicInterior 𝕜 (f '' s) = f '' intrinsicInterior 𝕜 s

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
⊢ intrinsicInterior 𝕜 (f '' s) = f '' intrinsicInterior 𝕜 s
Module: Mathlib.Analysis.Convex.Integral

Goal state before:
pp: case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
h0' : μ (toMeasurable μ t)ᶜ = 0
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

pp: case neg
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
h0' : ¬μ (toMeasurable μ t)ᶜ = 0
⊢ ⨍ (x : α), f x ∂μ ∈ interior s

Tactic:
·

Goal state after:
case pos
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
s : Set E
t : Set α
f : α → E
inst✝ : IsFiniteMeasure μ
hs : Convex ℝ s
h0 : μ (toMeasurable μ t) ≠ 0
hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s
hfi : Integrable f μ
ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s
h0' : μ (toMeasurable μ t)ᶜ = 0
⊢ ⨍ (x : α), f x ∂μ ∈ interior s
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inl
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
e : [Nonempty ↑∅] → ↥(affineSpan 𝕜 ∅) → ↥(affineSpan 𝕜 (f '' ∅))
he_homeo : ∀ [inst : Nonempty ↑∅], IsHomeomorph e
he : ∀ [inst : Nonempty ↑∅] (x : ↥(affineSpan 𝕜 ∅)), ↑(e x) = f ↑x
⊢ intrinsicFrontier 𝕜 (f '' ∅) = f '' intrinsicFrontier 𝕜 ∅

pp: case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
⊢ intrinsicFrontier 𝕜 (f '' s) = f '' intrinsicFrontier 𝕜 s

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
e : [Nonempty ↑∅] → ↥(affineSpan 𝕜 ∅) → ↥(affineSpan 𝕜 (f '' ∅))
he_homeo : ∀ [inst : Nonempty ↑∅], IsHomeomorph e
he : ∀ [inst : Nonempty ↑∅] (x : ↥(affineSpan 𝕜 ∅)), ↑(e x) = f ↑x
⊢ intrinsicFrontier 𝕜 (f '' ∅) = f '' intrinsicFrontier 𝕜 ∅
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
⊢ intrinsicFrontier 𝕜 (f '' s) = f '' intrinsicFrontier 𝕜 s

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
⊢ intrinsicFrontier 𝕜 (f '' s) = f '' intrinsicFrontier 𝕜 s
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hf : ConvexOn ℝ ∅ f
⊢ LocallyLipschitzOn ∅ f ↔ ContinuousOn f ∅

pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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:
·

Goal state after:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hf : ConvexOn ℝ ∅ f
⊢ LocallyLipschitzOn ∅ f ↔ ContinuousOn f ∅
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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:
·

Goal state after:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : 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
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hf : ConvexOn ℝ ∅ f
⊢ LocallyLipschitzOn ∅ f

pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
C : Set E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConvexOn ℝ C f
x₀ : E
hx₀ : x₀ ∈ C
⊢ LocallyLipschitzOn C f

Tactic:
·

Goal state after:
case inl
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] ∅
hf : ConvexOn ℝ ∅ f
⊢ LocallyLipschitzOn ∅ f
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
C : Set E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConvexOn ℝ C f
x₀ : E
hx₀ : x₀ ∈ C
⊢ LocallyLipschitzOn C f

Tactic:
·

Goal state after:
case inr
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
C : Set E
f : E → ℝ
inst✝ : FiniteDimensional ℝ E
hC : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] C
hf : ConvexOn ℝ C f
x₀ : E
hx₀ : x₀ ∈ C
⊢ LocallyLipschitzOn C f
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inl
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
e : [Nonempty ↑∅] → ↥(affineSpan 𝕜 ∅) → ↥(affineSpan 𝕜 (f '' ∅))
he_homeo : ∀ [inst : Nonempty ↑∅], IsHomeomorph e
he : ∀ [inst : Nonempty ↑∅] (x : ↥(affineSpan 𝕜 ∅)), ↑(e x) = f ↑x
⊢ intrinsicClosure 𝕜 (f '' ∅) = f '' intrinsicClosure 𝕜 ∅

pp: case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
⊢ intrinsicClosure 𝕜 (f '' s) = f '' intrinsicClosure 𝕜 s

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
e : [Nonempty ↑∅] → ↥(affineSpan 𝕜 ∅) → ↥(affineSpan 𝕜 (f '' ∅))
he_homeo : ∀ [inst : Nonempty ↑∅], IsHomeomorph e
he : ∀ [inst : Nonempty ↑∅] (x : ↥(affineSpan 𝕜 ∅)), ↑(e x) = f ↑x
⊢ intrinsicClosure 𝕜 (f '' ∅) = f '' intrinsicClosure 𝕜 ∅
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
⊢ intrinsicClosure 𝕜 (f '' s) = f '' intrinsicClosure 𝕜 s

Tactic:
·

Goal state after:
case inr
𝕜 : Type u_1
V : Type u_2
W : Type u_3
Q : Type u_4
P : Type u_5
inst✝⁸ : Ring 𝕜
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module 𝕜 V
inst✝⁵ : TopologicalSpace P
inst✝⁴ : AddTorsor V P
inst✝³ : AddCommGroup W
inst✝² : Module 𝕜 W
inst✝¹ : TopologicalSpace Q
inst✝ : AddTorsor W Q
f : P → Q
s : Set P
e : [Nonempty ↑s] → ↥(affineSpan 𝕜 s) → ↥(affineSpan 𝕜 (f '' s))
he_homeo : ∀ [inst : Nonempty ↑s], IsHomeomorph e
he : ∀ [inst : Nonempty ↑s] (x : ↥(affineSpan 𝕜 s)), ↑(e x) = f ↑x
hs : s.Nonempty
⊢ intrinsicClosure 𝕜 (f '' s) = f '' intrinsicClosure 𝕜 s
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inl
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
hx : y ∈ Ici y
⊢ ContinuousWithinAt f (Ici y) y

pp: case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ici y
hxy : y < x
⊢ ContinuousWithinAt f (Ici y) x

Tactic:
·

Goal state after:
case inl
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
hx : y ∈ Ici y
⊢ ContinuousWithinAt f (Ici y) y
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ici y
hxy : y < x
⊢ ContinuousWithinAt f (Ici y) x

Tactic:
·

Goal state after:
case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ici y
hxy : y < x
⊢ ContinuousWithinAt f (Ici y) x
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ici y
hxy : y < x
h : y < x → ContinuousWithinAt f (Ioi y) x
⊢ ContinuousWithinAt f (Ici y) x

Tactic:
rw [continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hxy)] at h

Goal state after:
case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Ici y) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ici y
hxy : y < x
h : y < x → ContinuousAt f x
⊢ ContinuousWithinAt f (Ici y) x
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inl
f : ℝ → ℝ
x : ℝ
hf_cvx : ConvexOn ℝ (Iic x) f
hf_cont : ContinuousWithinAt f (Iic x) x
hx : x ∈ Iic x
⊢ ContinuousWithinAt f (Iic x) x

pp: case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Iic y) f
hf_cont : ContinuousWithinAt f (Iic y) y
x : ℝ
hx : x ∈ Iic y
hxy : x < y
⊢ ContinuousWithinAt f (Iic y) x

Tactic:
·

Goal state after:
case inl
f : ℝ → ℝ
x : ℝ
hf_cvx : ConvexOn ℝ (Iic x) f
hf_cont : ContinuousWithinAt f (Iic x) x
hx : x ∈ Iic x
⊢ ContinuousWithinAt f (Iic x) x
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Iic y) f
hf_cont : ContinuousWithinAt f (Iic y) y
x : ℝ
hx : x ∈ Iic y
hxy : x < y
⊢ ContinuousWithinAt f (Iic y) x

Tactic:
·

Goal state after:
case inr
f : ℝ → ℝ
y : ℝ
hf_cvx : ConvexOn ℝ (Iic y) f
hf_cont : ContinuousWithinAt f (Iic y) y
x : ℝ
hx : x ∈ Iic y
hxy : x < y
⊢ ContinuousWithinAt f (Iic y) x
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inl
f : ℝ → ℝ
y x : ℝ
hf_cvx : ConvexOn ℝ (Ioc y x) f
hf_cont : ContinuousWithinAt f (Iic x) x
hx : x ∈ Ioc y x
⊢ ContinuousWithinAt f (Ioc y x) x

pp: case inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ioc y z) f
hf_cont : ContinuousWithinAt f (Iic z) z
x : ℝ
hx : x ∈ Ioc y z
hxz : x < z
⊢ ContinuousWithinAt f (Ioc y z) x

Tactic:
·

Goal state after:
case inl
f : ℝ → ℝ
y x : ℝ
hf_cvx : ConvexOn ℝ (Ioc y x) f
hf_cont : ContinuousWithinAt f (Iic x) x
hx : x ∈ Ioc y x
⊢ ContinuousWithinAt f (Ioc y x) x
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ioc y z) f
hf_cont : ContinuousWithinAt f (Iic z) z
x : ℝ
hx : x ∈ Ioc y z
hxz : x < z
⊢ ContinuousWithinAt f (Ioc y z) x

Tactic:
·

Goal state after:
case inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ioc y z) f
hf_cont : ContinuousWithinAt f (Iic z) z
x : ℝ
hx : x ∈ Ioc y z
hxz : x < z
⊢ ContinuousWithinAt f (Ioc y z) x
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inl
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
hx : y ∈ Ico y z
⊢ ContinuousWithinAt f (Ico y z) y

pp: case inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ico y z
hyx : y < x
⊢ ContinuousWithinAt f (Ico y z) x

Tactic:
·

Goal state after:
case inl
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
hx : y ∈ Ico y z
⊢ ContinuousWithinAt f (Ico y z) y
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ico y z
hyx : y < x
⊢ ContinuousWithinAt f (Ico y z) x

Tactic:
·

Goal state after:
case inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Ico y z) f
hf_cont : ContinuousWithinAt f (Ici y) y
x : ℝ
hx : x ∈ Ico y z
hyx : y < x
⊢ ContinuousWithinAt f (Ico y z) x
Module: Mathlib.Analysis.Convex.Intrinsic

Goal state before:
pp: case refine_1
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
⊢ (∃ y,
      (∀ (o : Set ↥(affineSpan 𝕜 s)),
          IsOpen[instTopologicalSpaceSubtype] o → y ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty) ∧
        ↑y = x) →
    ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty

pp: case refine_2
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
⊢ ∀ (o : Set ↥(affineSpan 𝕜 s)),
    IsOpen[instTopologicalSpaceSubtype] o → ⟨x, ?refine_3⟩ ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty

pp: case refine_3
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
h : ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
⊢ x ∈ affineSpan 𝕜 s

Tactic:
·

Goal state after:
case refine_1
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : CompleteSpace 𝕜
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedSpace 𝕜 V
inst✝² : FiniteDimensional 𝕜 V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Set P
x : P
⊢ (∃ y,
      (∀ (o : Set ↥(affineSpan 𝕜 s)),
          IsOpen[instTopologicalSpaceSubtype] o → y ∈ o → (o ∩ Subtype.val ⁻¹' s).Nonempty) ∧
        ↑y = x) →
    ∀ (o : Set P), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] o → x ∈ o → (o ∩ s).Nonempty
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inl
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
this : ContinuousOn f (Ico y z) ∧ ContinuousOn f (Ioc y z)
hx : y ∈ Icc y z
⊢ ContinuousWithinAt f (Icc y z) y

pp: case inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
this : ContinuousOn f (Ico y z) ∧ ContinuousOn f (Ioc y z)
x : ℝ
hx : x ∈ Icc y z
hyx : y < x
⊢ ContinuousWithinAt f (Icc y z) x

Tactic:
·

Goal state after:
case inl
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
this : ContinuousOn f (Ico y z) ∧ ContinuousOn f (Ioc y z)
hx : y ∈ Icc y z
⊢ ContinuousWithinAt f (Icc y z) y
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case inr.inl
f : ℝ → ℝ
y : ℝ
hfy : ContinuousWithinAt f (Ici y) y
x : ℝ
hyx : y < x
hf_cvx : ConvexOn ℝ (Icc y x) f
hyz : y < x
hfz : ContinuousWithinAt f (Iic x) x
this : ContinuousOn f (Ico y x) ∧ ContinuousOn f (Ioc y x)
hx : x ∈ Icc y x
⊢ ContinuousWithinAt f (Icc y x) x

pp: case inr.inr
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
this : ContinuousOn f (Ico y z) ∧ ContinuousOn f (Ioc y z)
x : ℝ
hx : x ∈ Icc y z
hyx : y < x
hxz : x < z
⊢ ContinuousWithinAt f (Icc y z) x

Tactic:
·

Goal state after:
case inr.inl
f : ℝ → ℝ
y : ℝ
hfy : ContinuousWithinAt f (Ici y) y
x : ℝ
hyx : y < x
hf_cvx : ConvexOn ℝ (Icc y x) f
hyz : y < x
hfz : ContinuousWithinAt f (Iic x) x
this : ContinuousOn f (Ico y x) ∧ ContinuousOn f (Ioc y x)
hx : x ∈ Icc y x
⊢ ContinuousWithinAt f (Icc y x) x
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case refine_1
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
⊢ ConvexOn ℝ (Ico y z) f

pp: case refine_2
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
⊢ ConvexOn ℝ (Ioc y z) f

Tactic:
·

Goal state after:
case refine_1
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
⊢ ConvexOn ℝ (Ico y z) f
Module: Mathlib.Analysis.Convex.Continuous

Goal state before:
pp: case refine_2
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
⊢ ConvexOn ℝ (Ioc y z) f

Tactic:
·

Goal state after:
case refine_2
f : ℝ → ℝ
y z : ℝ
hf_cvx : ConvexOn ℝ (Icc y z) f
hyz : y < z
hfy : ContinuousWithinAt f (Ici y) y
hfz : ContinuousWithinAt f (Iic z) z
⊢ ConvexOn ℝ (Ioc y z) f