awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (hypothesis)
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) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
have h : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ interior s
Tactic: have h := hs hx hy ((add_right_injective _).ne hxy) 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 : 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
h : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ interior s
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
have rwa : ∀ (h : a • z + a • x + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ interior s),
  Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
Tactic: rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h
Cleared hypotheses: h
-- 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
h : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ interior s
rwa :
  ∀ (h : a • z + a • x + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
have rwa₁ : ∀ (h : a • z + a • x + (b • z + b • y) ∈ interior s),
  Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
Tactic: rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h
Cleared hypotheses: h
-- 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
h : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ interior s
rwa :
  ∀ (h : a • z + a • x + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
rwa₁ :
  ∀ (h : a • z + a • x + (b • z + b • y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
have rwa₂ : ∀ (h : a • z + b • z + (a • x + b • y) ∈ interior s),
  Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
Tactic: rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h
Cleared hypotheses: h
-- 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
h : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ interior s
rwa :
  ∀ (h : a • z + a • x + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
rwa₁ :
  ∀ (h : a • z + a • x + (b • z + b • y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
rwa₂ :
  ∀ (h : a • z + b • z + (a • x + b • y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
have rwa₃ : ∀ (h : (a + b) • z + (a • x + b • y) ∈ interior s),
  Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
Tactic: rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h
Cleared hypotheses: h
-- 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
h : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ interior s
rwa :
  ∀ (h : a • z + a • x + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
rwa₁ :
  ∀ (h : a • z + a • x + (b • z + b • y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
rwa₂ :
  ∀ (h : a • z + b • z + (a • x + b • y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
rwa₃ :
  ∀ (h : (a + b) • z + (a • x + b • y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
have rwa₄ : ∀ (h : HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 1 z + (a • x + b • y) ∈ interior s),
  Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
Tactic: rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h
Cleared hypotheses: h
-- 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
h : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ interior s
rwa :
  ∀ (h : a • z + a • x + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
rwa₁ :
  ∀ (h : a • z + a • x + (b • z + b • y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
rwa₂ :
  ∀ (h : a • z + b • z + (a • x + b • y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
rwa₃ :
  ∀ (h : (a + b) • z + (a • x + b • y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
rwa₄ :
  ∀ (h : HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 1 z + (a • x + b • y) ∈ interior s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
have rwa₅ : ∀ (h : z + (a • x + b • y) ∈ interior s),
  Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
Tactic: rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h
Cleared hypotheses: h
-- 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 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : Ne.{u_3 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 + x2) v w) ((fun (x1 x2 : E) ↦ x1 + x2) x y)
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ HSMul.hSMul (β := E) a ((fun (x1 x2 : E) ↦ x1 + x2) v w) + HSMul.hSMul (β := E) b ((fun (x1 x2 : E) ↦ x1 + x2) x y) ∈
    interior (s + t)
have rw : a • v + b • x + (a • w + b • y) ∈ interior (s + t)
Tactic: rw [smul_add, smul_add, add_add_add_comm]
-- 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 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : Ne.{u_3 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 + x2) v w) ((fun (x1 x2 : E) ↦ x1 + x2) x y)
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)
have inl : ∀ (hx : v ∈ s) (h : Ne.{u_3 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 + x2) v w) ((fun (x1 x2 : E) ↦ x1 + x2) v y)),
  a • v + b • v + (a • w + b • y) ∈ interior (s + t)
Tactic: obtain rfl | hvx := eq_or_ne v x
Cleared hypotheses: x, hx, h
-- 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 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
x : E
hx : x ∈ s
y : E
hy : y ∈ t
h : Ne.{u_3 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 + x2) v w) ((fun (x1 x2 : E) ↦ x1 + x2) x y)
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inl :
  ∀ (hx : v ∈ s) (h : Ne.{u_3 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 + x2) v w) ((fun (x1 x2 : E) ↦ x1 + x2) v y)),
    a • v + b • v + (a • w + b • y) ∈ interior (s + t)
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)
have inr : ∀ (hvx : v ≠ x), a • v + b • x + (a • w + b • y) ∈ interior (s + t)
Tactic: obtain rfl | hvx := eq_or_ne v x
-- 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 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : v ∈ s
h : Ne.{u_3 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 + x2) v w) ((fun (x1 x2 : E) ↦ x1 + x2) v y)
⊢ a • v + b • v + (a • w + b • y) ∈ interior (s + t)
have inl : a • v + b • v + (a • w + b • y) ∈ interior ({v} + t)
Tactic: refine interior_mono (add_subset_add (singleton_subset_iff.2 hv) Subset.rfl) ?_
-- 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 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : ContinuousAdd E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
v : E
hv : v ∈ s
w : E
hw : w ∈ t
y : E
hy : y ∈ t
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hx : v ∈ s
h : Ne.{u_3 + 1} (α := E) ((fun (x1 x2 : E) ↦ x1 + x2) v w) ((fun (x1 x2 : E) ↦ x1 + x2) v y)
⊢ a • v + b • v + (a • w + b • y) ∈ interior ({v} + t)
have inl : Membership.mem (γ := Set E) (interior ((fun (x : E) ↦ v + x) '' t)) (v + (a • w + b • y))
Tactic: rw [Convex.combo_self hab, singleton_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : Field 𝕝
inst_6 : Module 𝕝 E
inst_7 : ContinuousConstSMul 𝕝 E
inst_8 : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕝
⊢ StrictConvex 𝕜 (c • s)
have inl : StrictConvex 𝕜 (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕝) 0 s)
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
𝕝 : Type u_2
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : Field 𝕝
inst_6 : Module 𝕝 E
inst_7 : ContinuousConstSMul 𝕝 E
inst_8 : LinearMap.CompatibleSMul E E 𝕜 𝕝
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕝
inl : StrictConvex 𝕜 (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕝) 0 s)
⊢ StrictConvex 𝕜 (c • s)
have inr : ∀ (hc : c ≠ 0), StrictConvex 𝕜 (c • s)
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : CommSemiring 𝕜
inst_1 : IsDomain 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
inst_6 : Module.IsTorsionFree 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
⊢ StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)
have inl : StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 z) ⁻¹' s)
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : CommSemiring 𝕜
inst_1 : IsDomain 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
inst_6 : Module.IsTorsionFree 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
inl : StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 z) ⁻¹' s)
⊢ StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)
have inr : ∀ (hc : c ≠ 0), StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : CommSemiring 𝕜
inst_1 : IsDomain 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
inst_6 : Module.IsTorsionFree 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 z) ⁻¹' s)
have inl : StrictConvex.{u_1, u_3} 𝕜 (E := E) (if 0 ∈ s then univ else ∅)
Tactic: simp_rw [zero_smul, preimage_const]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : CommSemiring 𝕜
inst_1 : IsDomain 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
inst_6 : Module.IsTorsionFree 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
⊢ StrictConvex.{u_1, u_3} 𝕜 (E := E) (if 0 ∈ s then univ else ∅)
have pos : 0 ∈ s → StrictConvex.{u_1, u_3} 𝕜 (E := E) univ
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : CommSemiring 𝕜
inst_1 : IsDomain 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
inst_6 : Module.IsTorsionFree 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
pos : 0 ∈ s → StrictConvex.{u_1, u_3} 𝕜 (E := E) univ
⊢ StrictConvex.{u_1, u_3} 𝕜 (E := E) (if 0 ∈ s then univ else ∅)
have neg : 0 ∉ s → StrictConvex.{u_1, u_3} 𝕜 (E := E) ∅
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : CommSemiring 𝕜
inst_1 : IsDomain 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
inst_6 : Module.IsTorsionFree 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
hc : c ≠ 0
⊢ StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)
have inr : Continuous.{u_3, u_3} (X := E) (Y := E) (⇑((LinearMap.lsmul 𝕜 E : (a : 𝕜) → E →ₗ[𝕜] E) c : E →ₗ[𝕜] E) : (a : E) → E)
Tactic: refine hs.linear_preimage (LinearMap.lsmul _ _ c) ?_ (smul_right_injective E hc)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : CommSemiring 𝕜
inst_1 : IsDomain 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
inst_6 : Module.IsTorsionFree 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
hc : c ≠ 0
⊢ Continuous.{u_3, u_3} (X := E) (Y := E) (⇑((LinearMap.lsmul 𝕜 E : (a : 𝕜) → E →ₗ[𝕜] E) c : E →ₗ[𝕜] E) : (a : E) → E)
have inr : Continuous.{u_3, u_3} (X := E) (Y := E)
  (⇑(({ toFun := fun (m : 𝕜) ↦ { toFun := (fun (x1 : 𝕜) (x2 : E) ↦ x1 • x2) m, map_add' := sorry, map_smul' := sorry },
              map_add' := sorry, map_smul' := sorry } :
            (a : 𝕜) → E →ₗ[𝕜] E)
          c :
        E →ₗ[𝕜] E) :
    (a : E) → E)
Tactic: unfold LinearMap.lsmul LinearMap.mk₂ LinearMap.mk₂' LinearMap.mk₂'ₛₗ
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : CommSemiring 𝕜
inst_1 : IsDomain 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
inst_6 : Module.IsTorsionFree 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
⊢ StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)
have inl : StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 z) ⁻¹' s)
Tactic: classical
    obtain rfl | hc := eq_or_ne c 0
    · simp_rw [zero_smul, preimage_const]
      split_ifs
      · exact strictConvex_univ
      · exact strictConvex_empty
    refine hs.linear_preimage (LinearMap.lsmul _ _ c) ?_ (smul_right_injective E hc)
    unfold LinearMap.lsmul LinearMap.mk₂ LinearMap.mk₂' LinearMap.mk₂'ₛₗ
    exact continuous_const_smul _
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : CommSemiring 𝕜
inst_1 : IsDomain 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
inst_6 : Module.IsTorsionFree 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
inl : StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 z) ⁻¹' s)
⊢ StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)
have inr : ∀ (hc : c ≠ 0), StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)
Tactic: classical
    obtain rfl | hc := eq_or_ne c 0
    · simp_rw [zero_smul, preimage_const]
      split_ifs
      · exact strictConvex_univ
      · exact strictConvex_empty
    refine hs.linear_preimage (LinearMap.lsmul _ _ c) ?_ (smul_right_injective E hc)
    unfold LinearMap.lsmul LinearMap.mk₂ LinearMap.mk₂' LinearMap.mk₂'ₛₗ
    exact continuous_const_smul _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : CommSemiring 𝕜
inst_1 : IsDomain 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
inst_6 : Module.IsTorsionFree 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
inl : StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 z) ⁻¹' s)
inr inr₁ : ∀ (hc : c ≠ 0), StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)
⊢ StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)
have inr₂ : ∀ (hc : c ≠ 0),
  Continuous.{u_3, u_3} (X := E) (Y := E) (⇑((LinearMap.lsmul 𝕜 E : (a : 𝕜) → E →ₗ[𝕜] E) c : E →ₗ[𝕜] E) : (a : E) → E)
Tactic: classical
    obtain rfl | hc := eq_or_ne c 0
    · simp_rw [zero_smul, preimage_const]
      split_ifs
      · exact strictConvex_univ
      · exact strictConvex_empty
    refine hs.linear_preimage (LinearMap.lsmul _ _ c) ?_ (smul_right_injective E hc)
    unfold LinearMap.lsmul LinearMap.mk₂ LinearMap.mk₂' LinearMap.mk₂'ₛₗ
    exact continuous_const_smul _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : CommSemiring 𝕜
inst_1 : IsDomain 𝕜
inst_2 : PartialOrder 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
inst_6 : Module.IsTorsionFree 𝕜 E
inst_7 : ContinuousConstSMul 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
c : 𝕜
inl : StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 z) ⁻¹' s)
inr inr₁ : ∀ (hc : c ≠ 0), StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)
inr₂ :
  ∀ (hc : c ≠ 0),
    Continuous.{u_3, u_3} (X := E) (Y := E) (⇑((LinearMap.lsmul 𝕜 E : (a : 𝕜) → E →ₗ[𝕜] E) c : E →ₗ[𝕜] E) : (a : E) → E)
⊢ StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)
have inr₃ : ∀ (hc : c ≠ 0),
  Continuous.{u_3, u_3} (X := E) (Y := E)
    (⇑(({ toFun := fun (m : 𝕜) ↦ { toFun := (fun (x1 : 𝕜) (x2 : E) ↦ x1 • x2) m, map_add' := sorry, map_smul' := sorry },
                map_add' := sorry, map_smul' := sorry } :
              (a : 𝕜) → E →ₗ[𝕜] E)
            c :
          E →ₗ[𝕜] E) :
      (a : E) → E)
Tactic: classical
    obtain rfl | hc := eq_or_ne c 0
    · simp_rw [zero_smul, preimage_const]
      split_ifs
      · exact strictConvex_univ
      · exact strictConvex_empty
    refine hs.linear_preimage (LinearMap.lsmul _ _ c) ?_ (smul_right_injective E hc)
    unfold LinearMap.lsmul LinearMap.mk₂ LinearMap.mk₂' LinearMap.mk₂'ₛₗ
    exact continuous_const_smul _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x y : E
inst_5 : IsOrderedRing 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
⊢ x = y
have obtain : ∀ (a : 𝕜) (ha₀ : 0 < a) (ha₁ : a < 1), x = y
Tactic: obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x y : E
inst_5 : IsOrderedRing 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ x = y
have by_contra : ∀ (hxy : ¬x = y), False
Tactic: by_contra hxy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x y : E
inst_5 : IsOrderedRing 𝕜
inst_6 : Nontrivial 𝕜
inst_7 : DenselyOrdered 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
h : openSegment 𝕜 x y ⊆ frontier s
a : 𝕜
ha₀ : 0 < a
ha₁ : a < 1
⊢ x = y
have by_contra : ¬x = y → False
Tactic: classical
    by_contra hxy
    exact
      (h ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, rfl⟩).2
        (hs hx hy hxy ha₀ (sub_pos_of_lt ha₁) <| add_sub_cancel _ _)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Strict (goal)
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
x y : E
inst_5 : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
hx : x ∈ s
hxy : x + y ∈ s
hy : y ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ x + t • y = (1 - t) • x + t • (x + y)
have match_scalars : 1 = (1 - t) * 1 + t * 1
Tactic: match_scalars