awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
inst_3 : BoundedSpace X
T : Type u_3
inst_4 : 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}ᶜ)
⊢ Continuous.{u_3, u_2} (Y := X) fun (i : T) ↦ convexCombPair (f i) (1 - f i) ⋯ ⋯ ⋯ (x i) (y i)

Tactic:
continuous_convexCombPair_of_isBounded f hf hf0 hf1 x y hx hy (.all _) (.all _)

Premises used: Bornology.IsBounded.all, Convexity.continuous_convexCombPair_of_isBounded
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 ⋯
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
⊢ dist (iConvexComb f Prod.fst) (iConvexComb f Prod.snd) ≤ iConvexComb f fun (x : P × P) ↦ dist x.1 x.2

Tactic:
simp only [AddTorsor.iConvexComb_eq_affineCombination]

Premises used: AddTorsor.iConvexComb_eq_affineCombination
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 ⋯
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
⊢ 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:
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]

Premises used: Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one, Convexity.StdSimplex.total
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 ⋯
this :
  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‖
⊢ 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:
simpa [dist_eq_norm_vsub, Finsupp.sum, ← Finset.sum_sub_distrib, ← smul_sub]

Premises used: Finsupp.sum, smul_sub, Finset.sum_sub_distrib, dist_eq_norm_vsub
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 ⋯
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‖
⊢ 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:
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]
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 ⋯
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‖)
⊢ 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:
grw [Finsupp.sum, Finsupp.sum, norm_sum_le]

Premises used: Finsupp.sum, norm_sum_le
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 ⋯
⊢ 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:
simp [norm_smul, abs_eq_self.mpr (f.nonneg _)]

Premises used: Iff.mpr, norm_smul, Convexity.StdSimplex.nonneg, abs_eq_self
-- Module: Mathlib.Analysis.Convex.MetricSpace
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)

Tactic:
⟨fun f ↦ ?_⟩

Premises used: Convexity.IsConvexDist.mk
-- Module: Mathlib.Analysis.Convex.MetricSpace
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
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
⊢ IsConvexDist.{u_2} (↑s : Type u_2)

Tactic:
refine ⟨fun f ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.MetricSpace
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 (α := 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) ≤
    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:
dist_iConvexComb_fst_snd_le (X := X) (f.map fun x ↦ (x.1, x.2))

Premises used: Convexity.IsConvexDist.dist_iConvexComb_fst_snd_le, Prod.mk, Convexity.StdSimplex.map
-- Module: Mathlib.Analysis.Convex.MetricSpace
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)
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)
⊢ 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:
convert dist_iConvexComb_fst_snd_le (X := X) (f.map fun x ↦ (x.1, x.2))

Premises used: Convexity.IsConvexDist.dist_iConvexComb_fst_snd_le, Prod.mk, Convexity.StdSimplex.map
-- Module: Mathlib.Analysis.Convex.MetricSpace
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) =
    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:
simp [Subtype.dist_eq, Finsupp.sum_mapDomain_index, add_mul]

Premises used: add_mul, Finsupp.sum_mapDomain_index, Subtype.dist_eq
-- Module: Mathlib.Analysis.Convex.MetricSpace
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))
⊢ 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:
simp [Subtype.dist_eq, Finsupp.sum_mapDomain_index, add_mul]

Premises used: add_mul, Finsupp.sum_mapDomain_index, Subtype.dist_eq
-- Module: Mathlib.Analysis.Convex.MetricSpace
Goal:
I : Type u_1
X : Type u_2
inst : ConvexSpace ℝ X
inst_1 : MetricSpace X
inst_2 : IsConvexDist X
F : Type u_3
M : Type u_4
inst_3 : AddCommGroup M
inst_4 : MetricSpace M
inst_5 : Module ℝ M
inst_6 : ConvexSpace ℝ M
inst_7 : IsModuleConvexSpace ℝ M
inst_8 : IsConvexDist M
inst_9 : SetLike F M
inst_10 : AddSubmonoidClass F M
inst_11 : SMulMemClass F ℝ M
S : F
⊢ IsConvexDist.{u_4} ↥S

Tactic:
.subtype _ _

Premises used: Convexity.IsConvexDist.subtype
-- Module: Mathlib.Analysis.Convex.Mul
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)

Tactic:
⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩

Premises used: And.left, And.intro, ConvexOn
-- Module: Mathlib.Analysis.Convex.Mul
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
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
⊢ ConvexOn 𝕜 s (f • g)

Tactic:
refine ⟨hf.1, fun x hx y hy a b ha hb hab ↦ ?_⟩
-- Module: Mathlib.Analysis.Convex.Mul
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
dsimp : f (a • x + b • y) • g (a • x + b • y) ≤ a • f x • g x + b • f y • g y
⊢ (f • g) (a • x + b • y) ≤ a • (f • g) x + b • (f • g) y

Tactic:
dsimp
-- Module: Mathlib.Analysis.Convex.Mul
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

Tactic:
(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 ?_

Premises used: smul_nonneg, add_nonneg, smul_le_smul, And.right, And.left, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Mul
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
hx₁ : (a • f x + b • f y) • (a • g x + b • g y) ≤ a • f x • g x + b • f y • g y
⊢ f (a • x + b • y) • g (a • x + b • 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 ?_

Premises used: smul_nonneg, add_nonneg, smul_le_smul, And.right, And.left, LE.le.trans
-- Module: Mathlib.Analysis.Convex.Mul
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)

Tactic:
?_
-- Module: Mathlib.Analysis.Convex.Mul
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
bc : f x • g y + f y • g x ≤ f x • g x + f y • g y
⊢ (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)

Tactic:
gcongr _ + (a * b) • ?_

Premises used: HMul.hMul
-- Module: Mathlib.Analysis.Convex.Mul
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 x • g y + f y • g x ≤ f x • g x + f y • g y

Tactic:
hfg.smul_add_smul_le_smul_add_smul hx hy

Premises used: MonovaryOn.smul_add_smul_le_smul_add_smul
-- Module: Mathlib.Analysis.Convex.Mul
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 x • g y + f y • g x ≤ f x • g x + f y • g y

Tactic:
exact hfg.smul_add_smul_le_smul_add_smul hx hy

Premises used: MonovaryOn.smul_add_smul_le_smul_add_smul
-- Module: Mathlib.Analysis.Convex.Mul
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
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)
⊢ (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

Tactic:
simp only [mul_add, add_smul, smul_add, mul_comm _ a]

Premises used: add_smul, mul_comm, mul_add, smul_add
-- Module: Mathlib.Analysis.Convex.Mul
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 + (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:
abel
-- Module: Mathlib.Analysis.Convex.Mul
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
simp_rw : (a * 1) • f x • g x + (b * 1) • f y • g y = a • f x • g x + b • f y • g y
⊢ (a * (a + b)) • f x • g x + (b * (a + b)) • f y • g y = a • f x • g x + b • f y • g y

Tactic:
simp_rw [hab, mul_one]

Premises used: mul_one