awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha_1 : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha : 0 < a
inr : ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 0) (hab : a + 0 = 1), a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
⊢ a • x + b • y ∈ s
have inr₁ : ∀ (hb : 0 < b), a • x + b • y ∈ s
Tactic: obtain rfl | hb := hb.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (hypothesis)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha_1 : 0 ≤ a
ha : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
have hab₁ : a = 1
Tactic: rw [add_zero] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha_1 : 0 ≤ a
ha : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
have inr : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
Tactic: rwa [hab, one_smul, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha_1 : 0 ≤ a
ha : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
inr : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
have inr₁ : x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
Tactic: rwa [hab, one_smul, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha_1 : 0 ≤ a
ha : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
inr : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
inr₁ : x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
have inr₂ : x + 0 ∈ s
Tactic: rwa [hab, one_smul, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
⊢ StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
have refine : (∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) → StarConvex 𝕜 x s
Tactic: refine ⟨fun h y hy _ a b ha hb hab => h hy ha.le hb.le hab, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s
have inl : ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
Tactic: obtain rfl | ha' := ha.eq_or_lt
Cleared hypotheses: a, ha, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
inl : ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1), HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
⊢ a • x + b • y ∈ s
have inr : ∀ (ha' : 0 < a), a • x + b • y ∈ s
Tactic: obtain rfl | ha' := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (hypothesis)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : 0 + b = 1
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
have hab₁ : b = 1
Tactic: rw [zero_add] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
have inl : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y ∈ s
Tactic: rwa [hab, zero_smul, one_smul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
inl : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y ∈ s
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
have inl₁ : 0 + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y ∈ s
Tactic: rwa [hab, zero_smul, one_smul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
inl : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y ∈ s
inl₁ : 0 + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 y ∈ s
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + b • y ∈ s
have inl₂ : 0 + y ∈ s
Tactic: rwa [hab, zero_smul, one_smul, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ s
have inr : ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 0) (hab : a + 0 = 1), a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
Tactic: obtain rfl | hb' := hb.eq_or_lt
Cleared hypotheses: b, hb, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
inr : ∀ (hb : LE.le.{u_1} (α := 𝕜) 0 0) (hab : a + 0 = 1), a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
⊢ a • x + b • y ∈ s
have inr₁ : ∀ (hb' : 0 < b), a • x + b • y ∈ s
Tactic: obtain rfl | hb' := hb.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (hypothesis)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha : 0 ≤ a
ha' : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a + 0 = 1
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
have hab₁ : a = 1
Tactic: rw [add_zero] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha : 0 ≤ a
ha' : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
have inr : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
Tactic: rwa [hab, zero_smul, one_smul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha : 0 ≤ a
ha' : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
inr : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
have inr₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + 0 ∈ s
Tactic: rwa [hab, zero_smul, one_smul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a : 𝕜
ha : 0 ≤ a
ha' : 0 < a
hb : LE.le.{u_1} (α := 𝕜) 0 0
hab : a = 1
inr : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
inr₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + 0 ∈ s
⊢ a • x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y ∈ s
have inr₂ : x + 0 ∈ s
Tactic: rwa [hab, zero_smul, one_smul, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
hb' : 0 < b
⊢ a • x + b • y ∈ s
have inr : ∀ (hy : x ∈ s), a • x + b • x ∈ s
Tactic: obtain rfl | hxy := eq_or_ne x y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
hx : x ∈ s
h : ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
hb' : 0 < b
inr : ∀ (hy : x ∈ s), a • x + b • x ∈ s
⊢ a • x + b • y ∈ s
have inr₁ : ∀ (hxy : x ≠ y), a • x + b • y ∈ s
Tactic: obtain rfl | hxy := eq_or_ne x y
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ (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)
have 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)
Tactic: rw [f.map_add, f.map_smul, f.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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)
⊢ (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)
have 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)
Tactic: rw [f.map_add, f.map_smul, f.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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)
⊢ (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)
have 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)
Tactic: rw [f.map_add, f.map_smul, f.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) (a • x + b • y)
have rw : HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + HSMul.hSMul (β := F) b ((f : (a : E) → F) y : F) ∈ s
Tactic: rw [mem_preimage, f.map_add, f.map_smul, f.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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) (s + t)
have rw : StarConvex 𝕜 (x + y) ((fun (x : E × E) ↦ x.1 + x.2) '' s ×ˢ t)
Tactic: rw [← add_image_prod]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) '' s) (a • (z + x) + b • y)
have 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'))
Tactic: obtain ⟨y', hy', rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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'))
have refine : (fun (x : E) ↦ z + x) (a • x + b • y') = a • (z + x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y')
Tactic: refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ (fun (x : E) ↦ z + x) (a • x + b • y') = a • (z + x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y')
have match_scalars : 1 = a * 1 + b * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ (fun (x : E) ↦ z + x) (a • x + b • y') = a • (z + x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y')
have match_scalars₁ : a * 1 = a * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ (fun (x : E) ↦ z + x) (a • x + b • y') = a • (z + x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y')
have match_scalars₂ : b * 1 = b * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ x + z) '' s) (a • (x + z) + b • y)
have 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'))
Tactic: obtain ⟨y', hy', rfl⟩ := hy
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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'))
have refine : (fun (x : E) ↦ x + z) (a • x + b • y') = a • (x + z) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ x + z) y')
Tactic: refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ (fun (x : E) ↦ x + z) (a • x + b • y') = a • (x + z) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ x + z) y')
have match_scalars : a * 1 = a * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ (fun (x : E) ↦ x + z) (a • x + b • y') = a • (x + z) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ x + z) y')
have match_scalars₁ : b * 1 = b * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ (fun (x : E) ↦ x + z) (a • x + b • y') = a • (x + z) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ x + z) y')
have match_scalars₂ : 1 = a * 1 + b * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (hypothesis)
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
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
have h : a • (z + x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ s
Tactic: have h := hs hy ha hb hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
have 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)
Tactic: rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
have 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)
Tactic: rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
have 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)
Tactic: rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h
Cleared hypotheses: h