awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw :
  Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' s) ((f : (a : E) → F) x : F) ∧
    ∀ (x₁ : F),
      Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₁ →
        ∀ (x₂ : F),
          Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₂ →
            Membership.mem (α := F) (openSegment ℝ x₁ x₂) ((f : (a : E) → F) x : F) →
              x₁ = (f : (a : E) → F) x ∧ x₂ = (f : (a : E) → F) x
ht :
  IsCompact.{u_1} (X := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
ht₀ :
  Set.Nonempty.{u_1} (α := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
hyt :
  ∀ ⦃x₁ : E⦄,
    Membership.mem (γ := Set E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₁ →
      ∀ ⦃x₂ : E⦄,
        Membership.mem (γ := Set E)
            {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₂ →
          x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this :
  Eq.{u_2 + 1} (α := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z : Set F)
    (openSegment ℝ ((f : (a : E) → F) y) ((f : (a : E) → F) z) : Set F)
⊢ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) y : F) ((f : (a : E) → F) x : F) ∧
    Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) z : F) ((f : (a : E) → F) x : F)

Tactic:
have := hw.2 _ (mem_image_of_mem _ hy) _ (mem_image_of_mem _ hz) <| by
    rw [← this]; exact mem_image_of_mem _ hxyz
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw :
  Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' s) ((f : (a : E) → F) x : F) ∧
    ∀ (x₁ : F),
      Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₁ →
        ∀ (x₂ : F),
          Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₂ →
            Membership.mem (α := F) (openSegment ℝ x₁ x₂) ((f : (a : E) → F) x : F) →
              x₁ = (f : (a : E) → F) x ∧ x₂ = (f : (a : E) → F) x
ht :
  IsCompact.{u_1} (X := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
ht₀ :
  Set.Nonempty.{u_1} (α := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
hyt :
  ∀ ⦃x₁ : E⦄,
    Membership.mem (γ := Set E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₁ →
      ∀ ⦃x₂ : E⦄,
        Membership.mem (γ := Set E)
            {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₂ →
          x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this_1 :
  Eq.{u_2 + 1} (α := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z : Set F)
    (openSegment ℝ ((f : (a : E) → F) y) ((f : (a : E) → F) z) : Set F)
this :
  Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) y : F) ((f : (a : E) → F) x : F) ∧
    Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) z : F) ((f : (a : E) → F) x : F)
⊢ y = x

Tactic:
hyt ⟨hy, this.1⟩ ⟨hz, this.2⟩ hxyz

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Convex.KreinMilman
Goal:
E : Type u_1
F : Type u_2
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : T2Space E
inst_4 : IsTopologicalAddGroup E
inst_5 : ContinuousSMul ℝ E
inst_6 : LocallyConvexSpace ℝ E
s : Set E
inst_7 : AddCommGroup F
inst_8 : Module ℝ F
inst_9 : TopologicalSpace F
inst_10 : T1Space F
f : E →ᴬ[ℝ] F
hs : IsCompact s
x : E
hx : x ∈ s
hw :
  Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' s) ((f : (a : E) → F) x : F) ∧
    ∀ (x₁ : F),
      Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₁ →
        ∀ (x₂ : F),
          Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' s) x₂ →
            Membership.mem (α := F) (openSegment ℝ x₁ x₂) ((f : (a : E) → F) x : F) →
              x₁ = (f : (a : E) → F) x ∧ x₂ = (f : (a : E) → F) x
ht :
  IsCompact.{u_1} (X := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
ht₀ :
  Set.Nonempty.{u_1} (α := E)
    {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)}
hyt :
  ∀ ⦃x₁ : E⦄,
    Membership.mem (γ := Set E)
        {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₁ →
      ∀ ⦃x₂ : E⦄,
        Membership.mem (γ := Set E)
            {x_1 : E | x_1 ∈ s ∧ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x_1 : F) ((f : (a : E) → F) x : F)} x₂ →
          x ∈ openSegment ℝ x₁ x₂ → x₁ = x
y : E
hy : y ∈ s
z : E
hz : z ∈ s
hxyz : x ∈ openSegment ℝ y z
this_1 :
  Eq.{u_2 + 1} (α := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z : Set F)
    (openSegment ℝ ((f : (a : E) → F) y) ((f : (a : E) → F) z) : Set F)
this :
  Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) y : F) ((f : (a : E) → F) x : F) ∧
    Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) z : F) ((f : (a : E) → F) x : F)
⊢ y = x

Tactic:
exact hyt ⟨hy, this.1⟩ ⟨hz, this.2⟩ hxyz

Premises used: And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Convex.LinearIsometry
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
s : Set F
e : E ≃ₗᵢ[𝕜] F
⊢ StrictConvex.{u_1, u_2} 𝕜 (E := E) ((⇑e : (a : E) → F) ⁻¹' s) ↔ StrictConvex 𝕜 s

Tactic:
e.toContinuousLinearEquiv.strictConvex_preimage

Premises used: LinearIsometryEquiv.toContinuousLinearEquiv, ContinuousLinearEquiv.strictConvex_preimage
-- Module: Mathlib.Analysis.Convex.LinearIsometry
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : SeminormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
s : Set E
e : E ≃ₗᵢ[𝕜] F
⊢ StrictConvex.{u_1, u_3} 𝕜 (E := F) ((⇑e : (a : E) → F) '' s) ↔ StrictConvex 𝕜 s

Tactic:
e.toContinuousLinearEquiv.strictConvex_image

Premises used: ContinuousLinearEquiv.strictConvex_image, LinearIsometryEquiv.toContinuousLinearEquiv
-- Module: Mathlib.Analysis.Convex.LinearIsometry
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : SeminormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
s : Set F
hs : StrictConvex 𝕜 s
e : E →ₗᵢ[𝕜] F
⊢ StrictConvex.{u_1, u_2} 𝕜 (E := E) ((⇑e : (a : E) → F) ⁻¹' s)

Tactic:
hs.linear_preimage _ e.continuous e.injective

Premises used: StrictConvex.linear_preimage, LinearIsometry.continuous, LinearIsometry.injective
-- Module: Mathlib.Analysis.Convex.LinearIsometry
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
e : E ≃ₗᵢ[𝕜] F
⊢ StrictConvexSpace 𝕜 E ↔ StrictConvexSpace 𝕜 F

Tactic:
simp only [strictConvexSpace_iff, ← map_zero e, ← e.image_closedBall, e.strictConvex_image]

Premises used: LinearIsometryEquiv.map_zero, strictConvexSpace_iff, LinearIsometryEquiv.strictConvex_image, LinearIsometryEquiv.image_closedBall
-- Module: Mathlib.Analysis.Convex.LinearIsometry
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
e : E →ₗᵢ[𝕜] F
⊢ StrictConvexSpace.{u_1, u_3} 𝕜
      ↥(LinearMap.range
          (↑e :
            [inst_6 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F)) ↔
    StrictConvexSpace 𝕜 E

Tactic:
e.equivRange.strictConvexSpace_iff.symm

Premises used: Set.Mem, LinearIsometryEquiv.strictConvexSpace_iff, SemilinearMapClass.semilinearMap, LinearIsometry.equivRange, Iff.symm
-- Module: Mathlib.Analysis.Convex.LinearIsometry
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : StrictConvexSpace 𝕜 E
e : E →ₗᵢ[𝕜] F
⊢ StrictConvexSpace.{u_1, u_3} 𝕜
    ↥(LinearMap.range
        (↑e : [inst_7 : FunLike (E →ₗᵢ[𝕜] F) E F] → [SemilinearMapClass (E →ₗᵢ[𝕜] F) (RingHom.id 𝕜) E F] → E →ₗ[𝕜] F))

Tactic:
e.strictConvexSpace_range_iff.mpr ‹_›

Premises used: Iff.mpr, LinearIsometry.strictConvexSpace_range_iff
-- Module: Mathlib.Analysis.Convex.LinearIsometry
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : StrictConvexSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
r : ℝ
hr : 0 < r
rw :
  StrictConvex.{u_1, u_2} 𝕜 (E := E)
    (preimage.{u_2, u_3} (β := F) ((⇑f : (a : E) → F) : (a : E) → F) (closedBall ((f : (a : E) → F) 0) r : Set F))
⊢ StrictConvex.{u_1, u_2} 𝕜 (E := E) (closedBall 0 r)

Tactic:
rw [← f.isometry.preimage_closedBall]

Premises used: Isometry.preimage_closedBall, LinearIsometry.isometry
-- Module: Mathlib.Analysis.Convex.LinearIsometry
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : StrictConvexSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
r : ℝ
hr : 0 < r
⊢ StrictConvex.{u_1, u_2} 𝕜 (E := E)
    (preimage.{u_2, u_3} (β := F) ((⇑f : (a : E) → F) : (a : E) → F) (closedBall ((f : (a : E) → F) 0) r : Set F))

Tactic:
(strictConvex_closedBall _ _ _).linearIsometry_preimage _

Premises used: strictConvex_closedBall, StrictConvex.linearIsometry_preimage
-- Module: Mathlib.Analysis.Convex.LinearIsometry
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : StrictConvexSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
r : ℝ
hr : 0 < r
⊢ StrictConvex.{u_1, u_2} 𝕜 (E := E)
    (preimage.{u_2, u_3} (β := F) ((⇑f : (a : E) → F) : (a : E) → F) (closedBall ((f : (a : E) → F) 0) r : Set F))

Tactic:
exact (strictConvex_closedBall _ _ _).linearIsometry_preimage _

Premises used: strictConvex_closedBall, StrictConvex.linearIsometry_preimage
-- Module: Mathlib.Analysis.Convex.LinearIsometry
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NormedField 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedAddCommGroup F
inst_5 : NormedSpace 𝕜 F
inst_6 : StrictConvexSpace 𝕜 E
p : Submodule 𝕜 E
⊢ StrictConvexSpace.{u_1, u_2} 𝕜 ↥p

Tactic:
p.subtypeₗᵢ.strictConvexSpace

Premises used: Set.Mem, LinearIsometry.strictConvexSpace, Submodule.subtypeₗᵢ
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
inl :
  ∀ (hspan : Ne (α := AffineSubspace ℝ E) (affineSpan ℝ s) ⊤),
    Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
inr :
  ∀ (hspan : Eq (α := AffineSubspace ℝ E) (affineSpan ℝ s) ⊤),
    Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases ne_or_eq (affineSpan ℝ s) ⊤ with hspan | hspan

Premises used: ne_or_eq, Real, affineSpan, Top.top
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
hspan : Ne (α := AffineSubspace ℝ E) (affineSpan ℝ s) ⊤
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null ?_ (addHaar_affineSubspace _ _ hspan)

Premises used: MeasureTheory.measure_mono_null, MeasureTheory.Measure.addHaar_affineSubspace
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
hspan : Ne (α := AffineSubspace ℝ E) (affineSpan ℝ s) ⊤
inl : frontier s ⊆ (↑(affineSpan ℝ s) : Set E)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine measure_mono_null ?_ (addHaar_affineSubspace _ _ hspan)

Premises used: MeasureTheory.measure_mono_null, MeasureTheory.Measure.addHaar_affineSubspace
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
hspan : Ne (α := AffineSubspace ℝ E) (affineSpan ℝ s) ⊤
⊢ frontier s ⊆ (↑(affineSpan ℝ s) : Set E)

Tactic:
frontier_subset_closure.trans
      (closure_minimal (subset_affineSpan _ _) (affineSpan ℝ s).closed_of_finiteDimensional)

Premises used: Real, closure_minimal, HasSubset.Subset.trans, AffineSubspace.closed_of_finiteDimensional, subset_affineSpan, affineSpan, frontier_subset_closure
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
hspan : Ne (α := AffineSubspace ℝ E) (affineSpan ℝ s) ⊤
⊢ frontier s ⊆ (↑(affineSpan ℝ s) : Set E)

Tactic:
exact frontier_subset_closure.trans
      (closure_minimal (subset_affineSpan _ _) (affineSpan ℝ s).closed_of_finiteDimensional)

Premises used: Real, closure_minimal, HasSubset.Subset.trans, AffineSubspace.closed_of_finiteDimensional, subset_affineSpan, affineSpan, frontier_subset_closure
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
hspan : Eq (α := AffineSubspace ℝ E) (affineSpan ℝ s) ⊤
⊢ (interior s).Nonempty

Tactic:
rw [← hs.interior_nonempty_iff_affineSpan_eq_top] at hspan

Premises used: Convex.interior_nonempty_iff_affineSpan_eq_top
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
hspan : (interior s).Nonempty
inr : ∀ (x : E) (hx : x ∈ interior s), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rcases hspan with ⟨x, hx⟩
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), frontier (s ∩ B n)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_iUnion_null fun n =>
        H _ (hs.inter (convex_ball _ _)) ?_ (isBounded_ball.subset inter_subset_right)

Premises used: Metric.isBounded_ball, MeasureTheory.measure_iUnion_null, Convex.inter, Nat.cast, convex_ball, Inter.inter, HAdd.hAdd, Bornology.IsBounded.subset, OfNat.ofNat, Set.inter_subset_right
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
refine : ∀ (n : ℕ), x ∈ interior (s ∩ B n)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), frontier (s ∩ B n)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine measure_iUnion_null fun n =>
        H _ (hs.inter (convex_ball _ _)) ?_ (isBounded_ball.subset inter_subset_right)

Premises used: Metric.isBounded_ball, MeasureTheory.measure_iUnion_null, Metric.ball, Convex.inter, convex_ball, Inter.inter, Bornology.IsBounded.subset, Set.inter_subset_right
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
n : ℕ
rw : x ∈ interior s ∩ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ x ∈ interior (s ∩ B n)

Tactic:
rw [interior_inter, isOpen_ball.interior_eq]

Premises used: interior_inter, Metric.isOpen_ball, IsOpen.interior_eq
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
n : ℕ
⊢ x ∈ interior s ∩ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
⟨hx, mem_ball_self (add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one)⟩

Premises used: Set.Mem, Nat.cast_nonneg, setOf, Metric.mem_ball_self, Set.inter, zero_lt_one, add_pos_of_nonneg_of_pos, And.intro
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
n : ℕ
⊢ x ∈ interior s ∩ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)

Tactic:
exact ⟨hx, mem_ball_self (add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one)⟩
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), frontier (s ∩ B n)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have : μ (⋃ n : ℕ, frontier (s ∩ B n)) = 0 := by
      refine measure_iUnion_null fun n =>
        H _ (hs.inter (convex_ball _ _)) ?_ (isBounded_ball.subset inter_subset_right)
      rw [interior_inter, isOpen_ball.interior_eq]
      exact ⟨hx, mem_ball_self (add_pos_of_nonneg_of_pos n.cast_nonneg zero_lt_one)⟩
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), frontier (s ∩ B n)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
measure_mono_null (fun y hy => ?_) this

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
this : Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (⋃ (n : ℕ), frontier (s ∩ B n)) : ℝ≥0∞) (0 : ℝ≥0∞)
refine : ∀ (y : E) (hy : y ∈ frontier s), Membership.mem (γ := Set E) (⋃ (n : ℕ), frontier (s ∩ B n)) y
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine measure_mono_null (fun y hy => ?_) this

Premises used: MeasureTheory.measure_mono_null
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
⊢ Membership.mem (γ := Set E) (⋃ (n : ℕ), frontier (s ∩ B n)) y

Tactic:
mem_iUnion.2 ⟨N, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro
-- Module: Mathlib.Analysis.Convex.Measure
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : MeasurableSpace E
inst_3 : BorelSpace E
inst_4 : FiniteDimensional ℝ E
μ : Measure E
inst_5 : μ.IsAddHaarMeasure
s : Set E
hs : Convex ℝ s
x : E
hx : x ∈ interior s
H :
  ∀ (t : Set E),
    Convex ℝ t →
      x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
B : ℕ → Set E := fun (n : ℕ) ↦ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
y : E
hy : y ∈ frontier s
N : ℕ := ⌊dist y x⌋₊
refine : y ∈ frontier (s ∩ B N)
⊢ Membership.mem (γ := Set E) (⋃ (n : ℕ), frontier (s ∩ B n)) y

Tactic:
refine mem_iUnion.2 ⟨N, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro