awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ (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 • 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)
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)]
-- 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)
⊢ (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 • 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)
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)]
-- 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)
⊢ (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 • 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)
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)]
-- 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)
⊢ (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 • 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)
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)]
-- 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)
⊢ (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 * 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)
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)]
-- 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)
⊢ (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 * 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)
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)]
-- 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)
⊢ (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 * 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)
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)]
-- 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)
⊢ (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 + (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)
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)]
-- 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)
⊢ (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 + (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)
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)]
-- 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
inst_18 : IsOrderedModule 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
⊢ ConcaveOn 𝕜 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),
  a • (f • g) x + b • (f • g) y ≤ (f • g) (a • x + b • 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
inst_18 : IsOrderedModule 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn 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 • g) x + b • (f • g) y ≤ (f • g) (a • x + b • y)
have dsimp : a • f x • g x + b • f y • g y ≤ f (a • x + b • y) • g (a • x + b • y)
Tactic: dsimp