awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
hn0 : ¬x = 0
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : K) → ℝ) x : ℝ) ((f : (a : K) → ℝ) (c * x⁻¹) : ℝ) ≤ 0
have rw : HMul.hMul (α := ℝ) (β := ℝ) ((f.toAddGroupSeminorm : (a : K) → ℝ) x : ℝ)
    ((f.toAddGroupSeminorm : (a : K) → ℝ) (c * x⁻¹) : ℝ) ≤
  0
Tactic: rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx,
                zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
hn0 : ¬x = 0
rw :
  HMul.hMul (α := ℝ) (β := ℝ) ((f.toAddGroupSeminorm : (a : K) → ℝ) x : ℝ)
      ((f.toAddGroupSeminorm : (a : K) → ℝ) (c * x⁻¹) : ℝ) ≤
    0
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : K) → ℝ) x : ℝ) ((f : (a : K) → ℝ) (c * x⁻¹) : ℝ) ≤ 0
have rw₁ : f.toFun x * f.toFun (c * x⁻¹) ≤ 0
Tactic: rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx,
                zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
hn0 : ¬x = 0
rw :
  HMul.hMul (α := ℝ) (β := ℝ) ((f.toAddGroupSeminorm : (a : K) → ℝ) x : ℝ)
      ((f.toAddGroupSeminorm : (a : K) → ℝ) (c * x⁻¹) : ℝ) ≤
    0
rw₁ : f.toFun x * f.toFun (c * x⁻¹) ≤ 0
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : K) → ℝ) x : ℝ) ((f : (a : K) → ℝ) (c * x⁻¹) : ℝ) ≤ 0
have rw₂ : 0 * f.toFun (c * x⁻¹) ≤ 0
Tactic: rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx,
                zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (goal)
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
hn0 : ¬x = 0
rw :
  HMul.hMul (α := ℝ) (β := ℝ) ((f.toAddGroupSeminorm : (a : K) → ℝ) x : ℝ)
      ((f.toAddGroupSeminorm : (a : K) → ℝ) (c * x⁻¹) : ℝ) ≤
    0
rw₁ : f.toFun x * f.toFun (c * x⁻¹) ≤ 0
rw₂ : 0 * f.toFun (c * x⁻¹) ≤ 0
⊢ HMul.hMul (α := ℝ) (β := ℝ) ((f : (a : K) → ℝ) x : ℝ) ((f : (a : K) → ℝ) (c * x⁻¹) : ℝ) ≤ 0
have rw₃ : LE.le (α := ℝ) 0 0
Tactic: rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx,
                zero_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.RingSeminorm (hypothesis)
Goal:
R : Type u_1
K : Type u_2
inst : Field K
f : RingSeminorm K
hnt : f ≠ 0
x : K
hx : f.toFun x = 0
c : K
hc : Ne (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
hn0 : ¬x = 0
⊢ False
have hc0 : Eq (α := ℝ) ((f : (a : K) → ℝ) c : ℝ) (0 : ℝ)
Tactic: have hc0 : f c = 0 := by
        rw [← mul_one c, ← mul_inv_cancel₀ hn0, ← mul_assoc, mul_comm c, mul_assoc]
        exact
          le_antisymm
            (le_trans (map_mul_le_mul f _ _)
              (by rw [← RingSeminorm.toFun_eq_coe, ← AddGroupSeminorm.toFun_eq_coe, hx,
                zero_mul]))
            (apply_nonneg f _)
-- 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
h1 : f 1 = 0
⊢ False
have f_mul₁ : ∀ (y : R), f (1 * y) ≤ c * f 1 * f y
Tactic: specialize f_mul 1
Cleared hypotheses: f_mul
-- 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
h1 : f 1 = 0
f_mul : ∀ (y : R), f (1 * y) ≤ c * f 1 * f y
⊢ False
have f_mul₁ : ∀ (y : R), f y ≤ 0
Tactic: simp_rw [h1, one_mul, mul_zero, zero_mul] at f_mul
Cleared hypotheses: 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
h1 : f 1 = 0
f_mul : ∀ (y : R), f y ≤ 0
⊢ False
have obtain : ∀ (z : R) (hz : f z ≠ 0 z), False
Tactic: obtain ⟨z, hz⟩ := Function.ne_iff.mp f_ne_zero
-- 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
x : R
hx : IsUnit x
hfx : f x ≠ 0
n : ℕ
f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y
⊢ f (x ^ n) ≠ 0
have h1 : f 1 ≠ 0
Tactic: have h1 : f 1 ≠ 0 := map_one_ne_zero (Function.ne_iff.mpr ⟨x, hfx⟩) f_nonneg f_mul
-- 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
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
⊢ False
have this : f 1 ≤ 0
Tactic: have : f 1 ≤ 0 := by simpa [← mul_pow, hxn] using f_mul (x ^ n) (hx.unit⁻¹ ^ n)
-- 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 : R
hx : f x = 0
y : R
⊢ f (x * y) = 0
have f_mul₁ : f (x * y) ≤ 0
Tactic: replace f_mul : f (x * y) ≤ 0 := by simpa [hx] using f_mul x y
Cleared hypotheses: f_mul
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_zero : f 0 = 0
⊢ seminormFromBounded' f 0 = 0
have simp_rw : Eq (α := ℝ) (⨆ (y : R), f (0 * y) / f y) 0
Tactic: simp_rw [seminormFromBounded', zero_mul, f_zero, zero_div, ciSup_const]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ seminormFromBounded' f 0 = 0
have simp_rw₁ : Eq (α := ℝ) (⨆ (y : R), f 0 / f y) 0
Tactic: simp_rw [seminormFromBounded', zero_mul, f_zero, zero_div, ciSup_const]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ seminormFromBounded' f 0 = 0
have simp_rw₂ : Eq (α := ℝ) (⨆ (y : R), 0 / f y) 0
Tactic: simp_rw [seminormFromBounded', zero_mul, f_zero, zero_div, ciSup_const]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ seminormFromBounded' f 0 = 0
have simp_rw₃ : Eq (α := ℝ) (⨆ (y : R), 0) 0
Tactic: simp_rw [seminormFromBounded', zero_mul, f_zero, zero_div, ciSup_const]
-- 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
⊢ 0 ≤ c * f x
have inl : ∀ (hx : f x = 0 x), 0 ≤ c * f x
Tactic: rcases (f_nonneg x).eq_or_lt' with hx | hx
-- 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
inl : ∀ (hx : f x = 0 x), 0 ≤ c * f x
⊢ 0 ≤ c * f x
have inr : ∀ (hx : 0 x < f x), 0 ≤ c * f x
Tactic: rcases (f_nonneg x).eq_or_lt' with hx | hx
-- 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 : R
hx : 0 x < f x
⊢ 0 ≤ c * f x
have hx₁ : 0 < f x
Tactic: change 0 < f x at hx
Cleared hypotheses: hx
-- 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 : R
hx : 0 < f x
⊢ 0 ≤ c
have f_mul₁ : f (x * 1) ≤ c * f x * f 1
Tactic: specialize f_mul x 1
Cleared hypotheses: f_mul
-- 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
x : R
hx : 0 < f x
f_mul : f (x * 1) ≤ c * f x * f 1
⊢ 0 ≤ c
have f_mul₁ : 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
Cleared hypotheses: f_mul
-- 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
x : R
hx : 0 < f x
f_mul : 1 ≤ c * f 1
⊢ 0 ≤ c
have f_nonneg₁ : 0 ≤ f 1
Tactic: replace f_nonneg : 0 ≤ f 1 := f_nonneg 1
Cleared hypotheses: f_nonneg
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ 0 ≤ c
have inl : ∀ (h1 : f 1 = 0), 0 ≤ c
Tactic: rcases f_nonneg.eq_or_lt' with h1 | h1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ 0 ≤ c
have inr : ∀ (h1 : 0 < f 1), 0 ≤ c
Tactic: rcases f_nonneg.eq_or_lt' with h1 | h1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ 0 ≤ c
have linarith : c < 0 → -1 + HSub.hSub (α := ℝ) 1 0 = 0
Tactic: linarith [show (1 : ℝ) ≤ 0 by simpa [h1] using f_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (hypothesis)
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
⊢ 0 ≤ c
have f_mul₁ : 1 / f 1 ≤ c
Tactic: rw [← div_le_iff₀ h1] at f_mul
Cleared hypotheses: f_mul, f_nonneg, h1
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ 0 ≤ c
have linarith : c < 0 → 1 * (1 / f 1) - 1 * c + (c - 0) + (HMul.hMul (α := ℝ) 1 0 - 1 * (1 / f 1)) = 0
Tactic: linarith [one_div_pos.mpr h1]
-- 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 : R
hx : 0 < f x
⊢ 0 ≤ c * f x
have hc : 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]
-- 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
⊢ BddAbove (α := ℝ) (Set.range fun (y : R) ↦ f (x * y) / f y)
have h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (y : R) ↦ f (x * y) / f y)) (c * f x)
Tactic: use c * f 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 y : R
⊢ (fun (y : R) ↦ f (x * y) / f y) y ≤ c * f x
have h : ∀ (hy0 : f y = 0 y), (fun (y : R) ↦ f (x * y) / f y) y ≤ c * f x
Tactic: rcases (f_nonneg y).eq_or_lt' with hy0 | hy0
-- 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
h : ∀ (hy0 : f y = 0 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
have h₁ : ∀ (hy0 : 0 y < f y), (fun (y : R) ↦ f (x * y) / f y) y ≤ c * f x
Tactic: rcases (f_nonneg y).eq_or_lt' with hy0 | hy0
-- 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
⊢ seminormFromBounded' f x ≤ c * f x
have refine : ∀ (y : R), f (x * y) / f y ≤ c * f x
Tactic: refine ciSup_le (fun 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
⊢ f (x * y) / f y ≤ c * f x
have inl : ∀ (hy : f y = 0 y), f (x * y) / f y ≤ c * f x
Tactic: rcases (f_nonneg y).eq_or_lt' with hy | hy
-- 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
inl : ∀ (hy : f y = 0 y), f (x * y) / f y ≤ c * f x
⊢ f (x * y) / f y ≤ c * f x
have inr : ∀ (hy : 0 y < f y), f (x * y) / f y ≤ c * f x
Tactic: rcases (f_nonneg y).eq_or_lt' with hy | hy
-- 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 : 0 y < f y
⊢ f (x * y) / f y ≤ c * f x
have inr : f (x * y) ≤ c * f x * f y
Tactic: rw [div_le_iff₀ hy]
-- 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
⊢ f x ≤ f 1 * seminormFromBounded' f x
have pos : ∀ (h1 : f 1 = 0), f x ≤ f 1 * seminormFromBounded' f x
Tactic: by_cases h1 : f 1 = 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 : R
pos : ∀ (h1 : f 1 = 0), f x ≤ f 1 * seminormFromBounded' f x
⊢ f x ≤ f 1 * seminormFromBounded' f x
have neg : ∀ (h1 : ¬f 1 = 0), f x ≤ f 1 * seminormFromBounded' f x
Tactic: by_cases h1 : f 1 = 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 : R
h1 : f 1 = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x
have f_mul₁ : f (x * 1) ≤ c * f x * f 1
Tactic: specialize f_mul x 1
Cleared hypotheses: f_mul
-- 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
x : R
h1 : f 1 = 0
f_mul : f (x * 1) ≤ c * f x * f 1
⊢ f x ≤ f 1 * seminormFromBounded' f x
have f_mul₁ : f x ≤ 0
Tactic: rw [mul_one, h1, mul_zero] at f_mul
Cleared hypotheses: f_mul
-- 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
x : R
h1 : f 1 = 0
f_mul : f x ≤ 0
⊢ f x ≤ f 1 * seminormFromBounded' f x
have hx0 : f x = 0
Tactic: have hx0 : f x = 0 := f_mul.antisymm (f_nonneg _)
-- 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
x : R
h1 : f 1 = 0
f_mul : f x ≤ 0
hx0 : f x = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x
have pos : 0 ≤ f 1 * seminormFromBounded' f x
Tactic: rw [hx0, h1, zero_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
x : R
h1 : f 1 = 0
f_mul : f x ≤ 0
hx0 : f x = 0
pos : 0 ≤ f 1 * seminormFromBounded' f x
⊢ f x ≤ f 1 * seminormFromBounded' f x
have pos₁ : 0 ≤ 0 * seminormFromBounded' f x
Tactic: rw [hx0, h1, zero_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
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
⊢ f x ≤ f 1 * seminormFromBounded' f x
have pos₂ : LE.le (α := ℝ) 0 0
Tactic: rw [hx0, h1, zero_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
x : R
h1 : ¬f 1 = 0
⊢ f x ≤ f 1 * seminormFromBounded' f x
have neg : f x / f 1 ≤ seminormFromBounded' f x
Tactic: rw [mul_comm, ← div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) h1)]
-- 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
h1 : ¬f 1 = 0
| f x / f 1
have rw : f (x * 1) / f 1
Tactic: rw [← mul_one 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 : R
h1 : ¬f 1 = 0
⊢ f x / f 1 ≤ seminormFromBounded' f x
have neg : f (x * 1) / f 1 ≤ seminormFromBounded' f x
Tactic: conv_lhs => rw [← mul_one 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 : R
⊢ seminormFromBounded' f x = 0 ↔ f x = 0
have refine_1 : ∀ (h : seminormFromBounded' f x = 0), f x = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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
refine_1 : ∀ (h : seminormFromBounded' f x = 0), f x = 0
⊢ seminormFromBounded' f x = 0 ↔ f x = 0
have refine_2 : ∀ (h : f x = 0), seminormFromBounded' f x = 0
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- 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 : R
h : seminormFromBounded' f x = 0
⊢ f x = 0
have hf : f x ≤ f 1 * seminormFromBounded' f x
Tactic: have hf := seminormFromBounded_ge f_nonneg f_mul x
-- 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 : R
h : seminormFromBounded' f x = 0
hf : f x ≤ f 1 * seminormFromBounded' f x
⊢ f x = 0
have hf₁ : f x ≤ 0
Tactic: rw [h, mul_zero] at hf
Cleared hypotheses: hf
-- 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 : R
h : f x = 0
⊢ seminormFromBounded' f x = 0
have hf : seminormFromBounded' f x ≤ c * f x
Tactic: have hf : seminormFromBounded' f x ≤ c * f x :=
      seminormFromBounded_le f_nonneg f_mul x
-- 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 : R
h : f x = 0
hf : seminormFromBounded' f x ≤ c * f x
⊢ seminormFromBounded' f x = 0
have hf₁ : seminormFromBounded' f x ≤ 0
Tactic: rw [h, mul_zero] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
⊢ Eq (α := ℝ) (⨆ (y : R), f (-x * y) / f y) (⨆ (y : R), f (x * y) / f y)
have e_s : Eq.{u_1 + 1} (α := R → ℝ) (fun (y : R) ↦ f (-x * y) / f y) fun (y : R) ↦ f (x * y) / f y
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x : R
⊢ Eq.{u_1 + 1} (α := R → ℝ) (fun (y : R) ↦ f (-x * y) / f y) fun (y : R) ↦ f (x * y) / f y
have e_s : ∀ (y : R), f (-x * y) / f y = f (x * y) / f y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
f_neg : ∀ (x : R), f (-x) = f x
x y : R
⊢ f (-x * y) / f y = f (x * y) / f y
have e_s : f (-(x * y)) / f y = f (x * y) / f y
Tactic: rw [neg_mul, f_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f (-x * y) / f y = f (x * y) / f y
have e_s₁ : f (x * y) / f y = f (x * y) / f y
Tactic: rw [neg_mul, f_neg]
-- 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
⊢ seminormFromBounded' f (x * y) ≤ seminormFromBounded' f x * seminormFromBounded' f y
have H : ∀ (x_1 : R), f (x * y * x_1) / f x_1 ≤ seminormFromBounded' f x * seminormFromBounded' f y
Tactic: apply ciSup_le
-- 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
⊢ ∀ (x_1 : R), f (x * y * x_1) / f x_1 ≤ seminormFromBounded' f x * seminormFromBounded' f y
have pos : ∀ (hy : seminormFromBounded' f y = 0) (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
-- 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
pos :
  ∀ (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
have neg : ∀ (hy : ¬seminormFromBounded' f y = 0) (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
-- 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
⊢ ∀ (x_1 : R), f (x * y * x_1) / f x_1 ≤ seminormFromBounded' f x * seminormFromBounded' f y
have hy₁ : f y = 0
Tactic: rw [seminormFromBounded_eq_zero_iff f_nonneg f_mul] at hy
Cleared hypotheses: hy
-- 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 : f y = 0
z : R
⊢ f (x * y * z) / f z ≤ seminormFromBounded' f x * seminormFromBounded' f y
have pos : 0 ≤ 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]
-- 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 x * seminormFromBounded' f y
have neg : f (x * y * z) / f z / seminormFromBounded' f y ≤ seminormFromBounded' f x
Tactic: rw [← div_le_iff₀ (lt_of_le_of_ne' (seminormFromBounded_nonneg f_nonneg f_mul _) hy)]