awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
h₁ : ∀ (j : ι) (hj : j ∈ s \ {i}), g j ≤ f j
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i
have h₂ : ∀ (j : ι) (hj : j ∈ s \ {i}), h j ≤ f j
Tactic: gcongr with j hj j hj
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
⊢ HAdd.hAdd (α := R) (∏ i ∈ s, g i) (∏ i ∈ s, h i) ≤ ∏ i ∈ s, f i
have simp_rw : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i
Tactic: classical
  simp_rw [prod_eq_mul_prod_diff_singleton_of_mem hi]
  grw [← h2i, right_distrib]
  gcongr with j hj j hj <;> simp_all
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
f g h : ι → R
s : Finset ι
i : ι
hi : i ∈ s
h2i : g i + h i ≤ f i
hgf : ∀ j ∈ s, j ≠ i → g j ≤ f j
hhf : ∀ j ∈ s, j ≠ i → h j ≤ f j
simp_rw : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i
⊢ HAdd.hAdd (α := R) (∏ i ∈ s, g i) (∏ i ∈ s, h i) ≤ ∏ i ∈ s, f i
have simp_rw₁ : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ g i * ∏ i ∈ s \ {i}, f i + h i * ∏ i ∈ s \ {i}, f i
Tactic: classical
  simp_rw [prod_eq_mul_prod_diff_singleton_of_mem hi]
  grw [← h2i, right_distrib]
  gcongr with j hj j hj <;> simp_all
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have inl : ∀ (h : Eq.{u_2 + 1} (α := R) (∑ i ∈ s, g i) 0),
  HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
Tactic: obtain h | h := (sum_nonneg hg).eq_or_lt'
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
inl :
  ∀ (h : Eq.{u_2 + 1} (α := R) (∑ i ∈ s, g i) 0),
    HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have inr : ∀ (h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)),
  HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
Tactic: obtain h | h := (sum_nonneg hg).eq_or_lt'
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : Eq.{u_2 + 1} (α := R) (∑ i ∈ s, g i) 0
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have ht' : Eq.{u_2 + 1} (α := R) (∑ i ∈ s, r i) 0
Tactic: have ht' : ∑ i ∈ s, r i = 0 := sum_eq_zero fun i hi ↦ by
      simpa [(sum_eq_zero_iff_of_nonneg hg).1 h i hi] using ht i hi
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : Eq.{u_2 + 1} (α := R) (∑ i ∈ s, g i) 0
ht' : Eq.{u_2 + 1} (α := R) (∑ i ∈ s, r i) 0
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have inl : HPow.hPow (α := R) (β := ℕ) 0 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) 0
Tactic: rw [h, ht']
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤ HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have inr : (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
    (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤
  (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
    (∑ i ∈ s, g i) * HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
Tactic: refine le_of_mul_le_mul_of_pos_left
      (le_of_add_le_add_left (a := (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2) ?_) h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
⊢ (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 =
    ∑ i ∈ s, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j
have simp_rw : (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
    (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 =
  2 * ((∑ i ∈ s, r i) * HMul.hMul (α := R) (∑ i ∈ s, g i) (∑ i ∈ s, r i))
Tactic: simp_rw [mul_assoc, ← mul_sum, ← sum_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
⊢ LE.le.{u_2} (α := R) (∑ i ∈ s, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
    (∑ i ∈ s, (f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 + g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2))
have h₁ : ∀ (i : ι) (hi : i ∈ s),
  (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j ≤
    f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 + g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2
Tactic: gcongr with i hi
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
i : ι
hi : i ∈ s
⊢ HPow.hPow (β := ℕ) ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) 2 ≤
    f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 * (g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2)
have h₁ : 0 ≤ HPow.hPow (β := ℕ) (HMul.hMul (α := R) (∑ j ∈ s, g j) (∑ j ∈ s, r j)) 2
Tactic: grw [mul_mul_mul_comm, ← mul_pow, mul_assoc, mul_pow, ht i hi]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
i : ι
hi : i ∈ s
⊢ (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j ≤
    f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 + g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2
have ht₁ : HPow.hPow (β := ℕ) ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) 2 ≤
  f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 * (g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2)
Tactic: have ht : (r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j)) ^ 2 ≤
              (f i * (∑ j ∈ s, g j) ^ 2) * (g i * (∑ j ∈ s, r j) ^ 2) := by
            grw [mul_mul_mul_comm, ← mul_pow, mul_assoc, mul_pow, ht i hi]
            exact sq_nonneg _
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht_1 : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
i : ι
hi : i ∈ s
ht :
  HPow.hPow (β := ℕ) ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) 2 ≤
    f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 * (g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2)
⊢ (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j ≤
    f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 + g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2
have h₁ : (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
Tactic: refine le_of_eq_of_le ?_ (two_mul_le_add_of_sq_le_mul
            (mul_nonneg (hf i hi) (sq_nonneg _)) (mul_nonneg (hg i hi) (sq_nonneg _)) ht)
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht_1 : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
i : ι
hi : i ∈ s
ht :
  HPow.hPow (β := ℕ) ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) 2 ≤
    f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 * (g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2)
⊢ (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
have h₁ : 2 * r i * HMul.hMul (α := R) (∑ j ∈ s, g j) (∑ j ∈ s, r j) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht_1 : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
i : ι
hi : i ∈ s
ht :
  HPow.hPow (β := ℕ) ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) 2 ≤
    f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 * (g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2)
⊢ 2 * r i * HMul.hMul (α := R) (∑ j ∈ s, g j) (∑ j ∈ s, r j) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
have h₁ : 2 * (r i * HMul.hMul (α := R) (∑ j ∈ s, g j) (∑ j ∈ s, r j)) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht_1 : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
i : ι
hi : i ∈ s
ht :
  HPow.hPow (β := ℕ) ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) 2 ≤
    f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 * (g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2)
⊢ 2 * (r i * HMul.hMul (α := R) (∑ j ∈ s, g j) (∑ j ∈ s, r j)) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
have h₁ : 2 * (r i * HMul.hMul (α := R) (∑ j ∈ s, g j) (∑ j ∈ s, r j)) =
  2 * (r i * HMul.hMul (α := R) (∑ j ∈ s, g j) (∑ j ∈ s, r j))
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht_1 : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
i : ι
hi : i ∈ s
ht :
  HPow.hPow (β := ℕ) ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) 2 ≤
    f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 * (g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2)
⊢ (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
have h₁ : 2 * r i * HMul.hMul (α := R) (∑ j ∈ s, g j) (∑ j ∈ s, r j) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
Tactic: repeat rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht_1 : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
i : ι
hi : i ∈ s
ht :
  HPow.hPow (β := ℕ) ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) 2 ≤
    f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 * (g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2)
h₁ h₂ h₃ : 2 * r i * HMul.hMul (α := R) (∑ j ∈ s, g j) (∑ j ∈ s, r j) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
⊢ (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
have h₄ : 2 * (r i * HMul.hMul (α := R) (∑ j ∈ s, g j) (∑ j ∈ s, r j)) = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
Tactic: repeat rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
⊢ ∑ i ∈ s, (f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 + g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2) =
    (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have simp_rw : (∑ i ∈ s, f i) * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 +
    (∑ j ∈ s, g j) * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2 =
  (∑ j ∈ s, g j) * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2 +
    (∑ j ∈ s, g j) * HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ j ∈ s, g j)
Tactic: simp_rw [sum_add_distrib, ← sum_mul]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
⊢ (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤
    (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have _ : (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
    (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 =
  ∑ i ∈ s, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j
Tactic: calc
      _ = ∑ i ∈ s, 2 * r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j) := by
          simp_rw [mul_assoc, ← mul_sum, ← sum_mul]; ring
      _ ≤ ∑ i ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) := by
          gcongr with i hi
          have ht : (r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j)) ^ 2 ≤
              (f i * (∑ j ∈ s, g j) ^ 2) * (g i * (∑ j ∈ s, r j) ^ 2) := by
            grw [mul_mul_mul_comm, ← mul_pow, mul_assoc, mul_pow, ht i hi]
            exact sq_nonneg _
          refine le_of_eq_of_le ?_ (two_mul_le_add_of_sq_le_mul
            (mul_nonneg (hf i hi) (sq_nonneg _)) (mul_nonneg (hg i hi) (sq_nonneg _)) ht)
          repeat rw [mul_assoc]
      _ = _ := by simp_rw [sum_add_distrib, ← sum_mul]; ring
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
_ :
  (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 =
    ∑ i ∈ s, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j
⊢ (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤
    (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have _₁ : LE.le.{u_2} (α := R) (∑ i ∈ s, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
  (∑ i ∈ s, (f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 + g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2))
Tactic: calc
      _ = ∑ i ∈ s, 2 * r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j) := by
          simp_rw [mul_assoc, ← mul_sum, ← sum_mul]; ring
      _ ≤ ∑ i ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) := by
          gcongr with i hi
          have ht : (r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j)) ^ 2 ≤
              (f i * (∑ j ∈ s, g j) ^ 2) * (g i * (∑ j ∈ s, r j) ^ 2) := by
            grw [mul_mul_mul_comm, ← mul_pow, mul_assoc, mul_pow, ht i hi]
            exact sq_nonneg _
          refine le_of_eq_of_le ?_ (two_mul_le_add_of_sq_le_mul
            (mul_nonneg (hf i hi) (sq_nonneg _)) (mul_nonneg (hg i hi) (sq_nonneg _)) ht)
          repeat rw [mul_assoc]
      _ = _ := by simp_rw [sum_add_distrib, ← sum_mul]; ring
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommSemiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, HPow.hPow (β := ℕ) (r i) 2 ≤ f i * g i
h : LT.lt.{u_2} (α := R) 0 (∑ i ∈ s, g i)
_ :
  (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 =
    ∑ i ∈ s, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j
_₁ :
  LE.le.{u_2} (α := R) (∑ i ∈ s, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)
    (∑ i ∈ s, (f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 + g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2))
⊢ (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 ≤
    (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
      (∑ i ∈ s, g i) * HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
have _₂ : ∑ i ∈ s, (f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 + g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2) =
  (∑ i ∈ s, g i) * HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, r i) 2 +
    (∑ i ∈ s, g i) * HMul.hMul (α := R) (∑ i ∈ s, f i) (∑ i ∈ s, g i)
Tactic: calc
      _ = ∑ i ∈ s, 2 * r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j) := by
          simp_rw [mul_assoc, ← mul_sum, ← sum_mul]; ring
      _ ≤ ∑ i ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) := by
          gcongr with i hi
          have ht : (r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j)) ^ 2 ≤
              (f i * (∑ j ∈ s, g j) ^ 2) * (g i * (∑ j ∈ s, r j) ^ 2) := by
            grw [mul_mul_mul_comm, ← mul_pow, mul_assoc, mul_pow, ht i hi]
            exact sq_nonneg _
          refine le_of_eq_of_le ?_ (two_mul_le_add_of_sq_le_mul
            (mul_nonneg (hf i hi) (sq_nonneg _)) (mul_nonneg (hg i hi) (sq_nonneg _)) ht)
          repeat rw [mul_assoc]
      _ = _ := by simp_rw [sum_add_distrib, ← sum_mul]; ring
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, f i) 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2 / g i
have hg' : ∀ i ∈ s, 0 ≤ g i
Tactic: have hg' : ∀ i ∈ s, 0 ≤ g i := fun i hi ↦ (hg i hi).le
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, f i) 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2 / g i
have H : ∀ i ∈ s, 0 ≤ HPow.hPow (β := ℕ) (f i) 2 / g i
Tactic: have H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i := fun i hi ↦ div_nonneg (sq_nonneg _) (hg' i hi)
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ HPow.hPow (β := ℕ) (f i) 2 / g i
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, f i) 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2 / g i
have refine : ∀ (i : ι) (hi : i ∈ s), HPow.hPow (β := ℕ) (f i) 2 ≤ HPow.hPow (β := ℕ) (f i) 2 / g i * g i
Tactic: refine div_le_of_le_mul₀ (sum_nonneg hg') (sum_nonneg H)
    (sum_sq_le_sum_mul_sum_of_sq_le_mul _ H hg' fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : Semifield R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
f g : ι → R
hg : ∀ i ∈ s, 0 < g i
hg' : ∀ i ∈ s, 0 ≤ g i
H : ∀ i ∈ s, 0 ≤ HPow.hPow (β := ℕ) (f i) 2 / g i
i : ι
hi : i ∈ s
⊢ HPow.hPow (β := ℕ) (f i) 2 ≤ HPow.hPow (β := ℕ) (f i) 2 / g i * g i
have h : g i ≠ 0
Tactic: rw [div_mul_cancel₀]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.List (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : NoZeroDivisors α
inst_4 : Nontrivial α
x : α
xs : List α
⊢ 0 < (x :: xs).prod ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → 0 < x_1
have simp_rw : 0 < x * xs.prod ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → 0 < x_1
Tactic: simp_rw [List.prod_cons, List.forall_mem_cons, CanonicallyOrderedAdd.mul_pos,
    list_prod_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.List (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : NoZeroDivisors α
inst_4 : Nontrivial α
x : α
xs : List α
simp_rw : 0 < x * xs.prod ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → 0 < x_1
⊢ 0 < (x :: xs).prod ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → 0 < x_1
have simp_rw₁ : 0 < x * xs.prod ↔ 0 < x ∧ ∀ (x : α), x ∈ xs → 0 < x
Tactic: simp_rw [List.prod_cons, List.forall_mem_cons, CanonicallyOrderedAdd.mul_pos,
    list_prod_pos]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.List (goal)
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : NoZeroDivisors α
inst_4 : Nontrivial α
x : α
xs : List α
simp_rw : 0 < x * xs.prod ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → 0 < x_1
simp_rw₁ : 0 < x * xs.prod ↔ 0 < x ∧ ∀ (x : α), x ∈ xs → 0 < x
⊢ 0 < (x :: xs).prod ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → 0 < x_1
have simp_rw₂ : 0 < x ∧ 0 < xs.prod ↔ 0 < x ∧ ∀ (x : α), x ∈ xs → 0 < x
Tactic: simp_rw [List.prod_cons, List.forall_mem_cons, CanonicallyOrderedAdd.mul_pos,
    list_prod_pos]