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
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
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 • f y) • a • g x + ((a • f x) • b • g y + (b • f y) • b • g y)
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 • a) • f y • g x + ((a • f x) • b • g y + (b • f y) • b • g y)
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 • a) • f y • g x + ((a • b) • f x • g y + (b • f y) • b • g y)
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 • a) • f y • g x + ((a • b) • f x • g y + (b • b) • f y • g y)
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 • a) • f y • g x + ((a • b) • f x • g y + (b • b) • f y • g y)
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 * a) • f y • g x + ((a • b) • f x • g y + (b • b) • f y • g y)
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 * 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)
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 * a) • f y • g x + ((a * b) • f x • g y + (b * b) • f y • g y)
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 a,
    add_comm ((a * b) • f x • g y), add_comm ((a * b) • f x • g y), add_add_add_comm]
-- 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
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 • f y) • a • g x + ((a • f x) • b • g y + (b • f y) • b • g y)
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 • a) • f y • g x + ((a • f x) • b • g y + (b • f y) • b • g y)
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 • a) • f y • g x + ((a • b) • f x • g y + (b • f y) • b • g y)
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 • a) • f y • g x + ((a • b) • f x • g y + (b • b) • f y • g y)
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 • a) • f y • g x + ((a • b) • f x • g y + (b • b) • f y • g y)
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 * a) • f y • g x + ((a • b) • f x • g y + (b • b) • f y • g y)
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 * a) • f y • g x + ((a * b) • f x • g y + (b • b) • f y • g y)
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 * 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)
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 + (a * b) • f y • g x + ((a * b) • f x • g y + (b * b) • f y • g y)
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 a,
    add_comm ((a * b) • f x • g y), add_comm ((a * b) • f x • g y), add_add_add_comm]
-- 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 : 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)
have rw : ConcaveOn 𝕜 s (-f • -g)
Tactic: rw [← neg_smul_neg]
-- 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 : 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)
have rw : ConvexOn 𝕜 s (-f • -g)
Tactic: rw [← neg_smul_neg]
-- 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 : 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)
have rw : ConvexOn 𝕜 s (f • -g)
Tactic: rw [← neg_convexOn_iff, ← smul_neg]
-- 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 : 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)
have rw : ConcaveOn 𝕜 s (f • -g)
Tactic: rw [← neg_concaveOn_iff, ← smul_neg]
-- 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 : 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)
have rw : ConcaveOn 𝕜 s (f • -g)
Tactic: rw [← neg_concaveOn_iff, ← smul_neg]
-- 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 : 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)
have rw : ConvexOn 𝕜 s (f • -g)
Tactic: rw [← neg_convexOn_iff, ← smul_neg]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
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 ^ (n + 1))
have rw : ConvexOn 𝕜 s (f * f ^ n)
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
hn : Even n
⊢ ConvexOn 𝕜 (β := 𝕜) univ fun (x : 𝕜) ↦ x ^ n
have obtain : ∀ (n : ℕ), ConvexOn 𝕜 (β := 𝕜) univ fun (x : 𝕜) ↦ x ^ (n + n)
Tactic: obtain ⟨n, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (β := 𝕜) univ fun (x : 𝕜) ↦ x ^ (n + n)
have simp_rw : ConvexOn 𝕜 (β := 𝕜) univ fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 2 ^ n
Tactic: simp_rw [← two_mul, pow_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
inst : CommRing 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (β := 𝕜) univ fun (x : 𝕜) ↦ HPow.hPow (β := ℕ) x 2 ^ n
have 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
Tactic: refine ConvexOn.pow ⟨convex_univ, fun x _ y _ a b ha hb hab ↦ sub_nonneg.1 ?_⟩
    (fun _ _ ↦ by positivity) _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
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
⊢ a * b * HPow.hPow (β := ℕ) (x - y) 2 =
    a • HPow.hPow (β := ℕ) x 2 + b • HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) (a • x + b • y) 2
have 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
Tactic: obtain rfl := eq_sub_of_add_eq hab
Cleared hypotheses: a, ha, hab
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
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
have 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
Tactic: simp only [smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
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 • HPow.hPow (β := ℕ) x 2 + b • HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) (a • x + b • y) 2
have by : 0 ≤ a * b * HPow.hPow (β := ℕ) (x - 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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
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
⊢ 0 ≤ a • HPow.hPow (β := ℕ) x 2 + b • HPow.hPow (β := ℕ) y 2 - HPow.hPow (β := ℕ) (a • x + b • y) 2
have 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
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
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (β := 𝕜) (Ioi 0) fun (x : 𝕜) ↦ HPow.hPow (β := ℤ) x (↑n : ℤ)
have simp_rw : ConvexOn 𝕜 (β := 𝕜) (Ioi 0) fun (x : 𝕜) ↦ x ^ n
Tactic: simp_rw [zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (β := 𝕜) (Ioi 0) fun (x : 𝕜) ↦ x ^ -[n+1]
have simp_rw : ConvexOn 𝕜 (β := 𝕜) (Ioi 0) fun (x : 𝕜) ↦ x⁻¹ ^ (n + 1)
Tactic: simp_rw [zpow_negSucc, ← inv_pow]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
⊢ ConvexOn 𝕜 (β := 𝕜) (Ioi 0) fun (x : 𝕜) ↦ x⁻¹ ^ (n + 1)
have refine : ∀ ⦃x : 𝕜⦄,
  Membership.mem (γ := Set 𝕜) (Ioi 0) x →
    ∀ ⦃y : 𝕜⦄,
      Membership.mem (γ := Set 𝕜) (Ioi 0) y →
        ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → (a • x + b • y)⁻¹ ≤ a • x⁻¹ + b • y⁻¹
Tactic: refine (convexOn_iff_forall_pos.2 ⟨convex_Ioi _, ?_⟩).pow (fun x (hx : 0 < x) ↦ by positivity) _
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a • x + b • y)⁻¹ ≤ a • x⁻¹ + b • y⁻¹
have simp : (a * x + b * y)⁻¹ ≤ a * x⁻¹ + b * y⁻¹
Tactic: simp only [smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (goal)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ (a * x + b * y)⁻¹ ≤ a * x⁻¹ + b * y⁻¹
have field_simp : x * y ≤ (a * x + b * y) * (a * y + x * b)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Convex.Mul (hypothesis)
Goal:
𝕜 : Type u_1
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
n : ℕ
x : 𝕜
hx : 0 < x
y : 𝕜
hy : 0 < y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ x * y ≤ (a * x + b * y) * (a * y + x * b)
have H : 0 ≤ a * b * HPow.hPow (β := ℕ) (x - y) 2
Tactic: have H : 0 ≤ a * b * (x - y) ^ 2 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.Convex.NNReal (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : Module ℝ M
s : Set M
⊢ Convex ℝ≥0 s ↔ Convex ℝ s
have refine : ∀ (H : Convex ℝ≥0 s), Convex ℝ s
Tactic: refine ⟨fun H ↦ ?_, Convex.lift ℝ≥0⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.NNReal (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : Module ℝ M
s : Set M
H : Convex ℝ≥0 s
x : M
hx : x ∈ s
⊢ StarConvex ℝ x s
have _ : ∀ ⦃y : M⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
Tactic: _
-- Lean 4 proof step from Mathlib.Analysis.Convex.NNReal (goal)
Goal:
M : Type u_1
inst : AddCommMonoid M
inst_1 : Module ℝ M
s : Set M
H : Convex ℝ≥0 s
x : M
hx : x ∈ s
y : M
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) a ha + Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) b hb = 1
have a₁ : (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) a ha + Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) b hb) : ℝ) = (↑1 : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.PartitionOfUnity (goal)
Goal:
X : Type u_2
E : Type u_3
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : NormalSpace X
inst_4 : ParacompactSpace X
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
H : ∀ (x : X), ∃ U ∈ 𝓝 x, ∃ (g : X → E), ContinuousOn g U ∧ ∀ y ∈ U, g y ∈ t y
⊢ ∃ (g : C(X, E)), ∀ (x : X), Membership.mem (α := E) (t x) ((g : (a : X) → E) x : E)
have choose : ∀ (U : (x : X) → Set X) (hU : ∀ (x : X), U x ∈ 𝓝 x) (g : (x : X) → X → E) (hgc : ∀ (x : X), ContinuousOn (g x) (U x))
  (hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y),
  ∃ (g : C(X, E)), ∀ (x : X), Membership.mem (α := E) (t x) ((g : (a : X) → E) x : E)
Tactic: choose U hU g hgc hgt using H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Analysis.Convex.PartitionOfUnity (goal)
Goal:
X : Type u_2
E : Type u_3
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : NormalSpace X
inst_4 : ParacompactSpace X
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : (x : X) → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
⊢ ∃ (g : C(X, E)), ∀ (x : X), Membership.mem (α := E) (t x) ((g : (a : X) → E) x : E)
have obtain : ∀ (f : PartitionOfUnity X X) (hf : f.IsSubordinate (s := univ) fun (x : X) ↦ interior (U x)),
  ∃ (g : C(X, E)), ∀ (x : X), Membership.mem (α := E) (t x) ((g : (a : X) → E) x : E)
Tactic: obtain ⟨f, hf⟩ := PartitionOfUnity.exists_isSubordinate isClosed_univ (fun x => interior (U x))
    (fun x => isOpen_interior) fun x _ => mem_iUnion.2 ⟨x, mem_interior_iff_mem_nhds.2 (hU x)⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.PartitionOfUnity (goal)
Goal:
X : Type u_2
E : Type u_3
inst : TopologicalSpace X
inst_1 : AddCommGroup E
inst_2 : Module ℝ E
inst_3 : NormalSpace X
inst_4 : ParacompactSpace X
inst_5 : TopologicalSpace E
inst_6 : ContinuousAdd E
inst_7 : ContinuousSMul ℝ E
t : X → Set E
ht : ∀ (x : X), Convex ℝ (t x)
U : (x : X) → Set X
hU : ∀ (x : X), U x ∈ 𝓝 x
g : (x : X) → X → E
hgc : ∀ (x : X), ContinuousOn (g x) (U x)
hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y
f : PartitionOfUnity X X
hf : f.IsSubordinate (s := univ) fun (x : X) ↦ interior (U x)
⊢ ∃ (g : C(X, E)), ∀ (x : X), Membership.mem (α := E) (t x) ((g : (a : X) → E) x : E)
have refine : ∀ (x i : X) (hi : Ne (α := ℝ) ((((f : (a : X) → C(X, ℝ)) i : C(X, ℝ)) : (a : X) → ℝ) x : ℝ) (0 : ℝ)), x ∈ U i
Tactic: refine ⟨⟨fun x => ∑ᶠ i, f i x • g i x,
    hf.continuous_finsum_smul (fun i => isOpen_interior) fun i => (hgc i).mono interior_subset⟩,
    fun x => f.finsum_smul_mem_convex (mem_univ x) (fun i hi => hgt _ _ ?_) (ht _)⟩
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b : E
⊢ Continuous.{0, u_1} (Y := E) fun (t : (↑I : Type)) ↦ (lineMap a b : (a : ℝ) → E) (↑t : ℝ)
have dsimp : Continuous.{0, u_1} (Y := E) fun (t : (↑I : Type)) ↦ (↑t : ℝ) • (b - a) + a
Tactic: dsimp [lineMap]
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b : E
⊢ range (ι := (↑I : Type)) (⇑(Path.segment a b) : (a : (↑I : Type)) → E) = [a -[ℝ] b]
have rw : Eq (α := Set E) (range (ι := (↑I : Type)) (⇑(Path.segment a b) : (a : (↑I : Type)) → E))
  (range fun (x : (↑(Icc 0 1) : Type)) ↦ (lineMap a b : (a : ℝ) → E) (↑x : ℝ))
Tactic: rw [segment_eq_image_lineMap, image_eq_range]
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a : E
⊢ Eq (α := Path a a) (Path.segment a a) (refl a)
have a₁ : ∀ (x : (↑I : Type)),
  Eq (α := E) ((Path.segment a a : (a : (↑I : Type)) → E) x : E) ((refl a : (a : (↑I : Type)) → E) x : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b : E
⊢ Eq (α := Path b a) (symm (Path.segment a b)) (Path.segment b a)
have a₁ : ∀ (x : (↑I : Type)),
  Eq (α := E) ((symm (Path.segment a b) : (a : (↑I : Type)) → E) x : E)
    ((Path.segment b a : (a : (↑I : Type)) → E) x : E)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Convex.PathConnected (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℝ E
inst_2 : TopologicalSpace E
inst_3 : ContinuousAdd E
inst_4 : ContinuousSMul ℝ E
a b c d : E
⊢ Eq (α := Path (a + c) (b + d)) (Path.add (Path.segment a b) (Path.segment c d)) (Path.segment (a + c) (b + d))
have a₁ : ∀ (x : (↑I : Type)),
  Eq (α := E) ((Path.add (Path.segment a b) (Path.segment c d) : (a : (↑I : Type)) → E) x : E)
    ((Path.segment (a + c) (b + d) : (a : (↑I : Type)) → E) x : E)
Tactic: ext