awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∏ i ∈ s, x ^ w i)

Tactic:
prod_congr rfl fun i hi => ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
refine : ∀ (i : ι) (hi : i ∈ s), z i ^ w i = x ^ w i
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∏ i ∈ s, x ^ w i)

Tactic:
refine prod_congr rfl fun i hi => ?_

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
inl : ∀ (h₀ : w i = 0), z i ^ w i = x ^ w i
inr : ∀ (h₀ : w i ≠ 0), z i ^ w i = x ^ w i
⊢ z i ^ w i = x ^ w i

Tactic:
rcases eq_or_ne (w i) 0 with h₀ | h₀

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
h₀ : w i = 0
inl : HPow.hPow (β := ℝ) (z i) 0 = HPow.hPow (β := ℝ) x 0
inl₁ : 1 = HPow.hPow (β := ℝ) x 0
inl₂ inl₃ : Eq (α := ℝ) 1 1
⊢ z i ^ w i = x ^ w i

Tactic:
rw [h₀, rpow_zero, rpow_zero]

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

Tactic:
rw [hx i hi h₀]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
rw : 0 ≤ x
⊢ ∏ i ∈ s, x ^ w i = x

Tactic:
rw [← rpow_sum_of_nonneg _ hw, hw', rpow_one]

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

Tactic:
rw [hw']
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
⊢ Ne (α := ℝ) 1 0

Tactic:
one_ne_zero

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

Tactic:
exact one_ne_zero

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

Tactic:
have : (∑ i ∈ s, w i) ≠ 0 := by
        rw [hw']
        exact one_ne_zero
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
this : Ne (α := ℝ) (∑ i ∈ s, w i) 0
obtain : ∀ (i : ι) (his : i ∈ s) (hi : w i ≠ 0), 0 ≤ x
⊢ 0 ≤ x

Tactic:
obtain ⟨i, his, hi⟩ := exists_ne_zero_of_sum_ne_zero this

Premises used: Finset.exists_ne_zero_of_sum_ne_zero
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
this : Ne (α := ℝ) (∑ i ∈ s, w i) 0
i : ι
his : i ∈ s
hi : w i ≠ 0
rw : 0 ≤ z i
⊢ 0 ≤ x

Tactic:
rw [← hx i his hi]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
this : Ne (α := ℝ) (∑ i ∈ s, w i) 0
i : ι
his : i ∈ s
hi : w i ≠ 0
⊢ 0 ≤ z i

Tactic:
hz i his
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
this : Ne (α := ℝ) (∑ i ∈ s, w i) 0
i : ι
his : i ∈ s
hi : w i ≠ 0
⊢ 0 ≤ z i

Tactic:
exact hz i his
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
⊢ Eq (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i * x)

Tactic:
sum_congr rfl fun i hi => ?_

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

Tactic:
refine sum_congr rfl fun i hi => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
inl : ∀ (hwi : w i = 0), w i * z i = w i * x
inr : ∀ (hwi : w i ≠ 0), w i * z i = w i * x
⊢ w i * z i = w i * x

Tactic:
rcases eq_or_ne (w i) 0 with hwi | hwi

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i = 0
inl : 0 * z i = 0 * x
inl₁ : 0 = 0 * x
inl₂ inl₃ : Eq (α := ℝ) 0 0
⊢ w i * z i = w i * x

Tactic:
rw [hwi, zero_mul, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i ≠ 0
inr inr₁ : w i * x = w i * x
⊢ w i * z i = w i * x

Tactic:
rw [hx i hi hwi]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hx : ∀ i ∈ s, w i ≠ 0 → z i = x
rw : (∑ i ∈ s, w i) * x = x
rw₁ : 1 * x = x
rw₂ rw₃ : x = x
⊢ ∑ i ∈ s, w i * x = x

Tactic:
rw [← sum_mul, hw', one_mul]

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

Tactic:
rw [geom_mean_weighted_of_constant, arith_mean_weighted_of_constant]

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

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

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

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

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

Tactic:
assumption
-- 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
pos :
  ∀ (A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0),
    Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
neg :
  ∀ (A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0),
    Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
by_cases! A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0
-- 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 ∈ s, z i = 0 ∧ w i ≠ 0
pos :
  ∀ (i : ι) (his : i ∈ s) (hzi : z i = 0) (hwi : w i ≠ 0),
    Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
rcases A with ⟨i, his, hzi, hwi⟩
-- 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 : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
pos : Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
pos₁ : z i ^ w i = 0
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
rw [prod_eq_zero his]

Premises used: Finset.prod_eq_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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
pos : Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i) → ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
pos₁ : (∀ j ∈ s, z j = ∑ i ∈ s, w i * z i) → Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i)
⊢ Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
h : Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i)
pos : ∀ j ∈ s, z j = 0
⊢ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
rw [← 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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
h : Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i)
j : ι
hj : j ∈ s
pos : w j * z j = 0
⊢ z j = 0

Tactic:
apply eq_zero_of_ne_zero_of_mul_left_eq_zero (ne_of_lt (hw j hj)).symm

Premises used: Ne.symm, eq_zero_of_ne_zero_of_mul_left_eq_zero, ne_of_lt
-- 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 : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
h : Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i)
j : ι
hj : j ∈ s
apply : ∀ i ∈ s, 0 ≤ w i * z i
⊢ w j * z j = 0

Tactic:
apply (sum_eq_zero_iff_of_nonneg ?_).mp h.symm j hj

Premises used: Finset.sum_eq_zero_iff_of_nonneg, Iff.mp, Eq.symm
-- 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 : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
h : Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i)
j : ι
hj : j ∈ s
⊢ ∀ i ∈ s, 0 ≤ w i * z i

Tactic:
fun i hi => (mul_nonneg_iff_of_pos_left (hw i hi)).mpr (hz i hi)

Premises used: Iff.mpr, mul_nonneg_iff_of_pos_left
-- 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 : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
h : Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i)
j : ι
hj : j ∈ s
⊢ ∀ i ∈ s, 0 ≤ w i * z i

Tactic:
exact fun i hi => (mul_nonneg_iff_of_pos_left (hw i hi)).mpr (hz i hi)

Premises used: Iff.mpr, mul_nonneg_iff_of_pos_left
-- 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 : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
⊢ z i = ∑ i ∈ s, w i * z i

Tactic:
h i his
-- 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 : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
h₁ : 0 = z i
⊢ Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i)

Tactic:
convert! h i his
-- 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 : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
⊢ 0 = z i

Tactic:
hzi.symm

Premises used: Eq.symm
-- 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 : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
⊢ 0 = z i

Tactic:
exact hzi.symm

Premises used: Eq.symm
-- 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 : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
pos : HPow.hPow (α := ℝ) 0 (w i) = 0
⊢ z i ^ w i = 0

Tactic:
rw [hzi]
-- 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 : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ HPow.hPow (α := ℝ) 0 (w i) = 0

Tactic:
zero_rpow hwi

Premises used: Real.zero_rpow
-- 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 : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ HPow.hPow (α := ℝ) 0 (w i) = 0

Tactic:
exact zero_rpow hwi

Premises used: Real.zero_rpow
-- 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
⊢ ∀ (i : ι) (h : i ∈ s), 0 < z i

Tactic:
have hz' := fun i h => lt_of_le_of_ne (hz i h) (fun a => (ne_of_gt (hw i h)) (A i h a.symm))
-- 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
⊢ rexp (∑ i ∈ s, w i • log (z i)) = ∑ i ∈ s, w i • rexp (log (z i)) ↔ ∀ j ∈ s, log (z j) = ∑ i ∈ s, w i • log (z i)

Tactic:
have := strictConvexOn_exp.map_sum_eq_iff hw hw' fun i _ => Set.mem_univ <| log (z i)
-- 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 : rexp (∑ i ∈ s, w i • log (z i)) = ∑ i ∈ s, w i • rexp (log (z i)) ↔ ∀ j ∈ s, log (z j) = ∑ i ∈ s, w i • log (z i)
⊢ 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

Tactic:
simp only [exp_sum, smul_eq_mul, mul_comm (w _) (log _)] at this

Premises used: Real.log, mul_comm, smul_eq_mul, Real.exp_sum
-- 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
⊢ 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

Tactic:
this
-- 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 :
  Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔
    Eq (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))
h₁ : (∀ j ∈ s, z j = ∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i

Tactic:
convert! this using 1
-- 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 : Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∏ x ∈ s, rexp (log (z x) * w x))
h₁ : Eq (α := ℝ) (∑ i ∈ s, w i * z i) (∑ x ∈ s, w x * rexp (log (z x)))
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔
    Eq (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))

Tactic:
apply Eq.congr

Premises used: Eq.congr
-- 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 : ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w x)
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∏ x ∈ s, rexp (log (z x) * w x))

Tactic:
apply prod_congr rfl

Premises used: Finset.prod_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 : ∀ x ∈ s, w x * z x = w x * rexp (log (z x))
⊢ Eq (α := ℝ) (∑ i ∈ s, w i * z i) (∑ x ∈ s, w x * rexp (log (z x)))

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 : ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w x)
h₁ : ∀ x ∈ s, w x * z x = w x * rexp (log (z x))
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔
    Eq (α := ℝ) (∏ x ∈ s, rexp (log (z x) * w x)) (∑ x ∈ s, w x * rexp (log (z x)))

Tactic:
apply Eq.congr <;>
      [apply prod_congr rfl; apply sum_congr rfl]

Premises used: Finset.prod_congr, Eq.congr, 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
i : ι
hi : i ∈ s
⊢ z i ^ w i = rexp (log (z i) * w i)

Tactic:
simp only [exp_mul, exp_log (hz' i hi)]

Premises used: Real.exp_mul, Real.exp_log
-- 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
i : ι
hi : i ∈ s
⊢ w i * z i = w i * rexp (log (z i))

Tactic:
simp only [exp_mul, exp_log (hz' i hi)]

Premises used: Real.exp_mul, Real.exp_log
-- 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, z j = ∑ i ∈ s, w i * z i) → ∀ 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 ∈ s, z j = ∑ i ∈ s, w i * z i
⊢ (∀ j ∈ s, z j = ∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x

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
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
h₁ : Eq (α := ℝ) (∑ i ∈ s, w i * log (z j)) (∑ x ∈ s, log (z x) * w x)
⊢ 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]

Premises used: Real.arith_mean_weighted_of_constant, Real.log, 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, z j = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
h₁ : ∀ x ∈ s, w x * log (z j) = log (z x) * w x
⊢ Eq (α := ℝ) (∑ i ∈ s, w i * log (z j)) (∑ x ∈ s, log (z x) * w x)

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, z j = ∑ i ∈ s, w i * z i
j : ι
hj : j ∈ s
x : ι
hx : x ∈ s
⊢ w x * log (z j) = log (z x) * w x

Tactic:
simp only [mul_comm, h j hj, h x hx]

Premises used: mul_comm