-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_aux (f_nonneg : 0 ≤ f)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y) (x : R) : 0 ≤ c * 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
hx : 0 < f x
⊢ 0 ≤ c

Tactic:
specialize f_mul x 1

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : 0 < f x
f_mul : f (x * 1) ≤ c * f x * f 1
⊢ 0 ≤ c

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
⊢ 0 ≤ c * f x

Tactic:
rcases (f_nonneg x).eq_or_gt with hx | hx

Result:
case inl
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
hx : f x = 0 x
⊢ 0 ≤ c * f x

case inr
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
hx : 0 x < f x
⊢ 0 ≤ c * f x

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
f_nonneg : 0 ≤ f 1
h1 : f 1 = 0
⊢ 1 ≤ 0

Tactic:
simpa [h1] using f_mul

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
⊢ 0 ≤ c

Tactic:
replace f_nonneg : 0 ≤ f 1 := f_nonneg 1

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
f_nonneg : 0 ≤ f 1
⊢ 0 ≤ c

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : 0 < f x
f_mul : f x ≤ c * f x * f 1
⊢ c * f x * f 1 = c * f 1 * f x

Tactic:
ring

Result:
no goals

Proof state:
case inr
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
hx : 0 < f x
hc : 0 ≤ c
⊢ 0 ≤ c * f x

Tactic:
positivity

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : 0 < f x
f_mul : f (x * 1) ≤ c * f x * f 1
⊢ 0 ≤ c

Tactic:
rw [mul_one, show c * f x * f 1 = c * f 1 * f x by ring, le_mul_iff_one_le_left hx] at f_mul

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
⊢ 0 ≤ c

Proof state:
case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 / f 1 ≤ c
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
⊢ 0 ≤ c

Tactic:
linarith [one_div_pos.mpr h1]

Result:
no goals

Proof state:
case inl
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
hx : f x = 0 x
⊢ 0 ≤ c * f x

Tactic:
simp [hx]

Result:
no goals

Proof state:
case inr
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
hx : 0 x < f x
⊢ 0 ≤ c * f x

Tactic:
change 0 < f x at hx

Result:
case inr
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
hx : 0 < f x
⊢ 0 ≤ c * f x

Proof state:
case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
⊢ 0 ≤ c

Tactic:
rw [← div_le_iff₀ h1] at f_mul

Result:
case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 / f 1 ≤ c
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
⊢ 0 ≤ c

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
f_nonneg : 0 ≤ f 1
⊢ 0 ≤ c

Tactic:
rcases f_nonneg.eq_or_gt with h1 | h1

Result:
case inl
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
f_nonneg : 0 ≤ f 1
h1 : f 1 = 0
⊢ 0 ≤ c

case inr
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
⊢ 0 ≤ c

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

Tactic:
linarith [show (1 : ℝ) ≤ 0 by simpa [h1] using f_mul]

Result:
no goals