awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
pos :
  ∀ (hy : seminormFromBounded' f y = 0) (x_1 : R),
    f (x * y * x_1) / f x_1 ≤ seminormFromBounded' f x * seminormFromBounded' f y
neg :
  ∀ (hy : ¬seminormFromBounded' f y = 0) (x_1 : R),
    f (x * y * x_1) / f x_1 ≤ seminormFromBounded' f x * seminormFromBounded' f y
⊢ ∀ (x_1 : R), f (x * y * x_1) / f x_1 ≤ seminormFromBounded' f x * seminormFromBounded' f y

Tactic:
by_cases hy : seminormFromBounded' f y = 0

Premises used: seminormFromBounded'
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : seminormFromBounded' f y = 0
⊢ f y = 0

Tactic:
rw [seminormFromBounded_eq_zero_iff f_nonneg f_mul] at hy

Premises used: seminormFromBounded_eq_zero_iff
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : f y = 0
z : R
pos : 0 ≤ seminormFromBounded' f x * seminormFromBounded' f y
⊢ f (x * y * z) / f z ≤ seminormFromBounded' f x * seminormFromBounded' f y

Tactic:
rw [mul_comm x y, mul_assoc, map_mul_zero_of_map_zero f_nonneg f_mul hy (x * z), zero_div]

Premises used: map_mul_zero_of_map_zero, HMul.hMul, mul_assoc, zero_div, mul_comm
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : f y = 0
z : R
⊢ 0 ≤ seminormFromBounded' f x * seminormFromBounded' f y

Tactic:
mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul x)
      (seminormFromBounded_nonneg f_nonneg f_mul y)

Premises used: mul_nonneg, seminormFromBounded_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : f y = 0
z : R
⊢ 0 ≤ seminormFromBounded' f x * seminormFromBounded' f y

Tactic:
exact mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul x)
      (seminormFromBounded_nonneg f_nonneg f_mul y)

Premises used: mul_nonneg, seminormFromBounded_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
neg : f (x * y * z) / f z / seminormFromBounded' f y ≤ seminormFromBounded' f x
⊢ f (x * y * z) / f z ≤ seminormFromBounded' f x * seminormFromBounded' f y

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

Premises used: div_le_iff₀, seminormFromBounded_nonneg, lt_of_le_of_ne'
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
neg : f (x * y * z) / f z / seminormFromBounded' f y ≤ f (x * z) / f z
⊢ f (x * y * z) / f z / seminormFromBounded' f y ≤ seminormFromBounded' f x

Tactic:
apply le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z

Premises used: le_ciSup_of_le, seminormFromBounded_bddAbove_range
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
neg : f (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z
⊢ f (x * y * z) / f z / seminormFromBounded' f y ≤ f (x * z) / f z

Tactic:
rw [div_le_iff₀ (lt_of_le_of_ne' (seminormFromBounded_nonneg f_nonneg f_mul _) hy),
      div_mul_eq_mul_div]

Premises used: div_le_iff₀, div_mul_eq_mul_div, seminormFromBounded_nonneg, lt_of_le_of_ne'
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
pos : ∀ (hz : f z = 0), f (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z
neg : ∀ (hz : ¬f z = 0), f (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z
⊢ f (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z

Tactic:
by_cases hz : f z = 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : f z = 0
⊢ f (z * (x * y)) = 0

Tactic:
have hxyz : f (z * (x * y)) = 0 := map_mul_zero_of_map_zero f_nonneg f_mul hz _
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : f z = 0
hxyz : f (z * (x * y)) = 0
pos : 0 ≤ seminormFromBounded' f y * f (x * z) / f z
⊢ f (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z

Tactic:
simp_rw [mul_comm, hxyz, zero_div]

Premises used: zero_div, mul_comm
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : f z = 0
hxyz : f (z * (x * y)) = 0
⊢ 0 ≤ seminormFromBounded' f y * f (x * z) / f z

Tactic:
div_nonneg (mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul y) (f_nonneg _))
        (f_nonneg _)

Premises used: mul_nonneg, seminormFromBounded_nonneg, div_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : f z = 0
hxyz : f (z * (x * y)) = 0
⊢ 0 ≤ seminormFromBounded' f y * f (x * z) / f z

Tactic:
exact div_nonneg (mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul y) (f_nonneg _))
        (f_nonneg _)

Premises used: mul_nonneg, seminormFromBounded_nonneg, div_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : ¬f z = 0
neg : f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)
⊢ f (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z

Tactic:
rw [div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz), mul_comm (f (x * z))]

Premises used: HMul.hMul, div_le_div_iff_of_pos_right, lt_of_le_of_ne', mul_comm
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : ¬f z = 0
pos : ∀ (hxz : f (x * z) = 0), f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)
neg : ∀ (hxz : ¬f (x * z) = 0), f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)
⊢ f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)

Tactic:
by_cases hxz : f (x * z) = 0

Premises used: HMul.hMul
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : ¬f z = 0
hxz : f (x * z) = 0
pos : 0 ≤ seminormFromBounded' f y * f (x * z)
⊢ f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)

Tactic:
rw [mul_comm x y, mul_assoc, mul_comm y, map_mul_zero_of_map_zero f_nonneg f_mul hxz y]

Premises used: map_mul_zero_of_map_zero, mul_assoc, mul_comm
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : ¬f z = 0
hxz : f (x * z) = 0
⊢ 0 ≤ seminormFromBounded' f y * f (x * z)

Tactic:
mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul y) (f_nonneg _)

Premises used: mul_nonneg, seminormFromBounded_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : ¬f z = 0
hxz : f (x * z) = 0
⊢ 0 ≤ seminormFromBounded' f y * f (x * z)

Tactic:
exact mul_nonneg (seminormFromBounded_nonneg f_nonneg f_mul y) (f_nonneg _)

Premises used: mul_nonneg, seminormFromBounded_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : ¬f z = 0
hxz : ¬f (x * z) = 0
neg : f (x * y * z) / f (x * z) ≤ seminormFromBounded' f y
⊢ f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)

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

Premises used: div_le_iff₀, lt_of_le_of_ne'
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : ¬f z = 0
hxz : ¬f (x * z) = 0
neg : f (x * y * z) / f (x * z) ≤ f (y * (x * z)) / f (x * z)
⊢ f (x * y * z) / f (x * z) ≤ seminormFromBounded' f y

Tactic:
apply le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) (x * z)

Premises used: HMul.hMul, le_ciSup_of_le, seminormFromBounded_bddAbove_range
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 y : R
hy : ¬seminormFromBounded' f y = 0
z : R
hz : ¬f z = 0
hxz : ¬f (x * z) = 0
neg : f (x * y * z) ≤ f (y * (x * z))
neg₁ : f (y * x * z) ≤ f (y * (x * z))
neg₂ neg₃ : f (y * (x * z)) ≤ f (y * (x * z))
⊢ f (x * y * z) / f (x * z) ≤ f (y * (x * z)) / f (x * z)

Tactic:
rw [div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hxz), mul_comm x y, mul_assoc]

Premises used: mul_assoc, div_le_div_iff_of_pos_right, lt_of_le_of_ne', mul_comm
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
simp_rw : Eq (α := ℝ) (⨆ (y : R), f y / f y) 1
⊢ seminormFromBounded' f 1 = 1

Tactic:
simp_rw [seminormFromBounded', one_mul]

Premises used: seminormFromBounded', one_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
a : LE.le (α := ℝ) (⨆ (y : R), f y / f y) 1
a₁ : LE.le (α := ℝ) 1 (⨆ (y : R), f y / f y)
⊢ Eq (α := ℝ) (⨆ (y : R), f y / f y) 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ LE.le (α := ℝ) (⨆ (y : R), f y / f y) 1

Tactic:
ciSup_le (fun x ↦ ?_)

Premises used: ciSup_le
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
a : ∀ (x : R), f x / f x ≤ 1
⊢ LE.le (α := ℝ) (⨆ (y : R), f y / f y) 1

Tactic:
refine ciSup_le (fun x ↦ ?_)

Premises used: ciSup_le
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
pos : ∀ (hx : f x = 0), f x / f x ≤ 1
neg : ∀ (hx : ¬f x = 0), f x / f x ≤ 1
⊢ f x / f x ≤ 1

Tactic:
by_cases hx : f x = 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x = 0
pos : LE.le (α := ℝ) 0 1
⊢ f x / f x ≤ 1

Tactic:
rw [hx, div_zero]

Premises used: div_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x = 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : f x = 0
⊢ LE.le (α := ℝ) 0 1

Tactic:
exact zero_le_one

Premises used: zero_le_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ¬f x = 0
neg neg₁ : LE.le (α := ℝ) 1 1
⊢ f x / f x ≤ 1

Tactic:
rw [div_self hx]

Premises used: div_self
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
a : f 1 / f 1 ≤ ⨆ (y : R), f y / f y
⊢ LE.le (α := ℝ) 1 (⨆ (y : R), f y / f y)

Tactic:
rw [← div_self (map_one_ne_zero f_ne_zero f_nonneg f_mul)]

Premises used: map_one_ne_zero, div_self
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (y : R) ↦ f y / f y)) 1
⊢ BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f y / f y)

Tactic:
use (1 : ℝ)

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
y : R
pos : ∀ (hy : f y = 0), LE.le (α := ℝ) ((fun (y : R) ↦ f y / f y) y) 1
neg : ∀ (hy : ¬f y = 0), LE.le (α := ℝ) ((fun (y : R) ↦ f y / f y) y) 1
⊢ LE.le (α := ℝ) ((fun (y : R) ↦ f y / f y) y) 1

Tactic:
by_cases hy : f y = 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
y : R
hy : f y = 0
⊢ LE.le (α := ℝ) ((fun (y : R) ↦ f y / f y) y) 1

Tactic:
simp only [hy, div_zero, zero_le_one]

Premises used: zero_le_one, div_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
y : R
hy : ¬f y = 0
⊢ LE.le (α := ℝ) ((fun (y : R) ↦ f y / f y) y) 1

Tactic:
simp only [div_self hy, le_refl]

Premises used: le_refl, div_self
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f y / f y)

Tactic:
have h_bdd : BddAbove (Set.range fun y ↦ f y / f y) := by
      use (1 : ℝ)
      rintro r ⟨y, rfl⟩
      by_cases hy : f y = 0
      · simp only [hy, div_zero, zero_le_one]
      · simp only [div_self hy, le_refl]
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h_bdd : BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f y / f y)
⊢ f 1 / f 1 ≤ ⨆ (y : R), f y / f y

Tactic:
le_ciSup h_bdd (1 : R)

Premises used: le_ciSup, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_ne_zero : f ≠ 0
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h_bdd : BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f y / f y)
⊢ f 1 / f 1 ≤ ⨆ (y : R), f y / f y

Tactic:
exact le_ciSup h_bdd (1 : R)

Premises used: le_ciSup, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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
pos : ∀ (f_ne_zero : f ≠ 0), seminormFromBounded' f 1 ≤ 1
neg : ∀ (f_ne_zero : f = 0), seminormFromBounded' f 1 ≤ 1
⊢ seminormFromBounded' f 1 ≤ 1

Tactic:
by_cases! f_ne_zero : f ≠ 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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_ne_zero : f ≠ 0
⊢ seminormFromBounded' f 1 ≤ 1

Tactic:
le_of_eq (seminormFromBounded_one f_ne_zero f_nonneg f_mul)

Premises used: seminormFromBounded_one, le_of_eq
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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_ne_zero : f ≠ 0
⊢ seminormFromBounded' f 1 ≤ 1

Tactic:
exact le_of_eq (seminormFromBounded_one f_ne_zero f_nonneg f_mul)

Premises used: seminormFromBounded_one, le_of_eq
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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_ne_zero : f = 0
neg : LE.le (α := ℝ) (⨆ (y : R), f y / f y) 1
⊢ seminormFromBounded' f 1 ≤ 1

Tactic:
simp_rw [seminormFromBounded', one_mul]

Premises used: seminormFromBounded', one_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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_ne_zero : f = 0
⊢ LE.le (α := ℝ) (⨆ (y : R), f y / f y) 1

Tactic:
ciSup_le (fun _ ↦ ?_)

Premises used: ciSup_le
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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_ne_zero : f = 0
neg : ∀ (x : R), f x / f x ≤ 1
⊢ LE.le (α := ℝ) (⨆ (y : R), f y / f y) 1

Tactic:
refine ciSup_le (fun _ ↦ ?_)

Premises used: ciSup_le
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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_ne_zero : f = 0
x : R
⊢ f x / f x ≤ 1

Tactic:
simp only [f_ne_zero, Pi.zero_apply, div_zero, zero_le_one]

Premises used: Pi.zero_apply, zero_le_one, div_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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:
ciSup_le (fun z ↦ ?_)

Premises used: seminormFromBounded', ciSup_le
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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
refine : ∀ (z : R), f ((x + y) * z) / f z ≤ seminormFromBounded' f x + seminormFromBounded' f y
⊢ seminormFromBounded' f (x + y) ≤ seminormFromBounded' f x + seminormFromBounded' f y

Tactic:
refine ciSup_le (fun z ↦ ?_)

Premises used: ciSup_le
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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:
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 _)))

Premises used: le_refl, le_ciSup_of_le, add_le_add, seminormFromBounded_bddAbove_range, le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 _)))

Premises used: le_refl, le_ciSup_of_le, add_le_add, seminormFromBounded_bddAbove_range, le_trans
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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
suffices : 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:
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 _)))
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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
pos : ∀ (hz : f z = 0), f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z
neg : ∀ (hz : ¬f z = 0), f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z

Tactic:
by_cases hz : f z = 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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]

Premises used: le_refl, zero_add, div_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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
neg : f (x * z + y * z) ≤ f (x * z) + f (y * z)
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z

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

Premises used: add_mul, div_le_div_iff_of_pos_right, lt_of_le_of_ne', add_div
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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:
f_add _ _
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 _ _
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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:
fun x y ↦ ciSup_le (fun z ↦ ?_)

Premises used: seminormFromBounded', IsNonarchimedean, ciSup_le