awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) x
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 : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) 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.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) x
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 : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) x
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 : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) 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.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) x
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 : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) 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.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
s : Set E
hs : Convex 𝕜 s
z x : E
hx : Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) x
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 : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) 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.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : AddCommMonoid β
inst_5 : PartialOrder β
inst_6 : IsOrderedAddMonoid β
inst_7 : Module 𝕜 β
inst_8 : PosSMulMono 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {w : E | f w = r}
have simp_rw : Convex.{u_1, u_2} 𝕜 (E := E) {w : E | f w ≤ r ∧ r ≤ f w}
Tactic: simp_rw [le_antisymm_iff]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ Iio r
have inl : ∀ (ha : LE.le.{u_1} (α := 𝕜) 0 0) (hab : 0 + b = 1), HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 0 x + b • y ∈ Iio r
Tactic: obtain rfl | ha' := ha.eq_or_lt
Cleared hypotheses: a, ha, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
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_4, u_4} (α := 𝕜) 0 x + b • y ∈ Iio r
⊢ a • x + b • y ∈ Iio r
have inr : ∀ (ha' : 0 < a), a • x + b • y ∈ Iio r
Tactic: obtain rfl | ha' := ha.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (hypothesis)
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : 0 + b = 1
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 0 x + b • y ∈ Iio r
have hab₁ : b = 1
Tactic: rw [zero_add] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 0 x + b • y ∈ Iio r
have inl : 0 + b • y ∈ Iio r
Tactic: rwa [zero_smul, zero_add, hab, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
inl : 0 + b • y ∈ Iio r
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 0 x + b • y ∈ Iio r
have inl₁ : b • y ∈ Iio r
Tactic: rwa [zero_smul, zero_add, hab, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
b : 𝕜
hb : 0 ≤ b
ha : LE.le.{u_1} (α := 𝕜) 0 0
hab : b = 1
inl : 0 + b • y ∈ Iio r
inl₁ : b • y ∈ Iio r
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 0 x + b • y ∈ Iio r
have inl₂ : HSMul.hSMul.{u_1, u_4, u_4} (α := 𝕜) 1 y ∈ Iio r
Tactic: rwa [zero_smul, zero_add, hab, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
β : Type u_4
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : IsOrderedCancelAddMonoid β
inst_5 : Module 𝕜 β
inst_6 : PosSMulStrictMono 𝕜 β
r x : β
hx : x ∈ Iio r
y : β
hy : y ∈ Iio r
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
ha' : 0 < a
⊢ a • x + b • y ∈ Iio r
have inr : ∀ (hx : x < r) ⦃y : β⦄ (hy : y < r) ⦃a b : 𝕜⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (ha' : 0 < a),
  a • x + b • y ∈ Iio r
Tactic: rw [mem_Iio] at hx hy
Cleared hypotheses: hx, y, hy, a, b, ha, hb, hab, ha'
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_5
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • x + b • y ∈ s
have suffices : HSMul.hSMul (β := 𝕜) a 1 • x + HSMul.hSMul (β := 𝕜) b 1 • y ∈ s
Tactic: suffices (a • (1 : 𝕜)) • x + (b • (1 : 𝕜)) • y ∈ s by simpa using this
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_5
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ HSMul.hSMul (β := 𝕜) a 1 • x + HSMul.hSMul (β := 𝕜) b 1 • y ∈ s
have refine_1 : 0 ≤ HSMul.hSMul (β := 𝕜) a 1
Tactic: refine hs hx hy ?_ ?_ (by simpa [add_smul] using congr($(hab) • (1 : 𝕜)))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : ZeroLEOneClass 𝕜
inst_4 : Module 𝕜 E
R : Type u_5
inst_5 : Semiring R
inst_6 : PartialOrder R
inst_7 : Module R E
inst_8 : Module R 𝕜
inst_9 : IsScalarTower R 𝕜 E
inst_10 : SMulPosMono R 𝕜
s : Set E
hs : Convex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
refine_1 : 0 ≤ HSMul.hSMul (β := 𝕜) a 1
⊢ HSMul.hSMul (β := 𝕜) a 1 • x + HSMul.hSMul (β := 𝕜) b 1 • y ∈ s
have refine_2 : 0 ≤ HSMul.hSMul (β := 𝕜) b 1
Tactic: refine hs hx hy ?_ ?_ (by simpa [add_smul] using congr($(hab) • (1 : 𝕜)))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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
⊢ Convex 𝕜 (openSegment 𝕜 a b)
have rw : ∀ ⦃x : E⦄, x ∈ openSegment 𝕜 a b → ∀ ⦃y : E⦄, y ∈ openSegment 𝕜 a b → openSegment 𝕜 x y ⊆ openSegment 𝕜 a b
Tactic: rw [convex_iff_openSegment_subset]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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 • a_1 + bp • b_1) + b • (aq • a_1 + bq • b_1) ∈ openSegment 𝕜 a_1 b_1
have refine_1 : a * ap + b * aq + (a * bp + b * bq) = 1
Tactic: refine ⟨a * ap + b * aq, a * bp + b * bq, by positivity, by positivity, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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
⊢ a • (ap • a_1 + bp • b_1) + b • (aq • a_1 + bq • b_1) ∈ openSegment 𝕜 a_1 b_1
have 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)
Tactic: refine ⟨a * ap + b * aq, a * bp + b * bq, by positivity, by positivity, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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 * bp + b * bq) + (a * 1 + b * 1 + 1) = 1 + (a * (ap + bp) + b * (aq + bq) + (a + b))
have a₁ : a * ap + b * aq + (a * bp + b * bq) + (a + b + 1) = 1 + (a * ap + a * bp + (b * aq + b * bq) + (a + b))
Tactic: noncomm_ring
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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 * bp + b * bq) = 1
have a₁ : a * ap + b * aq + (a * bp + b * bq) + (a * 1 + b * 1 + 1) = 1 + (a * (ap + bp) + b * (aq + bq) + (a + b))
Tactic: linear_combination (norm := noncomm_ring) a * habp + b * habq + hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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)
have rw : Convex 𝕜 (s + -t)
Tactic: rw [sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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)
have match_scalars : 1 = (1 - t) * 1 + t * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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
⊢ x + t • y = (1 - t) • x + t • (x + y)
have match_scalars₁ : t * 1 = t * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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
⊢ 1 = (1 - t) * 1 + t * 1
have noncomm_ring : 1 = 1 + -t + t
Tactic: noncomm_ring
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (hypothesis)
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 ∈ 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 match_scalars <;> noncomm_ring
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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)
⊢ x + t • y ∈ s
have rw : (1 - t) • x + t • (x + y) ∈ s
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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
⊢ x + t • (y - x) ∈ s
have rw : t • (y - x) + x ∈ s
Tactic: rw [add_comm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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
⊢ 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'))
have 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'))
Tactic: obtain ⟨r, rfl⟩ : ∃ r : 𝕜, σ r = a := RingHomSurjective.is_surjective ..
Cleared hypotheses: a, ha, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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
⊢ 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'))
have 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'))
Tactic: obtain ⟨t, rfl⟩ : ∃ t : 𝕜, σ t = b := RingHomSurjective.is_surjective ..
Cleared hypotheses: b, hb, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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
⊢ 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'))
have refine : r + t = 1
Tactic: refine ⟨r • x + t • y, hs hx hy (by simp_all [(@hσ 0 r).mp]) (by simp_all [(@hσ 0 t).mp])
    ?_, by simp⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
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
⊢ r + t = 1
have apply_fun : Eq.{u_5 + 1} (α := 𝕜') ((σ : (a : 𝕜) → 𝕜') (r + t) : 𝕜') ((σ : (a : 𝕜) → 𝕜') 1 : 𝕜')
Tactic: apply_fun σ using Function.Injective.of_eq_imp_le (hσ.mp ·.le)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : AddCommMonoid E
inst_2 : LinearOrder 𝕜
inst_3 : IsOrderedRing 𝕜
inst_4 : SMul 𝕜 E
f : E → 𝕜
hf1 : ∀ (x y : E), f (x + y) ≤ f x + f y
hf2 : ∀ ⦃c : 𝕜⦄ (x : E), 0 ≤ c → f (c • x) ≤ c * f x
B : 𝕜
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | f x ≤ B}
have rw : ∀ ⦃x : E⦄,
  Membership.mem (γ := Set E) {x : E | f x ≤ B} x →
    ∀ ⦃y : E⦄, Membership.mem (γ := Set E) {x : E | f x ≤ B} y → [x -[𝕜] y] ⊆ {x : E | f x ≤ B}
Tactic: rw [convex_iff_segment_subset]