awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.List (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
i : ι
hi : i ∈ s
⊢ f i < g i
have h₂ : i ∈ a :: s
Tactic: apply h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.List (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ 0 < (map f s).prod
have c0 : ∀ (a : R), a ∈ map f s → 0 < a
Tactic: apply prod_pos
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.List (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_2
s_1 : List ι
f g : ι → R
a : ι
s : List ι
hs : a :: s ≠ []
h0 : ∀ (i : ι), i ∈ a :: s → 0 < f i
h : ∀ (i : ι), i ∈ a :: s → f i < g i
this : MulPosStrictMono R
⊢ 0 ≤ g a
have apply : a ∈ a :: s
Tactic: apply le_of_lt ((h0 _ _).trans (h _ _))
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
s : Multiset R
h : ∀ (a : R), a ∈ s → 0 ≤ a
⊢ 0 ≤ s.prod
have a : ∀ (a : List R) (h : ∀ (a_1 : R), a_1 ∈ ⟦a⟧ → 0 ≤ a_1), 0 ≤ prod ⟦a⟧
Tactic: cases s using Quotient.ind
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
a : List R
h : ∀ (a_1 : R), a_1 ∈ ⟦a⟧ → 0 ≤ a_1
⊢ 0 ≤ prod ⟦a⟧
have a : ∀ (h : ∀ (a_1 : R), a_1 ∈ a → 0 ≤ a_1), 0 ≤ a.prod
Tactic: simp only [quot_mk_to_coe, mem_coe, prod_coe] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
s : Multiset R
h : ∀ (a : R), a ∈ s → 1 ≤ a
⊢ 1 ≤ s.prod
have a : ∀ (a : List R) (h : ∀ (a_1 : R), a_1 ∈ ⟦a⟧ → 1 ≤ a_1), 1 ≤ prod ⟦a⟧
Tactic: cases s using Quotient.ind
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
a : List R
h : ∀ (a_1 : R), a_1 ∈ ⟦a⟧ → 1 ≤ a_1
⊢ 1 ≤ prod ⟦a⟧
have a : ∀ (h : ∀ (a_1 : R), a_1 ∈ a → 1 ≤ a_1), 1 ≤ a.prod
Tactic: simp only [quot_mk_to_coe, mem_coe, prod_coe] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
ι : Type u_2
s : Multiset ι
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h : ∀ (i : ι), i ∈ s → f i ≤ g i
⊢ (map f s).prod ≤ (map g s).prod
have a : ∀ (a : List ι) (h0 : ∀ (i : ι), i ∈ ⟦a⟧ → 0 ≤ f i) (h : ∀ (i : ι), i ∈ ⟦a⟧ → f i ≤ g i),
  (map f ⟦a⟧).prod ≤ (map g ⟦a⟧).prod
Tactic: cases s using Quotient.ind
Cleared hypotheses: s, h0, h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
ι : Type u_2
f g : ι → R
a : List ι
h0 : ∀ (i : ι), i ∈ ⟦a⟧ → 0 ≤ f i
h : ∀ (i : ι), i ∈ ⟦a⟧ → f i ≤ g i
⊢ (map f ⟦a⟧).prod ≤ (map g ⟦a⟧).prod
have a : ∀ (h0 : ∀ (i : ι), i ∈ a → 0 ≤ f i) (h : ∀ (i : ι), i ∈ a → f i ≤ g i), (List.map f a).prod ≤ (List.map g a).prod
Tactic: simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe] at *
Cleared hypotheses: h0, h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
F : Type u_2
L : Type u_3
inst_4 : FunLike F L R
f : F
r : R
t : Multiset L
hf0 : ∀ (x : L), x ∈ t → LE.le.{u_1} (α := R) (0 : R) ((f : (a : L) → R) x : R)
hf : ∀ (x : L), x ∈ t → (f : (a : L) → R) x ≤ r
⊢ prod (map (⇑f : (a : L) → R) t) ≤ r ^ t.card
have h : ∀ (a : List L) (hf0 : ∀ (x : L), x ∈ ⟦a⟧ → LE.le.{u_1} (α := R) (0 : R) ((f : (a : L) → R) x : R))
  (hf : ∀ (x : L), x ∈ ⟦a⟧ → (f : (a : L) → R) x ≤ r), prod (map (⇑f : (a : L) → R) ⟦a⟧) ≤ r ^ card ⟦a⟧
Tactic: induction t using Quotient.inductionOn
Cleared hypotheses: t, hf0, hf
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 0 ≤ f a
⊢ 0 ≤ (map f s).prod
have refine : ∀ (r : R) (hr : r ∈ map f s), 0 ≤ r
Tactic: refine prod_nonneg fun r hr ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 0 ≤ f a
r : R
hr : r ∈ map f s
⊢ 0 ≤ r
have obtain : ∀ (a : α) (ha : a ∈ s) (hr : f a ∈ map f s), 0 ≤ f a
Tactic: obtain ⟨a, ha, rfl⟩ := mem_map.mp hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 1 ≤ f a
⊢ 1 ≤ (map f s).prod
have refine : ∀ (r : R) (hr : r ∈ map f s), 1 ≤ r
Tactic: refine one_le_prod fun r hr ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
α : Type u_2
s : Multiset α
f : α → R
h : ∀ (a : α), a ∈ s → 1 ≤ f a
r : R
hr : r ∈ map f s
⊢ 1 ≤ r
have obtain : ∀ (a : α) (ha : a ∈ s) (hr : f a ∈ map f s), 1 ≤ f a
Tactic: obtain ⟨a, ha, rfl⟩ := mem_map.mp hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
s : Multiset R
h : ∀ (a : R), a ∈ s → 0 < a
⊢ 0 < s.prod
have a : ∀ (a : List R) (h : ∀ (a_1 : R), a_1 ∈ ⟦a⟧ → 0 < a_1), 0 < prod ⟦a⟧
Tactic: cases s using Quotient.ind
Cleared hypotheses: s, h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
a : List R
h : ∀ (a_1 : R), a_1 ∈ ⟦a⟧ → 0 < a_1
⊢ 0 < prod ⟦a⟧
have a : ∀ (h : ∀ (a_1 : R), a_1 ∈ a → 0 < a_1), 0 < a.prod
Tactic: simp only [quot_mk_to_coe, mem_coe, prod_coe] at *
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_3
s : Multiset ι
hs : s ≠ 0
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 < f i
h : ∀ (i : ι), i ∈ s → f i < g i
⊢ (map f s).prod < (map g s).prod
have a : ∀ (a : List ι) (hs : ⟦a⟧ ≠ 0) (h0 : ∀ (i : ι), i ∈ ⟦a⟧ → 0 < f i) (h : ∀ (i : ι), i ∈ ⟦a⟧ → f i < g i),
  (map f ⟦a⟧).prod < (map g ⟦a⟧).prod
Tactic: cases s using Quotient.ind
Cleared hypotheses: s, hs, h0, h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset (goal)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : NeZero.{u_1} (R := R) 1
ι : Type u_3
f g : ι → R
a : List ι
hs : ⟦a⟧ ≠ 0
h0 : ∀ (i : ι), i ∈ ⟦a⟧ → 0 < f i
h : ∀ (i : ι), i ∈ ⟦a⟧ → f i < g i
⊢ (map f ⟦a⟧).prod < (map g ⟦a⟧).prod
have a : ∀ (hs : ¬a = []) (h0 : ∀ (i : ι), i ∈ a → 0 < f i) (h : ∀ (i : ι), i ∈ a → f i < g i),
  (List.map f a).prod < (List.map g a).prod
Tactic: simp only [quot_mk_to_coe, mem_coe, map_coe, prod_coe, ne_eq, coe_eq_zero] at *
Cleared hypotheses: hs, h0, h
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2 ≤ HPow.hPow (α := R) (β := ℕ) (∑ i ∈ s, f i) 2
have simp : LE.le.{u_2} (α := R) (∑ x ∈ s, f x * f x) (∑ i ∈ s, ∑ j ∈ s, f i * f j)
Tactic: simp only [sq, sum_mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
⊢ LE.le.{u_2} (α := R) (∑ x ∈ s, f x * f x) (∑ i ∈ s, ∑ j ∈ s, f i * f j)
have refine : ∀ (i : ι) (hi : i ∈ s), f i * f i ≤ ∑ j ∈ s, f i * f j
Tactic: refine sum_le_sum fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i * f i ≤ ∑ j ∈ s, f i * f j
have rw : f i * f i ≤ f i * ∑ i ∈ s, f i
Tactic: rw [← mul_sum]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i * f i ≤ f i * ∑ i ∈ s, f i
have ha : 0 ≤ f i
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : PartialOrder R
inst_2 : IsOrderedRing R
f : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
ha : 0 ≤ f i
⊢ f i * f i ≤ f i * ∑ i ∈ s, f i
have hbc : f i ≤ ∑ i ∈ s, f i
Tactic: gcongr
-- 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 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h 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 ≤ f i * ∏ i ∈ s \ {i}, f i
Tactic: simp_rw [prod_eq_mul_prod_diff_singleton_of_mem 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 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i
have refine_1 : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ (g i + h i) * ∏ i ∈ s \ {i}, f i
Tactic: refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
-- 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 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
refine_1 : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ (g i + h i) * ∏ i ∈ s \ {i}, f i
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i
have refine_2 : LE.le.{u_2} (α := R) 0 (∏ i ∈ s \ {i}, f i)
Tactic: refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
-- 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 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ (g i + h i) * ∏ i ∈ s \ {i}, f i
have refine_1 : 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: rw [right_distrib]
-- 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 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ 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 refine_1 : 0 ≤ g i
Tactic: gcongr with 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 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
refine_1 : 0 ≤ g i
⊢ 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 refine_1₁ : ∀ i_1 ∈ s \ {i}, 0 ≤ g i_1
Tactic: gcongr with 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 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
refine_1 : 0 ≤ g i
refine_1₁ : ∀ i_1 ∈ s \ {i}, 0 ≤ g i_1
⊢ 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 refine_1₂ : ∀ (j : ι) (hj : j ∈ s \ {i}), g j ≤ f j
Tactic: gcongr with 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 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
refine_1 : 0 ≤ g i
refine_1₁ : ∀ i_1 ∈ s \ {i}, 0 ≤ g i_1
refine_1₂ : ∀ (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 refine_1₃ : 0 ≤ h i
Tactic: gcongr with 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 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
refine_1 : 0 ≤ g i
refine_1₁ : ∀ i_1 ∈ s \ {i}, 0 ≤ g i_1
refine_1₂ : ∀ (j : ι) (hj : j ∈ s \ {i}), g j ≤ f j
refine_1₃ : 0 ≤ h i
⊢ 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 refine_1₄ : ∀ i_1 ∈ s \ {i}, 0 ≤ h i_1
Tactic: gcongr with 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 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
refine_1 : 0 ≤ g i
refine_1₁ : ∀ i_1 ∈ s \ {i}, 0 ≤ g i_1
refine_1₂ : ∀ (j : ι) (hj : j ∈ s \ {i}), g j ≤ f j
refine_1₃ : 0 ≤ h i
refine_1₄ : ∀ i_1 ∈ s \ {i}, 0 ≤ h i_1
⊢ 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 refine_1₅ : ∀ i_1 ∈ s \ {i}, h i_1 ≤ f i_1
Tactic: gcongr with 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 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ LE.le.{u_2} (α := R) 0 (∏ i ∈ s \ {i}, f i)
have refine_2 : ∀ i_1 ∈ s \ {i}, 0 ≤ f i_1
Tactic: apply prod_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 : PartialOrder R
inst_2 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
⊢ ∀ i_1 ∈ s \ {i}, 0 ≤ f i_1
have refine_2 : ∀ i_1 ∈ s, ¬i_1 = i → 0 ≤ f i_1
Tactic: simp only [and_imp, mem_sdiff, mem_singleton]
-- 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 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h 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 ≤ f i * ∏ i ∈ s \ {i}, f i
Tactic: classical
  simp_rw [prod_eq_mul_prod_diff_singleton_of_mem hi]
  refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
  · rw [right_distrib]
    gcongr with j hj <;> aesop
  · apply prod_nonneg
    simp only [and_imp, mem_sdiff, mem_singleton]
    exact fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)
-- 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 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
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 refine_1 : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ (g i + h i) * ∏ i ∈ s \ {i}, f i
Tactic: classical
  simp_rw [prod_eq_mul_prod_diff_singleton_of_mem hi]
  refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
  · rw [right_distrib]
    gcongr with j hj <;> aesop
  · apply prod_nonneg
    simp only [and_imp, mem_sdiff, mem_singleton]
    exact fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)
-- 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 : IsOrderedRing R
s : Finset ι
i : ι
f g h : ι → R
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
hg : ∀ i ∈ s, 0 ≤ g i
hh : ∀ i ∈ s, 0 ≤ h i
simp_rw : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i
refine_1 : g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ (g i + h i) * ∏ i ∈ s \ {i}, f i
⊢ HAdd.hAdd (α := R) (∏ i ∈ s, g i) (∏ i ∈ s, h i) ≤ ∏ i ∈ s, f i
have refine_2 : LE.le.{u_2} (α := R) 0 (∏ i ∈ s \ {i}, f i)
Tactic: classical
  simp_rw [prod_eq_mul_prod_diff_singleton_of_mem hi]
  refine le_trans ?_ (mul_le_mul_of_nonneg_right h2i ?_)
  · rw [right_distrib]
    gcongr with j hj <;> aesop
  · apply prod_nonneg
    simp only [and_imp, mem_sdiff, mem_singleton]
    exact fun j hj hji ↦ le_trans (hg j hj) (hgf j hj hji)
-- 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 : IsOrderedRing R
M : Type u_4
inst_3 : CommMonoid M
f : M → R
p : M → Prop
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : M), p a → p b → p (a * b)
s : Finset ι
g : ι → M
hps : ∀ a ∈ s, p (g a)
⊢ f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
have apply : ∀ (a : M), Membership.mem (γ := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) a → p a
Tactic: apply le_trans (Multiset.le_prod_of_submultiplicative_on_pred_of_nonneg f p h_nonneg h_one
    h_mul hp_mul _ ?_) (by simp [Multiset.map_map])
-- 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 : IsOrderedRing R
M : Type u_4
inst_3 : CommMonoid M
f : M → R
p : M → Prop
h_nonneg : ∀ (a : M), 0 ≤ f a
h_one : f 1 ≤ 1
h_mul : ∀ (a b : M), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : M), p a → p b → p (a * b)
s : Finset ι
g : ι → M
hps : ∀ a ∈ s, p (g a)
a : M
ha : Membership.mem (γ := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) a
⊢ p a
have obtain : ∀ (i : ι) (hi : i ∈ s.val) (ha : Membership.mem (γ := Multiset M) (Multiset.map (fun (i : ι) ↦ g i) s.val) (g i)),
  p (g i)
Tactic: obtain ⟨i, hi, rfl⟩ := Multiset.mem_map.mp ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.Ring.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : ExistsAddOfLE R
s : Finset ι
f : ι → R
⊢ Eq.{u_2 + 1} (α := R) (∑ i ∈ s, f i * f i) 0 ↔ ∀ i ∈ s, f i = 0
have rw : (∀ i ∈ s, f i * f i = 0) ↔ ∀ i ∈ s, f i = 0
Tactic: rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ mul_self_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 : 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: simp_rw [prod_eq_mul_prod_diff_singleton_of_mem 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 : 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
⊢ g i * ∏ i ∈ s \ {i}, g i + h i * ∏ i ∈ s \ {i}, h i ≤ f i * ∏ i ∈ s \ {i}, f i
have grw : 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: grw [← h2i, right_distrib]
-- 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
⊢ 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}), g j ≤ f j
Tactic: gcongr with j hj j hj