awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x : L
n : ℕ
hn : 1 ≤ n
E : IntermediateField K L := K⟮x⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
g : ↥K⟮x⟯ := AdjoinSimple.gen K x
hg : g = AdjoinSimple.gen K x
h_map : HPow.hPow (α := L) ((algebraMap (↥E) L : (a : ↥E) → L) g : L) n = x ^ n
rw :
  spectralNorm K (↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
      (HPow.hPow (α := ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
        ((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)) :
              (a : ↥K⟮x⟯) → ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
            g :
          ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
        n) =
    spectralNorm K ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))
        ((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)) :
              (a : ↥K⟮x⟯) → ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
            g :
          ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))) ^
      n
⊢ spectralNorm K L (x ^ n) = spectralNorm K L x ^ n

Tactic:
rw [← spectralNorm.eq_of_normalClosure _ (IntermediateField.AdjoinSimple.algebraMap_gen K x),
    ← spectralNorm.eq_of_normalClosure (g ^ n) h_map, map_pow, ← hg]

Premises used: map_pow, HPow.hPow, spectralNorm.eq_of_normalClosure, IntermediateField.AdjoinSimple.algebraMap_gen
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x : L
n : ℕ
hn : 1 ≤ n
E : IntermediateField K L := K⟮x⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
g : ↥K⟮x⟯ := AdjoinSimple.gen K x
hg : g = AdjoinSimple.gen K x
h_map : HPow.hPow (α := L) ((algebraMap (↥E) L : (a : ↥E) → L) g : L) n = x ^ n
⊢ spectralNorm K (↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
      (HPow.hPow (α := ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
        ((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)) :
              (a : ↥K⟮x⟯) → ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
            g :
          ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
        n) =
    spectralNorm K ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))
        ((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)) :
              (a : ↥K⟮x⟯) → ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
            g :
          ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))) ^
      n

Tactic:
isPowMul_spectralNorm_of_finiteDimensional_normal _ _
    ((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))) g) hn

Premises used: isPowMul_spectralNorm_of_finiteDimensional_normal, Algebra.algebraMap, IntermediateField.normalClosure, Membership.mem, Subtype, IntermediateField.adjoin, Singleton.singleton, AlgebraicClosure, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x : L
n : ℕ
hn : 1 ≤ n
E : IntermediateField K L := K⟮x⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
g : ↥K⟮x⟯ := AdjoinSimple.gen K x
hg : g = AdjoinSimple.gen K x
h_map : HPow.hPow (α := L) ((algebraMap (↥E) L : (a : ↥E) → L) g : L) n = x ^ n
⊢ spectralNorm K (↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
      (HPow.hPow (α := ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
        ((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)) :
              (a : ↥K⟮x⟯) → ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
            g :
          ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
        n) =
    spectralNorm K ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))
        ((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)) :
              (a : ↥K⟮x⟯) → ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯)))
            g :
          ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))) ^
      n

Tactic:
exact isPowMul_spectralNorm_of_finiteDimensional_normal _ _
    ((algebraMap ↥K⟮x⟯ ↥(normalClosure K (↥K⟮x⟯) (AlgebraicClosure ↥K⟮x⟯))) g) hn

Premises used: isPowMul_spectralNorm_of_finiteDimensional_normal, Algebra.algebraMap, IntermediateField.normalClosure, Membership.mem, Subtype, IntermediateField.adjoin, Singleton.singleton, AlgebraicClosure, DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x y : L
E : IntermediateField K L := K⟮x, y⟯
⊢ FiniteDimensional.{u_2, u_3} K ↥E

Tactic:
haveI h_finiteDimensional_E : FiniteDimensional K E :=
    IntermediateField.finiteDimensional_adjoin_pair (h_alg.isAlgebraic x).isIntegral
       (h_alg.isAlgebraic y).isIntegral
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x y : L
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
⊢ x + y = (algebraMap (↥K⟮x, y⟯) L : (a : ↥K⟮x, y⟯) → L) (gx + gy)

Tactic:
have hxy : x + y = (algebraMap K⟮x, y⟯ L) (gx + gy) := rfl
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x y : L
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
hxy : x + y = (algebraMap (↥K⟮x, y⟯) L : (a : ↥K⟮x, y⟯) → L) (gx + gy)
rw :
  spectralNorm K (↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
      (HAdd.hAdd (α := ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) (β :=
        ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gx :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gy :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))) ≤
    max
      (spectralNorm K ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gx :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))))
      (spectralNorm K ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gy :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))))
⊢ spectralNorm K L (x + y) ≤ max (spectralNorm K L x) (spectralNorm K L y)

Tactic:
rw [hxy, ← spectralNorm.eq_of_normalClosure (gx + gy) hxy,
    ← spectralNorm.eq_of_normalClosure gx (IntermediateField.AdjoinPair.algebraMap_gen₁ K x y),
    ← spectralNorm.eq_of_normalClosure gy (IntermediateField.AdjoinPair.algebraMap_gen₂ K x y),
    _root_.map_add]

Premises used: map_add, IntermediateField.AdjoinPair.algebraMap_gen₁, HAdd.hAdd, spectralNorm.eq_of_normalClosure, IntermediateField.AdjoinPair.algebraMap_gen₂
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x y : L
E : IntermediateField K L := K⟮x, y⟯
h_finiteDimensional_E : FiniteDimensional.{u_2, u_3} K ↥E
gx : ↥K⟮x, y⟯ := AdjoinPair.gen₁ K x y
gy : ↥K⟮x, y⟯ := AdjoinPair.gen₂ K x y
hxy : x + y = (algebraMap (↥K⟮x, y⟯) L : (a : ↥K⟮x, y⟯) → L) (gx + gy)
⊢ spectralNorm K (↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
      (HAdd.hAdd (α := ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))) (β :=
        ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gx :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gy :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))) ≤
    max
      (spectralNorm K ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gx :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))))
      (spectralNorm K ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))
        ((algebraMap ↥K⟮x, y⟯ ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)) :
              (a : ↥K⟮x, y⟯) → ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯)))
            gy :
          ↥(normalClosure K (↥K⟮x, y⟯) (AlgebraicClosure ↥K⟮x, y⟯))))

Tactic:
apply isNonarchimedean_spectralNorm_of_finiteDimensional_normal

Premises used: isNonarchimedean_spectralNorm_of_finiteDimensional_normal
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
x : L
⊢ (spectralAlgNorm 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:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
k : K
⊢ (spectralAlgNorm K L : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) = ‖k‖

Tactic:
spectralNorm_extends k

Premises used: iSup, spectralNorm, dite, spectralNorm_extends, spectralValue
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
⊢ Eq (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) 1 : ℝ) (1 : ℝ)

Tactic:
spectralNorm_one

Premises used: iSup, spectralNorm, dite, spectralNorm_one, spectralValue
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
Goal:
K : Type u_2
inst : NormedField K
L : Type u_3
inst_1 : Field L
inst_2 : Algebra K L
inst_3 : IsUltrametricDist K
h_alg : Algebra.IsAlgebraic K L
⊢ IsPowMul (R := L) (⇑(spectralAlgNorm K L) : (a : L) → ℝ)

Tactic:
isPowMul_spectralNorm

Premises used: iSup, isPowMul_spectralNorm, spectralNorm, dite, spectralValue
-- 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
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x_1 x y : L
⊢ (Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toFun (x * y) ≤
    (Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toFun x *
      (Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toFun y

Tactic:
simp [AddGroupSeminorm.toFun_eq_coe, MulRingSeminorm.toFun_eq_coe]

Premises used: AddGroupSeminorm.toFun_eq_coe, MulRingSeminorm.toFun_eq_coe
-- 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
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x_1 : L
k : K
x : L
rw :
  HMul.hMul (α := ℝ) (β := ℝ)
      (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ)
          ((algebraMap K L : (a : K) → L) k : L) :
        ℝ)
      (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ) x : ℝ) =
    HMul.hMul (β := ℝ) ‖k‖
      (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ) x : ℝ)
⊢ ((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ) (k • x) =
    HMul.hMul (β := ℝ) ‖k‖
      (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ) x : ℝ)

Tactic:
rw [Algebra.smul_def, map_mul]

Premises used: map_mul, Algebra.smul_def
-- 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
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x_1 : L
k : K
x : L
e_a :
  ((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ)
      ((algebraMap K L : (a : K) → L) k : L) =
    ‖k‖
⊢ HMul.hMul (α := ℝ) (β := ℝ)
      (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ)
          ((algebraMap K L : (a : K) → L) k : L) :
        ℝ)
      (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ) x : ℝ) =
    HMul.hMul (β := ℝ) ‖k‖
      (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ) x : ℝ)

Tactic:
congr
-- 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
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x_1 : L
k : K
x : L
e_a :
  Eq (α := ℝ)
    (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ)
        ((algebraMap K L : (a : K) → L) k : L) :
      ℝ)
    ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)
⊢ ((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ)
      ((algebraMap K L : (a : K) → L) k : L) =
    ‖k‖

Tactic:
rw [← hf_ext k]
-- 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
f : AbsoluteValue L ℝ
hf_ext : ∀ (x : K), (f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) x : L) = ‖x‖
x_1 : L
k : K
x : L
⊢ Eq (α := ℝ)
    (((Equiv.invFun MulRingNorm.mulRingNormEquivAbsoluteValue f).toMulRingSeminorm : (a : L) → ℝ)
        ((algebraMap K L : (a : K) → L) k : L) :
      ℝ)
    ((f : (a : L) → ℝ) ((algebraMap K L : (a : K) → L) k : L) : ℝ)

Tactic:
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
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' := ⋯ }
⊢ IsPowMul (R := L) (⇑g : (a : L) → ℝ)

Tactic:
have hg_pow : IsPowMul g := MulRingNorm.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
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) → ℝ)
⊢ Eq (α := ℝ) ((f : (a : L) → ℝ) x : ℝ) ((g : (a : L) → ℝ) x : ℝ)

Tactic:
have hgx : f x = g x := 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
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
rw₂ rw₃ : spectralNorm K L x = spectralNorm K L x
⊢ (f : (a : L) → ℝ) x = spectralNorm K L x

Tactic:
rw [hgx, spectralNorm_unique hg_pow, spectralAlgNorm_def]

Premises used: spectralAlgNorm_def, spectralNorm_unique
-- Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm
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 : ℝ)
rw₃ rw₄ : Eq (α := ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ) ((spectralAlgNorm K L : (a : L) → ℝ) x : ℝ)
⊢ ‖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)]

Premises used: spectralAlgNorm_def, MulAlgebraNorm.coe_AlgebraNorm, NormedAlgebra.toMulAlgebraNorm, spectralNorm_unique, NormedAlgebra.toMulAlgebraNorm_apply, MulRingNorm.isPowMul, MulAlgebraNorm.toMulRingNorm
-- 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_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
rw₄ rw₅ : ‖k‖ * spectralNorm 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

Tactic:
rw [spectralNorm_extends, ← Algebra.smul_def, ← spectralAlgNorm_def,
          map_smul_eq_mul _ _ _, spectralAlgNorm_def]

Premises used: spectralAlgNorm_def, spectralNorm_extends, SeminormClass.map_smul_eq_mul, 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
⊢ ∀ (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]
-- 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
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)
⊢ 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:
rw [seminormFromConst_apply_of_isMul h1 hx' spectralAlgNorm_isPowMul h_mul]

Premises used: seminormFromConst_apply_of_isMul, 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
⊢ 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:
rfl