-- Mathlib/Analysis/MeanInequalities.lean
theorem geom_mean_lt_arith_mean_weighted_iff_of_pos (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, ∃ k ∈ s, z j ≠ z k

Proof state:
case mp
ι : 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, ∃ k ∈ s, z j ≠ z k

Tactic:
intro h

Result:
case mp
ι : 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, z i ^ w i < ∑ i ∈ s, w i * z i
⊢ ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k

Proof state:
case mpr.intro.intro.intro.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
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
this : ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i
h : ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i
⊢ False

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

Result:
case mpr.intro.intro.intro.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
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
this : ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
⊢ False

Proof state:
case mpr.intro.intro.intro.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
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
⊢ ∏ 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

Result:
case mpr.intro.intro.intro.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
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
this : ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i
⊢ ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i

Proof state:
case mpr.intro.intro.intro.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
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
this : ∏ 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

Result:
no goals

Proof state:
case mpr.intro.intro.intro.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
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
this : ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i
h : ∑ i ∈ s, w i * z i ≤ ∏ i ∈ s, z i ^ w i
⊢ False

Tactic:
apply le_antisymm this at h

Result:
case mpr.intro.intro.intro.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
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
this : ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i
h : ∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i
⊢ False

Proof state:
case mp
ι : 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 < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ False

Tactic:
exact (lt_self_iff_false _).mp h

Result:
no goals

Proof state:
case mp
ι : 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, z i ^ w i < ∑ i ∈ s, w i * z i
⊢ ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k

Tactic:
by_contra! h_contra

Result:
case mp
ι : 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, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ False

Proof state:
case mpr.intro.intro.intro.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
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
this : ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i
⊢ ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i

Tactic:
by_contra! h

Result:
case mpr.intro.intro.intro.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
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
this : ∏ i ∈ s, z i ^ w i ≤ ∑ i ∈ s, w i * z i
h : ∑ i ∈ s, w i * z i ≤ ∏ i ∈ s, z i ^ w i
⊢ False

Proof state:
case mpr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
⊢ (∃ j ∈ s, ∃ k ∈ s, z j ≠ z k) → ∏ i ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i

Tactic:
rintro ⟨j, hjs, k, hks, hzjk⟩

Result:
case mpr.intro.intro.intro.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
j : ι
hjs : j ∈ s
k : ι
hks : k ∈ s
hzjk : z j ≠ z k
⊢ ∏ i ∈ s, z i ^ w i < ∑ 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, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
j : ι
hjs : j ∈ s
⊢ ∑ 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))

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 ∈ s, z i ^ w i < ∑ i ∈ s, w i * z i ↔ ∃ j ∈ s, ∃ k ∈ s, z j ≠ z k

Tactic:
constructor

Result:
case mp
ι : 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, ∃ k ∈ s, z j ≠ z k

case mpr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : ∑ i ∈ s, w i = 1
hz : ∀ i ∈ s, 0 ≤ z i
⊢ (∃ j ∈ s, ∃ k ∈ s, z j ≠ z k) → ∏ i ∈ s, z i ^ w i < ∑ 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, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
intro j hjs

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, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
j : ι
hjs : j ∈ s
⊢ z j = ∑ i ∈ s, w i * z i

Proof state:
case mp
ι : 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, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ 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

Result:
case mp
ι : 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 < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ False

ι : 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, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
⊢ ∀ j ∈ s, 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, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
j : ι
hjs : j ∈ s
⊢ 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]

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, z i ^ w i < ∑ i ∈ s, w i * z i
h_contra : ∀ j ∈ s, ∀ k ∈ s, z j = z k
j : ι
hjs : j ∈ s
⊢ ∑ i ∈ s, w i * z j = ∑ i ∈ s, w i * z i