awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
hlt : ∃ i ∈ s, f i < g i
obtain : ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i), LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
obtain₁ : ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i), f i * ∏ x ∈ s.erase i, f x < g i * ∏ x ∈ s.erase i, g x
obtain₂ :
  ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i) (this : MulPosStrictMono R),
    f i * ∏ x ∈ s.erase i, f x < g i * ∏ x ∈ s.erase i, g x
refine_1 :
  ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i) (this : MulPosStrictMono R),
    LE.le.{u_2} (α := R) (∏ x ∈ s.erase i, f x) (∏ x ∈ s.erase i, g x)
⊢ LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have refine_2 : ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i) (this : MulPosStrictMono R), LT.lt.{u_2} (α := R) 0 (∏ x ∈ s.erase i, f x)
Tactic: classical
  obtain ⟨i, hi, hilt⟩ := hlt
  rw [← insert_erase hi, prod_insert (notMem_erase _ _), prod_insert (notMem_erase _ _)]
  have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
  refine mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_
  · exact prod_le_prod (fun j hj => le_of_lt (hf j (mem_of_mem_erase hj)))
      (fun _ hj ↦ hfg _ <| mem_of_mem_erase hj)
  · exact prod_pos fun j hj => hf j (mem_of_mem_erase hj)
  · exact (hf i hi).le.trans hilt.le
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i ≤ g i
hlt : ∃ i ∈ s, f i < g i
obtain : ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i), LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
obtain₁ : ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i), f i * ∏ x ∈ s.erase i, f x < g i * ∏ x ∈ s.erase i, g x
obtain₂ :
  ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i) (this : MulPosStrictMono R),
    f i * ∏ x ∈ s.erase i, f x < g i * ∏ x ∈ s.erase i, g x
refine_1 :
  ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i) (this : MulPosStrictMono R),
    LE.le.{u_2} (α := R) (∏ x ∈ s.erase i, f x) (∏ x ∈ s.erase i, g x)
refine_2 :
  ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i) (this : MulPosStrictMono R), LT.lt.{u_2} (α := R) 0 (∏ x ∈ s.erase i, f x)
⊢ LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have refine_3 : ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i) (this : MulPosStrictMono R), 0 ≤ g i
Tactic: classical
  obtain ⟨i, hi, hilt⟩ := hlt
  rw [← insert_erase hi, prod_insert (notMem_erase _ _), prod_insert (notMem_erase _ _)]
  have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
  refine mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_
  · exact prod_le_prod (fun j hj => le_of_lt (hf j (mem_of_mem_erase hj)))
      (fun _ hj ↦ hfg _ <| mem_of_mem_erase hj)
  · exact prod_pos fun j hj => hf j (mem_of_mem_erase hj)
  · exact (hf i hi).le.trans hilt.le
Cleared hypotheses: hlt
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
h_ne : s.Nonempty
⊢ LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have apply : ∃ i ∈ s, f i < g i
Tactic: apply prod_lt_prod hf fun i hi => le_of_lt (hfg i hi)
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulStrictMono R
inst_4 : Nontrivial R
f g : ι → R
s : Finset ι
hf : ∀ i ∈ s, 0 < f i
hfg : ∀ i ∈ s, f i < g i
h_ne : s.Nonempty
⊢ ∃ i ∈ s, f i < g i
have obtain : ∀ (i : ι) (hi : i ∈ s), ∃ i ∈ s, f i < g i
Tactic: obtain ⟨i, hi⟩ := h_ne
Cleared hypotheses: h_ne
-- 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 : PosMulMono R
head : R
tail : List R
hind : ∀ (h : ∀ (a : R), a ∈ tail → 0 ≤ a), 0 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 0 ≤ a
⊢ 0 ≤ (head :: tail).prod
have cons : 0 ≤ head * tail.prod
Tactic: simp only [prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.List (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
head : R
tail : List R
hind : ∀ (h : ∀ (a : R), a ∈ tail → 0 ≤ a), 0 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 0 ≤ a
⊢ 0 ≤ head * tail.prod
have h₁ : 0 ≤ head ∧ ∀ (a : R), a ∈ tail → 0 ≤ a
Tactic: simp only [mem_cons, forall_eq_or_imp] at h
Cleared hypotheses: 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 : PosMulMono R
s : List R
h : ∀ (a : R), a ∈ s → 0 ≤ a
⊢ 0 ≤ s.prod
have nil : ∀ (h : ∀ (a : R), Membership.mem (γ := List R) [] a → 0 ≤ a), LE.le.{u_1} (α := R) 0 (prod [])
Tactic: induction s with
  | nil => simp
  | cons head tail hind =>
    simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact mul_nonneg h.1 (hind h.2)
Cleared hypotheses: s, 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 : PosMulMono R
s : List R
h : ∀ (a : R), a ∈ s → 0 ≤ a
nil : ∀ (h : ∀ (a : R), Membership.mem (γ := List R) [] a → 0 ≤ a), LE.le.{u_1} (α := R) 0 (prod [])
⊢ 0 ≤ s.prod
have cons : ∀ (head : R) (tail : List R) (hind : ∀ (h : ∀ (a : R), a ∈ tail → 0 ≤ a), 0 ≤ tail.prod)
  (h : ∀ (a : R), a ∈ head :: tail → 0 ≤ a), 0 ≤ (head :: tail).prod
Tactic: induction s with
  | nil => simp
  | cons head tail hind =>
    simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact mul_nonneg h.1 (hind h.2)
Cleared hypotheses: s, 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 : PosMulMono R
head : R
tail : List R
hind : ∀ (h : ∀ (a : R), a ∈ tail → 1 ≤ a), 1 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 1 ≤ a
⊢ 1 ≤ (head :: tail).prod
have cons : 1 ≤ head * tail.prod
Tactic: simp only [prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.List (hypothesis)
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : PartialOrder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
head : R
tail : List R
hind : ∀ (h : ∀ (a : R), a ∈ tail → 1 ≤ a), 1 ≤ tail.prod
h : ∀ (a : R), a ∈ head :: tail → 1 ≤ a
⊢ 1 ≤ head * tail.prod
have h₁ : 1 ≤ head ∧ ∀ (a : R), a ∈ tail → 1 ≤ a
Tactic: simp only [mem_cons, forall_eq_or_imp] at h
Cleared hypotheses: 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 : PosMulMono R
s : List R
h : ∀ (a : R), a ∈ s → 1 ≤ a
⊢ 1 ≤ s.prod
have nil : ∀ (h : ∀ (a : R), Membership.mem (γ := List R) [] a → 1 ≤ a), LE.le.{u_1} (α := R) 1 (prod [])
Tactic: induction s with
  | nil => simp
  | cons head tail hind =>
    simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact one_le_mul_of_one_le_of_one_le h.1 (hind h.2)
Cleared hypotheses: s, 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 : PosMulMono R
s : List R
h : ∀ (a : R), a ∈ s → 1 ≤ a
nil : ∀ (h : ∀ (a : R), Membership.mem (γ := List R) [] a → 1 ≤ a), LE.le.{u_1} (α := R) 1 (prod [])
⊢ 1 ≤ s.prod
have cons : ∀ (head : R) (tail : List R) (hind : ∀ (h : ∀ (a : R), a ∈ tail → 1 ≤ a), 1 ≤ tail.prod)
  (h : ∀ (a : R), a ∈ head :: tail → 1 ≤ a), 1 ≤ (head :: tail).prod
Tactic: induction s with
  | nil => simp
  | cons head tail hind =>
    simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact one_le_mul_of_one_le_of_one_le h.1 (hind h.2)
Cleared hypotheses: s, 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 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
⊢ (map f (a :: s)).prod ≤ (map g (a :: s)).prod
have cons : f a * (map f s).prod ≤ g a * (map g s).prod
Tactic: simp only [map_cons, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.List (hypothesis)
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 : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
⊢ f a * (map f s).prod ≤ g a * (map g s).prod
have this : MulPosMono R
Tactic: have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
-- 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 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ f a * (map f s).prod ≤ g a * (map g s).prod
have cons : f a ≤ g a
Tactic: apply mul_le_mul
-- 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 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
cons : f a ≤ g a
⊢ f a * (map f s).prod ≤ g a * (map g s).prod
have cons₁ : (map f s).prod ≤ (map g s).prod
Tactic: apply mul_le_mul
-- 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 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
cons : f a ≤ g a
cons₁ : (map f s).prod ≤ (map g s).prod
⊢ f a * (map f s).prod ≤ g a * (map g s).prod
have cons₂ : 0 ≤ (map f s).prod
Tactic: apply mul_le_mul
-- 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 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
cons : f a ≤ g a
cons₁ : (map f s).prod ≤ (map g s).prod
cons₂ : 0 ≤ (map f s).prod
⊢ f a * (map f s).prod ≤ g a * (map g s).prod
have cons₃ : 0 ≤ g a
Tactic: apply mul_le_mul
-- 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 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ f a ≤ g a
have cons : a ∈ 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 : PosMulMono R
ι : Type u_2
f g : ι → R
a : ι
s : List ι
hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod
h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i
h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i
this : MulPosMono R
⊢ 0 ≤ g a
have apply : a ∈ a :: s
Tactic: apply (h0 _ _).trans (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 : PosMulMono R
ι : Type u_2
s : List ι
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 nil : ∀ (h0 : ∀ (i : ι), Membership.mem (γ := List ι) [] i → 0 ≤ f i)
  (h : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i ≤ g i), (map f []).prod ≤ (map g []).prod
Tactic: induction s with
  | nil => simp
  | cons a s hind =>
    simp only [map_cons, prod_cons]
    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
    apply mul_le_mul
    · apply h
      simp
    · grind
    · grind [prod_nonneg]
    · apply (h0 _ _).trans (h _ _) <;> simp only [mem_cons, true_or]
Cleared hypotheses: s, h0, 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 : PosMulMono R
ι : Type u_2
s : List ι
f g : ι → R
h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i
h : ∀ (i : ι), i ∈ s → f i ≤ g i
nil :
  ∀ (h0 : ∀ (i : ι), Membership.mem (γ := List ι) [] i → 0 ≤ f i)
    (h : ∀ (i : ι), Membership.mem (γ := List ι) [] i → f i ≤ g i), (map f []).prod ≤ (map g []).prod
⊢ (map f s).prod ≤ (map g s).prod
have cons : ∀ (a : ι) (s : List ι)
  (hind : ∀ (h0 : ∀ (i : ι), i ∈ s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ s → f i ≤ g i), (map f s).prod ≤ (map g s).prod)
  (h0 : ∀ (i : ι), i ∈ a :: s → 0 ≤ f i) (h : ∀ (i : ι), i ∈ a :: s → f i ≤ g i),
  (map f (a :: s)).prod ≤ (map g (a :: s)).prod
Tactic: induction s with
  | nil => simp
  | cons a s hind =>
    simp only [map_cons, prod_cons]
    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
    apply mul_le_mul
    · apply h
      simp
    · grind
    · grind [prod_nonneg]
    · apply (h0 _ _).trans (h _ _) <;> simp only [mem_cons, true_or]
Cleared hypotheses: s, h0, 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 : PosMulMono R
F : Type u_2
L : Type u_3
inst_4 : FunLike F L R
f : F
r : R
t : List 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.length
have h : r ^ t.length = (map (Function.const L r) t).prod
Tactic: convert! prod_map_le_prod_map₀ f (Function.const L r) hf0 hf
-- 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
a : R
s : List R
hind : ∀ (h : ∀ (a : R), a ∈ s → 0 < a), 0 < s.prod
h : ∀ (a_1 : R), a_1 ∈ a :: s → 0 < a_1
⊢ 0 < (a :: s).prod
have cons : 0 < a * s.prod
Tactic: simp only [prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.List (hypothesis)
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 : R
s : List R
hind : ∀ (h : ∀ (a : R), a ∈ s → 0 < a), 0 < s.prod
h : ∀ (a_1 : R), a_1 ∈ a :: s → 0 < a_1
⊢ 0 < a * s.prod
have h₁ : 0 < a ∧ ∀ (a : R), a ∈ s → 0 < a
Tactic: simp only [mem_cons, forall_eq_or_imp] at h
Cleared hypotheses: 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
s : List R
h : ∀ (a : R), a ∈ s → 0 < a
⊢ 0 < s.prod
have nil : ∀ (h : ∀ (a : R), Membership.mem (γ := List R) [] a → 0 < a), LT.lt.{u_1} (α := R) 0 (prod [])
Tactic: induction s with
  | nil => simp
  | cons a s hind =>
    simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact mul_pos h.1 (hind h.2)
Cleared hypotheses: s, 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
s : List R
h : ∀ (a : R), a ∈ s → 0 < a
nil : ∀ (h : ∀ (a : R), Membership.mem (γ := List R) [] a → 0 < a), LT.lt.{u_1} (α := R) 0 (prod [])
⊢ 0 < s.prod
have cons : ∀ (a : R) (s : List R) (hind : ∀ (h : ∀ (a : R), a ∈ s → 0 < a), 0 < s.prod) (h : ∀ (a_1 : R), a_1 ∈ a :: s → 0 < a_1),
  0 < (a :: s).prod
Tactic: induction s with
  | nil => simp
  | cons a s hind =>
    simp only [prod_cons]
    simp only [mem_cons, forall_eq_or_imp] at h
    exact mul_pos h.1 (hind h.2)
Cleared hypotheses: s, 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
⊢ (map f (a :: s)).prod < (map g (a :: s)).prod
have simp : f a * (map f s).prod < g a * (map g s).prod
Tactic: simp only [map_cons, prod_cons]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.List (hypothesis)
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
⊢ f a * (map f s).prod < g a * (map g s).prod
have this : MulPosStrictMono R
Tactic: have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
-- 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
⊢ f a * (map f s).prod < g a * (map g s).prod
have h₁ : f a < g a
Tactic: apply mul_lt_mul
-- 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
h₁ : f a < g a
⊢ f a * (map f s).prod < g a * (map g s).prod
have h₂ : (map f s).prod ≤ (map g s).prod
Tactic: apply mul_lt_mul
-- 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
h₁ : f a < g a
h₂ : (map f s).prod ≤ (map g s).prod
⊢ f a * (map f s).prod < g a * (map g s).prod
have c0 : 0 < (map f s).prod
Tactic: apply mul_lt_mul
-- 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
h₁ : f a < g a
h₂ : (map f s).prod ≤ (map g s).prod
c0 : 0 < (map f s).prod
⊢ f a * (map f s).prod < g a * (map g s).prod
have b0 : 0 ≤ g a
Tactic: apply mul_lt_mul
-- 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
⊢ f a < g a
have h₁ : a ∈ 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
⊢ (map f s).prod ≤ (map g s).prod
have h₂ : ∀ (i : ι), i ∈ s → 0 ≤ f i
Tactic: apply prod_map_le_prod_map₀
-- 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
h₂ : ∀ (i : ι), i ∈ s → 0 ≤ f i
⊢ (map f s).prod ≤ (map g s).prod
have h₃ : ∀ (i : ι), i ∈ s → f i ≤ g i
Tactic: apply prod_map_le_prod_map₀
-- 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
⊢ 0 ≤ f i
have h₂ : 0 < f i
Tactic: apply le_of_lt
-- 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
⊢ 0 < f i
have h₂ : i ∈ a :: s
Tactic: apply h0
-- 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₂ : f i < g i
Tactic: apply le_of_lt