awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x : L
g : AlgebraNorm K L :=
  let __src := Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f;
  { toAddGroupSeminorm := __src.toAddGroupSeminorm, mul_le' := ⋯, eq_zero_of_map_eq_zero' := ⋯, smul' := ⋯ }
hg_pow : IsPowMul (R := L) (⇑g : (a : L) → ℝ)
hgx : Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) ((g : (a : L) → ℝ) x : ℝ)
rw : (g : (a : L) → ℝ) x = spectralNorm K L x
rw₁ : (spectralAlgNorm K L : (a : L) → ℝ) x = spectralNorm K L x
⊢ (f : (a : L) → ℝ) x = spectralNorm K L x
have rw₂ : spectralNorm K L x = spectralNorm K L x
Tactic: rw [hgx, spectralNorm_unique hg_pow, spectralAlgNorm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u
inst : NontriviallyNormedField K
hu : IsUltrametricDist K
L : Type u_2
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
inst_3 : Algebra.IsAlgebraic K L
inst_4 : CompleteSpace K
x : L
⊢ ‖x‖ = spectralNorm K L x
have rw : (toMulAlgebraNorm K L : (a : L) → ℝ) x = spectralNorm K L x
Tactic: rw [← toMulAlgebraNorm_apply K L x, ← spectralAlgNorm_def, ← MulAlgebraNorm.coe_AlgebraNorm,
      spectralNorm_unique (f := (toMulAlgebraNorm K L).toAlgebraNorm)
      (MulRingNorm.isPowMul (toMulAlgebraNorm K L).toMulRingNorm)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u
inst : NontriviallyNormedField K
hu : IsUltrametricDist K
L : Type u_2
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
inst_3 : Algebra.IsAlgebraic K L
inst_4 : CompleteSpace K
x : L
rw : (toMulAlgebraNorm K L : (a : L) → ℝ) x = spectralNorm K L x
⊢ ‖x‖ = spectralNorm K L x
have rw₁ : Eq (α := ℝ) ((toMulAlgebraNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ)
Tactic: rw [← toMulAlgebraNorm_apply K L x, ← spectralAlgNorm_def, ← MulAlgebraNorm.coe_AlgebraNorm,
      spectralNorm_unique (f := (toMulAlgebraNorm K L).toAlgebraNorm)
      (MulRingNorm.isPowMul (toMulAlgebraNorm K L).toMulRingNorm)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u
inst : NontriviallyNormedField K
hu : IsUltrametricDist K
L : Type u_2
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
inst_3 : Algebra.IsAlgebraic K L
inst_4 : CompleteSpace K
x : L
rw : (toMulAlgebraNorm K L : (a : L) → ℝ) x = spectralNorm K L x
rw₁ : Eq (α := ℝ) ((toMulAlgebraNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ)
⊢ ‖x‖ = spectralNorm K L x
have rw₂ : Eq (α := ℝ) ((MulAlgebraNorm.toAlgebraNorm (toMulAlgebraNorm K L) : (a : L) → ℝ) x : ℝ)
  ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ)
Tactic: rw [← toMulAlgebraNorm_apply K L x, ← spectralAlgNorm_def, ← MulAlgebraNorm.coe_AlgebraNorm,
      spectralNorm_unique (f := (toMulAlgebraNorm K L).toAlgebraNorm)
      (MulRingNorm.isPowMul (toMulAlgebraNorm K L).toMulRingNorm)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u
inst : NontriviallyNormedField K
hu : IsUltrametricDist K
L : Type u_2
inst_1 : NormedField L
inst_2 : NormedAlgebra K L
inst_3 : Algebra.IsAlgebraic K L
inst_4 : CompleteSpace K
x : L
rw : (toMulAlgebraNorm K L : (a : L) → ℝ) x = spectralNorm K L x
rw₁ : Eq (α := ℝ) ((toMulAlgebraNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ)
rw₂ :
  Eq (α := ℝ) ((MulAlgebraNorm.toAlgebraNorm (toMulAlgebraNorm K L) : (a : L) → ℝ) x : ℝ)
    ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ)
⊢ ‖x‖ = spectralNorm K L x
have rw₃ : Eq (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ)
Tactic: rw [← toMulAlgebraNorm_apply K L x, ← spectralAlgNorm_def, ← MulAlgebraNorm.coe_AlgebraNorm,
      spectralNorm_unique (f := (toMulAlgebraNorm K L).toAlgebraNorm)
      (MulRingNorm.isPowMul (toMulAlgebraNorm K L).toMulRingNorm)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 :
  LE.le (α := ℝ) ((RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)) : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
x : L
hx : x ≠ 0
hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
k : K
y_1 y : L
⊢ spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
    spectralNorm.{u, v} K L ((algebraMap K L : (a : K) → L) k : L) * spectralNorm K L y
have rw : spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = ‖k‖ * spectralNorm K L y
Tactic: rw [spectralNorm_extends, ← Algebra.smul_def, ← spectralAlgNorm_def,
          map_smul_eq_mul _ _ _, spectralAlgNorm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 :
  LE.le (α := ℝ) ((RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)) : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
x : L
hx : x ≠ 0
hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
k : K
y_1 y : L
rw : spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = ‖k‖ * spectralNorm K L y
⊢ spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
    spectralNorm.{u, v} K L ((algebraMap K L : (a : K) → L) k : L) * spectralNorm K L y
have rw₁ : spectralNorm K L (k • y) = ‖k‖ * spectralNorm K L y
Tactic: rw [spectralNorm_extends, ← Algebra.smul_def, ← spectralAlgNorm_def,
          map_smul_eq_mul _ _ _, spectralAlgNorm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 :
  LE.le (α := ℝ) ((RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)) : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
x : L
hx : x ≠ 0
hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
k : K
y_1 y : L
rw : spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = ‖k‖ * spectralNorm K L y
rw₁ : spectralNorm K L (k • y) = ‖k‖ * spectralNorm K L y
⊢ spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
    spectralNorm.{u, v} K L ((algebraMap K L : (a : K) → L) k : L) * spectralNorm K L y
have rw₂ : (spectralAlgNorm K L : (a : L) → ℝ) (k • y) = ‖k‖ * spectralNorm K L y
Tactic: rw [spectralNorm_extends, ← Algebra.smul_def, ← spectralAlgNorm_def,
          map_smul_eq_mul _ _ _, spectralAlgNorm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 :
  LE.le (α := ℝ) ((RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)) : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
x : L
hx : x ≠ 0
hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
k : K
y_1 y : L
rw : spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = ‖k‖ * spectralNorm K L y
rw₁ : spectralNorm K L (k • y) = ‖k‖ * spectralNorm K L y
rw₂ : (spectralAlgNorm K L : (a : L) → ℝ) (k • y) = ‖k‖ * spectralNorm K L y
⊢ spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
    spectralNorm.{u, v} K L ((algebraMap K L : (a : K) → L) k : L) * spectralNorm K L y
have rw₃ : HMul.hMul (β := ℝ) ‖k‖ ((spectralAlgNorm K L : (a : L) → ℝ) y : ℝ) = ‖k‖ * spectralNorm K L y
Tactic: rw [spectralNorm_extends, ← Algebra.smul_def, ← spectralAlgNorm_def,
          map_smul_eq_mul _ _ _, spectralAlgNorm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 :
  LE.le (α := ℝ) ((RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)) : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
x : L
hx : x ≠ 0
hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
k : K
y_1 y : L
rw : spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) = ‖k‖ * spectralNorm K L y
rw₁ : spectralNorm K L (k • y) = ‖k‖ * spectralNorm K L y
rw₂ : (spectralAlgNorm K L : (a : L) → ℝ) (k • y) = ‖k‖ * spectralNorm K L y
rw₃ : HMul.hMul (β := ℝ) ‖k‖ ((spectralAlgNorm K L : (a : L) → ℝ) y : ℝ) = ‖k‖ * spectralNorm K L y
⊢ spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
    spectralNorm.{u, v} K L ((algebraMap K L : (a : K) → L) k : L) * spectralNorm K L y
have rw₄ : ‖k‖ * spectralNorm K L y = ‖k‖ * spectralNorm K L y
Tactic: rw [spectralNorm_extends, ← Algebra.smul_def, ← spectralAlgNorm_def,
          map_smul_eq_mul _ _ _, spectralAlgNorm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 :
  LE.le (α := ℝ) ((RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)) : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
x : L
hx : x ≠ 0
hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
k : K
y : L
⊢ (normFromConst h1 hx' ⋯).toFun (k • y) = ‖k‖ * (normFromConst h1 hx' ⋯).toFun y
have h_mul : ∀ (y : L),
  spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
    spectralNorm.{u, v} K L ((algebraMap K L : (a : K) → L) k : L) * spectralNorm K L y
Tactic: have h_mul : ∀ y : L, spectralNorm K L (algebraMap K L k * y) =
          spectralNorm K L (algebraMap K L k) * spectralNorm K L y := fun y ↦ by
        rw [spectralNorm_extends, ← Algebra.smul_def, ← spectralAlgNorm_def,
          map_smul_eq_mul _ _ _, spectralAlgNorm_def]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 :
  LE.le (α := ℝ) ((RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)) : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
x : L
hx : x ≠ 0
hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
k : K
y : L
h_mul :
  ∀ (y : L),
    spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
      spectralNorm.{u, v} K L ((algebraMap K L : (a : K) → L) k : L) * spectralNorm K L y
⊢ spectralNorm.{u, v} K L ((algebraMap K L : (a : K) → L) k : L) =
    seminormFromConst' x (RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)))
      ((algebraMap K L : (a : K) → L) k)
have rw : spectralNorm.{u, v} K L ((algebraMap K L : (a : K) → L) k : L) =
  (RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)) : (a : L) → ℝ)
    ((algebraMap K L : (a : K) → L) k : L)
Tactic: rw [seminormFromConst_apply_of_isMul h1 hx' spectralAlgNorm_isPowMul h_mul]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 :
  LE.le (α := ℝ) ((RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)) : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
x : L
hx : x ≠ 0
hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
k : K
y : L
h_mul :
  ∀ (y : L),
    spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
      spectralNorm.{u, v} K L ((algebraMap K L : (a : K) → L) k : L) * spectralNorm K L y
⊢ (normFromConst h1 hx' ⋯).toFun (k • y) = ‖k‖ * (normFromConst h1 hx' ⋯).toFun y
have h : spectralNorm.{u, v} K L ((algebraMap K L : (a : K) → L) k : L) =
  seminormFromConst' x (RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)))
    ((algebraMap K L : (a : K) → L) k)
Tactic: have h : spectralNorm K L (algebraMap K L k) =
        seminormFromConst' x (spectralAlgNorm K L).toRingSeminorm (algebraMap K L k) := by
          rw [seminormFromConst_apply_of_isMul h1 hx' spectralAlgNorm_isPowMul h_mul]; rfl
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
h1 :
  LE.le (α := ℝ) ((RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)) : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
x : L
hx : x ≠ 0
hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
k : K
y : L
h_mul :
  ∀ (y : L),
    spectralNorm K L (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
      spectralNorm.{u, v} K L ((algebraMap K L : (a : K) → L) k : L) * spectralNorm K L y
h :
  spectralNorm.{u, v} K L ((algebraMap K L : (a : K) → L) k : L) =
    seminormFromConst' x (RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)))
      ((algebraMap K L : (a : K) → L) k)
⊢ (normFromConst h1 hx' ⋯).toFun (k • y) = ‖k‖ * (normFromConst h1 hx' ⋯).toFun y
have rw : (normFromConst h1 hx' sorry).toFun (HMul.hMul (α := L) ((algebraMap K L : (a : K) → L) k : L) y) =
  seminormFromConst' x (RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)))
      ((algebraMap K L : (a : K) → L) k) *
    (normFromConst h1 hx' sorry).toFun y
Tactic: rw [← @spectralNorm_extends K _ L _ _ k, Algebra.smul_def, h]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x y : L
⊢ (spectralAlgNorm K L : (a : L) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) y : ℝ)
have pos : ∀ (hx : x = 0),
  (spectralAlgNorm K L : (a : L) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) y : ℝ)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x y : L
pos :
  ∀ (hx : x = 0),
    (spectralAlgNorm K L : (a : L) → ℝ) (x * y) =
      HMul.hMul (α := ℝ) (β := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ)
        ((spectralAlgNorm K L : (a : L) → ℝ) y : ℝ)
⊢ (spectralAlgNorm K L : (a : L) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) y : ℝ)
have neg : ∀ (hx : ¬x = 0),
  (spectralAlgNorm K L : (a : L) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) y : ℝ)
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x y : L
hx : ¬x = 0
⊢ (spectralAlgNorm K L : (a : L) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) y : ℝ)
have hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
Tactic: have hx' : spectralAlgNorm K L x ≠ 0 :=
      ne_of_gt (spectralNorm_zero_lt hx (Algebra.IsAlgebraic.isAlgebraic x))
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x y : L
hx : ¬x = 0
hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
⊢ (spectralAlgNorm K L : (a : L) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) y : ℝ)
have hf1 : LE.le (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
Tactic: have hf1 : (spectralAlgNorm K L) 1 ≤ 1 := le_of_eq spectralAlgNorm_one
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x y : L
hx : ¬x = 0
hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
hf1 : LE.le (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
⊢ (spectralAlgNorm K L : (a : L) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) y : ℝ)
have hf : let f := algNormFromConst hf1 hx;
f = algNormFromConst hf1 hx
Tactic: set f : AlgebraNorm K L := algNormFromConst hf1 hx with hf
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (hypothesis)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x y : L
hx : ¬x = 0
hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
hf1 : LE.le (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
f : AlgebraNorm K L := algNormFromConst hf1 hx
hf : f = algNormFromConst hf1 hx
⊢ (spectralAlgNorm K L : (a : L) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) y : ℝ)
have hf_pow : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
Tactic: have hf_pow : IsPowMul f := seminormFromConst_isPowMul hf1 hx' isPowMul_spectralNorm
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x y : L
hx : ¬x = 0
hx' : Ne (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) (0 : ℝ)
hf1 : LE.le (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
f : AlgebraNorm K L := algNormFromConst hf1 hx
hf : f = algNormFromConst hf1 hx
hf_pow : IsPowMul (R := L) (⇑f : (a : L) → ℝ)
⊢ (spectralAlgNorm K L : (a : L) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) y : ℝ)
have neg : (algNormFromConst hf1 hx : (a : L) → ℝ) (x * y) =
  HMul.hMul (α := ℝ) (β := ℝ) ((algNormFromConst hf1 hx : (a : L) → ℝ) x : ℝ)
    ((algNormFromConst hf1 hx : (a : L) → ℝ) y : ℝ)
Tactic: rw [← spectralNorm_unique hf_pow, hf]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x y : L
⊢ spectralNorm K L (x - y) = spectralNorm K L (y - x)
have rw : spectralNorm K L (-(y - x)) = spectralNorm K L (y - x)
Tactic: rw [← neg_sub, spectralNorm_neg (Algebra.IsAlgebraic.isAlgebraic _)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x y : L
rw : spectralNorm K L (-(y - x)) = spectralNorm K L (y - x)
⊢ spectralNorm K L (x - y) = spectralNorm K L (y - x)
have rw₁ : spectralNorm K L (y - x) = spectralNorm K L (y - x)
Tactic: rw [← neg_sub, spectralNorm_neg (Algebra.IsAlgebraic.isAlgebraic _)]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x y : L
⊢ (↑(NNReal.mk ((fun (x y : L) ↦ spectralNorm K L (x - y)) x y) ⋯) : ENNReal) =
    ENNReal.ofReal (spectralNorm K L (x - y))
have rw : (↑(NNReal.mk ((fun (x y : L) ↦ spectralNorm K L (x - y)) x y) sorry) : ENNReal) =
  (↑(NNReal.mk (spectralNorm K L (x - y)) sorry) : ENNReal)
Tactic: rw [ENNReal.ofReal_eq_coe_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x y : L
rw :
  (↑(NNReal.mk ((fun (x y : L) ↦ spectralNorm K L (x - y)) x y) ⋯) : ENNReal) =
    (↑(NNReal.mk (spectralNorm K L (x - y)) ⋯) : ENNReal)
⊢ (↑(NNReal.mk ((fun (x y : L) ↦ spectralNorm K L (x - y)) x y) ⋯) : ENNReal) =
    ENNReal.ofReal (spectralNorm K L (x - y))
have rw₁ : 0 ≤ spectralNorm K L (x - y)
Tactic: rw [ENNReal.ofReal_eq_coe_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x y : L
hxy : spectralNorm K L (x - y) = 0
⊢ x = y
have rw : x - y = 0
Tactic: rw [← sub_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x y : L
⊢ spectralNorm K L (x - y) = spectralNorm K L (-x + y)
have rw : IsAlgebraic K (x - y)
Tactic: rw [← spectralNorm_neg, sub_eq_add_neg, neg_add, neg_neg]
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
⊢ NormedAddCommGroup L
have haveI : (this : NormedField L) → NormedAddCommGroup L
Tactic: haveI : NormedField L := normedField K L
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
⊢ SeminormedAddCommGroup L
have have : (this : NormedField L) → SeminormedAddCommGroup L
Tactic: have : NormedField L := normedField K L
-- Lean 4 proof step from Mathlib.Analysis.Normed.Unbundled.SpectralNorm (goal)
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L : Type v
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
x_1 : SeminormedAddCommGroup L := seminormedAddCommGroup K L
r : K
x : L
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
have change : (spectralAlgNorm K L : (a : L) → ℝ) (r • x) ≤ HMul.hMul (β := ℝ) ‖r‖ ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ)
Tactic: change spectralAlgNorm K L (r • x) ≤ ‖r‖ * spectralAlgNorm K L x