awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
⊢ ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) ≤ φ) ∧
      ⨆ (i : ℕ),
          Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) =
        φ
have obtain : ∀ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ)
  (hle :
    ∀ (i : ℕ),
      HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
          (Set.restrict (π := fun (a : E) ↦ ℝ) univ
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
          (const (↑univ : Type u_2) (c i)) ≤
        Set.restrict (π := fun (a : E) ↦ ℝ) univ φ)
  (hsup :
    Eq (α := (a : (↑univ : Type u_2)) → ℝ)
      (⨆ (i : ℕ),
        HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
          (Set.restrict (π := fun (a : E) ↦ ℝ) univ
            (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
          (const (↑univ : Type u_2) (c i)))
      (Set.restrict (π := fun (a : E) ↦ ℝ) univ φ)),
  ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) ≤ φ) ∧
      ⨆ (i : ℕ),
          Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) =
        φ
Tactic: obtain ⟨l, c, hle, hsup⟩ := hφcv.sSup_of_nat_affine_eq (𝕜 := 𝕜) (s := univ) isClosed_univ
    (lowerSemicontinuousOn_univ_iff.2 hφc)
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
l : ℕ → E →L[𝕜] 𝕜
c : ℕ → ℝ
hle :
  ∀ (i : ℕ),
    HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
        (Set.restrict (π := fun (a : E) ↦ ℝ) univ
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
        (const (↑univ : Type u_2) (c i)) ≤
      Set.restrict (π := fun (a : E) ↦ ℝ) univ φ
hsup :
  Eq (α := (a : (↑univ : Type u_2)) → ℝ)
    (⨆ (i : ℕ),
      HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
        (Set.restrict (π := fun (a : E) ↦ ℝ) univ
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
        (const (↑univ : Type u_2) (c i)))
    (Set.restrict (π := fun (a : E) ↦ ℝ) univ φ)
⊢ ∃ (l : ℕ → E →L[𝕜] 𝕜) (c : ℕ → ℝ),
    (∀ (i : ℕ),
        Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) ≤ φ) ∧
      ⨆ (i : ℕ),
          Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) =
        φ
have refine : ⨆ (i : ℕ), Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) = φ
Tactic: refine ⟨l, c, fun i x ↦ hle i ⟨x, trivial⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Approximation (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
φ : E → ℝ
inst : RCLike 𝕜
inst_1 : TopologicalSpace E
inst_2 : AddCommGroup E
inst_3 : Module ℝ E
inst_4 : Module 𝕜 E
inst_5 : IsScalarTower ℝ 𝕜 E
inst_6 : IsTopologicalAddGroup E
inst_7 : ContinuousSMul 𝕜 E
inst_8 : LocallyConvexSpace ℝ E
inst_9 : HereditarilyLindelofSpace E
hφc : LowerSemicontinuous φ
hφcv : ConvexOn ℝ univ φ
l : ℕ → E →L[𝕜] 𝕜
c : ℕ → ℝ
hle :
  ∀ (i : ℕ),
    HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
        (Set.restrict (π := fun (a : E) ↦ ℝ) univ
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
        (const (↑univ : Type u_2) (c i)) ≤
      Set.restrict (π := fun (a : E) ↦ ℝ) univ φ
hsup :
  Eq (α := (a : (↑univ : Type u_2)) → ℝ)
    (⨆ (i : ℕ),
      HAdd.hAdd (α := (a : (↑univ : Type u_2)) → ℝ)
        (Set.restrict (π := fun (a : E) ↦ ℝ) univ
          (Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜)))
        (const (↑univ : Type u_2) (c i)))
    (Set.restrict (π := fun (a : E) ↦ ℝ) univ φ)
⊢ ⨆ (i : ℕ), Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i) = φ
have h : ∀ (x : E),
  (⨆ (i : ℕ), Function.comp.{u_2 + 1, u_1 + 1, 1} (β := 𝕜) (⇑re : (a : 𝕜) → ℝ) (⇑(l i) : (a : E) → 𝕜) + const E (c i))
      x =
    φ x
Tactic: ext x
-- 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 : SMul 𝕜 E
s : Set E
⊢ Convex 𝕜 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
have simp_rw : (∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → [x -[𝕜] y] ⊆ s) ↔
  ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
Tactic: simp_rw [convex_iff_segment_subset, segment_subset_iff]
-- 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 : SMul 𝕜 E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x : E
hx : Membership.mem (γ := Set E) (⋃ (i : ι), s i) x
y : E
hy : Membership.mem (γ := Set E) (⋃ (i : ι), s i) y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Membership.mem (γ := Set E) (⋃ (i : ι), s i) (a • x + b • y)
have rw : ∀ (hx : ∃ (i : ι), x ∈ s i) ⦃y : E⦄ (hy : ∃ (i : ι), y ∈ s i) ⦃a b : 𝕜⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
  ∃ (i : ι), a • x + b • y ∈ s i
Tactic: rw [mem_iUnion] at hx hy ⊢
Cleared hypotheses: hx, y, hy, a, b, ha, hb, hab
-- 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 : SMul 𝕜 E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x : E
hx : ∃ (i : ι), x ∈ s i
y : E
hy : ∃ (i : ι), y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ∃ (i : ι), a • x + b • y ∈ s i
have obtain : ∀ (i : ι) (hx : x ∈ s i), ∃ (i : ι), a • x + b • y ∈ s i
Tactic: obtain ⟨i, hx⟩ := hx
Cleared hypotheses: hx
-- 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 : SMul 𝕜 E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x y : E
hy : ∃ (i : ι), y ∈ s i
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hx : x ∈ s i
⊢ ∃ (i : ι), a • x + b • y ∈ s i
have obtain : ∀ (j : ι) (hy : y ∈ s j), ∃ (i : ι), a • x + b • y ∈ s i
Tactic: obtain ⟨j, hy⟩ := hy
Cleared hypotheses: 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 : SMul 𝕜 E
ι : Sort u_5
s : ι → Set E
hdir : Directed (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) s
hc : ∀ ⦃i : ι⦄, Convex 𝕜 (s i)
x y : E
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
i : ι
hx : x ∈ s i
j : ι
hy : y ∈ s j
⊢ ∃ (i : ι), a • x + b • y ∈ s i
have obtain : ∀ (k : ι) (hik : s i ⊆ s k) (hjk : s j ⊆ s k), ∃ (i : ι), a • x + b • y ∈ s i
Tactic: obtain ⟨k, hik, hjk⟩ := hdir i j
-- 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 : SMul 𝕜 E
c : Set (Set E)
hdir : DirectedOn (fun (x1 x2 : Set E) ↦ x1 ⊆ x2) c
hc : ∀ ⦃A : Set E⦄, A ∈ c → Convex 𝕜 A
⊢ Convex 𝕜 (⋃₀ c)
have rw : Convex.{u_1, u_2} 𝕜 (E := E) (⋃ (i : (↑c : Type u_2)), (↑i : Set E))
Tactic: rw [sUnion_eq_iUnion]
-- 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 : SMul 𝕜 E
s : Set E
P : Prop
hs : Convex 𝕜 s
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | P → x ∈ s}
have pos : ∀ (hP : P), Convex.{u_1, u_2} 𝕜 (E := E) {x : E | P → x ∈ s}
Tactic: by_cases hP : P
-- 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 : SMul 𝕜 E
s : Set E
P : Prop
hs : Convex 𝕜 s
pos : ∀ (hP : P), Convex.{u_1, u_2} 𝕜 (E := E) {x : E | P → x ∈ s}
⊢ Convex.{u_1, u_2} 𝕜 (E := E) {x : E | P → x ∈ s}
have neg : ∀ (hP : ¬P), Convex.{u_1, u_2} 𝕜 (E := E) {x : E | P → x ∈ s}
Tactic: by_cases hP : P
-- 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
⊢ Convex 𝕜 s ↔ s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
have refine : (s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s) →
  ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
Tactic: refine convex_iff_forall_pos.trans ⟨fun h x hx y hy _ => h 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 : Module 𝕜 E
s : Set E
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ 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 : ∀ (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.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
h : s.Pairwise fun (x y : E) ↦ ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
inl : ∀ (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.Basic (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : Semiring 𝕜
inst_1 : PartialOrder 𝕜
inst_2 : AddCommMonoid E
inst_3 : Module 𝕜 E
inst_4 : IsOrderedRing 𝕜
x y : 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 • x + bp • y) + b • (aq • x + bq • y) ∈ [x -[𝕜] y]
have refine_1 : a * ap + b * aq + (a * bp + b * bq) = 1
Tactic: refine
    ⟨a * ap + b * aq, a * bp + b * bq, add_nonneg (mul_nonneg ha hap) (mul_nonneg hb haq),
      add_nonneg (mul_nonneg ha hbp) (mul_nonneg hb hbq), ?_, ?_⟩
-- 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
inst_4 : IsOrderedRing 𝕜
x y : 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 • x + bp • y) + b • (aq • x + bq • y) ∈ [x -[𝕜] y]
have refine_2 : (a * ap + b * aq) • x + (a * bp + b * bq) • y = a • (ap • x + bp • y) + b • (aq • x + bq • y)
Tactic: refine
    ⟨a * ap + b * aq, a * bp + b * bq, add_nonneg (mul_nonneg ha hap) (mul_nonneg hb haq),
      add_nonneg (mul_nonneg ha hbp) (mul_nonneg hb hbq), ?_, ?_⟩
-- 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
inst_4 : IsOrderedRing 𝕜
x y : 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 refine_1 : a * ap + a * bp + (b * aq + b * bq) = 1
Tactic: rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]
-- 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
inst_4 : IsOrderedRing 𝕜
x y : 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 + a * bp + (b * aq + b * bq) = 1
⊢ a * ap + b * aq + (a * bp + b * bq) = 1
have refine_1₁ : a * (ap + bp) + (b * aq + b * bq) = 1
Tactic: rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]
-- 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
inst_4 : IsOrderedRing 𝕜
x y : 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 + a * bp + (b * aq + b * bq) = 1
refine_1₁ : a * (ap + bp) + (b * aq + b * bq) = 1
⊢ a * ap + b * aq + (a * bp + b * bq) = 1
have refine_1₂ : a * (ap + bp) + b * (aq + bq) = 1
Tactic: rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]
-- 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
inst_4 : IsOrderedRing 𝕜
x y : 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 + a * bp + (b * aq + b * bq) = 1
refine_1₁ : a * (ap + bp) + (b * aq + b * bq) = 1
refine_1₂ : a * (ap + bp) + b * (aq + bq) = 1
⊢ a * ap + b * aq + (a * bp + b * bq) = 1
have refine_1₃ : a * 1 + b * (aq + bq) = 1
Tactic: rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]
-- 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
inst_4 : IsOrderedRing 𝕜
x y : 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 + a * bp + (b * aq + b * bq) = 1
refine_1₁ : a * (ap + bp) + (b * aq + b * bq) = 1
refine_1₂ : a * (ap + bp) + b * (aq + bq) = 1
refine_1₃ : a * 1 + b * (aq + bq) = 1
⊢ a * ap + b * aq + (a * bp + b * bq) = 1
have refine_1₄ : a * 1 + b * 1 = 1
Tactic: rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]
-- 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
inst_4 : IsOrderedRing 𝕜
x y : 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 + a * bp + (b * aq + b * bq) = 1
refine_1₁ : a * (ap + bp) + (b * aq + b * bq) = 1
refine_1₂ : a * (ap + bp) + b * (aq + bq) = 1
refine_1₃ : a * 1 + b * (aq + bq) = 1
refine_1₄ : a * 1 + b * 1 = 1
⊢ a * ap + b * aq + (a * bp + b * bq) = 1
have refine_1₅ : a + b * 1 = 1
Tactic: rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]
-- 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
inst_4 : IsOrderedRing 𝕜
x y : 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 + a * bp + (b * aq + b * bq) = 1
refine_1₁ : a * (ap + bp) + (b * aq + b * bq) = 1
refine_1₂ : a * (ap + bp) + b * (aq + bq) = 1
refine_1₃ : a * 1 + b * (aq + bq) = 1
refine_1₄ : a * 1 + b * 1 = 1
refine_1₅ : a + b * 1 = 1
refine_1₆ : a + b = 1
⊢ a * ap + b * aq + (a * bp + b * bq) = 1
have refine_1₇ : Eq.{u_1 + 1} (α := 𝕜) 1 1
Tactic: rw [add_add_add_comm, ← mul_add, ← mul_add, habp, habq, mul_one, mul_one, hab]
-- 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
inst_4 : IsOrderedRing 𝕜
x y : 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) • x + (a * bp + b * bq) • y = a • (ap • x + bp • y) + b • (aq • x + bq • y)
have match_scalars : (a * ap + b * aq) * 1 = a * (ap * 1) + b * (aq * 1)
Tactic: match_scalars
-- 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
inst_4 : IsOrderedRing 𝕜
x y : 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
match_scalars : (a * ap + b * aq) * 1 = a * (ap * 1) + b * (aq * 1)
⊢ (a * ap + b * aq) • x + (a * bp + b * bq) • y = a • (ap • x + bp • y) + b • (aq • x + bq • y)
have match_scalars₁ : (a * bp + b * bq) * 1 = a * (bp * 1) + b * (bq * 1)
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (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
s : Set E
hs : Convex 𝕜 s
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
⊢ (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.Basic (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
s : Set E
hs : Convex 𝕜 s
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
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.Basic (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
s : Set E
hs : Convex 𝕜 s
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
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.Basic (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
s : Set F
hs : Convex 𝕜 s
f : E →ₗ[𝕜] F
x : E
hx : Membership.mem (γ := Set E) ((⇑f : (a : E) → F) ⁻¹' s) x
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, LinearMap.map_smul_of_tower, LinearMap.map_smul_of_tower]
-- 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 t : Set E
hs : Convex 𝕜 s
ht : Convex 𝕜 t
⊢ Convex 𝕜 (s + t)
have rw : Convex 𝕜 (E := E) ((fun (x : E × E) ↦ x.1 + x.2) '' s ×ˢ t)
Tactic: rw [← add_image_prod]
-- 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 : E
⊢ Convex 𝕜 (z +ᵥ s)
have simp_rw : Convex 𝕜 ({z} + s)
Tactic: simp_rw [← image_vadd, vadd_eq_add, ← singleton_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Basic (hypothesis)
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
⊢ Membership.mem (γ := Set E) ((fun (x : E) ↦ z + x) ⁻¹' s) (a • x + b • y)
have h : HSMul.hSMul (β := E) a ((fun (x : E) ↦ z + x) x) + HSMul.hSMul (β := E) b ((fun (x : E) ↦ z + x) y) ∈ s
Tactic: have h := hs hx hy ha hb hab
-- 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
⊢ 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