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 : 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 : 𝕜
x : E
hx : Membership.mem (γ := Set E) {x : E | f x ≤ B} x
y : E
hy : Membership.mem (γ := Set E) {x : E | f x ≤ B} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ a • f x + b • f y ≤ a • B + b • B
have h₁ : f x ≤ B
Tactic: gcongr
-- 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 : 𝕜
x : E
hx : Membership.mem (γ := Set E) {x : E | f x ≤ B} x
y : E
hy : Membership.mem (γ := Set E) {x : E | f x ≤ B} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
h₁ : f x ≤ B
⊢ a • f x + b • f y ≤ a • B + b • B
have h₂ : f y ≤ B
Tactic: gcongr
-- 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 : 𝕜
x : E
hx : Membership.mem (γ := Set E) {x : E | f x ≤ B} x
y : E
hy : Membership.mem (γ := Set E) {x : E | f x ≤ B} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ a • B + b • B ≤ B
have rw : (a + b) • B ≤ B
Tactic: rw [← add_smul, hs, one_smul]
-- 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 : 𝕜
x : E
hx : Membership.mem (γ := Set E) {x : E | f x ≤ B} x
y : E
hy : Membership.mem (γ := Set E) {x : E | f x ≤ B} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
rw : (a + b) • B ≤ B
⊢ a • B + b • B ≤ B
have rw₁ : HSMul.hSMul (α := 𝕜) 1 B ≤ B
Tactic: rw [← add_smul, hs, one_smul]
-- 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 : 𝕜
x : E
hx : Membership.mem (γ := Set E) {x : E | f x ≤ B} x
y : E
hy : Membership.mem (γ := Set E) {x : E | f x ≤ B} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
rw : (a + b) • B ≤ B
rw₁ : HSMul.hSMul (α := 𝕜) 1 B ≤ B
⊢ a • B + b • B ≤ B
have rw₂ : B ≤ B
Tactic: rw [← add_smul, hs, one_smul]
-- 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 : 𝕜
x : E
hx : Membership.mem (γ := Set E) {x : E | f x ≤ B} x
y : E
hy : Membership.mem (γ := Set E) {x : E | f x ≤ B} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
⊢ Membership.mem (γ := Set E) {x : E | f x ≤ B} (a • x + b • y)
have _ : a • f x + b • f y ≤ a • B + b • B
Tactic: calc
    _ ≤ a • (f x) + b • (f y) := le_trans (hf1 _ _) (add_le_add (hf2 x ha) (hf2 y hb))
    _ ≤ a • B + b • B := by gcongr <;> assumption
    _ ≤ B := by rw [← add_smul, hs, one_smul]
-- 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 : 𝕜
x : E
hx : Membership.mem (γ := Set E) {x : E | f x ≤ B} x
y : E
hy : Membership.mem (γ := Set E) {x : E | f x ≤ B} y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hs : a + b = 1
_ : a • f x + b • f y ≤ a • B + b • B
⊢ Membership.mem (γ := Set E) {x : E | f x ≤ B} (a • x + b • y)
have _₁ : a • B + b • B ≤ B
Tactic: calc
    _ ≤ a • (f x) + b • (f y) := le_trans (hf1 _ _) (add_le_add (hf2 x ha) (hf2 y hb))
    _ ≤ a • B + b • B := by gcongr <;> assumption
    _ ≤ B := by rw [← add_smul, hs, one_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (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
s : Set E
h : Convex 𝕜 s
x : E
zero_mem : 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']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (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
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ∃ z ∈ s, (p + q) • z = p • x + q • y
have inl : ∀ (hp hq : LE.le.{u_1} (α := 𝕜) 0 0),
  ∃ z ∈ s,
    HAdd.hAdd (α := 𝕜) 0 0 • z = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
Tactic: rcases _root_.em (p = 0 ∧ q = 0) with (⟨rfl, rfl⟩ | hpq)
Cleared hypotheses: p, q, hp, hq
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (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
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
inl :
  ∀ (hp hq : LE.le.{u_1} (α := 𝕜) 0 0),
    ∃ z ∈ s,
      HAdd.hAdd (α := 𝕜) 0 0 • z = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
⊢ ∃ z ∈ s, (p + q) • z = p • x + q • y
have inr : ∀ (hpq : ¬(p = 0 ∧ q = 0)), ∃ z ∈ s, (p + q) • z = p • x + q • y
Tactic: rcases _root_.em (p = 0 ∧ q = 0) with (⟨rfl, rfl⟩ | hpq)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (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
s : Set E
h : Convex 𝕜 s
x y : E
hx : x ∈ s
hy : y ∈ s
hp hq : LE.le.{u_1} (α := 𝕜) 0 0
⊢ ∃ z ∈ s,
    HAdd.hAdd (α := 𝕜) 0 0 • z = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
have right : HAdd.hAdd (α := 𝕜) 0 0 • x = HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 x + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 0 y
Tactic: use x, hx
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (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
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : ¬(p = 0 ∧ q = 0)
⊢ ∃ z ∈ s, (p + q) • z = p • x + q • y
have hpq₁ : 0 < p + q
Tactic: replace hpq : 0 < p + q :=
      (add_nonneg hp hq).lt_of_ne' (mt (add_eq_zero_iff_of_nonneg hp hq).1 hpq)
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (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
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
⊢ ∃ z ∈ s, (p + q) • z = p • x + q • y
have inr : (p + q) • ((p / (p + q)) • x + (q / (p + q)) • y) = p • x + q • y
Tactic: refine ⟨_, convex_iff_div.1 h hx hy hp hq hpq, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (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
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
⊢ (p + q) • ((p / (p + q)) • x + (q / (p + q)) • y) = p • x + q • y
have match_scalars : (p + q) * (p / (p + q) * 1) = p * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (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
s : Set E
h : Convex 𝕜 s
x y : E
p q : 𝕜
hx : x ∈ s
hy : y ∈ s
hp : 0 ≤ p
hq : 0 ≤ q
hpq : 0 < p + q
match_scalars : (p + q) * (p / (p + q) * 1) = p * 1
⊢ (p + q) • ((p / (p + q)) • x + (q / (p + q)) • y) = p • x + q • y
have match_scalars₁ : (p + q) * (q / (p + q) * 1) = q * 1
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (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
s : Set E
h_conv : Convex 𝕜 s
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ s + HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 2⁻¹ s = s
have rw : HAdd.hAdd (α := 𝕜) 2⁻¹ 2⁻¹ • s = s
Tactic: rw [← h_conv.add_smul (by norm_num) (by norm_num)]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (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
s : Set E
h_conv : Convex 𝕜 s
⊢ HAdd.hAdd (α := 𝕜) 2⁻¹ 2⁻¹ • s = s
have ring_nf : HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 s = s
Tactic: ring_nf
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (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
s : Set E
h_conv : Convex 𝕜 s
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) 1 s = s
have rw : s = s
Tactic: rw [one_smul]
-- 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 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun (x1 x2 : E) ↦ x1 ≤ x2) s
⊢ Convex 𝕜 s
have refine : ∀ (x : E) (hx : x ∈ s) (y : E) (hy : y ∈ s), [x -[𝕜] y] ⊆ s
Tactic: refine convex_iff_segment_subset.mpr fun x hx y hy => ?_
-- 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 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun (x1 x2 : E) ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
⊢ [x -[𝕜] y] ⊆ s
have inl : ∀ (hxy : x ≤ y), [x -[𝕜] y] ⊆ s
Tactic: obtain hxy | hyx := h.total hx hy
-- 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 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun (x1 x2 : E) ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
inl : ∀ (hxy : x ≤ y), [x -[𝕜] y] ⊆ s
⊢ [x -[𝕜] y] ⊆ s
have inr : ∀ (hyx : y ≤ x), [x -[𝕜] y] ⊆ s
Tactic: obtain hxy | hyx := h.total hx hy
-- 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 : PartialOrder E
inst_4 : IsOrderedAddMonoid E
inst_5 : Module 𝕜 E
inst_6 : PosSMulMono 𝕜 E
s : Set E
hs : s.OrdConnected
h : IsChain (fun (x1 x2 : E) ↦ x1 ≤ x2) s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hyx : y ≤ x
⊢ [x -[𝕜] y] ⊆ s
have inr : [y -[𝕜] x] ⊆ s
Tactic: rw [segment_symm]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
⊢ Convex 𝕜 s ↔ s.OrdConnected
have simp_rw : (∀ ⦃x : 𝕜⦄, x ∈ s → ∀ ⦃y : 𝕜⦄, y ∈ s → [x -[𝕜] y] ⊆ s) ↔ s.OrdConnected
Tactic: simp_rw [convex_iff_segment_subset, segment_eq_uIcc, ordConnected_iff_uIcc_subset]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s : Set 𝕜
simp_rw : (∀ ⦃x : 𝕜⦄, x ∈ s → ∀ ⦃y : 𝕜⦄, y ∈ s → [x -[𝕜] y] ⊆ s) ↔ s.OrdConnected
⊢ Convex 𝕜 s ↔ s.OrdConnected
have simp_rw₁ : (∀ ⦃x : 𝕜⦄, x ∈ s → ∀ ⦃y : 𝕜⦄, y ∈ s → uIcc x y ⊆ s) ↔ s.OrdConnected
Tactic: simp_rw [convex_iff_segment_subset, segment_eq_uIcc, ordConnected_iff_uIcc_subset]
-- 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
K : Submodule 𝕜 E
⊢ Convex 𝕜 (↑K : Set E)
have repeat' : ∀ ⦃x : E⦄,
  x ∈ (↑K : Set E) → ∀ ⦃y : E⦄, y ∈ (↑K : Set E) → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ (↑K : Set E)
Tactic: repeat' intro
-- 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
K : Submodule 𝕜 E
x : E
h : x ∈ (↑K : Set E)
y : E
h_1 : y ∈ (↑K : Set E)
a b : 𝕜
h_2 : 0 ≤ a
h_3 : 0 ≤ b
h_4 : a + b = 1
⊢ a • x + b • y ∈ (↑K : Set E)
have refine_1 : x ∈ K
Tactic: refine add_mem (smul_mem _ _ ?_) (smul_mem _ _ ?_)
-- 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
K : Submodule 𝕜 E
x : E
h : x ∈ (↑K : Set E)
y : E
h_1 : y ∈ (↑K : Set E)
a b : 𝕜
h_2 : 0 ≤ a
h_3 : 0 ≤ b
h_4 : a + b = 1
refine_1 : x ∈ K
⊢ a • x + b • y ∈ (↑K : Set E)
have refine_2 : y ∈ K
Tactic: refine add_mem (smul_mem _ _ ?_) (smul_mem _ _ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • u + b • v ∈ s
have obtain : ∀ (c : R) (hc1 : Membership.mem (γ := Set R) (Ici 0) c) (hc2 : (algebraMap R A : (a : R) → A) c = a), a • u + b • v ∈ s
Tactic: obtain ⟨c, hc1, hc2⟩ := halg ha
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
⊢ a • u + b • v ∈ s
have obtain : ∀ (d : R) (hd1 : Membership.mem (γ := Set R) (Ici 0) d) (hd2 : (algebraMap R A : (a : R) → A) d = b), a • u + b • v ∈ s
Tactic: obtain ⟨d, hd1, hd2⟩ := halg hb
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
⊢ a • u + b • v ∈ s
have h : a • u = c • u
Tactic: convert! hs hu hv hc1 hd1 _ using 2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
h : a • u = c • u
⊢ a • u + b • v ∈ s
have h₁ : b • v = d • v
Tactic: convert! hs hu hv hc1 hd1 _ using 2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
h : a • u = c • u
h₁ : b • v = d • v
⊢ a • u + b • v ∈ s
have convert! : c + d = 1
Tactic: convert! hs hu hv hc1 hd1 _ using 2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
⊢ a • u = c • u
have h : HSMul.hSMul.{u_6, u_7, u_7} (α := A) ((algebraMap R A : (a : R) → A) c : A) u = c • u
Tactic: rw [← hc2, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
h : HSMul.hSMul.{u_6, u_7, u_7} (α := A) ((algebraMap R A : (a : R) → A) c : A) u = c • u
⊢ a • u = c • u
have h₁ : c • u = c • u
Tactic: rw [← hc2, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
⊢ b • v = d • v
have h : HSMul.hSMul.{u_6, u_7, u_7} (α := A) ((algebraMap R A : (a : R) → A) d : A) v = d • v
Tactic: rw [← hd2, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
h : HSMul.hSMul.{u_6, u_7, u_7} (α := A) ((algebraMap R A : (a : R) → A) d : A) v = d • v
⊢ b • v = d • v
have h₁ : d • v = d • v
Tactic: rw [← hd2, algebraMap_smul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (goal)
Goal:
R : Type u_5
inst : CommSemiring R
A : Type u_6
inst_1 : Semiring A
inst_2 : Algebra R A
M : Type u_7
inst_3 : AddCommMonoid M
inst_4 : Module A M
inst_5 : Module R M
inst_6 : IsScalarTower R A M
inst_7 : PartialOrder R
inst_8 : PartialOrder A
inst_9 : FaithfulSMul R A
s : Set M
halg : Subset.{u_6} (α := Set A) (Ici 0) (image.{u_5, u_6} (α := R) (⇑(algebraMap R A) : (a : R) → A) (Ici 0))
hs : ∀ ⦃x : M⦄, x ∈ s → ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : R⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
u : M
hu : u ∈ s
v : M
hv : v ∈ s
a b : A
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
c : R
hc1 : Membership.mem (γ := Set R) (Ici 0) c
hc2 : (algebraMap R A : (a : R) → A) c = a
d : R
hd1 : Membership.mem (γ := Set R) (Ici 0) d
hd2 : (algebraMap R A : (a : R) → A) d = b
⊢ c + d = 1
have rw : ∀ (hc1 : Membership.mem (γ := Set R) (Ici 0) c) (hc2 : (algebraMap R A : (a : R) → A) c = a) (d : R)
  (hab : Eq.{u_6 + 1} (α := A) (↑(c + d) : A) 1) (hd1 : Membership.mem (γ := Set R) (Ici 0) d)
  (hd2 : (algebraMap R A : (a : R) → A) d = b), c + d = 1
Tactic: rw [← hc2, ← hd2, ← algebraMap.coe_add] at hab
Cleared hypotheses: hab, hc1, hc2, d, hd1, hd2
-- Lean 4 proof step from Mathlib.Analysis.Convex.Between (goal)
Goal:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst : Ring R
inst_1 : PartialOrder R
inst_2 : AddCommGroup V
inst_3 : Module R V
inst_4 : AddTorsor V P
inst_5 : AddCommGroup V'
inst_6 : Module R V'
inst_7 : AddTorsor V' P'
f : P →ᵃ[R] P'
x y : P
⊢ Eq.{u_5 + 1} (α := Set P') ((⇑f : (a : P) → P') '' affineSegment R x y : Set P')
    (affineSegment R ((f : (a : P) → P') x) ((f : (a : P) → P') y) : Set P')
have rw : Eq.{u_5 + 1} (α := Set P') ((fun (x_1 : R) ↦ (f : (a : P) → P') ((lineMap x y : (a : R) → P) x_1 : P)) '' Set.Icc 0 1)
  (Set.image.{u_1, u_5} (α := R) (⇑(f.comp (lineMap x y)) : (a : R) → P') (Set.Icc 0 1))
Tactic: rw [affineSegment, affineSegment, Set.image_image, ← comp_lineMap]