awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (hypothesis)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht_1 : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : j ∈ x ⁻¹' Metric.ball (x t) (r / 3)
hj' : j ∈ f ⁻¹' Metric.ball 1 (r / D / 3)
⊢ convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y j) ∈ Metric.ball (x t) r
have hj₁ : dist (x j) (x t) < r / 3
Tactic: simp only [Set.mem_preimage, Metric.mem_ball, Real.dist_eq] at hj hj' ⊢
Cleared hypotheses: hj, hj'
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (hypothesis)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht_1 : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : j ∈ x ⁻¹' Metric.ball (x t) (r / 3)
hj' : j ∈ f ⁻¹' Metric.ball 1 (r / D / 3)
hj₁ : dist (x j) (x t) < r / 3
⊢ convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y j) ∈ Metric.ball (x t) r
have hj'₁ : |f j - 1| < r / D / 3
Tactic: simp only [Set.mem_preimage, Metric.mem_ball, Real.dist_eq] at hj hj' ⊢
Cleared hypotheses: hj, hj'
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht_1 : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
⊢ dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x j) (y j)) (x t) < r
have h : f j * dist (x j) (x t) + (1 - f j) * dist (y j) (y j) + dist (convexCombPair (f j) (1 - f j) sorry sorry sorry (x t) (y j)) (x t) <
  r
Tactic: grw [dist_triangle _ (convexCombPair (f j) (1 - f j) (hf0 _) (by simpa using hf1 _)
      (add_sub_cancel ..) (x t) (y j)), dist_convexCombPair_convexCombPair_le]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht_1 : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
⊢ f j * dist (x j) (x t) + (1 - f j) * dist (y j) (y j) +
      dist (convexCombPair (f j) (1 - f j) ⋯ ⋯ ⋯ (x t) (y j)) (x t) <
    r
have h : f j * dist (x j) (x t) + (1 - f j) * dist (x t) (y j) < r
Tactic: simp only [dist_self, mul_zero, add_zero, dist_convexCombPair_left]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (hypothesis)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht_1 : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : |f j - 1| < r / D / 3
⊢ f j * dist (x j) (x t) + (1 - f j) * dist (x t) (y j) < r
have hj'₁ : 1 - f j < r / D / 3
Tactic: grw [abs_sub_comm, ← le_abs_self] at hj'
Cleared hypotheses: hj'
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht_1 : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
⊢ f j * dist (x j) (x t) + (1 - f j) * dist (x t) (y j) < r
have h : 1 * (r / 3) + r / D / 3 * D < r
Tactic: grw [hj, hj', hf1, hD]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht_1 : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
h : 1 * (r / 3) + r / D / 3 * D < r
⊢ f j * dist (x j) (x t) + (1 - f j) * dist (x t) (y j) < r
have h₁ : 0 ≤ f j
Tactic: grw [hj, hj', hf1, hD]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
T : Type u_3
inst_3 : TopologicalSpace T
f : T → ℝ
hf : Continuous f
hf0 : ∀ (t : T), 0 ≤ f t
hf1 : ∀ (t : T), f t ≤ 1
x y : T → X
hx : ContinuousOn x (f ⁻¹' {0}ᶜ)
hy : ContinuousOn y (f ⁻¹' {1}ᶜ)
hx' : Bornology.IsBounded (Set.range x)
hy' : Bornology.IsBounded (Set.range y)
D : ℝ
hD' : 0 < D
hD : ∀ (t₁ t₂ : T), dist (x t₁) (y t₂) ≤ D
t : T
ht_1 : f t ∉ Set.Ioo 0 1
ht : f t = 1
r : ℝ
hr : 0 < r
j : T
hj : dist (x j) (x t) < r / 3
hj' : 1 - f j < r / D / 3
⊢ 1 * (r / 3) + r / D / 3 * D < r
have h : HAdd.hAdd (α := ℝ) 1 1 < 3
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
I : Type u_1
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
V : Type u_3
P : Type u_4
inst_3 : NormedAddCommGroup V
inst_4 : NormedSpace ℝ V
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
p : P := Nonempty.some ⋯
⊢ dist (iConvexComb f Prod.fst) (iConvexComb f Prod.snd) ≤ iConvexComb f fun (x : P × P) ↦ dist x.1 x.2
have simp : dist (α := P)
    ((Finset.affineCombination ℝ f.weights.support Prod.fst : (a : P × P → ℝ) → P) (⇑f.weights : (a : P × P) → ℝ) : P)
    ((Finset.affineCombination ℝ f.weights.support Prod.snd : (a : P × P → ℝ) → P) (⇑f.weights : (a : P × P) → ℝ) : P) ≤
  iConvexComb f fun (x : P × P) ↦ dist x.1 x.2
Tactic: simp only [AddTorsor.iConvexComb_eq_affineCombination]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
I : Type u_1
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
V : Type u_3
P : Type u_4
inst_3 : NormedAddCommGroup V
inst_4 : NormedSpace ℝ V
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
p : P := Nonempty.some ⋯
⊢ dist (α := P)
      ((Finset.affineCombination ℝ f.weights.support Prod.fst : (a : P × P → ℝ) → P) (⇑f.weights : (a : P × P) → ℝ) : P)
      ((Finset.affineCombination ℝ f.weights.support Prod.snd : (a : P × P → ℝ) → P) (⇑f.weights : (a : P × P) → ℝ) :
        P) ≤
    iConvexComb f fun (x : P × P) ↦ dist x.1 x.2
have rw : dist
    (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
      ((f.weights.support.weightedVSubOfPoint Prod.fst p : (a : P × P → ℝ) → V) fun (i : P × P) ↦
          (fun (x : P × P) (r : ℝ) ↦ r) i ((f.weights : (a : P × P) → ℝ) i) :
        V)
      p)
    (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
      ((f.weights.support.weightedVSubOfPoint Prod.snd p : (a : P × P → ℝ) → V) fun (i : P × P) ↦
          (fun (x : P × P) (r : ℝ) ↦ r) i ((f.weights : (a : P × P) → ℝ) i) :
        V)
      p) ≤
  iConvexComb f fun (x : P × P) ↦ dist x.1 x.2
Tactic: rw [Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ f.total p,
      Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one _ _ _ f.total p]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
I : Type u_1
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
V : Type u_3
P : Type u_4
inst_3 : NormedAddCommGroup V
inst_4 : NormedSpace ℝ V
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
p : P := Nonempty.some ⋯
⊢ dist
      (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
        ((f.weights.support.weightedVSubOfPoint Prod.fst p : (a : P × P → ℝ) → V) fun (i : P × P) ↦
            (fun (x : P × P) (r : ℝ) ↦ r) i ((f.weights : (a : P × P) → ℝ) i) :
          V)
        p)
      (HVAdd.hVAdd.{u_3, u_4, u_4} (α := V)
        ((f.weights.support.weightedVSubOfPoint Prod.snd p : (a : P × P → ℝ) → V) fun (i : P × P) ↦
            (fun (x : P × P) (r : ℝ) ↦ r) i ((f.weights : (a : P × P) → ℝ) i) :
          V)
        p) ≤
    iConvexComb f fun (x : P × P) ↦ dist x.1 x.2
have suffices : norm.{u_3} (E := V) (f.weights.sum fun (a : P × P) (b : ℝ) ↦ b • (a.1 -ᵥ a.2)) ≤
  f.weights.sum fun (a : P × P) (b : ℝ) ↦ b * ‖a.1 -ᵥ a.2‖
Tactic: suffices ‖f.weights.sum fun a b ↦ b • (a.1 -ᵥ a.2)‖ ≤
      f.weights.sum fun a b ↦ b * ‖a.1 -ᵥ a.2‖ by
      simpa [dist_eq_norm_vsub, Finsupp.sum, ← Finset.sum_sub_distrib, ← smul_sub]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
I : Type u_1
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
V : Type u_3
P : Type u_4
inst_3 : NormedAddCommGroup V
inst_4 : NormedSpace ℝ V
inst_5 : MetricSpace P
inst_6 : NormedAddTorsor V P
f : StdSimplex ℝ (P × P)
p : P := Nonempty.some ⋯
⊢ norm.{u_3} (E := V) (f.weights.sum fun (a : P × P) (b : ℝ) ↦ b • (a.1 -ᵥ a.2)) ≤
    f.weights.sum fun (a : P × P) (b : ℝ) ↦ b * ‖a.1 -ᵥ a.2‖
have grw : LE.le (α := ℝ) (∑ i ∈ f.weights.support, ‖HSMul.hSMul (α := ℝ) ((f.weights : (a : P × P) → ℝ) i : ℝ) (i.1 -ᵥ i.2)‖)
  (∑ a ∈ f.weights.support, HMul.hMul (α := ℝ) ((f.weights : (a : P × P) → ℝ) a : ℝ) ‖a.1 -ᵥ a.2‖)
Tactic: grw [Finsupp.sum, Finsupp.sum, norm_sum_le]
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
I : Type u_1
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s : Set X
hs : IsConvexSet ℝ s
this : ConvexSpace ℝ (↑s : Type u_2) := ConvexSpace.subtype s hs
⊢ IsConvexDist.{u_2} (↑s : Type u_2)
have refine : ∀ (f : StdSimplex ℝ ((↑s : Type u_2) × (↑s : Type u_2))),
  dist (iConvexComb f Prod.fst) (iConvexComb f Prod.snd) ≤
    iConvexComb f fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ dist x.1 x.2
Tactic: refine ⟨fun f ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
I : Type u_1
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s : Set X
hs : IsConvexSet ℝ s
this : ConvexSpace ℝ (↑s : Type u_2) := ConvexSpace.subtype s hs
f : StdSimplex ℝ ((↑s : Type u_2) × (↑s : Type u_2))
⊢ dist (iConvexComb f Prod.fst) (iConvexComb f Prod.snd) ≤
    iConvexComb f fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ dist x.1 x.2
have h : dist (iConvexComb f Prod.fst) (iConvexComb f Prod.snd) =
  dist (α := X)
    (iConvexComb (I := X × X)
      (StdSimplex.map (fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ ((↑x.1 : X), (↑x.2 : X))) f) Prod.fst)
    (iConvexComb (I := X × X)
      (StdSimplex.map (fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ ((↑x.1 : X), (↑x.2 : X))) f) Prod.snd)
Tactic: convert dist_iConvexComb_fst_snd_le (X := X) (f.map fun x ↦ (x.1, x.2))
-- Lean 4 proof step from Mathlib.Analysis.Convex.MetricSpace (goal)
Goal:
I : Type u_1
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
s : Set X
hs : IsConvexSet ℝ s
this : ConvexSpace ℝ (↑s : Type u_2) := ConvexSpace.subtype s hs
f : StdSimplex ℝ ((↑s : Type u_2) × (↑s : Type u_2))
h :
  dist (iConvexComb f Prod.fst) (iConvexComb f Prod.snd) =
    dist (α := X)
      (iConvexComb (I := X × X)
        (StdSimplex.map (fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ ((↑x.1 : X), (↑x.2 : X))) f) Prod.fst)
      (iConvexComb (I := X × X)
        (StdSimplex.map (fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ ((↑x.1 : X), (↑x.2 : X))) f) Prod.snd)
⊢ dist (iConvexComb f Prod.fst) (iConvexComb f Prod.snd) ≤
    iConvexComb f fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ dist x.1 x.2
have h₁ : Eq (α := ℝ) (iConvexComb f fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ dist x.1 x.2)
  (iConvexComb (StdSimplex.map (fun (x : (↑s : Type u_2) × (↑s : Type u_2)) ↦ ((↑x.1 : X), (↑x.2 : X))) f)
    fun (x : X × X) ↦ dist x.1 x.2)
Tactic: convert dist_iConvexComb_fst_snd_le (X := X) (f.map fun x ↦ (x.1, x.2))
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : CommRing E
inst_4 : LinearOrder E
inst_5 : IsStrictOrderedRing E
inst_6 : AddCommGroup F
inst_7 : LinearOrder F
inst_8 : IsOrderedAddMonoid F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : Module 𝕜 E
inst_12 : Module 𝕜 F
inst_13 : Module E F
inst_14 : IsScalarTower 𝕜 E F
inst_15 : SMulCommClass 𝕜 E F
inst_16 : IsOrderedModule 𝕜 F
inst_17 : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
⊢ ConvexOn 𝕜 s (f • g)
have refine : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ s) (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
  (f • g) (a • x + b • y) ≤ a • (f • g) x + b • (f • g) y
Tactic: refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : CommRing E
inst_4 : LinearOrder E
inst_5 : IsStrictOrderedRing E
inst_6 : AddCommGroup F
inst_7 : LinearOrder F
inst_8 : IsOrderedAddMonoid F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : Module 𝕜 E
inst_12 : Module 𝕜 F
inst_13 : Module E F
inst_14 : IsScalarTower 𝕜 E F
inst_15 : SMulCommClass 𝕜 E F
inst_16 : IsOrderedModule 𝕜 F
inst_17 : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (f • g) (a • x + b • y) ≤ a • (f • g) x + b • (f • g) y
have dsimp : f (a • x + b • y) • g (a • x + b • y) ≤ a • f x • g x + b • f y • g y
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : CommRing E
inst_4 : LinearOrder E
inst_5 : IsStrictOrderedRing E
inst_6 : AddCommGroup F
inst_7 : LinearOrder F
inst_8 : IsOrderedAddMonoid F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : Module 𝕜 E
inst_12 : Module 𝕜 F
inst_13 : Module E F
inst_14 : IsScalarTower 𝕜 E F
inst_15 : SMulCommClass 𝕜 E F
inst_16 : IsOrderedModule 𝕜 F
inst_17 : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y) • g (a • x + b • y) ≤ a • f x • g x + b • f y • g y
have hx₁ : (a • f x + b • f y) • (a • g x + b • g y) ≤ a • f x • g x + b • f y • g y
Tactic: refine
    (smul_le_smul (hf.2 hx hy ha hb hab) (hg.2 hx hy ha hb hab) (hf₀ <| hf.1 hx hy ha hb hab) <|
      add_nonneg (smul_nonneg ha <| hg₀ hx) <| smul_nonneg hb <| hg₀ hy).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : CommRing E
inst_4 : LinearOrder E
inst_5 : IsStrictOrderedRing E
inst_6 : AddCommGroup F
inst_7 : LinearOrder F
inst_8 : IsOrderedAddMonoid F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : Module 𝕜 E
inst_12 : Module 𝕜 F
inst_13 : Module E F
inst_14 : IsScalarTower 𝕜 E F
inst_15 : SMulCommClass 𝕜 E F
inst_16 : IsOrderedModule 𝕜 F
inst_17 : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g y + f y • g x) ≤
    (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g x + f y • g y)
have bc : f x • g y + f y • g x ≤ f x • g x + f y • g y
Tactic: gcongr _ + (a * b) • ?_
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : CommRing E
inst_4 : LinearOrder E
inst_5 : IsStrictOrderedRing E
inst_6 : AddCommGroup F
inst_7 : LinearOrder F
inst_8 : IsOrderedAddMonoid F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : Module 𝕜 E
inst_12 : Module 𝕜 F
inst_13 : Module E F
inst_14 : IsScalarTower 𝕜 E F
inst_15 : SMulCommClass 𝕜 E F
inst_16 : IsOrderedModule 𝕜 F
inst_17 : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g x + f y • g y) =
    (a * (a + b)) • f x • g x + (b * (a + b)) • f y • g y
have simp : (a * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f x • g x + (a * b) • f y • g y) =
  (a * a) • f x • g x + (a * b) • f x • g x + ((a * b) • f y • g y + (b * b) • f y • g y)
Tactic: simp only [mul_add, add_smul, smul_add, mul_comm _ a]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : CommRing E
inst_4 : LinearOrder E
inst_5 : IsStrictOrderedRing E
inst_6 : AddCommGroup F
inst_7 : LinearOrder F
inst_8 : IsOrderedAddMonoid F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : Module 𝕜 E
inst_12 : Module 𝕜 F
inst_13 : Module E F
inst_14 : IsScalarTower 𝕜 E F
inst_15 : SMulCommClass 𝕜 E F
inst_16 : IsOrderedModule 𝕜 F
inst_17 : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a * (a + b)) • f x • g x + (b * (a + b)) • f y • g y = a • f x • g x + b • f y • g y
have simp_rw : (a * 1) • f x • g x + (b * 1) • f y • g y = a • f x • g x + b • f y • g y
Tactic: simp_rw [hab, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : CommRing E
inst_4 : LinearOrder E
inst_5 : IsStrictOrderedRing E
inst_6 : AddCommGroup F
inst_7 : LinearOrder F
inst_8 : IsOrderedAddMonoid F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : Module 𝕜 E
inst_12 : Module 𝕜 F
inst_13 : Module E F
inst_14 : IsScalarTower 𝕜 E F
inst_15 : SMulCommClass 𝕜 E F
inst_16 : IsOrderedModule 𝕜 F
inst_17 : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a • f x + b • f y) • (a • g x + b • g y) ≤ a • f x • g x + b • f y • g y
have _ : (a • f x + b • f y) • (a • g x + b • g y) =
  (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g y + f y • g x)
Tactic: calc
      _ = (a * a) • (f x • g x) + (b * b) • (f y • g y) + (a * b) • (f x • g y + f y • g x) := ?_
    _ ≤ (a * a) • (f x • g x) + (b * b) • (f y • g y) + (a * b) • (f x • g x + f y • g y) := by
        gcongr _ + (a * b) • ?_; exact hfg.smul_add_smul_le_smul_add_smul hx hy
    _ = (a * (a + b)) • (f x • g x) + (b * (a + b)) • (f y • g y) := by
        simp only [mul_add, add_smul, smul_add, mul_comm _ a]; abel
    _ = _ := by simp_rw [hab, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : CommRing E
inst_4 : LinearOrder E
inst_5 : IsStrictOrderedRing E
inst_6 : AddCommGroup F
inst_7 : LinearOrder F
inst_8 : IsOrderedAddMonoid F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : Module 𝕜 E
inst_12 : Module 𝕜 F
inst_13 : Module E F
inst_14 : IsScalarTower 𝕜 E F
inst_15 : SMulCommClass 𝕜 E F
inst_16 : IsOrderedModule 𝕜 F
inst_17 : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a • f x + b • f y) • (a • g x + b • g y) =
    (a * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g y + f y • g x)
have simp : (a • f x) • a • g x + (b • f y) • a • g x + ((a • f x) • b • g y + (b • f y) • b • g y) =
  (a * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f x • g y + (a * b) • f y • g x)
Tactic: simp only [add_smul, smul_add]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
inst_3 : CommRing E
inst_4 : LinearOrder E
inst_5 : IsStrictOrderedRing E
inst_6 : AddCommGroup F
inst_7 : LinearOrder F
inst_8 : IsOrderedAddMonoid F
inst_9 : AddCommGroup G
inst_10 : Module 𝕜 G
inst_11 : Module 𝕜 E
inst_12 : Module 𝕜 F
inst_13 : Module E F
inst_14 : IsScalarTower 𝕜 E F
inst_15 : SMulCommClass 𝕜 E F
inst_16 : IsOrderedModule 𝕜 F
inst_17 : IsStrictOrderedModule E F
s : Set G
f : G → E
g : G → F
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
x : G
hx : x ∈ s
y : G
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (a • f x) • a • g x + (b • f y) • a • g x + ((a • f x) • b • g y + (b • f y) • b • g y) =
    (a * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f x • g y + (a * b) • f y • g x)
have rw : (a • a) • f x • g x + (b • f y) • a • g x + ((a • f x) • b • g y + (b • f y) • b • g y) =
  (a * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f x • g y + (a * b) • f y • g x)
Tactic: rw [← smul_smul_smul_comm a, ← smul_smul_smul_comm b, ← smul_smul_smul_comm a b,
    ← smul_smul_smul_comm b b, smul_eq_mul, smul_eq_mul, smul_eq_mul, smul_eq_mul, mul_comm b,
    add_comm _ ((b * b) • f y • g y), add_add_add_comm, add_comm ((a * b) • f y • g x)]