no goals
α : Type ?u.13548
β✝ : Type ?u.13551
γ : Type ?u.13554
ι : Type ?u.13557
inst✝² : NonUnitalSeminormedRing α
β : Type u_1
inst✝¹ : NormedRing β
inst✝ : Nontrivial β
⊢ ‖1‖ ≤ ‖1‖ * ‖1‖
simpa only [mul_one] using norm_mul_le (1 : β) 1