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

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

Tactic:
rw [le_max_iff]

Premises used: le_max_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
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
inl :
  ∀ (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
inr :
  ∀ (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
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x ∨ f ((x + y) * z) / f z ≤ seminormFromBounded' f y

Tactic:
rcases hf with hfx | hfy
-- 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
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:
Or.inl <| le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z hfx

Premises used: le_ciSup_of_le, Or.inl, 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
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

Premises used: le_ciSup_of_le, Or.inl, 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
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:
Or.inr <| le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) z hfy

Premises used: le_ciSup_of_le, seminormFromBounded_bddAbove_range, Or.inr
-- 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
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

Premises used: le_ciSup_of_le, seminormFromBounded_bddAbove_range, Or.inr
-- 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
x y z : R
suffices : 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:
suffices hf : f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * z) / f z ≤ f (y * z) / f z by
    rcases hf with hfx | hfy
    · exact Or.inl <| le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z hfx
    · exact Or.inr <| le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) z hfy
-- 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
x y z : R
pos : ∀ (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
neg : ∀ (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
⊢ 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
-- 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
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]

Premises used: le_refl, or_self_iff, 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
hna : IsNonarchimedean f
x y z : R
hz : ¬f z = 0
neg : f (x * z + y * z) ≤ max (f (x * z)) (f (y * z))
⊢ 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]

Premises used: add_mul, div_le_div_iff_of_pos_right, lt_of_le_of_ne', le_max_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
hna : IsNonarchimedean f
x y z : R
hz : ¬f z = 0
⊢ f (x * z + y * z) ≤ max (f (x * z)) (f (y * z))

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

Tactic:
exact hna _ _
-- 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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
simp_rw : ⨆ (y : R), f x * (f y / f y) = f x
⊢ seminormFromBounded' f x = f x

Tactic:
simp_rw [seminormFromBounded', hx, ← mul_div_assoc']

Premises used: mul_div_assoc', 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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
a : ⨆ (y : R), f x * (f y / f y) ≤ f x
a₁ : f x ≤ ⨆ (y : R), f x * (f y / f y)
⊢ ⨆ (y : R), f x * (f y / f y) = f x

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_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
⊢ ⨆ (y : R), f x * (f y / f y) ≤ f x

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_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
a : ∀ (x_1 : R), f x * (f x_1 / f x_1) ≤ f x
⊢ ⨆ (y : R), f x * (f y / f y) ≤ f x

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_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x_1 : R
hx : ∀ (y : R), f (x_1 * y) = f x_1 * f y
x : R
pos : ∀ (hx : f x = 0), f x_1 * (f x / f x) ≤ f x_1
neg : ∀ (hx : ¬f x = 0), f x_1 * (f x / f x) ≤ f x_1
⊢ f x_1 * (f x / 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_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x_1 : R
hx_1 : ∀ (y : R), f (x_1 * y) = f x_1 * f y
x : R
hx : f x = 0
pos : 0 ≤ f x_1
⊢ f x_1 * (f x / f x) ≤ f x_1

Tactic:
rw [hx, div_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, 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
x_1 : R
hx_1 : ∀ (y : R), f (x_1 * y) = f x_1 * f y
x : R
hx : f x = 0
⊢ 0 ≤ f x_1

Tactic:
f_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_1 : R
hx_1 : ∀ (y : R), f (x_1 * y) = f x_1 * f y
x : R
hx : f x = 0
⊢ 0 ≤ f x_1

Tactic:
exact f_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_1 : R
hx_1 : ∀ (y : R), f (x_1 * y) = f x_1 * f y
x : R
hx : ¬f x = 0
neg : f x_1 * 1 ≤ f x_1
neg₁ neg₂ : f x_1 ≤ f x_1
⊢ f x_1 * (f x / f x) ≤ f x_1

Tactic:
rw [div_self hx, mul_one]

Premises used: mul_one, div_self
-- 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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
pos : ∀ (f_ne_zero : f ≠ 0), f x ≤ ⨆ (y : R), f x * (f y / f y)
neg : ∀ (f_ne_zero : f = 0), f x ≤ ⨆ (y : R), f x * (f y / f y)
⊢ f x ≤ ⨆ (y : R), f x * (f y / f y)

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
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
rw : f x * 1
| f x

Tactic:
rw [← mul_one (f x)]

Premises used: mul_one
-- 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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
pos : f x * 1 ≤ ⨆ (y : R), f x * (f y / f y)
⊢ f x ≤ ⨆ (y : R), f x * (f y / f y)

Tactic:
conv_lhs => rw [← mul_one (f x)]

Premises used: mul_one
-- 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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
pos : f x * (f 1 / f 1) ≤ ⨆ (y : R), f x * (f y / f y)
⊢ f x * 1 ≤ ⨆ (y : R), f x * (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_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (y : R) ↦ f x * (f y / f y))) (f x)
⊢ BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f x * (f y / f y))

Tactic:
use f x
-- 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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
y : R
pos : ∀ (hy0 : f y = 0), (fun (y : R) ↦ f x * (f y / f y)) y ≤ f x
neg : ∀ (hy0 : ¬f y = 0), (fun (y : R) ↦ f x * (f y / f y)) y ≤ f x
⊢ (fun (y : R) ↦ f x * (f y / f y)) y ≤ f x

Tactic:
by_cases hy0 : f y = 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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
y : R
hy0 : f y = 0
pos : 0 ≤ f x
⊢ (fun (y : R) ↦ f x * (f y / f y)) y ≤ f x

Tactic:
simp only [hy0, div_zero, mul_zero]

Premises used: MulZeroClass.mul_zero, 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
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
y : R
hy0 : f y = 0
⊢ 0 ≤ f x

Tactic:
f_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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
y : R
hy0 : f y = 0
⊢ 0 ≤ f x

Tactic:
exact f_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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
y : R
hy0 : ¬f y = 0
⊢ (fun (y : R) ↦ f x * (f y / f y)) y ≤ f x

Tactic:
simp only [div_self hy0, mul_one, le_refl]

Premises used: le_refl, mul_one, div_self
-- 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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
⊢ BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f x * (f y / f y))

Tactic:
have h_bdd : BddAbove (Set.range fun y ↦ f x * (f y / f y)) := by
        use f x
        rintro r ⟨y, rfl⟩
        by_cases hy0 : f y = 0
        · simp only [hy0, div_zero, mul_zero]; exact f_nonneg _
        · simp only [div_self hy0, mul_one, 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
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
h_bdd : BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f x * (f y / f y))
⊢ f x * (f 1 / f 1) ≤ ⨆ (y : R), f x * (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_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
h_bdd : BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f x * (f y / f y))
⊢ f x * (f 1 / f 1) ≤ ⨆ (y : R), f x * (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
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f = 0
neg : LE.le (α := ℝ) 0 0
⊢ f x ≤ ⨆ (y : R), f x * (f y / f y)

Tactic:
simp_rw [f_ne_zero, Pi.zero_apply, zero_div, zero_mul, ciSup_const]

Premises used: MulZeroClass.zero_mul, zero_div, Pi.zero_apply, ciSup_const
-- 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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f = 0
⊢ LE.le (α := ℝ) 0 0

Tactic:
rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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
a : ⨆ (y : R), f (x * y) / f y ≤ f x
a₁ : f x ≤ ⨆ (y : R), f (x * y) / f y
⊢ ⨆ (y : R), f (x * y) / f y = f x

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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:
ciSup_le (fun y ↦ ?_)

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

Tactic:
refine ciSup_le (fun y ↦ ?_)

Premises used: ciSup_le
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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
pos : ∀ (hy : f y = 0), f (x * y) / f y ≤ f x
neg : ∀ (hy : ¬f y = 0), f (x * y) / f y ≤ f x
⊢ f (x * y) / f y ≤ f x

Tactic:
by_cases hy : f y = 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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
pos : 0 ≤ f x
⊢ f (x * y) / f y ≤ f x

Tactic:
rw [hy, div_zero]

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

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

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 → ℝ
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

Tactic:
hx _
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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

Tactic:
exact hx _
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (y : R) ↦ f (x * y) / f y)) (f x)
⊢ BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f (x * y) / f y)

Tactic:
use f x
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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
pos : ∀ (hy0 : f y = 0), (fun (y : R) ↦ f (x * y) / f y) y ≤ f x
neg : ∀ (hy0 : ¬f y = 0), (fun (y : R) ↦ f (x * y) / f y) y ≤ f x
⊢ (fun (y : R) ↦ f (x * y) / f y) y ≤ f x

Tactic:
by_cases hy0 : f y = 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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
pos : 0 ≤ f x
⊢ (fun (y : R) ↦ f (x * y) / f y) y ≤ f x

Tactic:
simp only [hy0, div_zero]

Premises used: div_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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:
f_nonneg _
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 _
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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
neg : f (x * y) ≤ f x * f y
⊢ (fun (y : R) ↦ 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]

Premises used: div_le_iff₀, mul_div_assoc, lt_of_le_of_ne', mul_one, div_self
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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:
hx y
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 : R) ↦ f (x * y) / f y)

Tactic:
have h_bdd : BddAbove (Set.range fun y ↦ f (x * y) / f y) := by
      use f x
      rintro r ⟨y, rfl⟩
      by_cases hy0 : f y = 0
      · simp only [hy0, div_zero]
        exact f_nonneg _
      · 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]
        exact hx y
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 : R) ↦ f (x * y) / f y)
⊢ f (x * 1) / f 1 ≤ ⨆ (y : R), f (x * 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 → ℝ
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 : R) ↦ f (x * y) / f y)
h : f x = f (x * 1) / f 1
⊢ f x ≤ ⨆ (y : R), f (x * y) / f y

Tactic:
convert! 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 → ℝ
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 : R) ↦ f (x * y) / f y)
pos : ∀ (h0 : f x = 0), f x = f (x * 1) / f 1
neg : ∀ (h0 : ¬f x = 0), f x = f (x * 1) / f 1
⊢ f x = f (x * 1) / f 1

Tactic:
by_cases h0 : f x = 0
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 : R) ↦ f (x * y) / f y)
h0 : f x = 0
pos : f x = f x / f 1
pos₁ : 0 = 0 / f 1
pos₂ pos₃ : Eq (α := ℝ) 0 0
⊢ f x = f (x * 1) / f 1

Tactic:
rw [mul_one, h0, zero_div]

Premises used: zero_div, mul_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
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 : R) ↦ f (x * y) / f y)
h0 : ¬f x = 0
apply : 1 ≤ f 1
⊢ f 1 = 1

Tactic:
apply h_one.antisymm

Premises used: LE.le.antisymm