awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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, z j = ∑ i ∈ s, w i * z i) → ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
⊢ (∀ j ∈ s, z j = ∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
have h₁ : (∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x) → ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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, z j = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
⊢ log (z j) = ∑ x ∈ s, log (z x) * w x
have h₁ : Eq (α := ℝ) (∑ i ∈ s, w i * log (z j)) (∑ x ∈ s, log (z x) * w x)
Tactic: rw [← arith_mean_weighted_of_constant s w _ (log (z j)) hw' fun i _ => congrFun rfl]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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, z j = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
⊢ Eq (α := ℝ) (∑ i ∈ s, w i * log (z j)) (∑ x ∈ s, log (z x) * w x)
have h₁ : ∀ x ∈ s, w x * log (z j) = log (z x) * w x
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ z j = ∑ i ∈ s, w i * z i
have h₁ : Eq (α := ℝ) (∑ i ∈ s, w 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]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ Eq (α := ℝ) (∑ i ∈ s, w i * z j) (∑ i ∈ s, w i * z i)
have h₁ : ∀ x ∈ s, w x * z j = w x * z x
Tactic: apply sum_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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
⊢ 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
have h : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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
⊢ 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
have h' : ∀ 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
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ 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
have 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
Tactic: rw [← sum_filter_of_ne h, ← prod_filter_of_ne h', geom_mean_eq_arith_mean_weighted_iff']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ 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
have hw₁ : ∀ i ∈ {x ∈ s | w x ≠ 0}, 0 < w i
Tactic: rw [← sum_filter_of_ne h, ← prod_filter_of_ne h', geom_mean_eq_arith_mean_weighted_iff']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ 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
have hw'₁ : Eq (α := ℝ) (∑ i ∈ s with w i ≠ 0, w i) 1
Tactic: rw [← sum_filter_of_ne h, ← prod_filter_of_ne h', geom_mean_eq_arith_mean_weighted_iff']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ 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
have hz₁ : ∀ i ∈ {x ∈ s | w x ≠ 0}, 0 ≤ z i
Tactic: rw [← sum_filter_of_ne h, ← prod_filter_of_ne h', geom_mean_eq_arith_mean_weighted_iff']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k
have mp : LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) → ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k
have mpr : (∃ j ∈ s, ∃ k ∈ s, z j ≠ z k) → LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
⊢ ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k
have mp : ∀ (h_contra : ∀ (j : ι) (_ : j ∈ s) (k : ι) (_ : k ∈ s), z j = z k), False
Tactic: by_contra! h_contra
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ False
have 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
Tactic: rw [(geom_mean_eq_arith_mean_weighted_iff' s w z hw hw' hz).mpr ?_] at h
Cleared hypotheses: h, h_contra
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ False
have rw : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
Tactic: rw [(geom_mean_eq_arith_mean_weighted_iff' s w z hw hw' hz).mpr ?_] at h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ z j = ∑ i ∈ s, w i * z i
have rw : Eq (α := ℝ) (∑ i ∈ s, w 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]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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
⊢ LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
⊢ LT.lt (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
have mpr : ∀ (h : LE.le (α := ℝ) (∑ i ∈ s, w i * z i) (∏ i ∈ s, z i ^ w i)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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)
⊢ False
have h₁ : Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i)
Tactic: apply le_antisymm this at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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)
⊢ False
have h₁ : ∀ 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : Eq (α := ℝ≥0) (∑ i ∈ s, w i) 1
⊢ Eq (α := ℝ) (∑ i ∈ s, (↑(w i) : ℝ)) 1
have assumption_mod_cast : ∀ (hw' : Eq (α := ℝ≥0) (∑ i ∈ s, w i) 1), Eq (α := ℝ≥0) (∑ i ∈ s, w i) 1
Tactic: assumption_mod_cast
Cleared hypotheses: hw'
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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, w i / z i)⁻¹ (∏ i ∈ s, z i ^ w i)
have this : 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)))
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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)
⊢ LE.le (α := ℝ) (∑ i ∈ s, w i / z i)⁻¹ (∏ i ∈ s, z i ^ w i)
have p_pos : 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)) _
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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)
⊢ LE.le (α := ℝ) (∑ i ∈ s, w i / z i)⁻¹ (∏ i ∈ s, z i ^ w i)
have s_pos : 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
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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)
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)⁻¹
⊢ LE.le (α := ℝ) (∑ i ∈ s, w i / z i)⁻¹ (∏ i ∈ s, z i ^ w i)
have apply : LE.le (α := ℝ) (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹ (∏ i ∈ s, z i ^ w i)
Tactic: apply le_trans this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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)⁻¹
⊢ LE.le (α := ℝ) (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹ (∏ i ∈ s, z i ^ w i)
have p_pos₂ : 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)) _)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)⁻¹
⊢ LE.le (α := ℝ) (∏ i ∈ s, (z i)⁻¹ ^ w i)⁻¹ (∏ i ∈ s, z i ^ w i)
have rw : LE.le (α := ℝ) (∏ x ∈ s, (z x ^ w x)⁻¹) (∏ 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]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)⁻¹
⊢ LE.le (α := ℝ) (∏ x ∈ s, (z x ^ w x)⁻¹) (∏ i ∈ s, (z i)⁻¹ ^ w i)
have h0 : ∀ i ∈ s, 0 ≤ (z i ^ w i)⁻¹
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)⁻¹
⊢ LE.le (α := ℝ) (∏ x ∈ s, (z x ^ w x)⁻¹) (∏ i ∈ s, (z i)⁻¹ ^ w i)
have h1 : ∀ i ∈ s, (z i ^ w i)⁻¹ ≤ (z i)⁻¹ ^ w i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ 0 ≤ (z i ^ w i)⁻¹
have positivity : 0 < z i → 0 ≤ (z i ^ w i)⁻¹
Tactic: positivity [hz i hi]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ (z i ^ w i)⁻¹ ≤ (z i)⁻¹ ^ w i
have h1 : 0 ≤ z i
Tactic: rw [Real.inv_rpow]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i / z i) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹
have 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)⁻¹
Tactic: have := harm_mean_le_geom_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z hs ?_ ?_ hz
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)⁻¹
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i / z i) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹
have refine_1 : ∀ i ∈ s, LT.lt (α := ℝ) 0 ((fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i)
Tactic: have := harm_mean_le_geom_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z hs ?_ ?_ hz
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i / z i) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹
have refine_2 : Eq (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i) 1
Tactic: have := harm_mean_le_geom_mean_weighted s (fun i => (w i) / ∑ i ∈ s, w i) z hs ?_ ?_ hz
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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))
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i / z i) ≤
    HPow.hPow (α := ℝ) (β := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i)⁻¹
have 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⁻¹
Tactic: set n := ∑ i ∈ s, w i
Cleared hypotheses: hw', this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
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⁻¹
have refine_3 : (∑ i ∈ s, n⁻¹ * (w i / z i))⁻¹ ≤ HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹
Tactic: nth_rw 1 [div_eq_mul_inv, (show n = (n⁻¹)⁻¹ by simp), ← mul_inv, Finset.mul_sum _ _ n⁻¹]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
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))
⊢ (∑ i ∈ s, n⁻¹ * (w i / z i))⁻¹ ≤ HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹
have refine_3 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹
Tactic: simp_rw [inv_mul_eq_div n ((w _) / (z _)), div_right_comm _ _ n]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
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))
⊢ (∑ x ∈ s, w x / n / z x)⁻¹ ≤ HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹
have h : HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹ = ∏ x ∈ s, z x ^ (w x / n)
Tactic: convert! this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
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))
i : ι
hi : i ∈ s
⊢ 0 ≤ z i ^ w i
have positivity : 0 < z i → 0 ≤ z i ^ w i
Tactic: positivity [hz i hi]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
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))
⊢ HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹ = ∏ x ∈ s, z x ^ (w x / n)
have h : Eq (α := ℝ) (∏ i ∈ s, (z i ^ w i) ^ n⁻¹) (∏ x ∈ s, z x ^ (w x / n))
Tactic: rw [← Real.finsetProd_rpow s _ (fun i hi ↦ by positivity [hz i hi])]