awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Strict
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 𝕜 β
r : β
⊢ StrictConvex 𝕜 (Iio r)

Tactic:
ordConnected_Iio.strictConvex

Premises used: Set.OrdConnected.strictConvex, Set.ordConnected_Iio
-- Module: Mathlib.Analysis.Convex.Strict
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 𝕜 β
r : β
⊢ StrictConvex 𝕜 (Ioi r)

Tactic:
ordConnected_Ioi.strictConvex

Premises used: Set.ordConnected_Ioi, Set.OrdConnected.strictConvex
-- Module: Mathlib.Analysis.Convex.Strict
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 𝕜 β
r s : β
⊢ StrictConvex 𝕜 (Icc r s)

Tactic:
ordConnected_Icc.strictConvex

Premises used: Set.ordConnected_Icc, Set.OrdConnected.strictConvex
-- Module: Mathlib.Analysis.Convex.Strict
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 𝕜 β
r s : β
⊢ StrictConvex 𝕜 (Ioo r s)

Tactic:
ordConnected_Ioo.strictConvex

Premises used: Set.ordConnected_Ioo, Set.OrdConnected.strictConvex
-- Module: Mathlib.Analysis.Convex.Strict
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 𝕜 β
r s : β
⊢ StrictConvex 𝕜 (Ico r s)

Tactic:
ordConnected_Ico.strictConvex

Premises used: Set.ordConnected_Ico, Set.OrdConnected.strictConvex
-- Module: Mathlib.Analysis.Convex.Strict
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 𝕜 β
r s : β
⊢ StrictConvex 𝕜 (Ioc r s)

Tactic:
ordConnected_Ioc.strictConvex

Premises used: Set.ordConnected_Ioc, Set.OrdConnected.strictConvex
-- Module: Mathlib.Analysis.Convex.Strict
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 𝕜 β
r s : β
⊢ StrictConvex 𝕜 (uIcc r s)

Tactic:
strictConvex_Icc _ _

Premises used: strictConvex_Icc, Set.uIcc
-- Module: Mathlib.Analysis.Convex.Strict
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 𝕜 β
r s : β
⊢ StrictConvex 𝕜 (uIoc r s)

Tactic:
strictConvex_Ioc _ _

Premises used: Set.uIoc, strictConvex_Ioc
-- Module: Mathlib.Analysis.Convex.Strict
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)

Tactic:
preimage_interior_subset_interior_preimage (continuous_const_add _) ?_

Premises used: preimage_interior_subset_interior_preimage, continuous_const_add
-- Module: Mathlib.Analysis.Convex.Strict
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
refine : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' interior s) (a • x + b • y)
⊢ Membership.mem (γ := Set E) (interior ((fun (x : E) ↦ z + x) ⁻¹' s)) (a • x + b • y)

Tactic:
refine preimage_interior_subset_interior_preimage (continuous_const_add _) ?_

Premises used: preimage_interior_subset_interior_preimage, continuous_const_add
-- Module: Mathlib.Analysis.Convex.Strict
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
⊢ 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
-- Module: Mathlib.Analysis.Convex.Strict
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)
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀ (h : 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)

Tactic:
rwa [smul_add, smul_add, add_add_add_comm, ← _root_.add_smul, hab, one_smul] at h

Premises used: one_smul, add_smul, add_add_add_comm, smul_add
-- Module: Mathlib.Analysis.Convex.Strict
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 : E
⊢ StrictConvex 𝕜 (E := E) ((fun (x : E) ↦ x + z) ⁻¹' s)

Tactic:
simpa only [add_comm] using hs.preimage_add_right z

Premises used: add_comm, StrictConvex.preimage_add_right
-- Module: Mathlib.Analysis.Convex.Strict
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
rw : a • v + b • x + (a • w + b • y) ∈ interior (s + t)
⊢ 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)

Tactic:
rw [smul_add, smul_add, add_add_add_comm]

Premises used: add_add_add_comm, smul_add
-- Module: Mathlib.Analysis.Convex.Strict
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)
inr : ∀ (hvx : v ≠ x), a • v + b • x + (a • w + b • y) ∈ interior (s + t)
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)

Tactic:
obtain rfl | hvx := eq_or_ne v x

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Analysis.Convex.Strict
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)

Tactic:
interior_mono (add_subset_add (singleton_subset_iff.2 hv) Subset.rfl) ?_

Premises used: Iff.mpr, Set.singleton_subset_iff, interior_mono, Set.Subset.rfl, Set.add_subset_add
-- Module: Mathlib.Analysis.Convex.Strict
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)
inl : a • v + b • v + (a • w + b • y) ∈ interior ({v} + t)
⊢ a • v + b • v + (a • w + b • y) ∈ interior (s + t)

Tactic:
refine interior_mono (add_subset_add (singleton_subset_iff.2 hv) Subset.rfl) ?_

Premises used: Iff.mpr, Set.singleton_subset_iff, interior_mono, Set.Subset.rfl, Set.add_subset_add
-- Module: Mathlib.Analysis.Convex.Strict
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)
inl : Membership.mem (γ := Set E) (interior ((fun (x : E) ↦ v + x) '' t)) (v + (a • w + b • y))
⊢ a • v + b • v + (a • w + b • y) ∈ interior ({v} + t)

Tactic:
rw [Convex.combo_self hab, singleton_add]

Premises used: Convex.combo_self, Set.singleton_add
-- Module: Mathlib.Analysis.Convex.Strict
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)
⊢ Membership.mem (γ := Set E) (interior ((fun (x : E) ↦ v + x) '' t)) (v + (a • w + b • y))

Tactic:
(isOpenMap_add_left _).image_interior_subset _
        (mem_image_of_mem _ <| ht hw hy (ne_of_apply_ne _ h) ha hb hab)

Premises used: isOpenMap_add_left, IsOpenMap.image_interior_subset, Set.Mem, ne_of_apply_ne, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Strict
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)
⊢ Membership.mem (γ := Set E) (interior ((fun (x : E) ↦ v + x) '' t)) (v + (a • w + b • y))

Tactic:
exact
      (isOpenMap_add_left _).image_interior_subset _
        (mem_image_of_mem _ <| ht hw hy (ne_of_apply_ne _ h) ha hb hab)

Premises used: isOpenMap_add_left, IsOpenMap.image_interior_subset, ne_of_apply_ne, Set.mem_image_of_mem
-- Module: Mathlib.Analysis.Convex.Strict
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
hvx : v ≠ x
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)

Tactic:
subset_interior_add_left
      (add_mem_add (hs hv hx hvx ha hb hab) <| ht.convex hw hy ha.le hb.le hab)

Premises used: Set.Mem, subset_interior_add_left, LT.lt.le, Set.add_mem_add, StrictConvex.convex
-- Module: Mathlib.Analysis.Convex.Strict
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
hvx : v ≠ x
⊢ a • v + b • x + (a • w + b • y) ∈ interior (s + t)

Tactic:
exact
    subset_interior_add_left
      (add_mem_add (hs hv hx hvx ha hb hab) <| ht.convex hw hy ha.le hb.le hab)

Premises used: subset_interior_add_left, LT.lt.le, Set.add_mem_add, StrictConvex.convex
-- Module: Mathlib.Analysis.Convex.Strict
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 : Set E
hs : StrictConvex 𝕜 s
z : E
⊢ StrictConvex 𝕜 (E := E) ((fun (x : E) ↦ z + x) '' s)

Tactic:
simpa only [singleton_add] using (strictConvex_singleton z).add hs

Premises used: StrictConvex.add, Set.singleton_add, strictConvex_singleton
-- Module: Mathlib.Analysis.Convex.Strict
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 : Set E
hs : StrictConvex 𝕜 s
z : E
⊢ StrictConvex 𝕜 (E := E) ((fun (x : E) ↦ x + z) '' s)

Tactic:
simpa only [add_comm] using hs.add_left z

Premises used: StrictConvex.add_left, add_comm
-- Module: Mathlib.Analysis.Convex.Strict
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 : Set E
hs : StrictConvex 𝕜 s
x : E
⊢ StrictConvex 𝕜 (x +ᵥ s)

Tactic:
hs.add_left x

Premises used: StrictConvex.add_left
-- Module: Mathlib.Analysis.Convex.Strict
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)
inr : ∀ (hc : c ≠ 0), StrictConvex 𝕜 (c • s)
⊢ StrictConvex 𝕜 (c • s)

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Convex.Strict
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
⊢ StrictConvex 𝕜 (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕝) 0 s)

Tactic:
(subsingleton_zero_smul_set _).strictConvex

Premises used: Set.subsingleton_zero_smul_set, Set.Subsingleton.strictConvex
-- Module: Mathlib.Analysis.Convex.Strict
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
⊢ StrictConvex 𝕜 (HSMul.hSMul.{u_2, u_3, u_3} (α := 𝕝) 0 s)

Tactic:
exact (subsingleton_zero_smul_set _).strictConvex

Premises used: Set.subsingleton_zero_smul_set, Set.Subsingleton.strictConvex
-- Module: Mathlib.Analysis.Convex.Strict
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 : 𝕝
hc : c ≠ 0
⊢ StrictConvex 𝕜 (c • s)

Tactic:
hs.linear_image (LinearMap.lsmul _ _ c) (isOpenMap_smul₀ hc)

Premises used: LinearMap.lsmul, isOpenMap_smul₀, StrictConvex.linear_image, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Strict
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 : 𝕝
hc : c ≠ 0
⊢ StrictConvex 𝕜 (c • s)

Tactic:
exact hs.linear_image (LinearMap.lsmul _ _ c) (isOpenMap_smul₀ hc)

Premises used: LinearMap.lsmul, isOpenMap_smul₀, StrictConvex.linear_image, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Strict
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
inst_9 : ContinuousAdd E
hs : StrictConvex 𝕜 s
z : E
c : 𝕝
⊢ StrictConvex 𝕜 (z +ᵥ c • s)

Tactic:
(hs.smul c).vadd z

Premises used: StrictConvex.smul, StrictConvex.vadd
-- Module: Mathlib.Analysis.Convex.Strict
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 : ∀ (hc : c ≠ 0), StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)
⊢ StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)

Tactic:
obtain rfl | hc := eq_or_ne c 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Convex.Strict
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
inl : StrictConvex.{u_1, u_3} 𝕜 (E := E) (if 0 ∈ s then univ else ∅)
⊢ StrictConvex 𝕜 (E := E) ((fun (z : E) ↦ HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) 0 z) ⁻¹' s)

Tactic:
simp_rw [zero_smul, preimage_const]

Premises used: Set.preimage_const, zero_smul
-- Module: Mathlib.Analysis.Convex.Strict
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
neg : 0 ∉ s → StrictConvex.{u_1, u_3} 𝕜 (E := E) ∅
⊢ StrictConvex.{u_1, u_3} 𝕜 (E := E) (if 0 ∈ s then univ else ∅)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Convex.Strict
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
h : 0 ∈ s
⊢ StrictConvex.{u_1, u_3} 𝕜 (E := E) univ

Tactic:
strictConvex_univ

Premises used: strictConvex_univ
-- Module: Mathlib.Analysis.Convex.Strict
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
h : 0 ∈ s
⊢ StrictConvex.{u_1, u_3} 𝕜 (E := E) univ

Tactic:
exact strictConvex_univ

Premises used: strictConvex_univ
-- Module: Mathlib.Analysis.Convex.Strict
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
h : 0 ∉ s
⊢ StrictConvex.{u_1, u_3} 𝕜 (E := E) ∅

Tactic:
strictConvex_empty

Premises used: strictConvex_empty
-- Module: Mathlib.Analysis.Convex.Strict
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
h : 0 ∉ s
⊢ StrictConvex.{u_1, u_3} 𝕜 (E := E) ∅

Tactic:
exact strictConvex_empty

Premises used: strictConvex_empty
-- Module: Mathlib.Analysis.Convex.Strict
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)

Tactic:
hs.linear_preimage (LinearMap.lsmul _ _ c) ?_ (smul_right_injective E hc)

Premises used: LinearMap.lsmul, smul_right_injective, StrictConvex.linear_preimage, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Strict
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
inr :
  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)

Tactic:
refine hs.linear_preimage (LinearMap.lsmul _ _ c) ?_ (smul_right_injective E hc)

Premises used: LinearMap.lsmul, smul_right_injective, StrictConvex.linear_preimage, DFunLike.coe