-- Mathlib/Analysis/MeanInequalities.lean
theorem harm_mean_le_geom_mean {ι : Type*} (s : Finset ι) (hs : s.Nonempty) (w : ι → ℝ)
    (z : ι → ℝ) (hw : ∀ i ∈ s, 0 < w i) (hw' : 0 < ∑ i ∈ s, w i) (hz : ∀ i ∈ s, 0 < z i) :
    (∑ i ∈ s, w i) / (∑ i ∈ s, w i / z i) ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹

Proof state:
case h.e'_4
ι : 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 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / n)
⊢ ∏ i ∈ s, (z i ^ w i) ^ n⁻¹ = ∏ x ∈ s, z x ^ (w x / n)

Tactic:
refine Finset.prod_congr rfl (fun i hi => ?_)

Result:
case h.e'_4
ι : 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 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / n)
i : ι
hi : i ∈ s
⊢ (z i ^ w i) ^ n⁻¹ = z i ^ (w i / n)

Proof state:
case refine_2
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ ∑ i ∈ s, (fun i => w i / ∑ i ∈ s, w i) i = 1

Tactic:
simp_rw [div_eq_mul_inv (w _) (∑ i ∈ s, w i), ← Finset.sum_mul _ _ (∑ i ∈ s, w i)⁻¹]

Result:
case refine_2
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ (∑ i ∈ s, w i) * (∑ i ∈ s, w i)⁻¹ = 1

Proof state:
case refine_2
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ (∑ i ∈ s, w i) * (∑ i ∈ s, w i)⁻¹ = 1

Tactic:
exact mul_inv_cancel₀ hw'.ne'

Result:
no goals

Proof state:
case h.e'_4
ι : 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 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / n)
⊢ (∏ i ∈ s, z i ^ w i) ^ n⁻¹ = ∏ x ∈ s, z x ^ (w x / n)

Tactic:
rw [← Real.finset_prod_rpow s _ (fun i hi ↦ Real.rpow_nonneg (le_of_lt <| hz i hi) _)]

Result:
case h.e'_4
ι : 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 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / n)
⊢ ∏ i ∈ s, (z i ^ w i) ^ n⁻¹ = ∏ x ∈ s, z x ^ (w x / n)

Proof state:
ι : 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 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / n)
⊢ n = n⁻¹⁻¹

Tactic:
norm_num

Result:
no goals

Proof state:
case h.e'_4
ι : 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 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / n)
i : ι
hi : i ∈ s
⊢ (z i ^ w i) ^ n⁻¹ = z i ^ (w i / n)

Tactic:
rw [← Real.rpow_mul (le_of_lt <| hz i hi) (w _) n⁻¹, div_eq_mul_inv (w _) n]

Result:
no goals

Proof state:
case refine_3
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
this : (∑ i ∈ s, (fun i => w i / ∑ i ∈ s, w i) i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (fun i => w i / ∑ i ∈ s, w i) i
⊢ (∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹

Tactic:
simp only at this

Result:
case refine_3
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
this : (∑ x ∈ s, (w x / ∑ i ∈ s, w i) / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / ∑ i ∈ s, w i)
⊢ (∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹

Proof state:
case refine_3
ι : 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 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / n)
⊢ n / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ n⁻¹

Tactic:
nth_rw 1 [div_eq_mul_inv, (show n = (n⁻¹)⁻¹ by norm_num), ← mul_inv, Finset.mul_sum _ _ n⁻¹]

Result:
case refine_3
ι : 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 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / n)
⊢ (∑ i ∈ s, n⁻¹ * (w i / z i))⁻¹ ≤ (∏ i ∈ s, z i ^ w i) ^ n⁻¹

Proof state:
case refine_3
ι : 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 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / n)
⊢ (∑ x ∈ s, w x / n / z x)⁻¹ ≤ (∏ i ∈ s, z i ^ w i) ^ n⁻¹

Tactic:
convert this

Result:
case h.e'_4
ι : 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 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / n)
⊢ (∏ i ∈ s, z i ^ w i) ^ n⁻¹ = ∏ x ∈ s, z x ^ (w x / n)

Proof state:
case refine_3
ι : 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 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / n)
⊢ (∑ i ∈ s, n⁻¹ * (w i / z i))⁻¹ ≤ (∏ i ∈ s, z i ^ w i) ^ n⁻¹

Tactic:
simp_rw [inv_mul_eq_div n ((w _)/(z _)), div_right_comm _ _ n]

Result:
case refine_3
ι : 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 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / n)
⊢ (∑ x ∈ s, w x / n / z x)⁻¹ ≤ (∏ i ∈ s, z i ^ w i) ^ n⁻¹

Proof state:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ (∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ 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

Result:
case refine_3
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
this : (∑ i ∈ s, (fun i => w i / ∑ i ∈ s, w i) i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (fun i => w i / ∑ i ∈ s, w i) i
⊢ (∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹

case refine_1
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ ∀ i ∈ s, 0 < (fun i => w i / ∑ i ∈ s, w i) i

case refine_2
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ ∑ i ∈ s, (fun i => w i / ∑ i ∈ s, w i) i = 1

Proof state:
case refine_3
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
this : (∑ x ∈ s, (w x / ∑ i ∈ s, w i) / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / ∑ i ∈ s, w i)
⊢ (∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹

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

Result:
case refine_3
ι : 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 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ ∏ x ∈ s, z x ^ (w x / n)
⊢ n / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ n⁻¹

Proof state:
case refine_1
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : 0 < ∑ i ∈ s, w i
hz : ∀ i ∈ s, 0 < z i
⊢ ∀ i ∈ s, 0 < (fun i => w i / ∑ i ∈ s, w i) i

Tactic:
exact fun i hi ↦ div_pos (hw i hi) hw'

Result:
no goals