awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
inst_4 : ZeroLEOneClass 𝕜
hx : x ∈ s
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → openSegment 𝕜 x y ⊆ s

Tactic:
starConvex_iff_segment_subset.trans <|
    forall₂_congr fun _ hy => (openSegment_subset_iff_segment_subset hx hy).symm

Premises used: starConvex_iff_segment_subset, forall₂_congr, Iff.trans, Iff.symm, openSegment_subset_iff_segment_subset
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
y : E
a b : 𝕜
h : 0 ≤ a
h_1 : 0 ≤ b
hab : a + b = 1
⊢ Membership.mem (γ := Set E) {y} (a • y + b • y)

Tactic:
Convex.combo_self hab _

Premises used: Set.Mem, setOf, Convex.combo_self, Set.singleton
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
y : E
a b : 𝕜
h : 0 ≤ a
h_1 : 0 ≤ b
hab : a + b = 1
⊢ Membership.mem (γ := Set E) {y} (a • y + b • y)

Tactic:
exact Convex.combo_self hab _

Premises used: Convex.combo_self
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
x : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
y : E
hy : y ∈ s
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 [f.map_add, f.map_smul, f.map_smul]

Premises used: LinearMap.map_add, LinearMap.map_smul
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
x : E
s : Set E
hs : StarConvex 𝕜 x s
f : E →ₗ[𝕜] F
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 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:
exact ⟨a • x + b • y, hs hy ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
x : E
s : Set E
hs : StarConvex 𝕜 x s
f : E → F
hf : IsLinearMap 𝕜 f
⊢ StarConvex 𝕜 (f x) (f '' s)

Tactic:
hs.linear_image <| hf.mk' f

Premises used: StarConvex.linear_image, IsLinearMap.mk'
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
x : E
s : Set F
f : E →ₗ[𝕜] F
hs : StarConvex 𝕜 ((f : (a : E) → F) x) s
y : E
hy : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) 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) ∈ s
⊢ Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' 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.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
x : E
s : Set F
f : E →ₗ[𝕜] F
hs : StarConvex 𝕜 ((f : (a : E) → F) x) s
y : E
hy : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) 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) ∈ s

Tactic:
hs hy ha hb hab

Premises used: Set.Mem
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
x : E
s : Set F
f : E →ₗ[𝕜] F
hs : StarConvex 𝕜 ((f : (a : E) → F) x) s
y : E
hy : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) 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) ∈ s

Tactic:
exact hs hy ha hb hab
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : AddCommMonoid F
inst_4 : Module 𝕜 E
inst_5 : Module 𝕜 F
x : E
s : Set F
f : E → F
hs : StarConvex 𝕜 (f x) s
hf : IsLinearMap 𝕜 f
⊢ StarConvex 𝕜 x (f ⁻¹' s)

Tactic:
hs.linear_preimage <| hf.mk' f

Premises used: IsLinearMap.mk', StarConvex.linear_preimage
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
rw : StarConvex 𝕜 (x + y) ((fun (x : E × E) ↦ x.1 + x.2) '' s ×ˢ t)
⊢ StarConvex 𝕜 (x + y) (s + t)

Tactic:
rw [← add_image_prod]

Premises used: Set.add_image_prod
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + y) ((fun (x : E × E) ↦ x.1 + x.2) '' s ×ˢ t)

Tactic:
(hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

Premises used: StarConvex.prod, IsLinearMap.isLinearMap_add, StarConvex.is_linear_image
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x y : E
s t : Set E
hs : StarConvex 𝕜 x s
ht : StarConvex 𝕜 y t
⊢ StarConvex 𝕜 (x + y) ((fun (x : E × E) ↦ x.1 + x.2) '' s ×ˢ t)

Tactic:
exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

Premises used: StarConvex.prod, IsLinearMap.isLinearMap_add, StarConvex.is_linear_image
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z y : E
hy : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) '' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
obtain :
  ∀ (y' : E) (hy' : y' ∈ s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) '' s)
      (a • (z + x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y'))
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) '' s) (a • (z + x) + b • y)

Tactic:
obtain ⟨y', hy', rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) '' s)
    (a • (z + x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y'))

Tactic:
⟨a • x + b • y', hs hy' ha hb hab, ?_⟩

Premises used: Set.Mem, setOf, HAdd.hAdd, And.intro, Exists.intro, Set.image, HSMul.hSMul
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
refine : (fun (x : E) ↦ z + x) (a • x + b • y') = a • (z + x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y')
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) '' s)
    (a • (z + x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y'))

Tactic:
refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
match_scalars : 1 = a * 1 + b * 1
match_scalars₁ : a * 1 = a * 1
match_scalars₂ : b * 1 = b * 1
⊢ (fun (x : E) ↦ z + x) (a • x + b • y') = a • (z + x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y')

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ 1 = a * 1 + b * 1

Tactic:
simp [hab]
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ a * 1 = a * 1

Tactic:
simp [hab]
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ b * 1 = b * 1

Tactic:
simp [hab]
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z y : E
hy : Membership.mem (γ := Set E) ((fun (x : E) ↦ x + z) '' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
obtain :
  ∀ (y' : E) (hy' : y' ∈ s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ x + z) '' s)
      (a • (x + z) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ x + z) y'))
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ x + z) '' s) (a • (x + z) + b • y)

Tactic:
obtain ⟨y', hy', rfl⟩ := hy

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ x + z) '' s)
    (a • (x + z) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ x + z) y'))

Tactic:
⟨a • x + b • y', hs hy' ha hb hab, ?_⟩

Premises used: Set.Mem, setOf, HAdd.hAdd, And.intro, Exists.intro, Set.image, HSMul.hSMul
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
refine : (fun (x : E) ↦ x + z) (a • x + b • y') = a • (x + z) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ x + z) y')
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ x + z) '' s)
    (a • (x + z) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ x + z) y'))

Tactic:
refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
y' : E
hy' : y' ∈ s
match_scalars : a * 1 = a * 1
match_scalars₁ : b * 1 = b * 1
match_scalars₂ : 1 = a * 1 + b * 1
⊢ (fun (x : E) ↦ x + z) (a • x + b • y') = a • (x + z) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ x + z) y')

Tactic:
match_scalars
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (z + x) s
y : E
hy : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (z + x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ s

Tactic:
have h := hs hy ha hb hab
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (z + x) s
y : E
hy : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h : a • (z + x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ s
rwa :
  ∀ (h : a • z + a • x + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
rwa₁ :
  ∀ (h : a • z + a • x + (b • z + b • y) ∈ s), Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
rwa₂ :
  ∀ (h : a • z + b • z + (a • x + b • y) ∈ s), Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
rwa₃ :
  ∀ (h : (a + b) • z + (a • x + b • y) ∈ s), Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
rwa₄ :
  ∀ (h : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 z + (a • x + b • y) ∈ s),
    Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
rwa₅ rwa₆ rwa₇ rwa₈ :
  ∀ (h : z + (a • x + b • y) ∈ s), Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)

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

Premises used: one_smul, add_smul, add_add_add_comm, smul_add
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (x + z) s
⊢ StarConvex 𝕜 (z + x) s

Tactic:
rw [add_comm] at hs

Premises used: add_comm
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x z : E
s : Set E
hs : StarConvex 𝕜 (z + x) s
⊢ StarConvex 𝕜 x ((fun (x : E) ↦ x + z) ⁻¹' s)

Tactic:
simpa only [add_comm] using hs.preimage_add_right

Premises used: StarConvex.preimage_add_right, add_comm
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
x y : E
s : Set (E × E)
hs : StarConvex 𝕜 (x, y) s
⊢ StarConvex 𝕜 (x - y) ((fun (x : E × E) ↦ x.1 - x.2) '' s)

Tactic:
hs.is_linear_image IsLinearMap.isLinearMap_sub

Premises used: IsLinearMap.isLinearMap_sub, StarConvex.is_linear_image
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
c : 𝕜
⊢ StarConvex 𝕜 (c • x) (c • s)

Tactic:
hs.linear_image <| LinearMap.lsmul _ _ c

Premises used: LinearMap.lsmul, StarConvex.linear_image, DFunLike.coe
-- Module: Mathlib.Analysis.Convex.Star
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 : StarConvex 𝕜 0 s
c : 𝕜
⊢ StarConvex 𝕜 0 (c • s)

Tactic:
simpa using hs.smul c

Premises used: StarConvex.smul
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
c : 𝕜
hs : StarConvex 𝕜 (c • x) s
⊢ StarConvex 𝕜 x ((fun (z : E) ↦ c • z) ⁻¹' s)

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

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

Tactic:
have h := (hs.smul c).add_left z
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : CommSemiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
z : E
c : 𝕜
h : StarConvex 𝕜 (z + c • x) ((fun (x : E) ↦ z + x) '' (c • s))
rwa :
  ∀ (h : StarConvex 𝕜 (z + c • x) ((fun (x : E) ↦ z + x) '' (fun (x : E) ↦ c • x) '' s)),
    StarConvex 𝕜 (z + c • x) ((fun (x : E) ↦ z + c • x) '' s)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (h : StarConvex 𝕜 (z + c • x) ((fun (x : E) ↦ z + c • x) '' s)),
    StarConvex 𝕜 (z + c • x) ((fun (x : E) ↦ z + c • x) '' s)
⊢ StarConvex 𝕜 (z + c • x) ((fun (x : E) ↦ z + c • x) '' s)

Tactic:
rwa [← image_smul, image_image] at h

Premises used: Set.image_image, Set.image_smul
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommMonoid E
inst_4 : SMulWithZero 𝕜 E
s : Set E
⊢ StarConvex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s

Tactic:
forall_congr' fun x => forall_congr' fun _ => ⟨fun h a ha₀ ha₁ => ?_, fun h a b ha hb hab => ?_⟩

Premises used: Iff.intro, forall_congr', StarConvex
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommMonoid E
inst_4 : SMulWithZero 𝕜 E
s : Set E
refine_1 :
  ∀ x ∈ s,
    ∀ (h : ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → HSMul.hSMul (β := E) a 0 + b • x ∈ s) (a : 𝕜) (ha₀ : 0 ≤ a)
      (ha₁ : a ≤ 1), a • x ∈ s
refine_2 :
  ∀ x ∈ s,
    ∀ (h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s) (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
      HSMul.hSMul (β := E) a 0 + b • x ∈ s
⊢ StarConvex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s

Tactic:
refine
    forall_congr' fun x => forall_congr' fun _ => ⟨fun h a ha₀ ha₁ => ?_, fun h a b ha hb hab => ?_⟩

Premises used: Iff.intro, forall_congr'
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommMonoid E
inst_4 : SMulWithZero 𝕜 E
s : Set E
x : E
h_1 : x ∈ s
h : ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → HSMul.hSMul (β := E) a 0 + b • x ∈ s
a : 𝕜
ha₀ : 0 ≤ a
ha₁ : a ≤ 1
⊢ a • x ∈ s

Tactic:
simpa only [sub_add_cancel, eq_self_iff_true, forall_true_left, zero_add, smul_zero] using
      h (sub_nonneg_of_le ha₁) ha₀

Premises used: forall_true_left, sub_nonneg_of_le, smul_zero, zero_add, sub_add_cancel, eq_self_iff_true
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommMonoid E
inst_4 : SMulWithZero 𝕜 E
s : Set E
x : E
h_1 : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_2 : b • x ∈ s
⊢ HSMul.hSMul (β := E) a 0 + b • x ∈ s

Tactic:
rw [smul_zero, zero_add]

Premises used: smul_zero, zero_add
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommMonoid E
inst_4 : SMulWithZero 𝕜 E
s : Set E
x : E
h_1 : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
rw : b ≤ a + b
⊢ b ≤ 1

Tactic:
rw [← hab]
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommMonoid E
inst_4 : SMulWithZero 𝕜 E
s : Set E
x : E
h_1 : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b ≤ a + b

Tactic:
le_add_of_nonneg_left ha

Premises used: le_add_of_nonneg_left
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommMonoid E
inst_4 : SMulWithZero 𝕜 E
s : Set E
x : E
h_1 : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b ≤ a + b

Tactic:
exact le_add_of_nonneg_left ha

Premises used: le_add_of_nonneg_left
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommMonoid E
inst_4 : SMulWithZero 𝕜 E
s : Set E
x : E
h_1 : x ∈ s
h : ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ b • x ∈ s

Tactic:
exact h hb (by rw [← hab]; exact le_add_of_nonneg_left ha)
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
rw : x + t • y = (1 - t) • x + (t • x + t • y)
rw₁ : x + t • y = (1 - t) • x + t • x + t • y
rw₂ : x + t • y = (1 - t + t) • x + t • y
rw₃ : x + t • y = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + t • y
rw₄ rw₅ : x + t • y = x + t • y
⊢ x + t • y = (1 - t) • x + t • (x + y)

Tactic:
rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]

Premises used: add_assoc, one_smul, add_smul, sub_add_cancel, smul_add
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
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
    rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
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.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ s

Tactic:
hs hy (sub_nonneg_of_le ht₁) ht₀ (sub_add_cancel _ _)

Premises used: sub_nonneg_of_le, sub_add_cancel
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x y : E
s : Set E
hs : StarConvex 𝕜 x s
hy : x + y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
h : x + t • y = (1 - t) • x + t • (x + y)
⊢ (1 - t) • x + t • (x + y) ∈ s

Tactic:
exact hs hy (sub_nonneg_of_le ht₁) ht₀ (sub_add_cancel _ _)

Premises used: sub_nonneg_of_le, sub_add_cancel
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ 0 + x ∈ s

Tactic:
simpa using hx
-- Module: Mathlib.Analysis.Convex.Star
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddRightMono 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ t • x ∈ s

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

Premises used: StarConvex.add_smul_mem