awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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)

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
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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)
rw :
  (normFromConst h1 hx' ⋯).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' ⋯).toFun y
⊢ (normFromConst h1 hx' ⋯).toFun (k • y) = ‖k‖ * (normFromConst h1 hx' ⋯).toFun y

Tactic:
rw [← @spectralNorm_extends K _ L _ _ k, Algebra.smul_def, h]

Premises used: spectralNorm_extends, Algebra.smul_def
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 (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' ⋯).toFun y

Tactic:
seminormFromConst_isMul_of_isMul h1 hx' spectralAlgNorm_isPowMul h_mul y

Premises used: iInf, seminormFromConst_isMul_of_isMul, seminormFromConst', spectralAlgNorm_isPowMul
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 (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' ⋯).toFun y

Tactic:
exact seminormFromConst_isMul_of_isMul h1 hx' spectralAlgNorm_isPowMul h_mul y

Premises used: seminormFromConst_isMul_of_isMul, spectralAlgNorm_isPowMul
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
h1 :
  LE.le (α := ℝ) ((RingNorm.toRingSeminorm (AlgebraNorm.toRingNorm (spectralAlgNorm K L)) : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)
x y : L
hx : x ≠ 0
⊢ Eq (α := ℝ) ((algNormFromConst h1 hx : (a : L) → ℝ) y : ℝ) ((seminormFromConst h1 ⋯ ⋯ : (a : L) → ℝ) y : ℝ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ)
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 : ℝ)
⊢ (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
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ)

Tactic:
simp [hx, zero_mul, map_zero]

Premises used: MulZeroClass.zero_mul, map_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ 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))
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ)
⊢ LE.le (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
have hf1 : (spectralAlgNorm K L) 1 ≤ 1 := le_of_eq spectralAlgNorm_one
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ)
⊢ let f := algNormFromConst hf1 hx;
  f = algNormFromConst hf1 hx

Tactic:
set f : AlgebraNorm K L := algNormFromConst hf1 hx with hf

Premises used: algNormFromConst, AlgebraNorm
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ IsPowMul (R := L) (⇑f : (a : L) → ℝ)

Tactic:
have hf_pow : IsPowMul f := seminormFromConst_isPowMul hf1 hx' isPowMul_spectralNorm
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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) → ℝ)
neg :
  (algNormFromConst hf1 hx : (a : L) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((algNormFromConst hf1 hx : (a : L) → ℝ) x : ℝ)
      ((algNormFromConst hf1 hx : (a : L) → ℝ) y : ℝ)
⊢ (spectralAlgNorm K L : (a : L) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) y : ℝ)

Tactic:
rw [← spectralNorm_unique hf_pow, hf]

Premises used: spectralNorm_unique
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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) → ℝ)
⊢ (algNormFromConst hf1 hx : (a : L) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((algNormFromConst hf1 hx : (a : L) → ℝ) x : ℝ)
      ((algNormFromConst hf1 hx : (a : L) → ℝ) y : ℝ)

Tactic:
seminormFromConst_const_mul hf1 hx' isPowMul_spectralNorm _

Premises used: iInf, isPowMul_spectralNorm, seminormFromConst', seminormFromConst_const_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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) → ℝ)
⊢ (algNormFromConst hf1 hx : (a : L) → ℝ) (x * y) =
    HMul.hMul (α := ℝ) (β := ℝ) ((algNormFromConst hf1 hx : (a : L) → ℝ) x : ℝ)
      ((algNormFromConst hf1 hx : (a : L) → ℝ) y : ℝ)

Tactic:
exact seminormFromConst_const_mul hf1 hx' isPowMul_spectralNorm _

Premises used: isPowMul_spectralNorm, seminormFromConst_const_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : L
⊢ (spectralMulAlgNorm K L : (a : L) → ℝ) x = spectralNorm K L x

Tactic:
rfl

Premises used: iSup, spectralNorm, dite, spectralValue, rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : L
⊢ spectralNorm K L (x - x) = 0

Tactic:
simp [sub_self, spectralNorm_zero]

Premises used: sub_self, spectralNorm_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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)
rw₁ rw₂ : spectralNorm K L (y - x) = spectralNorm K L (y - x)
⊢ spectralNorm K L (x - y) = spectralNorm K L (y - x)

Tactic:
rw [← neg_sub, spectralNorm_neg (Algebra.IsAlgebraic.isAlgebraic _)]

Premises used: Algebra.IsAlgebraic.isAlgebraic, spectralNorm_neg, neg_sub
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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)
rw₁ : 0 ≤ spectralNorm K L (x - y)
rw₂ :
  (↑(NNReal.mk ((fun (x y : L) ↦ spectralNorm K L (x - y)) x y) ⋯) : ENNReal) =
    (↑(NNReal.mk (spectralNorm K L (x - y)) ⋯) : ENNReal)
rw₃ : 0 ≤ spectralNorm K L (x - y)
⊢ (↑(NNReal.mk ((fun (x y : L) ↦ spectralNorm K L (x - y)) x y) ⋯) : ENNReal) =
    ENNReal.ofReal (spectralNorm K L (x - y))

Tactic:
rw [ENNReal.ofReal_eq_coe_nnreal]

Premises used: ENNReal.ofReal_eq_coe_nnreal
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
rw : x - y = 0
⊢ x = y

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 = 0

Tactic:
(map_eq_zero_iff_eq_zero (spectralMulAlgNorm K L)).mp hxy

Premises used: spectralMulAlgNorm, Iff.mp, map_eq_zero_iff_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 = 0

Tactic:
exact (map_eq_zero_iff_eq_zero (spectralMulAlgNorm K L)).mp hxy

Premises used: spectralMulAlgNorm, Iff.mp, map_eq_zero_iff_eq_zero
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : IsAlgebraic K (x - y)
⊢ spectralNorm K L (x - y) = spectralNorm K L (-x + y)

Tactic:
rw [← spectralNorm_neg, sub_eq_add_neg, neg_add, neg_neg]

Premises used: spectralNorm_neg, sub_eq_add_neg, neg_add, neg_neg
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ IsAlgebraic K (x - y)

Tactic:
Algebra.IsAlgebraic.isAlgebraic (x - y)

Premises used: Algebra.IsAlgebraic.isAlgebraic, HSub.hSub
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ IsAlgebraic K (x - y)

Tactic:
exact Algebra.IsAlgebraic.isAlgebraic (x - y)

Premises used: Algebra.IsAlgebraic.isAlgebraic, HSub.hSub
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 * spectralNorm K L y

Tactic:
simp [← spectralMulAlgNorm_def, map_mul]

Premises used: spectralMulAlgNorm_def, map_mul
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
this : NormedField L := normedField K L
⊢ SeminormedRing L

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
haveI : (this : NormedField L) → NormedAddCommGroup L
⊢ NormedAddCommGroup L

Tactic:
haveI : NormedField L := normedField K L
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
this : NormedField L
⊢ NormedAddCommGroup L

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
have : (this : NormedField L) → SeminormedAddCommGroup L
⊢ SeminormedAddCommGroup L

Tactic:
have : NormedField L := normedField K L
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
this : NormedField L
⊢ SeminormedAddCommGroup L

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
change :
  (spectralAlgNorm K L : (a : L) → ℝ) (r • x) ≤ HMul.hMul (β := ℝ) ‖r‖ ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ)
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖

Tactic:
change spectralAlgNorm K L (r • x) ≤ ‖r‖ * spectralAlgNorm K L x

Premises used: spectralAlgNorm, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ (spectralAlgNorm K L : (a : L) → ℝ) (r • x) ≤ HMul.hMul (β := ℝ) ‖r‖ ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ)

Tactic:
le_of_eq (map_smul_eq_mul _ _ _)

Premises used: SeminormClass.map_smul_eq_mul, le_of_eq
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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
⊢ (spectralAlgNorm K L : (a : L) → ℝ) (r • x) ≤ HMul.hMul (β := ℝ) ‖r‖ ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ)

Tactic:
exact le_of_eq (map_smul_eq_mul _ _ _)

Premises used: SeminormClass.map_smul_eq_mul, le_of_eq
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L_1 : Type v
inst_1 : Field L_1
inst_2 : Algebra K L_1
inst_3 : Algebra.IsAlgebraic K L_1
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
E : Type u_2
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra.IsAlgebraic K L
inst_8 : NormedField E
inst_9 : NormedAlgebra K E
inst_10 : Algebra E L
inst_11 : IsScalarTower K E L
x : NormedField L := normedField K L
x_1 : NormedAlgebra K L := normedAlgebra K L
h : Algebra.IsAlgebraic K E := ⋯
x_2 : E
x_3 : L
hab : ‖x_2 • x_3‖ = ‖x_2‖ * ‖x_3‖
⊢ ‖x_2 • x_3‖ ≤ ‖x_2‖ * ‖x_3‖

Tactic:
apply le_of_eq

Premises used: le_of_eq
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L_1 : Type v
inst_1 : Field L_1
inst_2 : Algebra K L_1
inst_3 : Algebra.IsAlgebraic K L_1
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
E : Type u_2
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra.IsAlgebraic K L
inst_8 : NormedField E
inst_9 : NormedAlgebra K E
inst_10 : Algebra E L
inst_11 : IsScalarTower K E L
x : NormedField L := normedField K L
x_1 : NormedAlgebra K L := normedAlgebra K L
h : Algebra.IsAlgebraic K E := ⋯
x_2 : E
x_3 : L
hab : norm.{u_3} (E := L) ((algebraMap E L : (a : E) → L) x_2 : L) = ‖x_2‖ ∨ x_3 = 0
⊢ ‖x_2 • x_3‖ = ‖x_2‖ * ‖x_3‖

Tactic:
simp only [Algebra.smul_def, norm_mul, mul_eq_mul_right_iff, _root_.norm_eq_zero]

Premises used: norm_eq_zero, mul_eq_mul_right_iff, norm_mul, Algebra.smul_def
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L_1 : Type v
inst_1 : Field L_1
inst_2 : Algebra K L_1
inst_3 : Algebra.IsAlgebraic K L_1
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
E : Type u_2
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra.IsAlgebraic K L
inst_8 : NormedField E
inst_9 : NormedAlgebra K E
inst_10 : Algebra E L
inst_11 : IsScalarTower K E L
x : NormedField L := normedField K L
x_1 : NormedAlgebra K L := normedAlgebra K L
h : Algebra.IsAlgebraic K E := ⋯
x_2 : E
x_3 : L
hab : spectralNorm.{u, u_3} K L ((algebraMap E L : (a : E) → L) x_2 : L) = spectralNorm K E x_2 ∨ x_3 = 0
⊢ norm.{u_3} (E := L) ((algebraMap E L : (a : E) → L) x_2 : L) = ‖x_2‖ ∨ x_3 = 0

Tactic:
simp only [NormedAlgebra.norm_eq_spectralNorm K]

Premises used: NormedAlgebra.norm_eq_spectralNorm
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L_1 : Type v
inst_1 : Field L_1
inst_2 : Algebra K L_1
inst_3 : Algebra.IsAlgebraic K L_1
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
E : Type u_2
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra.IsAlgebraic K L
inst_8 : NormedField E
inst_9 : NormedAlgebra K E
inst_10 : Algebra E L
inst_11 : IsScalarTower K E L
x : NormedField L := normedField K L
x_1 : NormedAlgebra K L := normedAlgebra K L
h : Algebra.IsAlgebraic K E := ⋯
x_2 : E
x_3 : L
⊢ spectralNorm.{u, u_3} K L ((algebraMap E L : (a : E) → L) x_2 : L) = spectralNorm K E x_2 ∨ x_3 = 0

Tactic:
Or.inl <| (spectralNorm.eq_of_tower _).symm

Premises used: spectralNorm.eq_of_tower, Or.inl, Eq.symm
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
R : Type u_1
K : Type u
inst : NontriviallyNormedField K
L_1 : Type v
inst_1 : Field L_1
inst_2 : Algebra K L_1
inst_3 : Algebra.IsAlgebraic K L_1
hu : IsUltrametricDist K
inst_4 : CompleteSpace K
E : Type u_2
L : Type u_3
inst_5 : Field L
inst_6 : Algebra K L
inst_7 : Algebra.IsAlgebraic K L
inst_8 : NormedField E
inst_9 : NormedAlgebra K E
inst_10 : Algebra E L
inst_11 : IsScalarTower K E L
x : NormedField L := normedField K L
x_1 : NormedAlgebra K L := normedAlgebra K L
h : Algebra.IsAlgebraic K E := ⋯
x_2 : E
x_3 : L
⊢ spectralNorm.{u, u_3} K L ((algebraMap E L : (a : E) → L) x_2 : L) = spectralNorm K E x_2 ∨ x_3 = 0

Tactic:
exact Or.inl <| (spectralNorm.eq_of_tower _).symm

Premises used: spectralNorm.eq_of_tower, Or.inl, Eq.symm