awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Strict
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 ∩ interior t

Tactic:
⟨hs hx.1 hy.1 hxy ha hb hab, ht hx.2 hy.2 hxy ha hb hab⟩

Premises used: Set.Mem, setOf, Set.inter, And.right, And.left, And.intro
-- Module: Mathlib.Analysis.Convex.Strict
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 ∩ interior t

Tactic:
exact ⟨hs hx.1 hy.1 hxy ha hb hab, ht hx.2 hy.2 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 : 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
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)
⊢ Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)

Tactic:
rw [mem_iUnion] at hx hy

Premises used: Set.mem_iUnion
-- Module: Mathlib.Analysis.Convex.Strict
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
obtain : ∀ (i : ι) (hx : x ∈ s i), Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)
⊢ Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)

Tactic:
obtain ⟨i, hx⟩ := hx
-- Module: Mathlib.Analysis.Convex.Strict
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
obtain : ∀ (j : ι) (hy : y ∈ s j), Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)
⊢ Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)

Tactic:
obtain ⟨j, hy⟩ := hy
-- Module: Mathlib.Analysis.Convex.Strict
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
obtain :
  ∀ (k : ι) (hik : s i ⊆ s k) (hjk : s j ⊆ s k), Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)
⊢ Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)

Tactic:
obtain ⟨k, hik, hjk⟩ := hdir i j
-- Module: Mathlib.Analysis.Convex.Strict
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
k : ι
hik : s i ⊆ s k
hjk : s j ⊆ s k
⊢ Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)

Tactic:
interior_mono (subset_iUnion s k) (hs (hik hx) (hjk hy) hxy ha hb hab)

Premises used: interior_mono, Set.subset_iUnion
-- Module: Mathlib.Analysis.Convex.Strict
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
k : ι
hik : s i ⊆ s k
hjk : s j ⊆ s k
⊢ Membership.mem (γ := Set E) (interior (⋃ (i : ι), s i)) (a • x + b • y)

Tactic:
exact interior_mono (subset_iUnion s k) (hs (hik hx) (hjk hy) hxy ha hb hab)

Premises used: interior_mono, Set.subset_iUnion
-- Module: Mathlib.Analysis.Convex.Strict
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
rw : StrictConvex.{u_1, u_3} 𝕜 (E := E) (⋃ (i : (↑S : Type u_3)), (↑i : Set E))
⊢ StrictConvex 𝕜 (⋃₀ S)

Tactic:
rw [sUnion_eq_iUnion]

Premises used: Set.sUnion_eq_iUnion
-- Module: Mathlib.Analysis.Convex.Strict
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.{u_1, u_3} 𝕜 (E := E) (⋃ (i : (↑S : Type u_3)), (↑i : Set E))

Tactic:
(directedOn_iff_directed.1 hdir).strictConvex_iUnion fun s => hS _ s.2

Premises used: Directed.strictConvex_iUnion, directedOn_iff_directed, Iff.mp, Subtype.val, Subtype.property
-- Module: Mathlib.Analysis.Convex.Strict
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.{u_1, u_3} 𝕜 (E := E) (⋃ (i : (↑S : Type u_3)), (↑i : Set E))

Tactic:
exact (directedOn_iff_directed.1 hdir).strictConvex_iUnion fun s => hS _ s.2

Premises used: Directed.strictConvex_iUnion, directedOn_iff_directed, Iff.mp, Subtype.val, Subtype.property
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : Module 𝕜 E
s : Set E
hs : StrictConvex 𝕜 s
⊢ Convex 𝕜 s

Tactic:
convex_iff_pairwise_pos.2 fun _ hx _ hy hxy _ _ ha hb hab =>
    interior_subset <| hs hx hy hxy ha hb hab

Premises used: Iff.mpr, convex_iff_pairwise_pos, interior_subset
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : Module 𝕜 E
s : Set E
h : IsOpen s
hs : Convex 𝕜 s
⊢ StrictConvex 𝕜 s

Tactic:
fun _ hx _ hy _ _ _ ha hb hab => h.interior_eq.symm ▸ hs hx hy ha.le hb.le hab

Premises used: StrictConvex, Eq.rec, LT.lt.le, Set.Pairwise, IsOpen.interior_eq, Eq.symm
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : Module 𝕜 E
s : Set E
h : IsOpen s
⊢ StrictConvex 𝕜 s ↔ Convex 𝕜 s

Tactic:
⟨StrictConvex.convex, Convex.strictConvex_of_isOpen h⟩

Premises used: Iff.intro, StrictConvex.convex, Convex.strictConvex_of_isOpen
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : AddCommMonoid E
inst_4 : Module 𝕜 E
c : E
⊢ StrictConvex 𝕜 (E := E) {c}

Tactic:
pairwise_singleton _ _

Premises used: StrictConvex, Set.pairwise_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 : AddCommMonoid E
inst_4 : Module 𝕜 E
s : Set E
hs : s.Subsingleton
⊢ StrictConvex 𝕜 s

Tactic:
hs.pairwise _

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

Tactic:
hf.image_interior_subset _ ⟨a • x + b • y, hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, ?_⟩

Premises used: IsOpenMap.image_interior_subset, ne_of_apply_ne, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Analysis.Convex.Strict
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
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)
⊢ 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))

Tactic:
refine hf.image_interior_subset _ ⟨a • x + b • y, hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, ?_⟩

Premises used: IsOpenMap.image_interior_subset, ne_of_apply_ne, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul
-- Module: Mathlib.Analysis.Convex.Strict
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)
rw₂ 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)
⊢ (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:
rw [map_add, f.map_smul_of_tower a, f.map_smul_of_tower b]

Premises used: map_add, LinearMap.map_smul_of_tower
-- Module: Mathlib.Analysis.Convex.Strict
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 E
hs : StrictConvex 𝕜 s
f : E → F
h : IsLinearMap 𝕜 f
hf : IsOpenMap f
⊢ StrictConvex 𝕜 (f '' s)

Tactic:
hs.linear_image (h.mk' f) hf

Premises used: StrictConvex.linear_image, IsLinearMap.mk'
-- Module: Mathlib.Analysis.Convex.Strict
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)

Tactic:
preimage_interior_subset_interior_preimage hf ?_

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

Tactic:
refine preimage_interior_subset_interior_preimage hf ?_

Premises used: preimage_interior_subset_interior_preimage
-- Module: Mathlib.Analysis.Convex.Strict
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
rw : HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F) ∈ interior s
⊢ Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' interior s) (a • x + b • y)

Tactic:
rw [mem_preimage, f.map_add, f.map_smul, f.map_smul]

Premises used: LinearMap.map_add, LinearMap.map_smul, Set.mem_preimage
-- Module: Mathlib.Analysis.Convex.Strict
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
⊢ HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F) ∈ interior s

Tactic:
hs hx hy (hfinj.ne hxy) ha hb hab

Premises used: Set.Mem, Function.Injective.ne
-- Module: Mathlib.Analysis.Convex.Strict
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
⊢ HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F) ∈ interior s

Tactic:
exact hs hx hy (hfinj.ne hxy) ha hb hab

Premises used: Function.Injective.ne
-- Module: Mathlib.Analysis.Convex.Strict
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
h : IsLinearMap 𝕜 f
hf : Continuous f
hfinj : Injective f
⊢ StrictConvex 𝕜 (f ⁻¹' s)

Tactic:
hs.linear_preimage (h.mk' f) hf hfinj

Premises used: StrictConvex.linear_preimage, IsLinearMap.mk'
-- 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 𝕜 β
s : Set β
hs : s.OrdConnected
⊢ StrictConvex 𝕜 s

Tactic:
strictConvex_iff_openSegment_subset.2 fun x hx y hy hxy => ?_

Premises used: Iff.mpr, strictConvex_iff_openSegment_subset
-- 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 𝕜 β
s : Set β
hs : s.OrdConnected
refine : ∀ (x : β) (hx : x ∈ s) (y : β) (hy : y ∈ s) (hxy : x ≠ y), (fun (x y : β) ↦ openSegment 𝕜 x y ⊆ interior s) x y
⊢ StrictConvex 𝕜 s

Tactic:
refine strictConvex_iff_openSegment_subset.2 fun x hx y hy hxy => ?_

Premises used: Iff.mpr, strictConvex_iff_openSegment_subset
-- 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 𝕜 β
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
inr : ∀ (hlt : y < x), openSegment 𝕜 x y ⊆ interior s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
rcases hxy.lt_or_gt with hlt | hlt

Premises used: Ne.lt_or_gt
-- 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 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
hlt : y < x
inr : openSegment 𝕜 y x ⊆ interior s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
rw [openSegment_symm]

Premises used: openSegment_symm
-- 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 𝕜 β
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
inr : ∀ (hlt : y < x), openSegment 𝕜 y x ⊆ interior s
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
rcases hxy.lt_or_gt with hlt | hlt <;> [skip; rw [openSegment_symm]]

Premises used: openSegment_symm, Ne.lt_or_gt
-- 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 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
hlt : x < y
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
(openSegment_subset_Ioo hlt).trans
        (isOpen_Ioo.subset_interior_iff.2 <| Ioo_subset_Icc_self.trans <| hs.out ‹_› ‹_›)

Premises used: Iff.mpr, Set.Ioo_subset_Icc_self, isOpen_Ioo, IsOpen.subset_interior_iff, HasSubset.Subset.trans, Set.OrdConnected.out, openSegment_subset_Ioo
-- 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 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
hlt : x < y
⊢ openSegment 𝕜 x y ⊆ interior s

Tactic:
exact
      (openSegment_subset_Ioo hlt).trans
        (isOpen_Ioo.subset_interior_iff.2 <| Ioo_subset_Icc_self.trans <| hs.out ‹_› ‹_›)

Premises used: Iff.mpr, Set.Ioo_subset_Icc_self, isOpen_Ioo, IsOpen.subset_interior_iff, HasSubset.Subset.trans, Set.OrdConnected.out, openSegment_subset_Ioo
-- 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 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
hlt : y < x
⊢ openSegment 𝕜 y x ⊆ interior s

Tactic:
(openSegment_subset_Ioo hlt).trans
        (isOpen_Ioo.subset_interior_iff.2 <| Ioo_subset_Icc_self.trans <| hs.out ‹_› ‹_›)

Premises used: Iff.mpr, Set.Ioo_subset_Icc_self, isOpen_Ioo, IsOpen.subset_interior_iff, HasSubset.Subset.trans, Set.OrdConnected.out, openSegment_subset_Ioo
-- 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 𝕜 β
s : Set β
hs : s.OrdConnected
x : β
hx : x ∈ s
y : β
hy : y ∈ s
hxy : x ≠ y
hlt : y < x
⊢ openSegment 𝕜 y x ⊆ interior s

Tactic:
exact
      (openSegment_subset_Ioo hlt).trans
        (isOpen_Ioo.subset_interior_iff.2 <| Ioo_subset_Icc_self.trans <| hs.out ‹_› ‹_›)

Premises used: Iff.mpr, Set.Ioo_subset_Icc_self, isOpen_Ioo, IsOpen.subset_interior_iff, HasSubset.Subset.trans, Set.OrdConnected.out, openSegment_subset_Ioo
-- 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 𝕜 (Iic r)

Tactic:
ordConnected_Iic.strictConvex

Premises used: Set.ordConnected_Iic, 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 : β
⊢ StrictConvex 𝕜 (Ici r)

Tactic:
ordConnected_Ici.strictConvex

Premises used: Set.ordConnected_Ici, Set.OrdConnected.strictConvex