-- Mathlib/Analysis/MeanInequalities.lean
theorem geom_mean_eq_arith_mean_weighted_iff (w z : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i)
    (hw' : ∑ i ∈ s, w i = 1) (hz : ∀ i ∈ s, 0 ≤ z i) :
    ∏ 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

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ 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 ∈ 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']

Result:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ 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 ∈ filter (fun x => w x ≠ 0) s, z j = ∑ i ∈ filter (fun x => w x ≠ 0) s, w i * z i) ↔
    ∀ j ∈ s, w j ≠ 0 → z j = ∑ x ∈ filter (fun x => w x ≠ 0) s, w x * z x

case hw
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ 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 ∈ filter (fun x => w x ≠ 0) s, 0 < w i

case hw'
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ 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 ∈ filter (fun x => w x ≠ 0) s, w i = 1

case hz
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ 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 ∈ filter (fun x => w x ≠ 0) s, 0 ≤ z i

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
⊢ ∏ 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:
have h (i) (_ : i ∈ s) : w i * z i ≠ 0 → w i ≠ 0 := by apply left_ne_zero_of_mul

Result:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ 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 = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, w j ≠ 0 → z j = ∑ i ∈ s, w i * z i

Proof state:
case hw
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ 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 ∈ filter (fun x => w x ≠ 0) s, 0 < w i

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

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
i : ι
x✝ : i ∈ s
⊢ w i * z i ≠ 0 → w i ≠ 0

Tactic:
apply left_ne_zero_of_mul

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ 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 ∈ filter (fun x => w x ≠ 0) s, z j = ∑ i ∈ filter (fun x => w x ≠ 0) s, w i * z i) ↔
    ∀ j ∈ s, w j ≠ 0 → z j = ∑ x ∈ filter (fun x => w x ≠ 0) s, w x * z x

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ 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 = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, w j ≠ 0 → z j = ∑ i ∈ s, w i * z i

Tactic:
have h' (i) (_ : i ∈ s) : z i ^ w i ≠ 1 → w i ≠ 0 := by
  by_contra!
  obtain ⟨h1, h2⟩ := this
  simp only [h2, rpow_zero, ne_self_iff_false] at h1

Result:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ 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 ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, w j ≠ 0 → z j = ∑ i ∈ s, w i * z i

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0
i : ι
x✝ : i ∈ s
this : z i ^ w i ≠ 1 ∧ w i = 0
⊢ False

Tactic:
obtain ⟨h1, h2⟩ := this

Result:
case intro
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0
i : ι
x✝ : i ∈ s
h1 : z i ^ w i ≠ 1
h2 : w i = 0
⊢ False

Proof state:
case hw'
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ 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 ∈ filter (fun x => w x ≠ 0) s, w i = 1

Tactic:
rwa [sum_filter_ne_zero]

Result:
no goals

Proof state:
case intro
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0
i : ι
x✝ : 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

Result:
no goals

Proof state:
case hz
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ 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 ∈ filter (fun x => w x ≠ 0) s, 0 ≤ z i

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

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0
i : ι
x✝ : i ∈ s
⊢ z i ^ w i ≠ 1 → w i ≠ 0

Tactic:
by_contra!

Result:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
h : ∀ i ∈ s, w i * z i ≠ 0 → w i ≠ 0
i : ι
x✝ : i ∈ s
this : z i ^ w i ≠ 1 ∧ w i = 0
⊢ False