-- Mathlib/Analysis/Normed/Ring/SeminormFromBounded.lean
theorem seminormFromBounded_add (f_nonneg : 0 ≤ f)
    (f_mul : ∀ x y : R, f (x * y) ≤ c * f x * f y)
    (f_add : ∀ a b, f (a + b) ≤ f a + f b) (x y : R) :
    seminormFromBounded' f (x + y) ≤ seminormFromBounded' f x + seminormFromBounded' f y

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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
hz : f z = 0
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z

Tactic:
simp only [hz, div_zero, zero_add, le_refl, or_self_iff]

Result:
no goals

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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
hf : f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x + seminormFromBounded' f y

Tactic:
exact le_trans hf (add_le_add
  (le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z (le_refl _))
  (le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) z (le_refl _)))

Result:
no goals

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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y : R
⊢ seminormFromBounded' f (x + y) ≤ seminormFromBounded' f x + seminormFromBounded' f y

Tactic:
refine ciSup_le (fun z ↦ ?_)

Result:
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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x + seminormFromBounded' f y

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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
hz : ¬f z = 0
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z

Tactic:
rw [div_add_div_same, div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz), add_mul]

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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
hz : ¬f z = 0
⊢ f (x * z + y * z) ≤ f (x * z) + f (y * z)

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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x + seminormFromBounded' f y

Tactic:
suffices hf : f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z by
  exact le_trans hf (add_le_add
    (le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z (le_refl _))
    (le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) z (le_refl _)))

Result:
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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z

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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
hz : ¬f z = 0
⊢ f (x * z + y * z) ≤ f (x * z) + f (y * z)

Tactic:
exact f_add _ _

Result:
no goals

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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z

Tactic:
by_cases hz : f z = 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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
hz : f z = 0
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z

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
f_add : ∀ (a b : R), f (a + b) ≤ f a + f b
x y z : R
hz : ¬f z = 0
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z