awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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)
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
⊢ 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:
gcongr with i hi
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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
h₁ : 0 ≤ HPow.hPow (β := ℕ) (HMul.hMul (α := R) (∑ j ∈ s, g j) (∑ j ∈ s, r j)) 2
⊢ 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:
grw [mul_mul_mul_comm, ← mul_pow, mul_assoc, mul_pow, ht i hi]

Premises used: mul_mul_mul_comm, mul_assoc, mul_pow
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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
⊢ 0 ≤ HPow.hPow (β := ℕ) (HMul.hMul (α := R) (∑ j ∈ s, g j) (∑ j ∈ s, r j)) 2

Tactic:
sq_nonneg _

Premises used: sq_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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
⊢ 0 ≤ HPow.hPow (β := ℕ) (HMul.hMul (α := R) (∑ j ∈ s, g j) (∑ j ∈ s, r j)) 2

Tactic:
exact sq_nonneg _

Premises used: sq_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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)

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 _
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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

Tactic:
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)

Premises used: mul_nonneg, sq_nonneg, le_of_eq_of_le, two_mul_le_add_of_sq_le_mul
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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₁ : (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 ≤
    f i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, g j) 2 + g i * HPow.hPow (α := R) (β := ℕ) (∑ j ∈ s, r j) 2

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)

Premises used: mul_nonneg, sq_nonneg, le_of_eq_of_le, two_mul_le_add_of_sq_le_mul
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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₁ : 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)

Tactic:
rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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₁ : 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 * 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]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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₂ :
  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))
⊢ 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]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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)
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)

Tactic:
repeat rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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)
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)
⊢ ∑ 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:
simp_rw [sum_add_distrib, ← sum_mul]

Premises used: Finset.sum_add_distrib, Finset.sum_mul
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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 +
      (∑ 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:
ring
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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, (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)
⊢ (∑ 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:
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

Premises used: Finset.sum
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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)

Tactic:
sum_sq_le_sum_mul_sum_of_sq_le_mul s hf hg (fun i hi => (ht i hi).le)

Premises used: Finset.sum_sq_le_sum_mul_sum_of_sq_le_mul, Eq.le
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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 ι
f g : ι → R
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, f i * g i) 2 ≤
    HMul.hMul (α := R) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (∑ i ∈ s, HPow.hPow (β := ℕ) (g i) 2)

Tactic:
sum_sq_le_sum_mul_sum_of_sq_le_mul s
    (fun _ _ ↦ sq_nonneg _) (fun _ _ ↦ sq_nonneg _) (fun _ _ ↦ (mul_pow ..).le)

Premises used: Finset.sum_sq_le_sum_mul_sum_of_sq_le_mul, Eq.le, sq_nonneg, OfNat.ofNat, mul_pow
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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
⊢ ∀ i ∈ s, 0 ≤ g i

Tactic:
have hg' : ∀ i ∈ s, 0 ≤ g i := fun i hi ↦ (hg i hi).le
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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
⊢ ∀ 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)
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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

Tactic:
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 ↦ ?_)

Premises used: div_le_of_le_mul₀, Finset.sum_sq_le_sum_mul_sum_of_sq_le_mul, Finset.sum_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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
refine : ∀ (i : ι) (hi : i ∈ s), HPow.hPow (β := ℕ) (f i) 2 ≤ HPow.hPow (β := ℕ) (f i) 2 / g i * g i
⊢ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, f i) 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2 / 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 ↦ ?_)

Premises used: div_le_of_le_mul₀, Finset.sum_sq_le_sum_mul_sum_of_sq_le_mul, Finset.sum_nonneg
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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
h : g i ≠ 0
⊢ HPow.hPow (β := ℕ) (f i) 2 ≤ HPow.hPow (β := ℕ) (f i) 2 / g i * g i

Tactic:
rw [div_mul_cancel₀]

Premises used: div_mul_cancel₀
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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
⊢ g i ≠ 0

Tactic:
(hg i hi).ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
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
⊢ g i ≠ 0

Tactic:
exact (hg i hi).ne'

Premises used: LT.lt.ne'
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
inst_3 : IsOrderedRing S
abv : AbsoluteValue R S
s : Finset ι
f : ι → R
⊢ LE.le.{u_3} (α := S) ((abv : (a : R) → S) (∑ i ∈ s, f i) : S) (∑ i ∈ s, (abv : (a : R) → S) (f i) : S)

Tactic:
Finset.le_sum_of_subadditive abv (map_zero _).le abv.add_le _ _

Premises used: Finset.le_sum_of_subadditive, map_zero, Eq.le, AbsoluteValue.add_le, DFunLike.coe
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : PartialOrder S
inst_3 : IsOrderedRing S
abv : R → S
inst_4 : IsAbsoluteValue abv
f : ι → R
s : Finset ι
⊢ abv (∑ i ∈ s, f i) ≤ ∑ i ∈ s, abv (f i)

Tactic:
(IsAbsoluteValue.toAbsoluteValue abv).sum_le _ _

Premises used: IsAbsoluteValue.toAbsoluteValue, AbsoluteValue.sum_le
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
abv : AbsoluteValue R S
f : ι → R
s : Finset ι
⊢ Eq.{u_3 + 1} (α := S) ((abv : (a : R) → S) (∏ i ∈ s, f i) : S) (∏ i ∈ s, (abv : (a : R) → S) (f i) : S)

Tactic:
map_prod abv f s

Premises used: map_prod
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Finset
Goal:
ι : Type u_1
R : Type u_2
S : Type u_3
inst : CommSemiring R
inst_1 : Nontrivial R
inst_2 : CommRing S
inst_3 : LinearOrder S
inst_4 : IsStrictOrderedRing S
abv : R → S
inst_5 : IsAbsoluteValue abv
f : ι → R
s : Finset ι
⊢ abv (∏ i ∈ s, f i) = ∏ i ∈ s, abv (f i)

Tactic:
(IsAbsoluteValue.toAbsoluteValue abv).map_prod _ _

Premises used: IsAbsoluteValue.toAbsoluteValue, AbsoluteValue.map_prod
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.List
Goal:
α : Type u_2
inst : CommSemiring α
inst_1 : PartialOrder α
inst_2 : CanonicallyOrderedAdd α
inst_3 : NoZeroDivisors α
inst_4 : Nontrivial α
⊢ LT.lt.{u_2} (α := α) 0 (List.prod []) ↔ ∀ (x : α), Membership.mem (γ := List α) [] x → 0 < x

Tactic:
simp
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.List
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
simp_rw₂ : 0 < x ∧ 0 < xs.prod ↔ 0 < x ∧ ∀ (x : α), x ∈ xs → 0 < x
⊢ 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]

Premises used: List.forall_mem_cons, CanonicallyOrderedAdd.mul_pos, List.prod_cons
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
m : Multiset R
mk :
  ∀ (l : List R),
    0 < prod (Quot.mk (⇑(List.isSetoid R) : List R → List R → Prop) l) ↔
      ∀ (x : R), Membership.mem (γ := Multiset R) (Quot.mk (⇑(List.isSetoid R) : List R → List R → Prop) l) x → 0 < x
⊢ 0 < m.prod ↔ ∀ (x : R), x ∈ m → 0 < x

Tactic:
rcases m with ⟨l⟩
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
m : Multiset R
l : List R
mk : 0 < l.prod ↔ ∀ (x : R), x ∈ (↑l : Multiset R) → 0 < x
⊢ 0 < prod (Quot.mk (⇑(List.isSetoid R) : List R → List R → Prop) l) ↔
    ∀ (x : R), Membership.mem (γ := Multiset R) (Quot.mk (⇑(List.isSetoid R) : List R → List R → Prop) l) x → 0 < x

Tactic:
rw [Multiset.quot_mk_to_coe'', Multiset.prod_coe]

Premises used: Multiset.prod_coe, Multiset.quot_mk_to_coe''
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < l.prod ↔ ∀ (x : R), x ∈ (↑l : Multiset R) → 0 < x

Tactic:
CanonicallyOrderedAdd.list_prod_pos

Premises used: Multiset.Mem, CanonicallyOrderedAdd.list_prod_pos
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
R : Type u_1
inst : CommSemiring R
inst_1 : PartialOrder R
inst_2 : CanonicallyOrderedAdd R
inst_3 : NoZeroDivisors R
inst_4 : Nontrivial R
m : Multiset R
l : List R
⊢ 0 < l.prod ↔ ∀ (x : R), x ∈ (↑l : Multiset R) → 0 < x

Tactic:
exact CanonicallyOrderedAdd.list_prod_pos

Premises used: CanonicallyOrderedAdd.list_prod_pos
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
s : Multiset α
hps : ∀ (a : α), a ∈ s → p a
revert : ∀ (s : Multiset α) (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
⊢ f s.prod ≤ (map f s).prod

Tactic:
revert s
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
⊢ ∀ (hps : ∀ (a : α), Membership.mem (γ := Multiset α) 0 a → p a), f (prod 0) ≤ (map f 0).prod

Tactic:
simp [h_one]
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
refine :
  ∀ (a : α) (s : Multiset α),
    (∀ (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod) →
      ∀ (hps : ∀ (a_2 : α), a_2 ∈ a ::ₘ s → p a_2), f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
⊢ ∀ (s : Multiset α) (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod

Tactic:
refine Multiset.induction (by simp [h_one]) ?_
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : ∀ (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
pos : ∀ (hs0 : s = ∅), f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
neg : ∀ (hs0 : ¬s = ∅), f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
by_cases hs0 : s = ∅
-- Module: Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Goal:
α : Type u_1
β : Type u_2
inst : CommMonoid α
inst_1 : CommMonoidWithZero β
inst_2 : PartialOrder β
inst_3 : PosMulMono β
f : α → β
p : α → Prop
h0 : ∀ (a : α), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
a : α
s : Multiset α
hs : ∀ (hps : ∀ (a : α), a ∈ s → p a), f s.prod ≤ (map f s).prod
hpsa : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → p a_1
hs0 : s = ∅
⊢ f (a ::ₘ s).prod ≤ (map f (a ::ₘ s)).prod

Tactic:
simp [hs0]