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

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
hna : IsNonarchimedean f
⊢ IsNonarchimedean (seminormFromBounded' f)

Tactic:
refine fun x y ↦ 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
hna : IsNonarchimedean f
x y z : R
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x ⊔ seminormFromBounded' f y

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
hna : IsNonarchimedean f
x y z : R
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x ⊔ seminormFromBounded' f y

Tactic:
rw [le_max_iff]

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
hna : IsNonarchimedean f
x y z : R
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x ∨ f ((x + y) * z) / f z ≤ seminormFromBounded' f y

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
hna : IsNonarchimedean f
x y z : R
hfx : f ((x + y) * z) / f z ≤ f (x * z) / f z
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x ∨ f ((x + y) * z) / f z ≤ seminormFromBounded' f y

Tactic:
exact Or.inl <| le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z hfx

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
hna : IsNonarchimedean f
x y z : R
hfy : f ((x + y) * z) / f z ≤ f (y * z) / f z
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x ∨ f ((x + y) * z) / f z ≤ seminormFromBounded' f y

Tactic:
exact Or.inr <| le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) z hfy

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
hna : IsNonarchimedean f
x y z : R
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * 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
hna : IsNonarchimedean f
x y z : R
hz : f z = 0
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * 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
hna : IsNonarchimedean f
x y z : R
hz : ¬f z = 0
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * 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
hna : IsNonarchimedean f
x y z : R
hz : ¬f z = 0
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * z) / f z ≤ f (y * z) / f z

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

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
hna : IsNonarchimedean f
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
hna : IsNonarchimedean f
x y z : R
hf : f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * z) / f z ≤ f (y * z) / f z
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x ∨ f ((x + y) * z) / f z ≤ seminormFromBounded' f y

Tactic:
rcases hf with hfx | hfy

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
hna : IsNonarchimedean f
x y z : R
hfx : f ((x + y) * z) / f z ≤ f (x * z) / f z
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x ∨ f ((x + y) * z) / f z ≤ seminormFromBounded' f y

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
hna : IsNonarchimedean f
x y z : R
hfy : f ((x + y) * z) / f z ≤ f (y * z) / f z
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x ∨ f ((x + y) * z) / f z ≤ 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
hna : IsNonarchimedean f
x y z : R
hz : ¬f z = 0
⊢ f (x * z + y * z) ≤ f (x * z) ⊔ f (y * z)

Tactic:
exact hna _ _

Result:
no goals

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
hna : IsNonarchimedean f
x y z : R
hz : f z = 0
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * z) / f z ≤ f (y * z) / f z

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

Result:
no goals