awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
h : Convex ℝ s
x : E
h_1 : x ∈ s
y : E
h_2 : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
simp_rw simp_rw₁ :
  f (a • x + b • y) ≤ a • f x + b • f y - a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ↔
    f (a • x + b • y) - m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2 ≤
      a • (f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y - m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2)
simp_rw₂ :
  f (a • x + b • y) ≤ a • f x + b • f y - a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ↔
    f (a • x + b • y) ≤
      a • (f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y - m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) +
        m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2
simp_rw₃ :
  f (a • x + b • y) ≤ a * f x + b * f y - a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ↔
    f (a • x + b • y) ≤
      a * (f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b * (f y - m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) +
        m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2
simp_rw₄ :
  f (a • x + b • y) ≤ a * f x + b * f y - a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ↔
    f (a • x + b • y) ≤ a * f x + b * f y - m / 2 * a * b * HPow.hPow (β := ℕ) ‖x - y‖ 2
⊢ f (a • x + b • y) ≤ a • f x + b • f y - a * b * (fun (r : ℝ) ↦ m / 2 * HPow.hPow (β := ℕ) r 2) ‖x - y‖ ↔
    (fun (x : E) ↦ f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) (a • x + b • y) ≤
      HSMul.hSMul (β := ℝ) a ((fun (x : E) ↦ f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) x) +
        HSMul.hSMul (β := ℝ) b ((fun (x : E) ↦ f x - m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) y)
have simp_rw₅ : f (a • x + b • y) ≤ a * f x + b * f y - a * (b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2)) ↔
  f (a • x + b • y) ≤ a * f x + b * f y - m / 2 * (a * (b * HPow.hPow (β := ℕ) ‖x - y‖ 2))
Tactic: simp_rw [sub_le_iff_le_add, smul_eq_mul, aux_sub ha hb hab, mul_assoc, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
⊢ StrongConcaveOn s m f ↔ ConcaveOn ℝ (β := ℝ) s fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2
have refine : Convex ℝ s →
  ∀ x ∈ s,
    ∀ y ∈ s,
      ∀ (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
        a • f x + b • f y + a * b * (fun (r : ℝ) ↦ m / 2 * HPow.hPow (β := ℕ) r 2) ‖x - y‖ ≤ f (a • x + b • y) ↔
          HSMul.hSMul (β := ℝ) a ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) x) +
              HSMul.hSMul (β := ℝ) b ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) y) ≤
            (fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) (a • x + b • y)
Tactic: refine and_congr_right fun _ ↦ forall₄_congr fun x _ y _ ↦ forall₅_congr fun a b ha hb hab ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
h : Convex ℝ s
x : E
h_1 : x ∈ s
y : E
h_2 : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
simp_rw simp_rw₁ :
  a • f x + b • f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a • (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) ≤
      f (a • x + b • y) + m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2
⊢ a • f x + b • f y + a * b * (fun (r : ℝ) ↦ m / 2 * HPow.hPow (β := ℕ) r 2) ‖x - y‖ ≤ f (a • x + b • y) ↔
    HSMul.hSMul (β := ℝ) a ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) x) +
        HSMul.hSMul (β := ℝ) b ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) y) ≤
      (fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) (a • x + b • y)
have simp_rw₂ : a • f x + b • f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
  a • (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) -
      m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2 ≤
    f (a • x + b • y)
Tactic: simp_rw [← sub_le_iff_le_add, smul_eq_mul, aux_add ha hb hab, mul_assoc, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
h : Convex ℝ s
x : E
h_1 : x ∈ s
y : E
h_2 : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
simp_rw simp_rw₁ :
  a • f x + b • f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a • (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) ≤
      f (a • x + b • y) + m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2
simp_rw₂ :
  a • f x + b • f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a • (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) -
        m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2 ≤
      f (a • x + b • y)
⊢ a • f x + b • f y + a * b * (fun (r : ℝ) ↦ m / 2 * HPow.hPow (β := ℕ) r 2) ‖x - y‖ ≤ f (a • x + b • y) ↔
    HSMul.hSMul (β := ℝ) a ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) x) +
        HSMul.hSMul (β := ℝ) b ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) y) ≤
      (fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) (a • x + b • y)
have simp_rw₃ : a * f x + b * f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
  a * (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b * (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) -
      m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2 ≤
    f (a • x + b • y)
Tactic: simp_rw [← sub_le_iff_le_add, smul_eq_mul, aux_add ha hb hab, mul_assoc, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
h : Convex ℝ s
x : E
h_1 : x ∈ s
y : E
h_2 : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
simp_rw simp_rw₁ :
  a • f x + b • f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a • (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) ≤
      f (a • x + b • y) + m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2
simp_rw₂ :
  a • f x + b • f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a • (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) -
        m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2 ≤
      f (a • x + b • y)
simp_rw₃ :
  a * f x + b * f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a * (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b * (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) -
        m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2 ≤
      f (a • x + b • y)
⊢ a • f x + b • f y + a * b * (fun (r : ℝ) ↦ m / 2 * HPow.hPow (β := ℕ) r 2) ‖x - y‖ ≤ f (a • x + b • y) ↔
    HSMul.hSMul (β := ℝ) a ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) x) +
        HSMul.hSMul (β := ℝ) b ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) y) ≤
      (fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) (a • x + b • y)
have simp_rw₄ : a * f x + b * f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
  a * f x + b * f y + m / 2 * a * b * HPow.hPow (β := ℕ) ‖x - y‖ 2 ≤ f (a • x + b • y)
Tactic: simp_rw [← sub_le_iff_le_add, smul_eq_mul, aux_add ha hb hab, mul_assoc, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strong (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
s : Set E
m : ℝ
f : E → ℝ
h : Convex ℝ s
x : E
h_1 : x ∈ s
y : E
h_2 : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
simp_rw simp_rw₁ :
  a • f x + b • f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a • (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) ≤
      f (a • x + b • y) + m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2
simp_rw₂ :
  a • f x + b • f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a • (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b • (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) -
        m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2 ≤
      f (a • x + b • y)
simp_rw₃ :
  a * f x + b * f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a * (f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) + b * (f y + m / 2 * HPow.hPow (β := ℕ) ‖y‖ 2) -
        m / 2 * HPow.hPow (β := ℕ) ‖a • x + b • y‖ 2 ≤
      f (a • x + b • y)
simp_rw₄ :
  a * f x + b * f y + a * b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2) ≤ f (a • x + b • y) ↔
    a * f x + b * f y + m / 2 * a * b * HPow.hPow (β := ℕ) ‖x - y‖ 2 ≤ f (a • x + b • y)
⊢ a • f x + b • f y + a * b * (fun (r : ℝ) ↦ m / 2 * HPow.hPow (β := ℕ) r 2) ‖x - y‖ ≤ f (a • x + b • y) ↔
    HSMul.hSMul (β := ℝ) a ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) x) +
        HSMul.hSMul (β := ℝ) b ((fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) y) ≤
      (fun (x : E) ↦ f x + m / 2 * HPow.hPow (β := ℕ) ‖x‖ 2) (a • x + b • y)
have simp_rw₅ : a * f x + b * f y + a * (b * (m / 2 * HPow.hPow (β := ℕ) ‖x - y‖ 2)) ≤ f (a • x + b • y) ↔
  a * f x + b * f y + m / 2 * (a * (b * HPow.hPow (β := ℕ) ‖x - y‖ 2)) ≤ f (a • x + b • y)
Tactic: simp_rw [← sub_le_iff_le_add, smul_eq_mul, aux_add ha hb hab, mul_assoc, mul_left_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
r ε : ℝ
hε : 0 ≤ ε
⊢ closedBall r ε = [r - ε -[ℝ] r + ε]
have rw : Icc (r - ε) (r + ε) = [r - ε -[ℝ] r + ε]
Tactic: rw [closedBall_eq_Icc, segment_eq_Icc ((sub_le_self _ hε).trans <| le_add_of_nonneg_right hε)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
r ε : ℝ
hε : 0 ≤ ε
rw : Icc (r - ε) (r + ε) = [r - ε -[ℝ] r + ε]
⊢ closedBall r ε = [r - ε -[ℝ] r + ε]
have rw₁ : Icc (r - ε) (r + ε) = Icc (r - ε) (r + ε)
Tactic: rw [closedBall_eq_Icc, segment_eq_Icc ((sub_le_self _ hε).trans <| le_add_of_nonneg_right hε)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
r ε : ℝ
hε : 0 < ε
⊢ ball r ε = openSegment ℝ (r - ε) (r + ε)
have rw : Ioo (r - ε) (r + ε) = openSegment ℝ (r - ε) (r + ε)
Tactic: rw [ball_eq_Ioo, openSegment_eq_Ioo ((sub_lt_self _ hε).trans <| lt_add_of_pos_right _ hε)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
r ε : ℝ
hε : 0 < ε
rw : Ioo (r - ε) (r + ε) = openSegment ℝ (r - ε) (r + ε)
⊢ ball r ε = openSegment ℝ (r - ε) (r + ε)
have rw₁ : Ioo (r - ε) (r + ε) = Ioo (r - ε) (r + ε)
Tactic: rw [ball_eq_Ioo, openSegment_eq_Ioo ((sub_lt_self _ hε).trans <| lt_add_of_pos_right _ hε)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DenselyOrdered 𝕜
inst_4 : TopologicalSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : AddCommGroup E
inst_7 : TopologicalSpace E
inst_8 : ContinuousAdd E
inst_9 : Module 𝕜 E
inst_10 : ContinuousSMul 𝕜 E
x y : E
⊢ [x -[𝕜] y] ⊆ closure (openSegment 𝕜 x y)
have rw : Subset.{u_3} (α := Set E) ((fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' closure (Ioo 0 1))
  (closure ((fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' Ioo 0 1))
Tactic: rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : DenselyOrdered 𝕜
inst_4 : PseudoMetricSpace 𝕜
inst_5 : OrderTopology 𝕜
inst_6 : ProperSpace 𝕜
inst_7 : CompactIccSpace 𝕜
inst_8 : AddCommGroup E
inst_9 : TopologicalSpace E
inst_10 : T2Space E
inst_11 : ContinuousAdd E
inst_12 : Module 𝕜 E
inst_13 : ContinuousSMul 𝕜 E
x y : E
⊢ closure (openSegment 𝕜 x y) = [x -[𝕜] y]
have rw : Eq.{u_3 + 1} (α := Set E) (closure ((fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' Ioo 0 1))
  ((fun (θ : 𝕜) ↦ (1 - θ) • x + θ • y) '' closure (Ioo 0 1))
Tactic: rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 < a
hb : 0 ≤ b
hab : a + b = 1
⊢ interior (a • s) + closure (b • s) = interior (a • s) + b • s
have rw : interior (a • s) + b • s = interior (a • s) + b • s
Tactic: rw [isOpen_interior.add_closure (b • s)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a • closure s + b • interior s ⊆ interior s
have rw : b • interior s + a • closure s ⊆ interior s
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
inst_4 : TopologicalSpace E
inst_5 : IsTopologicalAddGroup E
inst_6 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 < b
hab : a + b = 1
⊢ a • s + b • interior s ⊆ interior s
have rw : b • interior s + a • s ⊆ interior s
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h :
  (s \ interior s).Pairwise fun (x y : E) ↦
    ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
⊢ StrictConvex 𝕜 s
have refine : s.Pairwise fun (x y : E) ↦ openSegment 𝕜 x y ⊆ interior s
Tactic: refine strictConvex_iff_openSegment_subset.2 ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h :
  (s \ interior s).Pairwise fun (x y : E) ↦
    ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
⊢ openSegment 𝕜 x y ⊆ interior s
have pos : ∀ (hx' : x ∈ interior s), openSegment 𝕜 x y ⊆ interior s
Tactic: by_cases hx' : x ∈ interior s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h :
  (s \ interior s).Pairwise fun (x y : E) ↦
    ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
pos : ∀ (hx' : x ∈ interior s), openSegment 𝕜 x y ⊆ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
have neg : ∀ (hx' : x ∉ interior s), openSegment 𝕜 x y ⊆ interior s
Tactic: by_cases hx' : x ∈ interior s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h :
  (s \ interior s).Pairwise fun (x y : E) ↦
    ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : x ∉ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
have pos : ∀ (hy' : y ∈ interior s), openSegment 𝕜 x y ⊆ interior s
Tactic: by_cases hy' : y ∈ interior s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h :
  (s \ interior s).Pairwise fun (x y : E) ↦
    ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : x ∉ interior s
pos : ∀ (hy' : y ∈ interior s), openSegment 𝕜 x y ⊆ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
have neg : ∀ (hy' : y ∉ interior s), openSegment 𝕜 x y ⊆ interior s
Tactic: by_cases hy' : y ∈ interior s
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h :
  (s \ interior s).Pairwise fun (x y : E) ↦
    ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : x ∉ interior s
hy' : y ∉ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
have neg : ∀ (c : 𝕜) (hc : Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)),
  openSegment 𝕜 x y ⊆ interior s
Tactic: rcases h ⟨hx, hx'⟩ ⟨hy, hy'⟩ hne with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h :
  (s \ interior s).Pairwise fun (x y : E) ↦
    ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : x ∉ interior s
hy' : y ∉ interior s
c : 𝕜
hc : Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
⊢ openSegment 𝕜 x y ⊆ interior s
have neg : openSegment 𝕜 x ((lineMap x y : (a : 𝕜) → E) c) ⊆ interior s
Tactic: refine (openSegment_subset_union x y ⟨c, rfl⟩).trans
    (insert_subset_iff.2 ⟨hc, union_subset ?_ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h :
  (s \ interior s).Pairwise fun (x y : E) ↦
    ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hne : x ≠ y
hx' : x ∉ interior s
hy' : y ∉ interior s
c : 𝕜
hc : Membership.mem (α := E) (interior s) ((lineMap x y : (a : 𝕜) → E) c : E)
neg : openSegment 𝕜 x ((lineMap x y : (a : 𝕜) → E) c) ⊆ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
have neg₁ : openSegment 𝕜 ((lineMap x y : (a : 𝕜) → E) c) y ⊆ interior s
Tactic: refine (openSegment_subset_union x y ⟨c, rfl⟩).trans
    (insert_subset_iff.2 ⟨hc, union_subset ?_ ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun (x y : E) ↦ ([x -[𝕜] y] \ frontier s).Nonempty
⊢ StrictConvex 𝕜 s
have refine : ∀ (x : E) (hx : x ∈ s \ interior s) (y : E) (hy : y ∈ s \ interior s),
  x ≠ y →
    (fun ⦃a b : E⦄ ↦
        ([a -[𝕜] b] \ frontier s).Nonempty →
          ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap a b : (a : 𝕜) → E) c : E))
      (a := x) (b := y)
Tactic: refine hs.strictConvex' <| h.imp_on fun x hx y hy _ => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun (x y : E) ↦ ([x -[𝕜] y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
h_1 : x ≠ y
⊢ (fun ⦃a b : E⦄ ↦
      ([a -[𝕜] b] \ frontier s).Nonempty →
        ∃ (c : 𝕜), Membership.mem (α := E) (interior s) ((lineMap a b : (a : 𝕜) → E) c : E))
    (a := x) (b := y)
have simp : (image.{u_2, u_3} (α := 𝕜) (⇑(lineMap x y) : (a : 𝕜) → E) (Icc 0 1) \ frontier s).Nonempty →
  ∃ (c : 𝕜), Membership.mem (α := E) (s \ frontier s) ((lineMap x y : (a : 𝕜) → E) c : E)
Tactic: simp only [segment_eq_image_lineMap, ← self_diff_frontier]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
h : (s \ interior s).Pairwise fun (x y : E) ↦ ([x -[𝕜] y] \ frontier s).Nonempty
x : E
hx : x ∈ s \ interior s
y : E
hy : y ∈ s \ interior s
h_1 : x ≠ y
c : 𝕜
hc : Membership.mem (γ := Set 𝕜) (Icc 0 1) c
hcs : ((lineMap x y : (a : 𝕜) → E) c : E) ∉ frontier s
⊢ ∃ (c : 𝕜), Membership.mem (α := E) (s \ frontier s) ((lineMap x y : (a : 𝕜) → E) c : E)
have refine : Membership.mem (α := E) [x -[𝕜] y] ((lineMap x y : (a : 𝕜) → E) c : E)
Tactic: refine ⟨c, hs.segment_subset hx.1 hy.1 ?_, hcs⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : TopologicalSpace 𝕜
inst_8 : OrderTopology 𝕜
inst_9 : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
hs' : (interior s).Nonempty
⊢ interior (closure s) = interior s
have refine : interior (closure s) ⊆ interior s
Tactic: refine subset_antisymm ?_ (interior_mono subset_closure)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : TopologicalSpace 𝕜
inst_8 : OrderTopology 𝕜
inst_9 : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
hs' : (interior s).Nonempty
y : E
hy : y ∈ interior (closure s)
⊢ y ∈ interior s
have rcases : ∀ (x : E) (hx : x ∈ interior s), y ∈ interior s
Tactic: rcases hs' with ⟨x, hx⟩
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (hypothesis)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : TopologicalSpace 𝕜
inst_8 : OrderTopology 𝕜
inst_9 : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
⊢ y ∈ interior s
have h : (AffineMap.lineMap x y : (a : 𝕜) → E) 1 = y
Tactic: have h := AffineMap.lineMap_apply_one (k := 𝕜) x y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Topology (goal)
Goal:
𝕜 : Type u_2
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : TopologicalSpace E
inst_6 : IsTopologicalAddGroup E
inst_7 : TopologicalSpace 𝕜
inst_8 : OrderTopology 𝕜
inst_9 : ContinuousSMul 𝕜 E
s : Set E
hs : Convex 𝕜 s
y : E
hy : y ∈ interior (closure s)
x : E
hx : x ∈ interior s
h : (AffineMap.lineMap x y : (a : 𝕜) → E) 1 = y
⊢ y ∈ interior s
have obtain : ∀ (t : 𝕜) (ht1 : 1 < t) (ht : Membership.mem (α := E) (closure s) ((AffineMap.lineMap x y : (a : 𝕜) → E) t : E)),
  y ∈ interior s
Tactic: obtain ⟨t, ht1, ht⟩ := AffineMap.lineMap_continuous.tendsto' _ _ h |>.eventually_mem
    (mem_interior_iff_mem_nhds.1 hy) |>.exists_gt