-- 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
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)
rw₁ :
  (a • a) • f x • g x + (b • a) • f y • 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)
rw₂ :
  (a • a) • f x • g x + (b • a) • f y • g x + ((a • b) • f x • 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)
rw₃ :
  (a • a) • f x • g x + (b • a) • f y • g x + ((a • b) • f x • 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 y + (a * b) • f y • g x)
rw₄ :
  (a * a) • f x • g x + (b • a) • f y • g x + ((a • b) • f x • 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 y + (a * b) • f y • g x)
rw₅ :
  (a * a) • f x • g x + (b * a) • f y • g x + ((a • b) • f x • 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 y + (a * b) • f y • g x)
rw₆ :
  (a * a) • f x • g x + (b * a) • f y • g x + ((a * b) • f x • 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 y + (a * b) • f y • g x)
rw₇ :
  (a * a) • f x • g x + (b * a) • f y • g x + ((a * b) • f x • 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 y + (a * b) • f y • g x)
rw₈ :
  (a * a) • f x • g x + (a * b) • f y • g x + ((a * b) • f x • 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 y + (a * b) • f y • g x)
rw₉ :
  (a * a) • f x • g x + (a * b) • f y • g x + ((b * b) • f y • g y + (a * b) • f x • 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)
rw₁₀ :
  (a * a) • f x • g x + (b * b) • f y • g y + ((a * b) • f y • g x + (a * b) • f x • 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)
⊢ (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 * b) • f y • g y + ((a * b) • f x • g y + (a * b) • f y • g x) =
  (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)]