α : Type u_1
inst✝ : CancelCommMonoidWithZero α
b : FactorSet α
h : none ≤ b
this : b = ⊤
⊢ FactorSet.prod none ≤ FactorSet.prod b
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
b : FactorSet α
h : none ≤ b
⊢ FactorSet.prod none ≤ FactorSet.prod b
have : b = ⊤ := top_unique h
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
b : FactorSet α
h : none ≤ b
this : b = ⊤
⊢ FactorSet.prod none ≤ 0
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
b : FactorSet α
h : none ≤ b
this : b = ⊤
⊢ FactorSet.prod none ≤ FactorSet.prod b
rw [this, prod_top]
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
b : FactorSet α
h : none ≤ b
this : b = ⊤
⊢ FactorSet.prod none ≤ 0
exact le_rfl
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : FactorSet α
x✝ : a ≤ none
⊢ FactorSet.prod a ≤ 0
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : FactorSet α
x✝ : a ≤ none
⊢ FactorSet.prod a ≤ FactorSet.prod ⊤
simp
no goals
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
a : FactorSet α
x✝ : a ≤ none
⊢ FactorSet.prod a ≤ 0
exact le_top