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_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
⊢ f x_1 * (f x / f x) ≤ f x_1
have neg₁ : f x_1 ≤ f x_1
Tactic: rw [div_self hx, mul_one]
-- 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
⊢ f x ≤ ⨆ (y : R), f x * (f y / f y)
have pos : ∀ (f_ne_zero : f ≠ 0), f x ≤ ⨆ (y : R), f x * (f y / f y)
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
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)
⊢ f x ≤ ⨆ (y : R), f x * (f y / f y)
have neg : ∀ (f_ne_zero : f = 0), f x ≤ ⨆ (y : R), f x * (f y / f y)
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
x : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
| f x
have rw : f x * 1
Tactic: rw [← mul_one (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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
⊢ f x ≤ ⨆ (y : R), f x * (f y / f y)
have pos : f x * 1 ≤ ⨆ (y : R), f x * (f y / f y)
Tactic: conv_lhs => rw [← mul_one (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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
⊢ f x * 1 ≤ ⨆ (y : R), f x * (f y / f y)
have pos : f x * (f 1 / f 1) ≤ ⨆ (y : R), f x * (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_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))
have h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (y : R) ↦ f x * (f y / f y))) (f x)
Tactic: use 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 : R
hx : ∀ (y : R), f (x * y) = f x * f y
f_ne_zero : f ≠ 0
y : R
⊢ (fun (y : R) ↦ f x * (f y / f y)) y ≤ f x
have pos : ∀ (hy0 : f y = 0), (fun (y : R) ↦ f x * (f y / f y)) y ≤ f x
Tactic: by_cases hy0 : 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 : 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
⊢ (fun (y : R) ↦ f x * (f y / f y)) y ≤ f x
have neg : ∀ (hy0 : ¬f y = 0), (fun (y : R) ↦ f x * (f y / f y)) y ≤ f x
Tactic: by_cases hy0 : 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 : 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
have pos : 0 ≤ f x
Tactic: simp only [hy0, div_zero, mul_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
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
⊢ f x * (f 1 / f 1) ≤ ⨆ (y : R), f x * (f y / f y)
have h_bdd : 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]
-- 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
f_ne_zero : f = 0
⊢ f x ≤ ⨆ (y : R), f x * (f y / f y)
have neg : LE.le (α := ℝ) 0 0
Tactic: simp_rw [f_ne_zero, Pi.zero_apply, zero_div, zero_mul, ciSup_const]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
have a : ⨆ (y : R), f (x * 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 → ℝ
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
have a₁ : f x ≤ ⨆ (y : R), f (x * 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 → ℝ
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
have a : ∀ (y : R), f (x * y) / f y ≤ 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 → ℝ
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
have pos : ∀ (hy : f y = 0), f (x * y) / f y ≤ f x
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 → ℝ
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
⊢ f (x * y) / f y ≤ f x
have neg : ∀ (hy : ¬f y = 0), f (x * y) / f y ≤ f x
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 → ℝ
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 y ≤ f x
have pos : 0 ≤ f x
Tactic: rw [hy, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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 y ≤ f x
have neg : f (x * y) ≤ f x * f y
Tactic: rw [div_le_iff₀ (lt_of_le_of_ne' (f_nonneg _) hy)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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)
have h : Membership.mem (γ := Set ℝ) (upperBounds (Set.range fun (y : R) ↦ f (x * y) / f y)) (f x)
Tactic: use f x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ (fun (y : R) ↦ f (x * y) / f y) y ≤ f x
have pos : ∀ (hy0 : f y = 0), (fun (y : R) ↦ f (x * y) / f y) y ≤ f x
Tactic: by_cases hy0 : f y = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ (fun (y : R) ↦ f (x * y) / f y) y ≤ f x
have neg : ∀ (hy0 : ¬f y = 0), (fun (y : R) ↦ f (x * y) / f y) y ≤ f x
Tactic: by_cases hy0 : f y = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ (fun (y : R) ↦ f (x * y) / f y) y ≤ f x
have pos : 0 ≤ f x
Tactic: simp only [hy0, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ (fun (y : R) ↦ f (x * y) / f y) y ≤ f x
have neg : f (x * y) ≤ f x * f y
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]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (hypothesis)
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
⊢ f x ≤ ⨆ (y : R), f (x * y) / f y
have h_bdd : 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
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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 ≤ ⨆ (y : R), f (x * y) / f y
have h : f x = f (x * 1) / f 1
Tactic: convert! le_ciSup h_bdd (1 : R)
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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 = f (x * 1) / f 1
have pos : ∀ (h0 : f x = 0), f x = f (x * 1) / f 1
Tactic: by_cases h0 : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f x = f (x * 1) / f 1
have neg : ∀ (h0 : ¬f x = 0), f x = f (x * 1) / f 1
Tactic: by_cases h0 : f x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f x = f (x * 1) / f 1
have pos : f x = f x / f 1
Tactic: rw [mul_one, h0, zero_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f x = f (x * 1) / f 1
have pos₁ : 0 = 0 / f 1
Tactic: rw [mul_one, h0, zero_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f x = f (x * 1) / f 1
have pos₂ : Eq (α := ℝ) 0 0
Tactic: rw [mul_one, h0, zero_div]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
⊢ f 1 = 1
have apply : 1 ≤ f 1
Tactic: apply h_one.antisymm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (hypothesis)
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
⊢ 1 ≤ f 1
have hx₁ : f (x * 1) ≤ f x * f 1
Tactic: specialize hx 1
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (hypothesis)
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
⊢ f x = f (x * 1) / f 1
have heq : f 1 = 1
Tactic: have heq : f 1 = 1 := by
        apply h_one.antisymm
        specialize hx 1
        rw [mul_one, le_mul_iff_one_le_right (lt_of_le_of_ne (f_nonneg _) (Ne.symm h0))] at hx
        exact hx
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
heq : f 1 = 1
⊢ f x = f (x * 1) / f 1
have neg : f x = f (x * 1) / 1
Tactic: rw [heq, mul_one, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
heq : f 1 = 1
neg : f x = f (x * 1) / 1
⊢ f x = f (x * 1) / f 1
have neg₁ : f x = f x / 1
Tactic: rw [heq, mul_one, div_one]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
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
heq : f 1 = 1
neg : f x = f (x * 1) / 1
neg₁ : f x = f x / 1
⊢ f x = f (x * 1) / f 1
have neg₂ : f x = f x
Tactic: rw [heq, mul_one, div_one]
-- 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 ≠ 0
have obtain : ∀ (x : R) (hx : f x ≠ 0 x), seminormFromBounded' f ≠ 0
Tactic: obtain ⟨x, hx⟩ := Function.ne_iff.mp f_ne_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 x
⊢ seminormFromBounded' f ≠ 0
have rw : ∃ (a : R), seminormFromBounded' f a ≠ 0 a
Tactic: rw [Function.ne_iff]
-- 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 x
⊢ ∃ (a : R), seminormFromBounded' f a ≠ 0 a
have h : seminormFromBounded' f x ≠ 0 x
Tactic: use 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
hx : f x ≠ 0 x
⊢ seminormFromBounded' f x ≠ 0 x
have h : ¬f x = 0
Tactic: rw [ne_eq, Pi.zero_apply, seminormFromBounded_eq_zero_iff f_nonneg f_mul 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
⊢ seminormFromBounded' f ⁻¹' {0} = f ⁻¹' {0}
have h : ∀ (x : R), x ∈ seminormFromBounded' f ⁻¹' {0} ↔ x ∈ f ⁻¹' {0}
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
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
f_neg : ∀ (x : R), f (-x) = f x
⊢ (∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0) ↔ f ⁻¹' {0} = {0}
have refine_1 : ∀ (h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0), f ⁻¹' {0} = {0}
Tactic: refine ⟨fun h0 ↦ ?_, fun h_ker x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
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
f_neg : ∀ (x : R), f (-x) = f x
refine_1 :
  ∀ (h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0), f ⁻¹' {0} = {0}
⊢ (∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0) ↔ f ⁻¹' {0} = {0}
have refine_2 : ∀ (h_ker : f ⁻¹' {0} = {0}) (x : R) (hx : (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0), x = 0
Tactic: refine ⟨fun h0 ↦ ?_, fun h_ker x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
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
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
⊢ f ⁻¹' {0} = {0}
have refine_1 : seminormFromBounded' f ⁻¹' {0} = {0}
Tactic: rw [← seminormFromBounded_ker 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_zero : f 0 = 0
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
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
⊢ seminormFromBounded' f ⁻¹' {0} = {0}
have refine_1 : ∀ (x : R), x ∈ seminormFromBounded' f ⁻¹' {0} ↔ Membership.mem (γ := Set R) {0} x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
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
f_neg : ∀ (x : R), f (-x) = f x
h0 : ∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0
x : R
h : x = 0
⊢ seminormFromBounded' f x = 0
have rw : seminormFromBounded' f 0 = 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded (goal)
Goal:
R : Type u_1
inst : CommRing R
f : R → ℝ
c : ℝ
f_zero : f 0 = 0
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
f_neg : ∀ (x : R), f (-x) = f x
h_ker : f ⁻¹' {0} = {0}
x : R
hx : (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0
⊢ x = 0
have refine_2 : seminormFromBounded' f x = 0
Tactic: rw [← Set.mem_singleton_iff, ← h_ker, Set.mem_preimage, Set.mem_singleton_iff,
      ← seminormFromBounded_eq_zero_iff f_nonneg f_mul 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
hx : ∀ (y : R), f (x * y) = f x * f y
y : R
⊢ seminormFromBounded' f (x * y) = seminormFromBounded' f x * seminormFromBounded' f y
have rw : seminormFromBounded' f (x * y) = f x * seminormFromBounded' f y
Tactic: rw [seminormFromBounded_of_mul_apply f_nonneg f_mul hx]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
x : R
⊢ BddBelow (Set.range (seminormFromConst_seq c f x))
have h : 0 ∈ lowerBounds (Set.range (seminormFromConst_seq c f x))
Tactic: use 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf : Eq (α := ℝ) ((f : (a : R) → ℝ) 0 : ℝ) (0 : ℝ)
⊢ Eq (α := ℕ → ℝ)
    (fun (n : ℕ) ↦
      HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (0 * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n))
    0
have h : ∀ (n : ℕ), HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (0 * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 0 n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf : Eq (α := ℝ) ((f : (a : R) → ℝ) 0 : ℝ) (0 : ℝ)
n : ℕ
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (0 * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 0 n
have h : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 0 n
Tactic: rw [zero_mul, hf, zero_div, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf : Eq (α := ℝ) ((f : (a : R) → ℝ) 0 : ℝ) (0 : ℝ)
n : ℕ
h : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 0 n
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (0 * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 0 n
have h₁ : 0 / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n = 0 n
Tactic: rw [zero_mul, hf, zero_div, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf : Eq (α := ℝ) ((f : (a : R) → ℝ) 0 : ℝ) (0 : ℝ)
n : ℕ
h : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 0 n
h₁ : 0 / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n = 0 n
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (0 * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 0 n
have h₂ : Eq (α := ℝ) 0 (0 n)
Tactic: rw [zero_mul, hf, zero_div, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hf : Eq (α := ℝ) ((f : (a : R) → ℝ) 0 : ℝ) (0 : ℝ)
n : ℕ
h : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) 0 : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 0 n
h₁ : 0 / HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n = 0 n
h₂ : Eq (α := ℝ) 0 (0 n)
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (0 * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 0 n
have h₃ : Eq (α := ℝ) 0 0
Tactic: rw [zero_mul, hf, zero_div, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SeminormFromConst (goal)
Goal:
R : Type u_1
inst : CommRing R
c : R
f : RingSeminorm R
hc : Ne (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) (0 : ℝ)
hpm : IsPowMul (R := R) (⇑f : (a : R) → ℝ)
n : ℕ
hn : 1 ≤ n
⊢ HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (1 * c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 1
have rw : HDiv.hDiv (α := ℝ) ((f : (a : R) → ℝ) (c ^ n) : ℝ) (HPow.hPow (α := ℝ) ((f : (a : R) → ℝ) c : ℝ) n) = 1
Tactic: rw [one_mul, hpm _ hn, div_self (pow_ne_zero n hc)]