-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_ge (f_nonneg : 0 ≤ f)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) (x : R) :
    f x ≤ f 1 * seminormFromBounded' f x

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
h1 : ¬f 1 = 0
⊢ f x / f 1 ≤ seminormFromBounded' f x

Tactic:
conv_lhs => rw [← mul_one x]

Result:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
h1 : ¬f 1 = 0
⊢ f (x * 1) / f 1 ≤ seminormFromBounded' f x

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
h1 : f 1 = 0
f_mul : f x ≤ 0
⊢ f x ≤ f 1 * seminormFromBounded' f x

Tactic:
have hx0 : f x = 0 := f_mul.antisymm (f_nonneg _)

Result:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
h1 : f 1 = 0
f_mul : f x ≤ 0
hx0 : f x = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
h1 : ¬f 1 = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x

Tactic:
rw [mul_comm, ← div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) h1)]

Result:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
h1 : ¬f 1 = 0
⊢ f x / f 1 ≤ seminormFromBounded' f x

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
h1 : f 1 = 0
f_mul : f (x * 1) ≤ c * f x * f 1
⊢ f x ≤ f 1 * seminormFromBounded' f x

Tactic:
rw [mul_one, h1, mul_zero] at f_mul

Result:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
h1 : f 1 = 0
f_mul : f x ≤ 0
⊢ f x ≤ f 1 * seminormFromBounded' f x

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
h1 : f 1 = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x

Tactic:
specialize f_mul x 1

Result:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
h1 : f 1 = 0
f_mul : f (x * 1) ≤ c * f x * f 1
⊢ f x ≤ f 1 * seminormFromBounded' f x

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
⊢ f x ≤ f 1 * seminormFromBounded' f x

Tactic:
by_cases h1 : f 1 = 0

Result:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
h1 : f 1 = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x

case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
h1 : ¬f 1 = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
h1 : f 1 = 0
f_mul : f x ≤ 0
hx0 : f x = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x

Tactic:
rw [hx0, h1, zero_mul]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
h1 : ¬f 1 = 0
⊢ f (x * 1) / f 1 ≤ seminormFromBounded' f x

Tactic:
exact le_ciSup (seminormFromBounded_bddAbove_range f_nonneg f_mul x) (1 : R)

Result:
no goals