awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f (x * y * z) / f z / seminormFromBounded' f y ≤ seminormFromBounded' f x
have neg : f (x * y * z) / f z / seminormFromBounded' f y ≤ f (x * z) / f z
Tactic: apply le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) z
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f (x * y * z) / f z / seminormFromBounded' f y ≤ f (x * z) / f z
have neg : f (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z
Tactic: rw [div_le_iff₀ (lt_of_le_of_ne' (seminormFromBounded_nonneg f_nonneg f_mul _) hy),
      div_mul_eq_mul_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z
have pos : ∀ (hz : f z = 0), f (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z
Tactic: by_cases hz : f z = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z
have neg : ∀ (hz : ¬f z = 0), f (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z
Tactic: by_cases hz : f z = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (hypothesis)
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 (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z
have hxyz : f (z * (x * y)) = 0
Tactic: have hxyz : f (z * (x * y)) = 0 := map_mul_zero_of_map_zero f_nonneg f_mul hz _
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z
have pos : 0 ≤ seminormFromBounded' f y * f (x * z) / f z
Tactic: simp_rw [mul_comm, hxyz, zero_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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 (x * y * z) / f z ≤ f (x * z) * seminormFromBounded' f y / f z
have neg : f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)
Tactic: rw [div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz), mul_comm (f (x * z))]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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 (x * y * z) ≤ seminormFromBounded' f y * f (x * z)
have pos : ∀ (hxz : f (x * z) = 0), f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)
Tactic: by_cases hxz : f (x * z) = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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)
⊢ f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)
have neg : ∀ (hxz : ¬f (x * z) = 0), f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)
Tactic: by_cases hxz : f (x * z) = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)
have pos : 0 ≤ 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f (x * y * z) ≤ seminormFromBounded' f y * f (x * z)
have neg : f (x * y * z) / f (x * z) ≤ seminormFromBounded' f y
Tactic: rw [← div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) hxz)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f (x * y * z) / f (x * z) ≤ seminormFromBounded' f y
have neg : f (x * y * z) / f (x * z) ≤ f (y * (x * z)) / f (x * z)
Tactic: apply le_ciSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul y) (x * z)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f (x * y * z) / f (x * z) ≤ f (y * (x * z)) / f (x * z)
have neg : f (x * y * z) ≤ f (y * (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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))
⊢ f (x * y * z) / f (x * z) ≤ f (y * (x * z)) / f (x * z)
have neg₁ : f (y * x * z) ≤ f (y * (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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))
⊢ f (x * y * z) / f (x * z) ≤ f (y * (x * z)) / f (x * z)
have neg₂ : f (y * (x * z)) ≤ f (y * (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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ seminormFromBounded' f 1 = 1
have simp_rw : Eq (α := ℝ) (⨆ (y : R), f y / f y) 1
Tactic: simp_rw [seminormFromBounded', one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ Eq (α := ℝ) (⨆ (y : R), f y / f y) 1
have a : LE.le (α := ℝ) (⨆ (y : R), f y / f y) 1
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ Eq (α := ℝ) (⨆ (y : R), f y / f y) 1
have a₁ : LE.le (α := ℝ) 1 (⨆ (y : R), f y / f y)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
have a : ∀ (x : R), f x / f x ≤ 1
Tactic: refine ciSup_le (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f x / f x ≤ 1
have pos : ∀ (hx : f x = 0), f x / f x ≤ 1
Tactic: by_cases hx : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f x / f x ≤ 1
have neg : ∀ (hx : ¬f x = 0), f x / f x ≤ 1
Tactic: by_cases hx : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f x / f x ≤ 1
have pos : LE.le (α := ℝ) 0 1
Tactic: rw [hx, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f x / f x ≤ 1
have neg : LE.le (α := ℝ) 1 1
Tactic: rw [div_self hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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 (α := ℝ) 1 (⨆ (y : R), f y / f y)
have a : f 1 / f 1 ≤ ⨆ (y : R), f y / f y
Tactic: rw [← div_self (map_one_ne_zero f_ne_zero f_nonneg f_mul)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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)
have h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (y : R) ↦ f y / f y)) 1
Tactic: use (1 : ℝ)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ LE.le (α := ℝ) ((fun (y : R) ↦ f y / f y) y) 1
have pos : ∀ (hy : f y = 0), LE.le (α := ℝ) ((fun (y : R) ↦ f y / f y) y) 1
Tactic: by_cases hy : f y = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ LE.le (α := ℝ) ((fun (y : R) ↦ f y / f y) y) 1
have neg : ∀ (hy : ¬f y = 0), LE.le (α := ℝ) ((fun (y : R) ↦ f y / f y) y) 1
Tactic: by_cases hy : f y = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (hypothesis)
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
⊢ f 1 / f 1 ≤ ⨆ (y : R), f y / f y
have h_bdd : 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ seminormFromBounded' f 1 ≤ 1
have pos : ∀ (f_ne_zero : f ≠ 0), seminormFromBounded' f 1 ≤ 1
Tactic: by_cases! f_ne_zero : f ≠ 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ seminormFromBounded' f 1 ≤ 1
have neg : ∀ (f_ne_zero : f = 0), seminormFromBounded' f 1 ≤ 1
Tactic: by_cases! f_ne_zero : f ≠ 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
have neg : LE.le (α := ℝ) (⨆ (y : R), f y / f y) 1
Tactic: simp_rw [seminormFromBounded', one_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
have neg : ∀ (x : R), f x / f x ≤ 1
Tactic: refine ciSup_le (fun _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
have refine : ∀ (z : R), f ((x + y) * z) / f z ≤ seminormFromBounded' f x + seminormFromBounded' f y
Tactic: refine ciSup_le (fun z ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x + seminormFromBounded' f y
have suffices : f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z
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 _)))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z
have pos : ∀ (hz : f z = 0), f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z
Tactic: by_cases hz : f z = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z
have neg : ∀ (hz : ¬f z = 0), f ((x + y) * z) / f z ≤ f (x * z) / f z + f (y * z) / f z
Tactic: by_cases hz : f z = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
have neg : f (x * z + y * z) ≤ f (x * z) + f (y * z)
Tactic: rw [← add_div, div_le_div_iff_of_pos_right (lt_of_le_of_ne' (f_nonneg _) hz), add_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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)
have refine : ∀ (x y z : R), f ((x + y) * z) / f z ≤ max (seminormFromBounded' f x) (seminormFromBounded' f y)
Tactic: refine fun x y ↦ ciSup_le (fun z ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f ((x + y) * z) / f z ≤ max (seminormFromBounded' f x) (seminormFromBounded' f y)
have rw : f ((x + y) * z) / f z ≤ seminormFromBounded' f x ∨ f ((x + y) * z) / f z ≤ seminormFromBounded' f y
Tactic: rw [le_max_iff]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x ∨ f ((x + y) * z) / f z ≤ seminormFromBounded' f y
have 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
Tactic: rcases hf with hfx | hfy
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x ∨ f ((x + y) * z) / f z ≤ seminormFromBounded' f y
have 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
Tactic: rcases hf with hfx | hfy
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f ((x + y) * z) / f z ≤ seminormFromBounded' f x ∨ f ((x + y) * z) / f z ≤ seminormFromBounded' f y
have suffices : f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * z) / f z ≤ f (y * z) / f z
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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * z) / f z ≤ f (y * z) / f z
have 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
Tactic: by_cases hz : f z = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f ((x + y) * z) / f z ≤ f (x * z) / f z ∨ f ((x + y) * z) / f z ≤ f (y * z) / f z
have 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
Tactic: by_cases hz : f z = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
have neg : f (x * z + y * z) ≤ max (f (x * z)) (f (y * 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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ seminormFromBounded' f x = f x
have simp_rw : ⨆ (y : R), f x * (f y / f y) = f x
Tactic: simp_rw [seminormFromBounded', hx, ← mul_div_assoc']
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
have a : ⨆ (y : R), f x * (f y / f y) ≤ f x
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ ⨆ (y : R), f x * (f y / f y) = f x
have a₁ : f x ≤ ⨆ (y : R), f x * (f y / f y)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
have a : ∀ (x_1 : R), f x * (f x_1 / f x_1) ≤ f x
Tactic: refine ciSup_le (fun x ↦ ?_)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f x_1 * (f x / f x) ≤ f x_1
have pos : ∀ (hx : f x = 0), f x_1 * (f x / f x) ≤ f x_1
Tactic: by_cases hx : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f x_1 * (f x / f x) ≤ f x_1
have neg : ∀ (hx : ¬f x = 0), f x_1 * (f x / f x) ≤ f x_1
Tactic: by_cases hx : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f x_1 * (f x / f x) ≤ f x_1
have pos : 0 ≤ f x_1
Tactic: rw [hx, div_zero, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f x_1 * (f x / f x) ≤ f x_1
have neg : f x_1 * 1 ≤ f x_1
Tactic: rw [div_self hx, mul_one]