awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : PartialOrder 𝕜
𝕜' : Type u_5
inst_3 : Semiring 𝕜'
inst_4 : PartialOrder 𝕜'
σ : 𝕜 →+* 𝕜'
inst_5 : RingHomSurjective σ
F' : Type u_6
inst_6 : AddCommMonoid F'
inst_7 : Module 𝕜' F'
inst_8 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
hσ : ∀ {s t : 𝕜}, LE.le.{u_5} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') s : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜') ↔ s ≤ t
f : E →ₛₗ[σ] F'
x : E
hx : x ∈ s
y : E
hy : y ∈ s
r : 𝕜
ha : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜')
t : 𝕜
hb : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜')
hab : HAdd.hAdd (α := 𝕜') (β := 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜') = 1
⊢ (f : (a : E) → F') (r • x + t • y) =
    HSMul.hSMul.{u_5, u_6, u_6} (α := 𝕜') (β := F') ((σ : (a : 𝕜) → 𝕜') r : 𝕜') ((f : (a : E) → F') x : F') +
      HSMul.hSMul.{u_5, u_6, u_6} (α := 𝕜') (β := F') ((σ : (a : 𝕜) → 𝕜') t : 𝕜') ((f : (a : E) → F') y : F')

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : PartialOrder 𝕜
𝕜' : Type u_5
inst_3 : Semiring 𝕜'
inst_4 : PartialOrder 𝕜'
σ : 𝕜 →+* 𝕜'
inst_5 : RingHomSurjective σ
F' : Type u_6
inst_6 : AddCommMonoid F'
inst_7 : Module 𝕜' F'
inst_8 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
hσ : ∀ {s t : 𝕜}, LE.le.{u_5} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') s : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜') ↔ s ≤ t
f : E →ₛₗ[σ] F'
x : E
hx : x ∈ s
y : E
hy : y ∈ s
r : 𝕜
ha : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜')
t : 𝕜
hb : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜')
hab : HAdd.hAdd (α := 𝕜') (β := 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜') = 1
refine : r + t = 1
⊢ Membership.mem (γ := Set F') ((⇑f : (a : E) → F') '' s)
    (HSMul.hSMul.{u_5, u_6, u_6} (α := 𝕜') (β := F') ((σ : (a : 𝕜) → 𝕜') r : 𝕜') ((f : (a : E) → F') x : F') +
      HSMul.hSMul.{u_5, u_6, u_6} (α := 𝕜') (β := F') ((σ : (a : 𝕜) → 𝕜') t : 𝕜') ((f : (a : E) → F') y : F'))

Tactic:
refine ⟨r • x + t • y, hs hx hy (by simp_all [(@hσ 0 r).mp]) (by simp_all [(@hσ 0 t).mp])
    ?_, by simp⟩
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : PartialOrder 𝕜
𝕜' : Type u_5
inst_3 : Semiring 𝕜'
inst_4 : PartialOrder 𝕜'
σ : 𝕜 →+* 𝕜'
inst_5 : RingHomSurjective σ
F' : Type u_6
inst_6 : AddCommMonoid F'
inst_7 : Module 𝕜' F'
inst_8 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
hσ : ∀ {s t : 𝕜}, LE.le.{u_5} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') s : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜') ↔ s ≤ t
f : E →ₛₗ[σ] F'
x : E
hx : x ∈ s
y : E
hy : y ∈ s
r : 𝕜
ha : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜')
t : 𝕜
hb : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜')
hab : HAdd.hAdd (α := 𝕜') (β := 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜') = 1
⊢ Function.Injective.{u_1 + 1, u_5 + 1} (α := 𝕜) (β := 𝕜') (⇑σ : (a : 𝕜) → 𝕜')

Tactic:
Function.Injective.of_eq_imp_le (hσ.mp ·.le)

Premises used: Eq.le, Iff.mp, Function.Injective.of_eq_imp_le
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : PartialOrder 𝕜
𝕜' : Type u_5
inst_3 : Semiring 𝕜'
inst_4 : PartialOrder 𝕜'
σ : 𝕜 →+* 𝕜'
inst_5 : RingHomSurjective σ
F' : Type u_6
inst_6 : AddCommMonoid F'
inst_7 : Module 𝕜' F'
inst_8 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
hσ : ∀ {s t : 𝕜}, LE.le.{u_5} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') s : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜') ↔ s ≤ t
f : E →ₛₗ[σ] F'
x : E
hx : x ∈ s
y : E
hy : y ∈ s
r : 𝕜
ha : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜')
t : 𝕜
hb : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜')
hab : HAdd.hAdd (α := 𝕜') (β := 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜') = 1
apply_fun : Eq.{u_5 + 1} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') (r + t) : 𝕜') ((σ : (a : 𝕜) → 𝕜') 1 : 𝕜')
⊢ r + t = 1

Tactic:
apply_fun σ using Function.Injective.of_eq_imp_le (hσ.mp ·.le)

Premises used: Eq.le, Iff.mp, Function.Injective.of_eq_imp_le
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : PartialOrder 𝕜
𝕜' : Type u_5
inst_3 : Semiring 𝕜'
inst_4 : PartialOrder 𝕜'
σ : 𝕜 →+* 𝕜'
inst_5 : RingHomSurjective σ
F' : Type u_6
inst_6 : AddCommMonoid F'
inst_7 : Module 𝕜' F'
inst_8 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
hσ : ∀ {s t : 𝕜}, LE.le.{u_5} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') s : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜') ↔ s ≤ t
f : E →ₛₗ[σ] F'
x : E
hx : x ∈ s
y : E
hy : y ∈ s
r : 𝕜
ha : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜')
t : 𝕜
hb : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜')
hab : HAdd.hAdd (α := 𝕜') (β := 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜') = 1
⊢ Eq.{u_5 + 1} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') (r + t) : 𝕜') ((σ : (a : 𝕜) → 𝕜') 1 : 𝕜')

Tactic:
simpa
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : LinearOrder 𝕜
inst_3 : IsOrderedRing 𝕜
inst_4 : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
rw :
  ∀ ⦃x : E⦄,
    Membership.mem (γ := Set E) {x : E | f x ≤ B} x →
      ∀ ⦃y : E⦄, Membership.mem (γ := Set E) {x : E | f x ≤ B} y → [x -[𝕜] y] ⊆ {x : E | f x ≤ B}
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | f x ≤ B}

Tactic:
rw [convex_iff_segment_subset]

Premises used: convex_iff_segment_subset
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : LinearOrder 𝕜
inst_3 : IsOrderedRing 𝕜
inst_4 : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : Membership.mem (γ := Set E) {x : E | f x ≤ B} x
y : E
hy : Membership.mem (γ := Set E) {x : E | f x ≤ B} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ f (a • x + b • y) ≤ a • f x + b • f y

Tactic:
le_trans (hf1 _ _) (add_le_add (hf2 x ha) (hf2 y hb))

Premises used: add_le_add, le_trans
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : LinearOrder 𝕜
inst_3 : IsOrderedRing 𝕜
inst_4 : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : Membership.mem (γ := Set E) {x : E | f x ≤ B} x
y : E
hy : Membership.mem (γ := Set E) {x : E | f x ≤ B} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
h₁ : f x ≤ B
h₂ : f y ≤ B
⊢ a • f x + b • f y ≤ a • B + b • B

Tactic:
gcongr
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : LinearOrder 𝕜
inst_3 : IsOrderedRing 𝕜
inst_4 : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : Membership.mem (γ := Set E) {x : E | f x ≤ B} x
y : E
hy : Membership.mem (γ := Set E) {x : E | f x ≤ B} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ f x ≤ B

Tactic:
assumption
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : LinearOrder 𝕜
inst_3 : IsOrderedRing 𝕜
inst_4 : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : Membership.mem (γ := Set E) {x : E | f x ≤ B} x
y : E
hy : Membership.mem (γ := Set E) {x : E | f x ≤ B} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ f y ≤ B

Tactic:
assumption
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : LinearOrder 𝕜
inst_3 : IsOrderedRing 𝕜
inst_4 : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : Membership.mem (γ := Set E) {x : E | f x ≤ B} x
y : E
hy : Membership.mem (γ := Set E) {x : E | f x ≤ B} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
rw : (a + b) • B ≤ B
rw₁ : HSMul.hSMul (α := 𝕜) 1 B ≤ B
rw₂ rw₃ : B ≤ B
⊢ a • B + b • B ≤ B

Tactic:
rw [← add_smul, hs, one_smul]

Premises used: one_smul, add_smul
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : LinearOrder 𝕜
inst_3 : IsOrderedRing 𝕜
inst_4 : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
x : E
hx : Membership.mem (γ := Set E) {x : E | f x ≤ B} x
y : E
hy : Membership.mem (γ := Set E) {x : E | f x ≤ B} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
_ : a • f x + b • f y ≤ a • B + b • B
_₁ : a • B + b • B ≤ B
⊢ Membership.mem (γ := Set E) {x : E | f x ≤ B} (a • x + b • y)

Tactic:
calc
    _ ≤ a • (f x) + b • (f y) := le_trans (hf1 _ _) (add_le_add (hf2 x ha) (hf2 y hb))
    _ ≤ a • B + b • B := by gcongr <;> assumption
    _ ≤ B := by rw [← add_smul, hs, one_smul]

Premises used: add_le_add, le_trans
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
inst_5 : Invertible (α := 𝕜) 2
s : Set E
x y : E
h : Convex 𝕜 s
hx : x ∈ s
hy : y ∈ s
⊢ midpoint 𝕜 x y ∈ s

Tactic:
h.segment_subset hx hy <| midpoint_mem_segment x y

Premises used: midpoint_mem_segment, Convex.segment_subset
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
⊢ Convex 𝕜 s ↔
    ∀ ⦃x : E⦄,
      x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s

Tactic:
forall₂_congr fun _ _ => starConvex_iff_div

Premises used: forall₂_congr, Convex, starConvex_iff_div
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
rw : t⁻¹ • x ∈ s
⊢ x ∈ t • s

Tactic:
rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']

Premises used: LT.lt.ne', zero_lt_one, LT.lt.trans_le, Set.mem_smul_set_iff_inv_smul_mem₀
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ t⁻¹ • x ∈ s

Tactic:
h.smul_mem_of_zero_mem zero_mem hx
    ⟨inv_nonneg.2 (zero_le_one.trans ht), inv_le_one_of_one_le₀ ht⟩

Premises used: Iff.mpr, Set.Mem, zero_le_one, inv_nonneg, And.intro, Convex.smul_mem_of_zero_mem, LE.le.trans, inv_le_one_of_one_le₀
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ t⁻¹ • x ∈ s

Tactic:
exact h.smul_mem_of_zero_mem zero_mem hx
    ⟨inv_nonneg.2 (zero_le_one.trans ht), inv_le_one_of_one_le₀ ht⟩

Premises used: Iff.mpr, zero_le_one, inv_nonneg, And.intro, Convex.smul_mem_of_zero_mem, LE.le.trans, inv_le_one_of_one_le₀
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
inl :
  ∀ (hp hq : LE.le.{u_1} (α := 𝕜) 0 0),
    ∃ z ∈ s,
      HAdd.hAdd (α := 𝕜) 0 0 • z = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
inr : ∀ (hpq : ¬(p = 0 ∧ q = 0)), ∃ z ∈ s, (p + q) • z = p • x + q • y
⊢ ∃ z ∈ s, (p + q) • z = p • x + q • y

Tactic:
rcases _root_.em (p = 0 ∧ q = 0) with (⟨rfl, rfl⟩ | hpq)

Premises used: em, And, OfNat.ofNat, Eq, rfl
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
hp hq : LE.le.{u_1} (α := 𝕜) 0 0
right : HAdd.hAdd (α := 𝕜) 0 0 • x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
⊢ ∃ z ∈ s,
    HAdd.hAdd (α := 𝕜) 0 0 • z = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y

Tactic:
use x, hx
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
hp hq : LE.le.{u_1} (α := 𝕜) 0 0
⊢ HAdd.hAdd (α := 𝕜) 0 0 • x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y

Tactic:
simp
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : ¬(p = 0 ∧ q = 0)
⊢ 0 < p + q

Tactic:
replace hpq : 0 < p + q :=
      (add_nonneg hp hq).lt_of_ne' (mt (add_eq_zero_iff_of_nonneg hp hq).1 hpq)
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
⊢ ∃ z ∈ s, (p + q) • z = p • x + q • y

Tactic:
⟨_, convex_iff_div.1 h hx hy hp hq hpq, ?_⟩

Premises used: And.intro, convex_iff_div, Exists.intro, Iff.mp
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
inr : (p + q) • ((p / (p + q)) • x + (q / (p + q)) • y) = p • x + q • y
⊢ ∃ z ∈ s, (p + q) • z = p • x + q • y

Tactic:
refine ⟨_, convex_iff_div.1 h hx hy hp hq hpq, ?_⟩
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
match_scalars : (p + q) * (p / (p + q) * 1) = p * 1
match_scalars₁ : (p + q) * (q / (p + q) * 1) = q * 1
⊢ (p + q) • ((p / (p + q)) • x + (q / (p + q)) • y) = p • x + q • y

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
⊢ (p + q) * (p / (p + q) * 1) = p * 1

Tactic:
field
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
⊢ (p + q) * (q / (p + q) * 1) = q * 1

Tactic:
field
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
v₁ : E
h₁ : v₁ ∈ s
v₂ : E
h₂ : v₂ ∈ s
⊢ (fun (x1 x2 : E) ↦ x1 + x2) ((fun (x : E) ↦ p • x) v₁) ((fun (x : E) ↦ q • x) v₂) ∈ (p + q) • s

Tactic:
h_conv.exists_mem_add_smul_eq h₁ h₂ hp hq

Premises used: Set.Mem, setOf, Set.image, Convex.exists_mem_add_smul_eq
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
p q : 𝕜
hp : 0 ≤ p
hq : 0 ≤ q
v₁ : E
h₁ : v₁ ∈ s
v₂ : E
h₂ : v₂ ∈ s
⊢ (fun (x1 x2 : E) ↦ x1 + x2) ((fun (x : E) ↦ p • x) v₁) ((fun (x : E) ↦ q • x) v₂) ∈ (p + q) • s

Tactic:
exact h_conv.exists_mem_add_smul_eq h₁ h₂ hp hq

Premises used: Convex.exists_mem_add_smul_eq
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
⊢ LE.le.{u_1} (α := 𝕜) 0 2⁻¹

Tactic:
norm_num
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
rw : HAdd.hAdd (α := 𝕜) 2⁻¹ 2⁻¹ • s = s
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ s + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ s = s

Tactic:
rw [← h_conv.add_smul (by norm_num) (by norm_num)]

Premises used: Convex.add_smul
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
ring_nf : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 s = s
⊢ HAdd.hAdd (α := 𝕜) 2⁻¹ 2⁻¹ • s = s

Tactic:
ring_nf
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
s : Set E
h_conv : Convex 𝕜 s
rw rw₁ : s = s
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 s = s

Tactic:
rw [one_smul]

Premises used: one_smul
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun (x1 x2 : E) ↦ x1 ≤ x2) s
⊢ Convex 𝕜 s

Tactic:
convex_iff_segment_subset.mpr fun x hx y hy => ?_

Premises used: Iff.mpr, convex_iff_segment_subset
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun (x1 x2 : E) ↦ x1 ≤ x2) s
refine : ∀ (x : E) (hx : x ∈ s) (y : E) (hy : y ∈ s), [x -[𝕜] y] ⊆ s
⊢ Convex 𝕜 s

Tactic:
refine convex_iff_segment_subset.mpr fun x hx y hy => ?_

Premises used: Iff.mpr, convex_iff_segment_subset
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun (x1 x2 : E) ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
inl : ∀ (hxy : x ≤ y), [x -[𝕜] y] ⊆ s
inr : ∀ (hyx : y ≤ x), [x -[𝕜] y] ⊆ s
⊢ [x -[𝕜] y] ⊆ s

Tactic:
obtain hxy | hyx := h.total hx hy

Premises used: IsChain.total
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun (x1 x2 : E) ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≤ y
⊢ [x -[𝕜] y] ⊆ s

Tactic:
(segment_subset_Icc hxy).trans (hs.out hx hy)

Premises used: HasSubset.Subset.trans, Set.OrdConnected.out, segment_subset_Icc
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun (x1 x2 : E) ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≤ y
⊢ [x -[𝕜] y] ⊆ s

Tactic:
exact (segment_subset_Icc hxy).trans (hs.out hx hy)

Premises used: HasSubset.Subset.trans, Set.OrdConnected.out, segment_subset_Icc
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun (x1 x2 : E) ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
inr : [y -[𝕜] x] ⊆ s
⊢ [x -[𝕜] y] ⊆ s

Tactic:
rw [segment_symm]

Premises used: segment_symm
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun (x1 x2 : E) ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [y -[𝕜] x] ⊆ s

Tactic:
(segment_subset_Icc hyx).trans (hs.out hy hx)

Premises used: HasSubset.Subset.trans, Set.OrdConnected.out, segment_subset_Icc
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun (x1 x2 : E) ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [y -[𝕜] x] ⊆ s

Tactic:
exact (segment_subset_Icc hyx).trans (hs.out hy hx)

Premises used: HasSubset.Subset.trans, Set.OrdConnected.out, segment_subset_Icc
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
⊢ Convex 𝕜 s

Tactic:
hs.convex_of_chain <| isChain_of_trichotomous s

Premises used: Set.OrdConnected.convex_of_chain, isChain_of_trichotomous
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
simp_rw : (∀ ⦃x : 𝕜⦄, x ∈ s → ∀ ⦃y : 𝕜⦄, y ∈ s → [x -[𝕜] y] ⊆ s) ↔ s.OrdConnected
simp_rw₁ : (∀ ⦃x : 𝕜⦄, x ∈ s → ∀ ⦃y : 𝕜⦄, y ∈ s → uIcc x y ⊆ s) ↔ s.OrdConnected
⊢ Convex 𝕜 s ↔ s.OrdConnected

Tactic:
simp_rw [convex_iff_segment_subset, segment_eq_uIcc, ordConnected_iff_uIcc_subset]

Premises used: segment_eq_uIcc, convex_iff_segment_subset, Set.ordConnected_iff_uIcc_subset
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
K : Submodule 𝕜 E
repeat' :
  ∀ ⦃x : E⦄,
    x ∈ (↑K : Set E) →
      ∀ ⦃y : E⦄, y ∈ (↑K : Set E) → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ (↑K : Set E)
⊢ Convex 𝕜 (↑K : Set E)

Tactic:
repeat' intro
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
K : Submodule 𝕜 E
x : E
h : x ∈ (↑K : Set E)
y : E
h_1 : y ∈ (↑K : Set E)
a b : 𝕜
h_2 : 0 ≤ a
h_3 : 0 ≤ b
h_4 : a + b = 1
⊢ a • x + b • y ∈ (↑K : Set E)

Tactic:
add_mem (smul_mem _ _ ?_) (smul_mem _ _ ?_)

Premises used: AddMemClass.add_mem, Submodule.smul_mem
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
K : Submodule 𝕜 E
x : E
h : x ∈ (↑K : Set E)
y : E
h_1 : y ∈ (↑K : Set E)
a b : 𝕜
h_2 : 0 ≤ a
h_3 : 0 ≤ b
h_4 : a + b = 1
refine_1 : x ∈ K
refine_2 : y ∈ K
⊢ a • x + b • y ∈ (↑K : Set E)

Tactic:
refine add_mem (smul_mem _ _ ?_) (smul_mem _ _ ?_)

Premises used: AddMemClass.add_mem, Submodule.smul_mem
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
K : Submodule 𝕜 E
x : E
h : x ∈ (↑K : Set E)
y : E
h_1 : y ∈ (↑K : Set E)
a b : 𝕜
h_2 : 0 ≤ a
h_3 : 0 ≤ b
h_4 : a + b = 1
⊢ x ∈ K

Tactic:
assumption