awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (hypothesis)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : Nontrivial E
S : Set E
x : E
h : x ∈ interior S ∩ extremePoints ℝ S
x_int : S ∈ 𝓝 x
x_ext : x ∈ extremePoints ℝ S
h₁ : ∀ᶠ (v : E) in 𝓝[≠] 0, x - v ∈ S
⊢ Membership.mem (γ := Set E) ∅ x
have h₂ : ∀ᶠ (v : E) in 𝓝[≠] 0, x + v ∈ S
Tactic: have h₂ : ∀ᶠ v in 𝓝[≠] 0, x + v ∈ S :=
    (tendsto_inf_left <| (continuous_const_add _).tendsto' _ _ (add_zero _)).eventually x_int
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : Nontrivial E
S : Set E
x : E
h : x ∈ interior S ∩ extremePoints ℝ S
x_int : S ∈ 𝓝 x
x_ext : x ∈ extremePoints ℝ S
h₁ : ∀ᶠ (v : E) in 𝓝[≠] 0, x - v ∈ S
h₂ : ∀ᶠ (v : E) in 𝓝[≠] 0, x + v ∈ S
⊢ Membership.mem (γ := Set E) ∅ x
have obtain : ∀ (v : E) (v_ne : v ≠ 0) (hv₁ : x - v ∈ S) (hv₂ : x + v ∈ S), Membership.mem (γ := Set E) ∅ x
Tactic: obtain ⟨v, ⟨hv₁, hv₂⟩, (v_ne : v ≠ 0)⟩ := h₁.and h₂ |>.and eventually_mem_nhdsWithin |>.exists
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (hypothesis)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : IsTopologicalAddGroup E
inst_4 : ContinuousSMul ℝ E
inst_5 : Nontrivial E
S : Set E
x : E
h : x ∈ interior S ∩ extremePoints ℝ S
x_int : S ∈ 𝓝 x
x_ext : x ∈ extremePoints ℝ S
h₁ : ∀ᶠ (v : E) in 𝓝[≠] 0, x - v ∈ S
h₂ : ∀ᶠ (v : E) in 𝓝[≠] 0, x + v ∈ S
v : E
v_ne : v ≠ 0
hv₁ : x - v ∈ S
hv₂ : x + v ∈ S
⊢ Membership.mem (γ := Set E) ∅ x
have key : x ∈ openSegment ℝ (x - v) (x + v)
Tactic: have key : x ∈ openSegment ℝ (x - v) (x + v) := mem_openSegment_sub_add _ _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
⊢ C \ interior C ⊆ extremePoints 𝕜 C
have refine : ∀ (x : A) (hx : x ∈ C \ interior C) (y : A) (hy : y ∈ C) (z : A) (hz : z ∈ C),
  x ∈ openSegment 𝕜 y z → ∀ (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1) (hxab : a • y + b • z = x), y = x
Tactic: refine fun x hx ↦ ⟨hx.1, fun y hy z hz ⟨a, b, ha, hb, hab, hxab⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
h : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • z = x
⊢ y = z
have by_contra : ∀ (this : ¬y = z), False
Tactic: by_contra
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (hypothesis)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
h : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • z = x
⊢ y = x
have hyz : y = z
Tactic: have hyz : y = z := by
    by_contra
    exact hx.2 <| hxab ▸ hc hy hz this ha hb hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
h : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • z = x
hyz : y = z
⊢ y = x
have rwa : ∀ (hxab : a • y + b • y = x) (hyz : y = z), y = x
Tactic: rwa [← hyz, ← add_smul, hab, one_smul] at hxab
Cleared hypotheses: hxab, hyz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
h : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • z = x
hyz : y = z
rwa : ∀ (hxab : a • y + b • y = x) (hyz : y = z), y = x
⊢ y = x
have rwa₁ : ∀ (hxab : (a + b) • y = x) (hyz : y = z), y = x
Tactic: rwa [← hyz, ← add_smul, hab, one_smul] at hxab
Cleared hypotheses: hxab, hyz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
h : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • z = x
hyz : y = z
rwa : ∀ (hxab : a • y + b • y = x) (hyz : y = z), y = x
rwa₁ : ∀ (hxab : (a + b) • y = x) (hyz : y = z), y = x
⊢ y = x
have rwa₂ : ∀ (hxab : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y = x) (hyz : y = z), y = x
Tactic: rwa [← hyz, ← add_smul, hab, one_smul] at hxab
Cleared hypotheses: hxab, hyz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (goal)
Goal:
𝕜 : Type u_1
A : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid A
inst_3 : Module 𝕜 A
inst_4 : TopologicalSpace A
C : Set A
hc : StrictConvex 𝕜 C
x : A
hx : x ∈ C \ interior C
y : A
hy : y ∈ C
z : A
hz : z ∈ C
h : x ∈ openSegment 𝕜 y z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hxab : a • y + b • z = x
hyz : y = z
rwa : ∀ (hxab : a • y + b • y = x) (hyz : y = z), y = x
rwa₁ : ∀ (hxab : (a + b) • y = x) (hyz : y = z), y = x
rwa₂ : ∀ (hxab : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y = x) (hyz : y = z), y = x
⊢ y = x
have rwa₃ : ∀ (hxab : y = x) (hyz : y = z), y = x
Tactic: rwa [← hyz, ← add_smul, hab, one_smul] at hxab
Cleared hypotheses: hxab, hyz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : NormedSpace ℝ A
inst_2 : Nontrivial A
x : A
r : ℝ
⊢ extremePoints ℝ (closedBall x r) ⊆ sphere x r
have rw : extremePoints ℝ (closedBall x r) ⊆ closedBall x r ∧
  Disjoint (extremePoints ℝ (closedBall x r)) (interior (closedBall x r))
Tactic: rw [← closedBall_diff_ball, subset_diff, ← interior_closedBall' _]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (hypothesis)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : NormedSpace ℝ A
inst_2 : StrictConvexSpace ℝ A
a : A
r : ℝ
hr : r ≠ 0
x : A
hx : x ∈ sphere a r
⊢ x ∈ extremePoints ℝ (closedBall a r)
have hx₁ : x ∈ closedBall a r \ interior (closedBall a r)
Tactic: rw [← frontier_closedBall _ hr, frontier, closure_closedBall] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : NormedSpace ℝ A
inst_2 : Nontrivial A
x : A
r : ℝ
inst_3 : StrictConvexSpace ℝ A
⊢ extremePoints ℝ (closedBall x r) = sphere x r
have rw : closedBall x r \ interior (closedBall x r) = sphere x r
Tactic: rw [(_root_.strictConvex_closedBall ℝ x r).extremePoints_eq_diff_interior, interior_closedBall',
    closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : NormedSpace ℝ A
inst_2 : Nontrivial A
x : A
r : ℝ
inst_3 : StrictConvexSpace ℝ A
rw : closedBall x r \ interior (closedBall x r) = sphere x r
⊢ extremePoints ℝ (closedBall x r) = sphere x r
have rw₁ : closedBall x r \ ball x r = sphere x r
Tactic: rw [(_root_.strictConvex_closedBall ℝ x r).extremePoints_eq_diff_interior, interior_closedBall',
    closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (goal)
Goal:
A : Type u_1
inst : NormedAddCommGroup A
inst_1 : NormedSpace ℝ A
inst_2 : Nontrivial A
x : A
r : ℝ
inst_3 : StrictConvexSpace ℝ A
rw : closedBall x r \ interior (closedBall x r) = sphere x r
rw₁ : closedBall x r \ ball x r = sphere x r
⊢ extremePoints ℝ (closedBall x r) = sphere x r
have rw₂ : sphere x r = sphere x r
Tactic: rw [(_root_.strictConvex_closedBall ℝ x r).extremePoints_eq_diff_interior, interior_closedBall',
    closedBall_diff_ball]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict.Extreme (goal)
Goal:
a b : ℝ
hab : a ≤ b
⊢ extremePoints ℝ (Icc a b) = {a, b}
have rw : sphere ((a + b) / 2) ((b - a) / 2) = {a, b}
Tactic: rw [Real.Icc_eq_closedBall, StrictConvexSpace.extremePoints_closedBall_eq_sphere]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
x : E
h : Membership.mem (γ := Set E) univ x
y : E
h_1 : Membership.mem (γ := Set E) univ y
h_2 : x ≠ y
a b : 𝕜
h_3 : 0 < a
h_4 : 0 < b
h_5 : a + b = 1
⊢ Membership.mem (γ := Set E) (interior univ) (a • x + b • y)
have rw : Membership.mem (γ := Set E) univ (a • x + b • y)
Tactic: rw [interior_univ]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
x : E
hx : x ∈ s ∩ t
y : E
hy : y ∈ s ∩ t
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior (s ∩ t)
have rw : a • x + b • y ∈ interior s ∩ interior t
Tactic: rw [interior_inter]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x : E
hx : Membership.mem (γ := Set E) (⋃ (i : ι), s i) x
y : E
hy : Membership.mem (γ := Set E) (⋃ (i : ι), s i) y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)
have rw : ∀ (hx : ∃ (i : ι), x ∈ s i) ⦃y : E⦄ (hy : ∃ (i : ι), y ∈ s i) (hxy : x ≠ y) ⦃a b : 𝕜⦄ (ha : 0 < a) (hb : 0 < b)
  (hab : a + b = 1), Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)
Tactic: rw [mem_iUnion] at hx hy
Cleared hypotheses: hx, y, hy, hxy, a, b, ha, hb, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x : E
hx : ∃ (i : ι), x ∈ s i
y : E
hy : ∃ (i : ι), y ∈ s i
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)
have obtain : ∀ (i : ι) (hx : x ∈ s i), Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)
Tactic: obtain ⟨i, hx⟩ := hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x y : E
hy : ∃ (i : ι), y ∈ s i
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
i : ι
hx : x ∈ s i
⊢ Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)
have obtain : ∀ (j : ι) (hy : y ∈ s j), Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)
Tactic: obtain ⟨j, hy⟩ := hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
ι : Sort u_6
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hs : ∀ ⦃i : ι⦄, StrictConvex 𝕜 (s i)
x y : E
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)
have obtain : ∀ (k : ι) (hik : s i ⊆ s k) (hjk : s j ⊆ s k), Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)
Tactic: obtain ⟨k, hik, hjk⟩ := hdir i j
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : SMul 𝕜 E
S : Set (Set E)
hdir : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) S
hS : ∀ s ∈ S, StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (⋃₀ S)
have rw : StrictConvex.{u_1, u_3} 𝕜 (E := E) (⋃ (i : (↑S : Type u_3)), (↑i : Set E))
Tactic: rw [sUnion_eq_iUnion]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid E
inst_5 : AddCommMonoid F
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
s : Set E
inst_8 : Semiring 𝕝
inst_9 : Module 𝕝 E
inst_10 : Module 𝕝 F
inst_11 : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : Ne.{u_4 + 1} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ Membership.mem (γ := Set F) (interior ((⇑f : (a : E) → F) '' s))
    (HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F))
have refine : (f : (a : E) → F) (a • x + b • y) =
  HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
Tactic: refine hf.image_interior_subset _ ⟨a • x + b • y, hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid E
inst_5 : AddCommMonoid F
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
s : Set E
inst_8 : Semiring 𝕝
inst_9 : Module 𝕝 E
inst_10 : Module 𝕝 F
inst_11 : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : Ne.{u_4 + 1} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (f : (a : E) → F) (a • x + b • y) =
    HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
have rw : HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) (a • x) : F) ((f : (a : E) → F) (b • y) : F) =
  HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
Tactic: rw [map_add, f.map_smul_of_tower a, f.map_smul_of_tower b]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid E
inst_5 : AddCommMonoid F
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
s : Set E
inst_8 : Semiring 𝕝
inst_9 : Module 𝕝 E
inst_10 : Module 𝕝 F
inst_11 : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : Ne.{u_4 + 1} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
rw :
  HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) (a • x) : F) ((f : (a : E) → F) (b • y) : F) =
    HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
⊢ (f : (a : E) → F) (a • x + b • y) =
    HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
have rw₁ : HAdd.hAdd (β := F) (HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F)) ((f : (a : E) → F) (b • y) : F) =
  HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
Tactic: rw [map_add, f.map_smul_of_tower a, f.map_smul_of_tower b]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid E
inst_5 : AddCommMonoid F
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
s : Set E
inst_8 : Semiring 𝕝
inst_9 : Module 𝕝 E
inst_10 : Module 𝕝 F
inst_11 : LinearMap.CompatibleSMul E F 𝕜 𝕝
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕝] F
hf : IsOpenMap.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F)
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : Ne.{u_4 + 1} (α := F) ((f : (a : E) → F) x : F) ((f : (a : E) → F) y : F)
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
rw :
  HAdd.hAdd (α := F) (β := F) ((f : (a : E) → F) (a • x) : F) ((f : (a : E) → F) (b • y) : F) =
    HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
rw₁ :
  HAdd.hAdd (β := F) (HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F)) ((f : (a : E) → F) (b • y) : F) =
    HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
⊢ (f : (a : E) → F) (a • x + b • y) =
    HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
have rw₂ : HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F) =
  HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F)
Tactic: rw [map_add, f.map_smul_of_tower a, f.map_smul_of_tower b]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid E
inst_5 : AddCommMonoid F
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
s : Set F
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕜] F
hf : Continuous.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F)
hfinj : Injective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
x : E
hx : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ Membership.mem (γ := Set E) (interior ((⇑f : (a : E) → F) ⁻¹' s)) (a • x + b • y)
have refine : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' interior s) (a • x + b • y)
Tactic: refine preimage_interior_subset_interior_preimage hf ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommMonoid E
inst_5 : AddCommMonoid F
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
s : Set F
hs : StrictConvex 𝕜 s
f : E →ₗ[𝕜] F
hf : Continuous.{u_3, u_4} (X := E) (Y := F) (⇑f : (a : E) → F)
hfinj : Injective.{u_3 + 1, u_4 + 1} (α := E) (β := F) (⇑f : (a : E) → F)
x : E
hx : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' interior s) (a • x + b • y)
have rw : HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F) ∈ interior s
Tactic: rw [mem_preimage, f.map_add, f.map_smul, f.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace β
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : OrderTopology β
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set β
hs : s.OrdConnected
⊢ StrictConvex 𝕜 s
have refine : ∀ (x : β) (hx : x ∈ s) (y : β) (hy : y ∈ s) (hxy : x ≠ y), (fun (x y : β) ↦ openSegment 𝕜 x y ⊆ interior s) x y
Tactic: refine strictConvex_iff_openSegment_subset.2 fun x hx y hy hxy => ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace β
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : OrderTopology β
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
⊢ (fun (x y : β) ↦ openSegment 𝕜 x y ⊆ interior s) x y
have inl : ∀ (hlt : x < y), openSegment 𝕜 x y ⊆ interior s
Tactic: rcases hxy.lt_or_gt with hlt | hlt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace β
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : OrderTopology β
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
inl : ∀ (hlt : x < y), openSegment 𝕜 x y ⊆ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
have inr : ∀ (hlt : y < x), openSegment 𝕜 x y ⊆ interior s
Tactic: rcases hxy.lt_or_gt with hlt | hlt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace β
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : OrderTopology β
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
hlt : y < x
⊢ openSegment 𝕜 x y ⊆ interior s
have inr : openSegment 𝕜 y x ⊆ interior s
Tactic: rw [openSegment_symm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace β
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : OrderTopology β
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
⊢ (fun (x y : β) ↦ openSegment 𝕜 x y ⊆ interior s) x y
have inl : ∀ (hlt : x < y), openSegment 𝕜 x y ⊆ interior s
Tactic: rcases hxy.lt_or_gt with hlt | hlt <;> [skip; rw [openSegment_symm]]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
β : Type u_5
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace β
inst_3 : AddCommMonoid β
inst_4 : LinearOrder β
inst_5 : IsOrderedCancelAddMonoid β
inst_6 : OrderTopology β
inst_7 : Module 𝕜 β
inst_8 : PosSMulStrictMono 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
inl : ∀ (hlt : x < y), openSegment 𝕜 x y ⊆ interior s
⊢ openSegment 𝕜 x y ⊆ interior s
have inr : ∀ (hlt : y < x), openSegment 𝕜 y x ⊆ interior s
Tactic: rcases hxy.lt_or_gt with hlt | hlt <;> [skip; rw [openSegment_symm]]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCancelCommMonoid E
inst_4 : ContinuousAdd E
inst_5 : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
z x : E
hx : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) x
y : E
hy : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) y
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ Membership.mem (γ := Set E) (interior ((fun (x : E) ↦ z + x) ⁻¹' s)) (a • x + b • y)
have refine : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
Tactic: refine preimage_interior_subset_interior_preimage (continuous_const_add _) ?_