awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → g x ≤ 0
hfg : AntivaryOn f g s
rw : ConvexOn 𝕜 s (f • -g)
⊢ ConcaveOn 𝕜 s (f • g)

Tactic:
rw [← neg_convexOn_iff, ← smul_neg]

Premises used: neg_convexOn_iff, smul_neg
-- 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 : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → g x ≤ 0
hfg : AntivaryOn f g s
⊢ ConvexOn 𝕜 s (f • -g)

Tactic:
hf.smul' hg.neg hf₀ (fun x hx ↦ neg_nonneg.2 <| hg₀ hx) hfg.neg_right

Premises used: Iff.mpr, neg_nonneg, ConcaveOn.neg, AntivaryOn.neg_right, ConvexOn.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 : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → g x ≤ 0
hfg : AntivaryOn f g s
⊢ ConvexOn 𝕜 s (f • -g)

Tactic:
exact hf.smul' hg.neg hf₀ (fun x hx ↦ neg_nonneg.2 <| hg₀ hx) hfg.neg_right

Premises used: Iff.mpr, neg_nonneg, ConcaveOn.neg, AntivaryOn.neg_right, ConvexOn.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
inst_18 : IsOrderedModule 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → g x ≤ 0
hfg : MonovaryOn f g s
rw : ConcaveOn 𝕜 s (f • -g)
⊢ ConvexOn 𝕜 s (f • g)

Tactic:
rw [← neg_concaveOn_iff, ← smul_neg]

Premises used: smul_neg, neg_concaveOn_iff
-- 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
inst_18 : IsOrderedModule 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → g x ≤ 0
hfg : MonovaryOn f g s
⊢ ConcaveOn 𝕜 s (f • -g)

Tactic:
hf.smul' hg.neg hf₀ (fun x hx ↦ neg_nonneg.2 <| hg₀ hx) hfg.neg_right

Premises used: Iff.mpr, ConvexOn.neg, neg_nonneg, MonovaryOn.neg_right, ConcaveOn.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
inst_18 : IsOrderedModule 𝕜 E
hf : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → g x ≤ 0
hfg : MonovaryOn f g s
⊢ ConcaveOn 𝕜 s (f • -g)

Tactic:
exact hf.smul' hg.neg hf₀ (fun x hx ↦ neg_nonneg.2 <| hg₀ hx) hfg.neg_right

Premises used: Iff.mpr, ConvexOn.neg, neg_nonneg, MonovaryOn.neg_right, ConcaveOn.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
inst_18 : IsOrderedModule 𝕜 E
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
rw : ConcaveOn 𝕜 s (f • -g)
⊢ ConvexOn 𝕜 s (f • g)

Tactic:
rw [← neg_concaveOn_iff, ← smul_neg]

Premises used: smul_neg, neg_concaveOn_iff
-- 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
inst_18 : IsOrderedModule 𝕜 E
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
⊢ ConcaveOn 𝕜 s (f • -g)

Tactic:
hf.smul'' hg.neg hf₀ (fun x hx ↦ neg_nonpos.2 <| hg₀ hx) hfg.neg_right

Premises used: ConvexOn.smul'', Iff.mpr, neg_nonpos, ConcaveOn.neg, MonovaryOn.neg_right
-- 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
inst_18 : IsOrderedModule 𝕜 E
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
⊢ ConcaveOn 𝕜 s (f • -g)

Tactic:
exact hf.smul'' hg.neg hf₀ (fun x hx ↦ neg_nonpos.2 <| hg₀ hx) hfg.neg_right

Premises used: ConvexOn.smul'', Iff.mpr, neg_nonpos, ConcaveOn.neg, MonovaryOn.neg_right
-- 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 : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
rw : ConvexOn 𝕜 s (f • -g)
⊢ ConcaveOn 𝕜 s (f • g)

Tactic:
rw [← neg_convexOn_iff, ← smul_neg]

Premises used: neg_convexOn_iff, smul_neg
-- 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 : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
⊢ ConvexOn 𝕜 s (f • -g)

Tactic:
hf.smul'' hg.neg hf₀ (fun x hx ↦ neg_nonpos.2 <| hg₀ hx) hfg.neg_right

Premises used: Iff.mpr, ConcaveOn.smul'', neg_nonpos, ConvexOn.neg, AntivaryOn.neg_right
-- 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 : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
⊢ ConvexOn 𝕜 s (f • -g)

Tactic:
exact hf.smul'' hg.neg hf₀ (fun x hx ↦ neg_nonpos.2 <| hg₀ hx) hfg.neg_right

Premises used: Iff.mpr, ConcaveOn.smul'', neg_nonpos, ConvexOn.neg, AntivaryOn.neg_right
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
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 G
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 E
s : Set G
inst_9 : IsOrderedModule 𝕜 E
inst_10 : IsScalarTower 𝕜 E E
inst_11 : SMulCommClass 𝕜 E E
f g : G → E
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.smul' hg hf₀ hg₀ hfg

Premises used: ConvexOn.smul'
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
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 G
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 E
s : Set G
inst_9 : IsOrderedModule 𝕜 E
inst_10 : IsScalarTower 𝕜 E E
inst_11 : SMulCommClass 𝕜 E E
f g : G → 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)

Tactic:
hf.smul' hg hf₀ hg₀ hfg

Premises used: ConcaveOn.smul'
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
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 G
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 E
s : Set G
inst_9 : IsOrderedModule 𝕜 E
inst_10 : IsScalarTower 𝕜 E E
inst_11 : SMulCommClass 𝕜 E E
f g : G → E
hf : ConvexOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → g x ≤ 0
hfg : AntivaryOn f g s
⊢ ConcaveOn 𝕜 s (f * g)

Tactic:
hf.smul'' hg hf₀ hg₀ hfg

Premises used: ConvexOn.smul''
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
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 G
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 E
s : Set G
inst_9 : IsOrderedModule 𝕜 E
inst_10 : IsScalarTower 𝕜 E E
inst_11 : SMulCommClass 𝕜 E E
f g : G → E
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → g x ≤ 0
hfg : MonovaryOn f g s
⊢ ConvexOn 𝕜 s (f * g)

Tactic:
hf.smul'' hg hf₀ hg₀ hfg

Premises used: ConcaveOn.smul''
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
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 G
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 E
s : Set G
inst_9 : IsOrderedModule 𝕜 E
inst_10 : IsScalarTower 𝕜 E E
inst_11 : SMulCommClass 𝕜 E E
f g : G → E
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → g x ≤ 0
hfg : AntivaryOn f g s
⊢ ConcaveOn 𝕜 s (f * g)

Tactic:
hf.smul_concaveOn hg hf₀ hg₀ hfg

Premises used: ConvexOn.smul_concaveOn
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
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 G
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 E
s : Set G
inst_9 : IsOrderedModule 𝕜 E
inst_10 : IsScalarTower 𝕜 E E
inst_11 : SMulCommClass 𝕜 E E
f g : G → E
hf : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
hg₀ : ∀ ⦃x : G⦄, x ∈ s → g x ≤ 0
hfg : MonovaryOn f g s
⊢ ConvexOn 𝕜 s (f * g)

Tactic:
hf.smul_convexOn hg hf₀ hg₀ hfg

Premises used: ConcaveOn.smul_convexOn
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
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 G
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 E
s : Set G
inst_9 : IsOrderedModule 𝕜 E
inst_10 : IsScalarTower 𝕜 E E
inst_11 : SMulCommClass 𝕜 E E
f g : G → E
hf : ConvexOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : MonovaryOn f g s
⊢ ConvexOn 𝕜 s (f * g)

Tactic:
hf.smul_concaveOn' hg hf₀ hg₀ hfg

Premises used: ConvexOn.smul_concaveOn'
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
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 G
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 E
s : Set G
inst_9 : IsOrderedModule 𝕜 E
inst_10 : IsScalarTower 𝕜 E E
inst_11 : SMulCommClass 𝕜 E E
f g : G → E
hf : ConcaveOn 𝕜 s f
hg : ConvexOn 𝕜 s g
hf₀ : ∀ ⦃x : G⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ g x
hfg : AntivaryOn f g s
⊢ ConcaveOn 𝕜 s (f • g)

Tactic:
hf.smul_convexOn' hg hf₀ hg₀ hfg

Premises used: ConcaveOn.smul_convexOn'
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
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 G
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 E
s : Set G
inst_9 : IsOrderedModule 𝕜 E
inst_10 : IsScalarTower 𝕜 E E
inst_11 : SMulCommClass 𝕜 E E
f : G → E
hf : ConvexOn 𝕜 s f
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
⊢ ConvexOn 𝕜 s (HPow.hPow (β := ℕ) f 0)

Tactic:
simpa using convexOn_const 1 hf.1

Premises used: And.left, OfNat.ofNat, convexOn_const
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
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 G
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 E
s : Set G
inst_9 : IsOrderedModule 𝕜 E
inst_10 : IsScalarTower 𝕜 E E
inst_11 : SMulCommClass 𝕜 E E
f : G → E
hf : ConvexOn 𝕜 s f
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
n : ℕ
rw : ConvexOn 𝕜 s (f * f ^ n)
⊢ ConvexOn 𝕜 s (f ^ (n + 1))

Tactic:
rw [pow_succ']

Premises used: pow_succ'
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
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 G
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 E
s : Set G
inst_9 : IsOrderedModule 𝕜 E
inst_10 : IsScalarTower 𝕜 E E
inst_11 : SMulCommClass 𝕜 E E
f : G → E
hf : ConvexOn 𝕜 s f
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
n : ℕ
⊢ ConvexOn 𝕜 s (f * f ^ n)

Tactic:
hf.mul (hf.pow hf₀ _) hf₀ (fun x hx ↦ pow_nonneg (hf₀ hx) _) <|
      (monovaryOn_self f s).pow_right₀ hf₀ n

Premises used: pow_nonneg, MonovaryOn.pow_right₀, monovaryOn_self, ConvexOn.mul
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
E : Type u_2
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 G
inst_7 : Module 𝕜 G
inst_8 : Module 𝕜 E
s : Set G
inst_9 : IsOrderedModule 𝕜 E
inst_10 : IsScalarTower 𝕜 E E
inst_11 : SMulCommClass 𝕜 E E
f : G → E
hf : ConvexOn 𝕜 s f
hf₀ : ∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x
n : ℕ
⊢ ConvexOn 𝕜 s (f * f ^ n)

Tactic:
exact hf.mul (hf.pow hf₀ _) hf₀ (fun x hx ↦ pow_nonneg (hf₀ hx) _) <|
      (monovaryOn_self f s).pow_right₀ hf₀ n

Premises used: pow_nonneg, MonovaryOn.pow_right₀, monovaryOn_self, ConvexOn.mul
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
⊢ ∀ (n : ℕ), ConvexOn 𝕜 (β := 𝕜) (Ici 0) fun (x : 𝕜) ↦ x ^ n

Tactic:
(convexOn_id <| convex_Ici _).pow fun _ ↦ id

Premises used: convexOn_id, id, convex_Ici, ConvexOn.pow
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
hn : Even n
obtain : ∀ (n : ℕ), ConvexOn 𝕜 (β := 𝕜) univ fun (x : 𝕜) ↦ x ^ (n + n)
⊢ ConvexOn 𝕜 (β := 𝕜) univ fun (x : 𝕜) ↦ x ^ n

Tactic:
obtain ⟨n, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
simp_rw : ConvexOn 𝕜 (β := 𝕜) univ fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 2 ^ n
⊢ ConvexOn 𝕜 (β := 𝕜) univ fun (x : 𝕜) ↦ x ^ (n + n)

Tactic:
simp_rw [← two_mul, pow_mul]

Premises used: two_mul, pow_mul
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
h : Membership.mem (γ := Set 𝕜) univ x
⊢ 0 ≤ HPow.hPow (β := ℕ) x 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
refine :
  ∀ (x : 𝕜),
    Membership.mem (γ := Set 𝕜) univ x →
      ∀ (y : 𝕜),
        Membership.mem (γ := Set 𝕜) univ y →
          ∀ (a b : 𝕜) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1),
            0 ≤ a • HPow.hPow (β := ℕ) x 2 + b • HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) (a • x + b • y) 2
⊢ ConvexOn 𝕜 (β := 𝕜) univ fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 2 ^ n

Tactic:
refine ConvexOn.pow ⟨convex_univ, fun x _ y _ a b ha hb hab ↦ sub_nonneg.1 ?_⟩
    (fun _ _ ↦ by positivity) _

Premises used: convex_univ, And.intro, Iff.mp, ConvexOn.pow, sub_nonneg
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
h : Membership.mem (γ := Set 𝕜) univ x
y : 𝕜
h_1 : Membership.mem (γ := Set 𝕜) univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ 0 ≤ a * b * HPow.hPow (β := ℕ) (x - y) 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
h : Membership.mem (γ := Set 𝕜) univ x
y : 𝕜
h_1 : Membership.mem (γ := Set 𝕜) univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
obtain :
  ∀ (ha : 0 ≤ 1 - b) (hab : 1 - b + b = 1),
    (1 - b) * b * HPow.hPow (β := ℕ) (x - y) 2 =
      (1 - b) • HPow.hPow (β := ℕ) x 2 + b • HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) ((1 - b) • x + b • y) 2
⊢ a * b * HPow.hPow (β := ℕ) (x - y) 2 =
    a • HPow.hPow (β := ℕ) x 2 + b • HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) (a • x + b • y) 2

Tactic:
obtain rfl := eq_sub_of_add_eq hab

Premises used: eq_sub_of_add_eq, rfl
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
h : Membership.mem (γ := Set 𝕜) univ x
y : 𝕜
h_1 : Membership.mem (γ := Set 𝕜) univ y
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 1 - b
hab : 1 - b + b = 1
simp :
  (1 - b) * b * HPow.hPow (β := ℕ) (x - y) 2 =
    (1 - b) * HPow.hPow (β := ℕ) x 2 + b * HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) ((1 - b) * x + b * y) 2
⊢ (1 - b) * b * HPow.hPow (β := ℕ) (x - y) 2 =
    (1 - b) • HPow.hPow (β := ℕ) x 2 + b • HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) ((1 - b) • x + b • y) 2

Tactic:
simp only [smul_eq_mul]

Premises used: smul_eq_mul
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
h : Membership.mem (γ := Set 𝕜) univ x
y : 𝕜
h_1 : Membership.mem (γ := Set 𝕜) univ y
b : 𝕜
hb : 0 ≤ b
ha : 0 ≤ 1 - b
hab : 1 - b + b = 1
⊢ (1 - b) * b * HPow.hPow (β := ℕ) (x - y) 2 =
    (1 - b) * HPow.hPow (β := ℕ) x 2 + b * HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) ((1 - b) * x + b * y) 2

Tactic:
ring
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
h : Membership.mem (γ := Set 𝕜) univ x
y : 𝕜
h_1 : Membership.mem (γ := Set 𝕜) univ y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
by : 0 ≤ a * b * HPow.hPow (β := ℕ) (x - y) 2
by₁ :
  a * b * HPow.hPow (β := ℕ) (x - y) 2 =
    a • HPow.hPow (β := ℕ) x 2 + b • HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) (a • x + b • y) 2
⊢ 0 ≤ a • HPow.hPow (β := ℕ) x 2 + b • HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) (a • x + b • y) 2

Tactic:
calc
    (0 : 𝕜) ≤ (a * b) * (x - y) ^ 2 := by positivity
    _ = _ := by obtain rfl := eq_sub_of_add_eq hab; simp only [smul_eq_mul]; ring

Premises used: HMul.hMul, HSub.hSub, OfNat.ofNat
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
simp_rw : ConvexOn 𝕜 (β := 𝕜) (Ioi 0) fun (x : 𝕜) ↦ x ^ n
⊢ ConvexOn 𝕜 (β := 𝕜) (Ioi 0) fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (↑n : ℤ)

Tactic:
simp_rw [zpow_natCast]

Premises used: zpow_natCast
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (β := 𝕜) (Ioi 0) fun (x : 𝕜) ↦ x ^ n

Tactic:
(convexOn_pow n).subset Ioi_subset_Ici_self (convex_Ioi _)

Premises used: Set.Ioi_subset_Ici_self, convexOn_pow, convex_Ioi, ConvexOn.subset
-- Module: Mathlib.Analysis.Convex.Mul
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (β := 𝕜) (Ioi 0) fun (x : 𝕜) ↦ x ^ n

Tactic:
exact (convexOn_pow n).subset Ioi_subset_Ici_self (convex_Ioi _)

Premises used: Set.Ioi_subset_Ici_self, convexOn_pow, convex_Ioi, ConvexOn.subset