awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
s : Set E
f : E → β
hf : AntitoneOn f s
hs : Convex 𝕜 s
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | x ∈ s ∧ r ≤ f x}

Tactic:
MonotoneOn.convex_le (β := βᵒᵈ) hf hs r

Premises used: MonotoneOn.convex_le, setOf
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
s : Set E
f : E → β
hf : AntitoneOn f s
hs : Convex 𝕜 s
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | x ∈ s ∧ r < f x}

Tactic:
MonotoneOn.convex_lt (β := βᵒᵈ) hf hs r

Premises used: setOf, MonotoneOn.convex_lt
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
f : E → β
hf : Monotone f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | f x ≤ r}

Tactic:
Set.sep_univ.subst ((hf.monotoneOn univ).convex_le convex_univ r)

Premises used: Set.sep_univ, MonotoneOn.convex_le, Set.univ, Eq.subst, convex_univ, Monotone.monotoneOn
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
f : E → β
hf : Monotone f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | r ≤ f x}

Tactic:
Set.sep_univ.subst ((hf.monotoneOn univ).convex_ge convex_univ r)

Premises used: Set.sep_univ, MonotoneOn.convex_ge, Set.univ, Eq.subst, convex_univ, Monotone.monotoneOn
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
f : E → β
hf : Antitone f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | f x ≤ r}

Tactic:
Set.sep_univ.subst ((hf.antitoneOn univ).convex_le convex_univ r)

Premises used: Set.sep_univ, Antitone.antitoneOn, AntitoneOn.convex_le, Set.univ, Eq.subst, convex_univ
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
f : E → β
hf : Antitone f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | f x < r}

Tactic:
Set.sep_univ.subst ((hf.antitoneOn univ).convex_lt convex_univ r)

Premises used: Set.sep_univ, Antitone.antitoneOn, Set.univ, Eq.subst, convex_univ, AntitoneOn.convex_lt
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
f : E → β
hf : Antitone f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | r ≤ f x}

Tactic:
Set.sep_univ.subst ((hf.antitoneOn univ).convex_ge convex_univ r)

Premises used: Set.sep_univ, Antitone.antitoneOn, Set.univ, Eq.subst, convex_univ, AntitoneOn.convex_ge
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : LinearOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : PartialOrder β
inst_6 : Module 𝕜 E
inst_7 : PosSMulMono 𝕜 E
f : E → β
hf : Antitone f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | r < f x}

Tactic:
Set.sep_univ.subst ((hf.antitoneOn univ).convex_gt convex_univ r)

Premises used: Set.sep_univ, Antitone.antitoneOn, AntitoneOn.convex_gt, Set.univ, Eq.subst, convex_univ
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
c : 𝕜
⊢ Convex 𝕜 (c • s)

Tactic:
hs.linear_image (LinearMap.lsmul _ _ c)

Premises used: LinearMap.lsmul, Convex.linear_image, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
c : 𝕜
⊢ Convex 𝕜 (E := E) ((fun (z : E) ↦ c • z) ⁻¹' s)

Tactic:
hs.linear_preimage (LinearMap.lsmul _ _ c)

Premises used: LinearMap.lsmul, DFunLike.coe, Convex.linear_preimage
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z : E
c : 𝕜
⊢ Convex 𝕜 (E := E) ((fun (x : E) ↦ z + c • x) '' s)

Tactic:
simpa only [← image_smul, ← image_vadd, image_image] using (hs.smul c).vadd z

Premises used: Set.image_image, Set.image_smul, Convex.vadd, Set.image_vadd, Convex.smul
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a b : E
rw : ∀ ⦃x : E⦄, x ∈ openSegment 𝕜 a b → ∀ ⦃y : E⦄, y ∈ openSegment 𝕜 a b → openSegment 𝕜 x y ⊆ openSegment 𝕜 a b
⊢ Convex 𝕜 (openSegment 𝕜 a b)

Tactic:
rw [convex_iff_openSegment_subset]

Premises used: convex_iff_openSegment_subset
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a_1 b_1 : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * ap + b * aq

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a_1 b_1 : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ 0 < a * bp + b * bq

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a_1 b_1 : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
refine_1 : a * ap + b * aq + (a * bp + b * bq) = 1
refine_2 : (a * ap + b * aq) • a_1 + (a * bp + b * bq) • b_1 = a • (ap • a_1 + bp • b_1) + b • (aq • a_1 + bq • b_1)
⊢ a • (ap • a_1 + bp • b_1) + b • (aq • a_1 + bq • b_1) ∈ openSegment 𝕜 a_1 b_1

Tactic:
refine ⟨a * ap + b * aq, a * bp + b * bq, by positivity, by positivity, ?_, ?_⟩
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a_1 b_1 : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
a₁ a₂ a₃ a₄ : a * ap + b * aq + (a * bp + b * bq) + (a + b + 1) = 1 + (a * ap + a * bp + (b * aq + b * bq) + (a + b))
⊢ a * ap + b * aq + (a * bp + b * bq) + (a * 1 + b * 1 + 1) = 1 + (a * (ap + bp) + b * (aq + bq) + (a + b))

Tactic:
noncomm_ring
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a_1 b_1 : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
a₁ : a * ap + b * aq + (a * bp + b * bq) + (a * 1 + b * 1 + 1) = 1 + (a * (ap + bp) + b * (aq + bq) + (a + b))
⊢ a * ap + b * aq + (a * bp + b * bq) = 1

Tactic:
linear_combination (norm := noncomm_ring) a * habp + b * habq + hab
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
a_1 b_1 : E
ap bp : 𝕜
hap : 0 < ap
hbp : 0 < bp
habp : ap + bp = 1
aq bq : 𝕜
haq : 0 < aq
hbq : 0 < bq
habq : aq + bq = 1
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a * ap + b * aq) • a_1 + (a * bp + b * bq) • b_1 = a • (ap • a_1 + bp • b_1) + b • (aq • a_1 + bq • b_1)

Tactic:
module
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
a : E
h : Convex 𝕜 (a +ᵥ s)
⊢ Convex 𝕜 s

Tactic:
simpa using h.vadd (-a)

Premises used: Convex.vadd, Neg.neg
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
Q : AffineSubspace 𝕜 E
x : E
hx : x ∈ (↑Q : Set E)
y : E
hy : y ∈ (↑Q : Set E)
a b : 𝕜
h : 0 ≤ a
h_1 : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ (↑Q : Set E)

Tactic:
simpa [Convex.combo_eq_smul_sub_add hab] using Q.2 _ hy hx hx

Premises used: Convex.combo_eq_smul_sub_add, AffineSubspace.smul_vsub_vadd_mem
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
f : E →ᵃ[𝕜] F
s : Set F
hs : Convex 𝕜 s
⊢ Convex.{u_1, u_2} 𝕜 (E := E) ((⇑f : (a : E) → F) ⁻¹' s)

Tactic:
fun _ hx => (hs hx).affine_preimage _

Premises used: StarConvex.affine_preimage, Convex
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
hs : Convex 𝕜 s
x : E
hx : x ∈ s
⊢ StarConvex.{u_1, u_3} 𝕜 (E := F) ((f : (a : E) → F) x : F) ((⇑f : (a : E) → F) '' s : Set F)

Tactic:
(hs hx).affine_image _

Premises used: StarConvex.affine_image
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : AddCommGroup F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
hs : Convex 𝕜 s
x : E
hx : x ∈ s
⊢ StarConvex.{u_1, u_3} 𝕜 (E := F) ((f : (a : E) → F) x : F) ((⇑f : (a : E) → F) '' s : Set F)

Tactic:
exact (hs hx).affine_image _

Premises used: StarConvex.affine_image
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
⊢ Convex 𝕜 (-s)

Tactic:
hs.is_linear_preimage IsLinearMap.isLinearMap_neg

Premises used: Convex.is_linear_preimage, IsLinearMap.isLinearMap_neg
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
rw : Convex 𝕜 (s + -t)
⊢ Convex 𝕜 (s - t)

Tactic:
rw [sub_eq_add_neg]

Premises used: sub_eq_add_neg
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s + -t)

Tactic:
hs.add ht.neg

Premises used: Convex.neg, Convex.add
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s + -t)

Tactic:
exact hs.add ht.neg

Premises used: Convex.neg, Convex.add
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
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.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
noncomm_ring noncomm_ring₁ noncomm_ring₂ noncomm_ring₃ : 1 = 1 + -t + t
⊢ 1 = (1 - t) * 1 + t * 1

Tactic:
noncomm_ring
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
⊢ t * 1 = t * 1

Tactic:
noncomm_ring
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
⊢ x + t • y = (1 - t) • x + t • (x + y)

Tactic:
have h : x + t • y = (1 - t) • x + t • (x + y) := by match_scalars <;> noncomm_ring
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
h : x + t • y = (1 - t) • x + t • (x + y)
rw : (1 - t) • x + t • (x + y) ∈ s
⊢ x + t • y ∈ s

Tactic:
rw [h]
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ s

Tactic:
hs hx hy (sub_nonneg_of_le ht.2) ht.1 (sub_add_cancel _ _)

Premises used: sub_nonneg_of_le, And.right, And.left, sub_add_cancel
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
hs : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : x + y ∈ s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ s

Tactic:
exact hs hx hy (sub_nonneg_of_le ht.2) ht.1 (sub_add_cancel _ _)

Premises used: sub_nonneg_of_le, And.right, And.left, sub_add_cancel
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
hs : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
⊢ 0 + x ∈ s

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
hs : Convex 𝕜 s
x : E
zero_mem : 0 ∈ s
hx : x ∈ s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
⊢ t • x ∈ s

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

Premises used: Convex.add_smul_mem
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
⊢ MapsTo.{u_1, u_2} (α := 𝕜) (⇑(AffineMap.lineMap x y) : (a : 𝕜) → E) (Icc 0 1) s

Tactic:
simpa only [mapsTo_iff_image_subset, segment_eq_image_lineMap] using h.segment_subset hx hy

Premises used: Set.mapsTo_iff_image_subset, segment_eq_image_lineMap, Convex.segment_subset
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
⊢ Membership.mem (α := E) s ((AffineMap.lineMap x y : (a : 𝕜) → E) t : E)

Tactic:
h.mapsTo_lineMap hx hy ht

Premises used: Convex.mapsTo_lineMap
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
rw : t • (y - x) + x ∈ s
⊢ x + t • (y - x) ∈ s

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
⊢ t • (y - x) + x ∈ s

Tactic:
h.lineMap_mem hx hy ht

Premises used: Convex.lineMap_mem, Set.Mem
-- Module: Mathlib.Analysis.Convex.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
s : Set E
inst_4 : AddRightMono 𝕜
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
t : 𝕜
ht : Membership.mem (γ := Set 𝕜) (Icc 0 1) t
⊢ t • (y - x) + x ∈ s

Tactic:
exact h.lineMap_mem hx hy ht

Premises used: Convex.lineMap_mem
-- 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
a b : 𝕜'
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ (r : 𝕜), (σ : (a : 𝕜) → 𝕜') r = a

Tactic:
RingHomSurjective.is_surjective ..

Premises used: RingHomSurjective.is_surjective
-- 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
a b : 𝕜'
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
obtain :
  ∀ (r : 𝕜) (ha : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜'))
    (hab : HAdd.hAdd (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜') b = 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 (β := F') b ((f : (a : E) → F') y : F'))
⊢ Membership.mem (γ := Set F') ((⇑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:
obtain ⟨r, rfl⟩ : ∃ r : 𝕜, σ r = a := RingHomSurjective.is_surjective ..

Premises used: rfl, RingHomSurjective.is_surjective
-- 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
b : 𝕜'
hb : 0 ≤ b
r : 𝕜
ha : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜')
hab : HAdd.hAdd (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜') b = 1
⊢ ∃ (t : 𝕜), (σ : (a : 𝕜) → 𝕜') t = b

Tactic:
RingHomSurjective.is_surjective ..

Premises used: RingHomSurjective.is_surjective
-- 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
b : 𝕜'
hb : 0 ≤ b
r : 𝕜
ha : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜')
hab : HAdd.hAdd (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜') b = 1
obtain :
  ∀ (t : 𝕜) (hb : LE.le.{u_5} (α := 𝕜') (0 : 𝕜') ((σ : (a : 𝕜) → 𝕜') t : 𝕜'))
    (hab : HAdd.hAdd (α := 𝕜') (β := 𝕜') ((σ : (a : 𝕜) → 𝕜') r : 𝕜') ((σ : (a : 𝕜) → 𝕜') 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'))
⊢ 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 (β := F') b ((f : (a : E) → F') y : F'))

Tactic:
obtain ⟨t, rfl⟩ : ∃ t : 𝕜, σ t = b := RingHomSurjective.is_surjective ..

Premises used: rfl, RingHomSurjective.is_surjective
-- 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
⊢ 0 ≤ r

Tactic:
simp_all [(@hσ 0 r).mp]

Premises used: Iff.mp
-- 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
⊢ 0 ≤ t

Tactic:
simp_all [(@hσ 0 t).mp]

Premises used: Iff.mp