awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
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
w : F
hw : Membership.mem (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) w
ht : IsCompact.{u_1} (X := E) {x : E | x ∈ s ∧ (f : (a : E) → F) x = w}
ht₀ : Set.Nonempty.{u_1} (α := E) {x : E | x ∈ s ∧ (f : (a : E) → F) x = w}
⊢ Membership.mem (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints ℝ s) w
have obtain : ∀ (x : E) (hx : x ∈ s)
  (hw :
    Membership.mem.{u_2, u_2} (α := F) (γ := Set F) (extremePoints ℝ ((⇑f : (a : E) → F) '' s))
      ((f : (a : E) → F) x : F))
  (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),
  Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints ℝ s) ((f : (a : E) → F) x : F)
Tactic: obtain ⟨x, ⟨hx, rfl⟩, hyt⟩ := ht.extremePoints_nonempty ht₀
Cleared hypotheses: w, hw, ht, ht₀
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
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) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) ((f : (a : E) → F) x : F)
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
⊢ Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((⇑f : (a : E) → F) '' extremePoints ℝ s) ((f : (a : E) → F) x : F)
have refine : ∀ (y : E) (hy : y ∈ s) (z : E) (hz : z ∈ s) (hxyz : x ∈ openSegment ℝ y z), y = x
Tactic: refine mem_image_of_mem _ ⟨hx, fun y hy z hz hxyz ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (hypothesis)
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) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) ((f : (a : E) → F) x : F)
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
⊢ y = x
have 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)
Tactic: have := by simpa using image_openSegment _ f.toAffineMap y z
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
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) (extremePoints ℝ ((⇑f : (a : E) → F) '' s)) ((f : (a : E) → F) x : F)
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)
⊢ y = x
have rw : ∀
  (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)),
  y = x
Tactic: rw [mem_extremePoints] at hw
Cleared hypotheses: hw, ht, ht₀, hyt, y, hy, z, hz, hxyz, this
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (goal)
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)
⊢ Membership.mem.{u_2, u_2} (α := F) (γ := Set F) (openSegment ℝ ((f : (a : E) → F) y) ((f : (a : E) → F) z) : Set F)
    ((f : (a : E) → F) x : F)
have rw : Membership.mem.{u_2, u_2} (α := F) (γ := Set F) ((fun (a : E) ↦ (f : (a : E) → F) a) '' openSegment ℝ y z)
  ((f : (a : E) → F) x : F)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Analysis.Convex.KreinMilman (hypothesis)
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)
⊢ y = x
have 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)
Tactic: have := hw.2 _ (mem_image_of_mem _ hy) _ (mem_image_of_mem _ hz) <| by
    rw [← this]; exact mem_image_of_mem _ hxyz
-- Lean 4 proof step from Mathlib.Analysis.Convex.LinearIsometry (goal)
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) (closedBall 0 r)
have 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))
Tactic: rw [← f.isometry.preimage_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
have inl : ∀ (hspan : Ne (α := AffineSubspace ℝ E) (affineSpan ℝ s) ⊤),
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases ne_or_eq (affineSpan ℝ s) ⊤ with hspan | hspan
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr : ∀ (hspan : Eq (α := AffineSubspace ℝ E) (affineSpan ℝ s) ⊤),
  Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases ne_or_eq (affineSpan ℝ s) ⊤ with hspan | hspan
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
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∞)
have inl : frontier s ⊆ (↑(affineSpan ℝ s) : Set E)
Tactic: refine measure_mono_null ?_ (addHaar_affineSubspace _ _ hspan)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (hypothesis)
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) ⊤
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
have hspan₁ : (interior s).Nonempty
Tactic: rw [← hs.interior_nonempty_iff_affineSpan_eq_top] at hspan
Cleared hypotheses: hspan
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr : ∀ (x : E) (hx : x ∈ interior s), Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rcases hspan with ⟨x, hx⟩
Cleared hypotheses: hspan
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
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∞)
have refine : ∀ (n : ℕ), x ∈ interior (s ∩ B n)
Tactic: refine measure_iUnion_null fun n =>
        H _ (hs.inter (convex_ball _ _)) ?_ (isBounded_ball.subset inter_subset_right)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
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 ∩ B n)
have rw : x ∈ interior s ∩ ball x (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
Tactic: rw [interior_inter, isOpen_ball.interior_eq]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (hypothesis)
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∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
have this : 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)⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
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∞)
have refine : ∀ (y : E) (hy : y ∈ frontier s), Membership.mem (γ := Set E) (⋃ (n : ℕ), frontier (s ∩ B n)) y
Tactic: refine measure_mono_null (fun y hy => ?_) this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
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
have refine : y ∈ frontier (s ∩ B N)
Tactic: refine mem_iUnion.2 ⟨N, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (hypothesis)
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⌋₊
⊢ y ∈ frontier (s ∩ B N)
have hN : y ∈ B N
Tactic: have hN : y ∈ B N := by simp [B, N, Nat.lt_floor_add_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
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⌋₊
hN : y ∈ B N
⊢ y ∈ frontier (s ∩ B N)
have suffices : y ∈ frontier (s ∩ B N) ∩ B N
Tactic: suffices y ∈ frontier (s ∩ B N) ∩ B N from this.1
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
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⌋₊
hN : y ∈ B N
⊢ y ∈ frontier (s ∩ B N) ∩ B N
have rw : y ∈ frontier s ∩ ball x (HAdd.hAdd (α := ℝ) (↑N : ℝ) 1)
Tactic: rw [frontier_inter_open_inter isOpen_ball]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
have inr : ∀ (t : Set E),
  Convex ℝ t →
    x ∈ interior t → Bornology.IsBounded t → Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier t) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: suffices H : ∀ t : Set E, Convex ℝ t → x ∈ interior t → IsBounded t → μ (frontier t) = 0 by
    let B : ℕ → Set E := fun n => ball x (n + 1)
    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)⟩
    refine measure_mono_null (fun y hy => ?_) this; clear this
    set N : ℕ := ⌊dist y x⌋₊
    refine mem_iUnion.2 ⟨N, ?_⟩
    have hN : y ∈ B N := by simp [B, N, Nat.lt_floor_add_one]
    suffices y ∈ frontier (s ∩ B N) ∩ B N from this.1
    rw [frontier_inter_open_inter isOpen_ball]
    exact ⟨hy, hN⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Measure (hypothesis)
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_1 : Set E
hs_1 : Convex ℝ s_1
x : E
hx_1 : x ∈ interior s_1
s : Set E
hs : Convex ℝ s
hx : x ∈ interior s
hb : Bornology.IsBounded s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (frontier s) : ℝ≥0∞) (0 : ℝ≥0∞)
have hb₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) (interior s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: replace hb : μ (interior s) ≠ ∞ := (hb.subset interior_subset).measure_lt_top.ne
Cleared hypotheses: hb