awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_2
inst : SeminormedRing R
x : R
⊢ (toRingSeminorm R : (a : R) → ℝ) x = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R_1 : Type u_1
R : Type u_2
inst : NormedRing R
x : R
hx : ‖x‖ = 0
rw : ‖x‖ = 0
⊢ x = 0

Tactic:
rw [← norm_eq_zero]

Premises used: norm_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R_1 : Type u_1
R : Type u_2
inst : NormedRing R
x : R
hx : ‖x‖ = 0
⊢ ‖x‖ = 0

Tactic:
hx
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R_1 : Type u_1
R : Type u_2
inst : NormedRing R
x : R
hx : ‖x‖ = 0
⊢ ‖x‖ = 0

Tactic:
exact hx
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R : Type u_2
inst : NormedRing R
x : R
⊢ (toRingNorm R : (a : R) → ℝ) x = ‖x‖

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R_1 : Type u_1
R : Type u_2
inst : NormedField R
x : R
hx : ‖x‖ = 0
rw : ‖x‖ = 0
⊢ x = 0

Tactic:
rw [← norm_eq_zero]

Premises used: norm_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R_1 : Type u_1
R : Type u_2
inst : NormedField R
x : R
hx : ‖x‖ = 0
⊢ ‖x‖ = 0

Tactic:
hx
-- Module: Mathlib.Analysis.Normed.Unbundled.RingSeminorm
Goal:
R_1 : Type u_1
R : Type u_2
inst : NormedField R
x : R
hx : ‖x‖ = 0
⊢ ‖x‖ = 0

Tactic:
exact hx
-- 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
h1 : f 1 = 0
⊢ ∀ (y : R), f (1 * y) ≤ c * f 1 * f y

Tactic:
specialize f_mul 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
h1 : f 1 = 0
f_mul : ∀ (y : R), f (1 * y) ≤ c * f 1 * f y
⊢ ∀ (y : R), f y ≤ 0

Tactic:
simp_rw [h1, one_mul, mul_zero, zero_mul] at f_mul

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, 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
h1 : f 1 = 0
f_mul : ∀ (y : R), f y ≤ 0
obtain : ∀ (z : R) (hz : f z ≠ 0 z), False
⊢ False

Tactic:
obtain ⟨z, hz⟩ := Function.ne_iff.mp f_ne_zero

Premises used: Function.ne_iff, Iff.mp
-- 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
h1 : f 1 = 0
f_mul : ∀ (y : R), f y ≤ 0
z : R
hz : f z ≠ 0 z
⊢ False

Tactic:
hz <| (f_mul z).antisymm (f_nonneg z)

Premises used: LE.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
h1 : f 1 = 0
f_mul : ∀ (y : R), f y ≤ 0
z : R
hz : f z ≠ 0 z
⊢ False

Tactic:
exact hz <| (f_mul z).antisymm (f_nonneg z)

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

Tactic:
have h1 : f 1 ≠ 0 := map_one_ne_zero (Function.ne_iff.mpr ⟨x, hfx⟩) f_nonneg f_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 ≠ 0
hxn : f (x ^ n) = 0
⊢ f 1 ≤ 0

Tactic:
simpa [← mul_pow, hxn] using f_mul (x ^ n) (hx.unit⁻¹ ^ n)

Premises used: Units.val, Inv.inv, HPow.hPow, IsUnit.unit, mul_pow
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 ≠ 0
hxn : f (x ^ n) = 0
⊢ f 1 ≤ 0

Tactic:
have : f 1 ≤ 0 := by simpa [← mul_pow, hxn] using f_mul (x ^ n) (hx.unit⁻¹ ^ n)
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 ≠ 0
hxn : f (x ^ n) = 0
this : f 1 ≤ 0
⊢ False

Tactic:
h1 <| this.antisymm (f_nonneg 1)

Premises used: LE.le.antisymm, OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
h1 : f 1 ≠ 0
hxn : f (x ^ n) = 0
this : f 1 ≤ 0
⊢ False

Tactic:
exact h1 <| this.antisymm (f_nonneg 1)

Premises used: LE.le.antisymm, 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 : f x = 0
y : R
⊢ f (x * y) ≤ 0

Tactic:
simpa [hx] using f_mul x y
-- 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 : f x = 0
y : R
⊢ f (x * y) ≤ 0

Tactic:
replace f_mul : f (x * y) ≤ 0 := by simpa [hx] using f_mul x y
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : f x = 0
y : R
f_mul : f (x * y) ≤ 0
⊢ f (x * y) = 0

Tactic:
le_antisymm f_mul (f_nonneg _)

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
x : R
hx : f x = 0
y : R
f_mul : f (x * y) ≤ 0
⊢ f (x * y) = 0

Tactic:
exact le_antisymm f_mul (f_nonneg _)

Premises used: le_antisymm
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_zero : f 0 = 0
simp_rw : Eq (α := ℝ) (⨆ (y : R), f (0 * y) / f y) 0
simp_rw₁ : Eq (α := ℝ) (⨆ (y : R), f 0 / f y) 0
simp_rw₂ : Eq (α := ℝ) (⨆ (y : R), 0 / f y) 0
simp_rw₃ : Eq (α := ℝ) (⨆ (y : R), 0) 0
⊢ seminormFromBounded' f 0 = 0

Tactic:
simp_rw [seminormFromBounded', zero_mul, f_zero, zero_div, ciSup_const]

Premises used: MulZeroClass.zero_mul, zero_div, seminormFromBounded', 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
inl : ∀ (hx : f x = 0 x), 0 ≤ c * f x
inr : ∀ (hx : 0 x < f x), 0 ≤ c * f x
⊢ 0 ≤ c * f x

Tactic:
rcases (f_nonneg x).eq_or_lt' with hx | hx

Premises used: LE.le.eq_or_lt'
-- 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 : f x = 0 x
⊢ 0 ≤ c * f x

Tactic:
simp [hx]
-- 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 : 0 x < f x
⊢ 0 < f x

Tactic:
change 0 < f x at hx
-- 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 : 0 < f x
⊢ f (x * 1) ≤ c * f x * f 1

Tactic:
specialize f_mul x 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : 0 < f x
f_mul : f x ≤ c * f x * f 1
⊢ c * f x * f 1 = c * f 1 * f x

Tactic:
ring
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : 0 < f x
f_mul : f (x * 1) ≤ c * f x * f 1
⊢ 1 ≤ c * f 1

Tactic:
rw [mul_one, show c * f x * f 1 = c * f 1 * f x by ring, le_mul_iff_one_le_left hx] at f_mul

Premises used: le_mul_iff_one_le_left, mul_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
⊢ 0 ≤ f 1

Tactic:
replace f_nonneg : 0 ≤ f 1 := f_nonneg 1
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
f_nonneg : 0 ≤ f 1
inl : ∀ (h1 : f 1 = 0), 0 ≤ c
inr : ∀ (h1 : 0 < f 1), 0 ≤ c
⊢ 0 ≤ c

Tactic:
rcases f_nonneg.eq_or_lt' with h1 | h1

Premises used: LE.le.eq_or_lt'
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
f_nonneg : 0 ≤ f 1
h1 : f 1 = 0
⊢ LE.le (α := ℝ) 1 0

Tactic:
simpa [h1] using f_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
f_nonneg : 0 ≤ f 1
h1 : f 1 = 0
linarith : c < 0 → -1 + HSub.hSub (α := ℝ) 1 0 = 0
⊢ 0 ≤ c

Tactic:
linarith [show (1 : ℝ) ≤ 0 by simpa [h1] using f_mul]
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
⊢ 1 / f 1 ≤ c

Tactic:
rw [← div_le_iff₀ h1] at f_mul

Premises used: div_le_iff₀
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
f_mul₁ : 1 / f 1 ≤ c
⊢ 0 ≤ f 1

Tactic:
rw [← div_le_iff₀ h1] at f_mul

Premises used: div_le_iff₀
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
f_mul₁ : 1 / f 1 ≤ c
f_nonneg₁ : 0 ≤ f 1
⊢ 0 < f 1

Tactic:
rw [← div_le_iff₀ h1] at f_mul

Premises used: div_le_iff₀
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
x : R
hx : 0 < f x
f_mul : 1 / f 1 ≤ c
f_nonneg : 0 ≤ f 1
h1 : 0 < f 1
linarith : c < 0 → 1 * (1 / f 1) - 1 * c + (c - 0) + (HMul.hMul (α := ℝ) 1 0 - 1 * (1 / f 1)) = 0
⊢ 0 ≤ c

Tactic:
linarith [one_div_pos.mpr h1]

Premises used: Iff.mpr, one_div_pos
-- 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 : 0 < f x
⊢ 0 ≤ c

Tactic:
have hc : 0 ≤ c := by
      specialize f_mul x 1
      rw [mul_one, show c * f x * f 1 = c * f 1 * f x by ring, le_mul_iff_one_le_left hx] at f_mul
      replace f_nonneg : 0 ≤ f 1 := f_nonneg 1
      rcases f_nonneg.eq_or_lt' with h1 | h1
      · linarith [show (1 : ℝ) ≤ 0 by simpa [h1] using f_mul]
      · rw [← div_le_iff₀ h1] at f_mul
        linarith [one_div_pos.mpr h1]
-- 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 : 0 < f x
hc : 0 ≤ c
⊢ 0 ≤ c * f x

Tactic:
positivity
-- 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
h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (y : R) ↦ f (x * y) / f y)) (c * f x)
⊢ BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f (x * y) / f y)

Tactic:
use c * 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 y : R
h : ∀ (hy0 : f y = 0 y), (fun (y : R) ↦ f (x * y) / f y) y ≤ c * f x
h₁ : ∀ (hy0 : 0 y < f y), (fun (y : R) ↦ f (x * y) / f y) y ≤ c * f x
⊢ (fun (y : R) ↦ f (x * y) / f y) y ≤ c * f x

Tactic:
rcases (f_nonneg y).eq_or_lt' with hy0 | hy0

Premises used: LE.le.eq_or_lt'
-- 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
hy0 : f y = 0 y
⊢ (fun (y : R) ↦ f (x * y) / f y) y ≤ c * f x

Tactic:
simpa [hy0] using seminormFromBounded_aux f_nonneg f_mul x

Premises used: seminormFromBounded_aux
-- 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
hy0 : 0 y < f y
⊢ (fun (y : R) ↦ f (x * y) / f y) y ≤ c * f x

Tactic:
simpa [div_le_iff₀ hy0] using f_mul x y

Premises used: div_le_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 : R
⊢ seminormFromBounded' f x ≤ c * f x

Tactic:
ciSup_le (fun y ↦ ?_)

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
x : R
refine : ∀ (y : R), f (x * y) / f y ≤ c * f x
⊢ seminormFromBounded' f x ≤ c * 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 → ℝ
c : ℝ
f_nonneg : 0 ≤ f
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
x y : R
inl : ∀ (hy : f y = 0 y), f (x * y) / f y ≤ c * f x
inr : ∀ (hy : 0 y < f y), f (x * y) / f y ≤ c * f x
⊢ f (x * y) / f y ≤ c * f x

Tactic:
rcases (f_nonneg y).eq_or_lt' with hy | hy

Premises used: LE.le.eq_or_lt'
-- 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 y
⊢ f (x * y) / f y ≤ c * f x

Tactic:
simpa [hy] using seminormFromBounded_aux f_nonneg f_mul x

Premises used: seminormFromBounded_aux
-- 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 : 0 y < f y
inr : f (x * y) ≤ c * f x * f y
⊢ f (x * y) / f y ≤ c * f x

Tactic:
rw [div_le_iff₀ hy]

Premises used: div_le_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 : 0 y < f y
⊢ f (x * y) ≤ c * f x * f y

Tactic:
apply f_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
x : R
pos : ∀ (h1 : f 1 = 0), f x ≤ f 1 * seminormFromBounded' f x
neg : ∀ (h1 : ¬f 1 = 0), f x ≤ f 1 * seminormFromBounded' f x
⊢ f x ≤ f 1 * seminormFromBounded' f x

Tactic:
by_cases h1 : f 1 = 0

Premises used: 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
h1 : f 1 = 0
⊢ f (x * 1) ≤ c * f x * f 1

Tactic:
specialize f_mul x 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
h1 : f 1 = 0
f_mul : f (x * 1) ≤ c * f x * f 1
⊢ f x ≤ 0

Tactic:
rw [mul_one, h1, mul_zero] at f_mul

Premises used: MulZeroClass.mul_zero, mul_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
h1 : f 1 = 0
f_mul : f x ≤ 0
⊢ f x = 0

Tactic:
have hx0 : f x = 0 := f_mul.antisymm (f_nonneg _)
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_nonneg : 0 ≤ f
x : R
h1 : f 1 = 0
f_mul : f x ≤ 0
hx0 : f x = 0
pos : 0 ≤ f 1 * seminormFromBounded' f x
pos₁ : 0 ≤ 0 * seminormFromBounded' f x
pos₂ pos₃ : LE.le (α := ℝ) 0 0
⊢ f x ≤ f 1 * seminormFromBounded' f x

Tactic:
rw [hx0, h1, zero_mul]

Premises used: MulZeroClass.zero_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
x : R
h1 : ¬f 1 = 0
neg : f x / f 1 ≤ seminormFromBounded' f x
⊢ f x ≤ f 1 * seminormFromBounded' f x

Tactic:
rw [mul_comm, ← div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) h1)]

Premises used: div_le_iff₀, 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 : R
h1 : ¬f 1 = 0
rw : f (x * 1) / f 1
| f x / f 1

Tactic:
rw [← mul_one 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
h1 : ¬f 1 = 0
neg : f (x * 1) / f 1 ≤ seminormFromBounded' f x
⊢ f x / f 1 ≤ seminormFromBounded' f x

Tactic:
conv_lhs => rw [← mul_one 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
h1 : ¬f 1 = 0
⊢ f (x * 1) / f 1 ≤ seminormFromBounded' f x

Tactic:
le_ciSup (seminormFromBounded_bddAbove_range f_nonneg f_mul x) (1 : R)

Premises used: le_ciSup, seminormFromBounded', OfNat.ofNat, 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 : R
h1 : ¬f 1 = 0
⊢ f (x * 1) / f 1 ≤ seminormFromBounded' f x

Tactic:
exact le_ciSup (seminormFromBounded_bddAbove_range f_nonneg f_mul x) (1 : R)

Premises used: le_ciSup, OfNat.ofNat, 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
⊢ 0 ≤ seminormFromBounded' f

Tactic:
fun x ↦
  le_csSup_of_le (seminormFromBounded_bddAbove_range f_nonneg f_mul x) ⟨1, rfl⟩
    (div_nonneg (f_nonneg _) (f_nonneg _))

Premises used: HMul.hMul, iSup, le_csSup_of_le, seminormFromBounded', Exists.intro, div_nonneg, OfNat.ofNat, seminormFromBounded_bddAbove_range, rfl
-- 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
⊢ seminormFromBounded' f x = 0 ↔ f x = 0

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- 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
refine_1 : ∀ (h : seminormFromBounded' f x = 0), f x = 0
refine_2 : ∀ (h : f x = 0), seminormFromBounded' f x = 0
⊢ seminormFromBounded' f x = 0 ↔ f x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
h : seminormFromBounded' f x = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x

Tactic:
have hf := seminormFromBounded_ge f_nonneg f_mul 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
h : seminormFromBounded' f x = 0
hf : f x ≤ f 1 * seminormFromBounded' f x
⊢ f x ≤ 0

Tactic:
rw [h, mul_zero] at hf

Premises used: MulZeroClass.mul_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
h : seminormFromBounded' f x = 0
hf : f x ≤ 0
⊢ f x = 0

Tactic:
hf.antisymm (f_nonneg _)

Premises used: LE.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
h : seminormFromBounded' f x = 0
hf : f x ≤ 0
⊢ f x = 0

Tactic:
exact hf.antisymm (f_nonneg _)

Premises used: LE.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
h : f x = 0
⊢ seminormFromBounded' f x ≤ c * f x

Tactic:
have hf : seminormFromBounded' f x ≤ c * f x :=
      seminormFromBounded_le f_nonneg f_mul 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
h : f x = 0
hf : seminormFromBounded' f x ≤ c * f x
⊢ seminormFromBounded' f x ≤ 0

Tactic:
rw [h, mul_zero] at hf

Premises used: MulZeroClass.mul_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
h : f x = 0
hf : seminormFromBounded' f x ≤ 0
⊢ seminormFromBounded' f x = 0

Tactic:
hf.antisymm (seminormFromBounded_nonneg f_nonneg f_mul x)

Premises used: LE.le.antisymm, 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 : R
h : f x = 0
hf : seminormFromBounded' f x ≤ 0
⊢ seminormFromBounded' f x = 0

Tactic:
exact hf.antisymm (seminormFromBounded_nonneg f_nonneg f_mul x)

Premises used: LE.le.antisymm, seminormFromBounded_nonneg
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
this : Eq (α := ℝ) (⨆ (y : R), f (-x * y) / f y) (⨆ (y : R), f (x * y) / f y)
⊢ seminormFromBounded' f (-x) = seminormFromBounded' f x

Tactic:
simpa only [seminormFromBounded']

Premises used: seminormFromBounded'
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
e_s : Eq.{u_1 + 1} (α := R → ℝ) (fun (y : R) ↦ f (-x * y) / f y) fun (y : R) ↦ f (x * y) / f y
⊢ Eq (α := ℝ) (⨆ (y : R), f (-x * y) / f y) (⨆ (y : R), f (x * y) / f y)

Tactic:
congr
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
e_s : ∀ (y : R), f (-x * y) / f y = f (x * y) / f y
⊢ Eq.{u_1 + 1} (α := R → ℝ) (fun (y : R) ↦ f (-x * y) / f y) fun (y : R) ↦ f (x * y) / f y

Tactic:
ext y
-- Module: Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x y : R
e_s : f (-(x * y)) / f y = f (x * y) / f y
e_s₁ e_s₂ : f (x * y) / f y = f (x * y) / f y
⊢ f (-x * y) / f y = f (x * y) / f y

Tactic:
rw [neg_mul, f_neg]

Premises used: neg_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
x y : R
H : ∀ (x_1 : R), f (x * y * x_1) / f x_1 ≤ seminormFromBounded' f x * seminormFromBounded' f y
⊢ seminormFromBounded' f (x * y) ≤ seminormFromBounded' f x * seminormFromBounded' f y

Tactic:
apply ciSup_le

Premises used: ciSup_le