awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
    (⇑(({ toFun := fun (m : 𝕜) ↦ { toFun := (fun (x1 : 𝕜) (x2 : E) ↦ x1 • x2) m, map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ } :
              (a : 𝕜) → E →ₗ[𝕜] E)
            c :
          E →ₗ[𝕜] E) :
      (a : E) → E)
⊢ Continuous.{u_3, u_3} (X := E) (Y := E) (⇑((LinearMap.lsmul 𝕜 E : (a : 𝕜) → E →ₗ[𝕜] E) c : E →ₗ[𝕜] E) : (a : E) → E)

Tactic:
unfold LinearMap.lsmul LinearMap.mk₂ LinearMap.mk₂' LinearMap.mk₂'ₛₗ

Premises used: LinearMap.mk₂, LinearMap.lsmul, LinearMap.mk₂'ₛₗ, LinearMap.mk₂'
-- 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
⊢ Continuous.{u_3, u_3} (X := E) (Y := E)
    (⇑(({ toFun := fun (m : 𝕜) ↦ { toFun := (fun (x1 : 𝕜) (x2 : E) ↦ x1 • x2) m, map_add' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ } :
              (a : 𝕜) → E →ₗ[𝕜] E)
            c :
          E →ₗ[𝕜] E) :
      (a : E) → E)

Tactic:
continuous_const_smul _

Premises used: ContinuousConstSMul.continuous_const_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
c : 𝕜
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' := ⋯, map_smul' := ⋯ },
                map_add' := ⋯, map_smul' := ⋯ } :
              (a : 𝕜) → E →ₗ[𝕜] E)
            c :
          E →ₗ[𝕜] E) :
      (a : E) → E)

Tactic:
exact continuous_const_smul _

Premises used: ContinuousConstSMul.continuous_const_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
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)
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' := ⋯, map_smul' := ⋯ },
                  map_add' := ⋯, map_smul' := ⋯ } :
                (a : 𝕜) → E →ₗ[𝕜] E)
              c :
            E →ₗ[𝕜] E) :
        (a : E) → E)
⊢ 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 _

Premises used: LinearMap.mk₂, ContinuousConstSMul.continuous_const_smul, Set.preimage_const, LinearMap.lsmul, LinearMap.mk₂'ₛₗ, strictConvex_empty, zero_smul, eq_or_ne, LinearMap.mk₂', OfNat.ofNat, strictConvex_univ, rfl
-- Module: Mathlib.Analysis.Convex.Strict
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
obtain : ∀ (a : 𝕜) (ha₀ : 0 < a) (ha₁ : a < 1), x = y
⊢ x = y

Tactic:
obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one

Premises used: zero_lt_one, OfNat.ofNat, DenselyOrdered.dense
-- Module: Mathlib.Analysis.Convex.Strict
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
by_contra : ∀ (hxy : ¬x = y), False
⊢ x = y

Tactic:
by_contra hxy
-- Module: Mathlib.Analysis.Convex.Strict
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
hxy : ¬x = y
⊢ False

Tactic:
(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 _ _)

Premises used: HSub.hSub, And.right, add_sub_cancel, And.intro, Exists.intro, OfNat.ofNat, rfl, sub_pos_of_lt
-- Module: Mathlib.Analysis.Convex.Strict
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
hxy : ¬x = y
⊢ False

Tactic:
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 _ _)

Premises used: HSub.hSub, And.right, add_sub_cancel, And.intro, Exists.intro, OfNat.ofNat, rfl, sub_pos_of_lt
-- Module: Mathlib.Analysis.Convex.Strict
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
by_contra by_contra₁ by_contra₂ : ∀ (hxy : ¬x = y), False
⊢ x = y

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 _ _)
-- Module: Mathlib.Analysis.Convex.Strict
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
match_scalars : 1 = (1 - t) * 1 + t * 1
match_scalars₁ : t * 1 = t * 1
⊢ x + t • y = (1 - t) • x + t • (x + y)

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Convex.Strict
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
⊢ 1 = (1 - t) * 1 + t * 1

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Strict
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
⊢ t * 1 = t * 1

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Strict
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)

Tactic:
have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> simp
-- Module: Mathlib.Analysis.Convex.Strict
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
h : x + t • y = (1 - t) • x + t • (x + y)
rw : (1 - t) • x + t • (x + y) ∈ interior s
⊢ x + t • y ∈ interior s

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Convex.Strict
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
h_1 : x + t • y = (1 - t) • x + t • (x + y)
h : x = x + y
rw : x = x + 0
rw₁ rw₂ : x = x
⊢ x + y = x + 0

Tactic:
rw [← h, add_zero]

Premises used: add_zero
-- Module: Mathlib.Analysis.Convex.Strict
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
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ interior s

Tactic:
exact hs hx hxy (fun h => hy <| add_left_cancel (a := x) (by rw [← h, add_zero]))
    (sub_pos_of_lt ht₁) ht₀ (sub_add_cancel 1 t)

Premises used: add_left_cancel, OfNat.ofNat, sub_add_cancel, sub_pos_of_lt
-- Module: Mathlib.Analysis.Convex.Strict
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 : E
inst_5 : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ 0 + x ∈ s

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.Convex.Strict
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 : E
inst_5 : AddRightStrictMono 𝕜
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ t • x ∈ interior s

Tactic:
simpa using hs.add_smul_mem zero_mem (by simpa using hx) hx₀ ht₀ ht₁

Premises used: StrictConvex.add_smul_mem
-- Module: Mathlib.Analysis.Convex.Strict
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 : AddRightMono 𝕜
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
a : x + t • (y - x) ∈ openSegment 𝕜 x y
⊢ x + t • (y - x) ∈ interior s

Tactic:
apply h.openSegment_subset hx hy hxy

Premises used: StrictConvex.openSegment_subset
-- Module: Mathlib.Analysis.Convex.Strict
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 : AddRightMono 𝕜
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
a : Membership.mem (γ := Set E) ((fun (θ : 𝕜) ↦ x + θ • (y - x)) '' Ioo 0 1) (x + t • (y - x))
⊢ x + t • (y - x) ∈ openSegment 𝕜 x y

Tactic:
rw [openSegment_eq_image']

Premises used: openSegment_eq_image'
-- Module: Mathlib.Analysis.Convex.Strict
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 : AddRightMono 𝕜
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ Membership.mem (γ := Set E) ((fun (θ : 𝕜) ↦ x + θ • (y - x)) '' Ioo 0 1) (x + t • (y - x))

Tactic:
mem_image_of_mem _ ⟨ht₀, ht₁⟩

Premises used: Set.mem_image_of_mem, And.intro
-- Module: Mathlib.Analysis.Convex.Strict
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 : AddRightMono 𝕜
h : StrictConvex 𝕜 s
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
t : 𝕜
ht₀ : 0 < t
ht₁ : t < 1
⊢ Membership.mem (γ := Set E) ((fun (θ : 𝕜) ↦ x + θ • (y - x)) '' Ioo 0 1) (x + t • (y - x))

Tactic:
exact mem_image_of_mem _ ⟨ht₀, ht₁⟩
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup E
inst_5 : AddCommGroup 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 : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup E
inst_5 : AddCommGroup 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 : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup E
inst_5 : AddCommGroup 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, Convex.combo_affine_apply hab]

Premises used: Set.mem_preimage, Convex.combo_affine_apply
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup E
inst_5 : AddCommGroup 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: Function.Injective.ne
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup E
inst_5 : AddCommGroup 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 : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
s : Set E
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, Convex.combo_affine_apply hab⟩⟩

Premises used: IsOpenMap.image_interior_subset, ne_of_apply_ne, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul, Convex.combo_affine_apply
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
F : Type u_4
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : TopologicalSpace E
inst_3 : TopologicalSpace F
inst_4 : AddCommGroup E
inst_5 : AddCommGroup F
inst_6 : Module 𝕜 E
inst_7 : Module 𝕜 F
s : Set E
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:
exact
    hf.image_interior_subset _
      ⟨a • x + b • y, ⟨hs hx hy (ne_of_apply_ne _ hxy) ha hb hab, Convex.combo_affine_apply hab⟩⟩

Premises used: IsOpenMap.image_interior_subset, ne_of_apply_ne, HAdd.hAdd, And.intro, Exists.intro, HSMul.hSMul, Convex.combo_affine_apply
-- Module: Mathlib.Analysis.Convex.Strict
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
inst_5 : IsTopologicalAddGroup E
hs : StrictConvex 𝕜 s
⊢ StrictConvex 𝕜 (-s)

Tactic:
hs.is_linear_preimage IsLinearMap.isLinearMap_neg continuous_id.neg neg_injective

Premises used: Continuous.neg, StrictConvex.is_linear_preimage, neg_injective, continuous_id, IsLinearMap.isLinearMap_neg
-- Module: Mathlib.Analysis.Convex.Strict
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 t : Set E
inst_5 : IsTopologicalAddGroup E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
⊢ StrictConvex 𝕜 (s - t)

Tactic:
(sub_eq_add_neg s t).symm ▸ hs.add ht.neg

Premises used: StrictConvex.neg, sub_eq_add_neg, Eq.rec, StrictConvex.add, Eq.symm
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
s : Set E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ 0 < a / (a + b)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
s : Set E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ 0 < b / (a + b)

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
s : Set E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
field
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
s : Set E
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s

Tactic:
h hx hy hxy ha hb
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
s : Set E
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h₁ : a = a / (a + b)
h₂ : b = b / (a + b)
⊢ a • x + b • y ∈ interior s

Tactic:
convert! h hx hy hxy ha hb
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
s : Set E
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h₁ : a = a / 1
h₂ h₃ : a = a
⊢ a = a / (a + b)

Tactic:
rw [hab, div_one]

Premises used: div_one
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
s : Set E
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
h₁ : b = b / 1
h₂ h₃ : b = b
⊢ b = b / (a + b)

Tactic:
rw [hab, div_one]

Premises used: div_one
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
⊢ t ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Strict
Goal:
𝕜 : Type u_1
E : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : TopologicalSpace E
inst_4 : AddCommGroup E
inst_5 : Module 𝕜 E
s : Set E
x : E
hs : StrictConvex 𝕜 s
zero_mem : 0 ∈ s
hx : x ∈ s
hx₀ : x ≠ 0
t : 𝕜
ht : 1 < t
rw : t⁻¹ • x ∈ interior s
⊢ x ∈ t • interior s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ (by positivity)]

Premises used: Set.mem_smul_set_iff_inv_smul_mem₀