awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
h : HMul.hMul (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)⁻¹ = ∑ x ∈ s, w x * (∑ i ∈ s, w i)⁻¹ * z x
h₁ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)⁻¹ = ∑ x ∈ s, w x * ((∑ i ∈ s, w i)⁻¹ * z x)
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i) = ∑ i ∈ s, (w i / ∑ i ∈ s, w i) * z i
have h₂ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i)⁻¹ (∑ i ∈ s, w i * z i) = ∑ x ∈ s, w x * (z x * (∑ i ∈ s, w i)⁻¹)
Tactic: simp_rw [div_eq_mul_inv, mul_assoc, mul_comm, ← mul_assoc, ← Finset.sum_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
h : HMul.hMul (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)⁻¹ = ∑ x ∈ s, w x * (∑ i ∈ s, w i)⁻¹ * z x
h₁ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)⁻¹ = ∑ x ∈ s, w x * ((∑ i ∈ s, w i)⁻¹ * z x)
h₂ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i)⁻¹ (∑ i ∈ s, w i * z i) = ∑ x ∈ s, w x * (z x * (∑ i ∈ s, w i)⁻¹)
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i) = ∑ i ∈ s, (w i / ∑ i ∈ s, w i) * z i
have h₃ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i)⁻¹ (∑ i ∈ s, w i * z i) = ∑ x ∈ s, w x * z x * (∑ i ∈ s, w i)⁻¹
Tactic: simp_rw [div_eq_mul_inv, mul_assoc, mul_comm, ← mul_assoc, ← Finset.sum_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
h : HMul.hMul (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)⁻¹ = ∑ x ∈ s, w x * (∑ i ∈ s, w i)⁻¹ * z x
h₁ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)⁻¹ = ∑ x ∈ s, w x * ((∑ i ∈ s, w i)⁻¹ * z x)
h₂ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i)⁻¹ (∑ i ∈ s, w i * z i) = ∑ x ∈ s, w x * (z x * (∑ i ∈ s, w i)⁻¹)
h₃ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i)⁻¹ (∑ i ∈ s, w i * z i) = ∑ x ∈ s, w x * z x * (∑ i ∈ s, w i)⁻¹
⊢ HDiv.hDiv (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i) = ∑ i ∈ s, (w i / ∑ i ∈ s, w i) * z i
have h₄ : HMul.hMul (α := ℝ) (∑ i ∈ s, w i)⁻¹ (∑ i ∈ s, w i * z i) = HMul.hMul (α := ℝ) (∑ i ∈ s, w i * z i) (∑ i ∈ s, w i)⁻¹
Tactic: simp_rw [div_eq_mul_inv, mul_assoc, mul_comm, ← mul_assoc, ← Finset.sum_mul, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
⊢ Eq (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i) 1
have convert_2 : HMul.hMul (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i)⁻¹ = 1
Tactic: simp_rw [div_eq_mul_inv, ← Finset.sum_mul]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 ≤ z i
⊢ Ne (α := ℝ) (∑ i ∈ s, w i) 0
have linarith : Eq (α := ℝ) (∑ i ∈ s, w i) 0 → HSub.hSub (α := ℝ) 0 (∑ i ∈ s, w i) + HSub.hSub (α := ℝ) (∑ i ∈ s, w i) 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
have refine : ∀ (i : ι) (hi : i ∈ s), z i ^ w i = x ^ w i
Tactic: refine prod_congr rfl fun i hi => ?_
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ z i ^ w i = x ^ w i
have inl : ∀ (h₀ : w i = 0), z i ^ w i = x ^ w i
Tactic: rcases eq_or_ne (w i) 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ z i ^ w i = x ^ w i
have inr : ∀ (h₀ : w i ≠ 0), z i ^ w i = x ^ w i
Tactic: rcases eq_or_ne (w i) 0 with h₀ | h₀
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ z i ^ w i = x ^ w i
have inl : HPow.hPow (β := ℝ) (z i) 0 = HPow.hPow (β := ℝ) x 0
Tactic: rw [h₀, rpow_zero, rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ z i ^ w i = x ^ w i
have inl₁ : 1 = HPow.hPow (β := ℝ) x 0
Tactic: rw [h₀, rpow_zero, rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ z i ^ w i = x ^ w i
have inl₂ : Eq (α := ℝ) 1 1
Tactic: rw [h₀, rpow_zero, rpow_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ z i ^ w i = x ^ w i
have inr : x ^ w i = x ^ w i
Tactic: rw [hx i hi h₀]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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, x ^ w i = x
have rw : 0 ≤ x
Tactic: rw [← rpow_sum_of_nonneg _ hw, hw', rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
have rw : Ne (α := ℝ) 1 0
Tactic: rw [hw']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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
⊢ 0 ≤ x
have this : Ne (α := ℝ) (∑ i ∈ s, w i) 0
Tactic: have : (∑ i ∈ s, w i) ≠ 0 := by
        rw [hw']
        exact one_ne_zero
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ 0 ≤ x
have obtain : ∀ (i : ι) (his : i ∈ s) (hi : w i ≠ 0), 0 ≤ x
Tactic: obtain ⟨i, his, hi⟩ := exists_ne_zero_of_sum_ne_zero this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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 ≤ x
have rw : 0 ≤ z i
Tactic: rw [← hx i his hi]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
have refine : ∀ (i : ι) (hi : i ∈ s), w i * z i = w i * x
Tactic: refine sum_congr rfl fun i hi => ?_
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ w i * z i = w i * x
have inl : ∀ (hwi : w i = 0), w i * z i = w i * x
Tactic: rcases eq_or_ne (w i) 0 with hwi | hwi
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ w i * z i = w i * x
have inr : ∀ (hwi : w i ≠ 0), w i * z i = w i * x
Tactic: rcases eq_or_ne (w i) 0 with hwi | hwi
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ w i * z i = w i * x
have inl : 0 * z i = 0 * x
Tactic: rw [hwi, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ w i * z i = w i * x
have inl₁ : 0 = 0 * x
Tactic: rw [hwi, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ w i * z i = w i * x
have inl₂ : Eq (α := ℝ) 0 0
Tactic: rw [hwi, zero_mul, zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ w i * z i = w i * x
have inr : w i * x = w i * x
Tactic: rw [hx i hi hwi]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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 ∈ s, w i * x = x
have rw : (∑ i ∈ s, w i) * x = x
Tactic: rw [← sum_mul, hw', one_mul]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ ∑ i ∈ s, w i * x = x
have rw₁ : 1 * x = x
Tactic: rw [← sum_mul, hw', one_mul]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ ∑ i ∈ s, w i * x = x
have rw₂ : x = x
Tactic: rw [← sum_mul, hw', one_mul]
-- 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
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
have 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
Tactic: by_cases! A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0
-- 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
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
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
have 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
Tactic: by_cases! A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0
-- 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 ∈ 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
have 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
Tactic: rcases A with ⟨i, his, hzi, hwi⟩
Cleared hypotheses: A
-- 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
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
have pos : Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
Tactic: rw [prod_eq_zero his]
-- 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
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
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
have pos₁ : z i ^ w i = 0
Tactic: rw [prod_eq_zero his]
-- 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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
have pos : Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i) → ∀ 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
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
⊢ Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
have pos₁ : (∀ j ∈ s, z j = ∑ i ∈ s, w i * z i) → Eq (α := ℝ) 0 (∑ 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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
h : Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i)
⊢ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
have pos : ∀ j ∈ s, z j = 0
Tactic: rw [← 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
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
⊢ z j = 0
have pos : w j * z j = 0
Tactic: apply eq_zero_of_ne_zero_of_mul_left_eq_zero (ne_of_lt (hw j hj)).symm
-- 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
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
⊢ w j * z j = 0
have apply : ∀ i ∈ s, 0 ≤ w i * z i
Tactic: apply (sum_eq_zero_iff_of_nonneg ?_).mp h.symm j hj
-- 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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
h : ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
⊢ Eq (α := ℝ) 0 (∑ i ∈ s, w i * z i)
have h₁ : 0 = z i
Tactic: convert! h i his
-- 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
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ z i ^ w i = 0
have pos : HPow.hPow (α := ℝ) 0 (w i) = 0
Tactic: rw [hzi]
-- 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
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
have hz' : ∀ (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))
-- 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
A : ∀ (i : ι) (_ : i ∈ s) (_ : z i = 0), w i = 0
hz' : ∀ (i : ι) (h : i ∈ s), 0 < 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
have 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)
Tactic: have := strictConvexOn_exp.map_sum_eq_iff hw hw' fun i _ => Set.mem_univ <| log (z i)
-- 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
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 (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
have 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
Tactic: simp only [exp_sum, smul_eq_mul, mul_comm (w _) (log _)] at this
Cleared hypotheses: this
-- 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
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
have 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)))
Tactic: convert! this using 1
-- 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 :
  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)))
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, z j = ∑ i ∈ s, w i * z i
have h₁ : (∀ j ∈ s, z j = ∑ i ∈ s, w i * z i) ↔ ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
Tactic: convert! this using 1
-- 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
⊢ 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)))
have h : Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∏ x ∈ s, rexp (log (z x) * w x))
Tactic: apply Eq.congr
-- 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 : Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∏ x ∈ s, rexp (log (z x) * w 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)))
have h₁ : Eq (α := ℝ) (∑ i ∈ s, w i * z i) (∑ x ∈ s, w x * rexp (log (z x)))
Tactic: apply Eq.congr
-- 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
⊢ Eq (α := ℝ) (∏ i ∈ s, z i ^ w i) (∏ x ∈ s, rexp (log (z x) * w x))
have h : ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w x)
Tactic: apply prod_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
⊢ Eq (α := ℝ) (∑ i ∈ s, w i * z i) (∑ x ∈ s, w x * rexp (log (z x)))
have h : ∀ x ∈ s, w x * z x = w x * rexp (log (z 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
⊢ 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)))
have h : ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w x)
Tactic: apply Eq.congr <;>
      [apply prod_congr rfl; 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 : ∀ x ∈ s, z x ^ w x = rexp (log (z x) * w 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)))
have h₁ : ∀ x ∈ s, w x * z x = w x * rexp (log (z x))
Tactic: apply Eq.congr <;>
      [apply prod_congr rfl; 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
⊢ (∀ 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, z j = ∑ i ∈ s, w i * z i) → ∀ j ∈ s, log (z j) = ∑ x ∈ s, log (z x) * w x
Tactic: constructor