case refine'_1
R : Type u
ι : Type ?u.260476
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
⊢ Multiset.prod 0 ≤ Multiset.inf 0

case refine'_2
R : Type u
ι : Type ?u.260476
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
⊢ ∀ ⦃a : Ideal R⦄ {s : Multiset (Ideal R)},
    Multiset.prod s ≤ Multiset.inf s → Multiset.prod (a ::ₘ s) ≤ Multiset.inf (a ::ₘ s)
R : Type u
ι : Type ?u.260476
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
⊢ Multiset.prod s ≤ Multiset.inf s
refine' s.induction_on _ _
case refine'_2
R : Type u
ι : Type ?u.260476
inst✝ : CommSemiring R
I J K L : Ideal R
s✝ : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod s ≤ Multiset.inf s
⊢ Multiset.prod (a ::ₘ s) ≤ Multiset.inf (a ::ₘ s)
case refine'_2
R : Type u
ι : Type ?u.260476
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
⊢ ∀ ⦃a : Ideal R⦄ {s : Multiset (Ideal R)},
    Multiset.prod s ≤ Multiset.inf s → Multiset.prod (a ::ₘ s) ≤ Multiset.inf (a ::ₘ s)
intro a s ih
case refine'_2
R : Type u
ι : Type ?u.260476
inst✝ : CommSemiring R
I J K L : Ideal R
s✝ : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod s ≤ Multiset.inf s
⊢ a * Multiset.prod s ≤ a ⊓ Multiset.inf s
case refine'_2
R : Type u
ι : Type ?u.260476
inst✝ : CommSemiring R
I J K L : Ideal R
s✝ : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod s ≤ Multiset.inf s
⊢ Multiset.prod (a ::ₘ s) ≤ Multiset.inf (a ::ₘ s)
rw [Multiset.prod_cons, Multiset.inf_cons]
no goals
case refine'_2
R : Type u
ι : Type ?u.260476
inst✝ : CommSemiring R
I J K L : Ideal R
s✝ : Multiset (Ideal R)
a : Ideal R
s : Multiset (Ideal R)
ih : Multiset.prod s ≤ Multiset.inf s
⊢ a * Multiset.prod s ≤ a ⊓ Multiset.inf s
exact le_trans mul_le_inf (inf_le_inf le_rfl ih)
case refine'_1
R : Type u
ι : Type ?u.260476
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
⊢ Multiset.prod 0 ≤ ⊤
case refine'_1
R : Type u
ι : Type ?u.260476
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
⊢ Multiset.prod 0 ≤ Multiset.inf 0
rw [Multiset.inf_zero]
no goals
case refine'_1
R : Type u
ι : Type ?u.260476
inst✝ : CommSemiring R
I J K L : Ideal R
s : Multiset (Ideal R)
⊢ Multiset.prod 0 ≤ ⊤
exact le_top