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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
h0 : ∀ i ∈ cons a s has, 0 ≤ f i
h1 : ∀ i ∈ cons a s has, f i ≤ g i
⊢ LE.le.{u_2} (α := R) (∏ i ∈ cons a s has, f i) (∏ i ∈ cons a s has, g i)
have cons : ∀ (h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x) (h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x), f a * ∏ i ∈ s, f i ≤ g a * ∏ i ∈ s, g i
Tactic: simp only [prod_cons, forall_mem_cons] at h0 h1 ⊢
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
⊢ f a * ∏ i ∈ s, f i ≤ g a * ∏ i ∈ s, g i
have this : MulPosMono R
Tactic: have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
-- 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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
⊢ f a * ∏ i ∈ s, f i ≤ g a * ∏ i ∈ s, g i
have cons : LE.le.{u_2} (α := R) 0 (∏ i ∈ s, f i)
Tactic: gcongr
-- 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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
cons : LE.le.{u_2} (α := R) 0 (∏ i ∈ s, f i)
⊢ f a * ∏ i ∈ s, f i ≤ g a * ∏ i ∈ s, g i
have cons₁ : 0 ≤ g a
Tactic: gcongr
-- 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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
cons : LE.le.{u_2} (α := R) 0 (∏ i ∈ s, f i)
cons₁ : 0 ≤ g a
⊢ f a * ∏ i ∈ s, f i ≤ g a * ∏ i ∈ s, g i
have cons₂ : f a ≤ g a
Tactic: gcongr
-- 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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
h0 : 0 ≤ f a ∧ ∀ x ∈ s, 0 ≤ f x
h1 : f a ≤ g a ∧ ∀ x ∈ s, f x ≤ g x
this : MulPosMono R
cons : LE.le.{u_2} (α := R) 0 (∏ i ∈ s, f i)
cons₁ : 0 ≤ g a
cons₂ : f a ≤ g a
⊢ f a * ∏ i ∈ s, f i ≤ g a * ∏ i ∈ s, g i
have cons₃ : LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
Tactic: gcongr
-- 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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ g i
⊢ LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have empty : ∀ (h0 : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ f i)
  (h1 : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≤ g i), LE.le.{u_2} (α := R) (∏ i ∈ ∅, f i) (∏ i ∈ ∅, g i)
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons a s has ih =>
    simp only [prod_cons, forall_mem_cons] at h0 h1 ⊢
    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
    gcongr
    exacts [prod_nonneg h0.2, h0.1.trans h1.1, h1.1, ih h0.2 h1.2]
Cleared hypotheses: h0, h1
-- 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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f g : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ g i
empty :
  ∀ (h0 : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → 0 ≤ f i)
    (h1 : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → f i ≤ g i), LE.le.{u_2} (α := R) (∏ i ∈ ∅, f i) (∏ i ∈ ∅, g i)
⊢ LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have cons : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (ih : ∀ (h0 : ∀ i ∈ s, 0 ≤ f i) (h1 : ∀ i ∈ s, f i ≤ g i), LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i))
  (h0 : ∀ i ∈ cons a s has, 0 ≤ f i) (h1 : ∀ i ∈ cons a s has, f i ≤ g i),
  LE.le.{u_2} (α := R) (∏ i ∈ cons a s has, f i) (∏ i ∈ cons a s has, g i)
Tactic: induction s using Finset.cons_induction with
  | empty => simp
  | cons a s has ih =>
    simp only [prod_cons, forall_mem_cons] at h0 h1 ⊢
    have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
    gcongr
    exacts [prod_nonneg h0.2, h0.1.trans h1.1, h1.1, ih h0.2 h1.2]
Cleared hypotheses: h0, h1
-- 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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s : Finset ι
h0 : ∀ i ∈ s, 0 ≤ f i
h1 : ∀ i ∈ s, f i ≤ 1
⊢ LE.le.{u_2} (α := R) (∏ i ∈ s, f i) 1
have h : Eq.{u_2 + 1} (α := R) (∏ i ∈ s, 1) 1
Tactic: convert! ← prod_le_prod h0 h1
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
⊢ f i ≤ ∏ i ∈ s, max (f i) 1
have inl : ∀ (hf : f i < 0), f i ≤ ∏ i ∈ s, max (f i) 1
Tactic: rcases lt_or_ge (f i) 0 with hf | hf
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
inl : ∀ (hf : f i < 0), f i ≤ ∏ i ∈ s, max (f i) 1
⊢ f i ≤ ∏ i ∈ s, max (f i) 1
have inr : ∀ (hf : 0 ≤ f i), f i ≤ ∏ i ∈ s, max (f i) 1
Tactic: rcases lt_or_ge (f i) 0 with hf | hf
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
⊢ f i = ∏ j ∈ s, if i = j then f i else 1
have rw : f i = if i = i then f i else 1
Tactic: rw [prod_eq_single_of_mem i hi fun _ _ _ ↦ by grind]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (hypothesis)
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
hf : 0 ≤ f i
⊢ f i ≤ ∏ i ∈ s, max (f i) 1
have this : f i = ∏ j ∈ s, if i = j then f i else 1
Tactic: have : f i = ∏ j ∈ s, if i = j then f i else 1 := by
    rw [prod_eq_single_of_mem i hi fun _ _ _ ↦ by grind]
    simp
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
⊢ f i ≤ ∏ i ∈ s, max (f i) 1
have inl : ∀ (hf : f i < 0), f i ≤ ∏ i ∈ s, max (f i) 1
Tactic: classical
  rcases lt_or_ge (f i) 0 with hf | hf
  · exact (hf.trans_le <| prod_nonneg fun _ _ ↦ le_sup_of_le_right zero_le_one).le
  have : f i = ∏ j ∈ s, if i = j then f i else 1 := by
    rw [prod_eq_single_of_mem i hi fun _ _ _ ↦ by grind]
    simp
  exact this ▸ prod_le_prod (fun _ _ ↦ by grind [zero_le_one]) fun _ _ ↦ by grind
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
inl : ∀ (hf : f i < 0), f i ≤ ∏ i ∈ s, max (f i) 1
⊢ f i ≤ ∏ i ∈ s, max (f i) 1
have inr : ∀ (hf : 0 ≤ f i), f i ≤ ∏ i ∈ s, max (f i) 1
Tactic: classical
  rcases lt_or_ge (f i) 0 with hf | hf
  · exact (hf.trans_le <| prod_nonneg fun _ _ ↦ le_sup_of_le_right zero_le_one).le
  have : f i = ∏ j ∈ s, if i = j then f i else 1 := by
    rw [prod_eq_single_of_mem i hi fun _ _ _ ↦ by grind]
    simp
  exact this ▸ prod_le_prod (fun _ _ ↦ by grind [zero_le_one]) fun _ _ ↦ by grind
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (goal)
Goal:
ι : Type u_1
s : Finset ι
M : Type u_4
inst : CommMonoidWithZero M
inst_1 : LinearOrder M
inst_2 : ZeroLEOneClass M
inst_3 : PosMulMono M
i : ι
hi : i ∈ s
f : ι → M
inl : ∀ (hf : f i < 0), f i ≤ ∏ i ∈ s, max (f i) 1
inr inr₁ : ∀ (hf : 0 ≤ f i), f i ≤ ∏ i ∈ s, max (f i) 1
⊢ f i ≤ ∏ i ∈ s, max (f i) 1
have inr₂ : ∀ (hf : 0 ≤ f i) (this : f i = ∏ j ∈ s, if i = j then f i else 1), f i ≤ ∏ i ∈ s, max (f i) 1
Tactic: classical
  rcases lt_or_ge (f i) 0 with hf | hf
  · exact (hf.trans_le <| prod_nonneg fun _ _ ↦ le_sup_of_le_right zero_le_one).le
  have : f i = ∏ j ∈ s, if i = j then f i else 1 := by
    rw [prod_eq_single_of_mem i hi fun _ _ _ ↦ by grind]
    simp
  exact this ▸ prod_le_prod (fun _ _ ↦ by grind [zero_le_one]) fun _ _ ↦ by grind
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
⊢ LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ t, f i)
have this : MulPosMono R
Tactic: have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
-- 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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
this : MulPosMono R
⊢ Eq.{u_2 + 1} (α := R) (∏ i ∈ t \ s ∪ s, f i) (∏ i ∈ t, f i)
have rw : Eq.{u_2 + 1} (α := R) (∏ i ∈ t, f i) (∏ i ∈ t, f i)
Tactic: rw [sdiff_union_of_subset h]
-- 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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
this : MulPosMono R
⊢ LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ t, f i)
have i : Eq.{u_2 + 1} (α := R) (∏ i ∈ t \ s ∪ s, f i) (∏ i ∈ t, f i)
Tactic: calc
      ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
        le_mul_of_one_le_left (prod_nonneg hf0) <| one_le_prod <| by simpa only [mem_sdiff, and_imp]
      _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
      _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]
-- 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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ s, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i
this : MulPosMono R
⊢ LE.le.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ t, f i)
have i : Eq.{u_2 + 1} (α := R) (∏ i ∈ t \ s ∪ s, f i) (∏ i ∈ t, f i)
Tactic: classical
  calc
      ∏ i ∈ s, f i ≤ (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i :=
        le_mul_of_one_le_left (prod_nonneg hf0) <| one_le_prod <| by simpa only [mem_sdiff, and_imp]
      _ = ∏ i ∈ t \ s ∪ s, f i := (prod_union sdiff_disjoint).symm
      _ = ∏ i ∈ t, f i := by rw [sdiff_union_of_subset h]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (hypothesis)
Goal:
ι : Type u_1
R : Type u_2
inst : CommMonoidWithZero R
inst_1 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
⊢ LE.le.{u_2} (α := R) (∏ i ∈ t, f i) (∏ i ∈ s, f i)
have this : MulPosMono R
Tactic: have := posMulMono_iff_mulPosMono.1 ‹PosMulMono R›
-- 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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
⊢ Eq.{u_2 + 1} (α := R) (∏ i ∈ t, f i) (∏ i ∈ t \ s ∪ s, f i)
have rw : Eq.{u_2 + 1} (α := R) (∏ i ∈ t, f i) (∏ i ∈ t, f i)
Tactic: rw [sdiff_union_of_subset h]
-- 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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
⊢ LE.le.{u_2} (α := R) (∏ i ∈ t, f i) (∏ i ∈ s, f i)
have i : Eq.{u_2 + 1} (α := R) (∏ i ∈ t, f i) (∏ i ∈ t \ s ∪ s, f i)
Tactic: calc
    ∏ i ∈ t, f i = ∏ i ∈ t \ s ∪ s, f i := by rw [sdiff_union_of_subset h]
    _ = (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i := prod_union sdiff_disjoint
    _ ≤ ∏ i ∈ s, f i :=
      mul_le_of_le_one_left (prod_nonneg (by grind)) (prod_le_one (by grind) (by grind))
-- 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 : Preorder R
inst_2 : ZeroLEOneClass R
inst_3 : PosMulMono R
f : ι → R
s t : Finset ι
h : s ⊆ t
hf0 : ∀ i ∈ t, 0 ≤ f i
hf : ∀ i ∈ t, i ∉ s → f i ≤ 1
this : MulPosMono R
⊢ LE.le.{u_2} (α := R) (∏ i ∈ t, f i) (∏ i ∈ s, f i)
have i : Eq.{u_2 + 1} (α := R) (∏ i ∈ t, f i) (∏ i ∈ t \ s ∪ s, f i)
Tactic: classical
  calc
    ∏ i ∈ t, f i = ∏ i ∈ t \ s ∪ s, f i := by rw [sdiff_union_of_subset h]
    _ = (∏ i ∈ t \ s, f i) * ∏ i ∈ s, f i := prod_union sdiff_disjoint
    _ ≤ ∏ i ∈ s, f i :=
      mul_le_of_le_one_left (prod_nonneg (by grind)) (prod_le_one (by grind) (by grind))
-- 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
⊢ LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have obtain : ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i), LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
Tactic: obtain ⟨i, hi, hilt⟩ := hlt
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
i : ι
hi : i ∈ s
hilt : f i < g i
⊢ LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have rw : f i * ∏ x ∈ s.erase i, f x < g i * ∏ x ∈ s.erase i, g x
Tactic: rw [← insert_erase hi, prod_insert (notMem_erase _ _), prod_insert (notMem_erase _ _)]
-- Lean 4 proof step from Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset (hypothesis)
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
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
have this : MulPosStrictMono R
Tactic: have := posMulStrictMono_iff_mulPosStrictMono.1 ‹PosMulStrictMono R›
-- 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
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
have refine_1 : LE.le.{u_2} (α := R) (∏ x ∈ s.erase i, f x) (∏ x ∈ s.erase i, g x)
Tactic: refine mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_
-- 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
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
refine_1 : LE.le.{u_2} (α := R) (∏ x ∈ s.erase i, f x) (∏ x ∈ s.erase i, g x)
⊢ f i * ∏ x ∈ s.erase i, f x < g i * ∏ x ∈ s.erase i, g x
have refine_2 : LT.lt.{u_2} (α := R) 0 (∏ x ∈ s.erase i, f x)
Tactic: refine mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_
-- 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
i : ι
hi : i ∈ s
hilt : f i < g i
this : MulPosStrictMono R
refine_1 : LE.le.{u_2} (α := R) (∏ x ∈ s.erase i, f x) (∏ x ∈ s.erase i, g x)
refine_2 : LT.lt.{u_2} (α := R) 0 (∏ x ∈ s.erase i, f x)
⊢ f i * ∏ x ∈ s.erase i, f x < g i * ∏ x ∈ s.erase i, g x
have refine_3 : 0 ≤ g i
Tactic: refine mul_lt_mul_of_pos_of_nonneg' hilt ?_ ?_ ?_
-- 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
⊢ LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have obtain : ∀ (i : ι) (hi : i ∈ s) (hilt : f i < g i), LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, 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
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)
⊢ LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have 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
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
⊢ LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have 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
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
⊢ LT.lt.{u_2} (α := R) (∏ i ∈ s, f i) (∏ i ∈ s, g i)
have 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)
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