-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_of_mul_le (f_nonneg : 0 ≤ f) {x : R}
    (hx : ∀ y : R, f (x * y) ≤ f x * f y) (h_one : f 1 ≤ 1) : seminormFromBounded' f x = f x

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : ¬f y = 0
⊢ f (x * y) ≤ f x * f y

Tactic:
exact hx y

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
⊢ f (x * y) / f y ≤ f x

Tactic:
by_cases hy : f y = 0

Result:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy : f y = 0
⊢ f (x * y) / f y ≤ f x

case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy : ¬f y = 0
⊢ f (x * y) / f y ≤ f x

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : f y = 0
⊢ 0 ≤ f x

Tactic:
exact f_nonneg _

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy : f y = 0
⊢ f (x * y) / f y ≤ f x

Tactic:
rw [hy, div_zero]

Result:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy : f y = 0
⊢ 0 ≤ f x

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
h0 : ¬f x = 0
hx : 1 ≤ f 1
⊢ 1 ≤ f 1

Tactic:
exact hx

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
h0 : ¬f x = 0
⊢ f 1 = 1

Tactic:
apply h_one.antisymm

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
h0 : ¬f x = 0
⊢ 1 ≤ f 1

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
⊢ ⨆ y, f (x * y) / f y = f x

Tactic:
apply le_antisymm

Result:
case a
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
⊢ ⨆ y, f (x * y) / f y ≤ f x

case a
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
⊢ f x ≤ ⨆ y, f (x * y) / f y

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
⊢ ⨆ y, f (x * y) / f y ≤ f x

Tactic:
refine ciSup_le (fun y ↦ ?_)

Result:
case a
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
⊢ f (x * y) / f y ≤ f x

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
h0 : ¬f x = 0
⊢ f x = f (x * 1) / f 1

Tactic:
have heq : f 1 = 1 := by
  apply h_one.antisymm
  specialize hx 1
  rw [mul_one, le_mul_iff_one_le_right (lt_of_le_of_ne (f_nonneg _) (Ne.symm h0))] at hx
  exact hx

Result:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
h0 : ¬f x = 0
heq : f 1 = 1
⊢ f x = f (x * 1) / f 1

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
h0 : ¬f x = 0
hx : f (x * 1) ≤ f x * f 1
⊢ 1 ≤ f 1

Tactic:
rw [mul_one, le_mul_iff_one_le_right (lt_of_le_of_ne (f_nonneg _) (Ne.symm h0))] at hx

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
h0 : ¬f x = 0
hx : 1 ≤ f 1
⊢ 1 ≤ f 1

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
h0 : ¬f x = 0
heq : f 1 = 1
⊢ f x = f (x * 1) / f 1

Tactic:
rw [heq, mul_one, div_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
⊢ BddAbove (Set.range fun y => f (x * y) / f y)

Tactic:
use f x

Result:
case h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
⊢ f x ∈ upperBounds (Set.range fun y => f (x * y) / f y)

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : ¬f y = 0
⊢ (fun y => f (x * y) / f y) y ≤ f x

Tactic:
rw [← mul_one (f x), ← div_self hy0, ← mul_div_assoc,
  div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) hy0), mul_div_assoc, div_self hy0, mul_one]

Result:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy0 : ¬f y = 0
⊢ f (x * y) ≤ f x * f y

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

Tactic:
simp_rw [seminormFromBounded']

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
⊢ ⨆ y, f (x * y) / f y = f x

Proof state:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
h0 : ¬f x = 0
⊢ 1 ≤ f 1

Tactic:
specialize hx 1

Result:
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
h0 : ¬f x = 0
hx : f (x * 1) ≤ f x * f 1
⊢ 1 ≤ f 1

Proof state:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy : ¬f y = 0
⊢ f (x * y) / f y ≤ f x

Tactic:
rw [div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) hy)]

Result:
case neg
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy : ¬f y = 0
⊢ f (x * y) ≤ f x * f y

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
⊢ f x ∈ upperBounds (Set.range fun y => f (x * y) / f y)

Tactic:
rintro r ⟨y, rfl⟩

Result:
case h.intro
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
⊢ (fun y => f (x * y) / f y) y ≤ f x

Proof state:
case pos
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
y : R
hy : f y = 0
⊢ 0 ≤ f x

Tactic:
exact f_nonneg _

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
⊢ f x ≤ ⨆ y, f (x * y) / f y

Tactic:
convert le_ciSup h_bdd (1 : R)

Result:
case h.e'_3
R : Type u_1
inst✝ : CommRing R
f : R → ℝ
f_nonneg : 0 ≤ f
x : R
hx : ∀ (y : R), f (x * y) ≤ f x * f y
h_one : f 1 ≤ 1
h_bdd : BddAbove (Set.range fun y => f (x * y) / f y)
⊢ f x = f (x * 1) / f 1