Module: Mathlib.Analysis.Normed.Unbundled.SpectralNorm

Goal state before:
pp: K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
x : L
E : Type v := id ↥K⟮x⟯
this✝¹ : Field E :=
  id
    (have this := inferInstance;
    this)
this✝ : Module K E :=
  id
    (have this := inferInstance;
    this)
id1 : ↥K⟮x⟯ →ₗ[K] E := LinearMap.id
id2 : E →ₗ[K] ↥K⟮x⟯ := LinearMap.id
hs_norm : RingNorm E :=
  { toFun := fun y ↦ spectralNorm K L ↑(id2 y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n1 : NormedRing E := hs_norm.toNormedRing
N1 : NormedSpace K E :=
  { toSMul := DistribMulAction.toDistribSMul.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯, norm_smul_le := ⋯ }
hf_norm : RingNorm ↥K⟮x⟯ :=
  { toFun := fun y ↦ f ((algebraMap (↥K⟮x⟯) L) y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n2 : NormedRing ↥K⟮x⟯ := hf_norm.toNormedRing
N2 : NormedSpace K ↥K⟮x⟯ :=
  { toSMul := K⟮x⟯.algebra'.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯,
    zero_smul := ⋯, norm_smul_le := ⋯ }
hKx_fin : FiniteDimensional K ↥K⟮x⟯
this : FiniteDimensional K E
Id1 : ↥K⟮x⟯ →L[K] E := { toLinearMap := id1, cont := ⋯ }
⊢ ∃ C₁ C₂,
    ∃ (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x_3 : ↥K[x]), f ↑x_3 ≤ C₁ * (spectralAlgNorm K L) ↑x_3 ∧ (spectralAlgNorm K L) ↑x_3 ≤ C₂ * f ↑x_3

Tactic:
set Id2 : E →L[K] K⟮x⟯ := ⟨id2, id2.continuous_of_finiteDimensional⟩

Goal state after:
K : Type u
inst✝⁴ : NontriviallyNormedField K
L : Type v
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Algebra.IsAlgebraic K L
hu : IsUltrametricDist K
inst✝ : CompleteSpace K
f : AlgebraNorm K L
hf_pm : IsPowMul ⇑f
x : L
E : Type v := id ↥K⟮x⟯
this✝¹ : Field E :=
  id
    (have this := inferInstance;
    this)
this✝ : Module K E :=
  id
    (have this := inferInstance;
    this)
id1 : ↥K⟮x⟯ →ₗ[K] E := LinearMap.id
id2 : E →ₗ[K] ↥K⟮x⟯ := LinearMap.id
hs_norm : RingNorm E :=
  { toFun := fun y ↦ spectralNorm K L ↑(id2 y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n1 : NormedRing E := hs_norm.toNormedRing
N1 : NormedSpace K E :=
  { toSMul := DistribMulAction.toDistribSMul.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯, norm_smul_le := ⋯ }
hf_norm : RingNorm ↥K⟮x⟯ :=
  { toFun := fun y ↦ f ((algebraMap (↥K⟮x⟯) L) y), map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, mul_le' := ⋯,
    eq_zero_of_map_eq_zero' := ⋯ }
n2 : NormedRing ↥K⟮x⟯ := hf_norm.toNormedRing
N2 : NormedSpace K ↥K⟮x⟯ :=
  { toSMul := K⟮x⟯.algebra'.toSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯,
    zero_smul := ⋯, norm_smul_le := ⋯ }
hKx_fin : FiniteDimensional K ↥K⟮x⟯
this : FiniteDimensional K E
Id1 : ↥K⟮x⟯ →L[K] E := { toLinearMap := id1, cont := ⋯ }
Id2 : E →L[K] ↥K⟮x⟯ := { toLinearMap := id2, cont := ⋯ }
⊢ ∃ C₁ C₂,
    ∃ (_ : 0 < C₁) (_ : 0 < C₂),
      ∀ (x_3 : ↥K[x]), f ↑x_3 ≤ C₁ * (spectralAlgNorm K L) ↑x_3 ∧ (spectralAlgNorm K L) ↑x_3 ≤ C₂ * f ↑x_3