awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
hz' : ∀ (i : ι) (h : i ∈ s), 0 < z i
this :
  Eq (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x))) ↔
    ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
h₁ : Eq (α := ℝ) (∑ i ∈ s, w i * z j) (∑ i ∈ s, w i * z i)
⊢ z j = ∑ i ∈ s, w i * z i

Tactic:
rw [← arith_mean_weighted_of_constant s w _ (z j) hw' fun i _ => congrFun rfl]

Premises used: Real.arith_mean_weighted_of_constant, congrFun, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
hz' : ∀ (i : ι) (h : i ∈ s), 0 < z i
this :
  Eq (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x))) ↔
    ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
h₁ : ∀ x ∈ s, w x * z j = w x * z x
⊢ Eq (α := ℝ) (∑ i ∈ s, w i * z j) (∑ i ∈ s, w i * z i)

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
hz' : ∀ (i : ι) (h : i ∈ s), 0 < z i
this :
  Eq (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x))) ↔
    ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
h : ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
j : ι
hj : j ∈ s
x : ι
hx : x ∈ s
⊢ w x * z j = w x * z x

Tactic:
simp only [log_injOn_pos (hz' j hj) (hz' x hx), h j hj, h x hx]

Premises used: Real.log_injOn_pos
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
h : i ∈ s
⊢ w i * z i ≠ 0 → w i ≠ 0

Tactic:
apply left_ne_zero_of_mul

Premises used: left_ne_zero_of_mul
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
⊢ ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0

Tactic:
have h (i) (_ : i ∈ s) : w i * z i ≠ 0 → w i ≠ 0 := by apply left_ne_zero_of_mul
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0
i : ι
h_1 : i ∈ s
by_contra! : ∀ (h1 : z i ^ w i ≠ 1) (h2 : w i = 0), False
⊢ z i ^ w i ≠ 1 → w i ≠ 0

Tactic:
by_contra! ⟨h1, h2⟩
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0
i : ι
h_1 : i ∈ s
h1 : z i ^ w i ≠ 1
h2 : w i = 0
⊢ False

Tactic:
simp only [h2, rpow_zero, ne_self_iff_false] at h1

Premises used: ne_self_iff_false, Real.rpow_zero
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0
⊢ ∀ i ∈ s, z i ^ w i ≠ 1 → w i ≠ 0

Tactic:
have h' (i) (_ : i ∈ s) : z i ^ w i ≠ 1 → w i ≠ 0 := by
    by_contra! ⟨h1, h2⟩
    simp only [h2, rpow_zero, ne_self_iff_false] at h1
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0
h' : ∀ i ∈ s, z i ^ w i ≠ 1 → w i ≠ 0
rw :
  (∀ j ∈ {x ∈ s | w x ≠ 0}, z j = ∑ i ∈ s with w i ≠ 0, w i * z i) ↔
    ∀ j ∈ s, w j ≠ 0 → z j = ∑ x ∈ s with w x ≠ 0, w x * z x
hw₁ : ∀ i ∈ {x ∈ s | w x ≠ 0}, 0 < w i
hw'₁ : Eq (α := ℝ) (∑ i ∈ s with w i ≠ 0, w i) 1
hz₁ : ∀ i ∈ {x ∈ s | w x ≠ 0}, 0 ≤ z i
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, w j ≠ 0 → z j = ∑ i ∈ s, w i * z i

Tactic:
rw [← sum_filter_of_ne h, ← prod_filter_of_ne h', geom_mean_eq_arith_mean_weighted_iff']

Premises used: Real.geom_mean_eq_arith_mean_weighted_iff', Finset.prod_filter_of_ne, Finset.sum_filter_of_ne
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0
h' : ∀ i ∈ s, z i ^ w i ≠ 1 → w i ≠ 0
⊢ (∀ j ∈ {x ∈ s | w x ≠ 0}, z j = ∑ i ∈ s with w i ≠ 0, w i * z i) ↔
    ∀ j ∈ s, w j ≠ 0 → z j = ∑ x ∈ s with w x ≠ 0, w x * z x

Tactic:
simp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0
h' : ∀ i ∈ s, z i ^ w i ≠ 1 → w i ≠ 0
⊢ ∀ i ∈ {x ∈ s | w x ≠ 0}, 0 < w i

Tactic:
simp +contextual [(hw _ _).lt_iff_ne']

Premises used: LE.le.lt_iff_ne'
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0
h' : ∀ i ∈ s, z i ^ w i ≠ 1 → w i ≠ 0
hw'₁ hw'₂ hw'₃ hw'₄ : Eq (α := ℝ) (∑ x ∈ s, w x) 1
⊢ Eq (α := ℝ) (∑ i ∈ s with w i ≠ 0, w i) 1

Tactic:
rwa [sum_filter_ne_zero]

Premises used: Finset.sum_filter_ne_zero
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0
h' : ∀ i ∈ s, z i ^ w i ≠ 1 → w i ≠ 0
⊢ ∀ i ∈ {x ∈ s | w x ≠ 0}, 0 ≤ z i

Tactic:
simp_all only [ne_eq, mul_eq_zero, not_or, not_false_eq_true, implies_true, mem_filter]

Premises used: mul_eq_zero, ne_eq, not_or, Finset.mem_filter, implies_true, not_false_eq_true
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
mp : LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) → ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k
mpr : (∃ j ∈ s, ∃ k ∈ s, z j ≠ z k) → LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
⊢ LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k

Tactic:
constructor
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
mp : ∀ (h_contra : ∀ (j : ι) (_ : j ∈ s) (k : ι) (_ : k ∈ s), z j = z k), False
⊢ ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k

Tactic:
by_contra! h_contra
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
h_contra : ∀ (j : ι) (_ : j ∈ s) (k : ι) (_ : k ∈ s), z j = z k
mp :
  ∀ (h : LT.lt (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i * z i))
    (h_contra : ∀ (j : ι) (_ : j ∈ s) (k : ι) (_ : k ∈ s), z j = z k), False
rw : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
⊢ False

Tactic:
rw [(geom_mean_eq_arith_mean_weighted_iff' s w z hw hw' hz).mpr ?_] at h

Premises used: Iff.mpr, Real.geom_mean_eq_arith_mean_weighted_iff'
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : LT.lt (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i * z i)
h_contra : ∀ (j : ι) (_ : j ∈ s) (k : ι) (_ : k ∈ s), z j = z k
⊢ False

Tactic:
(lt_self_iff_false _).mp h

Premises used: lt_self_iff_false, Iff.mp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : LT.lt (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i * z i)
h_contra : ∀ (j : ι) (_ : j ∈ s) (k : ι) (_ : k ∈ s), z j = z k
⊢ False

Tactic:
exact (lt_self_iff_false _).mp h

Premises used: lt_self_iff_false, Iff.mp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
h_contra : ∀ (j : ι) (_ : j ∈ s) (k : ι) (_ : k ∈ s), z j = z k
j : ι
hjs : j ∈ s
rw : Eq (α := ℝ) (∑ i ∈ s, w i * z j) (∑ i ∈ s, w i * z i)
⊢ z j = ∑ i ∈ s, w i * z i

Tactic:
rw [← arith_mean_weighted_of_constant s w (fun _ => z j) (z j) hw' fun _ _ => congrFun rfl]

Premises used: Real.arith_mean_weighted_of_constant, congrFun, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
h : LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
h_contra : ∀ (j : ι) (_ : j ∈ s) (k : ι) (_ : k ∈ s), z j = z k
j : ι
hjs : j ∈ s
⊢ Eq (α := ℝ) (∑ i ∈ s, w i * z j) (∑ i ∈ s, w i * z i)

Tactic:
apply sum_congr rfl (fun x a => congrArg (HMul.hMul (w x)) (h_contra j hjs x a))

Premises used: HMul.hMul, congrArg, Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
⊢ LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)

Tactic:
have := geom_mean_le_arith_mean_weighted s w z (fun i a => le_of_lt (hw i a)) hw' hz
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
this : LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
mpr : ∀ (h : LE.le (α := ℝ) (∑ i ∈ s, w i * z i) (∏ i ∈ s, z i ^ w i)), False
⊢ LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)

Tactic:
by_contra! h
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
this : LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
h : LE.le (α := ℝ) (∑ i ∈ s, w i * z i) (∏ i ∈ s, z i ^ w i)
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)

Tactic:
apply le_antisymm this at h

Premises used: le_antisymm
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
this : LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
h : Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
⊢ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
apply (geom_mean_eq_arith_mean_weighted_iff' s w z hw hw' hz).mp at h

Premises used: Real.geom_mean_eq_arith_mean_weighted_iff', Iff.mp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
this : LE.le (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
⊢ False

Tactic:
simp only [h j hjs, h k hks, ne_eq, not_true_eq_false] at hzjk

Premises used: not_true_eq_false, ne_eq
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : Eq (α := ℝ≥0) (∑ i ∈ s, w i) 1
assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ assumption_mod_cast₃ :
  ∀ (hw' : Eq (α := ℝ≥0) (∑ i ∈ s, w i) 1), Eq (α := ℝ≥0) (∑ i ∈ s, w i) 1
⊢ Eq (α := ℝ) (∑ i ∈ s, (↑(w i) : ℝ)) 1

Tactic:
assumption_mod_cast
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
w₁ w₂ p₁ p₂ : ℝ≥0
⊢ w₁ + w₂ = 1 → p₁ ^ (↑w₁ : ℝ) * p₂ ^ (↑w₂ : ℝ) ≤ w₁ * p₁ + w₂ * p₂

Tactic:
simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty,
    Finset.univ_eq_empty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one] using
    geom_mean_le_arith_mean_weighted univ ![w₁, w₂] ![p₁, p₂]

Premises used: Finset.prod_empty, Fin.cons_succ, Finset.univ, Finset.univ_eq_empty, Fin.prod_univ_succ, NNReal.geom_mean_le_arith_mean_weighted, Matrix.vecEmpty, Finset.sum_empty, mul_one, add_zero, Matrix.vecCons, Fin.sum_univ_succ, Fin.cons_zero
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
w₁ w₂ w₃ p₁ p₂ p₃ : ℝ≥0
⊢ w₁ + w₂ + w₃ = 1 → p₁ ^ (↑w₁ : ℝ) * p₂ ^ (↑w₂ : ℝ) * p₃ ^ (↑w₃ : ℝ) ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃

Tactic:
simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty,
    Finset.univ_eq_empty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one, ← add_assoc,
    mul_assoc] using geom_mean_le_arith_mean_weighted univ ![w₁, w₂, w₃] ![p₁, p₂, p₃]

Premises used: Finset.prod_empty, Fin.cons_succ, Finset.univ, add_assoc, mul_assoc, Finset.univ_eq_empty, Fin.prod_univ_succ, NNReal.geom_mean_le_arith_mean_weighted, Matrix.vecEmpty, Finset.sum_empty, mul_one, add_zero, Matrix.vecCons, Fin.sum_univ_succ, Fin.cons_zero
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ≥0
⊢ w₁ + w₂ + w₃ + w₄ = 1 →
    p₁ ^ (↑w₁ : ℝ) * p₂ ^ (↑w₂ : ℝ) * p₃ ^ (↑w₃ : ℝ) * p₄ ^ (↑w₄ : ℝ) ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄

Tactic:
simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty,
    Finset.univ_eq_empty, Fin.cons_succ, Fin.cons_zero, add_zero, mul_one, ← add_assoc,
    mul_assoc] using geom_mean_le_arith_mean_weighted univ ![w₁, w₂, w₃, w₄] ![p₁, p₂, p₃, p₄]

Premises used: Finset.prod_empty, Fin.cons_succ, Finset.univ, add_assoc, mul_assoc, Finset.univ_eq_empty, Fin.prod_univ_succ, NNReal.geom_mean_le_arith_mean_weighted, Matrix.vecEmpty, Finset.sum_empty, mul_one, add_zero, Matrix.vecCons, Fin.sum_univ_succ, Fin.cons_zero
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
w₁ w₂ p₁ p₂ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hw : w₁ + w₂ = 1
⊢ (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) w₁ hw₁ + Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) w₂ hw₂) : ℝ) = (↑1 : ℝ)

Tactic:
assumption
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
w₁ w₂ w₃ p₁ p₂ p₃ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hw₃ : 0 ≤ w₃
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hp₃ : 0 ≤ p₃
hw : w₁ + w₂ + w₃ = 1
⊢ p₁ ^ w₁ * p₂ ^ w₂ * p₃ ^ w₃ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃

Tactic:
NNReal.geom_mean_le_arith_mean3_weighted ⟨w₁, hw₁⟩ ⟨w₂, hw₂⟩ ⟨w₃, hw₃⟩ ⟨p₁, hp₁⟩ ⟨p₂, hp₂⟩
      ⟨p₃, hp₃⟩ <|
    NNReal.coe_inj.1 hw

Premises used: Subtype.mk, Iff.mp, NNReal.geom_mean_le_arith_mean3_weighted, NNReal.toReal, NNReal.coe_inj
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hw₃ : 0 ≤ w₃
hw₄ : 0 ≤ w₄
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hp₃ : 0 ≤ p₃
hp₄ : 0 ≤ p₄
hw : w₁ + w₂ + w₃ + w₄ = 1
⊢ (↑(Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) w₁ hw₁ + Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) w₂ hw₂ +
            Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) w₃ hw₃ +
          Subtype.mk (p := fun (r : ℝ) ↦ 0 ≤ r) w₄ hw₄) :
      ℝ) =
    (↑1 : ℝ)

Tactic:
assumption
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
⊢ LE.le (α := ℝ) (∏ i ∈ s, HDiv.hDiv (α := ι → ℝ) 1 z i ^ w i) (∑ i ∈ s, w i * HDiv.hDiv (α := ι → ℝ) 1 z i)

Tactic:
have : ∏ i ∈ s, (1 / z) i ^ w i ≤ ∑ i ∈ s, w i * (1 / z) i :=
    geom_mean_le_arith_mean_weighted s w (1 / z) (fun i hi ↦ le_of_lt (hw i hi)) hw'
    (fun i hi ↦ one_div_nonneg.2 (le_of_lt (hz i hi)))
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
this : LE.le (α := ℝ) (∏ i ∈ s, HDiv.hDiv (α := ι → ℝ) 1 z i ^ w i) (∑ i ∈ s, w i * HDiv.hDiv (α := ι → ℝ) 1 z i)
⊢ LT.lt (α := ℝ) 0 (∏ i ∈ s, (z i)⁻¹ ^ w i)

Tactic:
have p_pos : 0 < ∏ i ∈ s, (z i)⁻¹ ^ w i :=
    prod_pos fun i hi => rpow_pos_of_pos (inv_pos.2 (hz i hi)) _
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
this : LE.le (α := ℝ) (∏ i ∈ s, HDiv.hDiv (α := ι → ℝ) 1 z i ^ w i) (∑ i ∈ s, w i * HDiv.hDiv (α := ι → ℝ) 1 z i)
p_pos : LT.lt (α := ℝ) 0 (∏ i ∈ s, (z i)⁻¹ ^ w i)
⊢ LT.lt (α := ℝ) 0 (∑ i ∈ s, w i * (z i)⁻¹)

Tactic:
have s_pos : 0 < ∑ i ∈ s, w i * (z i)⁻¹ :=
    sum_pos (fun i hi => mul_pos (hw i hi) (inv_pos.2 (hz i hi))) hs
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
this : LE.le (α := ℝ) (∏ i ∈ s, HDiv.hDiv (α := ι → ℝ) 1 z i ^ w i) (∑ i ∈ s, w i * HDiv.hDiv (α := ι → ℝ) 1 z i)
p_pos : LT.lt (α := ℝ) 0 (∏ i ∈ s, (z i)⁻¹ ^ w i)
s_pos : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i * (z i)⁻¹)
⊢ LE.le (α := ℝ) (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹

Tactic:
simp only [Pi.div_apply, Pi.one_apply, one_div, ← inv_le_inv₀ s_pos p_pos] at this

Premises used: Pi.one_apply, Pi.div_apply, one_div, inv_le_inv₀
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
p_pos : LT.lt (α := ℝ) 0 (∏ i ∈ s, (z i)⁻¹ ^ w i)
s_pos : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i * (z i)⁻¹)
this : LE.le (α := ℝ) (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
apply : LE.le (α := ℝ) (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹ (∏ i ∈ s, z i ^ w i)
⊢ LE.le (α := ℝ) (∑ i ∈ s, w i / z i)⁻¹ (∏ i ∈ s, z i ^ w i)

Tactic:
apply le_trans this

Premises used: le_trans
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
p_pos : LT.lt (α := ℝ) 0 (∏ i ∈ s, (z i)⁻¹ ^ w i)
s_pos : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i * (z i)⁻¹)
this : LE.le (α := ℝ) (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
⊢ LT.lt (α := ℝ) 0 (∏ i ∈ s, z i ^ w i)⁻¹

Tactic:
have p_pos₂ : 0 < (∏ i ∈ s, (z i) ^ w i)⁻¹ :=
    inv_pos.2 (prod_pos fun i hi => rpow_pos_of_pos ((hz i hi)) _)
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
p_pos : LT.lt (α := ℝ) 0 (∏ i ∈ s, (z i)⁻¹ ^ w i)
s_pos : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i * (z i)⁻¹)
this : LE.le (α := ℝ) (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : LT.lt (α := ℝ) 0 (∏ i ∈ s, z i ^ w i)⁻¹
rw : LE.le (α := ℝ) (∏ x ∈ s, (z x ^ w x)⁻¹) (∏ i ∈ s, (z i)⁻¹ ^ w i)
⊢ LE.le (α := ℝ) (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹ (∏ i ∈ s, z i ^ w i)

Tactic:
rw [← inv_inv (∏ i ∈ s, z i ^ w i), inv_le_inv₀ p_pos p_pos₂, ← Finset.prod_inv_distrib]

Premises used: Finset.prod_inv_distrib, Finset.prod, HPow.hPow, inv_inv, inv_le_inv₀
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
p_pos : LT.lt (α := ℝ) 0 (∏ i ∈ s, (z i)⁻¹ ^ w i)
s_pos : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i * (z i)⁻¹)
this : LE.le (α := ℝ) (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : LT.lt (α := ℝ) 0 (∏ i ∈ s, z i ^ w i)⁻¹
h0 : ∀ i ∈ s, 0 ≤ (z i ^ w i)⁻¹
h1 : ∀ i ∈ s, (z i ^ w i)⁻¹ ≤ (z i)⁻¹ ^ w i
⊢ LE.le (α := ℝ) (∏ x ∈ s, (z x ^ w x)⁻¹) (∏ i ∈ s, (z i)⁻¹ ^ w i)

Tactic:
gcongr
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
p_pos : LT.lt (α := ℝ) 0 (∏ i ∈ s, (z i)⁻¹ ^ w i)
s_pos : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i * (z i)⁻¹)
this : LE.le (α := ℝ) (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : LT.lt (α := ℝ) 0 (∏ i ∈ s, z i ^ w i)⁻¹
i : ι
hi : i ∈ s
positivity positivity₁ positivity₂ positivity₃ : 0 < z i → 0 ≤ (z i ^ w i)⁻¹
⊢ 0 ≤ (z i ^ w i)⁻¹

Tactic:
positivity [hz i hi]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
p_pos : LT.lt (α := ℝ) 0 (∏ i ∈ s, (z i)⁻¹ ^ w i)
s_pos : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i * (z i)⁻¹)
this : LE.le (α := ℝ) (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : LT.lt (α := ℝ) 0 (∏ i ∈ s, z i ^ w i)⁻¹
⊢ ∀ i ∈ s, 0 ≤ (z i ^ w i)⁻¹

Tactic:
exact fun i hi ↦ by positivity [hz i hi]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
p_pos : LT.lt (α := ℝ) 0 (∏ i ∈ s, (z i)⁻¹ ^ w i)
s_pos : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i * (z i)⁻¹)
this : LE.le (α := ℝ) (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : LT.lt (α := ℝ) 0 (∏ i ∈ s, z i ^ w i)⁻¹
i : ι
h : i ∈ s
h1 : 0 ≤ z i
⊢ (z i ^ w i)⁻¹ ≤ (z i)⁻¹ ^ w i

Tactic:
rw [Real.inv_rpow]

Premises used: Real.inv_rpow
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
p_pos : LT.lt (α := ℝ) 0 (∏ i ∈ s, (z i)⁻¹ ^ w i)
s_pos : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i * (z i)⁻¹)
this : LE.le (α := ℝ) (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : LT.lt (α := ℝ) 0 (∏ i ∈ s, z i ^ w i)⁻¹
i : ι
h h1 : i ∈ s
⊢ 0 ≤ z i

Tactic:
apply fun i hi ↦ le_of_lt (hz i hi)

Premises used: le_of_lt
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hs : s.Nonempty
hw : ∀ i ∈ s, 0 < w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
p_pos : LT.lt (α := ℝ) 0 (∏ i ∈ s, (z i)⁻¹ ^ w i)
s_pos : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i * (z i)⁻¹)
this : LE.le (α := ℝ) (∑ i ∈ s, w i * (z i)⁻¹)⁻¹ (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹
p_pos₂ : LT.lt (α := ℝ) 0 (∏ i ∈ s, z i ^ w i)⁻¹
i : ι
h : i ∈ s
⊢ i ∈ s

Tactic:
assumption
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 < z i
refine_3 :
  ∀
    (this :
      LE.le (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i / z i)⁻¹
        (∏ i ∈ s, HPow.hPow (β := ℝ) (z i) ((fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i))),
    HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i / z i) ≤
      HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹
refine_1 : ∀ i ∈ s, LT.lt (α := ℝ) 0 ((fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i)
refine_2 : Eq (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i) 1
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i / z i) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹

Tactic:
have := harm_mean_le_geom_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z hs ?_ ?_ hz
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 < z i
this :
  LE.le (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i / z i)⁻¹
    (∏ i ∈ s, HPow.hPow (β := ℝ) (z i) ((fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i))
⊢ LE.le (α := ℝ) (∑ x ∈ s, (w x / ∑ i ∈ s, w i) / z x)⁻¹ (∏ x ∈ s, z x ^ (w x / ∑ i ∈ s, w i))

Tactic:
simp only at this
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 < z i
this : LE.le (α := ℝ) (∑ x ∈ s, (w x / ∑ i ∈ s, w i) / z x)⁻¹ (∏ x ∈ s, z x ^ (w x / ∑ i ∈ s, w i))
refine_3 :
  let n : ℝ := ∑ i ∈ s, w i;
  ∀ (hw' : 0 < n) (this : LE.le (α := ℝ) (∑ x ∈ s, w x / n / z x)⁻¹ (∏ x ∈ s, z x ^ (w x / n))),
    n / ∑ i ∈ s, w i / z i ≤ HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i / z i) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹

Tactic:
set n := ∑ i ∈ s, w i