-- Mathlib/Analysis/Convex/Mul.lean
lemma ConcaveOn.smul' [OrderedSMul 𝕜 E] (hf : ConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g)
    (hf₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ f x) (hg₀ : ∀ ⦃x⦄, x ∈ s → 0 ≤ g x) (hfg : AntivaryOn f g s) :
    ConcaveOn 𝕜 s (f • g)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : 𝕜
hx : x ∈ s
y : 𝕜
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 * a) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g x + f y • g y)

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

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ (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 + (a * b) • f y • g y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x • g x + b • f y • g y = (a * (a + b)) • f x • g x + (b * (a + b)) • f y • g y

Tactic:
simp_rw [hab, mul_one]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • (f • g) x + b • (f • g) y ≤ (f • g) (a • x + b • y)

Tactic:
dsimp

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x • g x + b • f y • g y ≤ f (a * x + b * y) • g (a * x + b * y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : 𝕜
hx : x ∈ s
y : 𝕜
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) • f x • g x + (b * b) • f y • g y + (a * b) • (f x • g y + f y • g x)

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

Result:
case bc.hb
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : 𝕜
hx : x ∈ s
y : 𝕜
hy : y ∈ s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f x • g x + f y • g y ≤ f x • g y + f y • g x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : 𝕜
hx : x ∈ s
y : 𝕜
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 • f x + b • f y) • (a • g x + b • g y)

Tactic:
simp only [mul_add, add_smul, smul_add]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : LinearOrderedCommRing 𝕜
inst✝⁹ : LinearOrderedCommRing E
inst✝⁸ : LinearOrderedAddCommGroup F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : Module E F
inst✝⁴ : IsScalarTower 𝕜 E F
inst✝³ : SMulCommClass 𝕜 E F
inst✝² : OrderedSMul 𝕜 F
inst✝¹ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
inst✝ : OrderedSMul 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
x : 𝕜
hx : x ∈ s
y : 𝕜
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 + (a * b) • f y • g x) =
    (a • f x) • a • g x + (b • f y) • a • g x + ((a • f x) • b • g y + (b • f y) • b • g y)