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 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)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
have rwa₃ : ∀ (h : (a + 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
-- 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)
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)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
have 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)
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)
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)
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
have rwa₅ : ∀ (h : 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
-- 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 𝕜 (x + z) s
⊢ StarConvex 𝕜 x ((fun (x : E) ↦ x + z) ⁻¹' s)
have hs₁ : StarConvex 𝕜 (z + x) s
Tactic: rw [add_comm] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (hypothesis)
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 + c • x) '' s)
have h : StarConvex 𝕜 (z + c • x) ((fun (x : E) ↦ z + x) '' (c • s))
Tactic: have h := (hs.smul c).add_left z
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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))
⊢ StarConvex 𝕜 (z + c • x) ((fun (x : E) ↦ z + c • x) '' s)
have 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)
Tactic: rwa [← image_smul, image_image] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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)
⊢ StarConvex 𝕜 (z + c • x) ((fun (x : E) ↦ z + c • x) '' s)
have rwa₁ : ∀ (h : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
have 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
Tactic: refine
    forall_congr' fun x => forall_congr' fun _ => ⟨fun h a ha₀ ha₁ => ?_, fun h a b ha hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ StarConvex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s
have 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
Tactic: refine
    forall_congr' fun x => forall_congr' fun _ => ⟨fun h a ha₀ ha₁ => ?_, fun h a b ha hb hab => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ HSMul.hSMul (β := E) a 0 + b • x ∈ s
have refine_2 : b • x ∈ s
Tactic: rw [smul_zero, zero_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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 ≤ 1
have rw : b ≤ a + b
Tactic: rw [← hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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)
have rw : x + t • y = (1 - t) • x + (t • x + t • y)
Tactic: rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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)
⊢ x + t • y = (1 - t) • x + t • (x + y)
have rw₁ : x + t • y = (1 - t) • x + t • x + t • y
Tactic: rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ x + t • y = (1 - t) • x + t • (x + y)
have rw₂ : x + t • y = (1 - t + t) • x + t • y
Tactic: rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ x + t • y = (1 - t) • x + t • (x + y)
have rw₃ : x + t • y = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x + t • y
Tactic: rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
⊢ x + t • y = (1 - t) • x + t • (x + y)
have rw₄ : x + t • y = x + t • y
Tactic: rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (hypothesis)
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 ∈ s
have h : 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]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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)
⊢ x + t • y ∈ s
have rw : (1 - t) • x + t • (x + y) ∈ s
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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 : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • (y - x) ∈ s
have a : x + t • (y - x) ∈ [x -[𝕜] y]
Tactic: apply hs.segment_subset hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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 : y ∈ s
t : 𝕜
ht₀ : 0 ≤ t
ht₁ : t ≤ 1
⊢ x + t • (y - x) ∈ [x -[𝕜] y]
have a : Membership.mem (γ := Set E) ((fun (θ : 𝕜) ↦ x + θ • (y - x)) '' Icc 0 1) (x + t • (y - x))
Tactic: rw [segment_eq_image']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
x : E
f : E →ᵃ[𝕜] F
s : Set 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, Convex.combo_affine_apply hab]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
y : F
y' : E
hy' : y' ∈ s
hy'f : (f : (a : E) → F) y' = y
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) + b • y)
have refine : (f : (a : E) → F) (a • x + b • y') = HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + b • 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
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
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
y : F
y' : E
hy' : y' ∈ s
hy'f : (f : (a : E) → F) y' = y
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) + b • y
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) + b • y
Tactic: rw [Convex.combo_affine_apply hab, hy'f]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
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
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
y : F
y' : E
hy' : y' ∈ s
hy'f : (f : (a : E) → F) y' = 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) =
    HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + b • y
⊢ (f : (a : E) → F) (a • x + b • y') = HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + b • y
have rw₁ : HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + b • y = HSMul.hSMul (β := F) a ((f : (a : E) → F) x : F) + b • y
Tactic: rw [Convex.combo_affine_apply hab, hy'f]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 x s
⊢ StarConvex 𝕜 (-x) (-s)
have rw : StarConvex 𝕜 (-x) ((fun (x : E) ↦ -x) '' s)
Tactic: rw [← image_neg_eq_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup 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 simp_rw : StarConvex 𝕜 (x + -y) (s + -t)
Tactic: simp_rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
⊢ StarConvex 𝕜 y (Iic x)ᶜ
have refine : ∀ (z : E) (hz : z ∈ (Iic x)ᶜ) (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), a • y + b • z ∈ (Iic x)ᶜ
Tactic: refine (starConvex_iff_forall_pos <| by simp [h.not_ge]).mpr fun z hz a b ha hb hab ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
hz : z ∈ (Iic x)ᶜ
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • y + b • z ∈ (Iic x)ᶜ
have rw : ∀ (hz : ¬z ≤ x) (a b : 𝕜) (ha : 0 < a) (hb : 0 < b) (hab : a + b = 1), ¬a • y + b • z ≤ x
Tactic: rw [mem_compl_iff, mem_Iic] at hz ⊢
Cleared hypotheses: hz, a, b, ha, hb, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
hz : ¬z ≤ x
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ ¬a • y + b • z ≤ x
have contrapose : ∀ (hz : a • y + b • z ≤ x), z ≤ x
Tactic: contrapose hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ z ≤ x
have refine : b • z < b • x
Tactic: refine (lt_of_smul_lt_smul_of_nonneg_left ?_ hb.le).le
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ b • z ≤ (a + b) • x - a • y
have rwa : a • y + b • z ≤ (a + b) • x
Tactic: rwa [le_sub_iff_add_le', hab, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
rwa : a • y + b • z ≤ (a + b) • x
⊢ b • z ≤ (a + b) • x - a • y
have rwa₁ : a • y + b • z ≤ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 x
Tactic: rwa [le_sub_iff_add_le', hab, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ (a + b) • x - a • y < b • x
have rw : a • x + b • x < a • y + b • x
Tactic: rw [add_smul, sub_lt_iff_lt_add']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
⊢ b • z < b • x
have b₁ : b • z ≤ (a + b) • x - a • y
Tactic: calc
    b • z ≤ (a + b) • x - a • y := by rwa [le_sub_iff_add_le', hab, one_smul]
    _ < b • x := by
      rw [add_smul, sub_lt_iff_lt_add']
      gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Ring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommGroup E
inst_3 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : IsStrictOrderedModule 𝕜 E
inst_7 : PosSMulReflectLT 𝕜 E
x y : E
h : x < y
z : E
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hz : a • y + b • z ≤ x
b₁ : b • z ≤ (a + b) • x - a • y
⊢ b • z < b • x
have b₂ : (a + b) • x - a • y < b • x
Tactic: calc
    b • z ≤ (a + b) • x - a • y := by rwa [le_sub_iff_add_le', hab, one_smul]
    _ < b • x := by
      rw [add_smul, sub_lt_iff_lt_add']
      gcongr
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ (a / (a + b)) • x + (b / (a + b)) • y ∈ s
have a₁ : 0 ≤ a / (a + b)
Tactic: apply h hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
a₁ : 0 ≤ a / (a + b)
⊢ (a / (a + b)) • x + (b / (a + b)) • y ∈ s
have a₂ : 0 ≤ b / (a + b)
Tactic: apply h hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
a₁ : 0 ≤ a / (a + b)
a₂ : 0 ≤ b / (a + b)
⊢ (a / (a + b)) • x + (b / (a + b)) • y ∈ s
have a₃ : a / (a + b) + b / (a + b) = 1
Tactic: apply h hy
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : StarConvex 𝕜 x s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : 0 < a + b
⊢ a / (a + b) + b / (a + b) = 1
have a₁ : (a + b) / (a + b) = 1
Tactic: rw [← add_div]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + 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 h' : 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
Tactic: have h' := h hy ha hb
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
h : ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
h' : 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s
⊢ a • x + b • y ∈ s
have h'₁ : LT.lt.{u_1} (α := 𝕜) 0 1 → a • x + b • y ∈ s
Tactic: rw [hab, div_one, div_one] at h'
Cleared hypotheses: h'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Star (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : AddCommGroup E
inst_4 : Module 𝕜 E
x : E
s : Set E
hs : StarConvex 𝕜 0 s
hx : x ∈ s
t : 𝕜
ht : 1 ≤ t
⊢ x ∈ t • s
have rw : t⁻¹ • x ∈ s
Tactic: rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']